Program doğrulamada Rocq neden Lean'den daha iyi

 (joomy.korkutblech.com)
1 puan yazan GN⁺ 3 시간 전 | Henüz yorum yok. | WhatsApp'ta paylaş
  • Matematiksel biçimselleştirmede Lean'in büyümesi belirgin olsa da, çalıştırılabilir program doğrulaması için yerel ortaközyineleme ve çeşitli çıkarım yolları ile birikmiş doğrulama ekosistemine sahip Rocq daha uygundur
  • Rocq, CoInductive ve CoFixpoint ile ortak veriyi tanımlayıp guardedness denetimi yaptıktan sonra bunu gecikmeli yürütme kodu olarak çıkarırken, Lean'de kütüphane kodlaması, yineleyiciler, Thunk veya partial def seçeneklerinden birini tercih etmek gerekir
  • Lean'in iç içe geçmiş tümevarımlı tür denetleyicisi, Rocq'nun kabul ettiği bazı doğrulama ilişkilerini reddeder; bu yüzden JSON şeması örneğinde tek bir Forall₂ ispatını birden fazla ilişkiye bölmek ve ayrı bir tümevarım ilkesi hazırlamak gerekir
  • Rocq, OCaml·Haskell·Rust·C++·WebAssembly gibi program çıkarım yolları ile Iris·CompCert·Interaction Trees gibi doğrulama temelleri sunar; böylece gerçek oyunların doğrulanmış mantığı çalıştırılabilir koda bağlanabilir
  • Yapay zeka ajanları da belge ve örnekler olduğunda Rocq kodu yazabilir; ancak Lean'e geçmek için yalnızca tanımları değil, çıkarım hattını, kütüphaneleri, düzenleyici ve kurumsal geçmişi de değiştirmek gerektiğinden mevcut işte pratik faydası sınırlıdır

Program doğrulaması ölçütüne göre karşılaştırma

  • Karşılaştırma konusu matematiksel biçimselleştirme değil, program doğrulamasıdır; matematik alanında ise Lean gerçekten bir büyüme ivmesine sahiptir
  • “Daha iyi” ifadesi mutlak bir üstünlük anlamına gelmez; yalnızca Rocq'nun şu anda yürütülen işe daha uygun olduğunu ifade eder
  • Yapay zekanın matematik alanındaki başarıları ve Lean'e yönelik ilginin artmasıyla birlikte neden hâlâ Rocq kullanıldığı sıkça sorulmuş, argüman da LangSec açılış konuşmasının slaytlarından yola çıkmıştır

