From ba36ae8ae4d0792cdad58ff7e219e19682bcc876 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 29 Jul 2026 20:24:04 +0200 Subject: [PATCH 1/2] Point yul-semantics at the Mathlib-narrowed rev; 29 MB off `yulc` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A Lean module's `initialize_M` calls the initializer of every module `M` imports. That is a real symbol reference, so a bare `import Mathlib` anywhere in the runtime closure links all of compiled Mathlib into `yulc` and `libyulc` (and hence into any solc statically linked against `libyulc`). `canon-narrow-mathlib-import` removed this repo's only bare `import Mathlib` and measured no effect, because the pinned `yul-semantics` had two of its own — `YulSemantics/Dialect/EVM.lean` (which most of `YulEvmCompiler` imports) and `YulSemantics/Basic.lean`. Both are now narrowed upstream; this commit points `rev` at that work and fixes the downstream cascade. Measured on `.lake/build/bin/yulc`, ordinary runnable link, no `--unresolved-symbols` games: before 165,277,392 bytes 8,724 objects in yulc.rsp after 134,841,520 bytes 1,112 objects in yulc.rsp delta -30,435,872 bytes (-29.0 MiB, -18.4%) The `.c.o.export` input to the link is 19.7 MB after. The resulting binary was run: it compiles a small Yul object to the same bytecode as the baseline binary. ## Downstream cascade Modules that were getting Mathlib transitively through `YulSemantics.Dialect.EVM` now import what they use: * `YulEvmCompiler/Value.lean` — `Mathlib.Data.BitVec` (`BitVec.toNat_injective`), `Mathlib.Algebra.Divisibility.Basic` (`Dvd.dvd.mul_left`), `Mathlib.Algebra.Order.GroupWithZero.Basic` (`pow_lt_pow_right₀`), and the `ring` / `positivity` / `norm_num` tactics. * `YulEvmCompiler/Optimizer/Implementation/Simplify.lean` — `Mathlib.Data.BitVec`, `Batteries.Data.BitVec.Lemmas` (`BitVec.toNat_pow`, `BitVec.ofNat_pow`), and the monoid `pow` lemmas. * `YulEvmCompiler/Decode.lean` — `fin_cases`, `interval_cases`. * `YulEvmCompiler/Asm.lean` — `norm_num` (`.Basic` + `.Ineq`). * `YulEvmCompiler/ObjectResolve.lean` — `by_contra`, `push`, and `Mathlib.Data.Nat.SuccPred` for `simp_wf`, exactly as `YulParser/Canon.lean` needed on the parent commit. * `YulIR/FrameCongr.lean` — `Batteries.Data.List.Basic` (`List.Forall₂`); no Mathlib needed. ## Explicit dialect annotations (72 sites, no proof content changed) `Step`, `EquivExpr`, `VEnv.set_keys` and friends take `[DecidableEq D.Value]`, and these terms are elaborated before the expected type fixes `D`. With Mathlib in scope, `DecidableEq (Dialect.Value ?D)` was *inconclusive* rather than failing — `LinearOrder.toDecidableEq` and the long chain below it leave the search stuck on metavariables — so Lean postponed it until `?D` was known. Without Mathlib there are no candidate instances at all, so it is a hard failure. The fix is to name the dialect: `(«D» := D)`. The guillemets are needed because these files declare `local notation "D" => evmWithExternal calls creates`, which makes bare `D` a token rather than an identifier, so the parameter name has to be escaped. The proof terms are otherwise untouched. ## Tactic-syntax changes, called out Six `decreasing_by` blocks changed. `all_goals simp_wf <;> omega` became `all_goals simp_wf; omega` in five places (`ObjectResolve`, `InlineHelpers` x3, and the Batteries `unnecessarySeqFocus` linter's own recommendation — it fires because `simp_wf` now leaves one goal per invocation instead of several), and `DeadPureResolve`'s bare `all_goals simp_wf` gained `; omega` because `simp_wf` alone no longer closes `2 * sizeOf body ≤ 2 * (1 + sizeOf body)`. ## Audited spec surface: one hash moved, deliberately `SpecClosure.lean`'s pin for `YulEvmCompiler.opTable` changed from `e1b0c299397baebd` to `58d5b129f84835ed`, and `SPEC.md` is regenerated. The *value is identical*; only the elaboration of the five `Fin 5` literals in the LOG rows changed. With all of Mathlib in scope they were going through `SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat` — the `OfNat` instance on the simplicial-category object `[4]`, which happens to be defeq to `Fin 5`. They now use core's `Fin.instOfNat`. Verified by diffing the fully elaborated `opTable` term across the two trees (that instance is the only difference) and by evaluating the table on `log0..log4` in both: both give `Operation.Log { topics := 0..4 }`. The other 88 audited hashes and the 155-declaration external boundary hash are unchanged. Co-Authored-By: Claude Opus 5 (1M context) --- SPEC.md | 16 ++-- SpecClosure.lean | 2 +- YulEvmCompiler/Asm.lean | 2 + YulEvmCompiler/Decode.lean | 2 + YulEvmCompiler/ObjectResolve.lean | 5 +- .../Implementation/CoalesceCopies.lean | 3 +- .../Optimizer/Implementation/DeadLits.lean | 2 +- .../Optimizer/Implementation/DeadPure.lean | 10 +-- .../Implementation/DeadPureResolve.lean | 2 +- .../Implementation/FlattenSound.lean | 6 +- .../Implementation/FreshenCalls.lean | 6 +- .../Implementation/FreshenCallsResolve.lean | 2 +- .../Implementation/FuseDeclAssignSound.lean | 8 +- .../Optimizer/Implementation/HoistCalls.lean | 10 +-- .../Implementation/HoistCallsResolve.lean | 2 +- .../Implementation/InlineCallsSound.lean | 8 +- .../Implementation/InlineHelpers.lean | 9 ++- .../Optimizer/Implementation/Pipeline.lean | 4 +- .../Implementation/ReuseValuesSound.lean | 2 +- .../Optimizer/Implementation/Simplify.lean | 7 +- .../Implementation/StackLayoutSound.lean | 74 +++++++++---------- .../Implementation/StorageForwardResolve.lean | 2 +- .../Implementation/StorageForwardSound.lean | 2 +- YulEvmCompiler/Value.lean | 6 ++ YulIR/FrameCongr.lean | 1 + lake-manifest.json | 4 +- lakefile.toml | 2 +- 27 files changed, 110 insertions(+), 89 deletions(-) diff --git a/SPEC.md b/SPEC.md index 64f7e347..7ffd854b 100644 --- a/SPEC.md +++ b/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` | diff --git a/SpecClosure.lean b/SpecClosure.lean index 6b2853e4..282b580e 100644 --- a/SpecClosure.lean +++ b/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 diff --git a/YulEvmCompiler/Asm.lean b/YulEvmCompiler/Asm.lean index 60795f3b..7d5aad27 100644 --- a/YulEvmCompiler/Asm.lean +++ b/YulEvmCompiler/Asm.lean @@ -1,3 +1,5 @@ +import Mathlib.Tactic.NormNum.Ineq +import Mathlib.Tactic.NormNum.Basic import YulEvmCompiler.OpTable set_option warningAsError true /-! diff --git a/YulEvmCompiler/Decode.lean b/YulEvmCompiler/Decode.lean index 9db3b540..27386a68 100644 --- a/YulEvmCompiler/Decode.lean +++ b/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 diff --git a/YulEvmCompiler/ObjectResolve.lean b/YulEvmCompiler/ObjectResolve.lean index 104a60b9..c898ba38 100644 --- a/YulEvmCompiler/ObjectResolve.lean +++ b/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) | [] => [] diff --git a/YulEvmCompiler/Optimizer/Implementation/CoalesceCopies.lean b/YulEvmCompiler/Optimizer/Implementation/CoalesceCopies.lean index bbae07ab..36aa4e79 100644 --- a/YulEvmCompiler/Optimizer/Implementation/CoalesceCopies.lean +++ b/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₂), diff --git a/YulEvmCompiler/Optimizer/Implementation/DeadLits.lean b/YulEvmCompiler/Optimizer/Implementation/DeadLits.lean index 5f1241b7..0ff641a6 100644 --- a/YulEvmCompiler/Optimizer/Implementation/DeadLits.lean +++ b/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)) : diff --git a/YulEvmCompiler/Optimizer/Implementation/DeadPure.lean b/YulEvmCompiler/Optimizer/Implementation/DeadPure.lean index 77d195e2..347a5cd1 100644 --- a/YulEvmCompiler/Optimizer/Implementation/DeadPure.lean +++ b/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 diff --git a/YulEvmCompiler/Optimizer/Implementation/DeadPureResolve.lean b/YulEvmCompiler/Optimizer/Implementation/DeadPureResolve.lean index 3f2146c8..89a32b57 100644 --- a/YulEvmCompiler/Optimizer/Implementation/DeadPureResolve.lean +++ b/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), diff --git a/YulEvmCompiler/Optimizer/Implementation/FlattenSound.lean b/YulEvmCompiler/Optimizer/Implementation/FlattenSound.lean index 2c1a2078..ae8850ac 100644 --- a/YulEvmCompiler/Optimizer/Implementation/FlattenSound.lean +++ b/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 diff --git a/YulEvmCompiler/Optimizer/Implementation/FreshenCalls.lean b/YulEvmCompiler/Optimizer/Implementation/FreshenCalls.lean index fab607a8..cd976a95 100644 --- a/YulEvmCompiler/Optimizer/Implementation/FreshenCalls.lean +++ b/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)) diff --git a/YulEvmCompiler/Optimizer/Implementation/FreshenCallsResolve.lean b/YulEvmCompiler/Optimizer/Implementation/FreshenCallsResolve.lean index 10c0702a..abf4f6d8 100644 --- a/YulEvmCompiler/Optimizer/Implementation/FreshenCallsResolve.lean +++ b/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)) diff --git a/YulEvmCompiler/Optimizer/Implementation/FuseDeclAssignSound.lean b/YulEvmCompiler/Optimizer/Implementation/FuseDeclAssignSound.lean index 8c6d1eb2..518a47cd 100644 --- a/YulEvmCompiler/Optimizer/Implementation/FuseDeclAssignSound.lean +++ b/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⟩ diff --git a/YulEvmCompiler/Optimizer/Implementation/HoistCalls.lean b/YulEvmCompiler/Optimizer/Implementation/HoistCalls.lean index a0298c24..dc0805ae 100644 --- a/YulEvmCompiler/Optimizer/Implementation/HoistCalls.lean +++ b/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)) diff --git a/YulEvmCompiler/Optimizer/Implementation/HoistCallsResolve.lean b/YulEvmCompiler/Optimizer/Implementation/HoistCallsResolve.lean index 7d68a066..01066370 100644 --- a/YulEvmCompiler/Optimizer/Implementation/HoistCallsResolve.lean +++ b/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)) diff --git a/YulEvmCompiler/Optimizer/Implementation/InlineCallsSound.lean b/YulEvmCompiler/Optimizer/Implementation/InlineCallsSound.lean index 1f5d439d..505640d7 100644 --- a/YulEvmCompiler/Optimizer/Implementation/InlineCallsSound.lean +++ b/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 diff --git a/YulEvmCompiler/Optimizer/Implementation/InlineHelpers.lean b/YulEvmCompiler/Optimizer/Implementation/InlineHelpers.lean index f2fb9a59..22381536 100644 --- a/YulEvmCompiler/Optimizer/Implementation/InlineHelpers.lean +++ b/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} diff --git a/YulEvmCompiler/Optimizer/Implementation/Pipeline.lean b/YulEvmCompiler/Optimizer/Implementation/Pipeline.lean index f33cf511..49ee0776 100644 --- a/YulEvmCompiler/Optimizer/Implementation/Pipeline.lean +++ b/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)) diff --git a/YulEvmCompiler/Optimizer/Implementation/ReuseValuesSound.lean b/YulEvmCompiler/Optimizer/Implementation/ReuseValuesSound.lean index a491d374..e3561d28 100644 --- a/YulEvmCompiler/Optimizer/Implementation/ReuseValuesSound.lean +++ b/YulEvmCompiler/Optimizer/Implementation/ReuseValuesSound.lean @@ -3479,7 +3479,7 @@ theorem rvFunStmt_equiv : ∀ s : Stmt Op, EquivStmt D s (rvFunStmt s) (rvFunDflt_equiv dflt) | .forLoop init c post body => by simpa [rvFunStmt] using - (EquivStmt.forLoop_congr init (EquivExpr.refl c) + (EquivStmt.forLoop_congr init (EquivExpr.refl («D» := D) c) ((EquivBlock.of_stmts_funs (EquivStmts.of_forall₂ (rvFunStmts_forall2 post)) (rvFunScopeRel post)).trans diff --git a/YulEvmCompiler/Optimizer/Implementation/Simplify.lean b/YulEvmCompiler/Optimizer/Implementation/Simplify.lean index 62ad0490..e5aa0a18 100644 --- a/YulEvmCompiler/Optimizer/Implementation/Simplify.lean +++ b/YulEvmCompiler/Optimizer/Implementation/Simplify.lean @@ -1,3 +1,7 @@ +import Mathlib.Data.BitVec +import Batteries.Data.BitVec.Lemmas +import Mathlib.Algebra.Group.Defs +import Mathlib.Algebra.GroupWithZero.Basic import YulEvmCompiler.Optimizer.Spec.LocalPass import YulEvmCompiler.Optimizer.Core.Rule import YulEvmCompiler.Optimizer.Implementation.FunCongr @@ -1633,7 +1637,8 @@ theorem cond_lit_zero_equiv (l : Literal) (body : Block Op) cases h with | block hb => cases hb - simpa [restore] using (Step.ifFalse (body := body) Step.lit hz) + simpa [restore] using + (Step.ifFalse («D» := D) (body := body) Step.lit hz) /-- A true literal `if` is exactly its body block. -/ theorem cond_lit_nonzero_equiv (l : Literal) (body : Block Op) diff --git a/YulEvmCompiler/Optimizer/Implementation/StackLayoutSound.lean b/YulEvmCompiler/Optimizer/Implementation/StackLayoutSound.lean index 550b6b63..b6594d0f 100644 --- a/YulEvmCompiler/Optimizer/Implementation/StackLayoutSound.lean +++ b/YulEvmCompiler/Optimizer/Implementation/StackLayoutSound.lean @@ -159,7 +159,7 @@ theorem rightAssocAdd_equiv (a c : Expr Op) : · next a b c ihb iha => exact (add_assoc_equiv a b c).trans ((EquivExpr.builtin_congr Op.add (EquivArgs.of_forall₂ - (.cons (EquivExpr.refl a) (.cons ihb .nil)))).trans iha) + (.cons (EquivExpr.refl («D» := D) a) (.cons ihb .nil)))).trans iha) · exact EquivExpr.refl _ theorem scheduleBuiltin_equiv (op : Op) (args : List (Expr Op)) : @@ -487,7 +487,7 @@ theorem copyBackSite_equivBlock {pre suffix : Block Op} {ts ds : List Ident} (VEnv.setMany Vp ds vals) := by have hm0 := zip_mins (calls := calls) (creates := creates) (VEnv.setMany Vp ds vals) hvals' - rw [VEnv.setMany_length] at hm0 + rw [VEnv.setMany_length («D» := D)] at hm0 exact hm0 have hifree : InsFree (tempIns Vp.length ts) (.stmts suffix) := by intro p hp @@ -532,7 +532,7 @@ theorem copyBackSite_equivBlock {pre suffix : Block Op} {ts ds : List Ident} (VEnv.setMany Vp ds vals) := by have hm0 := zip_mins (calls := calls) (creates := creates) (VEnv.setMany Vp ds vals) hvals' - rw [VEnv.setMany_length] at hm0 + rw [VEnv.setMany_length («D» := D)] at hm0 exact hm0 have hifree : InsFree (tempIns Vp.length ts) (.stmts suffix) := by intro p hp @@ -988,12 +988,12 @@ theorem set_ne {d : Nat} {x z : Ident} {V : VEnv D} (h : LocalAt d x V) · rw [VEnv.set_append_mem hza] refine ⟨VEnv.set above z value, below, old, ?_, ?_, hd⟩ · rfl - · rw [VEnv.set_keys] + · rw [VEnv.set_keys («D» := D)] exact hx · rw [VEnv.set_append_not_mem hza] simp only [VEnv.set, if_neg (Ne.symm hz)] refine ⟨above, VEnv.set below z value, old, rfl, hx, ?_⟩ - rw [VEnv.set_length, hd] + rw [VEnv.set_length («D» := D), hd] end LocalAt @@ -1024,7 +1024,7 @@ namespace SlotRel theorem length {d dx : Nat} {x y : Ident} {V₁ V₂ : VEnv D} (h : SlotRel d dx x y V₁ V₂) : V₁.length = V₂.length + 1 := by obtain ⟨above, tail, value, rfl, rfl, -, -, -, -⟩ := h - rw [List.length_append, List.length_cons, List.length_append, VEnv.set_length] + rw [List.length_append, List.length_cons, List.length_append, VEnv.set_length («D» := D)] omega theorem get_y {d dx : Nat} {x y : Ident} {V₁ V₂ : VEnv D} @@ -1083,16 +1083,16 @@ theorem set {d dx : Nat} {x y z : Ident} {V₁ V₂ : VEnv D} refine ⟨VEnv.set above z value, tail, old, ?_, ?_, ?_, ?_, hd, hlocal⟩ · rfl · rfl - · rw [VEnv.set_keys] + · rw [VEnv.set_keys («D» := D)] exact hxa - · rw [VEnv.set_keys] + · rw [VEnv.set_keys («D» := D)] exact hya · rw [VEnv.set_append_not_mem hza, VEnv.set_append_not_mem hza] simp only [VEnv.set, if_neg (Ne.symm hzy)] have hcomm := VEnv.set_comm hzx tail value old rw [← hcomm] refine ⟨above, VEnv.set tail z value, old, rfl, rfl, hxa, hya, ?_, ?_⟩ - · rw [VEnv.set_length, hd] + · rw [VEnv.set_length («D» := D), hd] · exact hlocal.set_ne hzx value theorem setMany {d dx : Nat} {x y : Ident} {V₁ V₂ : VEnv D} @@ -1225,7 +1225,7 @@ theorem restore_nested {d dx : Nat} {x y : Ident} {Ve₁ Ve₂ Vb₁ Vb₂ : VEn omega have hk₂ : Vb₂.length - Ve₂.length = bodyAbove.length - entryAbove.length := by rw [he₂, hb₂, List.length_append, List.length_append, - VEnv.set_length, VEnv.set_length, hed, hbd] + VEnv.set_length («D» := D), VEnv.set_length («D» := D), hed, hbd] omega unfold YulSemantics.restore rw [hk₁, hk₂, hb₁, hb₂, @@ -1812,12 +1812,12 @@ theorem slot_fwd {funs : FunEnv D} {V₁ : VEnv D} {st : EvmState} · subst z refine ⟨.eres (.vals [value] st), ?_, ?_⟩ · simpa [renameCode, renameExpr] using - Step.var (by rw [← hslot.get_y]; exact hget) + Step.var («D» := D) (by rw [← hslot.get_y]; exact hget) · rfl · have hzx : z ≠ x := fun hzx => hmx hzx.symm refine ⟨.eres (.vals [value] st), ?_, ?_⟩ · simpa [renameCode, renameExpr, hzy] using - Step.var (by rw [← hslot.get_other hzx hzy]; exact hget) + Step.var («D» := D) (by rw [← hslot.get_other hzx hzy]; exact hget) · rfl | builtinOk hargs hb ihargs => intro d dx x y V₂ hslot hmx hdy @@ -1886,7 +1886,7 @@ theorem slot_fwd {funs : FunEnv D} {V₁ : VEnv D} {st : EvmState} | @funDef funs V st n ps rs body => intro d dx x y V₂ hslot _ _ refine ⟨.sres V₂ st .normal, ?_, ?_⟩ - · simpa [renameCode, renameStmt] using Step.funDef + · simpa [renameCode, renameStmt] using Step.funDef («D» := D) · exact ⟨hslot, rfl, rfl⟩ | @block funs V st body Vb stb o hbody ihbody => intro d dx x y V₂ hslot hmx hdy @@ -1909,7 +1909,7 @@ theorem slot_fwd {funs : FunEnv D} {V₁ : VEnv D} {st : EvmState} decide_eq_false_iff_not] at hmx simp only [codeDeclares, stmtDeclares] at hdy refine ⟨.sres (bindZeros D vars ++ V₂) st .normal, ?_, ?_⟩ - · simpa [renameCode, renameStmt] using Step.letZero + · simpa [renameCode, renameStmt] using Step.letZero («D» := D) · exact ⟨hslot.prependZeros hmx (by simpa using hdy), rfl, rfl⟩ | @letVal _ _ _ vars e values st' hexpr hlen ih => intro d dx x y V₂ hslot hmx hdy @@ -2082,20 +2082,20 @@ theorem slot_fwd {funs : FunEnv D} {V₁ : VEnv D} {st : EvmState} | @«break» funs V st => intro d dx x y V₂ hslot _ _ refine ⟨.sres V₂ st .«break», ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmt] using Step.break + simpa [renameCode, renameStmt] using Step.break («D» := D) | @«continue» funs V st => intro d dx x y V₂ hslot _ _ refine ⟨.sres V₂ st .«continue», ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmt] using Step.continue + simpa [renameCode, renameStmt] using Step.continue («D» := D) | @«leave» funs V st => intro d dx x y V₂ hslot _ _ refine ⟨.sres V₂ st .leave, ?_, ?_⟩ - · simpa [renameCode, renameStmt] using Step.leave + · simpa [renameCode, renameStmt] using Step.leave («D» := D) · exact ⟨hslot, rfl, rfl⟩ | @seqNil funs V st => intro d dx x y V₂ hslot _ _ refine ⟨.sres V₂ st .normal, ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmts] using Step.seqNil + simpa [renameCode, renameStmts] using Step.seqNil («D» := D) | @seqCons funs V st s rest Vs sts Vr str o hstmt hrest ihstmt ihrest => intro d dx x y V₂ hslot hmx hdy simp only [codeMentions, stmtsMentions, Bool.or_eq_false_iff] at hmx @@ -2264,12 +2264,12 @@ theorem slot_rev_fwd {funs : FunEnv D} {V₂ : VEnv D} {st : EvmState} · subst z refine ⟨.eres (.vals [value] st), ?_, ?_⟩ · simpa [renameCode, renameExpr] using - Step.var (by rw [hslot.get_y]; exact hget) + Step.var («D» := D) (by rw [hslot.get_y]; exact hget) · rfl · have hzy : z ≠ y := fun hzy => hmy hzy.symm refine ⟨.eres (.vals [value] st), ?_, ?_⟩ · simpa [renameCode, renameExpr, hzx] using - Step.var (by rw [hslot.get_other hzx hzy]; exact hget) + Step.var («D» := D) (by rw [hslot.get_other hzx hzy]; exact hget) · rfl | builtinOk hargs hb ihargs => intro d dx x y V₁ hslot hxy hmy hdx @@ -2338,7 +2338,7 @@ theorem slot_rev_fwd {funs : FunEnv D} {V₂ : VEnv D} {st : EvmState} | @funDef funs V st n ps rs body => intro d dx x y V₁ hslot hxy hmy hdx refine ⟨.sres V₁ st .normal, ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmt] using Step.funDef + simpa [renameCode, renameStmt] using Step.funDef («D» := D) | @block funs V st body Vb stb o hbody ihbody => intro d dx x y V₁ hslot hxy hmy hdx simp only [codeMentions, stmtMentions] at hmy @@ -2364,7 +2364,7 @@ theorem slot_rev_fwd {funs : FunEnv D} {V₂ : VEnv D} {st : EvmState} decide_eq_false_iff_not] at hmy simp only [codeDeclares, stmtDeclares] at hdx refine ⟨.sres (bindZeros D vars ++ V₁) st .normal, ?_, ?_⟩ - · simpa [renameCode, renameStmt] using Step.letZero + · simpa [renameCode, renameStmt] using Step.letZero («D» := D) · exact ⟨hslot.prependZeros (by simpa using hdx) (by simpa using hmy), rfl, rfl⟩ | @letVal funs V st vars e values st' hexpr hlen ih => intro d dx x y V₁ hslot hxy hmy hdx @@ -2534,19 +2534,19 @@ theorem slot_rev_fwd {funs : FunEnv D} {V₂ : VEnv D} {st : EvmState} | @«break» funs V st => intro d dx x y V₁ hslot hxy hmy hdx refine ⟨.sres V₁ st .«break», ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmt] using Step.break + simpa [renameCode, renameStmt] using Step.break («D» := D) | @«continue» funs V st => intro d dx x y V₁ hslot hxy hmy hdx refine ⟨.sres V₁ st .«continue», ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmt] using Step.continue + simpa [renameCode, renameStmt] using Step.continue («D» := D) | @«leave» funs V st => intro d dx x y V₁ hslot hxy hmy hdx refine ⟨.sres V₁ st .leave, ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmt] using Step.leave + simpa [renameCode, renameStmt] using Step.leave («D» := D) | @seqNil funs V st => intro d dx x y V₁ hslot hxy hmy hdx refine ⟨.sres V₁ st .normal, ?_, ⟨hslot, rfl, rfl⟩⟩ - simpa [renameCode, renameStmts] using Step.seqNil + simpa [renameCode, renameStmts] using Step.seqNil («D» := D) | @seqCons funs V st s rest Vs sts Vr str o hstmt hrest ihstmt ihrest => intro d dx x y V₁ hslot hxy hmy hdx simp only [codeMentions, stmtsMentions, Bool.or_eq_false_iff] at hmy @@ -2742,7 +2742,7 @@ theorem reuseSlot_equivBlock {pre rest : Block Op} {x y : Ident} Vp stp (.stmt (.assign [x] (.lit (.number 0)))) (.sres (VEnv.set Vp x (evmWithExternal calls creates).zero) stp .normal) := - Step.assignVal Step.lit rfl + Step.assignVal Step.lit («D» := D) rfl have hjoin := stmts_append_normal hpre (Step.seqCons hassign htarget) have hr := hslot'.restore_eq hxbase @@ -2971,7 +2971,7 @@ mutual obtain ⟨body', hb, hs'⟩ := Option.map_eq_some_iff.mp h subst s' exact ⟨EquivStmt.forLoop_congr init (fun _ _ _ _ => Iff.rfl) - (EquivBlock.refl _) + (EquivBlock.refl («D» := D) _) (stageOneStmts_sound P Phi' loopLayout body _ hb []), ScopeRel.refl _⟩ | _, _, _, .letDecl _ _, _, h => by simp [stageOneStmt] at h @@ -3116,7 +3116,7 @@ mutual obtain ⟨body', hb, hs'⟩ := Option.map_eq_some_iff.mp h subst s' exact ⟨EquivStmt.forLoop_congr init (fun _ _ _ _ => Iff.rfl) - (EquivBlock.refl _) + (EquivBlock.refl («D» := D) _) (copyOneStmts_sound (layoutAfter layout init) body _ hb []), ScopeRel.refl _⟩ | _, .letDecl _ _, _, h => by simp [copyOneStmt] at h @@ -3260,7 +3260,7 @@ mutual subst s' have heq := reuseOneStmts_sound layout [] body _ hb [] (by simp) exact ⟨EquivStmt.forLoop_congr init (fun _ _ _ _ => Iff.rfl) - (EquivBlock.refl _) heq, ScopeRel.refl _⟩ + (EquivBlock.refl («D» := D) _) heq, ScopeRel.refl _⟩ | _, .letDecl _ _, _, h => by simp [reuseOneStmt] at h | _, .assign _ _, _, h => by simp [reuseOneStmt] at h | _, .exprStmt _, _, h => by simp [reuseOneStmt] at h @@ -3491,7 +3491,7 @@ theorem restore_erase_head_set {outer tail : VEnv D} {c r : Ident} (c, old) :: VEnv.set tail r result := by simp [VEnv.set, hcr] rw [hc, hr₁, hr₂] simp only [restore, List.length_cons] - rw [VEnv.set_length] + rw [VEnv.set_length («D» := D)] rw [show tail.length + 1 - outer.length = (tail.length - outer.length) + 1 by omega] rfl @@ -3797,7 +3797,7 @@ theorem scopeTail_equivBlock {pre middle : Block Op} {carrier result : Ident} restore V (VEnv.set Vm result value) := by rw [← hrcomm] apply restore_restore hOuterVc - rw [VEnv.set_length] + rw [VEnv.set_length («D» := D)] exact hVcLen have henv : restore V (VEnv.set (restore Vc (VEnv.set Vm carrier value)) @@ -4035,7 +4035,7 @@ theorem scopeTail_equivBlock {pre middle : Block Op} {carrier result : Ident} restore V (VEnv.set Vm result value) := by rw [← hrcomm] apply restore_restore hOuterVc - rw [VEnv.set_length] + rw [VEnv.set_length («D» := D)] exact hVcLen have henv : restore V (VEnv.set @@ -4433,7 +4433,7 @@ mutual subst s' have heq := scopeOneStmts_sound layout body _ hb [] exact ⟨EquivStmt.forLoop_congr init (fun _ _ _ _ => Iff.rfl) - (EquivBlock.refl _) heq, ScopeRel.refl _⟩ + (EquivBlock.refl («D» := D) _) heq, ScopeRel.refl _⟩ | _, .letDecl _ _, _, h => by simp [scopeOneStmt] at h | _, .assign _ _, _, h => by simp [scopeOneStmt] at h | _, .exprStmt _, _, h => by simp [scopeOneStmt] at h @@ -5440,7 +5440,7 @@ mutual obtain ⟨body', hb, hs'⟩ := Option.map_eq_some_iff.mp h subst s' exact ⟨EquivStmt.forLoop_congr init (fun _ _ _ _ => Iff.rfl) - (EquivBlock.refl _) + (EquivBlock.refl («D» := D) _) (scopeOneDeadPrefixStmts_sound body _ hb []), ScopeRel.refl _⟩ | .letDecl _ _, _, h => by simp [StackV2.scopeOneDeadPrefixStmt] at h | .assign _ _, _, h => by simp [StackV2.scopeOneDeadPrefixStmt] at h @@ -6333,7 +6333,7 @@ private theorem aliasOneStmts_bound {layout : List Ident} · rintro ⟨_, hrun⟩ cases hrun with | block hbody => - have hrunOut := Step.block (by + have hrunOut := Step.block («D» := D) (by rw [hh] exact (hs (hoist D body :: funs) V st hbmem _ _ _).mp hbody) exact ⟨_, hrunOut⟩ @@ -6406,7 +6406,7 @@ private theorem SlotRel.copyBack_restore {d dx : Nat} {x y : Ident} have htail := congrArg List.length hkeys simp only [List.length_map, List.length_cons] at htail have htailBase : tail.length = base.length := by omega - rw [List.length_cons, VEnv.set_length, htailBase] + rw [List.length_cons, VEnv.set_length («D» := D), htailBase] simp rw [hlen] simp [hV₂] diff --git a/YulEvmCompiler/Optimizer/Implementation/StorageForwardResolve.lean b/YulEvmCompiler/Optimizer/Implementation/StorageForwardResolve.lean index 810b3872..eabedb97 100644 --- a/YulEvmCompiler/Optimizer/Implementation/StorageForwardResolve.lean +++ b/YulEvmCompiler/Optimizer/Implementation/StorageForwardResolve.lean @@ -235,7 +235,7 @@ theorem resolveSfFunStmt_equiv (L : Layout) : ∀ s : Stmt Op, | .forLoop init c post body => by rw [sfFunStmt, resolveForLayoutStmt_forLoop, resolveForLayoutStmt_forLoop] exact EquivStmt.forLoop_congr (resolveForLayoutStmts L init) - (EquivExpr.refl _) + (EquivExpr.refl («D» := D) _) ((EquivBlock.of_stmts_funs (EquivStmts.of_forall₂ (resolveSfFunStmts_forall2 L post)) (resolveSfFunScopeRel L post)).trans diff --git a/YulEvmCompiler/Optimizer/Implementation/StorageForwardSound.lean b/YulEvmCompiler/Optimizer/Implementation/StorageForwardSound.lean index 219eca52..02e67de9 100644 --- a/YulEvmCompiler/Optimizer/Implementation/StorageForwardSound.lean +++ b/YulEvmCompiler/Optimizer/Implementation/StorageForwardSound.lean @@ -1707,7 +1707,7 @@ theorem sfFunStmt_equiv : ∀ s : Stmt Op, EquivStmt D s (sfFunStmt s) (sfFunDflt_equiv dflt) | .forLoop init c post body => by simpa [sfFunStmt, storageForwardShallow] using - (EquivStmt.forLoop_congr init (EquivExpr.refl c) + (EquivStmt.forLoop_congr init (EquivExpr.refl («D» := D) c) ((EquivBlock.of_stmts_funs (EquivStmts.of_forall₂ (sfFunStmts_forall2 post)) (sfFunScopeRel post)).trans diff --git a/YulEvmCompiler/Value.lean b/YulEvmCompiler/Value.lean index 2ce86363..5ef45218 100644 --- a/YulEvmCompiler/Value.lean +++ b/YulEvmCompiler/Value.lean @@ -1,3 +1,9 @@ +import Mathlib.Algebra.Divisibility.Basic +import Mathlib.Algebra.Order.GroupWithZero.Basic +import Mathlib.Data.BitVec +import Mathlib.Tactic.NormNum.Basic +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring import EvmSemantics.Data.UInt256 import YulSemantics.Dialect.EVM set_option warningAsError true diff --git a/YulIR/FrameCongr.lean b/YulIR/FrameCongr.lean index 1eafded9..f43a9970 100644 --- a/YulIR/FrameCongr.lean +++ b/YulIR/FrameCongr.lean @@ -1,3 +1,4 @@ +import Batteries.Data.List.Basic import YulIR.FrameBigStep set_option warningAsError true diff --git a/lake-manifest.json b/lake-manifest.json index ea394f1e..7c3590c1 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "81b9e3ecaf4f17e3ade277af20383f87dde70862", + "rev": "a06f9701ea2299e465ece245b43204e94185c8dc", "name": "«yul-semantics»", "manifestFile": "lake-manifest.json", - "inputRev": "81b9e3ecaf4f17e3ade277af20383f87dde70862", + "inputRev": "a06f9701ea2299e465ece245b43204e94185c8dc", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", diff --git a/lakefile.toml b/lakefile.toml index 30b1abdb..0010ba4f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ defaultTargets = ["YulEvmCompiler", "YulParser", "YulEvmCompilerTests", "YulIR", [[require]] name = "yul-semantics" git = "https://github.com/powdr-labs/yul-semantics" -rev = "81b9e3ecaf4f17e3ade277af20383f87dde70862" +rev = "a06f9701ea2299e465ece245b43204e94185c8dc" # Target-language semantics: the EVM small-step/big-step relations. [[require]] From f92a5052c3b4388f2ec5d24288b4828870d6bf2e Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Thu, 30 Jul 2026 01:22:33 +0200 Subject: [PATCH 2/2] chore: repoint yul-semantics at the merged commit powdr-labs/yul-semantics#40 is merged. Move the pin off the unmerged branch commit and onto 4c6f9753 on that repository's main. The two commits have the identical tree (6f559621), so this changes the recorded SHA and nothing else; the build and corpus results measured against the branch commit carry over unchanged. Co-Authored-By: Claude Opus 5 (1M context) --- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 7c3590c1..fb4d1d9b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a06f9701ea2299e465ece245b43204e94185c8dc", + "rev": "4c6f9753cc0e5850f6bdaf6fb0df76457204699a", "name": "«yul-semantics»", "manifestFile": "lake-manifest.json", - "inputRev": "a06f9701ea2299e465ece245b43204e94185c8dc", + "inputRev": "4c6f9753cc0e5850f6bdaf6fb0df76457204699a", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", diff --git a/lakefile.toml b/lakefile.toml index 0010ba4f..237d9290 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ defaultTargets = ["YulEvmCompiler", "YulParser", "YulEvmCompilerTests", "YulIR", [[require]] name = "yul-semantics" git = "https://github.com/powdr-labs/yul-semantics" -rev = "a06f9701ea2299e465ece245b43204e94185c8dc" +rev = "4c6f9753cc0e5850f6bdaf6fb0df76457204699a" # Target-language semantics: the EVM small-step/big-step relations. [[require]]