Vì sao Rocq tốt hơn Lean trong kiểm chứng chương trình

 (joomy.korkutblech.com)
1 điểm bởi GN⁺ 2 giờ trước | Chưa có bình luận nào. | Chia sẻ qua WhatsApp
  • Dù đà tăng trưởng của Lean trong hình thức hóa toán học là rõ rệt, với kiểm chứng chương trình có thể thực thi, Rocq phù hợp hơn nhờ có đồng quy nạp native, nhiều đường dẫn trích xuất và một hệ sinh thái kiểm chứng đã tích lũy
  • Rocq khai báo dữ liệu đồng quy nạp bằng CoInductive và CoFixpoint, kiểm tra guardedness rồi trích xuất thành mã thực thi lười, trong khi ở Lean phải chọn một trong các cách: mã hóa bằng thư viện, iterator, Thunk hoặc partial def
  • Bộ kiểm tra kiểu quy nạp lồng nhau của Lean từ chối một số quan hệ kiểm chứng mà Rocq cho phép; trong ví dụ JSON schema, cần tách một chứng minh Forall₂ thành nhiều quan hệ và chuẩn bị nguyên lý quy nạp riêng
  • Rocq cung cấp các đường dẫn trích xuất chương trình như OCaml, Haskell, Rust, C++, WebAssembly, cùng các nền tảng kiểm chứng như Iris, CompCert, Interaction Trees, giúp nối logic đã được kiểm chứng của game thực tế với mã thực thi
  • Tác tử AI cũng có thể viết mã Rocq nếu có tài liệu và ví dụ; để chuyển sang Lean không chỉ phải thay thế định nghĩa mà còn cả pipeline trích xuất, thư viện, lịch sử pháp quy và thể chế, nên với công việc hiện tại lợi ích thực tế là không đủ

So sánh theo tiêu chí kiểm chứng chương trình

  • Đối tượng so sánh không phải là hình thức hóa toán học mà là kiểm chứng chương trình; trong lĩnh vực toán học, Lean thực sự có động lực tăng trưởng
  • “Tốt hơn” không phải là ưu thế tuyệt đối, mà có nghĩa là Rocq phù hợp hơn với công việc đang thực hiện hiện nay
  • Khi thành quả của AI trong lĩnh vực toán học và sự quan tâm dành cho Lean tăng lên, tôi thường được hỏi vì sao vẫn tiếp tục dùng Rocq; luận điểm này bắt đầu từ các slide của bài keynote LangSec

