Mengapa Rocq Lebih Baik daripada Lean untuk Verifikasi Program

 (joomy.korkutblech.com)
1 poin oleh GN⁺ 2 jam lalu | Belum ada komentar. | Bagikan ke WhatsApp
  • Meski pertumbuhan Lean dalam formalisasi matematika terlihat jelas, untuk verifikasi program yang dapat dieksekusi, Rocq lebih cocok karena memiliki koinduksi native, beragam jalur ekstraksi, dan ekosistem verifikasi yang telah terakumulasi
  • Rocq mendeklarasikan codata dengan CoInductive dan CoFixpoint, memeriksa guardedness, lalu mengekstraknya sebagai kode evaluasi tertunda, sedangkan di Lean harus memilih salah satu dari encoding pustaka, iterator, Thunk, atau partial def
  • Pemeriksa tipe induktif bersarang di Lean menolak sebagian relasi verifikasi yang diizinkan Rocq, sehingga pada kasus skema JSON satu pembuktian Forall₂ harus dipecah menjadi beberapa relasi dan prinsip induksi terpisah harus disiapkan
  • Rocq menyediakan jalur ekstraksi program seperti OCaml, Haskell, Rust, C++, dan WebAssembly, serta fondasi verifikasi seperti Iris, CompCert, dan Interaction Trees, sehingga logika terverifikasi dari game nyata dapat dihubungkan ke kode yang dieksekusi
  • Agen AI juga dapat menulis kode Rocq bila tersedia dokumentasi dan contoh, sementara beralih ke Lean mengharuskan penggantian bukan hanya definisi tetapi juga pipeline ekstraksi, pustaka, serta riwayat regulasi dan kelembagaan, sehingga untuk pekerjaan saat ini manfaat nyatanya kecil

Perbandingan berdasarkan verifikasi program

  • Yang dibandingkan bukan formalisasi matematika melainkan verifikasi program; di bidang matematika Lean memang memiliki momentum pertumbuhan yang nyata
  • “Lebih baik” bukan berarti keunggulan absolut, melainkan bahwa Rocq lebih sesuai untuk pekerjaan yang sedang dikerjakan saat ini
  • Seiring meningkatnya capaian AI di bidang matematika dan minat terhadap Lean, penulis sering ditanya mengapa tetap menggunakan Rocq, dan argumen ini berangkat dari slide presentasi keynote LangSec

Tipe koinduktif native dan cofixpoint

  • Cakupan yang disediakan coinductive di Lean

    • Dukungan predikat koinduktif yang dikembangkan Wojciech Różowski dan Joachim Breitner dari Lean FRO telah dimasukkan ke perintah coinductive di Lean 4.25
    • Fitur ini berguna untuk bisimulation dan pembuktian koinduktif, tetapi tidak menyediakan cofixpoint yang dapat dieksekusi di Type atau program yang bisa diekstrak
    • CoInductive dan CoFixpoint di Rocq langsung menyediakan codata yang dapat dieksekusi di Type
    • Lean tidak memiliki deklarasi kernel yang setara, sehingga harus memakai fungsi/struktur biasa atau encoding pustaka

  • Batasan deklarasi QPFTypes

    • QPFTypes karya Alex Keizer adalah paket proof-of-concept untuk codata umum yang menghasilkan destructor, corecursor, dan prinsip bisimulation dari spesifikasi codata
    • Berbeda dari CoInductive di Rocq, ini adalah encoding pustaka, bukan deklarasi kernel
    • Contohnya menggunakan toolchain tetap pada Lean 4.25.0, yang saat itu merupakan versi dukungan terbaru
    • Di Rocq, tiga deklarasi berikut yang biasa saja tidak berjalan di QPFTypes
      • Codata tanpa parameter gagal karena bug implementasi
      • Deklarasi koinduktif mutual seperti tree dan forest tidak didukung karena batasan mutual block di Lean
      • Keluarga koinduktif berindeks seperti istream, yang indeks clock-nya maju di setiap langkah, tidak didukung karena keterbatasan QPF itu sendiri
    • Pola koinduktif berindeks juga dipakai pada protokol, tahap, ukuran, dan state machine, tetapi bila keluar dari cakupan sederhana, non-mutual, dan non-indeks milik QPFTypes, pengguna harus langsung memakai API MvQPF.Cofix.corec dan bisim tingkat rendah, atau memang tidak bisa diimplementasikan
    • Rocq juga tidak mudah dalam hal pemeriksa guardedness, tetapi kasus-kasus di atas tetap bisa dideklarasikan tanpa encoding terpisah
    • Paco dan coinduction karya Damien Pous mendukung predikat koinduktif dan pembuktian relasi, tetapi tidak menggantikan CoFixpoint untuk program

  • Perbedaan pada program hasil ekstraksi

    • CoFixpoint native Rocq diekstrak menjadi nilai OCaml lazy yang nyata
    • unfold_cotree dari game tree library menjadi tree yang dibungkus Lazy.t dan fungsi pembangkit lazy yang rekursif
    • Hasilnya dekat dengan struktur tree lazy yang kemungkinan akan ditulis langsung oleh manusia
    • Di QPFTypes, konstruksi dan observasi melewati MvQPF.Cofix.corec dan MvQPF.Cofix.dest, dan program hasil ekstraksinya juga mempertahankan representasi Cofix yang digeneralisasi
    • BadCoinduction.lean memuat Colist, Cotree, antarmuka yang dihasilkan, contoh kegagalan codata tanpa parameter, mutual, dan berindeks, serta commit QPFTypes dan perintah untuk reproduksi

