admission runs the containment checker extracted from rocq

1 files changed, 8 insertions, 3 deletions

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