ทำไม Rocq ถึงดีกว่า Lean สำหรับการพิสูจน์ความถูกต้องของโปรแกรม

 (joomy.korkutblech.com)
1 คะแนน โดย GN⁺ 2 시간 전 | ยังไม่มีความคิดเห็น | แชร์ทาง WhatsApp
  • แม้ Lean จะเติบโตอย่างชัดเจนในด้านการทำคณิตศาสตร์ให้เป็นแบบรูปนัย แต่สำหรับการพิสูจน์ความถูกต้องของโปรแกรมที่รันได้ Rocq เหมาะกว่าด้วย coinduction แบบเนทีฟ, เส้นทางการ extract ที่หลากหลาย และระบบนิเวศด้านการพิสูจน์ที่สั่งสมมา
  • Rocq ประกาศ codata ด้วย CoInductive และ CoFixpoint ตรวจสอบ guardedness แล้ว extract เป็นโค้ดแบบประมวลผลแบบหน่วงเวลา แต่ใน Lean ต้องเลือกอย่างใดอย่างหนึ่งระหว่างการเข้ารหัสด้วยไลบรารี, iterator, Thunk หรือ partial def
  • ตัวตรวจสอบ nested inductive type ของ Lean ปฏิเสธความสัมพันธ์สำหรับการพิสูจน์บางส่วนที่ Rocq ยอมรับ ทำให้ในกรณีของ JSON schema ต้องแยกการพิสูจน์ Forall₂ หนึ่งรายการออกเป็นหลายความสัมพันธ์ และต้องเตรียมหลักอุปนัยแยกต่างหาก
  • Rocq มี เส้นทางการ extract โปรแกรม ไปยัง OCaml, Haskell, Rust, C++, WebAssembly ฯลฯ และมีรากฐานการพิสูจน์อย่าง Iris, CompCert, Interaction Trees จึงเชื่อมตรรกะที่พิสูจน์แล้วของเกมจริงเข้ากับโค้ดที่รันได้
  • แม้แต่ AI agent ก็เขียนโค้ด Rocq ได้หากมีเอกสารและตัวอย่าง แต่การย้ายไป Lean ต้องแทนที่ไม่ใช่แค่คำนิยามเท่านั้น ยังรวมถึง extraction pipeline, ไลบรารี, ประวัติด้านกฎระเบียบและสถาบันด้วย จึงแทบไม่มีประโยชน์เชิงปฏิบัติสำหรับงานปัจจุบัน

การเปรียบเทียบโดยใช้การพิสูจน์ความถูกต้องของโปรแกรมเป็นเกณฑ์

  • สิ่งที่เปรียบเทียบไม่ใช่การทำคณิตศาสตร์ให้เป็นแบบรูปนัย แต่คือ การพิสูจน์ความถูกต้องของโปรแกรม และในแวดวงคณิตศาสตร์ Lean ก็มีแรงขับการเติบโตจริง
  • คำว่า “ดีกว่า” ไม่ได้หมายถึงเหนือกว่าแบบสัมบูรณ์ แต่หมายถึง Rocq เหมาะกับงานที่กำลังทำอยู่มากกว่าในตอนนี้
  • เมื่อ AI ทำผลงานในสายคณิตศาสตร์ได้มากขึ้นและความสนใจต่อ Lean เพิ่มขึ้น ผู้เขียนจึงถูกถามบ่อยว่าทำไมยังใช้ Rocq ต่อไป โดยประเด็นหลักเริ่มต้นจากสไลด์ในคีย์โน้ต LangSec

