From 66394a13db53b8637c5138eeb05658d0e0c1e8b1 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Mon, 26 Oct 2026 09:21:10 +0100
Subject: [PATCH] perf(reduction): drop a dead let binding without reducing its
 value

The iota rule for a let-tuple required the bound value to be a syntactic
tuple and otherwise asked for the reduction of the value, even when none
of the bound variables occurs in the body; a dead let introduced by wp
for a tuple assignment (the flags of an x86 instruction) was then fully
evaluated before being thrown away. The zeta, let-tuple and let-record
rules now return the body at once when the binding is dead.
---
 src/ecReduction.ml          |  8 +++++++-
 tests/reduction-dead-let.ec | 29 +++++++++++++++++++++++++++++
 2 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 tests/reduction-dead-let.ec

diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index 7b967e263..d8d913a74 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -1006,11 +1006,14 @@ let reduce_head simplify ri env hyps f =
 
     (* ζ-reduction *)
   | Flet (LSymbol(x,_), e1, e2) when ri.zeta ->
+      if not (Mid.mem x e2.f_fv) then e2 else
       let s = Fsubst.f_bind_local Fsubst.f_subst_id x e1 in
       Fsubst.f_subst s e2
 
-    (* ι-reduction (let-tuple) *)
+    (* ι-reduction (let-tuple): a binding whose variables do not occur in
+       the body is dropped without reducing its value *)
   | Flet (LTuple ids, e1, e2) when ri.iota ->
+    if List.for_all (fun (x, _) -> not (Mid.mem x e2.f_fv)) ids then e2 else
     if is_tuple e1 then
       let es = destr_tuple e1 in
       let s =
@@ -1023,6 +1026,9 @@ let reduce_head simplify ri env hyps f =
 
     (* ι-reduction (let-records) *)
   | Flet (LRecord (_, ids), f1, f2) when ri.iota ->
+    if List.for_all (fun (x, _) ->
+         match x with None -> true | Some x -> not (Mid.mem x f2.f_fv)) ids
+    then f2 else
     if is_record env f1 then
       let args  = snd (EcFol.destr_app f1) in
       let subst =
diff --git a/tests/reduction-dead-let.ec b/tests/reduction-dead-let.ec
new file mode 100644
index 000000000..fed97fd7e
--- /dev/null
+++ b/tests/reduction-dead-let.ec
@@ -0,0 +1,29 @@
+(* A let binding none of whose variables occurs in the body is dropped
+   without its value being reduced: the value may be a stuck term (an
+   opaque operator applied to a variable) that is not a tuple. *)
+
+require import AllCore.
+
+op f : int -> int * int.
+op g : int -> int.
+
+(* head reduction: let-tuple on a value that is not a tuple *)
+lemma t1 (x : int) : (let (a, b) = f x in 0) = 0.
+proof. by move=> /=. qed.
+
+(* head reduction: let-symbol *)
+lemma t2 (x : int) : (let a = g x in 0) = 0.
+proof. by move=> /=. qed.
+
+(* the binding dies once the body is reduced *)
+lemma t3 (x : int) : (let (a, b) = f x in (fun y => 0) a) = 0.
+proof. by move=> /=. qed.
+
+(* a chain of bindings only feeding a dead one *)
+lemma t4 (x : int) :
+  (let a = g x in let (b, c) = f a in let d = g b in 0) = 0.
+proof. by move=> /=. qed.
+
+(* a live binding is still substituted *)
+lemma l1 (x : int) : (let (a, b) = (g x, 1) in a + b) = g x + 1.
+proof. by move=> /=. qed.