Kiểu đồng quy nạp native và cofixpoint

  • Phạm vi mà coinductive của Lean cung cấp

    • Hỗ trợ vị từ đồng quy nạp do Wojciech Różowski và Joachim Breitner của Lean FRO phát triển đã được đưa vào lệnh coinductive của Lean 4.25
    • Tính năng này hữu ích cho bisimulation và chứng minh đồng quy nạp, nhưng không cung cấp cofixpoint có thể thực thi trong Type hay chương trình có thể trích xuất
    • CoInductive và CoFixpoint của Rocq cung cấp trực tiếp dữ liệu đồng quy nạp (codata) có thể thực thi trong Type
    • Lean không có khai báo kernel tương ứng, nên phải dùng hàm/cấu trúc thông thường hoặc mã hóa bằng thư viện

  • Ràng buộc khai báo của QPFTypes

    • QPFTypes của Alex Keizer là một gói proof-of-concept cho dữ liệu đồng quy nạp tổng quát, sinh ra các nguyên lý destructor, corecursor và bisimulation từ đặc tả codata
    • Khác với CoInductive của Rocq, đây là mã hóa bằng thư viện chứ không phải khai báo kernel
    • Ví dụ sử dụng toolchain cố định Lean 4.25.0, phiên bản hỗ trợ mới nhất lúc đó
    • Trong Rocq, ba khai báo bình thường sau không hoạt động trong QPFTypes
      • Dữ liệu đồng quy nạp không có tham số thất bại do lỗi triển khai
      • Khai báo đồng quy nạp tương hỗ như tree và forest không được hỗ trợ vì ràng buộc mutual block của Lean
      • Các họ đồng quy nạp có chỉ số như istream, nơi chỉ số clock tiến lên ở mỗi bước, không được hỗ trợ do giới hạn của chính QPF
    • Các mẫu đồng quy nạp có chỉ số cũng được dùng trong giao thức, giai đoạn, kích thước và state machine, nhưng nếu vượt ra ngoài phạm vi đơn giản, không tương hỗ, không chỉ số của QPFTypes, phải trực tiếp dùng API cấp thấp MvQPF.Cofix.corec và bisim, hoặc không thể triển khai
    • Rocq cũng khó xử lý bộ kiểm tra guardedness, nhưng các trường hợp trên có thể khai báo mà không cần mã hóa riêng
    • Paco và coinduction của Damien Pous hỗ trợ vị từ đồng quy nạp và chứng minh quan hệ, nhưng không thay thế CoFixpoint dành cho chương trình

  • Khác biệt của chương trình được trích xuất

    • Cofixpoint native của Rocq được trích xuất thành giá trị OCaml lười thực sự
    • unfold_cotree của game tree library trở thành cây được bọc bằng Lazy.t và hàm sinh lười đệ quy
    • Kết quả gần với cấu trúc cây lười mà con người có thể tự viết
    • Trong QPFTypes, việc sinh và quan sát đi qua MvQPF.Cofix.corec và MvQPF.Cofix.dest, và chương trình được trích xuất cũng giữ biểu diễn Cofix đã tổng quát hóa
    • BadCoinduction.lean chứa Colist, Cotree, giao diện được sinh ra, các trường hợp thất bại của dữ liệu đồng quy nạp không tham số, tương hỗ và có chỉ số, cùng commit QPFTypes và các lệnh để tái hiện

Các lựa chọn thay thế trong Lean

  • Stream và iterator

    • Stream' của mathlib là hàm Nat → α
    • Có thể tính phần tử tại vị trí n và cung cấp corecursor, tính mở rộng, bisimulation và các bổ đề hỗ trợ đồng quy nạp
    • Tuy nhiên, nó không phải là constructor sinh lười với phần đuôi là một stream khác, và cũng không giải quyết được mọi loại đồng dữ liệu tương hỗ hay có chỉ số tùy ý
    • Một máy trạng thái dùng trạng thái tường minh và hàm step cũng có thể đóng vai trò corecursor
    • Iter của Lean là một giao diện tuần tự tính từng bước theo yêu cầu
    • Iterator có thể có chứng minh Productive bảo đảm sinh giá trị hoặc kết thúc; Iter.repeat đã được cung cấp sẵn chứng minh này
    • Với iterator tự định nghĩa, người dùng phải tự cung cấp giao diện step, bất biến và, nếu cần, chứng minh tính sinh sản
    • CoFixpoint của Rocq kiểm tra guardedness của lời gọi đệ quy và trả về giá trị đồng quy nạp mà không cần công việc kết nối riêng giữa máy trạng thái và chuỗi

  • Thunk, partial def, unsafe def

    • Thunk của Lean tính khi bị ép lần đầu trong mã đã biên dịch và cache kết quả, nhưng không cung cấp đồng quy nạp
    • Trong logic, nó trông như Unit → α, nên có thể dùng toàn bộ định nghĩa trong chứng minh, nhưng cache thì không hiển thị
    • Nó cũng không cho phép đệ quy hay kiểm tra liệu đệ quy cuối cùng có sinh ra constructor hay không
    • Mã trích xuất của Rocq cũng dùng tính lười ở runtime, nhưng trước hết phải vượt qua kiểm tra guardedness
    • partial def có thể thực thi thân đệ quy, nhưng trong logic chỉ còn lại một hằng số mờ
    • Không kiểm tra tính kết thúc hay tính sinh sản, nên chấp nhận cả producer số tự nhiên lẫn producer lập tức đệ quy vô hạn
    • unsafe def cũng có thể thực thi, nhưng không thể được tham chiếu trong các khai báo theorem-safe
    • MLList của Batteries kết hợp triển khai lười unsafe riêng tư, giao diện công khai mờ, và các producer fix·iterate viết bằng partial def
    • Những producer như vậy không thể được unfold trong chứng minh như cofixpoint Rocq quan sát được
    • partial_fixpoint giữ lại phương trình, nhưng không chấp nhận đệ quy kết hợp constructor và thunk
    • QPFTypes cung cấp corecursor và nguyên lý bisimulation để tránh tính mờ, nhưng phải chấp nhận biểu diễn Cofix tổng quát và các ràng buộc khai báo