native coinductive type และ cofixpoint

  • ขอบเขตที่ coinductive ของ Lean รองรับ

    • การรองรับ coinductive predicate ที่พัฒนาโดย Wojciech Różowski และ Joachim Breitner แห่ง Lean FRO ถูกรวมอยู่ในคำสั่ง coinductive ของ Lean 4.25
    • ฟีเจอร์นี้มีประโยชน์กับ bisimulation และการพิสูจน์แบบ coinduction แต่ไม่ได้ให้ cofixpoint ที่รันได้ใน Type หรือโปรแกรมที่ extract ได้
    • CoInductive และ CoFixpoint ของ Rocq มอบ codata ที่รันได้โดยตรงใน Type
    • Lean ไม่มีการประกาศระดับเคอร์เนลที่สอดคล้องกัน จึงต้องใช้ฟังก์ชันทั่วไป, struct หรือการเข้ารหัสด้วยไลบรารีแทน

  • ข้อจำกัดของการประกาศใน QPFTypes

    • QPFTypes ของ Alex Keizer เป็นแพ็กเกจพิสูจน์แนวคิดสำหรับ codata ทั่วไป โดยสร้าง destructor, corecursor และหลัก bisimulation จากสเปก codata
    • ต่างจาก CoInductive ของ Rocq ตรงที่เป็นการเข้ารหัสด้วยไลบรารี ไม่ใช่การประกาศระดับเคอร์เนล
    • ตัวอย่างใช้ toolchain แบบตรึงเวอร์ชันที่รองรับล่าสุดในขณะนั้นคือ Lean 4.25.0
    • ใน Rocq การประกาศถัดไปนี้ที่เป็นเรื่องปกติกลับใช้งานไม่ได้ใน QPFTypes
      • codata ที่ไม่มีพารามิเตอร์ ล้มเหลวเพราะบั๊กในการติดตั้ง
      • การประกาศ coinductive แบบ mutual อย่าง tree และ forest ไม่รองรับเพราะข้อจำกัดของ mutual block ใน Lean
      • indexed coinductive family อย่าง istream ที่มี clock index เดินหน้าในแต่ละสเต็ป ไม่รองรับเพราะข้อจำกัดของ QPF เอง
    • รูปแบบ indexed coinduction ยังใช้กับโปรโตคอล, สเตจ, ขนาด และ state machine ด้วย แต่เมื่อพ้นขอบเขตแบบเรียบง่าย ไม่ mutual และไม่ indexed ของ QPFTypes แล้ว ก็ต้องเรียก API ระดับล่าง MvQPF.Cofix.corec และ bisim โดยตรง หรือไม่ก็ทำไม่ได้เลย
    • แม้ Rocq เองก็จัดการกับ ตัวตรวจสอบ guardedness ได้ไม่ง่าย แต่กรณีข้างต้นสามารถประกาศได้โดยไม่ต้องมี encoding แยก
    • Paco และ coinduction ของ Damien Pous รองรับการพิสูจน์ predicate และ relation แบบ coinduction แต่ไม่ได้มาแทน CoFixpoint สำหรับโปรแกรม

  • ความต่างของโปรแกรมที่ถูก extract

    • cofixpoint แบบเนทีฟของ Rocq ถูก extract เป็น ค่า OCaml แบบ lazy จริง
    • unfold_cotree ของ game tree library กลายเป็น tree ที่ห่อด้วย Lazy.t และฟังก์ชันสร้างแบบหน่วงเวลาที่เรียกซ้ำได้
    • ผลลัพธ์ที่ได้ใกล้เคียงกับโครงสร้างต้นไม้แบบ lazy ที่มนุษย์น่าจะเขียนเอง
    • ใน QPFTypes การสร้างและการสังเกตผ่าน MvQPF.Cofix.corec และ MvQPF.Cofix.dest และโปรแกรมที่ extract ออกมาก็ยังคงรูปแบบ Cofix ที่ทำให้เป็นนามธรรมไว้
    • BadCoinduction.lean มี Colist, Cotree, อินเทอร์เฟซที่ถูกสร้างขึ้น, กรณีล้มเหลวของ codata แบบไม่มีพารามิเตอร์ แบบ mutual และแบบ indexed รวมถึงคอมมิตและคำสั่งของ QPFTypes สำหรับการทำซ้ำผลลัพธ์