Alternatif yang bisa dipilih di Lean

  • Stream dan iterator

    • Stream' di mathlib adalah fungsi Nat → α
    • Dapat menghitung elemen pada posisi n dan menyediakan corecursor, ekstensialitas, bisimulation, dan lemma bantu koinduksi
    • Namun, ini bukan konstruktor malas yang ekornya berupa stream lain, dan juga tidak menyelesaikan kodata mutual maupun terindeks yang arbitrer
    • Mesin status yang menggunakan state eksplisit dan fungsi step juga dapat berperan sebagai corecursor
    • Iter di Lean adalah antarmuka sekuensial yang menghitung satu langkah setiap kali diminta
    • Iterator dapat memiliki pembuktian Productive yang menjamin menghasilkan nilai atau berhenti, dan Iter.repeat sudah menyediakannya
    • Untuk iterator buatan pengguna, antarmuka step, invarian, dan bila perlu pembuktian produktivitas harus disediakan sendiri
    • CoFixpoint di Rocq memeriksa guardedness dari pemanggilan rekursif dan mengembalikan nilai koinduktif tanpa perlu pekerjaan penghubung terpisah antara mesin status dan sekuens

  • Thunk, partial def, unsafe def

    • Thunk di Lean menghitung saat pertama kali dipaksa dalam kode hasil kompilasi dan menyimpan hasilnya dalam cache, tetapi tidak menyediakan koinduksi
    • Dalam logika, ini tampak sebagai Unit → α, sehingga definisi total dapat digunakan dalam pembuktian, tetapi cache tidak terlihat
    • Ini juga tidak mengizinkan rekursi maupun memeriksa apakah rekursi pada akhirnya menghasilkan konstruktor
    • Kode hasil ekstraksi Rocq juga menggunakan kelambatan runtime, tetapi terlebih dahulu lolos pemeriksaan guardedness
    • partial def dapat menjalankan body rekursif, tetapi dalam logika hanya menyisakan konstanta opak
    • Karena tidak memeriksa terminasi atau produktivitas, ini mengizinkan baik penghasil bilangan alami maupun penghasil yang langsung masuk ke rekursi tak hingga
    • unsafe def juga dapat dijalankan, tetapi tidak dapat dirujuk dalam deklarasi yang theorem-safe
    • MLList di Batteries menggabungkan implementasi lazy unsafe privat, antarmuka publik opak, dan penghasil fix serta iterate yang ditulis dengan partial def
    • Penghasil seperti ini tidak dapat dibuka dalam pembuktian seperti cofixpoint Rocq yang dapat diamati
    • partial_fixpoint mempertahankan persamaan, tetapi tidak menerima rekursi yang menggabungkan konstruktor dan thunk
    • QPFTypes menyediakan prinsip corecursor dan bisimulation untuk menghindari keopakan, tetapi harus menerima representasi Cofix yang digeneralisasi dan batasan deklarasi