Chương trình có hiệu ứng và không kết thúc

  • Interaction Trees biểu diễn các chương trình có hiệu ứng và có thể không kết thúc dưới dạng cây đồng quy nạp
    • Có thể viết, diễn giải và trích xuất chương trình bằng cùng một cây, đồng thời chứng minh các phương trình thường bao gồm cả weak bisimulation
  • Stream' và Iter chỉ cung cấp chuỗi, nên không thể biểu diễn continuation phân nhánh cần cho hiệu ứng
  • Nếu chạy cây hiệu ứng bằng Thunk và partial def, producer đệ quy trở nên mờ trong chứng minh; để hỗ trợ cả tính toán lẫn chứng minh, cần mã hóa bằng thư viện đồng dữ liệu
  • lean4-itree của MIT PLV triển khai Interaction Trees bằng final coalgebra PFunctor.M của Mathlib
  • PolyFun bổ sung handler, thủ tục đệ quy, vết thực thi, strong/weak bisimulation cùng chứng minh các luật monad và iteration
    • Có thể tính toán và chứng minh cây trong Lean, nhưng vẫn là M-type được mã hóa bằng thư viện
    • Không có khai báo đồng dữ liệu native, và thay vì chương trình lười trực tiếp thì vẫn duy trì biểu diễn tổng quát
  • HITrees cũng không vượt qua được ràng buộc này
    • Vì Lean không có kiểu đồng quy nạp native, nên không dùng cách tiếp cận Delay-monad đồng quy nạp của ITrees
    • Cây là quy nạp, còn tính không kết thúc trở thành hiệu ứng đệ quy bậc cao
    • Tính toán đệ quy nhận được ý nghĩa khi handler diễn giải hiệu ứng, chứ không phải là cây vô hạn có thể quan sát và unfold
    • Có thể thực thi bằng diễn giải monadic và chứng minh bằng diễn giải máy trạng thái, nhưng lý thuyết phương trình của HITree không cung cấp phương trình unfold đệ quy thông thường
  • Rocq hỗ trợ khai báo đồng dữ liệu, producer có guardedness, suy luận dựa trên quan sát và trích xuất mã lười trực tiếp trong một luồng thống nhất