Yerel ortaközyinelemeli türler ve cofixpoint

  • Lean'in coinductive yapısının sunduğu kapsam

    • Lean FRO'dan Wojciech Różowski ve Joachim Breitner tarafından geliştirilen ortaközyinelemeli yüklem desteği, Lean 4.25 içindeki coinductive komutuna dahil edilmiştir
    • Bu özellik bisimulation ve ortaközyinelemeli ispatlar için yararlıdır, ancak Type içinde çalıştırılabilir cofixpoint ya da çıkarılabilir programlar sağlamaz
    • Rocq'nun CoInductive ve CoFixpoint yapıları, çalıştırılabilir ortak veri (codata) yapısını doğrudan Type içinde sunar
    • Lean'de buna karşılık gelen bir kernel bildirimi yoktur; bu yüzden normal fonksiyonlar, yapılar veya kütüphane kodlamaları kullanılmalıdır

  • QPFTypes'ın bildirim kısıtları

    • Alex Keizer'in QPFTypes projesi, genel ortak veri için bir kavram kanıtı paketidir; codata tanımından destructor, corecursor ve bisimulation ilkeleri üretir
    • Rocq'nun CoInductive yapısından farklı olarak bu, kernel bildirimi değil bir kütüphane kodlamasıdır
    • Örnekler, o dönemde desteklenen en güncel sürüm olan Lean 4.25.0'a sabitlenmiş araç zincirini kullanır
    • Rocq'da sıradan olan aşağıdaki üç bildirim, QPFTypes içinde çalışmaz
      • Parametresiz ortak veri, bir uygulama hatası nedeniyle başarısız olur
      • tree ve forest gibi karşılıklı ortaközyinelemeli bildirimler, Lean'in mutual block kısıtları nedeniyle desteklenmez
      • Her adımda clock indeksinin ilerlediği istream gibi indeksli ortaközyinelemeli aileler, QPF'nin kendi sınırları nedeniyle desteklenmez
    • Protokoller, adımlar, boyutlar ve durum makinelerinde de indeksli ortaközyinelemeli desenler kullanılır; ancak QPFTypes'ın basit, karşılıklı olmayan ve indekslenmemiş kapsamının dışına çıkıldığında ya düşük seviyeli MvQPF.Cofix.corec ve bisim API'leri doğrudan kullanılmalı ya da bunu uygulamak mümkün olmaz
    • Rocq'da da guardedness denetleyicisi ile uğraşmak zordur, ancak yukarıdaki örnekler ek kodlama olmadan bildirilebilir
    • Paco ve Damien Pous'nun coinduction kütüphanesi ortaközyinelemeli yüklemler ve ilişki ispatlarını destekler, ancak programlar için CoFixpoint yerine geçmez

  • Çıkarılan programlardaki fark

    • Rocq'nun yerel cofixpoint yapısı gerçek tembel OCaml değerleri olarak çıkarılır
    • game tree library içindeki unfold_cotree, Lazy.t ile sarılmış bir ağaç ve özyinelemeli gecikmeli üretim fonksiyonu hâline gelir
    • Ortaya çıkan sonuç, bir insanın doğrudan yazabileceği tembel ağaç yapısına yakındır
    • QPFTypes'ta oluşturma ve gözlemleme MvQPF.Cofix.corec ile MvQPF.Cofix.dest üzerinden yapılır; çıkarılan program da genelleştirilmiş Cofix gösterimini korur
    • BadCoinduction.lean içinde Colist, Cotree, üretilen arayüz, parametresiz, karşılıklı ve indeksli ortak veri için başarısız örnekler ile yeniden üretim için QPFTypes commit'i ve komutları yer alır

Lean'de seçilebilecek alternatifler

  • Stream ve iterator'ler

    • mathlib'deki Stream', Nat → α fonksiyonudur
    • n konumundaki öğeyi hesaplayabilir ve corecursor, extensionality, bisimulation ve corecursion yardımcı teoremleri sunar
    • Ancak kuyruğu başka bir stream olan gecikmeli bir üretici değildir ve keyfi karşılıklı ya da indeksli codata'yı da çözmez
    • Açık durum ve step fonksiyonu kullanan bir durum makinesi de corecursor rolü oynayabilir
    • Lean'in Iter yapısı, istek üzerine her seferinde bir adım hesaplayan sıralı bir arayüzdür
    • Iterator'ler, değer ürettiğini veya sonlandığını garanti eden Productive kanıtına sahip olabilir; bu Iter.repeat için zaten sağlanır
    • Kullanıcı tanımlı iterator'lerde step arayüzünü, invariant'ları ve gerekirse üretkenlik kanıtını doğrudan sizin sağlamanız gerekir
    • Rocq'un CoFixpoint yapısı özyinelemeli çağrıların guardedness'ını denetler ve durum makinesi ile sequence arasında ayrı bir bağlama işi olmadan coinductive değer döndürür

  • Thunk, partial def, unsafe def

    • Lean'in Thunk yapısı derlenmiş kodda ilk zorlandığında hesaplama yapar ve sonucu önbelleğe alır, ancak koindüksiyon sağlamaz
    • Mantıkta Unit → α olarak göründüğü için tam tanımı ispatlarda kullanabilirsiniz, ancak önbellek görünmez
    • Özyinelemeye izin vermez ve özyinelemenin sonunda gerçekten bir üretici üretip üretmediğini de denetlemez
    • Rocq'un extraction kodu da çalışma zamanında tembellik kullanır, ancak önce guardedness denetiminden geçer
    • partial def, özyinelemeli gövdeyi çalıştırabilir ama mantıkta yalnızca opak bir sabit bırakır
    • Sonlanma ya da üretkenliği denetlemediği için hem doğal sayı üreticilerini hem de anında sonsuz özyinelemeye giren üreticileri kabul eder
    • unsafe def de çalıştırılabilir, ancak theorem-safe bildirimlerde ona başvurulamaz
    • Batteries'nin MLList yapısı; özel unsafe lazy uygulama, opak açık arayüz ve partial def ile yazılmış fix ve iterate üreticilerini birleştirir
    • Bu tür üreticiler, gözlemlenen Rocq cofixpoint'leri gibi ispatlarda açımlanamaz
    • partial_fixpoint denklemleri korur, ancak üretici ile thunk'u birleştiren özyinelemeyi kabul etmez
    • QPFTypes, opaklıktan kaçınmak için corecursor ve bisimulation ilkeleri sunar, ancak bunun karşılığında genelleştirilmiş Cofix gösterimini ve bildirim kısıtlarını kabul etmeniz gerekir

