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/virtual-machine-specification.org | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'docs/virtual-machine-specification.org') 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