प्रोग्राम वेरिफिकेशन में Rocq, Lean से बेहतर क्यों है

 (joomy.korkutblech.com)
1 पॉइंट द्वारा GN⁺ 2 시간 전 | अभी कोई टिप्पणी नहीं है. | WhatsApp पर शेयर करें
  • गणितीय formalization में Lean की वृद्धि स्पष्ट है, लेकिन executable program verification के लिए native coinduction, कई extraction paths, और संचित verification ecosystem वाला Rocq अधिक उपयुक्त है
  • Rocq, CoInductive और CoFixpoint से codata घोषित करता है, guardedness की जांच करता है, और फिर lazy execution code में extract करता है; जबकि Lean में library encoding, iterator, Thunk, या partial def में से एक चुनना पड़ता है
  • Lean का nested inductive type checker, Rocq द्वारा स्वीकार किए जाने वाले कुछ verification relations को अस्वीकार कर देता है; इसलिए JSON schema उदाहरण में एक Forall₂ proof को कई relations में बांटना पड़ता है और अलग inductive principle तैयार करना पड़ता है
  • Rocq, OCaml·Haskell·Rust·C++·WebAssembly जैसी program extraction paths और Iris·CompCert·Interaction Trees जैसे verification foundations देता है, जिससे वास्तविक गेम के verified logic को executable code से जोड़ा जा सकता है
  • AI agent भी अगर documentation और उदाहरण हों तो Rocq code लिख सकते हैं; लेकिन Lean में जाने के लिए definitions के साथ-साथ extraction pipeline, libraries, regulatory और institutional history तक बदलनी पड़ेगी, इसलिए मौजूदा काम में इसका व्यावहारिक लाभ कम है

प्रोग्राम वेरिफिकेशन के आधार पर तुलना

  • तुलना का विषय mathematical formalization नहीं बल्कि program verification है, और गणित के क्षेत्र में Lean के पास वास्तविक growth momentum है
  • “बेहतर” का मतलब कोई पूर्ण श्रेष्ठता नहीं, बल्कि यह कि मौजूदा काम के लिए Rocq अधिक उपयुक्त है
  • AI के गणित क्षेत्र में परिणामों और Lean में बढ़ती रुचि के साथ, Rocq का उपयोग जारी रखने का कारण अक्सर पूछा गया, और तर्क की शुरुआत LangSec keynote की slides से हुई