Efektli ve sonlanmayan programlar

  • Interaction Trees, efektli ve sonlanmayabilecek programları koindüktif ağaçlar olarak ifade eder
    • Aynı ağaçla program yazabilir, yorumlayabilir ve extraction yapabilir, ayrıca genellikle weak bisimulation dahil denklemleri ispatlayabilirsiniz
  • Stream' ve Iter yalnızca sequence sağladığı için efektler için gerekli olan dallanan continuation yapısını ifade edemez
  • Thunk ve partial def ile efekt ağaçlarını çalıştırmak, özyinelemeli üreticileri ispatlara karşı opak hale getirir; hesaplama ve ispatı birlikte desteklemek için codata kütüphanesi encoding'i gerekir
  • MIT PLV'nin lean4-itree projesi, Mathlib'in PFunctor.M final coalgebra'sı ile Interaction Trees'i uygular
  • PolyFun, handler, özyinelemeli prosedürler, yürütme izleri, strong/weak bisimulation ile monad ve iteration yasalarının ispatlarını ekler
    • Lean'de ağaçları hem hesaplayabilir hem ispatlayabilirsiniz, ancak bu hâlâ kütüphane içinde encode edilmiş bir M-type'tır
    • Yerel codata bildirimi yoktur ve doğrudan lazy programlar yerine genel temsil korunur
  • HITrees da bu kısıtı aşmaz
    • Lean'de yerel koindüktif tipler olmadığı için ITrees'in koindüktif Delay-monad yaklaşımını kullanmaz
    • Ağaçlar indüktiftir ve sonlanmama yüksek dereceli bir özyineleme efekti olur
    • Özyinelemeli hesaplama, gözlemlenip açımlanabilen sonsuz bir ağaç değil; handler efektleri yorumladığında anlam kazanan bir şeydir
    • Monadic interpretation ile çalıştırabilir ve durum makinesi yorumu ile ispatlayabilirsiniz, ancak HITree'nin denklem teorisi genel özyineleme açılım denklemlerini sağlamaz
  • Rocq; codata bildirimi, guarded producer, gözleme dayalı akıl yürütme ve doğrudan lazy kod extraction'ını tek bir akışta destekler

