diff options
Diffstat (limited to 'docs/virtual-machine-specification.org')
| -rw-r--r-- | docs/virtual-machine-specification.org | 11 |
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 |