diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/extraction.org | 50 | ||||
| -rw-r--r-- | docs/virtual-machine-specification.org | 11 | ||||
| -rw-r--r-- | lib/dune | 9 | ||||
| -rw-r--r-- | lib/extract.v | 9 | ||||
| -rw-r--r-- | lib/pattern.ml | 40 | ||||
| -rw-r--r-- | test/test_vm.ml | 15 | ||||
| -rw-r--r-- | theories/DecreaseChecker.v | 118 | ||||
| -rw-r--r-- | theories/dune | 13 |
8 files changed, 253 insertions, 12 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 @@ -3,6 +3,15 @@ (public_name sol) (libraries zarith)) +; The proven containment checker, extracted from Rocq. The .v files +; are the source of truth; the generated module is a build artifact. +(rule + (targets decrease_extracted.ml decrease_extracted.mli) + (deps extract.v ../theories/DecreaseChecker.vo) + (action + (setenv OCAMLPATH "" + (run coqc -q -Q ../theories "" extract.v)))) + (ocamllex lexer) (menhir diff --git a/lib/extract.v b/lib/extract.v new file mode 100644 index 0000000..5c8ff7c --- /dev/null +++ b/lib/extract.v @@ -0,0 +1,9 @@ +(* Extraction driver: turns the proven checker of + theories/DecreaseChecker.v into lib/decrease_extracted.ml, which + Pattern.strictly_contains runs. Kept beside the library so the + generated module lands where dune collects it. *) + +From Stdlib Require Import Extraction ExtrOcamlBasic. +Require Import DecreaseChecker. + +Extraction "decrease_extracted.ml" contains term_eqb. diff --git a/lib/pattern.ml b/lib/pattern.ml index 823162c..5186e04 100644 --- a/lib/pattern.ml +++ b/lib/pattern.ml @@ -64,13 +64,41 @@ let rec equal a b = | Record x, Record y -> Label.Map.equal equal x y | _ -> false +(* Containment runs the checker extracted from + theories/DecreaseChecker.v, whose soundness and decrease are + proven. The trusted seam is this conversion (injective by leaf + kind) and the two equality functions. *) +type checker_leaf = + | L_var of string + | L_int of Z.t + | L_rat of Q.t + | L_str of string + | L_nil + +let checker_leaf_equal a b = + match (a, b) with + | L_var x, L_var y | L_str x, L_str y -> String.equal x y + | L_int x, L_int y -> Z.equal x y + | L_rat x, L_rat y -> Q.equal x y + | L_nil, L_nil -> true + | _ -> false + +let rec to_checker = function + | Var v -> Decrease_extracted.Leaf (L_var v) + | Integer z -> Decrease_extracted.Leaf (L_int z) + | Rational q -> Decrease_extracted.Leaf (L_rat q) + | String s -> Decrease_extracted.Leaf (L_str s) + | Nil -> Decrease_extracted.Leaf L_nil + | Record map -> + Decrease_extracted.Node + (List.fold_right + (fun (label, value) rest -> + Decrease_extracted.FCons (label, to_checker value, rest)) + (Label.Map.bindings map) Decrease_extracted.FNil) + let strictly_contains pattern ~sub = - let rec inside p = equal p sub || strictly p - and strictly = function - | Record map -> Label.Map.exists (fun _ p -> inside p) map - | _ -> false - in - strictly pattern + Decrease_extracted.contains Label.equal checker_leaf_equal (to_checker sub) + (to_checker pattern) let rec pp fmt = function | Var v -> Format.pp_print_string fmt v diff --git a/test/test_vm.ml b/test/test_vm.ml index 38bbcc9..bf7ea35 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -130,6 +130,19 @@ let test_loop_rule_rejected () = | Error _ -> () | Ok _ -> Alcotest.fail "a rule with no structural decrease must be rejected" +let test_fresh_variable_is_no_decrease () = + (* The recursive argument is a fresh variable, not a subterm of + the head. Leaf identity matters here: a checker that conflated + variables would wrongly accept this rule. *) + match + load + {| + Rule name: "cheat" head: [Cheat list: #(H | T)] body: [Cheat list: Z] + |} + with + | Error _ -> () + | Ok _ -> Alcotest.fail "a fresh variable is not a structural decrease" + let test_mutual_recursion_rejected () = match load @@ -303,6 +316,8 @@ let () = ( "totality", [ Alcotest.test_case "loop rejected" `Quick test_loop_rule_rejected; + Alcotest.test_case "fresh variable is no decrease" `Quick + test_fresh_variable_is_no_decrease; Alcotest.test_case "mutual recursion rejected" `Quick test_mutual_recursion_rejected; Alcotest.test_case "unbounded membership rejected" `Quick diff --git a/theories/DecreaseChecker.v b/theories/DecreaseChecker.v new file mode 100644 index 0000000..d24887a --- /dev/null +++ b/theories/DecreaseChecker.v @@ -0,0 +1,118 @@ +(* The executable admission checker, proven and extracted. + + Decrease.v states the abstract argument: strict containment + decreases a well founded measure. This file carries the argument + over to an executable checker faithful to lib/pattern.ml: terms + keep their labels and leaf identities, the checker is a boolean + function, and its soundness is proven, so extraction can replace + the hand written OCaml. The equality functions supplied by the + host and the conversion from Pattern.t are the remaining trusted + seam. *) + +From Stdlib Require Import Arith Lia Bool Wf_nat. + +Section Checker. + Variables (L A : Type). + Variables (eqL : L -> L -> bool) (eqA : A -> A -> bool). + + (* Terms as the checker sees them: leaves carry their identity + (variable name, scalar value), nodes carry labeled fields in + canonical order. Mirrors Pattern.t through an injective + conversion. *) + Inductive term : Type := + | Leaf : A -> term + | Node : fields -> term + with fields : Type := + | FNil : fields + | FCons : L -> term -> fields -> fields. + + Scheme term_mut := Induction for term Sort Prop + with fields_mut := Induction for fields Sort Prop. + Combined Scheme term_fields_mut from term_mut, fields_mut. + + Fixpoint term_eqb (x y : term) : bool := + match x, y with + | Leaf a, Leaf b => eqA a b + | Node f, Node g => fields_eqb f g + | _, _ => false + end + with fields_eqb (f g : fields) : bool := + match f, g with + | FNil, FNil => true + | FCons l t r, FCons l' t' r' => + eqL l l' && term_eqb t t' && fields_eqb r r' + | _, _ => false + end. + + (* Strict containment: [sub] occurs somewhere inside the fields of + [t], at depth one or more. *) + Fixpoint contains (sub t : term) : bool := + match t with + | Leaf _ => false + | Node f => fields_contain sub f + end + with fields_contain (sub : term) (f : fields) : bool := + match f with + | FNil => false + | FCons _ t r => term_eqb t sub || contains sub t || fields_contain sub r + end. + + Fixpoint size (t : term) : nat := + match t with + | Leaf _ => 1 + | Node f => S (fields_size f) + end + with fields_size (f : fields) : nat := + match f with + | FNil => 0 + | FCons _ t r => size t + fields_size r + end. + + Hypothesis eqL_sound : forall x y, eqL x y = true -> x = y. + Hypothesis eqA_sound : forall x y, eqA x y = true -> x = y. + + Lemma eqb_sound_all : + (forall x, forall y, term_eqb x y = true -> x = y) + /\ (forall f, forall g, fields_eqb f g = true -> f = g). + Proof. + apply term_fields_mut. + - intros a y H; destruct y; simpl in H; [ f_equal; auto | discriminate ]. + - intros f IH y H; destruct y; simpl in H; [ discriminate | f_equal; auto ]. + - intros g H; destruct g; [ reflexivity | discriminate ]. + - intros l t IHt r IHr g H; destruct g; simpl in H; [ discriminate | ]. + rewrite !andb_true_iff in H; destruct H as [[Hl Ht] Hr]. + f_equal; auto. + Qed. + + Definition term_eqb_sound := proj1 eqb_sound_all. + + Lemma contains_size_all : + (forall t, forall sub, contains sub t = true -> size sub < size t) + /\ (forall f, forall sub, fields_contain sub f = true -> size sub <= fields_size f). + Proof. + apply term_fields_mut. + - intros a sub H; simpl in H; discriminate. + - intros f IH sub H; simpl in H; simpl. + specialize (IH _ H); lia. + - intros sub H; simpl in H; discriminate. + - intros l t IHt r IHr sub H; simpl in H; simpl. + rewrite !orb_true_iff in H; destruct H as [[He | Hc] | Hr]. + + apply term_eqb_sound in He; subst; lia. + + specialize (IHt _ Hc); lia. + + specialize (IHr _ Hr); lia. + Qed. + + Definition contains_decreases := proj1 contains_size_all. + + (* The checker's acceptance order is well founded: any chain of + recursive unfoldings whose argument the checker accepts is + finite. This is what admission buys at runtime. *) + Definition decrease (b a : term) : Prop := contains b a = true. + + Theorem decrease_well_founded : well_founded decrease. + Proof. + apply well_founded_lt_compat with (f := size). + intros x y H; apply contains_decreases; exact H. + Qed. + +End Checker. diff --git a/theories/dune b/theories/dune index 895fc92..3ef9648 100644 --- a/theories/dune +++ b/theories/dune @@ -1,6 +1,6 @@ ; Checked with rocq's coqc directly: the coq.theory stanza trips on -; the devshell's OCaml findlib path, and a plain rule with a clean -; environment is enough to keep the proofs in the default build. +; the devshell's OCaml findlib path, and plain rules with a clean +; environment are enough to keep the proofs in the default build. (rule (targets Decrease.vo Decrease.glob) (deps Decrease.v) @@ -8,6 +8,13 @@ (setenv OCAMLPATH "" (run coqc -q Decrease.v)))) +(rule + (targets DecreaseChecker.vo DecreaseChecker.glob) + (deps DecreaseChecker.v) + (action + (setenv OCAMLPATH "" + (run coqc -q DecreaseChecker.v)))) + (alias (name default) - (deps Decrease.vo)) + (deps Decrease.vo DecreaseChecker.vo)) |