İç içe geçmiş tümevarımlı tipler ve yüklemler

  • JSON şema doğrulama örneği

    • Lean birden fazla iç içe geçmiş tümevarımlı tanıma izin veriyor, ancak Rocq'un kabul ettiği bazı tanımları reddediyor
    • Bu fark A Rose Tree Is Blooming'de kullanıldı ve daha küçük bir JSON şema örneğiyle yeniden üretilebiliyor
    • JSON ve şemanın kendisi iki dilde de sorunsuz biçimde tanımlanabiliyor
    • Nesne şeması doğrulamada alan adlarının eşleştiğini ve her JSON değerinin karşılık gelen alt şema için geçerli olup olmadığını çiftler halinde kontrol etmek gerekiyor
    • Rocq, ad eşitliği ile özyinelemeli doğrulamayı tek bir Forall2 türetiminde saklayabiliyor
    • Rocq 9.0, özyinelemeli ortaya çıkışın çevresindeki tuple-pattern lambda'yı strict positivity ihlali olarak reddediyor, ancak pattern yerine projection kullanılırsa derleniyor
    • Lean 4.32.1, aynı nesne kurucusunda özyinelemeli ortaya çıkış hem Forall₂ hem de And içinden geçtiğinde içteki And ifadesini hatalı iç içe geçmiş tümevarımlı veri tipi olarak reddediyor
    • Forall₂ ParRed, And·Exists üzerinden doğrudan özyineleme ve Forall₂ (fun sf jf => Valid sf.2 jf.2) gibi bitişik biçimlere izin veriyor
    • İlişki parametresinin kurucu yerel değişkeni env'yi yakaladığı Forall₂ (Eval env), Forall₂ aşamasında başarısız oluyor

  • Geçici çözümler ve ispat maliyeti

    • Lean'de nesne doğrulama iki Forall₂ türetimine bölünebiliyor
      • biri alan adlarının eşitliğini koruyor
      • diğeri karşılık gelen değerlerin özyinelemeli doğrulamasını koruyor
    • Ayrı indeksler veya uzunluk ispatları olmadan liste yapısını korumak ve head kaldırmayı da yapısal olarak ispatlamak mümkün, ancak her iki türetimi de parçalamak gerekiyor
    • İlişki ayrıldığında her ad eşitliği ile özyinelemeli doğrulamanın bir çift olarak bağlandığı tek bir ispat nesnesi kayboluyor
    • Karşılıklı ValidFields ilişkisiyle bu bağ yeniden kurulabiliyor, ancak Lean'in induction taktiği karşılıklı tümevarımlı tipleri desteklemiyor ve üretilen recursor da her ilişki için motive istiyor
    • Kullanıcı tanımlı bir tümevarım teoremi oluşturmak bu kurulumu gizleyebiliyor
    • Rocq standart Forall2 gösterimini koruyor ve karşılıklı tanım gerektiğinde Scheme ile birleşik ilkeyi üretebiliyor
    • Lean de indeks tabanlı encoding olmadan aynı önermeyi ifade edebiliyor, ancak bildirimleri yeniden düzenlemek ve daha fazla ispat altyapısı kurmak gerekiyor
    • Tam karşılaştırma dosyaları Rocq 9.0.0 için NestedPain.v ve Lean 4.32.1 için NestedPain.lean; Lean'deki beklenen başarısızlıklar derleme sırasında #guard_msgs ile kontrol ediliyor

  • İç içe geçmiş argümanlar için güçlü tümevarım ilkeleri

    • Term'ün list Term içermesi durumunda olduğu gibi, iç içe geçmiş veride öğe başına varsayımların gerektiği ispatlarda iki sistemde de daha güçlü bir recursor gerekti
    • Rocq 9.2, nesting type için All yüklemi ve teoremini kaydederse iç içe geçmiş argümanlar için tümevarım varsayımları üretiyor
    • Standart kütüphane bunu varsayılan olarak kaydetmediği için Term bildiriminden önce Scheme All for list. satırını eklemek gerekiyor
    • Üretilen Term_ind ve Term_rect, app durumunda list_all Term P l varsayımını alıyor ve gövde list_all_forall çağırıyor
    • Scheme All for Forall2. eklenirse ParRed_ind de Forall2 ParRed args args' öncülü için tümevarım varsayımları sağlıyor
    • Kayıt yapılmazsa mevcut zayıf ilke ile birlikte [register-all] uyarısı çıkıyor
    • Lean'de ise güçlü recursor'ü hâlâ elle sağlamak gerekiyor

Program çıkarımı seçenekleri

  • Lean standart araç zinciri kendi runtime'ı üzerinden derleme yapıyor; Lean kütüphaneleri üretmek ve runtime tasarımı uygunsa bu avantajlı olabiliyor
  • Kim Morrison'ın doğrulanmış lean-zip, saf Rust miniz_oxide'dan daha hızlı sıkıştırma yapabildiği için performans etkileyici
  • Ancak Lean birden fazla alternatif extraction backend'i sunmuyor ve mevcut derleme hattında şu anda uçtan uca doğruluk ispatı bulunmuyor
    • Kiran Gopinathan'ın bulduğu runtime hatası gibi nadir sorunlar ortaya çıkabiliyor
    • Üretilen kod runtime'a özelleştirilmiş ve insanlar tarafından okunmak için tasarlanmamış
  • Rocq, güven temeli ile okunabilirlik arasında farklı ödünleşimler sunan birden fazla yola sahip