ทางเลือกที่มีใน Lean

  • สตรีมและอิเทอเรเตอร์

    • Stream' ของ mathlib เป็นฟังก์ชัน Nat → α
    • สามารถคำนวณสมาชิกที่ตำแหน่ง n ได้ และมี corecursor, extensionality, bisimulation และบทช่วยพิสูจน์แบบ coinduction
    • แต่ไม่ใช่ตัวสร้างแบบ lazy ที่ tail เป็นสตรีมอีกตัว และไม่ได้ครอบคลุม codata แบบ mutual หรือ indexed ตามอำเภอใจ
    • state machine ที่ใช้สถานะอย่างชัดเจนและฟังก์ชัน step ก็ทำหน้าที่เป็น corecursor ได้เช่นกัน
    • Iter ของ Lean เป็นอินเทอร์เฟซแบบลำดับที่คำนวณทีละขั้นเมื่อมีการร้องขอ
    • อิเทอเรเตอร์สามารถมีหลักฐาน Productive ที่รับประกันการสร้างค่าหรือการสิ้นสุดได้ และ Iter.repeat มีมาให้อยู่แล้ว
    • สำหรับอิเทอเรเตอร์ที่ผู้ใช้กำหนดเอง ต้องจัดเตรียมอินเทอร์เฟซ step, invariant และหากจำเป็นก็ต้องมีหลักฐานเรื่อง productivity เอง
    • CoFixpoint ของ Rocq ตรวจสอบ guardedness ของการเรียกซ้ำ และคืนค่าแบบ coinductive โดยไม่ต้องมีงานเชื่อมต่อแยกระหว่าง state machine กับ sequence

  • Thunk, partial def, unsafe def

    • Thunk ของ Lean จะคำนวณเมื่อถูก force ครั้งแรกในโค้ดที่คอมไพล์แล้วและแคชผลลัพธ์ไว้ แต่ไม่ได้ให้ coinduction
    • ในตรรกะมันจึงมองเป็น Unit → α ทำให้ใช้คำนิยามทั้งหมดในการพิสูจน์ได้ แต่ไม่เห็นแคช
    • มันไม่ได้อนุญาตการเรียกซ้ำ หรือไม่ได้ตรวจสอบว่าการเรียกซ้ำจะสร้าง constructor ในที่สุดหรือไม่
    • โค้ดที่สกัดออกของ Rocq ก็ใช้ความเป็น lazy ตอนรันไทม์เช่นกัน แต่ต้องผ่านการตรวจ guardedness ก่อน
    • partial def สามารถรันเนื้อความของการเรียกซ้ำได้ แต่ในตรรกะจะเหลือเพียงค่าคงที่ทึบแสง
    • มันไม่ตรวจสอบ termination หรือ productivity จึงยอมรับได้ทั้งตัวสร้างจำนวนธรรมชาติและตัวสร้างที่วนซ้ำไม่สิ้นสุดทันที
    • unsafe def ก็รันได้เช่นกัน แต่ไม่สามารถอ้างอิงได้ในประกาศที่ปลอดภัยในเชิงทฤษฎีบท
    • MLList ของ Batteries ผสานการทำ lazy แบบ unsafe ภายในที่ไม่เปิดเผย, อินเทอร์เฟซสาธารณะที่ทึบแสง และตัวสร้าง fix กับ iterate ที่เขียนด้วย partial def
    • ตัวสร้างเหล่านี้ไม่สามารถคลี่ออกในการพิสูจน์ได้เหมือน cofixpoint ของ Rocq ที่สังเกตได้
    • partial_fixpoint รักษาสมการไว้ แต่ไม่ยอมรับการเรียกซ้ำที่ผสาน constructor กับ thunk
    • QPFTypes ให้ corecursor และหลักการ bisimulation เพื่อหลีกเลี่ยงความทึบแสง แต่ต้องแลกกับรูปแบบ Cofix ที่ทำให้เป็นทั่วไปและข้อจำกัดของการประกาศ

