From df096c5bf76a907d0fe25b547ab1bcb6419d48fa 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(cbv): drop a dead let binding without evaluating its
 value

The call-by-value normaliser evaluated the value of every let binding
before its body. A binding introduced by wp for a dead assignment (the
flags of an x86 instruction, a register accumulated across an unrolled
loop) had its value fully evaluated before being discarded; on 256-bit
vector code this took minutes where the rest of the goal takes seconds.
A binding none of whose variables occurs in the body is now dropped at
once, and a preliminary pass drops the dead bindings of the goal from
the inside out, so that a chain of bindings only feeding a dead one
disappears as well.
---
 src/ecCallbyValue.ml        | 27 ++++++++++++++++++++++++++-
 tests/reduction-dead-let.ec | 18 ++++++++++++++++--
 2 files changed, 42 insertions(+), 3 deletions(-)

diff --git a/src/ecCallbyValue.ml b/src/ecCallbyValue.ml
index 771b0e712..7697f06f4 100644
--- a/src/ecCallbyValue.ml
+++ b/src/ecCallbyValue.ml
@@ -240,6 +240,26 @@ let norm_stmt s c  = Subst.subst_stmt s c
 let norm_me   s me = Subst.subst_me s me
 let norm_e    s e  = Subst.subst_e s e
 
+(* -------------------------------------------------------------------- *)
+(* Let bindings whose variables are dead: `let p = e in b` is `b` when no
+   variable of `p` occurs in `b`, and the value `e` need not be looked at. *)
+let dead_binding (p : lpattern) (body : form) : bool =
+  let bound =
+    match p with
+    | LSymbol (x, _) -> [x]
+    | LTuple ids -> List.map fst ids
+    | LRecord (_, ids) -> List.filter_map fst ids in
+  List.for_all (fun x -> not (Mid.mem x body.f_fv)) bound
+
+(* Drop the dead bindings of a formula, bodies first, so that a chain of
+   bindings only used by a dead one disappears as well. *)
+let rec drop_dead_lets (f : form) : form =
+  match f.f_node with
+  | Flet (p, e1, e2) ->
+    let e2 = drop_dead_lets e2 in
+    if dead_binding p e2 then e2 else f_let p (drop_dead_lets e1) e2
+  | _ -> f_map (fun ty -> ty) drop_dead_lets f
+
 (* -------------------------------------------------------------------- *)
 let rec norm st s f =
 (* FIXME : I think substitution in type is wrong *)
@@ -529,6 +549,11 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
         let bs = List.map (norm st s) bs in
         app_red st (f_match (norm st s cf) bs ty) args
 
+  (* a binding whose variables do not occur in the body is dropped
+     without evaluating its value *)
+  | Flet (p, _, f2) when st.st_ri.zeta && dead_binding p f2 ->
+    cbv st s f2 args
+
   | Flet (p, f1, f2) ->
     let f1 = cbv_init st s f1 in
     begin match p, f1.f_node with
@@ -715,4 +740,4 @@ let norm_cbv (ri : reduction_info) hyps f =
       Subst.subst_id
       (List.rev (LDecl.tohyps hyps).h_local)
 
-  in norm st s f
+  in norm st s (if ri.zeta then drop_dead_lets f else f)
diff --git a/tests/reduction-dead-let.ec b/tests/reduction-dead-let.ec
index fed97fd7e..1b245c533 100644
--- a/tests/reduction-dead-let.ec
+++ b/tests/reduction-dead-let.ec
@@ -1,6 +1,6 @@
 (* 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. *)
+   without its value being reduced or evaluated: the value may be a stuck
+   term (an opaque operator applied to a variable) that is not a tuple. *)
 
 require import AllCore.
 
@@ -24,6 +24,20 @@ 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.
 
+(* the same, in the call-by-value normaliser *)
+lemma c1 (x : int) : (let (a, b) = f x in 0) = 0.
+proof. by cbv. qed.
+
+lemma c2 (x : int) : (let (a, b) = f x in (fun y => 0) a) = 0.
+proof. by cbv. qed.
+
+lemma c3 (x : int) :
+  (let a = g x in let (b, c) = f a in let d = g b in 0) = 0.
+proof. by cbv. 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.
+
+lemma l2 (x : int) : (let (a, b) = (g x, 1) in a + b) = g x + 1.
+proof. by cbv. qed.