Point yul-semantics at the Mathlib-narrowed rev; 29 MB off yulc

SPEC.md

@@ -108,15 +108,15 @@ Concrete spec-level functions (outcome maps, canonicalisation, byte assembly).
 | `YulEvmCompiler.assemble` | [YulEvmCompiler/Instr.lean#L188](YulEvmCompiler/Instr.lean#L188) | `c1c9c0c9a1ad80c8` |
 | `YulEvmCompiler.assembleBytes` | [YulEvmCompiler/Instr.lean#L176](YulEvmCompiler/Instr.lean#L176) | `29d8e692638cce98` |
 | `YulEvmCompiler.assembleWithPayload` | [YulEvmCompiler/LowerDefs.lean#L143](YulEvmCompiler/LowerDefs.lean#L143) | `55ba5256c2c91c08` |
-| `YulEvmCompiler.conv` | [YulEvmCompiler/Value.lean#L23](YulEvmCompiler/Value.lean#L23) | `25e701af8a9ce7bb` |
-| `YulEvmCompiler.mkCode` | [YulEvmCompiler/Decode.lean#L21](YulEvmCompiler/Decode.lean#L21) | `edacb826e56f9571` |
+| `YulEvmCompiler.conv` | [YulEvmCompiler/Value.lean#L29](YulEvmCompiler/Value.lean#L29) | `25e701af8a9ce7bb` |
+| `YulEvmCompiler.mkCode` | [YulEvmCompiler/Decode.lean#L23](YulEvmCompiler/Decode.lean#L23) | `edacb826e56f9571` |
 | `YulEvmCompiler.natToBE` | [YulEvmCompiler/Instr.lean#L26](YulEvmCompiler/Instr.lean#L26) | `d47a19daef761803` |
-| `YulEvmCompiler.opTable` | [YulEvmCompiler/OpTable.lean#L19](YulEvmCompiler/OpTable.lean#L19) | `e1b0c299397baebd` |
-| `YulEvmCompiler.resolveForLayoutCases` | [YulEvmCompiler/ObjectResolve.lean#L74](YulEvmCompiler/ObjectResolve.lean#L74) | `a635c809600d2d8a` |
-| `YulEvmCompiler.resolveForLayoutExpr` | [YulEvmCompiler/ObjectResolve.lean#L22](YulEvmCompiler/ObjectResolve.lean#L22) | `15bc9ca915a17f5a` |
-| `YulEvmCompiler.resolveForLayoutExprs` | [YulEvmCompiler/ObjectResolve.lean#L35](YulEvmCompiler/ObjectResolve.lean#L35) | `deee862dd8d61de4` |
-| `YulEvmCompiler.resolveForLayoutStmt` | [YulEvmCompiler/ObjectResolve.lean#L42](YulEvmCompiler/ObjectResolve.lean#L42) | `ef48ed8902b73d01` |
-| `YulEvmCompiler.resolveForLayoutStmts` | [YulEvmCompiler/ObjectResolve.lean#L68](YulEvmCompiler/ObjectResolve.lean#L68) | `e61eedc003fbb530` |
+| `YulEvmCompiler.opTable` | [YulEvmCompiler/OpTable.lean#L19](YulEvmCompiler/OpTable.lean#L19) | `58d5b129f84835ed` |
+| `YulEvmCompiler.resolveForLayoutCases` | [YulEvmCompiler/ObjectResolve.lean#L77](YulEvmCompiler/ObjectResolve.lean#L77) | `a635c809600d2d8a` |
+| `YulEvmCompiler.resolveForLayoutExpr` | [YulEvmCompiler/ObjectResolve.lean#L25](YulEvmCompiler/ObjectResolve.lean#L25) | `15bc9ca915a17f5a` |
+| `YulEvmCompiler.resolveForLayoutExprs` | [YulEvmCompiler/ObjectResolve.lean#L38](YulEvmCompiler/ObjectResolve.lean#L38) | `deee862dd8d61de4` |
+| `YulEvmCompiler.resolveForLayoutStmt` | [YulEvmCompiler/ObjectResolve.lean#L45](YulEvmCompiler/ObjectResolve.lean#L45) | `ef48ed8902b73d01` |
+| `YulEvmCompiler.resolveForLayoutStmts` | [YulEvmCompiler/ObjectResolve.lean#L71](YulEvmCompiler/ObjectResolve.lean#L71) | `e61eedc003fbb530` |
 | `YulEvmCompiler.resultOf` | [YulEvmCompiler/StateRel.lean#L1264](YulEvmCompiler/StateRel.lean#L1264) | `9a4fae748007bd7b` |
 | `YulParser.afterBlockComment` | [YulParser/Tokens.lean#L30](YulParser/Tokens.lean#L30) | `5deac78dd9073c67` |
 | `YulParser.canon` | [YulParser/Canon.lean#L82](YulParser/Canon.lean#L82) | `b2d8eb356dc83a9c` |

SpecClosure.lean

@@ -550,7 +550,7 @@ SPEC CLOSURE — audited this-repo surface (89 decls)
   datadef YulEvmCompiler.conv 25e701af8a9ce7bb
   datadef YulEvmCompiler.mkCode edacb826e56f9571
   datadef YulEvmCompiler.natToBE d47a19daef761803
-  datadef YulEvmCompiler.opTable e1b0c299397baebd
+  datadef YulEvmCompiler.opTable 58d5b129f84835ed
   datadef YulEvmCompiler.resolveForLayoutCases a635c809600d2d8a
   datadef YulEvmCompiler.resolveForLayoutExpr 15bc9ca915a17f5a
   datadef YulEvmCompiler.resolveForLayoutExprs deee862dd8d61de4

YulEvmCompiler/Asm.lean

@@ -1,3 +1,5 @@
+import Mathlib.Tactic.NormNum.Ineq
+import Mathlib.Tactic.NormNum.Basic
 import YulEvmCompiler.OpTable
 set_option warningAsError true
 /-!

YulEvmCompiler/Decode.lean

@@ -1,3 +1,5 @@
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.IntervalCases
 import YulEvmCompiler.OpTable
 import Batteries.Data.ByteArray
 set_option warningAsError true

YulEvmCompiler/ObjectResolve.lean

@@ -1,3 +1,6 @@
+import Mathlib.Data.Nat.SuccPred
+import Mathlib.Tactic.ByContra
+import Mathlib.Tactic.Push
 import YulSemantics.Determinism
 import YulSemantics.ObjectRun
 set_option warningAsError true
@@ -63,7 +66,7 @@ mutual
     | .«continue» => .«continue»
     | .leave => .leave
     termination_by statement => 2 * sizeOf statement + 1
-    decreasing_by all_goals simp_wf <;> omega
+    decreasing_by all_goals simp_wf; omega
 
   def resolveForLayoutStmts (L : Layout) : List (Stmt Op) → List (Stmt Op)
     | [] => []

YulEvmCompiler/Optimizer/Implementation/CoalesceCopies.lean

@@ -307,7 +307,8 @@ theorem ccPairs_bwd : ∀ (ss : List (Stmt Op)) {funs : FunEnv D} {V : VEnv D}
             have hlet_y' : ∀ st2 : EvmState, Step D funs ((x', v) :: V) st2
                 (.stmt (.letDecl [y] (some (.var x'))))
                 (.sres ((y, v) :: (x', v) :: V) st2 .normal) := fun st2 =>
-              Step.letVal (vars := [y]) (Step.var (by simp [VEnv.get])) rfl
+              Step.letVal («D» := D) (vars := [y])
+                (Step.var (by simp [VEnv.get])) rfl
             rcases hshape with ⟨rfl, rfl, rfl⟩ | ⟨e, rfl, he⟩
             · exact ⟨V₁, Step.seqCons Step.letZero
                 (Step.seqCons (hlet_y' _) hstep₂),

YulEvmCompiler/Optimizer/Implementation/DeadLits.lean

@@ -146,7 +146,7 @@ theorem let_lit_run {x : Ident} {val : Option (Expr Op)} (funs : FunEnv D)
     ∃ v, Step D funs V st (.stmt (.letDecl [x] val)) (.sres ((x, v) :: V) st .normal) := by
   rcases hval with rfl | ⟨l, rfl⟩
   · exact ⟨_, Step.letZero⟩
-  · exact ⟨_, Step.letVal Step.lit rfl⟩
+  · exact ⟨_, Step.letVal («D» := D) Step.lit rfl⟩
 
 /-- Dropping a `letDecl` never changes the hoisted function scope. -/
 theorem hoist_drop_let (pre rest : List (Stmt Op)) (x : Ident) (val : Option (Expr Op)) :

YulEvmCompiler/Optimizer/Implementation/DeadPure.lean

@@ -630,7 +630,7 @@ theorem DrFrame.set {base V : VEnv D} {owned : List Ident}
   have hxA : x ∈ A.map Prod.fst := by simpa [hkeys] using hx
   refine ⟨VEnv.set A x v, ?_, ?_⟩
   · exact VEnv.set_append_mem hxA base v
-  · rw [VEnv.set_keys, hkeys]
+  · rw [VEnv.set_keys («D» := D), hkeys]
 
 mutual
 
@@ -801,7 +801,7 @@ theorem discardStmt_run {sink : Ident} {ctx ctx' : DrCtx} {s : Stmt Op}
               · have h := Step.assignVal (vars := [x]) he rfl
                 rwa [VEnv.setMany_singleton] at h
               · intro z hz
-                rw [VEnv.set_keys]
+                rw [VEnv.set_keys («D» := D)]
                 exact hb z hz
   | cond _ _ => simp [discardStmt] at hcheck
   | switch _ _ _ => simp [discardStmt] at hcheck
@@ -931,7 +931,7 @@ theorem discardStmt_inv {sink : Ident} {ctx ctx' : DrCtx} {s : Stmt Op}
                   rw [VEnv.setMany_singleton]
                   refine ⟨rfl, rfl, hframe.set hx v, ?_⟩
                   intro z hz
-                  rw [VEnv.set_keys]
+                  rw [VEnv.set_keys («D» := D)]
                   exact hb z hz
               | assignHalt he =>
                   obtain ⟨v, hv⟩ := dcEvalInv rhs hae he
@@ -2436,7 +2436,7 @@ theorem dc_fwd {funs₁ : FunEnv D} {V₁ : VEnv D} {st : EvmState}
           refine ⟨_, Step.assignVal hstepe hlen, VEnv.setMany V₂ vars vals,
             rfl, MIns.setMany vals hins hdisj, fun _ => ?_⟩
           intro y hy
-          rw [VEnv.setMany_keys]
+          rw [VEnv.setMany_keys («D» := D)]
           exact hb y hy
   | @assignHalt funs V st vars e st1 he ihe =>
       intro funs₂ V₂ ins bound bound' pc' hR hrel hins hfree hb
@@ -3223,7 +3223,7 @@ theorem dc_bwd {funs₂ : FunEnv D} {V₂ : VEnv D} {st : EvmState}
           refine ⟨_, Step.assignVal hstepe hlen, VEnv.setMany V₁ vars vals,
             rfl, MIns.setMany vals hins hdisj, fun _ => ?_⟩
           intro y hy
-          rw [VEnv.setMany_keys]
+          rw [VEnv.setMany_keys («D» := D)]
           exact hb y hy
   | @assignHalt funs V st vars e st1 he ihe =>
       intro funs₁ V₁ ins bound bound' pc hR hrel hins hfree hb

YulEvmCompiler/Optimizer/Implementation/DeadPureResolve.lean

@@ -121,7 +121,7 @@ theorem discardStmt_resolve (L : Layout) {sink : Ident} : ∀
   | _, .continue, _, h => by simp [discardStmt] at h
   | _, .leave, _, h => by simp [discardStmt] at h
   termination_by _ s _ _ => 2 * sizeOf s + 1
-  decreasing_by all_goals simp_wf
+  decreasing_by all_goals simp_wf; omega
 
 theorem discardStmts_resolve (L : Layout) {sink : Ident} : ∀
     (ctx : DrCtx) (ss : Block Op) (ctx' : DrCtx),

YulEvmCompiler/Optimizer/Implementation/FlattenSound.lean

@@ -211,7 +211,7 @@ theorem find_isSome_set {x y : Ident} {C : VEnv D}
     (hx : (C.find? (fun p => p.1 = x)).isSome)
     (v : (evmWithExternal calls creates).Value) :
     ((VEnv.set C y v).find? (fun p => p.1 = x)).isSome := by
-  rw [find_key_isSome_iff, VEnv.set_keys]
+  rw [find_key_isSome_iff, VEnv.set_keys («D» := D)]
   exact find_key_isSome_iff.mp hx
 
 /-- Renaming commutes with an update to `x`/`x'` (the segment never binds
@@ -348,7 +348,7 @@ theorem RnRel.set_ren {x x' : Ident} {n : Nat} {V₁ V₂ : VEnv D}
             rw [set_append_of_none hC v,
               set_append_of_none (by rw [renKeys_find_other hyx hyx']; exact hC) v]
             exact RnRel.mk C (VEnv.set base y v) hx hx'
-              (by rw [VEnv.set_length]; exact hn)
+              (by rw [VEnv.set_length («D» := D)]; exact hn)
 
 /-- Source `setMany` matches target `setMany` on the renamed targets. -/
 theorem RnRel.setMany_ren {x x' : Ident} {n : Nat} :
@@ -722,7 +722,7 @@ theorem Step.rn_congr {x x' : Ident} {n : Nat}
         exact hm.1 hy
       refine ⟨_, ?_, .sres _ _ (hR.pushMany (ps := bindZeros _ vars) ?_)⟩
       · have hmap : vars.map (renVar x x') = vars := map_renVar_id hxv
-        show Step _ _ _ _ (.stmt (.letDecl (vars.map (renVar x x')) none)) _
+        show Step D _ _ _ (.stmt (.letDecl (vars.map (renVar x x')) none)) _
         rw [hmap]
         exact Step.letZero
       · intro p hp

YulEvmCompiler/Optimizer/Implementation/FreshenCalls.lean

@@ -428,19 +428,19 @@ private theorem fcStmt_equiv (P : String) (Δ : DEnv) :
   | .cond c body =>
       by
         simpa [fcStmt, fcBlock] using
-          (EquivStmt.cond_congr (EquivExpr.refl c)
+          (EquivStmt.cond_congr (EquivExpr.refl («D» := D) c)
             (EquivBlock.of_stmts_funs
               (EquivStmts.of_forall₂ (fcStmts_forall2 P (deltaExtend Δ body) body))
               (fcScopeRel P (deltaExtend Δ body) body)))
   | .switch c cases dflt =>
       by
         simpa [fcStmt] using
-          (EquivStmt.switch_congr (EquivExpr.refl c)
+          (EquivStmt.switch_congr (EquivExpr.refl («D» := D) c)
             (fcCases_forall2 P Δ cases) (fcDflt_equiv P Δ dflt))
   | .forLoop init c post body => by
       let ΔL := Δ.filter (fun p => !(definedFuns init).contains p.1)
       simpa [fcStmt, fcBlock, ΔL] using
-        (EquivStmt.forLoop_congr init (EquivExpr.refl c)
+        (EquivStmt.forLoop_congr init (EquivExpr.refl («D» := D) c)
           (EquivBlock.of_stmts_funs
             (EquivStmts.of_forall₂ (fcStmts_forall2 P (deltaExtend ΔL post) post))
             (fcScopeRel P (deltaExtend ΔL post) post))

YulEvmCompiler/Optimizer/Implementation/FreshenCallsResolve.lean

@@ -99,7 +99,7 @@ private theorem resolveFcStmt_equiv (L : Layout) (P : String) (Δ : DEnv) :
       rw [fcStmt, resolveForLayoutStmt_forLoop, resolveForLayoutStmt_forLoop]
       simpa [fcBlock, ΔL] using
         (EquivStmt.forLoop_congr (resolveForLayoutStmts L init)
-          (EquivExpr.refl (resolveForLayoutExpr L c))
+          (EquivExpr.refl («D» := D) (resolveForLayoutExpr L c))
           (EquivBlock.of_stmts_funs
             (EquivStmts.of_forall₂
               (resolveFcStmts_forall2 L P (deltaExtend ΔL post) post))

YulEvmCompiler/Optimizer/Implementation/FuseDeclAssignSound.lean

@@ -182,7 +182,7 @@ theorem MvRel.set {x : Ident} {dA dB : Nat} {V₁ V₂ : VEnv D}
                       rw [if_neg (fun hc : x = y => hxy hc.symm)],
                   set_append_of_found (by simp [hA']) w]
                 refine MvRel.mk C (VEnv.set A y w) B v ?_
-                  (by rw [VEnv.set_length]; exact hdA) hdB
+                  (by rw [VEnv.set_length («D» := D)]; exact hdA) hdB
                 intro p hp
                 obtain ⟨q', hq', hqe⟩ := mem_set_key hp
                 rw [← hqe]
@@ -199,7 +199,7 @@ theorem MvRel.set {x : Ident} {dA dB : Nat} {V₁ V₂ : VEnv D}
                       simp only [VEnv.set]
                       rw [if_neg (fun hc : x = y => hxy hc.symm)]]
                 exact MvRel.mk C A (VEnv.set B y w) v hA hdA
-                  (by rw [VEnv.set_length]; exact hdB)
+                  (by rw [VEnv.set_length («D» := D)]; exact hdB)
 
 /-- `setMany` preserves the relation. -/
 theorem MvRel.setMany {x : Ident} {dA dB : Nat} {V₁ V₂ : VEnv D}
@@ -797,7 +797,7 @@ theorem step_new_keys_free {x : Ident} {funs : FunEnv D} {V : VEnv D}
   | assignVal =>
       intro V' st' o heq _
       injection heq with h1 _ _; subst h1
-      exact ⟨[], by rw [VEnv.setMany_keys]; rfl, by simp⟩
+      exact ⟨[], by rw [VEnv.setMany_keys («D» := D)]; rfl, by simp⟩
   | assignHalt =>
       intro V' st' o heq _
       injection heq with h1 _ _; subst h1
@@ -1501,7 +1501,7 @@ theorem fuse_site_bwd {funs : FunEnv D} {V : VEnv D} {st : EvmState}
     ⟨[], V, rfl, rfl, rfl⟩
   have hlet1 : ∀ st2, Step D funs V st2 (.stmt (.letDecl [x] (some (.lit l))))
       (.sres ((x, (evmWithExternal calls creates).litValue l) :: V) st2 .normal) :=
-    fun st2 => by simpa using Step.letVal (vars := [x]) Step.lit (by simp)
+    fun st2 => by simpa using Step.letVal («D» := D) (vars := [x]) Step.lit (by simp)
   cases h with
   | seqStop hlet hne =>
       rcases letSome_inv hlet with ⟨val, hev, rfl, hno⟩ | ⟨hev, rfl, rfl⟩

YulEvmCompiler/Optimizer/Implementation/HoistCalls.lean

@@ -161,7 +161,7 @@ theorem hoistUnaryCore_equiv_of (P : String) (xs : List Ident) (f g : Ident)
                           | var hv =>
                           have hvv : v = vOuter := by simpa [VEnv.get] using hv
                           subst vOuter
-                          have hargs0 := Step.argsCons Step.argsNil hinner0
+                          have hargs0 := Step.argsCons Step.argsNil («D» := D) hinner0
                           have hcall0 := Step.callOk hargs0
                             (by simpa [lookupFun] using hl) harity hbody hout
                           have hassign0 := Step.assignVal hcall0 hxs
@@ -195,7 +195,7 @@ theorem hoistUnaryCore_equiv_of (P : String) (xs : List Ident) (f g : Ident)
                           | var hv =>
                           have hvv : v = vOuter := by simpa [VEnv.get] using hv
                           subst vOuter
-                          have hargs0 := Step.argsCons Step.argsNil hinner0
+                          have hargs0 := Step.argsCons Step.argsNil («D» := D) hinner0
                           have hcall0 := Step.callHalt hargs0
                             (by simpa [lookupFun] using hl) harity hbody
                           simpa [restore] using
@@ -293,18 +293,18 @@ private theorem hcStmt_equiv (P : String) (Δ : DEnv) :
       · exact EquivStmt.refl _
   | .cond c body => by
       simpa [hcStmt, hcBlock] using
-        (EquivStmt.cond_congr (EquivExpr.refl c)
+        (EquivStmt.cond_congr (EquivExpr.refl («D» := D) c)
           (EquivBlock.of_stmts_funs
             (EquivStmts.of_forall₂ (hcStmts_forall2 P (deltaExtend Δ body) body))
             (hcScopeRel P (deltaExtend Δ body) body)))
   | .switch c cases dflt => by
       simpa [hcStmt] using
-        (EquivStmt.switch_congr (EquivExpr.refl c)
+        (EquivStmt.switch_congr (EquivExpr.refl («D» := D) c)
           (hcCases_forall2 P Δ cases) (hcDflt_equiv P Δ dflt))
   | .forLoop init c post body => by
       let ΔL := Δ.filter (fun p => !(definedFuns init).contains p.1)
       simpa [hcStmt, hcBlock, ΔL] using
-        (EquivStmt.forLoop_congr init (EquivExpr.refl c)
+        (EquivStmt.forLoop_congr init (EquivExpr.refl («D» := D) c)
           (EquivBlock.of_stmts_funs
             (EquivStmts.of_forall₂ (hcStmts_forall2 P (deltaExtend ΔL post) post))
             (hcScopeRel P (deltaExtend ΔL post) post))

YulEvmCompiler/Optimizer/Implementation/HoistCallsResolve.lean

@@ -74,7 +74,7 @@ private theorem resolveHcStmt_equiv (L : Layout) (P : String) (Δ : DEnv) :
       rw [hcStmt, resolveForLayoutStmt_forLoop, resolveForLayoutStmt_forLoop]
       simpa [hcBlock, ΔL] using
         (EquivStmt.forLoop_congr (resolveForLayoutStmts L init)
-          (EquivExpr.refl (resolveForLayoutExpr L c))
+          (EquivExpr.refl («D» := D) (resolveForLayoutExpr L c))
           (EquivBlock.of_stmts_funs
             (EquivStmts.of_forall₂
               (resolveHcStmts_forall2 L P (deltaExtend ΔL post) post))

YulEvmCompiler/Optimizer/Implementation/InlineCallsSound.lean

@@ -105,7 +105,7 @@ theorem VEnv.setMany_append_mem {A W : VEnv D} {xs : List Ident} {vs : List U256
           simp only [List.zip_cons_cons, List.foldl_cons]
           rw [VEnv.set_append_mem (h x (by simp)) W v]
           exact ih (fun y hy => by
-            rw [VEnv.set_keys]
+            rw [VEnv.set_keys («D» := D)]
             exact h y (List.mem_cons_of_mem _ hy))
 
 /-- `restore` distributes over a common extension. -/
@@ -422,7 +422,7 @@ theorem scoped_transfer {funs₁ : FunEnv D} {V₁ : VEnv D} {st : EvmState}
           have hpost : postBound bound (Code.stmt (.assign vars e)) = bound := by
             simp [postBound, scopedStmt, hsc'.1, hsc'.2]
           rw [hpost] at hx
-          rw [VEnv.setMany_keys]
+          rw [VEnv.setMany_keys («D» := D)]
           exact hb x hx
   | @assignHalt funs V st vars e st1 he ihe =>
       intro A W bound funs₂ W' hV hsc hb
@@ -843,7 +843,7 @@ theorem argLets_fwd {rs : List Ident} :
       cases ps with
       | nil =>
           cases h with
-          | argsNil => simpa using Step.seqNil
+          | argsNil => simpa using Step.seqNil («D» := D)
       | cons p ps' => simp at hlen
   | cons a as' ih =>
       intro argvals funs V st st1 h hlen hnc hsh N hN funs₂
@@ -975,7 +975,7 @@ theorem assigns_fwd {A' : VEnv D} :
   | nil =>
       intro rs hr hx hlen funs Wb st
       cases rs with
-      | nil => simpa [VEnv.setMany] using Step.seqNil
+      | nil => simpa [VEnv.setMany] using Step.seqNil («D» := D)
       | cons r rs' => simp at hlen
   | cons x xs' ih =>
       intro rs hr hx hlen funs Wb st

YulEvmCompiler/Optimizer/Implementation/InlineHelpers.lean

@@ -297,14 +297,14 @@ def inlineHelpersStmt (litOK : Bool) (static : FunEnv D) : Stmt Op → Stmt Op
   | .continue => .continue
   | .leave => .leave
   termination_by statement => 2 * sizeOf statement + 1
-  decreasing_by all_goals simp_wf <;> omega
+  decreasing_by all_goals simp_wf; omega
 
 /-- Rewrite a statement sequence under an already-established scope stack. -/
 def inlineHelpersStmts (litOK : Bool) (static : FunEnv D) : Block Op → Block Op
   | [] => []
   | s :: rest => inlineHelpersStmt litOK static s :: inlineHelpersStmts litOK static rest
   termination_by statements => 2 * sizeOf statements
-  decreasing_by all_goals simp_wf <;> omega
+  decreasing_by all_goals simp_wf; omega
 
 /-- Rewrite switch cases, each of whose body is a block. -/
 def inlineHelpersCases (litOK : Bool) (static : FunEnv D) :
@@ -314,7 +314,7 @@ def inlineHelpersCases (litOK : Bool) (static : FunEnv D) :
       (l, inlineHelpersStmts litOK (hoist D body :: static) body) ::
         inlineHelpersCases litOK static rest
   termination_by cases => 2 * sizeOf cases
-  decreasing_by all_goals simp_wf <;> omega
+  decreasing_by all_goals simp_wf; omega
 
 end
 
@@ -746,7 +746,8 @@ theorem identity_call_value {funs cenv : FunEnv D} {V st st' fn e}
          body := [.assign [ret] (.var param)] }, cenv)) :
     Step D funs V st (.expr (.call fn [e])) (.eres (.vals [v] st')) := by
   obtain ⟨Vend, hbody, hret⟩ := identity_body_value cenv param ret v st'
-  have hc := Step.callOk (Step.argsCons Step.argsNil he) hl (by simp) hbody (Or.inl rfl)
+  have hc := Step.callOk («D» := D)
+    (Step.argsCons Step.argsNil he) hl (by simp) hbody (Or.inl rfl)
   simpa [hret] using hc
 
 theorem identity_call_halt {funs : FunEnv D} {V st st' fn e}

YulEvmCompiler/Optimizer/Implementation/Pipeline.lean

@@ -85,9 +85,9 @@ theorem RPass.resolve_equiv_ofList (ps : List (RPass calls creates))
     (L : Layout) (b : Block Op) :
     EquivBlock D
       (resolveForLayoutStmts L b)
-      (resolveForLayoutStmts L ((LocalPass.ofList (ps.map (·.pass))).run b)) := by
+      (resolveForLayoutStmts L ((LocalPass.ofList («D» := D) (ps.map (·.pass))).run b)) := by
   induction ps generalizing b with
-  | nil => exact EquivBlock.refl _
+  | nil => exact EquivBlock.refl («D» := D) _
   | cons p rest ih =>
       exact (p.resolve_equiv L b).trans (ih (p.pass.run b))