โปรแกรมที่มีเอฟเฟกต์และไม่สิ้นสุด

  • Interaction Trees แทนโปรแกรมที่มีเอฟเฟกต์และอาจไม่สิ้นสุดด้วยต้นไม้แบบ coinductive
    • สามารถเขียน, ตีความ และสกัดโปรแกรมด้วยต้นไม้ชุดเดียวกัน และโดยทั่วไปพิสูจน์สมการได้รวมถึง weak bisimulation
  • Stream' และ Iter ให้เพียง sequence จึงไม่สามารถแทน branching continuation ที่จำเป็นต่อเอฟเฟกต์ได้
  • เมื่อรันเอฟเฟกต์ทรีด้วย Thunk และ partial def ตัวสร้างแบบเรียกซ้ำจะทึบแสงต่อการพิสูจน์ และหากต้องการรองรับทั้งการคำนวณและการพิสูจน์ร่วมกัน ก็จำเป็นต้องมีการเข้ารหัสด้วยไลบรารี codata
  • lean4-itree ของ MIT PLV ใช้ final coalgebra PFunctor.M ของ Mathlib เพื่ออิมพลีเมนต์ Interaction Trees
  • PolyFun เพิ่ม handler, recursive procedure, execution trace, strong/weak bisimulation รวมถึงการพิสูจน์กฎของ monad และ iteration
    • สามารถคำนวณและพิสูจน์ต้นไม้ใน Lean ได้ แต่ก็ยังเป็น M-type ที่เข้ารหัสผ่านไลบรารี
    • ไม่มีการประกาศ codata แบบ native และยังคงรักษาการแทนค่าแบบทั่วไปแทนโปรแกรม lazy โดยตรง
  • HITrees ก็ไม่ได้หลีกเลี่ยงข้อจำกัดนี้
    • เนื่องจาก Lean ไม่มีชนิด coinductive แบบ native จึงไม่ใช้แนวทาง Delay-monad แบบ coinductive ของ ITrees
    • ต้นไม้เป็นแบบอุปนัย และการไม่สิ้นสุดกลายเป็นเอฟเฟกต์การเรียกซ้ำลำดับสูง
    • การคำนวณแบบเรียกซ้ำไม่ได้เป็นต้นไม้อนันต์ที่สังเกตและคลี่ออกได้ แต่จะมีความหมายเมื่อ handler ตีความเอฟเฟกต์
    • สามารถรันด้วย monadic interpretation และพิสูจน์ด้วยการตีความแบบ state machine ได้ แต่ทฤษฎีสมการของ HITree ไม่ได้ให้สมการการคลี่การเรียกซ้ำทั่วไป
  • Rocq รองรับการประกาศ codata, guarded producer, การให้เหตุผลจากการสังเกต และการสกัดโค้ด lazy โดยตรงในโฟลว์เดียว

