lexicographic order proven well founded, checker extracted and verifying admission

1 files changed, 21 insertions, 0 deletions

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