Doğrulanmış mantığı çalıştıran oyunlar

  • Rocq'ta çalışan programla aynı kaynak kodun özellikleri makineyle doğrulandıktan sonra, Crane ile mantık ve event loop C++'a çıkarılıyor ve rocq-crane-sdl2 ile SDL2'ye bağlanıyor

  • Rocqman

    • Rocqman, frame loop'un kullandığı oyun durumu geçişlerini ispatlıyor
      • skor azalmaz
      • can ve kalan toplanabilirler artmaz
      • bitiş durumu tick'in sabit noktasıdır
      • duraklatma ve bitiş ekranı geçişlerini kontrol eder

  • Rocqsweeper

    • Rocqsweeper, Minesweeper kurallarını ve girdi katmanını ispatlıyor
      • ilk tıklama güvenlidir
      • bayrak yerleştirme mayın ve komşuluk verisini korur
      • flood fill mayınları korur ve gizli güvenli hücreleri artırmaz
      • imleç sınırların dışına çıkmaz
      • fare olayları beklenen hücre olarak yorumlanır

  • Reversirocq

    • Reversirocq, Charles C. Norton'ın eklediği Reversi kuralları ile aynı game tree library içindeki ortak tümevarımlı alpha-beta yapay zeka kullanıyor
    • Teoremler yasal hamlelerin listelenmesini ve oyun sonucunu ele alıyor; aranan sonlu prefix üzerinde alpha-beta ile minimax'ı ilişkilendiriyor

  • Doğrulama sınırı

    • İspat sınırı Rocq kaynağında sona eriyor; SDL·Crane·üretilen C++·native runtime buna dahil değil
    • Sınırın içinde, çalışan programdan ayrı bir modelin değil, gerçek çalışan mantığın özellikleri ispatlanıyor

