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..fb4d1d9b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "81b9e3ecaf4f17e3ade277af20383f87dde70862", + "rev": "4c6f9753cc0e5850f6bdaf6fb0df76457204699a", "name": "«yul-semantics»", "manifestFile": "lake-manifest.json", - "inputRev": "81b9e3ecaf4f17e3ade277af20383f87dde70862", + "inputRev": "4c6f9753cc0e5850f6bdaf6fb0df76457204699a", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", diff --git a/lakefile.toml b/lakefile.toml index 30b1abdb..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 = "81b9e3ecaf4f17e3ade277af20383f87dde70862" +rev = "4c6f9753cc0e5850f6bdaf6fb0df76457204699a" # Target-language semantics: the EVM small-step/big-step relations. [[require]]