lexicographic order proven well founded, checker extracted and verifying admission

4 files changed, 36 insertions, 3 deletions

diff --git a/lib/dune b/lib/dune
index 3f8be6f..896800b 100644
--- a/lib/dune
+++ b/lib/dune
@@ -7,7 +7,7 @@
 ; 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)
+ (deps extract.v ../theories/DecreaseChecker.vo ../theories/Lex.vo)
  (action
   (setenv OCAMLPATH ""
    (run coqc -q -Q ../theories "" extract.v))))
diff --git a/lib/extract.v b/lib/extract.v
index 5c8ff7c..3fee1f7 100644
--- a/lib/extract.v
+++ b/lib/extract.v
@@ -3,7 +3,8 @@
    Pattern.strictly_contains runs. Kept beside the library so the
    generated module lands where dune collects it. *)
 
-From Stdlib Require Import Extraction ExtrOcamlBasic.
+From Stdlib Require Import Extraction ExtrOcamlBasic ExtrOcamlNatInt.
 Require Import DecreaseChecker.
+Require Import Lex.
 
-Extraction "decrease_extracted.ml" contains term_eqb.
+Extraction "decrease_extracted.ml" contains term_eqb lex_ltb.
diff --git a/lib/pattern.mli b/lib/pattern.mli
index 5fc16c6..f79dce0 100644
--- a/lib/pattern.mli
+++ b/lib/pattern.mli
@@ -45,6 +45,17 @@ val strictly_contains : t -> sub:t -> bool
 
 val pp : Format.formatter -> t -> unit
 
+(** The verified checker's view of patterns. Admission projects
+    patterns through {!to_checker} and runs the containment and
+    lexicographic checkers extracted from Rocq; the conversion is
+    injective by leaf kind, and these two equalities are the
+    trusted seam. *)
+type checker_leaf
+
+val checker_leaf_equal : checker_leaf -> checker_leaf -> bool
+
+val to_checker : t -> (Label.t, checker_leaf) Decrease_extracted.term
+
 (** Substitutions bind variables to patterns. They only grow;
     unification never revokes a binding. *)
 module Subst : sig
diff --git a/lib/world.ml b/lib/world.ml
index 8ade9da..a053c2c 100644
--- a/lib/world.ml
+++ b/lib/world.ml
@@ -586,6 +586,27 @@ module Standalone = struct
               in
               match lex_measure calls candidates with
               | None -> Error (Non_total_component members)
+              | Some measure
+                when
+                  (* The search is an untrusted heuristic; the
+                     measure it found is validated call by call with
+                     the lexicographic checker extracted from Rocq,
+                     whose soundness and well-foundedness are
+                     proven. *)
+                  not
+                    (List.for_all
+                       (fun c ->
+                         let project bindings =
+                           List.map
+                             (fun label ->
+                               Pattern.to_checker (Label.Map.find label bindings))
+                             measure
+                         in
+                         Decrease_extracted.lex_ltb Label.equal
+                           Pattern.checker_leaf_equal (project c.args)
+                           (project c.head))
+                       calls) ->
+                  Error (Non_total_component members)
               | Some measure ->
                   Ok
                     (List.fold_left