admission runs the containment checker extracted from rocq

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
 
diff --git a/lib/dune b/lib/dune
index 2d9154e..3f8be6f 100644
--- a/lib/dune
+++ b/lib/dune
@@ -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))