From d90033c89c6119823412608f5337d48493b1d685 Mon Sep 17 00:00:00 2001
From: Xingyu Xie <namasikanam@gmail.com>
Date: Wed, 26 Aug 2026 17:08:31 +0200
Subject: [PATCH] fix(fixpoint): matchfix termination check must descend into
 all call arguments

`trans_matchfix`'s `check_body` (ecHiInductive.ml) verified that a recursive
call's argument in the decreasing position is a structural subterm, but then
returned without inspecting the call's OTHER arguments. A non-decreasing
recursive call hidden in a sibling argument therefore escaped the check, e.g.

    op f (n : t) (b : bool) : bool =
      with n = Z   => b
      with n = S k => f k (! (f n b)).

Here the outer `f k (...)` decreases on `k`, so the check accepted it and never
looked at the second argument `! (f n b)`, which recurses on the whole input
`n`. This definition satisfies `f (S Z) b = ! (f (S Z) b)`, i.e. `f x = not f x`,
which has no total-function solution -- the theory becomes inconsistent.

Descend into every argument of an accepted recursive call (`List.iter
check_body args`) so nested non-decreasing calls are also checked. Legitimate
recursion (including nested decreasing calls like `f k (f k b)`) is unaffected;
the standard library still builds.

Regression: tests/matchfix-termination.ec (the bad fixpoint must be rejected).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 src/ecHiInductive.ml          |  7 ++++++-
 tests/matchfix-termination.ec | 15 +++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 tests/matchfix-termination.ec

diff --git a/src/ecHiInductive.ml b/src/ecHiInductive.ml
index 4d59c0f29..0e94794de 100644
--- a/src/ecHiInductive.ml
+++ b/src/ecHiInductive.ml
@@ -466,7 +466,12 @@ let trans_matchfix
         match destr_app e with
         | ({ e_node = Elocal x }, args) when x = opname -> begin
           match List.nth_opt args pos with
-          | Some { e_node = Elocal a } when Sid.mem a pvars -> ()
+          | Some { e_node = Elocal a } when Sid.mem a pvars ->
+            (* The decreasing argument is a valid structural subterm, but the
+               OTHER arguments may themselves hide a non-decreasing recursive
+               call (e.g. `f k (! (f n b))` with n the whole input). Descend
+               into every argument so such calls are also checked. *)
+            List.iter check_body args
           | _ -> fxerror loc env TT.FXE_SynCheckFailure
           end
         | _ -> EcTypes.e_iter check_body e
diff --git a/tests/matchfix-termination.ec b/tests/matchfix-termination.ec
new file mode 100644
index 000000000..656e7873e
--- /dev/null
+++ b/tests/matchfix-termination.ec
@@ -0,0 +1,15 @@
+(* Regression for the matchfix termination-check hole.
+
+   `check_body` (ecHiInductive.ml) accepts a recursive call whose decreasing
+   argument is a valid structural subterm, but used to return without checking
+   the call's OTHER arguments -- so a non-decreasing recursive call hidden in a
+   sibling argument escaped. The op below defines `f (S Z) b = ! (f (S Z) b)`
+   (i.e. `f x = not (f x)`), which has no total-function solution and makes the
+   logic inconsistent. It MUST be rejected by the termination check. *)
+require import AllCore.
+
+type t = [ Z | S of t ].
+
+fail op f (n : t) (b : bool) : bool =
+  with n = Z   => b
+  with n = S k => f k (! (f n b)).