From d6ea09d2be9864c8f970a73f7fff1176193ecd47 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 11 May 2026 11:12:00 +0200 Subject: [PATCH 1/2] restrict lazy WHNF to reducible --- src/Lean/Meta/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 9d7201e1630e..af523d6aef0d 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -2111,7 +2111,7 @@ def whnfI (e : Expr) : MetaM Expr := /-- `whnf` with at most instances transparency. -/ def whnfAtMostI (e : Expr) : MetaM Expr := do match (← getTransparency) with - | .all | .default => withTransparency TransparencyMode.instances <| whnf e + | .all | .default => withTransparency TransparencyMode.reducible <| whnf e | _ => whnf e /-- From 63f5f11e848cf541e09f4d762ab5b7819e366d2b Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 11 May 2026 14:16:59 +0200 Subject: [PATCH 2/2] completely disable lazy whnf, fix problems in the BVDecide library --- src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 2 +- .../Bitblast/BVExpr/Circuit/Impl/Expr.lean | 24 ++++++++++++++----- .../BVExpr/Circuit/Impl/Operations/Add.lean | 5 ++++ .../Bitblast/BVExpr/Circuit/Impl/Pred.lean | 4 +++- 5 files changed, 28 insertions(+), 9 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index af523d6aef0d..9d7201e1630e 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -2111,7 +2111,7 @@ def whnfI (e : Expr) : MetaM Expr := /-- `whnf` with at most instances transparency. -/ def whnfAtMostI (e : Expr) : MetaM Expr := do match (← getTransparency) with - | .all | .default => withTransparency TransparencyMode.reducible <| whnf e + | .all | .default => withTransparency TransparencyMode.instances <| whnf e | _ => whnf e /-- diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 43bf97a60cb1..fa9ad77d6e9e 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -17,7 +17,7 @@ register_builtin_option backward.isDefEq.lazyProjDelta : Bool := { } register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := { - defValue := true + defValue := false descr := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used" } diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean index b5a96db49450..3c96d5aa26e3 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean @@ -205,21 +205,27 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateLeft) dsimp only at heaig assumption - ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateLeft) ..)⟩ + ⟨⟨res, this⟩, cache.cast (by + simp only [res] + exact AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateLeft) ..)⟩ | .rotateRight distance => let res := bitblast.blastRotateRight eaig ⟨evec, distance⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateRight) dsimp only at heaig assumption - ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateRight) ..)⟩ + ⟨⟨res, this⟩, cache.cast (by + simp only [res] + exact AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateRight) ..)⟩ | .arithShiftRightConst distance => let res := bitblast.blastArithShiftRightConst eaig ⟨evec, distance⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastArithShiftRightConst) dsimp only at heaig assumption - ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩ + ⟨⟨res, this⟩, cache.cast (by + simp only [res] + exact AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩ | .reverse => let res := bitblast.blastReverse eaig evec have := by @@ -250,7 +256,9 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastAppend) dsimp only at hlaig hraig omega - ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastAppend) ..)⟩ + ⟨⟨res, this⟩, cache.cast (by + simp only [res] + exact AIG.LawfulVecOperator.le_size (f := bitblast.blastAppend) ..)⟩ | .replicate n expr h => let ⟨⟨⟨aig, expr⟩, haig⟩, cache⟩ := goCache aig expr cache let res := bitblast.blastReplicate aig ⟨n, expr, h⟩ @@ -258,7 +266,9 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastReplicate) dsimp only at haig assumption - ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastReplicate) ..)⟩ + ⟨⟨res, this⟩, cache.cast (by + simp only [res] + exact AIG.LawfulVecOperator.le_size (f := bitblast.blastReplicate) ..)⟩ | .extract start len expr => let ⟨⟨⟨eaig, evec⟩, heaig⟩, cache⟩ := goCache aig expr cache let res := bitblast.blastExtract eaig ⟨evec, start⟩ @@ -266,7 +276,9 @@ where apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastExtract) dsimp only at heaig exact heaig - ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastExtract) ..)⟩ + ⟨⟨res, this⟩, cache.cast (by + simp only [res] + exact AIG.LawfulVecOperator.le_size (f := bitblast.blastExtract) ..)⟩ | .shiftLeft lhs rhs => let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean index fb5e48ff543d..29d0f4ea6b11 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean @@ -227,6 +227,11 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R apply AIG.LawfulOperator.lt_size_of_lt_aig_size exact h1 have h4 : idx < (mkFullAdder aig { lhs := lhs.get curr h, rhs := rhs.get curr h, cin := cin }).aig.decls.size := by + /- + Without the unfolding of `mkFullAdder`, `apply` will pick the wrong `f`, and simply adding + `(f := mkFullAdderCarry)` runs into the heartbeat limit. + -/ + simp only [mkFullAdder] apply AIG.LawfulOperator.lt_size_of_lt_aig_size exact h3 rw [go_decl_eq (w := w) (curr := curr + 1) (h1 := h4)] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean index 94d51d73ad1e..769fd2e26423 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean @@ -51,7 +51,9 @@ def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return ai apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt) dsimp only at hlhs hrhs omega - ⟨⟨res, this⟩, cache⟩ + ⟨⟨res, this⟩, by + simp only + exact cache⟩ | .getLsbD expr idx => /- Note: This blasts the entire expression up to `w` despite only needing it up to `idx`.