ชนิดอุปนัยและเพรดิเคตแบบซ้อนกัน

  • กรณีศึกษาการตรวจสอบความถูกต้องของ JSON schema

    • Lean อนุญาตนิยามอุปนัยแบบซ้อนหลายแบบ แต่ปฏิเสธบางนิยามที่ Rocq ยอมรับ
    • ความแตกต่างนี้ถูกใช้ใน A Rose Tree Is Blooming และสามารถทำซ้ำได้ด้วยกรณี JSON schema ที่เล็กกว่า
    • ทั้ง JSON และ schema เองสามารถนิยามได้โดยไม่มีปัญหาในทั้งสองภาษา
    • ในการตรวจสอบความถูกต้องของ object schema ต้องตรวจสอบเป็นคู่ ๆ ว่าชื่อฟิลด์ตรงกันและค่า JSON แต่ละค่าถูกต้องตาม subschema ที่สอดคล้องกันหรือไม่
    • Rocq สามารถเก็บทั้งความเท่ากันของชื่อและการตรวจสอบแบบเรียกซ้ำไว้ในอุปนัย Forall2 ตัวเดียวได้
    • Rocq 9.0 ปฏิเสธ lambda แบบ tuple-pattern รอบการปรากฏแบบเรียกซ้ำว่าเป็นการละเมิด strict positivity แต่ถ้าใช้ projection แทน pattern จะคอมไพล์ได้
    • Lean 4.32.1 เมื่อการปรากฏแบบเรียกซ้ำผ่านทั้ง Forall₂ และ And ใน constructor ของ object เดียวกัน จะปฏิเสธ And ชั้นในโดยมองว่าเป็น nested inductive data type ที่ไม่ถูกต้อง
    • อนุญาต Forall₂ ParRed, การเรียกซ้ำโดยตรงผ่าน And·Exists, และรูปแบบข้างเคียงอย่าง Forall₂ (fun sf jf => Valid sf.2 jf.2)
    • Forall₂ (Eval env) ที่พารามิเตอร์ relation จับตัวแปรท้องถิ่นของ constructor อย่าง env จะล้มเหลวที่ขั้น Forall₂

  • วิธีเลี่ยงและต้นทุนของการพิสูจน์

    • ใน Lean การตรวจสอบ object สามารถแยกเป็นอุปนัย Forall₂ สองตัวได้
      • ตัวหนึ่งเก็บการคงไว้ของความเท่ากันของชื่อฟิลด์
      • อีกตัวเก็บการตรวจสอบแบบเรียกซ้ำของค่าที่สอดคล้องกัน
    • โดยไม่ต้องมีดัชนีแยกหรือตัวพิสูจน์ความยาว ก็ยังคงโครงสร้างลิสต์ไว้และพิสูจน์การตัด head ออกเชิงโครงสร้างได้ แต่ต้องแยกทั้งสองอุปนัยออก
    • เมื่อแยก relation ออก จะเสีย วัตถุพิสูจน์เดี่ยว ที่จับคู่ความเท่ากันของชื่อกับการตรวจสอบแบบเรียกซ้ำแต่ละคู่ไว้
    • สามารถกู้การจับคู่นี้กลับมาด้วย relation ร่วมกัน ValidFields แต่ tactic induction ของ Lean ไม่รองรับชนิดอุปนัยร่วม และ recursor ที่สร้างขึ้นก็ต้องการ motive แยกสำหรับแต่ละ relation
    • หากสร้างทฤษฎีบทอุปนัยแบบกำหนดเอง ก็สามารถซ่อนการตั้งค่านี้ได้
    • Rocq ยังคงใช้รูปแบบมาตรฐาน Forall2 และหากต้องใช้นิยามร่วม ก็สร้างหลักการรวมได้ด้วย Scheme
    • Lean ก็สามารถแสดง proposition เดียวกันได้โดยไม่ต้องเข้ารหัสแบบอิงดัชนี แต่ต้องจัดเรียง declaration ใหม่และสร้างเครื่องมือช่วยพิสูจน์เพิ่ม
    • ไฟล์เปรียบเทียบฉบับเต็มอยู่ที่ NestedPain.v สำหรับ Rocq 9.0.0 และ NestedPain.lean สำหรับ Lean 4.32.1 โดยความล้มเหลวที่คาดไว้ของ Lean ถูกตรวจตอนคอมไพล์ด้วย #guard_msgs

  • หลักการอุปนัยที่แข็งแรงกว่าสำหรับอาร์กิวเมนต์แบบซ้อน

    • ในการพิสูจน์ที่ต้องการสมมติฐานรายองค์ประกอบของข้อมูลแบบซ้อน เช่นกรณีที่ Term มี list Term อยู่ภายใน ทั้งสองระบบต่างก็ต้องการ recursor ที่แข็งแรงกว่า
    • Rocq 9.2 จะสร้างสมมติฐานอุปนัยสำหรับอาร์กิวเมนต์แบบซ้อน หากมีการลงทะเบียนเพรดิเคตและทฤษฎีบท All ให้กับ nesting type
    • standard library ไม่ได้ลงทะเบียนสิ่งนี้ไว้โดยปริยาย ดังนั้นจึงต้องเพิ่ม Scheme All for list. หนึ่งบรรทัดก่อนประกาศ Term
    • Term_ind และ Term_rect ที่สร้างขึ้นจะได้สมมติฐาน list_all Term P l ในกรณี app และในเนื้อหาจะเรียก list_all_forall
    • หากเพิ่ม Scheme All for Forall2. แล้ว ParRed_ind ก็จะให้สมมติฐานอุปนัยสำหรับเงื่อนไขตั้งต้น Forall2 ParRed args args' ด้วย
    • หากไม่ลงทะเบียน จะมีคำเตือน [register-all] พร้อมหลักการแบบอ่อนเดิม
    • ใน Lean ยังต้องจัดเตรียม recursor ที่แข็งแรงเอง

