admission runs the containment checker extracted from rocq

2 files changed, 128 insertions, 3 deletions

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))