Kiểu và vị từ quy nạp lồng nhau

  • Ví dụ xác minh JSON Schema

    • Lean cho phép nhiều định nghĩa quy nạp lồng nhau, nhưng lại từ chối một số định nghĩa mà Rocq chấp nhận
    • Khác biệt này đã được dùng trong A Rose Tree Is Blooming, và có thể tái hiện bằng một ví dụ JSON Schema nhỏ hơn
    • Bản thân JSON và schema đều có thể được định nghĩa không vấn đề gì trong cả hai ngôn ngữ
    • Khi xác minh schema đối tượng, cần kiểm tra theo từng cặp rằng tên trường khớp nhau và mỗi giá trị JSON là hợp lệ với schema con tương ứng
    • Rocq có thể lưu cả tính bằng nhau của tên và phép xác minh đệ quy trong một dẫn xuất Forall2
    • Rocq 9.0 từ chối lambda dạng tuple-pattern quanh lần xuất hiện đệ quy vì vi phạm strict positivity, nhưng nếu dùng projection thay cho pattern thì biên dịch được
    • Lean 4.32.1 từ chối And bên trong như một kiểu dữ liệu quy nạp lồng nhau không hợp lệ khi lần xuất hiện đệ quy trong cùng constructor đối tượng đi qua cả Forall₂ lẫn And
    • Các dạng lân cận như Forall₂ ParRed, đệ quy trực tiếp qua And·Exists, và Forall₂ (fun sf jf => Valid sf.2 jf.2) thì được chấp nhận
    • Forall₂ (Eval env), trong đó tham số quan hệ bắt giữ biến cục bộ env của constructor, thất bại ở bước Forall₂

  • Cách обход và chi phí chứng minh

    • Trong Lean, có thể tách xác minh đối tượng thành hai dẫn xuất Forall₂
      • Một dẫn xuất bảo toàn tính bằng nhau của tên trường
      • Dẫn xuất còn lại bảo toàn phép xác minh đệ quy của giá trị tương ứng
    • Có thể giữ nguyên cấu trúc danh sách mà không cần chỉ mục riêng hay chứng minh độ dài, và cũng có thể chứng minh việc loại bỏ head theo cấu trúc, nhưng phải phân rã cả hai dẫn xuất
    • Khi tách quan hệ, sẽ mất một đối tượng chứng minh duy nhất ghép từng tính bằng nhau của tên với phép xác minh đệ quy thành một cặp
    • Có thể khôi phục sự ghép nối bằng quan hệ tương hỗ ValidFields, nhưng tactic induction của Lean không hỗ trợ kiểu quy nạp tương hỗ, và recursor được sinh ra cũng yêu cầu motive cho từng quan hệ
    • Nếu tạo định lý quy nạp tùy chỉnh, có thể che giấu phần thiết lập này
    • Rocq vẫn giữ biểu diễn Forall2 chuẩn; nếu cần định nghĩa tương hỗ, có thể sinh nguyên lý kết hợp bằng Scheme
    • Lean cũng có thể biểu diễn cùng mệnh đề mà không cần mã hóa dựa trên chỉ mục, nhưng phải sắp xếp lại khai báo và tạo thêm nhiều cơ chế chứng minh hơn
    • Tệp so sánh đầy đủ nằm tại NestedPain.v cho Rocq 9.0.0 và NestedPain.lean cho Lean 4.32.1; các lỗi dự kiến của Lean được kiểm tra khi biên dịch bằng #guard_msgs

  • Nguyên lý quy nạp mạnh cho đối số lồng nhau

    • Trong các chứng minh cần giả thiết theo từng phần tử của dữ liệu lồng nhau, chẳng hạn khi Term chứa list Term, cả hai hệ thống đều cần recursor mạnh hơn
    • Rocq 9.2 sinh giả thiết quy nạp cho đối số lồng nhau nếu đăng ký vị từ All và các định lý cho nesting type
    • Thư viện chuẩn không đăng ký sẵn điều này, nên cần thêm một dòng Scheme All for list. trước khai báo Term
    • Term_ind và Term_rect được sinh ra sẽ nhận giả thiết list_all Term P l trong trường hợp app, và phần thân gọi list_all_forall
    • Nếu thêm Scheme All for Forall2., ParRed_ind cũng cung cấp giả thiết quy nạp cho tiền đề Forall2 ParRed args args'
    • Nếu không đăng ký, sẽ xuất hiện cảnh báo [register-all] cùng với nguyên lý yếu cũ
    • Trong Lean, vẫn phải tự chuẩn bị recursor mạnh

Các lựa chọn trích xuất chương trình

  • Chuỗi công cụ chuẩn của Lean biên dịch thông qua runtime riêng, và có lợi thế khi xây dựng thư viện Lean cũng như khi thiết kế runtime phù hợp
  • lean-zip đã được kiểm chứng của Kim Morrison thậm chí có thể nén nhanh hơn miniz_oxide viết bằng Rust thuần, cho thấy hiệu năng rất ấn tượng
  • Tuy nhiên Lean không cung cấp nhiều backend trích xuất thay thế, và pipeline biên dịch hiện tại không có chứng minh tính đúng đắn đầu cuối
    • Có thể xảy ra các vấn đề hiếm gặp như lỗi runtime mà Kiran Gopinathan phát hiện
    • Mã sinh ra được chuyên biệt hóa cho runtime và không được thiết kế để con người đọc
  • Rocq có nhiều con đường với các đánh đổi khác nhau giữa nền tảng tin cậy và khả năng đọc

