From f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 22:03:21 -0300 Subject: admission runs the containment checker extracted from rocq --- docs/extraction.org | 50 ++++++++++++++++++++++++++++++++++ docs/virtual-machine-specification.org | 11 ++++++-- 2 files changed, 58 insertions(+), 3 deletions(-) create mode 100644 docs/extraction.org (limited to 'docs') diff --git a/docs/extraction.org b/docs/extraction.org new file mode 100644 index 0000000..17ce70d --- /dev/null +++ b/docs/extraction.org @@ -0,0 +1,50 @@ +#+TITLE: Extraction + +* About + +Decision 10 says the thing proven should be the thing running. This +document describes the first instance: the structural containment +check that admission relies on is extracted from Rocq and linked +into the library, replacing the hand written OCaml. + +* The pieces + +- =theories/Decrease.v= states the abstract argument: strict + containment decreases a natural measure and the induced order is + well founded. +- =theories/DecreaseChecker.v= carries the argument to an executable + checker faithful to the real term shape: leaves keep their + identity (variable names, scalar values) and nodes keep their + labels. Both matter; a checker that conflated two variables or two + label sets would accept rules that do not decrease. The file + proves the boolean checker sound (a successful check is real + containment) and proves the decrease theorem over it. +- =lib/extract.v= drives extraction into =decrease_extracted.ml=, a + build artifact generated by dune, never committed. +- =lib/pattern.ml= converts a pattern into the checker's term shape + and calls the extracted function. + +* The trusted seam + +Extraction does not remove trust, it narrows it. What remains +outside the proofs: + +- the conversion from =Pattern.t= to the checker's terms, injective + by construction: each leaf kind is distinct and records become + labeled field lists in canonical order; +- the two equality functions handed to the checker, label equality + and leaf equality, which are the standard equalities of their + types; +- the admission logic around the check, and the engine itself. + +The regression suite pins the sharp edge: a recursive rule whose +call argument is a fresh variable must be rejected, which fails on +any checker that conflates leaf identities. + +* Building + +The proofs compile as part of the default build through plain dune +rules that call =coqc= with a clean =OCAMLPATH= (the =coq.theory= +stanza clashes with the devshell's OCaml). The Rocq standard library +comes from =pkgs.coqPackages.stdlib=, packaged separately from Rocq +itself. diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org index 8699f94..90cc6c0 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -75,9 +75,14 @@ piece machine checkable and one piece machine checked today: bounded generators enumerate finite ranges; 4. disjunction and rule choice branch finitely. -The remaining trusted gap between the OCaml checker and the Rocq -statement closes by extraction (decision 10): the admission checker -is the piece to extract first. +The containment check itself is no longer hand written: admission +runs the checker extracted from =theories/DecreaseChecker.v=, where +its soundness (a successful check really is strict containment, +leaves and labels included) and the decrease theorem are proven. +What remains trusted: the injective conversion from =Pattern.t= to +the checker's term shape, the two equality functions handed to it, +and the surrounding admission logic. Each future extraction shrinks +that list. * Integrity control hooks -- cgit v1.2.3