Program berefek dan tidak berhenti

  • Interaction Trees merepresentasikan program yang berefek dan mungkin tidak berhenti sebagai pohon koinduktif
    • Dengan pohon yang sama, program dapat ditulis, diinterpretasikan, dan diekstrak, dan biasanya persamaan hingga weak bisimulation juga dapat dibuktikan
  • Stream' dan Iter hanya menyediakan sekuens, sehingga tidak dapat merepresentasikan branching continuation yang dibutuhkan oleh efek
  • Jika pohon efek dijalankan dengan Thunk dan partial def, penghasil rekursif menjadi opak bagi pembuktian, dan untuk mendukung komputasi serta pembuktian sekaligus dibutuhkan encoding library kodata
  • lean4-itree dari MIT PLV mengimplementasikan Interaction Trees dengan final coalgebra PFunctor.M dari Mathlib
  • PolyFun menambahkan handler, prosedur rekursif, jejak eksekusi, strong/weak bisimulation, serta pembuktian hukum monad dan iteration
    • Pohon dapat dihitung dan dibuktikan di Lean, tetapi tetap merupakan M-type yang dienkodekan sebagai library
    • Tidak ada deklarasi kodata native, dan representasi umum tetap dipertahankan alih-alih program lazy yang langsung
  • HITrees juga tidak menghindari keterbatasan ini
    • Karena Lean tidak memiliki tipe koinduktif native, ini tidak menggunakan pendekatan Delay-monad koinduktif dari ITrees
    • Pohonnya bersifat induktif, dan non-terminasi menjadi efek rekursif tingkat tinggi
    • Komputasi rekursif memperoleh makna saat handler menginterpretasikan efek, bukan sebagai pohon tak hingga yang dapat diamati dan dibuka
    • Ini dapat dijalankan dengan interpretasi monadik dan dibuktikan dengan interpretasi mesin status, tetapi teori persamaan HITree tidak menyediakan persamaan pembukaan rekursif yang umum
  • Rocq mendukung deklarasi kodata, producer yang guarded, penalaran berbasis observasi, dan ekstraksi langsung kode lazy dalam satu alur

Tipe induktif bertingkat dan predikat

  • Kasus validasi skema JSON

    • Lean mengizinkan beberapa definisi induktif bertingkat, tetapi menolak sebagian definisi yang diterima Rocq
    • Perbedaan ini digunakan dalam A Rose Tree Is Blooming, dan dapat direproduksi dengan contoh skema JSON yang lebih kecil
    • JSON dan skema itu sendiri dapat didefinisikan tanpa masalah di kedua bahasa
    • Dalam validasi skema objek, kita harus memeriksa per pasangan apakah nama field cocok dan apakah setiap nilai JSON valid terhadap sub-skema yang bersesuaian
    • Rocq dapat menyimpan kesamaan nama dan validasi rekursif dalam satu derivasi Forall2
    • Rocq 9.0 menolak lambda tuple-pattern di sekitar kemunculan rekursif sebagai pelanggaran strict positivity, tetapi jika menggunakan projection alih-alih pattern maka kode dapat dikompilasi
    • Lean 4.32.1 menolak And di bagian dalam sebagai tipe data induktif bertingkat yang tidak valid jika kemunculan rekursif dalam konstruktor objek yang sama melewati Forall₂ dan And
    • Forall₂ ParRed, rekursi langsung melalui And·Exists, dan bentuk yang berdekatan seperti Forall₂ (fun sf jf => Valid sf.2 jf.2) diizinkan
    • Forall₂ (Eval env) yang parameter relasinya menangkap variabel lokal konstruktor env gagal pada tahap Forall₂

  • Cara mem-bypass dan biaya pembuktian

    • Di Lean, validasi objek dapat dipecah menjadi dua derivasi Forall₂
      • Satu mempertahankan kesamaan nama field
      • Yang lain mempertahankan validasi rekursif nilai yang bersesuaian
    • Tanpa indeks terpisah atau bukti panjang, struktur list tetap terjaga dan penghapusan head juga bisa dibuktikan secara struktural, tetapi kedua derivasi itu harus diurai
    • Dengan memisahkan relasi, kita kehilangan satu objek bukti yang mengikat setiap kesamaan nama dan validasi rekursif sebagai sepasang
    • Ini dapat dipulihkan dengan relasi mutual ValidFields, tetapi taktik induction di Lean tidak mendukung tipe induktif mutual dan recursor yang dihasilkan juga menuntut motive per relasi
    • Jika membuat teorema induksi buatan pengguna, pengaturan ini bisa disembunyikan
    • Rocq mempertahankan representasi Forall2 standar, dan jika definisi mutual diperlukan, prinsip gabungan dapat dibuat dengan Scheme
    • Lean juga dapat mengekspresikan proposisi yang sama tanpa encoding berbasis indeks, tetapi deklarasi harus disusun ulang dan lebih banyak perangkat pembuktian perlu dibuat
    • File perbandingan lengkap tersedia di NestedPain.v untuk Rocq 9.0.0 dan NestedPain.lean untuk Lean 4.32.1, dan kegagalan yang diharapkan di Lean diperiksa saat kompilasi dengan #guard_msgs

  • Prinsip induksi kuat untuk argumen bertingkat

    • Dalam pembuktian yang memerlukan asumsi per elemen untuk data bertingkat, seperti saat Term memuat list Term, kedua sistem sama-sama memerlukan recursor yang lebih kuat
    • Rocq 9.2 menghasilkan asumsi induksi untuk argumen bertingkat jika predikat dan teorema All didaftarkan pada nesting type
    • Standard library tidak mendaftarkannya secara bawaan, jadi perlu menambahkan satu baris Scheme All for list. sebelum deklarasi Term
    • Term_ind dan Term_rect yang dihasilkan memperoleh asumsi list_all Term P l pada kasus app, dan isi buktinya memanggil list_all_forall
    • Jika menambahkan Scheme All for Forall2., maka ParRed_ind juga memberikan asumsi induksi untuk premis Forall2 ParRed args args'
    • Jika tidak didaftarkan, akan muncul peringatan [register-all] bersama prinsip lemah yang lama
    • Di Lean, recursor kuat seperti itu masih harus disiapkan secara manual