native coinductive types और cofixpoint

  • Lean के coinductive की उपलब्ध सीमा

    • Lean FRO के Wojciech Różowski और Joachim Breitner द्वारा विकसित coinductive predicate support को Lean 4.25 के coinductive command में शामिल किया गया है
    • यह feature bisimulation और coinductive proofs के लिए उपयोगी है, लेकिन Type में executable cofixpoint या extract होने वाले programs नहीं देता
    • Rocq का CoInductive और CoFixpoint, Type में सीधे executable codata प्रदान करता है
    • Lean में इसके अनुरूप कोई kernel declaration नहीं है, इसलिए सामान्य functions, structs, या library encoding का उपयोग करना पड़ता है

  • QPFTypes की declaration constraints

    • Alex Keizer का QPFTypes सामान्य codata के लिए एक proof-of-concept package है, जो codata specification से destructor, corecursor, और bisimulation principles बनाता है
    • Rocq के CoInductive से अलग, यह kernel declaration नहीं बल्कि library encoding है
    • उदाहरण उस समय के नवीनतम supported version Lean 4.25.0 पर fixed toolchain का उपयोग करता है
    • Rocq में सामान्य लगने वाली नीचे की तीन declarations, QPFTypes में काम नहीं करतीं
      • parameter-less codata implementation bug के कारण विफल हो जाती है
      • tree और forest जैसी mutual coinductive declarations, Lean की mutual block constraints के कारण समर्थित नहीं हैं
      • istream जैसी indexed coinductive families, जिनमें हर चरण पर clock index आगे बढ़ता है, QPF की अपनी सीमाओं के कारण समर्थित नहीं हैं
    • protocol, stage, size, और state machine में भी indexed coinductive patterns उपयोग होते हैं, लेकिन QPFTypes की सरल, non-mutual, non-indexed सीमा से बाहर जाते ही low-level MvQPF.Cofix.corec और bisim API को सीधे इस्तेमाल करना पड़ता है, या फिर इसे लागू ही नहीं किया जा सकता
    • Rocq में भी guardedness checker को संभालना आसान नहीं है, लेकिन ऊपर के मामलों को अलग encoding के बिना declare किया जा सकता है
    • Paco और Damien Pous का coinduction coinductive predicates और relation proofs को support करते हैं, लेकिन programs के लिए CoFixpoint का विकल्प नहीं हैं

  • extracted programs का अंतर

    • Rocq का native cofixpoint वास्तविक lazy OCaml values के रूप में extract होता है
    • game tree library का unfold_cotree, Lazy.t में लिपटे tree और recursive lazy generator function में बदल जाता है
    • परिणाम उस lazy tree structure के करीब होता है जिसे कोई व्यक्ति सीधे लिखता
    • QPFTypes में निर्माण और observation, MvQPF.Cofix.corec और MvQPF.Cofix.dest के जरिए होते हैं, और extracted program भी generalized Cofix representation बनाए रखता है
    • BadCoinduction.lean में Colist·Cotree, generated interface, parameter-less, mutual, और indexed codata के failure cases, साथ ही reproduction के लिए QPFTypes commit और commands शामिल हैं

Lean में उपलब्ध विकल्प

  • stream और iterator

    • mathlib का Stream', Nat → α फ़ंक्शन है
    • यह स्थान n पर मौजूद तत्व की गणना कर सकता है और corecursor, extensionality, bisimulation, और coinduction सहायक लेम्मा प्रदान करता है
    • लेकिन यह ऐसा lazy constructor नहीं है जिसकी tail कोई दूसरा stream हो, और न ही यह मनमाने mutual और indexed codata तक समस्या हल करता है
    • explicit state और step function का उपयोग करने वाली state machine भी corecursor की भूमिका निभा सकती है
    • Lean का Iter एक sequential interface है जो मांग के अनुसार एक-एक step की गणना करता है
    • iterator के पास ऐसा Productive proof हो सकता है जो value generation या termination की गारंटी देता है, और Iter.repeat में यह पहले से उपलब्ध है
    • user-defined iterator के लिए step interface, invariant, और ज़रूरत पड़ने पर productivity proof स्वयं देना पड़ता है
    • Rocq का CoFixpoint recursive call की guardedness जाँचता है और state machine तथा sequence के बीच अलग connection work के बिना coinductive value लौटाता है

  • Thunk, partial def, unsafe def

    • Lean का Thunk compiled code में पहली बार force किए जाने पर गणना करता है और परिणाम cache करता है, लेकिन coinduction प्रदान नहीं करता
    • logic में यह Unit → α की तरह दिखता है, इसलिए total definition को proof में इस्तेमाल किया जा सकता है, लेकिन cache दिखाई नहीं देता
    • यह recursion की अनुमति भी नहीं देता और न ही यह जाँचता है कि recursion अंततः constructor पैदा करता है या नहीं
    • Rocq का extracted code भी runtime laziness का उपयोग करता है, लेकिन पहले guardedness check से गुजरता है
    • partial def recursive body को execute कर सकता है, लेकिन logic में केवल opaque constant छोड़ता है
    • यह termination या productivity की जाँच नहीं करता, इसलिए natural number producer और तुरंत infinite recursion करने वाले producer, दोनों को स्वीकार करता है
    • unsafe def भी execute हो सकता है, लेकिन theorem-safe declaration में इसे reference नहीं किया जा सकता
    • Batteries का MLList private unsafe lazy implementation, opaque public interface, और partial def से लिखे गए fix और iterate producer का संयोजन करता है
    • ऐसे producer को observed Rocq cofixpoint की तरह proof में unfold नहीं किया जा सकता
    • partial_fixpoint equation को बनाए रखता है, लेकिन constructor और thunk को मिलाने वाली recursion को स्वीकार नहीं करता
    • QPFTypes corecursor और bisimulation principles देता है ताकि opacity से बचा जा सके, लेकिन इसके बदले generalized Cofix representation और declaration constraints स्वीकार करने पड़ते हैं