ตัวเลือกการ extract โปรแกรม

  • toolchain มาตรฐานของ Lean คอมไพล์ผ่าน runtime ของตัวเอง ซึ่งมีข้อดีเมื่อสร้างไลบรารี Lean และเมื่อการออกแบบ runtime เหมาะสม
  • lean-zip ที่ผ่านการตรวจพิสูจน์ของ Kim Morrison อาจบีบอัดได้เร็วกว่า miniz_oxide แบบ Rust ล้วนด้วยซ้ำ จึงน่าประทับใจในด้านประสิทธิภาพ
  • อย่างไรก็ตาม Lean ไม่มี backend ทางเลือกสำหรับการ extract หลายแบบ และปัจจุบัน pipeline การคอมไพล์ก็ยังไม่มี การพิสูจน์ความถูกต้องแบบ end-to-end
    • อาจเกิดปัญหาที่พบได้ยาก เช่น runtime bug ที่ Kiran Gopinathan ค้นพบ
    • โค้ดที่สร้างขึ้นถูกปรับให้เฉพาะกับ runtime และไม่ได้ออกแบบมาให้อ่านโดยมนุษย์
  • Rocq มีหลายเส้นทางที่ให้จุดแลกเปลี่ยนระหว่างฐานความเชื่อถือกับความอ่านง่ายต่างกัน

เกมที่รันลอจิกซึ่งผ่านการพิสูจน์แล้ว

  • ใน Rocq มีการพิสูจน์เชิงกลคุณสมบัติของซอร์สโค้ดเดียวกับโปรแกรมที่รันจริง จากนั้น extract ลอจิกและ event loop เป็น C++ ด้วย Crane แล้วเชื่อมกับ SDL2 ผ่าน rocq-crane-sdl2

  • Rocqman

    • Rocqman พิสูจน์ state transition ของเกมที่ frame loop ใช้งาน
      • คะแนนไม่ลดลง
      • จำนวนชีวิตและของสะสมที่เหลือไม่เพิ่มขึ้น
      • สถานะสิ้นสุดเป็นจุดตรึงของ tick
      • ตรวจสอบการเปลี่ยนสถานะของหน้าจอพักเกมและจบเกม

  • Rocqsweeper

    • Rocqsweeper พิสูจน์กฎของ Minesweeper และชั้นอินพุต
      • การคลิกครั้งแรกปลอดภัย
      • การปักธงคงข้อมูลทุ่นระเบิดและข้อมูลช่องข้างเคียงไว้
      • flood fill คงทุ่นระเบิดไว้และไม่เพิ่มจำนวนช่องปลอดภัยที่ถูกซ่อน
      • เคอร์เซอร์ไม่ออกนอกขอบเขต
      • เหตุการณ์จากเมาส์ถูกตีความเป็นเซลล์ที่คาดไว้

  • Reversirocq

    • Reversirocq ใช้ alpha-beta AI แบบ coinductive ของ game tree library เช่นเดียวกับ กฎ Reversi ที่ Charles C. Norton เพิ่มเข้าไป
    • ทฤษฎีบทครอบคลุมการไล่รายชื่อการเดินที่ถูกกฎหมายและผลลัพธ์ของเกม และเชื่อม alpha-beta กับ minimax บน prefix จำกัดที่ถูกค้นหา

  • ขอบเขตการพิสูจน์

    • ขอบเขตของการพิสูจน์สิ้นสุดที่ ซอร์ส Rocq และไม่รวม SDL·Crane·C++ ที่สร้างขึ้น·native runtime
    • ภายในขอบเขตนั้น เป็นการพิสูจน์คุณสมบัติของลอจิกที่รันจริง ไม่ใช่โมเดลที่แยกจากโปรแกรมที่ทำงาน