Opsi ekstraksi program

  • Toolchain standar Lean mengompilasi melalui runtime miliknya sendiri, yang menjadi keunggulan jika Anda membangun library Lean dan desain runtime tersebut cocok
  • lean-zip terverifikasi buatan Kim Morrison bahkan dapat mengompresi lebih cepat daripada miniz_oxide Rust murni, sehingga performanya mengesankan
  • Namun, Lean tidak menyediakan banyak backend ekstraksi alternatif, dan pipeline kompilasi saat ini tidak memiliki bukti ketepatan end-to-end
    • Masalah langka seperti bug runtime yang ditemukan Kiran Gopinathan dapat terjadi
    • Kode yang dihasilkan dioptimalkan untuk runtime dan tidak dirancang agar mudah dibaca manusia
  • Rocq memiliki beberapa jalur yang menawarkan kompromi berbeda antara basis kepercayaan dan keterbacaan

Game yang menjalankan logika terverifikasi

  • Di Rocq, setelah memverifikasi secara mekanis properti dari source code yang sama dengan program yang dijalankan, logika dan event loop diekstrak ke C++ dengan Crane lalu dihubungkan ke SDL2 dengan rocq-crane-sdl2

  • Rocqman

    • Rocqman membuktikan transisi state game yang digunakan oleh frame loop
      • Skor tidak berkurang
      • Nyawa dan jumlah koleksi yang tersisa tidak bertambah
      • State akhir adalah titik tetap dari tick
      • Memeriksa transisi layar pause dan akhir

  • Rocqsweeper

    • Rocqsweeper membuktikan aturan Minesweeper dan lapisan input
      • Klik pertama aman
      • Penandaan bendera mempertahankan data ranjau dan kedekatan
      • Flood fill mempertahankan ranjau dan tidak menambah sel aman yang tersembunyi
      • Kursor tidak keluar batas
      • Event mouse diinterpretasikan sebagai sel yang diharapkan

  • Reversirocq

    • Reversirocq menggunakan AI alpha-beta koinduktif dari game tree library yang sama dengan aturan Reversi yang ditambahkan oleh Charles C. Norton
    • Teorema-teoremanya menangani enumerasi langkah legal dan hasil permainan, serta menghubungkan alpha-beta dan minimax pada prefix hingga yang ditelusuri

  • Batas verifikasi

    • Batas pembuktian berakhir pada source Rocq dan tidak mencakup SDL·Crane·C++ hasil generasi·runtime native
    • Di dalam batas itu, yang dibuktikan adalah properti dari logika eksekusi nyata, bukan model yang terpisah dari program yang dijalankan