प्रभाव वाले और terminate न होने वाले प्रोग्राम

  • Interaction Trees प्रभाव वाले और संभवतः terminate न होने वाले प्रोग्रामों को coinductive tree के रूप में व्यक्त करता है
    • उसी tree से प्रोग्राम लिखे, interpret किए, और extract किए जा सकते हैं, और आम तौर पर weak bisimulation तक शामिल करने वाले equations सिद्ध किए जा सकते हैं
  • Stream' और Iter केवल sequence प्रदान करते हैं, इसलिए वे effect के लिए ज़रूरी branching continuation को व्यक्त नहीं कर सकते
  • Thunk और partial def से effect tree चलाने पर recursive producer proof में opaque हो जाते हैं, और अगर computation और proof दोनों को साथ समर्थन देना हो तो codata library encoding की ज़रूरत पड़ती है
  • MIT PLV का lean4-itree Mathlib के PFunctor.M final coalgebra से Interaction Trees को implement करता है
  • PolyFun handler, recursive procedure, execution trace, strong/weak bisimulation, और monad तथा iteration laws के proofs जोड़ता है
    • Lean में tree की computation और proof दोनों किए जा सकते हैं, लेकिन यह अब भी library में encoded M-type ही है
    • native codata declaration नहीं है, और direct lazy program की जगह सामान्य representation बना रहता है
  • HITrees भी इस constraint को bypass नहीं करता
    • Lean में native coinductive type नहीं होने के कारण यह ITrees के coinductive Delay-monad approach का उपयोग नहीं करता
    • tree inductive हैं, और nontermination higher-order recursive effect बन जाती है
    • recursive computation कोई ऐसा infinite tree नहीं है जिसे observe और unfold किया जा सके; इसका अर्थ तब बनता है जब handler effect को interpret करता है
    • monadic interpretation से execute किया जा सकता है और state machine interpretation से proof किया जा सकता है, लेकिन HITree का equational theory सामान्य recursive unfolding equations प्रदान नहीं करता
  • Rocq codata declaration, guarded producer, observation-based reasoning, और direct lazy code extraction को एक ही flow में support करता है

