From f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 22:03:21 -0300 Subject: admission runs the containment checker extracted from rocq --- test/test_vm.ml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'test') 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 -- cgit v1.2.3