ระบบนิเวศการพิสูจน์ความถูกต้องของโปรแกรมด้วย Rocq

  • การทำให้นามธรรมในการแทนโปรแกรม

    • Interaction Trees: ใช้ต้นไม้ coinductive ของเหตุการณ์ภายนอกเพื่อแทนโปรแกรมที่มี effect และอาจไม่สิ้นสุด พร้อมให้ denotational semantics และการให้เหตุผลเชิงสมการสำหรับโค้ดที่ไม่บริสุทธิ์
    • Choice Trees: เพิ่มการเลือกแบบไม่กำหนดแน่นอนภายในเพื่อจำลองระบบที่ไม่กำหนดแน่นอน เช่น งานพร้อมกัน

  • เฟรมเวิร์กการพิสูจน์ความถูกต้องของโปรแกรม

    • Iris: เฟรมเวิร์กระดับ higher-order concurrent separation logic สำหรับโปรแกรมที่มีสถานะและงานพร้อมกัน
    • Iris-Lean ก็พัฒนาอย่างรวดเร็วและรองรับฟีเจอร์จำนวนมาก แต่ยังไม่ได้ถูกใช้อย่างกว้างขวางเท่ากับ Rocq Iris
    • CFML: นำซอร์ส OCaml เข้ามาใน Rocq สร้าง characteristic formula และให้ tactic สำหรับสเปก higher-order separation logic
    • Perennial: เฟรมเวิร์กบน Iris สำหรับพิสูจน์ความถูกต้องของระบบพร้อมกัน ระบบจัดเก็บข้อมูลที่ปลอดภัยต่อการขัดข้อง และระบบกระจาย โดยเชื่อมกับโปรแกรมที่รันได้ของส่วนย่อยของ Go ผ่าน Goose
    • VST: Verified Software Toolchain สำหรับพิสูจน์ความถูกต้องเชิงฟังก์ชันของโปรแกรม C บนฐาน semantics ของ CompCert
    • BRiCk: program logic และ toolchain สำหรับโปรแกรม C++ จริง

  • เครื่องมือที่มีแบ็กเอนด์หรือคอมโพเนนต์ของ Rocq

    • Frama-C: แพลตฟอร์มสำหรับการวิเคราะห์และการพิสูจน์เชิงนิรนัยของ C ที่สามารถส่ง proof obligation ไปยัง Rocq ได้
    • Why3: ส่งเป้าหมายจากภาษาของตนเองไปยังตัวพิสูจน์หลายตัว และส่งออก proof obligation แบบโต้ตอบสำหรับ Rocq ได้
    • Cerberus: formal semantics แบบรันได้สำหรับส่วนย่อยขนาดใหญ่ของ C ที่ใช้จริง และมี implementation ใน Rocq สำหรับโมเดลหน่วยความจำ CHERI C

  • semantics ของภาษาจริงและคอมไพเลอร์ที่พิสูจน์แล้ว

    • CompCert: คอมไพเลอร์ C แบบเพิ่มประสิทธิภาพที่ผ่านการพิสูจน์อย่างเป็นทางการ
    • Vellvm: ให้สเปก Rocq และ abstract semantics ของ LLVM IR รวมถึงตัวแปลผลแบบรันได้ที่พิสูจน์แล้วว่าเป็นการทำให้ละเอียดขึ้นของสิ่งเหล่านั้น
    • Vélus: คอมไพเลอร์ที่พิสูจน์แล้วจาก Lustre ไปยัง Clight ของ CompCert
    • WasmCert: formal semantics ที่ทำให้เป็นกลไกของ WebAssembly
    • JSCert: formal semantics ของ JavaScript ที่ติดตามสเปก ECMAScript 5

  • การพิสูจน์แบบน้ำหนักเบาด้วยการแปล

    • hs-to-coq: แปลซอร์ส Haskell เป็น Rocq
    • rocq-of-ocaml: แปลซอร์ส OCaml เป็น Rocq
    • rocq-of-python: แปลซอร์ส Python เป็น Rocq
    • rocq-of-rust: แปลซอร์ส Rust เป็น Rocq
    • Aeneas: แปลง Rust ที่ผ่าน borrow check แล้วให้เป็นโมเดลฟังก์ชันบริสุทธิ์สำหรับการพิสูจน์ความถูกต้อง และรองรับ Lean เป็นเป้าหมายด้วย

  • การสังเคราะห์โปรแกรมและการพาร์ส

    • Fiat Crypto: อนุมานเลขคณิตเชิงเข้ารหัสประสิทธิภาพสูงที่ใช้ได้กับเบราว์เซอร์และไลบรารี TLS ด้วยแนวทาง correct-by-construction
    • Rupicola: เครื่องมือคอมไพล์เชิงสัมพันธ์ที่เปลี่ยนโปรแกรม Gallina เชิงฟังก์ชันระดับล่างให้เป็นโปรแกรม Bedrock2 แบบ imperative
    • Narcissus: อนุมาน encoder และ decoder ของรูปแบบไบนารีด้วยแนวทาง correct-by-construction
    • Verbatim: lexer ที่พิสูจน์แล้วบนฐาน regular expression
    • CoStar: parser ที่พิสูจน์แล้วบนฐานอัลกอริทึม ALL(*)

  • สถานะการบำรุงรักษา

    • บางโครงการไม่ได้รับการบำรุงรักษาอย่างแข็งขัน แต่ยังสามารถมอบหมายให้เอเจนต์ช่วย build และรันใหม่ได้
    • แม้จะพอร์ตองค์ประกอบที่จำเป็นชิ้นหนึ่งไปยัง Lean ได้ในระยะสั้น แต่ความสามารถและประวัติการใช้งานที่สะสมอยู่ทั้งระบบนิเวศจะไม่ถูกย้ายตามไปโดยอัตโนมัติ