Nested inductive types और predicates

  • JSON schema validation का उदाहरण

    • Lean कई nested inductive definitions की अनुमति देता है, लेकिन Rocq जिन कुछ definitions को स्वीकार करता है उन्हें अस्वीकार कर देता है
    • यह अंतर A Rose Tree Is Blooming में इस्तेमाल हुआ था, और इसे एक छोटे JSON schema उदाहरण से दोहराया जा सकता है
    • JSON और schema स्वयं दोनों भाषाओं में बिना समस्या के define किए जा सकते हैं
    • object schema validation में field names के मेल और हर JSON value के संबंधित sub-schema के लिए valid होने को pair-wise जांचना पड़ता है
    • Rocq नाम की समानता और recursive validation को एक ही Forall2 derivation में रख सकता है
    • Rocq 9.0 recursive occurrence के आसपास tuple-pattern lambda को strict positivity violation मानकर अस्वीकार करता है, लेकिन pattern की जगह projection इस्तेमाल करने पर compile हो जाता है
    • Lean 4.32.1 उसी object constructor में recursive occurrence के Forall₂ और And दोनों से गुजरने पर inner And को गलत nested inductive data type मानकर अस्वीकार कर देता है
    • Forall₂ ParRed, And·Exists के जरिए direct recursion, और Forall₂ (fun sf jf => Valid sf.2 jf.2) जैसे पास-पड़ोस के रूप स्वीकार किए जाते हैं
    • relation parameter constructor-local variable env को capture करने वाला Forall₂ (Eval env) Forall₂ चरण पर ही विफल हो जाता है

  • workaround तरीके और proof की लागत

    • Lean में object validation को दो Forall₂ derivations में बांटा जा सकता है
      • एक field names की समानता को संरक्षित करता है
      • दूसरा संबंधित values की recursive validation को संरक्षित करता है
    • अलग indices या length proofs के बिना list structure को बनाए रखा जा सकता है और head removal को भी structurally सिद्ध किया जा सकता है, लेकिन दोनों derivations को decompose करना पड़ता है
    • relation अलग करने पर हर name equality और recursive validation के जोड़े में बंधा single proof object खो जाता है
    • mutual ValidFields relation से इस binding को वापस लाया जा सकता है, लेकिन Lean की induction tactic mutual inductive types को support नहीं करती और generated recursor भी हर relation के लिए motive मांगता है
    • custom induction theorem बनाने पर इस setup को छिपाया जा सकता है
    • Rocq standard Forall2 representation बनाए रखता है, और अगर mutual definition चाहिए तो Scheme से combined principle generate किया जा सकता है
    • Lean भी index-based encoding के बिना वही proposition व्यक्त कर सकता है, लेकिन declaration को फिर से व्यवस्थित करना पड़ता है और ज्यादा proof machinery बनानी पड़ती है
    • पूरी तुलना वाली file Rocq 9.0.0 के लिए NestedPain.v और Lean 4.32.1 के लिए NestedPain.lean में है, और Lean की अपेक्षित विफलताएं compile समय पर #guard_msgs से जांची जाती हैं

  • nested arguments के लिए strong induction principle

    • जब Term में list Term शामिल हो जैसे मामलों में nested data के elements के लिए assumptions चाहिए होती हैं, तब दोनों systems में stronger recursor की जरूरत पड़ी
    • Rocq 9.2 nesting type के लिए All predicate और theorem register करने पर nested arguments के लिए induction hypotheses generate करता है
    • standard library इसे default रूप से register नहीं करती, इसलिए Term declaration से पहले Scheme All for list. की एक पंक्ति जोड़नी पड़ती है
    • generated Term_ind और Term_rect को app case में list_all Term P l assumption मिलती है और body list_all_forall को call करती है
    • Scheme All for Forall2. जोड़ने पर ParRed_ind भी Forall2 ParRed args args' premise के लिए induction hypotheses देता है
    • register न करने पर पहले वाला weak principle बना रहता है और [register-all] warning आती है
    • Lean में अभी भी strong recursor खुद तैयार करना पड़ता है

program extraction के विकल्प

  • Lean standard toolchain अपने runtime के जरिए compile करती है, और Lean libraries बनाते समय तथा जब runtime design उपयुक्त हो तब यह फायदेमंद है
  • Kim Morrison का verified lean-zip pure Rust miniz_oxide से भी तेज compress कर सकता है, इसलिए performance प्रभावशाली है
  • लेकिन Lean कई वैकल्पिक extraction backends नहीं देता, और मौजूदा compile pipeline के लिए end-to-end correctness proof नहीं है
    • Kiran Gopinathan द्वारा खोजे गए runtime bug जैसे दुर्लभ मुद्दे आ सकते हैं
    • generated code runtime के लिए विशेषीकृत है और इंसानों द्वारा पढ़ने के लिए डिजाइन नहीं की गई है
  • Rocq के पास trust और readability के बीच अलग-अलग trade-off देने वाले कई रास्ते हैं

