admission runs the containment checker extracted from rocq

2 files changed, 58 insertions, 3 deletions

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