Game chạy logic đã được kiểm chứng

  • Trong Rocq, sau khi kiểm chứng bằng máy các thuộc tính của cùng mã nguồn với chương trình thực thi, logic và event loop được trích xuất sang C++ bằng Crane rồi kết nối với SDL2 bằng rocq-crane-sdl2

  • Rocqman

    • Rocqman chứng minh các chuyển đổi trạng thái game mà frame loop sử dụng
      • Điểm số không giảm
      • Mạng và số vật phẩm còn lại không tăng
      • Trạng thái kết thúc là điểm cố định của tick
      • Kiểm tra các chuyển đổi sang tạm dừng và màn hình kết thúc

  • Rocqsweeper

    • Rocqsweeper chứng minh luật Minesweeper và tầng nhập liệu
      • Cú nhấp đầu tiên an toàn
      • Đánh dấu cờ bảo toàn dữ liệu mìn và dữ liệu ô lân cận
      • Flood fill bảo toàn mìn và không làm tăng số ô an toàn còn ẩn
      • Con trỏ không vượt ra ngoài biên
      • Sự kiện chuột được diễn giải thành ô như dự kiến

  • Reversirocq

    • Reversirocq dùng AI alpha-beta đồng quy nạp của cùng game tree library với luật Reversi do Charles C. Norton bổ sung
    • Các định lý xử lý việc liệt kê nước đi hợp lệ và kết quả ván chơi, đồng thời liên kết alpha-beta với minimax trên prefix hữu hạn được tìm kiếm

  • Ranh giới kiểm chứng

    • Ranh giới chứng minh kết thúc ở mã nguồn Rocq; SDL, Crane, C++ được sinh ra và runtime native không nằm trong phạm vi này
    • Bên trong ranh giới đó, các thuộc tính được chứng minh là của logic thực thi thật, chứ không phải một mô hình tách rời khỏi chương trình thực thi