verified logic को चलाने वाले games

  • Rocq में executable program के उसी source code के properties को machine-verify करने के बाद, Crane से logic और event loop को C++ में extract किया जाता है और rocq-crane-sdl2 से SDL2 से जोड़ा जाता है

  • Rocqman

    • Rocqman frame loop द्वारा उपयोग किए जाने वाले game state transitions को सिद्ध करता है
      • score कम नहीं होता
      • lives और बाकी collectibles नहीं बढ़ते
      • terminal states tick के fixed points हैं
      • pause और game-over screen transitions की जांच की जाती है

  • Rocqsweeper

    • Rocqsweeper Minesweeper के rules और input layer को सिद्ध करता है
      • पहला click सुरक्षित होता है
      • flag placement mines और adjacent data को संरक्षित करती है
      • flood fill mines को संरक्षित करता है और छिपे हुए सुरक्षित cells नहीं बढ़ाता
      • cursor boundaries के बाहर नहीं जाता
      • mouse events को अपेक्षित cells के रूप में interpret किया जाता है

  • Reversirocq

    • Reversirocq game tree library के coinductive alpha-beta AI का उपयोग करता है, जिसमें Charles C. Norton द्वारा जोड़े गए Reversi rules भी शामिल हैं
    • theorems legal move enumeration और game outcomes को कवर करते हैं, और खोजे गए finite prefix पर alpha-beta को minimax से जोड़ते हैं

  • verification boundary

    • proof boundary Rocq source पर समाप्त होती है, और इसमें SDL·Crane·generated C++·native runtime शामिल नहीं हैं
    • boundary के भीतर, executable program से अलग किसी model की नहीं बल्कि वास्तविक executable logic की properties सिद्ध की जाती हैं

Rocq प्रोग्राम वेरिफिकेशन इकोसिस्टम

  • प्रोग्राम प्रतिनिधित्व एब्स्ट्रैक्शन

    • Interaction Trees: बाहरी इवेंट्स के coinductive trees के रूप में effectful और संभवतः non-terminating प्रोग्राम्स को व्यक्त करता है, और impure code के लिए denotational semantics तथा equational reasoning प्रदान करता है
    • Choice Trees: आंतरिक nondeterministic choices जोड़कर concurrency जैसे nondeterministic systems को मॉडल करता है

  • प्रोग्राम वेरिफिकेशन फ्रेमवर्क

    • Iris: stateful और concurrent प्रोग्राम्स के लिए एक उच्च-क्रम concurrent separation logic फ्रेमवर्क है
    • Iris-Lean भी तेज़ी से विकसित हो रहा है और कई features को support करता है, लेकिन Rocq Iris जितना व्यापक रूप से इस्तेमाल नहीं हुआ है
    • CFML: OCaml source को Rocq में लाकर characteristic formulas बनाता है और उच्च-क्रम separation logic specifications के लिए tactics प्रदान करता है
    • Perennial: concurrency, crash-safe storage और distributed systems को verify करने वाला Iris-आधारित फ्रेमवर्क है, और Goose के जरिए Go के subset के executable programs से जुड़ता है
    • VST: CompCert semantics पर आधारित C programs की functional correctness साबित करने वाली Verified Software Toolchain है
    • BRiCk: वास्तविक C++ programs के लिए program logic और toolchain है

  • Rocq backend या components वाले tools

    • Frama-C: C analysis और deductive verification platform, जो proof obligations को Rocq को सौंप सकता है
    • Why3: अपनी language के goals को कई provers के पास भेजता है और Rocq के लिए interactive proof obligations export कर सकता है
    • Cerberus: व्यावहारिक बड़े C subset की executable formal semantics है, और CHERI C memory model का Rocq implementation मौजूद है

  • वास्तविक languages की semantics और verified compilers

    • CompCert: formally verified optimizing C compiler है
    • Vellvm: LLVM IR के लिए Rocq specifications और abstract semantics प्रदान करता है, साथ ही एक executable interpreter भी देता है जिसके refinement को साबित किया गया है
    • Vélus: Lustre से CompCert के Clight तक जाने वाला verified compiler है
    • WasmCert: WebAssembly की mechanized formal semantics है
    • JSCert: ECMAScript 5 specification को track करने वाली JavaScript formal semantics है

  • translation-आधारित lightweight verification

    • hs-to-coq: Haskell source को Rocq में अनुवाद करता है
    • rocq-of-ocaml: OCaml source को Rocq में अनुवाद करता है
    • rocq-of-python: Python source को Rocq में अनुवाद करता है
    • rocq-of-rust: Rust source को Rocq में अनुवाद करता है
    • Aeneas: borrow check पास कर चुके Rust को verification के लिए pure functional model में बदलता है, और Lean को भी target के रूप में support करता है

  • प्रोग्राम synthesis और parsing

    • Fiat Crypto: ब्राउज़र और TLS libraries में इस्तेमाल हो सकने वाले high-performance cryptographic arithmetic को correct-by-construction तरीके से derive करता है
    • Rupicola: निम्न-स्तरीय functional Gallina programs को imperative Bedrock2 programs में बदलने वाला relational compilation tool है
    • Narcissus: binary formats के correct-by-construction encoder और decoder derive करता है
    • Verbatim: regular expression-आधारित verified lexer है
    • CoStar: ALL(*) algorithm-आधारित verified parser है

  • रखरखाव की स्थिति

    • कुछ projects का सक्रिय रखरखाव नहीं हो रहा है, लेकिन इन्हें agents को देकर फिर से build और run कराया जा सका
    • भले ही किसी एक ज़रूरी घटक को कम समय में Lean में port किया जा सके, पूरे इकोसिस्टम ने जो features और usage history जमा की है, वह अपने-आप साथ नहीं आती