Ekosistem verifikasi program Rocq

  • Abstraksi representasi program

    • Interaction Trees: merepresentasikan program yang berefek dan mungkin tidak berhenti sebagai pohon koinduktif dari kejadian eksternal, serta menyediakan semantik denotasional dan penalaran persamaan untuk kode non-murni
    • Choice Trees: memodelkan sistem nondeterministik seperti konkurensi dengan menambahkan pilihan nondeterministik internal

  • Kerangka kerja verifikasi program

    • Iris: kerangka kerja concurrent separation logic tingkat tinggi untuk program berbasis state dan konkurensi
    • Iris-Lean juga berkembang cepat dan mendukung banyak fitur, tetapi belum digunakan seluas Rocq Iris
    • CFML: mengimpor source OCaml ke Rocq, menghasilkan characteristic formula, dan menyediakan taktik untuk spesifikasi separation logic tingkat tinggi
    • Perennial: kerangka kerja berbasis Iris untuk memverifikasi konkurensi, penyimpanan aman terhadap crash, dan sistem terdistribusi, serta terhubung ke program subset Go yang dapat dijalankan melalui Goose
    • VST: Verified Software Toolchain untuk membuktikan kebenaran fungsional program C berdasarkan semantik CompCert
    • BRiCk: logika program dan toolchain untuk program C++ nyata

  • Alat dengan backend atau komponen Rocq

    • Frama-C: platform analisis dan verifikasi deduktif C yang dapat meneruskan proof obligation ke Rocq
    • Why3: dapat mengirim goal dari bahasanya sendiri ke beberapa prover dan mengekspor proof obligation interaktif untuk Rocq
    • Cerberus: semantik formal yang dapat dieksekusi untuk subset besar C yang praktis, dan memiliki implementasi Rocq untuk model memori CHERI C

  • Semantik bahasa nyata dan kompiler terverifikasi

    • CompCert: kompiler C pengoptimal yang diverifikasi secara formal
    • Vellvm: menyediakan spesifikasi Rocq dan semantik abstrak untuk LLVM IR, serta interpreter eksekusi yang terbukti menyempurnakannya
    • Vélus: kompiler terverifikasi dari Lustre ke Clight milik CompCert
    • WasmCert: semantik formal termekanisasi untuk WebAssembly
    • JSCert: semantik formal JavaScript yang mengikuti spesifikasi ECMAScript 5

  • Verifikasi ringan berbasis translasi

    • hs-to-coq: menerjemahkan source Haskell ke Rocq
    • rocq-of-ocaml: menerjemahkan source OCaml ke Rocq
    • rocq-of-python: menerjemahkan source Python ke Rocq
    • rocq-of-rust: menerjemahkan source Rust ke Rocq
    • Aeneas: mengubah Rust yang lolos borrow check menjadi model fungsi murni untuk verifikasi, dan juga mendukung Lean sebagai target

  • Sintesis program dan parsing

    • Fiat Crypto: menurunkan aritmetika kriptografi berperforma tinggi untuk browser dan library TLS dengan pendekatan correct-by-construction
    • Rupicola: alat kompilasi relasional yang mengubah program Gallina fungsional tingkat rendah menjadi program imperatif Bedrock2
    • Narcissus: menurunkan encoder dan decoder format biner dengan pendekatan correct-by-construction
    • Verbatim: lexer terverifikasi berbasis regular expression
    • CoStar: parser terverifikasi berbasis algoritme ALL(*)

  • Status pemeliharaan

    • Sebagian proyek tidak dipelihara secara aktif, tetapi masih dapat dibangun dan dijalankan kembali dengan bantuan agen
    • Meskipun satu komponen yang diperlukan bisa dipindahkan ke Lean dalam waktu singkat, fitur dan riwayat penggunaan yang telah terakumulasi di seluruh ekosistem tidak otomatis ikut berpindah

Riwayat regulasi dan sertifikasi

  • Tidak ada pengalaman sertifikasi langsung terkait penerimaan regulasi, tetapi ini bisa menjadi faktor yang lebih penting terutama bagi praktisi di Eropa
  • ANSSI Prancis mempublikasikan kriteria untuk penggunaan Rocq dalam evaluasi Common Criteria
  • CompCert menyatakan telah berhasil qualification untuk komputer MFC_NG pada pesawat ATR 42/72 tahun 2026 melalui pekerjaan yang dilakukan AbsInt atas arahan Airbus
  • Tidak diketahui persyaratan apa yang harus dipenuhi port Lean dalam lingkungan yang sama, dan meskipun dipindahkan dengan rapi, port itu tidak otomatis mewarisi riwayat sertifikasi yang sudah ada

Agen AI dan biaya migrasi

  • Berlawanan dengan anggapan bahwa agen AI hanya pandai menulis Lean, agen juga cukup mampu menulis kode Rocq
  • Rocq telah ada sejak akhir 1980-an, sehingga banyak kode dan dokumentasi yang telah terakumulasi
  • Model saat ini dapat beradaptasi dengan baik ke bahasa yang tidak familier bila diberi dokumentasi dan contoh, sehingga fakta bahwa model hanya mengenal bahasa populer bukan alasan jangka panjang untuk mengganti proof assistant
  • Di Lean juga sedang berlangsung pekerjaan verifikasi program yang serius seperti mvcgen dan Velvet
  • Untuk memindahkan pekerjaan saat ini ke Lean, perlu menyusun ulang definisi serta mengganti pipeline ekstraksi, library, dan riwayat institusional, sehingga untuk saat ini Rocq lebih cocok

Bacaan terkait

Belum ada komentar.

Belum ada komentar.