Hệ sinh thái kiểm chứng chương trình của Rocq

  • Trừu tượng hóa biểu diễn chương trình

    • Interaction Trees: biểu diễn các chương trình có hiệu ứng và có thể không kết thúc dưới dạng cây đồng quy nạp của các sự kiện bên ngoài, đồng thời cung cấp ngữ nghĩa biểu thị và suy luận phương trình cho mã không thuần
    • Choice Trees: thêm lựa chọn bất định nội bộ để mô hình hóa các hệ thống bất định như đồng thời

  • Framework kiểm chứng chương trình

    • Iris: framework concurrent separation logic bậc cao cho các chương trình có trạng thái và đồng thời
    • Iris-Lean cũng đang phát triển nhanh và hỗ trợ nhiều tính năng, nhưng chưa được sử dụng rộng rãi như Rocq Iris
    • CFML: đưa mã nguồn OCaml vào Rocq, tạo characteristic formula và cung cấp tactic cho đặc tả separation logic bậc cao
    • Perennial: framework dựa trên Iris để kiểm chứng tính đồng thời, kho lưu trữ an toàn trước sự cố và hệ thống phân tán; liên kết với chương trình thực thi của một tập con Go thông qua Goose
    • VST: Verified Software Toolchain chứng minh tính đúng đắn hàm của chương trình C dựa trên ngữ nghĩa CompCert
    • BRiCk: logic chương trình và toolchain cho các chương trình C++ thực tế

  • Công cụ có backend hoặc thành phần Rocq

    • Frama-C: nền tảng phân tích và kiểm chứng suy diễn cho C, có thể chuyển các nghĩa vụ chứng minh sang Rocq
    • Why3: gửi các mục tiêu trong ngôn ngữ riêng của mình tới nhiều bộ chứng minh và có thể xuất các nghĩa vụ chứng minh tương tác cho Rocq
    • Cerberus: ngữ nghĩa hình thức có thể thực thi cho một tập con C lớn và thực dụng, với bản triển khai Rocq cho mô hình bộ nhớ CHERI C

  • Ngữ nghĩa của ngôn ngữ thực tế và compiler đã kiểm chứng

    • CompCert: compiler C tối ưu hóa đã được kiểm chứng hình thức
    • Vellvm: cung cấp đặc tả Rocq và ngữ nghĩa trừu tượng của LLVM IR, cùng một interpreter thực thi đã được chứng minh là tinh chỉnh các đặc tả đó
    • Vélus: compiler đã kiểm chứng từ Lustre sang Clight của CompCert
    • WasmCert: ngữ nghĩa hình thức được cơ giới hóa của WebAssembly
    • JSCert: ngữ nghĩa hình thức JavaScript bám theo đặc tả ECMAScript 5

  • Kiểm chứng nhẹ dựa trên dịch mã

    • hs-to-coq: dịch mã nguồn Haskell sang Rocq
    • rocq-of-ocaml: dịch mã nguồn OCaml sang Rocq
    • rocq-of-python: dịch mã nguồn Python sang Rocq
    • rocq-of-rust: dịch mã nguồn Rust sang Rocq
    • Aeneas: chuyển Rust đã vượt qua borrow check thành mô hình hàm thuần để kiểm chứng, đồng thời cũng hỗ trợ Lean làm đích

  • Tổng hợp chương trình và parsing

    • Fiat Crypto: suy dẫn theo cách correct-by-construction các phép toán số học mật mã hiệu năng cao có thể dùng trong trình duyệt và thư viện TLS
    • Rupicola: công cụ biên dịch quan hệ chuyển các chương trình Gallina hàm cấp thấp thành chương trình mệnh lệnh Bedrock2
    • Narcissus: suy dẫn encoder và decoder correct-by-construction cho các định dạng nhị phân
    • Verbatim: lexer đã kiểm chứng dựa trên biểu thức chính quy
    • CoStar: parser đã kiểm chứng dựa trên thuật toán ALL(*)

  • Tình trạng bảo trì

    • Một số dự án không còn được bảo trì tích cực, nhưng vẫn có thể giao cho agent build lại và chạy được
    • Ngay cả khi có thể port một thành phần cần thiết sang Lean trong thời gian ngắn, điều đó cũng không tự động chuyển toàn bộ chức năng và lịch sử sử dụng mà hệ sinh thái đã tích lũy

Lịch sử quản lý và chứng nhận

  • Không có kinh nghiệm chứng nhận trực tiếp về việc được cơ quan quản lý chấp nhận; đây có thể là yếu tố đặc biệt quan trọng hơn đối với người làm việc ở châu Âu
  • ANSSI của Pháp đã công bố tiêu chí để sử dụng Rocq trong đánh giá Common Criteria
  • CompCert cho biết, thông qua công việc do AbsInt thực hiện theo hướng dẫn của Airbus, họ đã qualification thành công cho máy tính MFC_NG trên máy bay ATR 42/72 vào năm 2026
  • Không rõ một bản port Lean sẽ phải đáp ứng những yêu cầu nào trong cùng môi trường, và dù port sạch sẽ cũng không tự động kế thừa lịch sử chứng nhận hiện có

AI agent và chi phí chuyển đổi

  • Trái với giả định rằng AI agent chỉ viết tốt Lean, chúng cũng có thể viết mã Rocq đủ tốt
  • Rocq đã tồn tại từ cuối thập niên 1980 nên có rất nhiều mã và tài liệu được tích lũy
  • Các mô hình hiện nay thích nghi tốt với cả những ngôn ngữ chưa quen nếu được cung cấp tài liệu và ví dụ, vì vậy lý do chỉ biết các ngôn ngữ phổ biến không phải là căn cứ dài hạn để đổi proof assistant
  • Trong Lean cũng đang có các công việc kiểm chứng chương trình nghiêm túc như mvcgen và Velvet
  • Để chuyển công việc hiện tại sang Lean, cần tái cấu trúc các định nghĩa và thay thế pipeline trích xuất, thư viện cũng như lịch sử thể chế, nên hiện tại Rocq phù hợp hơn

Bài viết liên quan

Chưa có bình luận nào.

Chưa có bình luận nào.