admission runs the containment checker extracted from rocq

1 files changed, 50 insertions, 0 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.