नियामक और प्रमाणन इतिहास

  • नियामक स्वीकृति के प्रत्यक्ष प्रमाणन अनुभव की जानकारी नहीं है, हालांकि यह खासकर यूरोप के practitioners के लिए अधिक महत्वपूर्ण तत्व हो सकता है
  • फ़्रांस की ANSSI ने Common Criteria evaluation में Rocq के उपयोग के लिए मानदंड प्रकाशित किए हैं
  • CompCert का कहना है कि AbsInt द्वारा Airbus के निर्देशों के तहत किए गए कार्य के माध्यम से 2026 ATR 42/72 विमान के MFC_NG कंप्यूटर के लिए इसका qualification सफलतापूर्वक हुआ
  • यह ज्ञात नहीं है कि वही environment में Lean port को किन आवश्यकताओं को पूरा करना होगा, और साफ़-सुथरा port होने पर भी मौजूदा प्रमाणन इतिहास अपने-आप विरासत में नहीं मिलता

AI agents और migration cost

  • इस धारणा के विपरीत कि AI agents सिर्फ Lean ही अच्छी तरह लिखते हैं, वे Rocq code भी पर्याप्त रूप से लिख सकते हैं
  • Rocq 1980 के दशक के उत्तरार्ध से मौजूद है, इसलिए code और documentation का बड़ा भंडार जमा है
  • मौजूदा models documentation और examples दिए जाने पर अपरिचित languages के लिए भी अच्छी तरह अनुकूल हो जाते हैं, इसलिए सिर्फ लोकप्रिय languages जानना proof assistant बदलने का दीर्घकालिक आधार नहीं बनता
  • Lean में भी mvcgen और Velvet जैसे गंभीर प्रोग्राम वेरिफिकेशन प्रयास चल रहे हैं
  • मौजूदा काम को Lean में ले जाने के लिए definitions को फिर से बनाना होगा और extraction pipeline, libraries तथा institutional history को बदलना होगा, इसलिए अभी Rocq अधिक उपयुक्त है

संबंधित पढ़ाई

अभी कोई टिप्पणी नहीं है.

अभी कोई टिप्पणी नहीं है.