Rocq program doğrulama ekosistemi

  • Program gösterimi soyutlaması

    • Interaction Trees: dış olayların koindüktif ağaçlarıyla etkili ve sonlanmayabilen programları ifade eder; saf olmayan kod için belirtimsel anlambilim ve denklemsel akıl yürütme sağlar
    • Choice Trees: içsel nedensiz seçimleri ekleyerek eşzamanlılık gibi nedensiz sistemleri modeller

  • Program doğrulama çerçeveleri

    • Iris: durum ve eşzamanlı programlar için yüksek dereceli concurrent separation logic çerçevesidir
    • Iris-Lean da hızla gelişiyor ve birçok özelliği destekliyor, ancak Rocq Iris kadar yaygın kullanılmadı
    • CFML: OCaml kaynak kodunu Rocq'ye aktarır, characteristic formula üretir ve yüksek dereceli separation logic belirtimleri için taktikler sunar
    • Perennial: eşzamanlılık, çökme güvenli depolama ve dağıtık sistemleri doğrulayan Iris tabanlı bir çerçevedir; Goose ile Go'nun bir alt kümesindeki çalışan programlarla bağ kurar
    • VST: CompCert anlambilimine dayanan, C programlarının işlevsel doğruluğunu kanıtlayan Verified Software Toolchain'dir
    • BRiCk: gerçek C++ programları için bir program mantığı ve araç zinciridir

  • Rocq arka ucu veya bileşenleri kullanan araçlar

    • Frama-C: C analizi ve tümdengelimli doğrulama platformudur; proof obligation'ları Rocq'ye aktarabilir
    • Why3: kendi dilindeki hedefleri birden çok kanıtlayıcıya gönderir ve Rocq için etkileşimli proof obligation'lar dışa aktarabilir
    • Cerberus: pratik, büyük ölçekli bir C alt kümesinin yürütülebilir biçimsel anlambilimidir; CHERI C bellek modeli için Rocq uygulaması vardır

  • Gerçek dillerin anlambilimi ve doğrulanmış derleyiciler

    • CompCert: biçimsel olarak doğrulanmış, optimize eden bir C derleyicisidir
    • Vellvm: LLVM IR için Rocq belirtimi ve soyut anlambilim sağlar; ayrıca bunu rafine ettiği kanıtlanmış yürütülebilir bir yorumlayıcı sunar
    • Vélus: Lustre'dan CompCert'in Clight'ına giden doğrulanmış bir derleyicidir
    • WasmCert: WebAssembly'nin mekanikleştirilmiş biçimsel anlambilimidir
    • JSCert: ECMAScript 5 belirtimini izleyen bir JavaScript biçimsel anlambilimidir

  • Çeviri tabanlı hafif doğrulama

    • hs-to-coq: Haskell kaynak kodunu Rocq'ye çevirir
    • rocq-of-ocaml: OCaml kaynak kodunu Rocq'ye çevirir
    • rocq-of-python: Python kaynak kodunu Rocq'ye çevirir
    • rocq-of-rust: Rust kaynak kodunu Rocq'ye çevirir
    • Aeneas: borrow check'i geçen Rust kodunu doğrulama için saf fonksiyon modellerine dönüştürür; ayrıca Lean hedefini de destekler

  • Program sentezi ve parsing

    • Fiat Crypto: tarayıcılarda ve TLS kütüphanelerinde kullanılabilecek yüksek performanslı kriptografik aritmetiği correct-by-construction yöntemiyle türetir
    • Rupicola: düşük seviyeli işlevsel Gallina programlarını zorunlu Bedrock2 programlarına dönüştüren ilişkisel bir derleme aracıdır
    • Narcissus: ikili biçimler için correct-by-construction encoder ve decoder türetir
    • Verbatim: düzenli ifade tabanlı, doğrulanmış bir lexer'dır
    • CoStar: ALL(*) algoritmasına dayalı, doğrulanmış bir parser'dır

  • Bakım durumu

    • Bazı projeler aktif olarak sürdürülmüyor, ancak bunları ajanlara bırakarak yeniden derleyip çalıştırmak mümkün oldu
    • Gerekli tek bir bileşen kısa sürede Lean'e taşınabilse bile, tüm ekosistemin biriktirdiği özellikler ve kullanım geçmişi otomatik olarak taşınmaz

Regülasyon ve sertifikasyon geçmişi

  • Regülatif kabul konusunda doğrudan sertifikasyon deneyimi yok; bu özellikle Avrupa'daki uygulayıcılar için daha önemli olabilir
  • Fransa ANSSI, Common Criteria değerlendirmelerinde Rocq kullanımına ilişkin kriterleri yayımladı
  • CompCert, AbsInt'in Airbus yönergeleri doğrultusunda yürüttüğü çalışmalar sayesinde 2026 ATR 42/72 uçağındaki MFC_NG bilgisayarı için başarıyla qualification aldığını belirtiyor
  • Bir Lean portunun aynı ortamda hangi gereksinimleri karşılaması gerektiği bilinmiyor; temiz bir port yapılsa bile mevcut sertifikasyon geçmişi otomatik olarak devralınmaz

Yapay zeka ajanları ve geçiş maliyeti

  • Yapay zeka ajanlarının yalnızca Lean'i iyi yazdığı varsayımının aksine, Rocq kodu da yeterince iyi yazılabilir
  • Rocq, 1980'lerin sonlarından beri var olduğundan çok sayıda kod ve belge birikmiştir
  • Güncel modeller, belge ve örnek verildiğinde alışık olmadıkları dillere de iyi uyum sağladığından, yalnızca popüler dilleri bilmeleri proof assistant değiştirmek için uzun vadeli bir gerekçe oluşturmaz
  • Lean tarafında da mvcgen ve Velvet gibi ciddi program doğrulama çalışmaları yürütülüyor
  • Mevcut çalışmayı Lean'e taşımak için tanımları yeniden kurmak ve çıkarım hattı, kütüphaneler ile kurumsal geçmişi değiştirmek gerektiğinden, şu anda Rocq daha uygun

İlgili okumalar

Henüz yorum yok.

Henüz yorum yok.