ประวัติด้านกฎระเบียบและการรับรอง

  • ไม่มีประสบการณ์การรับรองโดยตรงเกี่ยวกับการยอมรับด้านกฎระเบียบ ซึ่งอาจเป็นปัจจัยที่สำคัญกว่าสำหรับผู้ปฏิบัติงานในยุโรป
  • ANSSI ของฝรั่งเศสเผยแพร่เกณฑ์สำหรับการใช้ Rocq ในการประเมิน Common Criteria
  • CompCert ระบุว่าได้ผ่าน qualification สำเร็จสำหรับคอมพิวเตอร์ MFC_NG ของอากาศยาน ATR 42/72 ในปี 2026 ผ่านงานที่ AbsInt ดำเนินการตามแนวทางของ Airbus
  • ไม่ทราบว่า Lean port จะต้องผ่านข้อกำหนดใดบ้างในสภาพแวดล้อมเดียวกัน และถึงจะพอร์ตได้อย่างเรียบร้อยก็ไม่ได้สืบทอด ประวัติการรับรอง เดิมโดยอัตโนมัติ

เอเจนต์ AI และต้นทุนในการย้าย

  • ตรงข้ามกับสมมติฐานที่ว่าเอเจนต์ AI เขียนได้ดีแค่ Lean นั้น มันก็สามารถเขียนโค้ด Rocq ได้ดีพอเช่นกัน
  • Rocq มีมาตั้งแต่ปลายทศวรรษ 1980 จึงมีทั้งโค้ดและเอกสารสะสมอยู่มาก
  • โมเดลปัจจุบันปรับตัวเข้ากับภาษาที่ไม่คุ้นเคยได้ดีเมื่อมีเอกสารและตัวอย่างให้ ดังนั้นการรู้แค่ภาษายอดนิยมจึงไม่ใช่เหตุผลระยะยาวที่ดีพอสำหรับการเปลี่ยน proof assistant
  • ใน Lean เองก็มีงานพิสูจน์ความถูกต้องของโปรแกรมอย่างจริงจัง เช่น mvcgen และ Velvet
  • หากจะย้ายงานปัจจุบันไปยัง Lean ก็ต้องสร้างนิยามขึ้นใหม่และเปลี่ยนทั้ง extraction pipeline, ไลบรารี และประวัติด้านสถาบัน ดังนั้นตอนนี้ Rocq จึงเหมาะสมกว่า

บทความที่เกี่ยวข้อง

ยังไม่มีความคิดเห็น

ยังไม่มีความคิดเห็น