diff --git a/DESIGN.md b/DESIGN.md index 52e7a594..b164e74d 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -705,8 +705,10 @@ CI), which must stay in sync as coverage grows. the verified smart layout fallback described above, then the guarded memory spilling fallback when a safe scratch reservation is available. Irreducible frames without that contract still need EIP-8024 activation upstream. - Independent unsupported operations such as `gas`, immutables, and live - linker-symbol values are not accepted merely because spilling succeeds. + Independent unsupported operations such as `gas` are not accepted merely + because spilling succeeds. Immutables and supplied linker-symbol values are + now handled (see the immutables and library-linking entries), but neither is + a consequence of spilling. * **Optimizer.** A verified multi-stage pipeline, iterated six times, runs in front of the backend for block-rooted `compileSource` inputs (see `Optimizer/Implementation/Pipeline.lean` for the current stage list, and diff --git a/README.md b/README.md index cf962fbf..dd295028 100644 --- a/README.md +++ b/README.md @@ -325,8 +325,21 @@ to fall back to doing nothing. and call-path footprint, not the total number of selected bindings. Existing successful candidates still win before this fallback, so their bytecode and gas are unchanged. Programs without a safe guard contract remain rejected. - This fallback addresses stack reach only; `gas` and immutables remain - separate unsupported features. + This fallback addresses stack reach only; `gas` remains a separate + unsupported feature. +- **Immutables.** `loadimmutable(name)` compiles to a fixed-width `PUSH32` + placeholder (`Asm.pushImmutable`) whose 32 immediate bytes therefore sit at a + value-independent offset, and `setimmutable(base, name, value)` is **desugared + in the front end** to one `mstore` per recorded placeholder offset before the + object layer runs. Those offsets are a theorem, not a trusted computation: + `immutableOffsets_correct` shows each one really does locate that immutable's + 32-byte immediate in the emitted code, so a wrong offset cannot silently + miscompile. The emitted constants must also match the layout the code runs + under — that is `ConfMatch.imms`, the counterpart of `Layout.Consistent` for + data segments, discharged because no step ever rewrites `env.immutable`. + What is *not* proved is `setimmutable`'s meaning: it has no source semantics, + so the correctness theorem covers the desugared program, in the same family as + `memoryguard` desugaring rather than a proved source-to-source pass. - **Library linking.** `compileSource` takes an optional `LinkEnv` — the same `file.sol:Lib = 0xADDR` information as solc's `--libraries`, exposed on the CLI as `yulc --libraries=NAME=0xADDR[,…]`. A live `linkersymbol("file:Lib")` diff --git a/SPEC.md b/SPEC.md index 2566b989..6033bc8a 100644 --- a/SPEC.md +++ b/SPEC.md @@ -9,8 +9,8 @@ computed by walking each headline theorem's **statement** (never its proof), so the hundreds of preservation lemmas are excluded automatically — what remains is exactly the specification vocabulary. -**Audited surface: 89 declarations** \ -relations: 12 · structures: 12 · data defs: 51 · statements: 9 · artifact signatures: 4 \ +**Audited surface: 90 declarations** \ +relations: 12 · structures: 12 · data defs: 52 · statements: 9 · artifact signatures: 4 \ **External boundary: 155 declarations** across the two pinned semantics. Axioms are pinned separately in `Checks.lean` (only `propext`, @@ -26,7 +26,7 @@ flowchart TD S["Headline theorem statements (9)"] R["Match relations & predicates (12)"] T["Structures & data types (12)"] - D["Data definitions (51)"] + D["Data definitions (52)"] A["Artifact signatures (4) — type only, bodies free"] end subgraph external ["trusted ground truth — pinned dependency semantics"] @@ -49,13 +49,13 @@ The shape of each guarantee. Read these first: the honest scoping lives here. | declaration | source | hash | |---|---|---| -| `YulEvmCompiler.Optimizer.LocalPass.optimize_then_compile_correct` | [YulEvmCompiler/Optimizer/Spec/Backend.lean#L30](YulEvmCompiler/Optimizer/Spec/Backend.lean#L30) | `b97af54bdbe04c9f` | -| `YulEvmCompiler.compileObject_consistent` | [YulEvmCompiler/ObjectCompile.lean#L945](YulEvmCompiler/ObjectCompile.lean#L945) | `6772c506631c72d` | -| `YulEvmCompiler.compileObject_correct` | [YulEvmCompiler/ObjectCompile.lean#L968](YulEvmCompiler/ObjectCompile.lean#L968) | `6c28d636cabfed71` | -| `YulEvmCompiler.compile_correct` | [YulEvmCompiler/Correctness.lean#L71](YulEvmCompiler/Correctness.lean#L71) | `ec51f1c553a52f8a` | -| `YulEvmCompiler.compile_correct_eval` | [YulEvmCompiler/Correctness.lean#L265](YulEvmCompiler/Correctness.lean#L265) | `999e96fc09d553b6` | -| `YulEvmCompiler.compile_correct_withPayload` | [YulEvmCompiler/Correctness.lean#L178](YulEvmCompiler/Correctness.lean#L178) | `50e2c3107c79f9ea` | -| `YulEvmCompiler.compiled_constructor_returns` | [YulEvmCompiler/ObjectCompile.lean#L1000](YulEvmCompiler/ObjectCompile.lean#L1000) | `9a99d76f5d037853` | +| `YulEvmCompiler.Optimizer.LocalPass.optimize_then_compile_correct` | [YulEvmCompiler/Optimizer/Spec/Backend.lean#L30](YulEvmCompiler/Optimizer/Spec/Backend.lean#L30) | `d0b206bd07992491` | +| `YulEvmCompiler.compileObject_consistent` | [YulEvmCompiler/ObjectCompile.lean#L1030](YulEvmCompiler/ObjectCompile.lean#L1030) | `6772c506631c72d` | +| `YulEvmCompiler.compileObject_correct` | [YulEvmCompiler/ObjectCompile.lean#L1053](YulEvmCompiler/ObjectCompile.lean#L1053) | `6c28d636cabfed71` | +| `YulEvmCompiler.compile_correct` | [YulEvmCompiler/Correctness.lean#L71](YulEvmCompiler/Correctness.lean#L71) | `5da903b63e70655d` | +| `YulEvmCompiler.compile_correct_eval` | [YulEvmCompiler/Correctness.lean#L267](YulEvmCompiler/Correctness.lean#L267) | `44f9f79182ec7eda` | +| `YulEvmCompiler.compile_correct_withPayload` | [YulEvmCompiler/Correctness.lean#L179](YulEvmCompiler/Correctness.lean#L179) | `7fe10d0f9ce8438a` | +| `YulEvmCompiler.compiled_constructor_returns` | [YulEvmCompiler/ObjectCompile.lean#L1091](YulEvmCompiler/ObjectCompile.lean#L1091) | `9a99d76f5d037853` | | `YulParser.parse_canon_block` | [YulParser/Stmt.lean#L313](YulParser/Stmt.lean#L313) | `565944a3acfe55d3` | | `YulParser.parse_canon_obj` | [YulParser/Obj.lean#L139](YulParser/Obj.lean#L139) | `f40759b3ea852432` | @@ -67,13 +67,13 @@ How a source state/outcome corresponds to a target state/outcome. The heart of t |---|---|---| | `YulEvmCompiler.HaltMatch` | [YulEvmCompiler/StateRel.lean#L1252](YulEvmCompiler/StateRel.lean#L1252) | `6557b5faae906a61` | | `YulEvmCompiler.HaltedMatch` | [YulEvmCompiler/OpStep.lean#L50](YulEvmCompiler/OpStep.lean#L50) | `bd6cde934ed46ce6` | -| `YulEvmCompiler.IsCallOp` | [YulEvmCompiler/OpTable.lean#L90](YulEvmCompiler/OpTable.lean#L90) | `93349e44f6cba900` | -| `YulEvmCompiler.IsCreateOp` | [YulEvmCompiler/OpTable.lean#L98](YulEvmCompiler/OpTable.lean#L98) | `188d5668d6c00b2b` | +| `YulEvmCompiler.IsCallOp` | [YulEvmCompiler/OpTable.lean#L90](YulEvmCompiler/OpTable.lean#L90) | `4068ec650592c03e` | +| `YulEvmCompiler.IsCreateOp` | [YulEvmCompiler/OpTable.lean#L98](YulEvmCompiler/OpTable.lean#L98) | `b78befe1df320f16` | | `YulEvmCompiler.LogEntryMatch` | [YulEvmCompiler/StateRel.lean#L934](YulEvmCompiler/StateRel.lean#L934) | `44220474a51dc6b6` | | `YulEvmCompiler.LogsMatch` | [YulEvmCompiler/StateRel.lean#L942](YulEvmCompiler/StateRel.lean#L942) | `6d1d2dd35bc25e39` | | `YulEvmCompiler.MemMatch` | [YulEvmCompiler/StateRel.lean#L32](YulEvmCompiler/StateRel.lean#L32) | `e48211ef54b0d862` | | `YulEvmCompiler.Optimizer.Sound` | [YulEvmCompiler/Optimizer/Spec/LocalPass.lean#L64](YulEvmCompiler/Optimizer/Spec/LocalPass.lean#L64) | `d9d7947b1bb2287` | -| `YulEvmCompiler.RunResolvedObject` | [YulEvmCompiler/ObjectCompile.lean#L962](YulEvmCompiler/ObjectCompile.lean#L962) | `22471129a83f65e3` | +| `YulEvmCompiler.RunResolvedObject` | [YulEvmCompiler/ObjectCompile.lean#L1047](YulEvmCompiler/ObjectCompile.lean#L1047) | `22471129a83f65e3` | | `YulEvmCompiler.SelfdestructEntryMatch` | [YulEvmCompiler/StateRel.lean#L956](YulEvmCompiler/StateRel.lean#L956) | `3b1f6c17c9cc3b3f` | | `YulEvmCompiler.SelfdestructsMatch` | [YulEvmCompiler/StateRel.lean#L963](YulEvmCompiler/StateRel.lean#L963) | `8fb6a9b19498848` | | `YulParser.Parser` | [YulParser/Core.lean#L13](YulParser/Core.lean#L13) | `c3c38aa9630539e` | @@ -84,12 +84,12 @@ The vocabulary the guarantee is phrased in. | declaration | source | hash | |---|---|---| -| `YulEvmCompiler.CallsRealized` | [YulEvmCompiler/LowerDefs.lean#L308](YulEvmCompiler/LowerDefs.lean#L308) | `60cec34bf4c3cac9` | -| `YulEvmCompiler.CreatesRealized` | [YulEvmCompiler/LowerDefs.lean#L355](YulEvmCompiler/LowerDefs.lean#L355) | `d608d1effb3509d1` | +| `YulEvmCompiler.CallsRealized` | [YulEvmCompiler/LowerDefs.lean#L329](YulEvmCompiler/LowerDefs.lean#L329) | `60cec34bf4c3cac9` | +| `YulEvmCompiler.CreatesRealized` | [YulEvmCompiler/LowerDefs.lean#L376](YulEvmCompiler/LowerDefs.lean#L376) | `d608d1effb3509d1` | | `YulEvmCompiler.EnvMatch` | [YulEvmCompiler/StateRel.lean#L429](YulEvmCompiler/StateRel.lean#L429) | `9cea97fa8ae94f99` | | `YulEvmCompiler.ExternalCodeMatch` | [YulEvmCompiler/StateRel.lean#L494](YulEvmCompiler/StateRel.lean#L494) | `2d46717e52ff1871` | | `YulEvmCompiler.ExternalModel` | [YulEvmCompiler/AsmSem.lean#L34](YulEvmCompiler/AsmSem.lean#L34) | `75bd1eadd7f209e2` | -| `YulEvmCompiler.ExternalsRealized` | [YulEvmCompiler/LowerDefs.lean#L403](YulEvmCompiler/LowerDefs.lean#L403) | `7fd85ee803561fa8` | +| `YulEvmCompiler.ExternalsRealized` | [YulEvmCompiler/LowerDefs.lean#L424](YulEvmCompiler/LowerDefs.lean#L424) | `7fd85ee803561fa8` | | `YulEvmCompiler.FrameOK` | [YulEvmCompiler/StateRel.lean#L1240](YulEvmCompiler/StateRel.lean#L1240) | `97dc148ae9bebed5` | | `YulEvmCompiler.Instr` | [YulEvmCompiler/Instr.lean#L38](YulEvmCompiler/Instr.lean#L38) | `6d2465d1d211750b` | | `YulEvmCompiler.Optimizer.LocalPass` | [YulEvmCompiler/Optimizer/Spec/LocalPass.lean#L72](YulEvmCompiler/Optimizer/Spec/LocalPass.lean#L72) | `6b8887154f59257c` | @@ -107,17 +107,18 @@ Concrete spec-level functions (outcome maps, canonicalisation, byte assembly). | `YulEvmCompiler.Instr.opByte` | [YulEvmCompiler/Instr.lean#L52](YulEvmCompiler/Instr.lean#L52) | `1063189e226fb3ef` | | `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.assembleWithPayload` | [YulEvmCompiler/LowerDefs.lean#L144](YulEvmCompiler/LowerDefs.lean#L144) | `55ba5256c2c91c08` | | `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) | `58d5b129f84835ed` | +| `YulEvmCompiler.opTable` | [YulEvmCompiler/OpTable.lean#L19](YulEvmCompiler/OpTable.lean#L19) | `d48771ade3ef37b6` | | `YulEvmCompiler.resolveForLayoutCases` | [YulEvmCompiler/ObjectResolve.lean#L77](YulEvmCompiler/ObjectResolve.lean#L77) | `a635c809600d2d8a` | -| `YulEvmCompiler.resolveForLayoutExpr` | [YulEvmCompiler/ObjectResolve.lean#L25](YulEvmCompiler/ObjectResolve.lean#L25) | `15bc9ca915a17f5a` | +| `YulEvmCompiler.resolveForLayoutExpr` | [YulEvmCompiler/ObjectResolve.lean#L25](YulEvmCompiler/ObjectResolve.lean#L25) | `6e8a6c9691954597` | | `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` | +| `YulEvmCompiler.unpatchedImmutables` | [YulEvmCompiler/Compile.lean#L342](YulEvmCompiler/Compile.lean#L342) | `4350bdab12d0a1ca` | | `YulParser.afterBlockComment` | [YulParser/Tokens.lean#L30](YulParser/Tokens.lean#L30) | `5deac78dd9073c67` | | `YulParser.canon` | [YulParser/Canon.lean#L82](YulParser/Canon.lean#L82) | `b2d8eb356dc83a9c` | | `YulParser.decDigitVal` | [YulParser/Canon.lean#L52](YulParser/Canon.lean#L52) | `aa9b35f8e24246bf` | @@ -161,8 +162,8 @@ The code being verified. Only the signatures are frozen; implementations are fre | declaration | source | hash | |---|---|---| -| `YulEvmCompiler.compile` | [YulEvmCompiler/Compile.lean#L335](YulEvmCompiler/Compile.lean#L335) | `49a8d9e93773bc82` | -| `YulEvmCompiler.compileObject` | [YulEvmCompiler/ObjectCompile.lean#L858](YulEvmCompiler/ObjectCompile.lean#L858) | `45cacb379f48e375` | +| `YulEvmCompiler.compile` | [YulEvmCompiler/Compile.lean#L352](YulEvmCompiler/Compile.lean#L352) | `8db82c40ac47d5a6` | +| `YulEvmCompiler.compileObject` | [YulEvmCompiler/ObjectCompile.lean#L927](YulEvmCompiler/ObjectCompile.lean#L927) | `45cacb379f48e375` | | `YulParser.parseBlock` | [YulParser/Stmt.lean#L305](YulParser/Stmt.lean#L305) | `548f44114c0c0376` | | `YulParser.parseObject` | [YulParser/Obj.lean#L131](YulParser/Obj.lean#L131) | `7de98252fdadddab` | diff --git a/SpecClosure.lean b/SpecClosure.lean index 282b580e..aeed23f8 100644 --- a/SpecClosure.lean +++ b/SpecClosure.lean @@ -511,7 +511,7 @@ toolchain. -/ -- BEGIN SPEC CLOSURE PIN (generated by scripts/update-spec.sh — do not edit by hand) /-- info: -SPEC CLOSURE — audited this-repo surface (89 decls) +SPEC CLOSURE — audited this-repo surface (90 decls) struct YulEvmCompiler.CallsRealized 60cec34bf4c3cac9 struct YulEvmCompiler.CreatesRealized d608d1effb3509d1 struct YulEvmCompiler.EnvMatch 9cea97fa8ae94f99 @@ -524,13 +524,13 @@ SPEC CLOSURE — audited this-repo surface (89 decls) struct YulEvmCompiler.Instr 6d2465d1d211750b datadef YulEvmCompiler.Instr.bytes 6cb9a3bc72e0ae11 datadef YulEvmCompiler.Instr.opByte 1063189e226fb3ef - relation YulEvmCompiler.IsCallOp 93349e44f6cba900 - relation YulEvmCompiler.IsCreateOp 188d5668d6c00b2b + relation YulEvmCompiler.IsCallOp 4068ec650592c03e + relation YulEvmCompiler.IsCreateOp b78befe1df320f16 relation YulEvmCompiler.LogEntryMatch 44220474a51dc6b6 relation YulEvmCompiler.LogsMatch 6d1d2dd35bc25e39 relation YulEvmCompiler.MemMatch e48211ef54b0d862 struct YulEvmCompiler.Optimizer.LocalPass 6b8887154f59257c - statement YulEvmCompiler.Optimizer.LocalPass.optimize_then_compile_correct b97af54bdbe04c9f + statement YulEvmCompiler.Optimizer.LocalPass.optimize_then_compile_correct d0b206bd07992491 relation YulEvmCompiler.Optimizer.Sound d9d7947b1bb2287 relation YulEvmCompiler.RunResolvedObject 22471129a83f65e3 relation YulEvmCompiler.SelfdestructEntryMatch 3b1f6c17c9cc3b3f @@ -539,24 +539,25 @@ SPEC CLOSURE — audited this-repo surface (89 decls) datadef YulEvmCompiler.assemble c1c9c0c9a1ad80c8 datadef YulEvmCompiler.assembleBytes 29d8e692638cce98 datadef YulEvmCompiler.assembleWithPayload 55ba5256c2c91c08 - artifact YulEvmCompiler.compile 49a8d9e93773bc82 + artifact YulEvmCompiler.compile 8db82c40ac47d5a6 artifact YulEvmCompiler.compileObject 45cacb379f48e375 statement YulEvmCompiler.compileObject_consistent 6772c506631c72d statement YulEvmCompiler.compileObject_correct 6c28d636cabfed71 - statement YulEvmCompiler.compile_correct ec51f1c553a52f8a - statement YulEvmCompiler.compile_correct_eval 999e96fc09d553b6 - statement YulEvmCompiler.compile_correct_withPayload 50e2c3107c79f9ea + statement YulEvmCompiler.compile_correct 5da903b63e70655d + statement YulEvmCompiler.compile_correct_eval 44f9f79182ec7eda + statement YulEvmCompiler.compile_correct_withPayload 7fe10d0f9ce8438a statement YulEvmCompiler.compiled_constructor_returns 9a99d76f5d037853 datadef YulEvmCompiler.conv 25e701af8a9ce7bb datadef YulEvmCompiler.mkCode edacb826e56f9571 datadef YulEvmCompiler.natToBE d47a19daef761803 - datadef YulEvmCompiler.opTable 58d5b129f84835ed + datadef YulEvmCompiler.opTable d48771ade3ef37b6 datadef YulEvmCompiler.resolveForLayoutCases a635c809600d2d8a - datadef YulEvmCompiler.resolveForLayoutExpr 15bc9ca915a17f5a + datadef YulEvmCompiler.resolveForLayoutExpr 6e8a6c9691954597 datadef YulEvmCompiler.resolveForLayoutExprs deee862dd8d61de4 datadef YulEvmCompiler.resolveForLayoutStmt ef48ed8902b73d01 datadef YulEvmCompiler.resolveForLayoutStmts e61eedc003fbb530 datadef YulEvmCompiler.resultOf 9a4fae748007bd7b + datadef YulEvmCompiler.unpatchedImmutables 4350bdab12d0a1ca struct YulParser.CTok f0018424d20ab2ce relation YulParser.Parser c3c38aa9630539e struct YulParser.QuotedScan fda150592f3cfc21 diff --git a/YulEvmCompiler/Asm.lean b/YulEvmCompiler/Asm.lean index ddaa402b..5c04b3af 100644 --- a/YulEvmCompiler/Asm.lean +++ b/YulEvmCompiler/Asm.lean @@ -73,6 +73,16 @@ inductive Asm /-- Jump to the code address on top of the stack (function returns): lowers to `JUMP`. -/ | dynJump + /-- An **immutable** read: pushes `v`, the value `key`'s immutable holds in the + deployed code, always as a full-width `PUSH32`. + + The fixed width is the whole point. Ordinary `push` takes the minimal `PUSHk` + encoding, so its byte length varies with the value; an immutable's 32 immediate + bytes must sit at an offset the *constructor* can compute and patch, which + requires that offset to be independent of the value stored there. `key` carries + no runtime meaning — it exists so the object layer can report where each + placeholder landed. -/ + | pushImmutable (key : String) deriving Repr, DecidableEq /-- The uniform number of address bytes emitted for a label push (`jump`, @@ -105,6 +115,8 @@ def size : Asm → Nat | jumpi _ => labelWidth + 2 | pushLabel _ => labelWidth + 1 | dynJump => 1 + -- `PUSH32` opcode byte plus 32 immediate bytes, independent of `v`. + | pushImmutable _ => 33 theorem size_pos (i : Asm) : 1 ≤ i.size := by cases i <;> simp only [size] <;> omega @@ -430,7 +442,7 @@ theorem wfCheck_iff {p : List Asm} : wfCheck p = true ↔ WFProg p := by /-- Lower one instruction, resolving labels against the whole program `prog`. `none` when a referenced label is undefined (excluded by `wfCheck`) or the Yul op is outside `opTable`'s verified domain. -/ -def lowerInstr (prog : List Asm) : Asm → Option (List Instr) +def lowerInstr (imm : String → U256) (prog : List Asm) : Asm → Option (List Instr) | .push v => some [Instr.pushMin (conv v)] | .op yop => (opTable yop).map (fun o => [.op o]) | .dup n => some [.op (.Dup ⟨n⟩)] @@ -444,17 +456,20 @@ def lowerInstr (prog : List Asm) : Asm → Option (List Instr) | .pushLabel l => (resolve l prog).map (fun a => [.push labelWidthFin (UInt256.ofNat a)]) | .dynJump => some [.op .JUMP] + -- Always the full 32-byte immediate, so the value's byte position is fixed. + | .pushImmutable key => some [.push ⟨32, by norm_num⟩ (conv (imm key))] /-- Lower a fragment (against the whole program `prog`). -/ -def lowerFrag (prog : List Asm) : List Asm → Option (List Instr) +def lowerFrag (imm : String → U256) (prog : List Asm) : List Asm → Option (List Instr) | [] => some [] | i :: rest => do - let is1 ← lowerInstr prog i - let is2 ← lowerFrag prog rest + let is1 ← lowerInstr imm prog i + let is2 ← lowerFrag imm prog rest return is1 ++ is2 /-- Lower a whole program. -/ -def lowerProg (p : List Asm) : Option (List Instr) := lowerFrag p p +def lowerProg (imm : String → U256) (p : List Asm) : Option (List Instr) := + lowerFrag imm p p /-! ### Verified fast lowering @@ -609,7 +624,8 @@ theorem findLabelMap_getElem? (p : List Asm) (l : Label) : simp /-- `lowerInstr` against a precomputed address table. -/ -def lowerInstrWith (addrs : Std.HashMap Label Nat) : Asm → Option (List Instr) +def lowerInstrWith (imm : String → U256) (addrs : Std.HashMap Label Nat) : + Asm → Option (List Instr) | .push v => some [Instr.pushMin (conv v)] | .op yop => (opTable yop).map (fun o => [.op o]) | .dup n => some [.op (.Dup ⟨n⟩)] @@ -623,43 +639,47 @@ def lowerInstrWith (addrs : Std.HashMap Label Nat) : Asm → Option (List Instr) | .pushLabel l => addrs[l]?.map (fun a => [.push labelWidthFin (UInt256.ofNat a)]) | .dynJump => some [.op .JUMP] + | .pushImmutable key => some [.push ⟨32, by norm_num⟩ (conv (imm key))] -theorem lowerInstrWith_eq (p : List Asm) (i : Asm) : - lowerInstrWith (labelAddrs p) i = lowerInstr p i := by +theorem lowerInstrWith_eq (imm : String → U256) (p : List Asm) (i : Asm) : + lowerInstrWith imm (labelAddrs p) i = lowerInstr imm p i := by cases i <;> simp [lowerInstrWith, lowerInstr, labelAddrs_getElem?] /-- `lowerFrag` against a precomputed address table. -/ -def lowerFragWith (addrs : Std.HashMap Label Nat) : +def lowerFragWith (imm : String → U256) (addrs : Std.HashMap Label Nat) : List Asm → Option (List Instr) | [] => some [] | i :: rest => do - let is1 ← lowerInstrWith addrs i - let is2 ← lowerFragWith addrs rest + let is1 ← lowerInstrWith imm addrs i + let is2 ← lowerFragWith imm addrs rest return is1 ++ is2 -theorem lowerFragWith_eq (p : List Asm) : - ∀ c : List Asm, lowerFragWith (labelAddrs p) c = lowerFrag p c := by +theorem lowerFragWith_eq (imm : String → U256) (p : List Asm) : + ∀ c : List Asm, lowerFragWith imm (labelAddrs p) c = lowerFrag imm p c := by intro c induction c with | nil => rfl | cons i rest ih => simp [lowerFragWith, lowerFrag, lowerInstrWith_eq, ih] /-- One-pass lowering: build the address table once, then lower. -/ -def lowerProgFast (p : List Asm) : Option (List Instr) := - lowerFragWith (labelAddrs p) p +def lowerProgFast (imm : String → U256) (p : List Asm) : Option (List Instr) := + lowerFragWith imm (labelAddrs p) p @[csimp] theorem lowerProg_eq_lowerProgFast : @lowerProg = @lowerProgFast := by - funext p + funext imm p rw [lowerProgFast, lowerProg, lowerFragWith_eq] /-- Lowered width is `Asm.size`, for every constructor. -/ -theorem lowerInstr_length {prog : List Asm} {i : Asm} {is : List Instr} - (h : lowerInstr prog i = some is) : +theorem lowerInstr_length {imm : String → U256} {prog : List Asm} {i : Asm} + {is : List Instr} (h : lowerInstr imm prog i = some is) : (assembleBytes is).length = i.size := by cases i <;> simp only [lowerInstr] at h case push v => obtain rfl : [Instr.pushMin (conv v)] = is := by simpa using h simp [Asm.size] + case pushImmutable key => + obtain rfl : [Instr.push ⟨32, by norm_num⟩ (conv (imm key))] = is := by simpa using h + simp [Asm.size, assembleBytes, Instr.bytes] case op yop => obtain ⟨o, -, rfl⟩ := Option.map_eq_some_iff.mp h simp [Asm.size] @@ -696,11 +716,11 @@ theorem lowerInstr_length {prog : List Asm} {i : Asm} {is : List Instr} obtain rfl : [Instr.op .JUMP] = is := by simpa using h simp [Asm.size] -@[simp] theorem lowerFrag_nil (prog : List Asm) : lowerFrag prog [] = some [] := rfl +@[simp] theorem lowerFrag_nil (prog : List Asm) : lowerFrag imm prog [] = some [] := rfl theorem lowerFrag_cons {prog : List Asm} {i : Asm} {p : List Asm} {is : List Instr} - (h : lowerFrag prog (i :: p) = some is) : - ∃ is1 is2, lowerInstr prog i = some is1 ∧ lowerFrag prog p = some is2 + (h : lowerFrag imm prog (i :: p) = some is) : + ∃ is1 is2, lowerInstr imm prog i = some is1 ∧ lowerFrag imm prog p = some is2 ∧ is = is1 ++ is2 := by rw [lowerFrag, Option.bind_eq_bind] at h obtain ⟨is1, h1, h'⟩ := Option.bind_eq_some_iff.mp h @@ -709,16 +729,16 @@ theorem lowerFrag_cons {prog : List Asm} {i : Asm} {p : List Asm} {is : List Ins theorem lowerFrag_cons' {prog : List Asm} {i : Asm} {p : List Asm} {is1 is2 : List Instr} - (h1 : lowerInstr prog i = some is1) (h2 : lowerFrag prog p = some is2) : - lowerFrag prog (i :: p) = some (is1 ++ is2) := by + (h1 : lowerInstr imm prog i = some is1) (h2 : lowerFrag imm prog p = some is2) : + lowerFrag imm prog (i :: p) = some (is1 ++ is2) := by rw [lowerFrag, Option.bind_eq_bind, h1, Option.bind_some, h2] rfl /-- Splitting a successful fragment lowering at an append. -/ theorem lowerFrag_append {prog : List Asm} : ∀ {p q : List Asm} {is : List Instr}, - lowerFrag prog (p ++ q) = some is → - ∃ is1 is2, lowerFrag prog p = some is1 ∧ lowerFrag prog q = some is2 + lowerFrag imm prog (p ++ q) = some is → + ∃ is1 is2, lowerFrag imm prog p = some is1 ∧ lowerFrag imm prog q = some is2 ∧ is = is1 ++ is2 := by intro p induction p with @@ -733,8 +753,8 @@ theorem lowerFrag_append {prog : List Asm} : /-- Joining fragment lowerings across an append. -/ theorem lowerFrag_append' {prog : List Asm} : ∀ {p q : List Asm} {is1 is2 : List Instr}, - lowerFrag prog p = some is1 → lowerFrag prog q = some is2 → - lowerFrag prog (p ++ q) = some (is1 ++ is2) := by + lowerFrag imm prog p = some is1 → lowerFrag imm prog q = some is2 → + lowerFrag imm prog (p ++ q) = some (is1 ++ is2) := by intro p induction p with | nil => @@ -751,7 +771,7 @@ theorem lowerFrag_append' {prog : List Asm} : /-- Lowered fragment byte length is its `codeSize`. -/ theorem lowerFrag_length {prog : List Asm} : ∀ {p : List Asm} {is : List Instr}, - lowerFrag prog p = some is → + lowerFrag imm prog p = some is → (assembleBytes is).length = codeSize p := by intro p induction p with diff --git a/YulEvmCompiler/AsmPeepholeSound.lean b/YulEvmCompiler/AsmPeepholeSound.lean index 657deb70..cff31379 100644 --- a/YulEvmCompiler/AsmPeepholeSound.lean +++ b/YulEvmCompiler/AsmPeepholeSound.lean @@ -78,6 +78,11 @@ theorem astep_stkRefs [model : ExternalModel] {R : List Label} rcases List.mem_cons.mp hl with h | h · cases h · exact hσ l h + | pushImmutable => + intro l hl + rcases List.mem_cons.mp hl with h | h + · cases h + · exact hσ l h | @op yop args rets c σ yst yst' hb => intro l hl rcases List.mem_append.mp hl with h | h @@ -235,6 +240,12 @@ theorem step_sim [model : ExternalModel] {R : List Label} {prog prog' : List Asm cases hc with | keep _ hc' => exact ⟨_, .single .push, .sync hc'⟩ | window hn hc' => exact ⟨_, .refl _, .mid1 hn hc'⟩ + | @pushImmutable key c σ2 yst => + -- No peephole window ever opens on an immutable placeholder, so the pass + -- can only `keep` it — which is exactly what must happen: folding one + -- would move the 32 bytes the constructor patches. + cases hc with + | keep _ hc' => exact ⟨_, .single .pushImmutable, .sync hc'⟩ | @op yop args rets c σ2 yst yst' hb => cases hc with | keep _ hc' => exact ⟨_, .single (.op hb), .sync hc'⟩ diff --git a/YulEvmCompiler/AsmSem.lean b/YulEvmCompiler/AsmSem.lean index e3e71839..53a3d2a6 100644 --- a/YulEvmCompiler/AsmSem.lean +++ b/YulEvmCompiler/AsmSem.lean @@ -70,6 +70,16 @@ inductive AStep (prog : List Asm) [model : ExternalModel] : /-- Push a word. -/ | push {v : U256} {c : List Asm} {σ : List AVal} {yst : EvmState} : AStep (model := model) prog ⟨.push v :: c, σ, yst⟩ ⟨c, .word v :: σ, yst⟩ + /-- Read an immutable: push the value the environment records for `key`, + mirroring the source built-in `loadimmutable` (which reads the same map on the + same keying). The premise is what ties the constant the compiler baked into + the instruction to the value the source semantics would produce, so a + placeholder that disagrees with the layout simply cannot step. -/ + | pushImmutable {key : String} {c : List Asm} {σ : List AVal} + {yst : EvmState} : + AStep (model := model) prog ⟨.pushImmutable key :: c, σ, yst⟩ + ⟨c, .word (yst.env.immutable (YulSemantics.EVM.litValue (.string key))) :: σ, + yst⟩ /-- A non-halting built-in: consume the argument words, push the results, step the machine state — all by the Yul dialect's own relation. -/ | op {yop : Op} {args rets : List U256} {c : List Asm} {σ : List AVal} @@ -171,6 +181,7 @@ theorem AStep.suffix [model : ExternalModel] exact ⟨pre ++ [i], by simpa using hpre⟩ cases h with | push => exact tail_suffix ha + | pushImmutable => exact tail_suffix ha | op _ => exact tail_suffix ha | dup _ => exact tail_suffix ha | swap _ => exact tail_suffix ha @@ -182,6 +193,65 @@ theorem AStep.suffix [model : ExternalModel] | pushLabel _ => exact tail_suffix ha | dynJump hfind => exact findLabel_suffix hfind +/-! ### The immutable map is never rewritten + +Phase B's `ConfMatch.imms` states, once, that the constants baked into the +emitted bytes are the ones the environment records. For that to survive a whole +run, no step may rewrite `env.immutable`. It does not: every environment update +in the source semantics is a `{ st.env with … }` over balances, code hashes, +nonces, storage or transient storage, and the open-world endpoints install a +`CallWorld`, which has the same shape. Each fact below is definitional. -/ + +section ImmutablePreserved +open YulSemantics.EVM + +@[simp] private theorem touchMemory_immutable (st : EvmState) (o n : Nat) : + (touchMemory st o n).env.immutable = st.env.immutable := rfl + +@[simp] private theorem touchMemory2_immutable (st : EvmState) (a b c d : Nat) : + (touchMemory2 st a b c d).env.immutable = st.env.immutable := rfl + +@[simp] private theorem install_immutable (w : CallWorld) (st : EvmState) : + (w.install st).env.immutable = st.env.immutable := rfl + +@[simp] private theorem appendLog_immutable (st : EvmState) (topics : List U256) + (o n : U256) : + (appendLog st topics o n).env.immutable = st.env.immutable := rfl + +@[simp] private theorem finishCall_immutable (kind : CallKind) (st : EvmState) + (r : CallResponse) (a b c d : Nat) : + (finishCall kind st r a b c d).env.immutable = st.env.immutable := by + unfold finishCall + split <;> rfl + +@[simp] private theorem finishCreate_immutable (st : EvmState) (r : CreateResponse) + (o n : Nat) : + (finishCreate st r o n).env.immutable = st.env.immutable := by + unfold finishCreate + split <;> rfl + +end ImmutablePreserved + +/-- **No step ever rewrites the immutable map.** This is what lets phase B's +layout-consistency obligation for immutables be stated once and carried along a +whole run. -/ +theorem builtinWithExternal_immutable_eq + {calls : ExternalCalls} {creates : ExternalCreates} {yop : Op} + {args rets : List U256} {yst yst' : EvmState} + (hb : builtinWithExternal calls creates yop args yst (.ok rets yst')) : + yst'.env.immutable = yst.env.immutable := by + cases yop <;> + rcases args with _ | ⟨x, _ | ⟨y, _ | ⟨z, _ | ⟨w, _ | ⟨u, _ | ⟨t, _ | ⟨r, args⟩⟩⟩⟩⟩⟩⟩ <;> + simp_all [YulSemantics.EVM.builtinWithExternal, YulSemantics.EVM.externalCall, + YulSemantics.EVM.externalCreate, YulSemantics.EVM.stepOp, + YulSemantics.EVM.un, YulSemantics.EVM.bin, YulSemantics.EVM.ter, + YulSemantics.EVM.rd0, YulSemantics.EVM.rd1, YulSemantics.EVM.guardStatic] <;> + (try (split at hb)) <;> + (try (obtain ⟨-, rfl⟩ := hb; simp)) <;> + (try (obtain ⟨_, -, -, rfl⟩ := hb; simp)) <;> + (try (obtain ⟨-, _, -, hres⟩ := hb; simp_all)) <;> + (try simp_all) + theorem ASteps.suffix [model : ExternalModel] {prog : List Asm} {a b : AConf} (h : ASteps (model := model) prog a b) (ha : a.code <:+ prog) : b.code <:+ prog := by diff --git a/YulEvmCompiler/Compile.lean b/YulEvmCompiler/Compile.lean index 3d27abd3..16baf3be 100644 --- a/YulEvmCompiler/Compile.lean +++ b/YulEvmCompiler/Compile.lean @@ -168,9 +168,16 @@ def compileExpr (Φ : FMap) (Γ : List Ident) (off : Nat) (n : Nat) : some ([.dup ⟨off + idx, h⟩], n) else none -- too deep for DUP16 (needs EIP-8024) - | .builtin op args => do - let (argCode, n1) ← compileArgs Φ Γ off n args - some (argCode ++ [.op op], n1) + | .builtin op args => + match op, args with + -- An immutable read is a link-time constant: emit a fixed-width + -- placeholder naming it. `lowerProg` bakes in the assignment's value, so + -- the byte position of those 32 bytes does not depend on the value the + -- deploying constructor will patch into them. + | .loadimmutable, [.lit (.string key)] => some ([.pushImmutable key], n) + | _, _ => do + let (argCode, n1) ← compileArgs Φ Γ off n args + some (argCode ++ [.op op], n1) | .call f args => do let (info, _) ← lookupF Φ f let lret := n @@ -332,6 +339,16 @@ def compileProgram (prog : Block Op) : Option (List Asm) := do let (asm, _, _) ← compileStmts [scope] [] none none n0 prog if wfCheck asm then some asm else none +/-- The assignment used when emitting *unpatched* code: every immutable's +placeholder is written as zero, for the deploying constructor's `setimmutable` +to overwrite with the real value. + +It is not "no immutables" — the placeholders are there, and `immutableOffsets` +records where. The choice of value is immaterial to the layout, because +`Asm.size` of `pushImmutable` is a constant, which is exactly what lets the +constructor compute the offsets it patches. -/ +def unpatchedImmutables : String → U256 := fun _ => 0 + /-- The full pipeline: Yul → labeled assembly → Asm-level peephole optimization → byte-level IR. `optimizeAsm` preserves the label structure (`codeRel_wf`), and `YulEvmCompiler.Correctness` threads its forward simulation (`AsmPeepholeSound`) between the phase-A and phase-B theorems. The `stackOK2` @@ -340,9 +357,97 @@ EVM operand stack — recursive calls and stack-growing loops — so every accep overflow-free (`StackScalable.run_stack_bound2`). The bound is taken on `optimizeAsm asm`, the code that actually runs. The gate is a *linear* frame-relative analysis + verified checker (`analyze` then `checkCert`). -/ -def compile (prog : Block Op) : Option (List Instr) := do +def compile (prog : Block Op) + (imm : String → U256 := unpatchedImmutables) : Option (List Instr) := do + let asm ← compileProgram prog + let opt := optimizeAsm asm + if stackOK2 opt then lowerProg imm opt else none + +/-- The accepted program's *optimized* `Asm` — the code `compile` actually +lowers. The object layer needs it to locate immutable placeholders, whose byte +offsets the deploying constructor patches. -/ +def compileAsm (prog : Block Op) : Option (List Asm) := do let asm ← compileProgram prog let opt := optimizeAsm asm - if stackOK2 opt then lowerProg opt else none + if stackOK2 opt then some opt else none + +/-- Byte offsets of each immutable placeholder's 32-byte immediate, relative to +the start of the emitted code. `Asm.size` is fixed for every constructor, so +these positions do not depend on the values that will be patched in. -/ +def immutableOffsets : List Asm → Nat → List (String × Nat) + | [], _ => [] + | .pushImmutable key :: rest, p => + -- one opcode byte, then the 32 immediate bytes + (key, p + 1) :: immutableOffsets rest (p + 33) + | i :: rest, p => immutableOffsets rest (p + i.size) + +/-- Dropping past a prefix. -/ +private theorem drop_append_ge {α : Type} : + ∀ (a b : List α) (n : Nat), a.length ≤ n → (a ++ b).drop n = b.drop (n - a.length) + | [], b, n, _ => by simp + | x :: a, b, 0, h => by simp at h + | x :: a, b, n + 1, h => by + simp only [List.cons_append, List.drop_succ_cons, List.length_cons] + rw [drop_append_ge a b n (by simpa using h), + show n + 1 - (a.length + 1) = n - a.length by omega] + +/-- **The reported offsets are right.** Reading 32 bytes at any offset +`immutableOffsets` reports yields exactly the immediate `lowerProg` emitted for +that immutable. `setimmutable` patches at those offsets and nothing else checks +them, so a wrong one would be a silent miscompilation; this rules that out. +Stated for a fragment at an arbitrary base so the induction goes through. -/ +theorem immutableOffsets_spec {imm : String → U256} {prog : List Asm} : + ∀ (c : List Asm) (base : Nat) (frag : List Instr), + lowerFrag imm prog c = some frag → + ∀ key off, (key, off) ∈ immutableOffsets c base → + base ≤ off ∧ + ((assembleBytes frag).drop (off - base)).take 32 + = natToBE (conv (imm key)).toNat 32 := by + intro c + induction c with + | nil => intro base frag _ key off hmem; simp [immutableOffsets] at hmem + | cons i rest ih => + intro base frag hlow key off hmem + simp only [lowerFrag, Option.bind_eq_bind] at hlow + obtain ⟨is1, his1, hlow⟩ := Option.bind_eq_some_iff.mp hlow + obtain ⟨is2, his2, hlow⟩ := Option.bind_eq_some_iff.mp hlow + obtain rfl : is1 ++ is2 = frag := by simpa using hlow + have hlen : (assembleBytes is1).length = i.size := lowerInstr_length his1 + have hsplit : assembleBytes (is1 ++ is2) = assembleBytes is1 ++ assembleBytes is2 := by + simp [assembleBytes] + cases i with + | pushImmutable k => + obtain rfl : [Instr.push ⟨32, by norm_num⟩ (conv (imm k))] = is1 := by + simpa [lowerInstr] using his1 + have hb : assembleBytes [Instr.push ⟨32, by norm_num⟩ (conv (imm k))] + = UInt8.ofNat (0x5f + 32) :: natToBE (conv (imm k)).toNat 32 := by + simp [assembleBytes, Instr.bytes] + have hb33 : (assembleBytes [Instr.push ⟨32, by norm_num⟩ (conv (imm k))]).length = 33 := by + rw [hb]; simp + simp only [immutableOffsets, List.mem_cons, Prod.mk.injEq] at hmem + rcases hmem with ⟨rfl, rfl⟩ | h + · refine ⟨by omega, ?_⟩ + rw [hsplit, hb, show base + 1 - base = 1 by omega] + simp + · obtain ⟨hge, hbytes⟩ := ih (base + 33) is2 his2 key off h + refine ⟨by omega, ?_⟩ + rw [hsplit, drop_append_ge _ _ _ (by rw [hb33]; omega), hb33, Nat.sub_sub] + exact hbytes + | _ => + simp only [immutableOffsets] at hmem + obtain ⟨hge, hbytes⟩ := ih (base + Asm.size _) is2 his2 key off hmem + refine ⟨by omega, ?_⟩ + rw [hsplit, drop_append_ge _ _ _ (by rw [hlen]; omega), hlen] + rw [Nat.sub_sub] + exact hbytes + +/-- Whole-program form: every offset `immutableOffsets` reports for the accepted +program locates that immutable's immediate in the emitted bytes. -/ +theorem immutableOffsets_correct {imm : String → U256} {p : List Asm} {is : List Instr} + (hlow : lowerProg imm p = some is) {key : String} {off : Nat} + (hmem : (key, off) ∈ immutableOffsets p 0) : + ((assembleBytes is).drop off).take 32 = natToBE (conv (imm key)).toNat 32 := by + have := (immutableOffsets_spec (imm := imm) (prog := p) p 0 is hlow key off hmem).2 + simpa using this end YulEvmCompiler diff --git a/YulEvmCompiler/Correctness.lean b/YulEvmCompiler/Correctness.lean index f9455672..93a83b3d 100644 --- a/YulEvmCompiler/Correctness.lean +++ b/YulEvmCompiler/Correctness.lean @@ -88,8 +88,9 @@ callee/init code, nested calls/creations, and reentrant executions are included. -/ theorem compile_correct (hexternal : ExternalsRealized model) {prog : YulSemantics.Block Op} {is : List Instr} - (hcomp : compile prog = some is) + (hcomp : compile prog imm = some is) {yst0 : EvmState} {V' : VEnv yulD} {yst' : EvmState} {o : Outcome} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) (hrun : YulSemantics.Run yulD prog yst0 V' yst' o) : ∃ b : Nat, ∀ s0 : State, FrameOK (assemble is) s0 → StateMatch yst0 s0 → @@ -104,7 +105,7 @@ theorem compile_correct (hexternal : ExternalsRealized model) -- extract the stack-overflow check (on the *optimized* Asm) and the lowering from the -- gated pipeline obtain ⟨hstk, hcomp⟩ : - stackOK2 (optimizeAsm asm) = true ∧ lowerProg (optimizeAsm asm) = some is := by + stackOK2 (optimizeAsm asm) = true ∧ lowerProg imm (optimizeAsm asm) = some is := by split at hcomp · next h => exact ⟨h, hcomp⟩ · exact absurd hcomp (by simp) @@ -139,8 +140,8 @@ theorem compile_correct (hexternal : ExternalsRealized model) (stackOK2_run_bound hstk yst0) refine ⟨bnd, ?_⟩ intro s0 hf hm hpc hstk0 hgas - have hcm0 : ConfMatch (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := - ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp⟩ + have hcm0 : ConfMatch imm (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := + ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp, himm⟩ obtain ⟨s1, hsteps1, hcm1, -⟩ := Hb s0 hcm0 hgas have hpc1 : s1.pc = UInt256.ofNat (assembleBytes is).length := by rw [hcm1.pc]; simp [hlen] @@ -167,8 +168,8 @@ theorem compile_correct (hexternal : ExternalsRealized model) (List.suffix_refl (optimizeAsm asm)) (stackOK2_run_bound hstk yst0) refine ⟨bnd, ?_⟩ intro s0 hf hm hpc hstk0 hgas - have hcm0 : ConfMatch (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := - ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp⟩ + have hcm0 : ConfMatch imm (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := + ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp, himm⟩ obtain ⟨s', hsteps', hsm', hcs', hhm'⟩ := Hb s0 hcm0 hgas exact ⟨s', hsteps', hcs', hsm', Or.inr ⟨rfl, hhm'⟩⟩ | «break» => rcases hout with ⟨lc, hlc, -⟩; exact absurd hlc (by simp) @@ -183,8 +184,9 @@ seam, while a source halt preserves its exact halt result before reaching the payload. -/ theorem compile_correct_withPayload (hexternal : ExternalsRealized model) {prog : YulSemantics.Block Op} {is : List Instr} {payload : List UInt8} - (hcomp : compile prog = some is) + (hcomp : compile prog imm = some is) {yst0 : EvmState} {V' : VEnv yulD} {yst' : EvmState} {o : Outcome} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) (hrun : YulSemantics.Run yulD prog yst0 V' yst' o) : ∃ b : Nat, ∀ s0 : State, FrameOK (assembleWithPayload is (0 :: payload)) s0 → StateMatch yst0 s0 → @@ -196,7 +198,7 @@ theorem compile_correct_withPayload (hexternal : ExternalsRealized model) · simp [compile, hpa] at hcomp · simp only [compile, hpa, bind, Option.bind] at hcomp obtain ⟨hstk, hcomp⟩ : - stackOK2 (optimizeAsm asm) = true ∧ lowerProg (optimizeAsm asm) = some is := by + stackOK2 (optimizeAsm asm) = true ∧ lowerProg imm (optimizeAsm asm) = some is := by split at hcomp · next h => exact ⟨h, hcomp⟩ · exact absurd hcomp (by simp) @@ -226,8 +228,8 @@ theorem compile_correct_withPayload (hexternal : ExternalsRealized model) refine ⟨bnd, ?_⟩ intro s0 hf hm hpc hstk0 hgas have hcm0 : ConfMatch (payload := 0 :: payload) - (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := - ⟨hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp⟩ + imm (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := + ⟨hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp, himm⟩ obtain ⟨s1, hsteps1, hcm1, -⟩ := Hb s0 hcm0 hgas have hpc1 : s1.pc = UInt256.ofNat (assembleBytes is).length := by rw [hcm1.pc] @@ -254,8 +256,8 @@ theorem compile_correct_withPayload (hexternal : ExternalsRealized model) refine ⟨bnd, ?_⟩ intro s0 hf hm hpc hstk0 hgas have hcm0 : ConfMatch (payload := 0 :: payload) - (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := - ⟨hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp⟩ + imm (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := + ⟨hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp, himm⟩ obtain ⟨s', hsteps', hsm', hcs', hhm'⟩ := Hb s0 hcm0 hgas exact ⟨s', hsteps', hcs', hsm', Or.inr ⟨rfl, hhm'⟩⟩ | «break» => rcases hout with ⟨lc, hlc, -⟩; exact absurd hlc (by simp) @@ -267,15 +269,16 @@ theorem compile_correct_withPayload (hexternal : ExternalsRealized model) that falls through; `resultOf` of the recorded halt otherwise). -/ theorem compile_correct_eval (hexternal : ExternalsRealized model) {prog : YulSemantics.Block Op} {is : List Instr} - (hcomp : compile prog = some is) + (hcomp : compile prog imm = some is) {yst0 : EvmState} {V' : VEnv yulD} {yst' : EvmState} {o : Outcome} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) (hrun : YulSemantics.Run yulD prog yst0 V' yst' o) : ∃ b : Nat, ∀ s0 : State, FrameOK (assemble is) s0 → StateMatch yst0 s0 → s0.pc = UInt256.ofNat 0 → s0.stack = [] → b ≤ s0.gasAvailable → (o = .normal → Eval s0 .success) ∧ (o = .halt → ∃ hk, yst'.halted = some hk ∧ Eval s0 (resultOf hk)) := by - obtain ⟨b, H⟩ := compile_correct hexternal hcomp hrun + obtain ⟨b, H⟩ := compile_correct hexternal hcomp himm hrun refine ⟨b, ?_⟩ intro s0 hf hm hpc hstk hgas obtain ⟨s', hsteps, hcs', hm', hres⟩ := H s0 hf hm hpc hstk hgas diff --git a/YulEvmCompiler/LowerCorrect.lean b/YulEvmCompiler/LowerCorrect.lean index d0b9b679..389a07bf 100644 --- a/YulEvmCompiler/LowerCorrect.lean +++ b/YulEvmCompiler/LowerCorrect.lean @@ -43,12 +43,12 @@ set_option linter.unusedTactic false in set_option linter.unreachableTactic false in theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) {prog : List Asm} {is : List Instr} {payload : List UInt8} - (hlow : lowerProg prog = some is) (hsmall : codeSize prog < 256 ^ labelWidth) + (hlow : lowerProg imm prog = some is) (hsmall : codeSize prog < 256 ^ labelWidth) {a b : AConf} (hstep : AStep prog a b) (hsuf : a.code <:+ prog) (hcap : a.stk.length ≤ 1023) : - ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) prog is a s → + ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) imm prog is a s → bnd ≤ s.gasAvailable → - ∃ s', Steps s s' ∧ ConfMatch (payload := payload) prog is b s' + ∃ s', Steps s s' ∧ ConfMatch (payload := payload) imm prog is b s' ∧ s.gasAvailable - bnd ≤ s'.gasAvailable := by cases hstep with | @push v c σ yst => @@ -69,7 +69,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) hm.frame hm.smatch (by rw [hm.pc, hpos, hlenPre]) hm.stack (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) hgas - refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_⟩, hg'⟩ + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hlenPre] exact congrArg UInt256.ofNat (by @@ -77,6 +77,37 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) omega) · rw [hstk'] rfl + | @pushImmutable key c σ yst => + -- Identical to `push` except the width is pinned to 32, which is what makes + -- the immediate's byte position independent of the value stored there. + obtain ⟨pre, isPre, isI, isC, hsplit, hI, hC, hbytes, hlenPre, hsize⟩ := + locate hlow hsuf + obtain rfl : [Instr.push ⟨32, by norm_num⟩ (conv (imm key))] = isI := by + simpa [lowerInstr] using hI + refine ⟨40000, ?_⟩ + intro s hm hgas + have hpos : codeSize prog - codeSize (Asm.pushImmutable key :: c) = codeSize pre := by + rw [codeSize_cons] + omega + obtain ⟨s', hstep, hf', hsm', hpc', hstk', hg'⟩ := + pushStepU (w := ⟨32, by norm_num⟩) (u := conv (imm key)) + (hwf := by + show (conv (imm key)).toNat < 256 ^ 32 + rw [conv_toNat, show (256:Nat) ^ 32 = 2 ^ 256 by norm_num] + exact (imm key).isLt) + (pre := assembleBytes isPre) (post := assembleBytes isC ++ payload) + (assembleWithPayload_at₁ hbytes payload) + hm.frame hm.smatch + (by rw [hm.pc, hpos, hlenPre]) + hm.stack (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); omega) hgas + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ + · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) + rw [hpc', hlenPre] + exact congrArg UInt256.ofNat (by + simp only [Asm.size] at hsize ⊢ + omega) + · rw [hstk', ← hm.imms key] + rfl | @op yop args rets c σ yst yst' hstepOp => obtain ⟨pre, isPre, isI, isC, hsplit, hI, hC, hbytes, hlenPre, hsize⟩ := locate hlow hsuf @@ -97,7 +128,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) obtain ⟨s', hsteps, hf', hsm', hpc', hstk', hg'⟩ := H hm.frame hm.smatch hdec (by rw [hm.stack, mapStk_words]) hgas (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) - refine ⟨s', hsteps, ⟨hf', hsm', ?_, ?_⟩, hg'⟩ + refine ⟨s', hsteps, ⟨hf', hsm', ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hm.pc, hpos] have := hf'.codeSmall @@ -121,7 +152,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) obtain ⟨s', hsteps, hf', hsm', hpc', hstk', hg'⟩ := H hm.frame hm.smatch hdec (by rw [hm.stack, mapStk_words]) hgas (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) - refine ⟨s', hsteps, ⟨hf', hsm', ?_, ?_⟩, hg'⟩ + refine ⟨s', hsteps, ⟨hf', hsm', ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hm.pc, hpos] have := hf'.codeSmall @@ -151,7 +182,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) (by rw [hm.stack, mapStk_words]) (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) hgas obtain ⟨s', hstep, hf', hsm', hpc', hstk', hg'⟩ := hok - refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_⟩, hg'⟩ + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hlenPre] exact congrArg UInt256.ofNat (by @@ -180,7 +211,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) hm.frame hm.smatch (by rw [hm.pc, hpos, hlenPre]) hget (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) hgas - refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_⟩, hg'⟩ + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hlenPre] exact congrArg UInt256.ofNat (by @@ -212,7 +243,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) hm.frame hm.smatch (by rw [hm.pc, hpos, hlenPre]) hswap (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) hgas - refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, hstk'⟩, hg'⟩ + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, hstk', hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hlenPre] exact congrArg UInt256.ofNat (by @@ -234,7 +265,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) hm.frame hm.smatch (by rw [hm.pc, hpos, hlenPre]) (by rw [hm.stack]; rfl) (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) hgas - refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, hstk'⟩, hg'⟩ + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, hstk', hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hlenPre] exact congrArg UInt256.ofNat (by @@ -255,7 +286,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) (assembleWithPayload_at₁ hbytes payload) hm.frame hm.smatch (by rw [hm.pc, hpos, hlenPre]) (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) hgas - refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, by rw [hstk', hm.stack]⟩, hg'⟩ + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, by rw [hstk', hm.stack], hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hlenPre] exact congrArg UInt256.ofNat (by @@ -311,7 +342,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) (by rw [hpc2, hlenPreL]) (by simp only [hstk2, hm.stack, mapStk, List.length_map, List.length_cons, Operation.pushArity, Operation.popArity] at hcap ⊢; omega) (by omega) refine ⟨s3, .trans st1 (.trans st2 (.trans st3 (.refl _))), - ⟨hf3, hsm3, ?_, ?_⟩, gasChain₃' hg1 hg2 hg3⟩ + ⟨hf3, hsm3, ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, gasChain₃' hg1 hg2 hg3⟩ · show s3.pc = UInt256.ofNat (codeSize prog - codeSize c') rw [hpc3, hlenPreL] exact congrArg UInt256.ofNat (by omega) @@ -373,7 +404,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) (by rw [hpc2, hlenPreL]) (by simp only [hstk2, hm.stack, mapStk, List.length_map, List.length_cons, Operation.pushArity, Operation.popArity] at hcap ⊢; omega) (by omega) refine ⟨s3, .trans st1 (.trans st2 (.trans st3 (.refl _))), - ⟨hf3, hsm3, ?_, ?_⟩, gasChain₃' hg1 hg2 hg3⟩ + ⟨hf3, hsm3, ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, gasChain₃' hg1 hg2 hg3⟩ · show s3.pc = UInt256.ofNat (codeSize prog - codeSize c') rw [hpc3, hlenPreL] exact congrArg UInt256.ofNat (by omega) @@ -419,7 +450,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) hcond (by simp only [hstk1, hm.stack, mapStk, List.length_map, List.length_cons, Operation.pushArity, Operation.popArity] at hcap ⊢; omega) (by omega) - refine ⟨s2, .trans st1 (.trans st2 (.refl _)), ⟨hf2, hsm2, ?_, hstk2⟩, + refine ⟨s2, .trans st1 (.trans st2 (.refl _)), ⟨hf2, hsm2, ?_, hstk2, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, gasChain₂' hg1 hg2⟩ · show s2.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc2, List.length_append, Instr.length_bytes_push, hlenPre] @@ -450,7 +481,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) hm.frame hm.smatch (by rw [hm.pc, hpos, hlenPre]) hm.stack (by have hlen : s.stack.length ≤ 1023 := (by rw [hm.stack]; simp only [mapStk, List.length_map]; exact hcap); first | ((try simp only [Operation.pushArity, Operation.popArity]); omega) | (have := op_arity_bound o; omega)) hgas - refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_⟩, hg'⟩ + refine ⟨s', .trans hstep (.refl _), ⟨hf', hsm', ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, hg'⟩ · show s'.pc = UInt256.ofNat (codeSize prog - codeSize c) rw [hpc', hlenPre] exact congrArg UInt256.ofNat (by @@ -501,7 +532,7 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model) hf1 hsm1 (by rw [hpc1, hlenPreL]) (by simp only [hstk1, hm.stack, mapStk, List.length_map, List.length_cons, Operation.pushArity, Operation.popArity] at hcap ⊢; omega) (by omega) - refine ⟨s2, .trans st1 (.trans st2 (.refl _)), ⟨hf2, hsm2, ?_, ?_⟩, + refine ⟨s2, .trans st1 (.trans st2 (.refl _)), ⟨hf2, hsm2, ?_, ?_, hm.imms_step (by first | rfl | exact builtinWithExternal_immutable_eq hstepOp)⟩, gasChain₂' hg1 hg2⟩ · show s2.pc = UInt256.ofNat (codeSize prog - codeSize c') rw [hpc2, hlenPreL] @@ -599,10 +630,10 @@ set_option linter.unreachableTactic false in step. -/ theorem ahalt_sim [model : ExternalModel] {prog : List Asm} {is : List Instr} {payload : List UInt8} - (hlow : lowerProg prog = some is) + (hlow : lowerProg imm prog = some is) {a : AConf} {yst' : EvmState} (hstep : AHalt prog a yst') (hsuf : a.code <:+ prog) (hcap : a.stk.length ≤ 1023) : - ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) prog is a s → + ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) imm prog is a s → bnd ≤ s.gasAvailable → ∃ s', Steps s s' ∧ StateMatch yst' s' ∧ s'.callStack = [] ∧ HaltedMatch yst' s' := by @@ -648,12 +679,12 @@ theorem ahalt_sim [model : ExternalModel] /-- **Phase B, many steps**: bounds add along an Asm execution. -/ theorem asteps_sim [model : ExternalModel] (hexternal : ExternalsRealized model) {prog : List Asm} {is : List Instr} {payload : List UInt8} - (hlow : lowerProg prog = some is) (hsmall : codeSize prog < 256 ^ labelWidth) + (hlow : lowerProg imm prog = some is) (hsmall : codeSize prog < 256 ^ labelWidth) {a b : AConf} (hsteps : ASteps prog a b) (hsuf : a.code <:+ prog) (hbound : ∀ mid, ASteps prog a mid → mid.stk.length ≤ 1023) : - ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) prog is a s → + ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) imm prog is a s → bnd ≤ s.gasAvailable → - ∃ s', Steps s s' ∧ ConfMatch (payload := payload) prog is b s' + ∃ s', Steps s s' ∧ ConfMatch (payload := payload) imm prog is b s' ∧ s.gasAvailable - bnd ≤ s'.gasAvailable := by induction hsteps with | refl a => @@ -671,12 +702,12 @@ theorem asteps_sim [model : ExternalModel] (hexternal : ExternalsRealized model) EVM execution ending in the matching halted state. -/ theorem arun_halt_sim [model : ExternalModel] (hexternal : ExternalsRealized model) {prog : List Asm} {is : List Instr} {payload : List UInt8} - (hlow : lowerProg prog = some is) (hsmall : codeSize prog < 256 ^ labelWidth) + (hlow : lowerProg imm prog = some is) (hsmall : codeSize prog < 256 ^ labelWidth) {a b : AConf} {yst' : EvmState} (hsteps : ASteps prog a b) (hhalt : AHalt prog b yst') (hsuf : a.code <:+ prog) (hbound : ∀ mid, ASteps prog a mid → mid.stk.length ≤ 1023) : - ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) prog is a s → + ∃ bnd : Nat, ∀ s : State, ConfMatch (payload := payload) imm prog is a s → bnd ≤ s.gasAvailable → ∃ s', Steps s s' ∧ StateMatch yst' s' ∧ s'.callStack = [] ∧ HaltedMatch yst' s' := by diff --git a/YulEvmCompiler/LowerDefs.lean b/YulEvmCompiler/LowerDefs.lean index 4a281d2e..1783cdd0 100644 --- a/YulEvmCompiler/LowerDefs.lean +++ b/YulEvmCompiler/LowerDefs.lean @@ -7,7 +7,7 @@ set_option warningAsError true **Phase B**: the generic simulation from the Asm semantics down to the EVM semantics of the lowered bytecode. -Fixing a program `prog` with `lowerProg prog = some is`, every reachable +Fixing a program `prog` with `lowerProg imm prog = some is`, every reachable Asm configuration `⟨c, σ, yst⟩` (its code a suffix of `prog`) corresponds to EVM states `s` with @@ -107,6 +107,7 @@ theorem AStep.stkOK [model : ExternalModel] {prog : List Asm} {a b : AConf} (h : AStep prog a b) (ha : StkOK prog a.stk) : StkOK prog b.stk := by cases h with | push => exact ha.cons_word + | pushImmutable => exact ha.cons_word | op _ => exact (ha.append_right).words_append _ | @dup n v τ ρ c yst _ => intro l hl @@ -155,18 +156,18 @@ def assembleWithPayload (is : List Instr) (payload : List UInt8) : ByteArray := decompose around `i`'s lowering, with the prefix's byte length equal to the suffix's byte position. -/ theorem locate {prog : List Asm} {is : List Instr} - (hlow : lowerProg prog = some is) {i : Asm} {c : List Asm} + (hlow : lowerProg imm prog = some is) {i : Asm} {c : List Asm} (hsuf : (i :: c) <:+ prog) : ∃ (pre : List Asm) (isPre isI isC : List Instr), prog = pre ++ i :: c - ∧ lowerInstr prog i = some isI - ∧ lowerFrag prog c = some isC + ∧ lowerInstr imm prog i = some isI + ∧ lowerFrag imm prog c = some isC ∧ assembleBytes is = assembleBytes isPre ++ assembleBytes isI ++ assembleBytes isC ∧ (assembleBytes isPre).length = codeSize pre ∧ codeSize prog = codeSize pre + i.size + codeSize c := by obtain ⟨pre, hpre⟩ := hsuf - have hlow' : lowerFrag prog (pre ++ i :: c) = some is := by + have hlow' : lowerFrag imm prog (pre ++ i :: c) = some is := by rw [hpre]; exact hlow obtain ⟨isPre, isRest, h1, h2, rfl⟩ := lowerFrag_append hlow' obtain ⟨isI, isC, hI, hC, rfl⟩ := lowerFrag_cons h2 @@ -179,7 +180,7 @@ theorem locate {prog : List Asm} {is : List Instr} the position accounts for the suffix, the lowered bytes decompose at the label's `JUMPDEST`, and that `JUMPDEST` passes the jumpdest analysis. -/ theorem locate_label {prog : List Asm} {is : List Instr} - (hlow : lowerProg prog = some is) {l : Label} {c' : List Asm} + (hlow : lowerProg imm prog = some is) {l : Label} {c' : List Asm} (hfind : findLabel l prog = some c') : ∃ (a : Nat) (isPreL isC' : List Instr), resolve l prog = some a @@ -217,7 +218,7 @@ theorem locate_label {prog : List Asm} {is : List Instr} object bytecode image. Appending a payload cannot change decoding at a label inside the lowered executable prefix. -/ theorem locate_label_withPayload {prog : List Asm} {is : List Instr} - (hlow : lowerProg prog = some is) {l : Label} {c' : List Asm} + (hlow : lowerProg imm prog = some is) {l : Label} {c' : List Asm} (hfind : findLabel l prog = some c') (payload : List UInt8) : ∃ (a : Nat) (isPreL isC' : List Instr), resolve l prog = some a @@ -287,12 +288,32 @@ theorem exchange_swap {α : Type} (x y : α) (τ ρ : List α) : /-- The phase-B invariant between an Asm configuration and an EVM state running the lowered bytecode. -/ -structure ConfMatch (prog : List Asm) (is : List Instr) (a : AConf) - (s : State) (payload : List UInt8 := []) : Prop where +structure ConfMatch (imm : String → U256) (prog : List Asm) (is : List Instr) + (a : AConf) (s : State) (payload : List UInt8 := []) : Prop where frame : FrameOK (assembleWithPayload is payload) s smatch : StateMatch a.yst s pc : s.pc = UInt256.ofNat (codeSize prog - codeSize a.code) stack : s.stack = mapStk prog a.stk + /-- The assignment the emitted bytes were lowered against is the one the + environment records. + + This is the compiler's *layout-consistency* obligation for immutables — the + exact counterpart of `Layout.Consistent` for data segments. Phase A does not + carry it (`AStep.pushImmutable` pushes the environment's value, so the source + built-in is matched regardless), which keeps the burden here, where the + emitted bytes actually exist. It survives a whole run because no step ever + writes `env.immutable` (`AStep.immutable_eq`). -/ + imms : ∀ key, imm key = a.yst.env.immutable (YulSemantics.EVM.litValue (.string key)) + +/-- Transport the immutable layout-consistency obligation across a step. -/ +theorem ConfMatch.imms_step {imm : String → U256} {prog : List Asm} {is : List Instr} + {payload : List UInt8} {a : AConf} {s : State} {yst' : EvmState} + (hm : ConfMatch (payload := payload) imm prog is a s) + (h : yst'.env.immutable = a.yst.env.immutable) : + ∀ key, imm key = yst'.env.immutable (YulSemantics.EVM.litValue (.string key)) := by + intro key + rw [h] + exact hm.imms key /-! ### Open-world call and creation realization @@ -736,7 +757,7 @@ theorem ExternalsRealized.insufficientBalanceCall : /-- The lowered program's byte size is `codeSize prog` (bounded by the frame invariant). -/ theorem codeSize_lt {prog : List Asm} {is : List Instr} {payload : List UInt8} - (hlow : lowerProg prog = some is) {s : State} + (hlow : lowerProg imm prog = some is) {s : State} (hf : FrameOK (assembleWithPayload is payload) s) : codeSize prog < 2 ^ 256 := by have h := hf.codeSmall rw [assembleWithPayload, size_mkCode, List.length_append, diff --git a/YulEvmCompiler/ObjectCompile.lean b/YulEvmCompiler/ObjectCompile.lean index ccfc90e6..685b45bb 100644 --- a/YulEvmCompiler/ObjectCompile.lean +++ b/YulEvmCompiler/ObjectCompile.lean @@ -64,6 +64,9 @@ structure ObjectPlan where subObjects : List ObjectPlan dataSegs : List (String × Data) entries : List ObjectEntry + /-- Byte offsets of this object's immutable placeholders, relative to the + start of its own bytecode — what a parent's `setimmutable` patches. -/ + immOffsets : List (String × Nat) bytecode : List UInt8 deriving Repr @@ -141,6 +144,61 @@ mutual (← resolveObjectCases resolve cases) end +/-! ### `setimmutable` + +`setimmutable(base, name, value)` writes `value` into the in-memory copy of the +deployed code that the constructor is about to return, at every position where +that code reads the immutable. Those positions are exactly the placeholder +offsets the child's plan recorded, so the call is *eliminable*: it expands to one +ordinary `mstore` per offset and nothing about it survives into the backend. + +Yul evaluates arguments right to left, so `value` is bound before `base`; the +generated names are `$imm$` prefixed, which no source identifier can be. -/ + +private def immValName : String := "$imm$value" +private def immBaseName : String := "$imm$base" + +/-- The `mstore` for one placeholder offset. -/ +private def setImmutableStore (offset : Nat) : YulSemantics.Stmt Op := + .exprStmt (.builtin .mstore + [.builtin .add [.var immBaseName, .lit (.number offset)], .var immValName]) + +/-- Expand `setimmutable(base, name, value)` against the recorded offsets. -/ +private def expandSetImmutable (offsets : List (String × Nat)) (name : String) + (base value : YulSemantics.Expr Op) : YulSemantics.Stmt Op := + .block ((.letDecl [immValName] (some value)) :: + (.letDecl [immBaseName] (some base)) :: + ((offsets.filter (fun p => p.1 == name)).map (fun p => setImmutableStore p.2))) + +/-- Rewrite every `setimmutable` in a code block against the recorded offsets. +Run *before* layout resolution, so the resolver and its semantic-preservation +proof never see the extension. -/ +partial def expandSetImmutablesStmts (offsets : List (String × Nat)) + (ambiguous : List String) : + List (YulSemantics.Stmt Op) → List (YulSemantics.Stmt Op) + | [] => [] + | stmt :: rest => + let tail := expandSetImmutablesStmts offsets ambiguous rest + match stmt with + | .exprStmt (.call "setimmutable" [base, .lit (.string name), value]) => + -- An ambiguous name is left as the raw call, so the backend rejects + -- the program. Expanding it to no stores would be just as wrong as + -- expanding it to the wrong ones — the immutable would stay zero. + if ambiguous.contains name then stmt :: tail + else expandSetImmutable offsets name base value :: tail + | .block body => .block (expandSetImmutablesStmts offsets ambiguous body) :: tail + | .funDef n ps rs body => + .funDef n ps rs (expandSetImmutablesStmts offsets ambiguous body) :: tail + | .cond c body => .cond c (expandSetImmutablesStmts offsets ambiguous body) :: tail + | .switch c cases dflt => + .switch c (cases.map (fun cb => (cb.1, expandSetImmutablesStmts offsets ambiguous cb.2))) + (dflt.map (expandSetImmutablesStmts offsets ambiguous)) :: tail + | .forLoop init c post body => + .forLoop (expandSetImmutablesStmts offsets ambiguous init) c + (expandSetImmutablesStmts offsets ambiguous post) + (expandSetImmutablesStmts offsets ambiguous body) :: tail + | other => other :: tail + private def placeholderResolver : RefResolver := fun _ => some (0, 0) /-- A partial planning resolver agrees with the total maps exposed by a @@ -482,16 +540,20 @@ private def planAttempt (name : String) (code : List (YulSemantics.Stmt Op)) let plan : ObjectPlan := { name, codeBlock := code, codeSize := c, size, subObjects := subPlans, dataSegs entries := { name, offset := 0, size } :: children ++ dataLayout + immOffsets := [] bytecode := [] } let resolvedCode ← resolveObjectStmts (planResolver plan) code + let resolvedAsm ← compileAsm resolvedCode let resolvedInstructions ← compile resolvedCode let executable := assembleBytes resolvedInstructions let c' := executable.length if c' == c then let childBytecode := (subPlans.map (·.bytecode)).flatten let bytecode := executable ++ [0] ++ childBytecode ++ dataRegion dataSegs - if bytecode.length == size then some (.inl { plan with bytecode }) else none + if bytecode.length == size then + some (.inl { plan with bytecode, immOffsets := immutableOffsets resolvedAsm 0 }) + else none else some (.inr c') else @@ -556,6 +618,12 @@ private def layoutOfPlan (plan : ObjectPlan) : Layout := { dataSize := entryMap (·.size) plan.entries } +/-- The immutable placeholder offsets of an object's own compiled code, for a +caller that needs to patch them (`setimmutable`). `none` when the object does +not plan. -/ +def objectImmutableOffsets (o : Object Op) : Option (List (String × Nat)) := + (planObject o).map (·.immOffsets) + /-- Compile a complete object tree to executable EVM bytecode plus real object-layout maps. References are actual offsets/sizes in the emitted bytes, not Solidity's synthetic AST-interpreter values. -/ @@ -689,6 +757,7 @@ private theorem planAttempt_spec split at h · rename_i hsmall obtain ⟨resolvedCode, hresolvedCode, h⟩ := Option.bind_eq_some_iff.mp h + obtain ⟨resolvedAsm, -, h⟩ := Option.bind_eq_some_iff.mp h obtain ⟨resolvedInstructions, hresolvedInstr, h⟩ := Option.bind_eq_some_iff.mp h split at h · rename_i hcc @@ -885,6 +954,7 @@ def planAttemptWith (compileFn : YulSemantics.Block Op → Option (List Instr)) let plan : ObjectPlan := { name, codeBlock := code, codeSize := c, size, subObjects := subPlans, dataSegs entries := { name, offset := 0, size } :: children ++ dataLayout + immOffsets := [] bytecode := [] } let resolvedCode ← resolveObjectStmts (planResolver plan) code @@ -894,7 +964,9 @@ def planAttemptWith (compileFn : YulSemantics.Block Op → Option (List Instr)) if c' == c then let childBytecode := (subPlans.map (·.bytecode)).flatten let bytecode := executable ++ [0] ++ childBytecode ++ dataRegion dataSegs - if bytecode.length == size then some (.inl { plan with bytecode }) else none + if bytecode.length == size then + some (.inl { plan with bytecode }) + else none else some (.inr c') else @@ -942,6 +1014,19 @@ def compileResolvedObjectWith if !(plan.entries.map entryKey).Nodup then none else some (layoutOfPlan plan) +/-- The object layer records no immutable values: it compiles placeholders as +zeros, and the layout it publishes reports the same. The deploying constructor +is what patches real values into the emitted bytes. -/ +theorem compileObject_immutable {o : Object Op} {L : Layout} + (h : compileObject o = some L) : L.immutable = fun _ => 0 := by + simp only [compileObject, compileResolvedObject, Option.bind_eq_bind] at h + obtain ⟨plan, -, h⟩ := Option.bind_eq_some_iff.mp h + split at h + · cases h + · simp only [Option.some.injEq] at h + subst h + rfl + /-- Public data-placement theorem for `compileObject`. -/ theorem compileObject_consistent {o : Object Op} {L : Layout} (h : compileObject o = some L) : L.Consistent o := @@ -987,7 +1072,13 @@ theorem compileObject_correct (hexternal : ExternalsRealized model) rw [hresolved] exact hrun obtain ⟨bound, hsim⟩ := - compile_correct_withPayload hexternal (payload := payload) hinstructions hrun' + compile_correct_withPayload hexternal (payload := payload) hinstructions + -- the object layer compiles against the all-zero assignment and records the + -- same map on the layout, so the two agree definitionally + (fun key => by + rw [show L.initState.env.immutable = L.immutable from rfl, + compileObject_immutable hcomp] + rfl) hrun' refine ⟨bound, ?_⟩ intro s0 hframe hmatch hpc hstack hgas apply hsim s0 diff --git a/YulEvmCompiler/Optimizer/Implementation/MemorySpillBackendSound.lean b/YulEvmCompiler/Optimizer/Implementation/MemorySpillBackendSound.lean index 717a7ac8..ae930566 100644 --- a/YulEvmCompiler/Optimizer/Implementation/MemorySpillBackendSound.lean +++ b/YulEvmCompiler/Optimizer/Implementation/MemorySpillBackendSound.lean @@ -56,6 +56,8 @@ theorem compile_spilled_correct result.base result.reserved) (hcomp : compile (resolveForLayoutStmts L result.block) = some instructions) + (himm : ∀ key, (0 : YulSemantics.EVM.U256) = + L.initState.env.immutable (YulSemantics.EVM.litValue (.string key))) {sourceEnv : WordEnv} {sourceFinal : EvmState} {out : Outcome} (hsource : Run (G result.base result.reserved) (resolveForLayoutStmts L @@ -81,7 +83,7 @@ theorem compile_spilled_correct have hobs : runObservables L.initState sourceFinal = runObservables L.initState targetFinal := ScratchRel.runObservables_eq hscratch - obtain ⟨bound, hbackend⟩ := compile_correct hexternal hcomp htarget + obtain ⟨bound, hbackend⟩ := compile_correct hexternal hcomp himm htarget exact ⟨targetEnv, targetFinal, htarget, hscratch, hobs, bound, hbackend⟩ /-- Generic object backend composition for an already established plan-node diff --git a/YulEvmCompiler/Optimizer/Implementation/MemorySpillSound.lean b/YulEvmCompiler/Optimizer/Implementation/MemorySpillSound.lean index 3575787c..e4f90746 100644 --- a/YulEvmCompiler/Optimizer/Implementation/MemorySpillSound.lean +++ b/YulEvmCompiler/Optimizer/Implementation/MemorySpillSound.lean @@ -142,6 +142,8 @@ theorem compile_spilled_correct result.base result.reserved) (hcomp : compile (resolveForLayoutStmts L result.block) = some instructions) + (himm : ∀ key, (0 : YulSemantics.EVM.U256) = + L.initState.env.immutable (YulSemantics.EVM.litValue (.string key))) {sourceEnv : MemorySpillObjectSound.WordEnv} {sourceFinal : EvmState} {out : Outcome} (hsource : Run @@ -167,7 +169,7 @@ theorem compile_spilled_correct (out = .halt ∧ HaltedMatch targetFinal s')) := MemorySpillBackendSound.compile_spilled_correct hexternal (spillNodeRunSound (calls := model.calls) (creates := model.creates) L) - hfacts hguarded hcomp hsource + hfacts hguarded hcomp himm hsource /-- Direct production block-root composition from a successful spill choice through ordinary Yul compilation and the verified EVM backend. -/ @@ -177,8 +179,10 @@ theorem compile_memorySpill_correct (hspill : spillBlock? raw = some result) (hguarded : GuardedExternals model.calls model.creates result.base result.reserved) - (hcomp : compile result.block = some instructions) + (hcomp : compile result.block imm = some instructions) {initial sourceFinal : EvmState} + (himm : ∀ key, imm key = + initial.env.immutable (YulSemantics.EVM.litValue (.string key))) {sourceEnv : MemorySpillObjectSound.WordEnv} {out : Outcome} (hsource : Run (guardedEvm model.calls model.creates result.base result.reserved) @@ -205,7 +209,7 @@ theorem compile_memorySpill_correct have hobs : runObservables initial sourceFinal = runObservables initial targetFinal := ScratchRel.runObservables_eq hscratch - obtain ⟨bound, hbackend⟩ := compile_correct hexternal hcomp htarget + obtain ⟨bound, hbackend⟩ := compile_correct hexternal hcomp himm htarget exact ⟨targetEnv, targetFinal, htarget, hscratch, hobs, bound, hbackend⟩ /-- Concrete production object theorem with recursive spill/fallback soundness diff --git a/YulEvmCompiler/Optimizer/Spec/Backend.lean b/YulEvmCompiler/Optimizer/Spec/Backend.lean index 9c858111..858b59c7 100644 --- a/YulEvmCompiler/Optimizer/Spec/Backend.lean +++ b/YulEvmCompiler/Optimizer/Spec/Backend.lean @@ -40,8 +40,9 @@ the end-to-end statement that optimizing before compiling is correct. -/ theorem LocalPass.optimize_then_compile_correct (P : LocalPass yulD) (hexternal : ExternalsRealized model) {prog : Block Op} {is : List Instr} - (hcomp : compile (P.run prog) = some is) + (hcomp : compile (P.run prog) imm = some is) {yst0 : EvmState} {V' : VEnv yulD} {yst' : EvmState} {o : Outcome} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) (hrun : Run yulD prog yst0 V' yst' o) : ∃ b : Nat, ∀ s0 : State, FrameOK (assemble is) s0 → StateMatch yst0 s0 → @@ -49,6 +50,6 @@ theorem LocalPass.optimize_then_compile_correct ∃ s', Steps s0 s' ∧ s'.callStack = [] ∧ StateMatch yst' s' ∧ ((o = .normal ∧ s'.halt = .Success ∧ s'.hReturn = .empty) ∨ (o = .halt ∧ HaltedMatch yst' s')) := - compile_correct hexternal hcomp (P.run_optimized hrun) + compile_correct hexternal hcomp himm (P.run_optimized hrun) end YulEvmCompiler.Optimizer diff --git a/YulEvmCompiler/Optimizer/Spec/EvmBackend.lean b/YulEvmCompiler/Optimizer/Spec/EvmBackend.lean index b730fed8..ac7467c3 100644 --- a/YulEvmCompiler/Optimizer/Spec/EvmBackend.lean +++ b/YulEvmCompiler/Optimizer/Spec/EvmBackend.lean @@ -38,13 +38,16 @@ call/create responses are realized, every accepted program, and every source run, the emitted bytecode simulates the run from every matching initial state with enough gas. -/ def EvmBackend.Correct - (compileFn : YulSemantics.Block Op → Option (List Instr)) : Prop := + (compileFn : YulSemantics.Block Op → + (String → YulSemantics.EVM.U256) → Option (List Instr)) : Prop := ∀ (model : ExternalModel), ExternalsRealized model → - ∀ {prog : YulSemantics.Block Op} {is : List Instr}, - compileFn prog = some is → + ∀ {imm : String → YulSemantics.EVM.U256} + {prog : YulSemantics.Block Op} {is : List Instr}, + compileFn prog imm = some is → ∀ {yst0 : EvmState} {V' : VEnv (evmWithExternal model.calls model.creates)} {yst' : EvmState} {o : Outcome}, + (∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) → Run (evmWithExternal model.calls model.creates) prog yst0 V' yst' o → ∃ b : Nat, ∀ s0 : State, FrameOK (assemble is) s0 → StateMatch yst0 s0 → @@ -59,17 +62,18 @@ compiler — the same by-construction discipline as `Optimizer.LocalPass`. -/ structure EvmBackend where /-- The compilation function (`Option`-valued: rejection, never miscompilation). -/ - compile : YulSemantics.Block Op → Option (List Instr) + compile : YulSemantics.Block Op → + (String → YulSemantics.EVM.U256) → Option (List Instr) /-- The proof obligation: the `compile_correct` statement shape. -/ correct : EvmBackend.Correct compile /-- The classic labeled-assembly backend as an `EvmBackend`: the `correct` field is exactly `compile_correct`. -/ def EvmBackend.classic : EvmBackend where - compile := YulEvmCompiler.compile + compile := fun prog imm => YulEvmCompiler.compile prog imm correct := by - intro model hext prog is hcomp yst0 V' yst' o hrun - exact compile_correct hext hcomp hrun + intro model hext imm prog is hcomp yst0 V' yst' o himm hrun + exact compile_correct hext hcomp himm hrun section Compose @@ -84,8 +88,9 @@ apply the backend's own correctness. -/ theorem LocalPass.optimize_then_backend_correct (B : EvmBackend) (P : LocalPass yulD) (hexternal : ExternalsRealized model) {prog : YulSemantics.Block Op} {is : List Instr} - (hcomp : B.compile (P.run prog) = some is) + (hcomp : B.compile (P.run prog) imm = some is) {yst0 : EvmState} {V' : VEnv yulD} {yst' : EvmState} {o : Outcome} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) (hrun : Run yulD prog yst0 V' yst' o) : ∃ b : Nat, ∀ s0 : State, FrameOK (assemble is) s0 → StateMatch yst0 s0 → @@ -93,7 +98,7 @@ theorem LocalPass.optimize_then_backend_correct ∃ s', Steps s0 s' ∧ s'.callStack = [] ∧ StateMatch yst' s' ∧ ((o = .normal ∧ s'.halt = .Success ∧ s'.hReturn = .empty) ∨ (o = .halt ∧ HaltedMatch yst' s')) := - B.correct model hexternal hcomp (P.run_optimized hrun) + B.correct model hexternal hcomp himm (P.run_optimized hrun) end Compose diff --git a/YulEvmCompiler/Optimizer/Spec/Observe.lean b/YulEvmCompiler/Optimizer/Spec/Observe.lean index 9d5f84b7..1f61b9a8 100644 --- a/YulEvmCompiler/Optimizer/Spec/Observe.lean +++ b/YulEvmCompiler/Optimizer/Spec/Observe.lean @@ -212,8 +212,9 @@ tier exists to express. -/ theorem optimize_then_compile_correct [model : ExternalModel] (hexternal : ExternalsRealized model) (P : ObsPass) {prog : Block Op} {is : List Instr} - (hcomp : compile (P.run prog) = some is) + (hcomp : compile (P.run prog) imm = some is) {yst0 : EvmState} {V' : VEnv (evmWithExternal model.calls model.creates)} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) {yst' : EvmState} {o : Outcome} (hrun : Run (evmWithExternal model.calls model.creates) prog yst0 V' yst' o) : ∃ V₂ yst₂, @@ -227,7 +228,7 @@ theorem optimize_then_compile_correct (o = .halt ∧ HaltedMatch yst₂ s')) := by obtain ⟨V₂, yst₂, hrun₂, hobs⟩ := (P.sound model.calls model.creates prog).1 yst0 V' yst' o hrun - exact ⟨V₂, yst₂, hrun₂, hobs, compile_correct hexternal hcomp hrun₂⟩ + exact ⟨V₂, yst₂, hrun₂, hobs, compile_correct hexternal hcomp himm hrun₂⟩ end ObsPass diff --git a/YulEvmCompiler/SimAsm.lean b/YulEvmCompiler/SimAsm.lean index aba226fd..c34ec68a 100644 --- a/YulEvmCompiler/SimAsm.lean +++ b/YulEvmCompiler/SimAsm.lean @@ -322,6 +322,17 @@ theorem ASimEHalt.extend {prog : List Asm} {yst yst' : EvmState} rw [List.append_assoc] exact hsteps +/-- The placeholder simulates a `loadimmutable` read: the Asm step pushes the +value the environment records for the key, which is exactly what the source +built-in produces. Nothing about the compile-time assignment is needed here — +that agreement is phase B's `ConfMatch.imms`. -/ +theorem asimE_pushImmutable {prog : List Asm} {yst : EvmState} {V : VEnv yulD} + {off : Nat} {key : String} : + ASimE prog yst V off [.pushImmutable key] + [yst.env.immutable (YulSemantics.EVM.litValue (.string key))] yst := by + intro pre c τ σ hp hτ + exact ASteps.single (by rw [hp]; exact AStep.pushImmutable) + /-- The built-in step, non-halting: consume the argument words (which sit as the innermost temporaries), push the results. -/ theorem asimE_op {prog : List Asm} {yst yst1 yst2 : EvmState} @@ -1640,13 +1651,17 @@ private theorem expr_var_inv {Φ : FMap} {Γ : List Ident} {off n : Nat} private theorem expr_builtin_inv {Φ : FMap} {Γ : List Ident} {off n : Nat} {op : Op} {args : List (Expr Op)} {asm : List Asm} {n' : Nat} + (hnotImm : ∀ key, ¬ (op = .loadimmutable ∧ args = [.lit (.string key)])) (h : compileExpr Φ Γ off n (.builtin op args) = some (asm, n')) : ∃ argCode, compileArgs Φ Γ off n args = some (argCode, n') ∧ asm = argCode ++ [.op op] := by - simp only [compileExpr, Option.bind_eq_bind] at h - obtain ⟨⟨argCode, n1⟩, hargs, h2⟩ := Option.bind_eq_some_iff.mp h - simp only [Option.some.injEq, Prod.mk.injEq] at h2 - exact ⟨argCode, h2.2 ▸ hargs, h2.1.symm⟩ + simp only [compileExpr] at h + split at h + · exact absurd ⟨rfl, rfl⟩ (hnotImm _) + · simp only [Option.bind_eq_bind] at h + obtain ⟨⟨argCode, n1⟩, hargs, h2⟩ := Option.bind_eq_some_iff.mp h + simp only [Option.some.injEq, Prod.mk.injEq] at h2 + exact ⟨argCode, h2.2 ▸ hargs, h2.1.symm⟩ private theorem expr_call_inv {Φ : FMap} {Γ : List Ident} {off n : Nat} {f : Ident} {args : List (Expr Op)} {asm : List Asm} {n' : Nat} @@ -2347,17 +2362,46 @@ theorem sim {prog : List Asm} (hnodup : (labelDefs prog).Nodup) intro Φ off n asm n' hc hΦ obtain ⟨idx, h16, hidx, rfl, rfl⟩ := expr_var_inv hc exact asimE_var h16 hget hidx - | builtinOk hargs hb ihargs => + | @builtinOk funs0 V0 st yop args0 argvals st1 rets st2 hargs hb ihargs => intro Φ off n asm n' hc hΦ - obtain ⟨argCode, hargs', rfl⟩ := expr_builtin_inv hc - exact asimE_op ((ihargs Φ off n argCode n' hargs').2 hΦ) hb + by_cases himm : ∃ key, yop = .loadimmutable ∧ args0 = [.lit (.string key)] + · obtain ⟨key, rfl, rfl⟩ := himm + -- `loadimmutable` is an ordinary environment read: the argument list is + -- the key's literal, the state is untouched, and the result is the map's + -- entry — exactly what the placeholder's `AStep` produces. + obtain ⟨rfl, rfl⟩ : [Asm.pushImmutable key] = asm ∧ n = n' := by + simpa [compileExpr] using hc + obtain ⟨rfl, rfl⟩ : argvals = [YulSemantics.EVM.litValue (.string key)] ∧ st = st1 := by + cases hargs with + | argsCons hrest hhead => + cases hrest + cases hhead + exact ⟨rfl, rfl⟩ + simp only [YulSemantics.EVM.builtinWithExternal, YulSemantics.EVM.stepOp, + YulSemantics.EVM.rd1, Option.some.injEq] at hb + obtain ⟨rfl, rfl⟩ := hb + exact asimE_pushImmutable + · obtain ⟨argCode, hargs', rfl⟩ := + expr_builtin_inv (fun key hk => himm ⟨key, hk.1, hk.2⟩) hc + exact asimE_op ((ihargs Φ off n argCode n' hargs').2 hΦ) hb | builtinHalt hargs hb ihargs => intro Φ off n asm n' hc hΦ - obtain ⟨argCode, hargs', rfl⟩ := expr_builtin_inv hc + obtain ⟨argCode, hargs', rfl⟩ := expr_builtin_inv (by + rintro key ⟨rfl, rfl⟩ + -- an environment read never halts + rename_i argvals _ _ + rcases argvals with _ | ⟨a, _ | ⟨b, rest⟩⟩ <;> + simp_all [YulSemantics.EVM.builtinWithExternal, YulSemantics.EVM.stepOp, + YulSemantics.EVM.rd1]) hc exact asimE_opHalt ((ihargs Φ off n argCode n' hargs').2 hΦ) hb | builtinArgsHalt hargs ihargs => intro Φ off n asm n' hc hΦ - obtain ⟨argCode, hargs', rfl⟩ := expr_builtin_inv hc + obtain ⟨argCode, hargs', rfl⟩ := expr_builtin_inv (by + rintro key ⟨rfl, rfl⟩ + -- evaluating a single string literal cannot halt + cases hargs with + | argsRestHalt hh => cases hh + | argsHeadHalt _ hh => cases hh) hc exact (ihargs Φ off n argCode n' hargs' hΦ).extend _ | callOk hargs hlk harity hbody ho ihargs ihbody => rename_i funs0 V0 st0 fn args0 argvals st1 decl cenv Vend st2 o diff --git a/YulEvmCompiler/SsaCfg/Implementation/Compile.lean b/YulEvmCompiler/SsaCfg/Implementation/Compile.lean index be28c966..e16ec9a8 100644 --- a/YulEvmCompiler/SsaCfg/Implementation/Compile.lean +++ b/YulEvmCompiler/SsaCfg/Implementation/Compile.lean @@ -34,16 +34,16 @@ open YulSemantics.EVM (Op) /-- Emit one SSA program through the shared final gates: `ToAsm` (in the given scheduling mode), `Asm` well-formedness, the peephole, the overflow certificate, label resolution. -/ -def finishProgOrd (ord : Bool) (P : Prog) : Option (List YulEvmCompiler.Instr) := do +def finishProgOrd (imm : String → YulSemantics.EVM.U256) (ord : Bool) (P : Prog) : Option (List YulEvmCompiler.Instr) := do let asm ← ToAsm.emitProgOrd ord P if !wfCheck asm then none else let opt := optimizeAsm asm - if stackOK2 opt then lowerProg opt else none + if stackOK2 opt then lowerProg imm opt else none /-- `finishProgOrd` in the default mode (kept for the correctness statements' vocabulary). -/ -def finishProg (P : Prog) : Option (List YulEvmCompiler.Instr) := - finishProgOrd false P +def finishProg (imm : String → YulSemantics.EVM.U256) (P : Prog) : Option (List YulEvmCompiler.Instr) := + finishProgOrd imm false P /-! ## Static cost — candidate selection @@ -140,15 +140,16 @@ dominance gate, then four candidates — {optimized, raw} × {next-use scheduling, plain} — with the statically cheapest artifact winning. Each candidate passes the full gate chain independently, so the choice is only ever among independently checked artifacts. -/ -def compileViaSsa (prog : YulSemantics.Block Op) : +def compileViaSsa (prog : YulSemantics.Block Op) + (imm : String → YulSemantics.EVM.U256 := YulEvmCompiler.unpatchedImmutables) : Option (List YulEvmCompiler.Instr) := do let P ← ofBlock prog -- dominance gate: the SSA passes are sound only on programs whose uses -- are dominated by their definitions (see `ToAsm.Prog.domCheck`) if !(ToAsm.Prog.domCheck P) then none else let Popt := optimizeProg P - let cands := [finishProgOrd true Popt, finishProgOrd false Popt, - finishProgOrd true P, finishProgOrd false P] + let cands := [finishProgOrd imm true Popt, finishProgOrd imm false Popt, + finishProgOrd imm true P, finishProgOrd imm false P] cands.foldl (pickMin instrCost) none end YulEvmCompiler.SsaCfg diff --git a/YulEvmCompiler/SsaCfg/Implementation/Object.lean b/YulEvmCompiler/SsaCfg/Implementation/Object.lean index c3b3941c..84fab63f 100644 --- a/YulEvmCompiler/SsaCfg/Implementation/Object.lean +++ b/YulEvmCompiler/SsaCfg/Implementation/Object.lean @@ -19,6 +19,6 @@ open YulSemantics.EVM (Op) /-- Compile a full object tree with the SSA backend on every code block. -/ def compileObjectViaSsa (o : Object Op) : Option YulSemantics.EVM.Layout := - compileResolvedObjectWith compileViaSsa o + compileResolvedObjectWith (compileViaSsa) o end YulEvmCompiler.SsaCfg diff --git a/YulEvmCompiler/SsaCfg/Implementation/ToAsmSound.lean b/YulEvmCompiler/SsaCfg/Implementation/ToAsmSound.lean index dfeed324..d6df3626 100644 --- a/YulEvmCompiler/SsaCfg/Implementation/ToAsmSound.lean +++ b/YulEvmCompiler/SsaCfg/Implementation/ToAsmSound.lean @@ -478,6 +478,9 @@ theorem findLabel_elideJumps (l : Label) (p : List Asm) : omit model in @[simp] theorem elideJumps_push (v : U256) (c : List Asm) : elideJumps (Asm.push v :: c) = Asm.push v :: elideJumps c := by simp [elideJumps] +omit model in @[simp] theorem elideJumps_pushImmutable (key : String) (c : List Asm) : + elideJumps (Asm.pushImmutable key :: c) = Asm.pushImmutable key :: elideJumps c := by + simp [elideJumps] omit model in @[simp] theorem elideJumps_op (yop : Op) (c : List Asm) : elideJumps (Asm.op yop :: c) = Asm.op yop :: elideJumps c := by simp [elideJumps] omit model in @[simp] theorem elideJumps_dup (n : Fin 16) (c : List Asm) : @@ -512,6 +515,9 @@ theorem astep_elideJumps {prog : List Asm} (hnodup : (labelDefs prog).Nodup) cases h with | @push v c σ yst => simp only [elideConf, ToAsm.elideJumps_push]; exact ASteps.single AStep.push + | @pushImmutable key c σ yst => + simp only [elideConf, ToAsm.elideJumps_pushImmutable] + exact ASteps.single AStep.pushImmutable | @op yop args rets c σ yst yst' hb => simp only [elideConf, ToAsm.elideJumps_op]; exact ASteps.single (AStep.op hb) | @dup n v τ ρ c yst hlen => @@ -587,6 +593,7 @@ theorem AStep.extend {prog : List Asm} {a b : AConf} (below : List AVal) ⟨b.code, b.stk ++ below, b.yst⟩ := by cases h with | push => simpa using AStep.push + | pushImmutable => simpa using AStep.pushImmutable | op hb => simpa [List.append_assoc] using AStep.op hb | @dup n v τ ρ c yst hlen => have := AStep.dup (model := model) (prog := prog) (n := n) (v := v) (τ := τ) diff --git a/YulEvmCompiler/SsaCfg/Spec/Backend.lean b/YulEvmCompiler/SsaCfg/Spec/Backend.lean index 0564c0a1..24d24574 100644 --- a/YulEvmCompiler/SsaCfg/Spec/Backend.lean +++ b/YulEvmCompiler/SsaCfg/Spec/Backend.lean @@ -42,7 +42,7 @@ open YulSemantics.EVM (U256 EvmState Op evmWithExternal) open YulSemantics (Outcome VEnv) open YulEvmCompiler -variable [model : ExternalModel] +variable [model : ExternalModel] {imm : String → YulSemantics.EVM.U256} local notation "yulD" => evmWithExternal model.calls model.creates /-- **Construction soundness**: if the construction accepts `prog` and the @@ -122,12 +122,12 @@ theorem optimizeProg_dom {P : Prog} (hdom : ToAsm.Prog.domCheck P = true) : omit model in /-- Invert a successful `finishProgOrd` into the shared final gates. -/ theorem finishProg_inv {ord : Bool} {P : Prog} {is : List YulEvmCompiler.Instr} - (h : finishProgOrd ord P = some is) : + (h : finishProgOrd imm ord P = some is) : ∃ asm : List Asm, ToAsm.emitProgOrd ord P = some asm ∧ wfCheck asm = true ∧ stackOK2 (optimizeAsm asm) = true - ∧ lowerProg (optimizeAsm asm) = some is := by + ∧ lowerProg imm (optimizeAsm asm) = some is := by unfold finishProgOrd at h rcases hemit : ToAsm.emitProgOrd ord P with _ | asm <;> rw [hemit] at h · exact absurd h (by simp) @@ -170,12 +170,12 @@ dominance gate passed, and the accepted bytecode is one of the four independently gated candidates ({optimized, raw} × {scheduling modes}). -/ theorem compileViaSsa_inv {prog : YulSemantics.Block Op} {is : List YulEvmCompiler.Instr} - (h : compileViaSsa prog = some is) : + (h : compileViaSsa prog imm = some is) : ∃ (P Q : Prog) (ord : Bool), ofBlock prog = some P ∧ ToAsm.Prog.domCheck P = true ∧ (Q = optimizeProg P ∨ Q = P) - ∧ finishProgOrd ord Q = some is := by + ∧ finishProgOrd imm ord Q = some is := by unfold compileViaSsa at h rcases hof : ofBlock prog with _ | P <;> rw [hof] at h · exact absurd h (by simp) @@ -203,8 +203,9 @@ is fully proved — it rests on the codegen simulation lemmas above. -/ theorem finishProg_correct (hexternal : ExternalsRealized model) {ord : Bool} {Q : Prog} {is : List YulEvmCompiler.Instr} (hQwf : Q.wfCheck = true) (hQdom : ToAsm.Prog.domCheck Q = true) - (hfin : finishProgOrd ord Q = some is) + (hfin : finishProgOrd imm ord Q = some is) {yst0 yst' : EvmState} {o : Outcome} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) (hssa : Run (model := model) Q yst0 yst' o) : ∃ b : Nat, ∀ s0 : State, FrameOK (assemble is) s0 → StateMatch yst0 s0 → @@ -230,8 +231,8 @@ theorem finishProg_correct (hexternal : ExternalsRealized model) (List.suffix_refl (optimizeAsm asm)) (stackOK2_run_bound hstk yst0) refine ⟨bnd, ?_⟩ intro s0 hf hm hpc hstk0 hgas - have hcm0 : ConfMatch (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := - ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp⟩ + have hcm0 : ConfMatch imm (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := + ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp, himm⟩ obtain ⟨s1, hsteps1, hcm1, -⟩ := Hb s0 hcm0 hgas have hpc1 : s1.pc = UInt256.ofNat (assembleBytes is).length := by rw [hcm1.pc]; simp [hlen] @@ -257,8 +258,8 @@ theorem finishProg_correct (hexternal : ExternalsRealized model) (List.suffix_refl (optimizeAsm asm)) (stackOK2_run_bound hstk yst0) refine ⟨bnd, ?_⟩ intro s0 hf hm hpc hstk0 hgas - have hcm0 : ConfMatch (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := - ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp⟩ + have hcm0 : ConfMatch imm (optimizeAsm asm) is ⟨optimizeAsm asm, [], yst0⟩ s0 := + ⟨by simpa using hf, hm, by rw [hpc]; simp, by rw [hstk0]; simp, himm⟩ obtain ⟨s', hsteps', hsm', hcs', hhm'⟩ := Hb s0 hcm0 hgas exact ⟨s', hsteps', hcs', hsm', Or.inr ⟨rfl, hhm'⟩⟩ @@ -268,8 +269,9 @@ on either the optimized program (through the pass-soundness lemma) or the original construction (which needs no pass soundness at all). -/ theorem compileViaSsa_correct (hexternal : ExternalsRealized model) {prog : YulSemantics.Block Op} {is : List YulEvmCompiler.Instr} - (hcomp : compileViaSsa prog = some is) + (hcomp : compileViaSsa prog imm = some is) {yst0 : EvmState} {V' : VEnv yulD} {yst' : EvmState} {o : Outcome} + (himm : ∀ key, imm key = yst0.env.immutable (YulSemantics.EVM.litValue (.string key))) (hrun : YulSemantics.Run yulD prog yst0 V' yst' o) : ∃ b : Nat, ∀ s0 : State, FrameOK (assemble is) s0 → StateMatch yst0 s0 → @@ -292,14 +294,14 @@ theorem compileViaSsa_correct (hexternal : ExternalsRealized model) rcases hQ with rfl | rfl · exact optimizeProg_dom hdom · exact hdom - exact finishProg_correct hexternal hQwf hQdom hfin hssa + exact finishProg_correct hexternal hQwf hQdom hfin himm hssa /-- The SSA backend, packaged under the generalized backend contract: the second `Optimizer.EvmBackend` inhabitant, next to `EvmBackend.classic`. -/ def evmBackend : Optimizer.EvmBackend where - compile := compileViaSsa + compile := fun prog imm => compileViaSsa prog imm correct := by - intro model hext prog is hcomp yst0 V' yst' o hrun - exact compileViaSsa_correct hext hcomp hrun + intro model hext imm prog is hcomp yst0 V' yst' o himm hrun + exact compileViaSsa_correct hext hcomp himm hrun end YulEvmCompiler.SsaCfg diff --git a/YulEvmCompiler/StackBound.lean b/YulEvmCompiler/StackBound.lean index 05552f87..2bebe02e 100644 --- a/YulEvmCompiler/StackBound.lean +++ b/YulEvmCompiler/StackBound.lean @@ -138,6 +138,8 @@ for the label-address push). `dup`/`swap` transport whatever cells they touch addresses — while `dynJump` requires the top cell's return layout `R` to equal the layout below it. -/ def stepConstraint (prog : List Asm) (H : LayoutMap) : Asm → List Asm → StkLayout → Prop | .push _, c, S => (.word :: S) ∈ H c ∧ S.length + 1 ≤ 1023 + -- Same stack effect as `push`; only the lowered width differs. + | .pushImmutable _, c, S => (.word :: S) ∈ H c ∧ S.length + 1 ≤ 1023 | .dup n, c, S => ∃ sl, S[n.val]? = some sl ∧ (sl :: S) ∈ H c ∧ S.length + 1 ≤ 1023 | .pushLabel l, c, S => (∃ c', findLabel l prog = some c' ∧ (.code c' :: S) ∈ H c) ∧ S.length + 1 ≤ 1023 @@ -219,6 +221,12 @@ theorem Inv.step {prog : List Asm} {H : LayoutMap} (hV : ValidHeights prog H) refine ⟨?_, .word :: S, hHc, .word hm⟩ show (AVal.word v :: σ).length ≤ 1023 simp only [List.length_cons, hL]; omega + | @pushImmutable key c σ yst => + obtain ⟨hHc, hlen⟩ := hV (.pushImmutable key) c hsuf _ hHa + have hL : σ.length = S.length := hm.length_eq + refine ⟨?_, .word :: S, hHc, .word hm⟩ + show (AVal.word _ :: σ).length ≤ 1023 + simp only [List.length_cons, hL]; omega | @op yop args rets c σ yst yst' hstepOp => obtain ⟨o, hop, _, hbnd, hHc⟩ := hV (.op yop) c hsuf _ hHa obtain ⟨hargs, hrets⟩ := builtin_arity hop hstepOp @@ -368,6 +376,8 @@ below, so a wrong proposal is simply rejected. -/ /-- Decidable mirror of `stepConstraint`. -/ def stepOK (prog : List Asm) (H : LayoutMap) : Asm → List Asm → StkLayout → Bool | .push _, c, S => decide ((.word :: S) ∈ H c) && decide (S.length + 1 ≤ 1023) + | .pushImmutable _, c, S => + decide ((.word :: S) ∈ H c) && decide (S.length + 1 ≤ 1023) | .dup n, c, S => match S[n.val]? with | some sl => decide ((sl :: S) ∈ H c) && decide (S.length + 1 ≤ 1023) | none => false @@ -403,6 +413,8 @@ theorem stepOK_sound {prog : List Asm} {H : LayoutMap} {i : Asm} {c : List Asm} (h : stepOK prog H i c S = true) : stepConstraint prog H i c S := by cases i with | push v => simp only [stepOK, Bool.and_eq_true, decide_eq_true_eq] at h; exact h + | pushImmutable key => + simp only [stepOK, Bool.and_eq_true, decide_eq_true_eq] at h; exact h | dup n => revert h; simp only [stepOK]; split · next sl he => @@ -484,6 +496,7 @@ contract. Positions are keyed by suffix length (unique among suffixes of a fixed /-- Successor positions and their layouts for one instruction. `none` = malformed / reject. -/ def succsOf (prog : List Asm) : Asm → List Asm → StkLayout → Option (List (List Asm × StkLayout)) | .push _, c, S => some [(c, .word :: S)] + | .pushImmutable _, c, S => some [(c, .word :: S)] | .dup n, c, S => match S[n.val]? with | some sl => some [(c, sl :: S)] | none => none | .pushLabel l, c, S => match findLabel l prog with | some tgt => some [(c, .code tgt :: S)] | none => none diff --git a/YulEvmCompiler/StackScalable.lean b/YulEvmCompiler/StackScalable.lean index edee6642..be9db64e 100644 --- a/YulEvmCompiler/StackScalable.lean +++ b/YulEvmCompiler/StackScalable.lean @@ -189,6 +189,9 @@ def Cert.Bounded (C : Cert) : Prop := /-- Per-instruction step constraint, given current `fl = some S`, `fbMax = some F`, `rl = some R`. -/ def frameStep (prog : List Asm) (C : Cert) : Asm → List Asm → FLayout → Nat → FLayout → Prop | .push _, c, S, F, R => C.fl c = some (.word :: S) ∧ C.fbMax c = some F ∧ C.rl c = some R + -- Same frame effect as `push`; only the lowered width differs. + | .pushImmutable _, c, S, F, R => + C.fl c = some (.word :: S) ∧ C.fbMax c = some F ∧ C.rl c = some R | .dup n, c, S, F, R => S[n.val]? = some FSlot.word ∧ C.fl c = some (.word :: S) ∧ C.fbMax c = some F ∧ C.rl c = some R | .pushLabel l, c, S, F, R => C.fl c = some (.retTo l :: S) ∧ C.fbMax c = some F ∧ C.rl c = some R @@ -532,6 +535,10 @@ theorem GoodStack.step {prog : List Asm} {C : Cert} (hV : C.Valid prog) obtain ⟨S, F, R, hfl, hfb, hrl⟩ := hinv.certAt obtain ⟨hflc, hfbc, hrlc⟩ := hV _ c S F R hfl hfb hrl exact hinv.growWord hfl hflc (by rw [hfbc, hfb]) (by rw [hrlc, hrl]) + | @pushImmutable key c σ yst => + obtain ⟨S, F, R, hfl, hfb, hrl⟩ := hinv.certAt + obtain ⟨hflc, hfbc, hrlc⟩ := hV _ c S F R hfl hfb hrl + exact hinv.growWord hfl hflc (by rw [hfbc, hfb]) (by rw [hrlc, hrl]) | @pushLabel l c σ yst hdef => obtain ⟨S, F, R, hfl, hfb, hrl⟩ := hinv.certAt obtain ⟨hflc, hfbc, hrlc⟩ := hV _ c S F R hfl hfb hrl @@ -769,6 +776,8 @@ conjunction, so soundness is a projection). -/ def frameStepB (prog : List Asm) (C : Cert) : Asm → List Asm → FLayout → Nat → FLayout → Bool | .push _, c, S, F, R => decide (C.fl c = some (.word :: S) ∧ C.fbMax c = some F ∧ C.rl c = some R) + | .pushImmutable _, c, S, F, R => + decide (C.fl c = some (.word :: S) ∧ C.fbMax c = some F ∧ C.rl c = some R) | .dup n, c, S, F, R => match S[n.val]? with | some FSlot.word => decide (C.fl c = some (.word :: S) ∧ C.fbMax c = some F ∧ C.rl c = some R) | _ => false @@ -827,6 +836,7 @@ theorem frameStepB_sound {prog : List Asm} {C : Cert} {i : Asm} {c : List Asm} { {F : Nat} {R : FLayout} (h : frameStepB prog C i c S F R = true) : frameStep prog C i c S F R := by cases i with | push v => simp only [frameStepB, decide_eq_true_eq] at h; exact h + | pushImmutable key => simp only [frameStepB, decide_eq_true_eq] at h; exact h | dup n => revert h; simp only [frameStepB]; split · next he => intro h; simp only [decide_eq_true_eq] at h; exact ⟨he, h⟩ @@ -1061,6 +1071,7 @@ looked up once instead of independently through `fl`, `fbMax`, and `rl`. -/ def frameStepLookupB (prog : List Asm) (lookup : CertLookup) : Asm → List Asm → FLayout → Nat → FLayout → Bool | .push _, c, S, F, R => decide (lookup c = some (.word :: S, F, R)) + | .pushImmutable _, c, S, F, R => decide (lookup c = some (.word :: S, F, R)) | .dup n, c, S, F, R => match S[n.val]? with | some FSlot.word => decide (lookup c = some (.word :: S, F, R)) | _ => false @@ -1133,6 +1144,7 @@ def frameStepLookupFastB (tgts : Std.HashMap Label (List Asm)) (lookup : CertLookup) : Asm → List Asm → FLayout → Nat → FLayout → Bool | .push _, c, S, F, R => decide (lookup c = some (.word :: S, F, R)) + | .pushImmutable _, c, S, F, R => decide (lookup c = some (.word :: S, F, R)) | .dup n, c, S, F, R => match S[n.val]? with | some FSlot.word => decide (lookup c = some (.word :: S, F, R)) | _ => false @@ -1201,6 +1213,8 @@ def frameStepLookupIdxB (tgts : Std.HashMap Label (List Asm)) (lookup : CertLookup) (tbl : Array (Option CertEntry)) (kc : Nat) : Asm → List Asm → FLayout → Nat → FLayout → Bool | .push _, c, S, F, R => decide (lookupAt tbl kc c = some (.word :: S, F, R)) + | .pushImmutable _, c, S, F, R => + decide (lookupAt tbl kc c = some (.word :: S, F, R)) | .dup n, c, S, F, R => match S[n.val]? with | some FSlot.word => decide (lookupAt tbl kc c = some (.word :: S, F, R)) | _ => false @@ -1414,6 +1428,7 @@ theorem frameStepLookupB_eq_frameStepB (prog : List Asm) (lookup : CertLookup) frameStepB prog lookup.toCert i c S F R := by cases i with | push => exact lookup.decide_eq_some_fields c (.word :: S) F R + | pushImmutable key => exact lookup.decide_eq_some_fields c (.word :: S) F R | pushLabel l => exact lookup.decide_eq_some_fields c (.retTo l :: S) F R | label => exact lookup.decide_eq_some_fields c S F R | jump l => @@ -1726,6 +1741,7 @@ def stepSuccs (tgts : Std.HashMap Label (List Asm × Nat)) (pls : Std.HashSet La let kc := k - 1 match i with | .push _ => some ([(kc, c, .word :: fl, rl, fe)], [], [], []) + | .pushImmutable _ => some ([(kc, c, .word :: fl, rl, fe)], [], [], []) | .dup n => match fl[n.val]? with | some FSlot.word => some ([(kc, c, .word :: fl, rl, fe)], [], [], []) | _ => none | .pop => match fl with | .word :: fl' => some ([(kc, c, fl', rl, fe)], [], [], []) | _ => none diff --git a/YulIR/Check.lean b/YulIR/Check.lean index cbfa9058..af9956fa 100644 --- a/YulIR/Check.lean +++ b/YulIR/Check.lean @@ -111,7 +111,8 @@ def currentOpt (b : YulSemantics.Block EVM.Op) : YulSemantics.Block EVM.Op := /-- Backend: block → bytecode, with the same stack-layout fallback `compileSource` uses. -/ def blockBytecode (b : YulSemantics.Block EVM.Op) : Option ByteArray := (YulEvmCompiler.compile b - <|> YulEvmCompiler.compile (YulEvmCompiler.Optimizer.stackLayoutBlock b)).map + <|> YulEvmCompiler.compile + (YulEvmCompiler.Optimizer.stackLayoutBlock b)).map YulEvmCompiler.assemble /-- Compiled code size in bytes, or `none` if the backend failed. -/ diff --git a/YulParser/Compile.lean b/YulParser/Compile.lean index 9f970507..a6599457 100644 --- a/YulParser/Compile.lean +++ b/YulParser/Compile.lean @@ -76,11 +76,19 @@ mutual def decodeValueExpr : Expr YulSemantics.EVM.Op → Expr YulSemantics.EVM.Op | .lit literal => .lit (decodeValueLiteral literal) | .var name => .var name + -- Only `setimmutable`'s middle argument names the immutable; the target and + -- the stored value are ordinary expressions and must be decoded, or an + -- escaped string value would be patched in as its escape spelling. + | .call "setimmutable" [base, .lit (.string key), value] => + .call "setimmutable" + [decodeValueExpr base, .lit (.string key), decodeValueExpr value] | .call name args => if literalNameCall name then .call name args else .call name (decodeValueArgs args) | .builtin op args => - if op == .dataoffset || op == .datasize then .builtin op args + if op == .dataoffset || op == .datasize || op == .loadimmutable then + -- name-valued arguments stay spelling-sensitive + .builtin op args else .builtin op (decodeValueArgs args) def decodeValueArgs : List (Expr YulSemantics.EVM.Op) → @@ -304,6 +312,86 @@ partial def linkObject {Op : Type} (env : LinkEnv) : Object Op → Object Op | .mk name code subs segs => .mk name (code.map (linkStmt env)) (subs.map (linkObject env)) segs +/-! ### `setimmutable` + +`setimmutable(base, name, value)` writes `value` into the in-memory copy of the +deployed code the constructor is about to return, at every position where that +code reads the immutable. Those positions are the placeholder offsets the child +object's compiled layout records, so the call is **eliminable**: it expands to +one ordinary `mstore` per offset, before anything else runs. + +That keeps the extension entirely in the front end — the object layer, its +layout-resolution proof and `compileObject_correct` never see it. + +**What is proved, and what is not.** The offsets are a theorem: +`immutableOffsets_correct` shows every offset this expansion patches really does +locate that immutable's 32-byte immediate in the emitted code, so a wrong offset +— the silent-miscompilation risk — is ruled out. + +What remains unproved is the *meaning*: `setimmutable` has no source semantics +(it is not an `Op`), so there is no source run to preserve and no +semantic-preservation theorem relates the original object to the expanded one. +The correctness theorem covers the **desugared** program, the one that performs +these `mstore`s. That is a front-end desugaring in the same family as +`memoryguard`, not a proved `Optimizer.Pass`; closing it would mean modeling +`setimmutable` upstream. -/ + +/-- Does this object tree read or write an immutable? -/ +partial def usesImmutablesExpr : Expr YulSemantics.EVM.Op → Bool + | .builtin .loadimmutable _ => true + | .call "setimmutable" _ => true + | .call _ args => args.any usesImmutablesExpr + | .builtin _ args => args.any usesImmutablesExpr + | _ => false + +partial def usesImmutablesStmt : Stmt YulSemantics.EVM.Op → Bool + | .block body | .funDef _ _ _ body => body.any usesImmutablesStmt + | .letDecl _ v => (v.map usesImmutablesExpr).getD false + | .assign _ v | .exprStmt v => usesImmutablesExpr v + | .cond c body => usesImmutablesExpr c || body.any usesImmutablesStmt + | .switch c cases dflt => + usesImmutablesExpr c || cases.any (fun cb => cb.2.any usesImmutablesStmt) || + ((dflt.map (·.any usesImmutablesStmt)).getD false) + | .forLoop init c post body => + init.any usesImmutablesStmt || usesImmutablesExpr c || + post.any usesImmutablesStmt || body.any usesImmutablesStmt + | _ => false + +partial def usesImmutablesObject : Object YulSemantics.EVM.Op → Bool + | .mk _ code subs _ => code.any usesImmutablesStmt || subs.any usesImmutablesObject + +/-- Expand every `setimmutable` in an object tree against the placeholder +offsets of that object's own children, or reject the tree. + +An immutable is patched by the **parent** of the object that reads it: the +parent copies the child's code into memory and stores over the placeholders. +Validation only pairs reads with writes *globally* across the whole tree, which +is too weak — a setter in an unrelated sibling patches nothing, and the reader +would deploy with the placeholder still zero. So the pairing is re-checked here +per scope, and a tree that fails it is rejected rather than silently +miscompiled. -/ +partial def expandSetImmutablesObject (o : Object YulSemantics.EVM.Op) : + Option (Object YulSemantics.EVM.Op) := + match o with + | .mk name code subs segs => do + let subs ← subs.mapM expandSetImmutablesObject + let perChild := subs.map fun sub => + (YulEvmCompiler.objectImmutableOffsets sub).getD [] + -- every immutable a direct child reads must be written by *this* object + let written := (collectImmutableCallsStmts code).2 + if !(perChild.flatten.all fun p => written.contains p.1) then none else + -- `setimmutable(base, name, value)` names no child, and `base` points at a + -- copy of one of them. If two children declare the same immutable the + -- offsets are not comparable against a single base, so that name is left + -- unexpanded and the backend rejects the program. + let declaredBy (n : String) : Nat := + (perChild.filter fun offs => offs.any (fun p => p.1 == n)).length + let all := perChild.flatten + let ambiguous := (all.map Prod.fst).filter fun n => declaredBy n > 1 + let offsets := all.filter fun p => declaredBy p.1 == 1 + return .mk name + (YulEvmCompiler.expandSetImmutablesStmts offsets ambiguous code) subs segs + /-- Parse and compile a complete Yul source program to executable EVM bytecode, using the documented compatibility parser when the verified parser does not apply. Hint builtins (`memoryguard`) are desugared for ordinary candidates and @@ -327,6 +415,11 @@ def compileSource (source : String) (libraries : LinkEnv := []) : Option ByteArray := do match parseSource source with | some (.block block) => + -- A block-rooted program has no object tree, so nothing could ever patch a + -- placeholder: a `loadimmutable` here would compile to a hard-coded zero. + -- Reject instead. (The grammar still accepts it — this is a compilation + -- limit, not a syntax rule, so the upstream syntax corpus is unaffected.) + if !(collectImmutableCallsStmts block).1.isEmpty then none else -- The link pass is an expensive identity when no addresses are supplied, -- and these inputs are megabytes of generated Yul; skip it entirely. let decoded := decodeValueStmts block @@ -403,6 +496,12 @@ def compileSource (source : String) (libraries : LinkEnv := []) : | none, cb => cb return YulEvmCompiler.assemble (← asm) | some (.object o) => + -- The root has no parent to copy and patch its code, so a `loadimmutable` + -- in the root's *own* code could only ever read the unpatched placeholder, + -- however many setters the tree contains. Reject it. + let rootReads := match decodeValueObject o with + | .mk _ code _ _ => (collectImmutableCallsStmts code).1 + if !rootReads.isEmpty then none else let decoded := decodeValueObject o let raw := pruneLinkerObjectTree (if libraries.isEmpty then decoded else linkObject libraries decoded) @@ -418,18 +517,27 @@ def compileSource (source : String) (libraries : LinkEnv := []) : (calls := YulSemantics.EVM.ExternalCalls.none) (creates := YulSemantics.EVM.ExternalCreates.none) o let tryLayouts (obj : Object YulSemantics.EVM.Op) := - YulEvmCompiler.compileObject obj - <|> YulEvmCompiler.compileObject - (YulEvmCompiler.Optimizer.cleanupAfterLayoutObject - (calls := YulSemantics.EVM.ExternalCalls.none) - (creates := YulSemantics.EVM.ExternalCreates.none) - (YulEvmCompiler.Optimizer.stackLayoutObject obj)) - <|> YulEvmCompiler.compileObject - (YulEvmCompiler.Optimizer.stackLayoutObject obj) + (expandSetImmutablesObject obj).bind YulEvmCompiler.compileObject + <|> (expandSetImmutablesObject + (YulEvmCompiler.Optimizer.cleanupAfterLayoutObject + (calls := YulSemantics.EVM.ExternalCalls.none) + (creates := YulSemantics.EVM.ExternalCreates.none) + (YulEvmCompiler.Optimizer.stackLayoutObject obj))).bind + YulEvmCompiler.compileObject + <|> (expandSetImmutablesObject + (YulEvmCompiler.Optimizer.stackLayoutObject obj)).bind + YulEvmCompiler.compileObject -- SSA-CFG backend on the object path too (same layout fixpoint, SSA -- per code block); both artifacts are kept and the cheaper bytecode -- (static stack-traffic cost) wins. - let ssaLayout := YulEvmCompiler.SsaCfg.compileObjectViaSsa optimized + -- The constructor's patch offsets are read off the *classic* plan + -- (`objectImmutableOffsets`), but the SSA object path schedules its code + -- independently and records no offsets, so a winning SSA artifact could + -- be patched at the wrong positions. Withhold that candidate whenever the + -- tree touches an immutable. + let ssaLayout := + if usesImmutablesObject optimized then none + else (expandSetImmutablesObject optimized).bind YulEvmCompiler.SsaCfg.compileObjectViaSsa let classicLayout := tryLayouts optimized <|> tryLayouts (YulEvmCompiler.Optimizer.optimizerPipelineObjectNoRejoin (calls := YulSemantics.EVM.ExternalCalls.none) @@ -437,7 +545,7 @@ def compileSource (source : String) (libraries : LinkEnv := []) : <|> tryLayouts (YulEvmCompiler.Optimizer.optimizerPipelineObjectLight (calls := YulSemantics.EVM.ExternalCalls.none) (creates := YulSemantics.EVM.ExternalCreates.none) o) - <|> YulEvmCompiler.compileObject o + <|> (expandSetImmutablesObject o).bind YulEvmCompiler.compileObject <|> (match YulEvmCompiler.Optimizer.MemorySpillSelect.spillObjectWithFallback raw optimized with | some spilled => @@ -449,7 +557,7 @@ def compileSource (source : String) (libraries : LinkEnv := []) : -- without it they never see the optimizer at all. Objects the -- plain spilled form cannot compile (live `gas`, immutables, -- linker symbols) skip the expensive pipeline entirely. - match YulEvmCompiler.compileObject spilled.object with + match (expandSetImmutablesObject spilled.object).bind YulEvmCompiler.compileObject with | none => none | some plainLayout => let spilledOpt := @@ -461,14 +569,16 @@ def compileSource (source : String) (libraries : LinkEnv := []) : YulSemantics.EVM.ExternalCalls.none YulSemantics.EVM.ExternalCreates.none) spilled.object) - YulEvmCompiler.compileObject spilledOpt - <|> YulEvmCompiler.compileObject - (YulEvmCompiler.Optimizer.cleanupAfterLayoutObject - (calls := YulSemantics.EVM.ExternalCalls.none) - (creates := YulSemantics.EVM.ExternalCreates.none) - (YulEvmCompiler.Optimizer.stackLayoutObject spilledOpt)) - <|> YulEvmCompiler.compileObject - (YulEvmCompiler.Optimizer.stackLayoutObject spilledOpt) + (expandSetImmutablesObject spilledOpt).bind YulEvmCompiler.compileObject + <|> (expandSetImmutablesObject + (YulEvmCompiler.Optimizer.cleanupAfterLayoutObject + (calls := YulSemantics.EVM.ExternalCalls.none) + (creates := YulSemantics.EVM.ExternalCreates.none) + (YulEvmCompiler.Optimizer.stackLayoutObject spilledOpt))).bind + YulEvmCompiler.compileObject + <|> (expandSetImmutablesObject + (YulEvmCompiler.Optimizer.stackLayoutObject spilledOpt)).bind + YulEvmCompiler.compileObject <|> some plainLayout | none => none) let layout ← diff --git a/YulParser/Examples.lean b/YulParser/Examples.lean index e7d06415..70d4b0cd 100644 --- a/YulParser/Examples.lean +++ b/YulParser/Examples.lean @@ -115,6 +115,88 @@ tree compiled before the fix too, so this pins that the fix did not change it. - "object \"Pd\" { code { sstore(0, 1) } " ++ "data \".metadata\" hex\"a2646970667358221220\" } } }")).isSome +/-! Immutables. `loadimmutable` compiles to a fixed-width `PUSH32` placeholder +in the deployed object, and the constructor's `setimmutable` becomes one +`mstore` per recorded placeholder offset — so the returned runtime carries the +value the constructor computed. -/ +def immutablePair : String := + "object \"A\" {\n" ++ + " code { let s := datasize(\"A_deployed\") codecopy(0, dataoffset(\"A_deployed\"), s)\n" ++ + " setimmutable(0, \"42\", caller()) return(0, s) }\n" ++ + " object \"A_deployed\" { code { sstore(0, loadimmutable(\"42\")) } }\n" ++ + "}\n" + +#guard (parseSource immutablePair).isSome +#guard (compileSource immutablePair).isSome + +/-! A block-rooted program has no object tree, so nothing could ever patch a +placeholder: a `loadimmutable` there is rejected rather than compiled to a +hard-coded zero. The *grammar* still accepts it — upstream's syntax corpus has a +fixture for exactly this — so the limit lives in compilation, not parsing. -/ +#guard (parseSource "{ sstore(0, loadimmutable(\"x\")) }").isSome +#guard (compileSource "{ sstore(0, loadimmutable(\"x\")) }").isNone + +/-! The root has no parent to copy and patch its code, so a `loadimmutable` in +the root's own code could only ever read the unpatched placeholder — however +many setters the tree contains. -/ +#guard (compileSource + ("object \"A\" { code { setimmutable(0, \"x\", caller()) " ++ + "sstore(0, loadimmutable(\"x\")) stop() } }")).isNone + +/-! Only `setimmutable`'s middle argument names the immutable; the target and +the stored value are ordinary expressions. An escaped string value must be +patched in as its *bytes*, not as the characters of its escape spelling — so +`"\\x01"` must compile exactly like `hex"01"`, the same bytes spelled without +escapes. -/ +def escapedImmutableValue (spelling : String) : String := + "object \"A\" {\n" ++ + " code { let s := datasize(\"B\") codecopy(0, dataoffset(\"B\"), s)\n" ++ + " setimmutable(0, \"x\", " ++ spelling ++ ") return(0, s) }\n" ++ + " object \"B\" { code { sstore(0, loadimmutable(\"x\")) } }\n" ++ + "}\n" + +#guard (compileSource (escapedImmutableValue "\"\\x01\"")).isSome +#guard (compileSource (escapedImmutableValue "\"\\x01\"")) == + (compileSource (escapedImmutableValue "hex\"01\"")) + +/-! An immutable is patched by the **parent** of the object that reads it. +Validation pairs reads with writes only globally, so a setter sitting in an +unrelated sibling satisfies it while patching nothing — the reader would deploy +with its placeholder still zero. The pairing is re-checked per scope. -/ +def crossScopeImmutable : String := + "object \"A\" {\n" ++ + " code { let s := datasize(\"B\") codecopy(0, dataoffset(\"B\"), s) return(0, s) }\n" ++ + " object \"B\" { code { sstore(0, loadimmutable(\"x\")) } }\n" ++ + " object \"C\" { code { setimmutable(0, \"x\", caller()) stop() } }\n" ++ + "}\n" + +#guard (parseSource crossScopeImmutable).isSome +#guard (compileSource crossScopeImmutable).isNone + +/-! Two sibling objects declaring the same immutable put its placeholder at +different offsets, but `setimmutable(base, name, value)` names no child and +`base` points at a copy of one of them. Patching one at the other's offsets +would overwrite its code, so the ambiguous name is rejected. -/ +def siblingImmutables : String := + "object \"A\" {\n" ++ + " code { let s := datasize(\"B\") codecopy(0, dataoffset(\"B\"), s)\n" ++ + " setimmutable(0, \"x\", caller()) return(0, s) }\n" ++ + " object \"B\" { code { sstore(0, loadimmutable(\"x\")) } }\n" ++ + " object \"C\" { code { sstore(1, 1) sstore(2, 2) sstore(3, loadimmutable(\"x\")) } }\n" ++ + "}\n" + +#guard (parseSource siblingImmutables).isSome +#guard (compileSource siblingImmutables).isNone + +/-! A `loadimmutable` with no matching `setimmutable` is rejected by validation: +nothing would ever write that placeholder. -/ +#guard (parseSource + "object \"A\" { code { sstore(0, loadimmutable(\"42\")) } }").isNone + +/-! `setimmutable` alone is fine — it simply patches nothing. -/ +#guard (compileSource + "object \"A\" { code { setimmutable(0, \"42\", 7) stop() } }").isSome + /-! The prune is shadowing-proof by over-approximation: if the bound name is referenced anywhere in the program — even a write — the binding is kept and the program is rejected rather than miscompiled. -/ diff --git a/YulParser/Validate.lean b/YulParser/Validate.lean index b2db2dc1..68ed8663 100644 --- a/YulParser/Validate.lean +++ b/YulParser/Validate.lean @@ -45,8 +45,10 @@ private def lowLevelReserved (name : String) : Bool := name == "pc" || name == "jump" || name == "jumpi" || name == "jumpdest" || numbered "dup" || numbered "swap" || numbered "push" +-- `loadimmutable` is no longer here: pinned yul-semantics models it as a real +-- `Op`, so `parse` recognizes it and it is validated like `dataoffset`/`datasize`. private def specialBuiltin (name : String) : Bool := - name == "memoryguard" || name == "linkersymbol" || name == "loadimmutable" || + name == "memoryguard" || name == "linkersymbol" || name == "setimmutable" || name.startsWith "verbatim_" private def builtinName (ctx : ValidateCtx) (name : String) : Bool := @@ -67,8 +69,8 @@ private def opInputs : Op → Nat | .call | .callcode => 7 | .delegatecall | .staticcall => 6 | .clz | .iszero | .not | .pop | .mload | .sload | .tload | .calldataload - | .datasize | .dataoffset | .balance | .extcodesize | .extcodehash | .blockhash - | .blobhash | .selfdestruct => 1 + | .datasize | .dataoffset | .loadimmutable | .balance | .extcodesize + | .extcodehash | .blockhash | .blobhash | .selfdestruct => 1 | .log0 => 2 | .log1 => 3 | .log2 => 4 @@ -146,6 +148,14 @@ private def exprOutputs (ctx : ValidateCtx) : Expr Op → Option Nat let name ← directString arg if objectNameAllowed ctx name then some (opOutputs op) else none | _ => none + else if op == .loadimmutable then + -- The immutable's name is a direct string literal, as for the layout + -- built-ins; unlike them it names no object, so no accessibility rule + -- applies. `validateObjectSource` separately requires a matching + -- `setimmutable`. + match args with + | [arg] => if (directString arg).isSome then some (opOutputs op) else none + | _ => none else validArgs ctx args some (opOutputs op) @@ -153,7 +163,7 @@ private def exprOutputs (ctx : ValidateCtx) : Expr Op → Option Nat if !validIdentifier name || lowLevelReserved name then none if name == "memoryguard" then if args.length != 1 then none else validArgs ctx args; some 1 - else if name == "linkersymbol" || name == "loadimmutable" then + else if name == "linkersymbol" then match args with | [arg] => if (directString arg).isSome then some 1 else none | _ => none @@ -386,39 +396,27 @@ private theorem contains_eq_false_append {s p q : String} (h : s.contains p = fa contains_eq_false_append hg, contains_eq_false_append hg, contains_eq_false_append hg] simp -def validateBlockSource (source : String) (body : List (Stmt Op)) : Bool := - sourceLexWF source && - (validateBlock { inactiveBuiltins := inactiveBuiltins source } body).isSome - -private def withPrefix (prefixName : String) (name : String) : String := - prefixName ++ "." ++ name - -private def accessibleObjectNames : Object Op → List String - | .mk name _ subs datas => - let dataNames := (datas.map Prod.fst).filter (fun n => !n.startsWith ".") - let subNames := subs.flatMap fun sub => - let child := Object.name sub - child :: ((accessibleObjectNames sub).filter (fun n => n != child && !n.startsWith ".") - |>.map (withPrefix child)) - name :: dataNames ++ subNames - -private def collectImmutableCallsExpr : Expr Op → List String × List String +/-- Collect the immutable names read (`loadimmutable`, now an ordinary `Op`) +and written (`setimmutable`, still a solc extension carried as a `.call`). -/ +def collectImmutableCallsExpr : Expr Op → List String × List String | .lit _ | .var _ | .builtin _ [] | .call _ [] => ([], []) - | .builtin _ args => args.foldl (fun acc e => - let found := collectImmutableCallsExpr e - (acc.1 ++ found.1, acc.2 ++ found.2)) ([], []) - | .call name args => + | .builtin op args => let nested := args.foldl (fun acc e => let found := collectImmutableCallsExpr e (acc.1 ++ found.1, acc.2 ++ found.2)) ([], []) - if name == "loadimmutable" then + if op == .loadimmutable then match args with | [.lit (.string key)] => (key :: nested.1, nested.2) | _ => nested - else if name == "setimmutable" then + else nested + | .call name args => + let nested := args.foldl (fun acc e => + let found := collectImmutableCallsExpr e + (acc.1 ++ found.1, acc.2 ++ found.2)) ([], []) + if name == "setimmutable" then match args with | [_, .lit (.string key), _] => (nested.1, key :: nested.2) | _ => nested else nested mutual -private partial def collectImmutableCallsStmt : Stmt Op → List String × List String +partial def collectImmutableCallsStmt : Stmt Op → List String × List String | .block body | .funDef _ _ _ body => collectImmutableCallsStmts body | .letDecl _ value => value.map collectImmutableCallsExpr |>.getD ([], []) | .assign _ value | .exprStmt value => collectImmutableCallsExpr value @@ -435,15 +433,32 @@ private partial def collectImmutableCallsStmt : Stmt Op → List String × List (combineImmutable (collectImmutableCallsStmts post) (collectImmutableCallsStmts body))) | .«break» | .«continue» | .leave => ([], []) -private partial def collectImmutableCallsStmts : List (Stmt Op) → List String × List String +partial def collectImmutableCallsStmts : List (Stmt Op) → List String × List String | [] => ([], []) | statement :: statements => combineImmutable (collectImmutableCallsStmt statement) (collectImmutableCallsStmts statements) -private partial def combineImmutable (a b : List String × List String) : List String × List String := +partial def combineImmutable (a b : List String × List String) : List String × List String := (a.1 ++ b.1, a.2 ++ b.2) end + +def validateBlockSource (source : String) (body : List (Stmt Op)) : Bool := + sourceLexWF source && + (validateBlock { inactiveBuiltins := inactiveBuiltins source } body).isSome + +private def withPrefix (prefixName : String) (name : String) : String := + prefixName ++ "." ++ name + +private def accessibleObjectNames : Object Op → List String + | .mk name _ subs datas => + let dataNames := (datas.map Prod.fst).filter (fun n => !n.startsWith ".") + let subNames := subs.flatMap fun sub => + let child := Object.name sub + child :: ((accessibleObjectNames sub).filter (fun n => n != child && !n.startsWith ".") + |>.map (withPrefix child)) + name :: dataNames ++ subNames + mutual private partial def collectImmutableCallsObject : Object Op → List String × List String | .mk _ code subs _ => combineImmutable (collectImmutableCallsStmts code) diff --git a/lake-manifest.json b/lake-manifest.json index fb4d1d9b..3d4d2919 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4c6f9753cc0e5850f6bdaf6fb0df76457204699a", + "rev": "90b33d7475e0c4fb2f67b72f3e151164ae8b4d6f", "name": "«yul-semantics»", "manifestFile": "lake-manifest.json", - "inputRev": "4c6f9753cc0e5850f6bdaf6fb0df76457204699a", + "inputRev": "90b33d7475e0c4fb2f67b72f3e151164ae8b4d6f", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", diff --git a/lakefile.toml b/lakefile.toml index 237d9290..9cdc58e5 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 = "4c6f9753cc0e5850f6bdaf6fb0df76457204699a" +rev = "90b33d7475e0c4fb2f67b72f3e151164ae8b4d6f" # Target-language semantics: the EVM small-step/big-step relations. [[require]] diff --git a/test/solidity-semantic-gas-baseline.txt b/test/solidity-semantic-gas-baseline.txt index 21d6401f..3c110cc4 100644 --- a/test/solidity-semantic-gas-baseline.txt +++ b/test/solidity-semantic-gas-baseline.txt @@ -519,6 +519,7 @@ expressions/tuple_from_ternary_expression.sol 169 142 expressions/unary_too_long_literal.sol 169 142 expressions/uncalled_address_transfer_send.sol 147 100 externalContracts/FixedFeeRegistrar.sol 244330 239633 +externalContracts/snark.sol 132 20 fallback/call_forward_bytes.sol 41953 41497 fallback/falback_return.sol 9108 8960 fallback/fallback_or_receive.sol 60210 59537 @@ -608,6 +609,22 @@ getters/string_and_bytes.sol 11654 11204 getters/struct_with_bytes.sol 4915 4750 getters/struct_with_bytes_simple.sol 4915 4750 getters/value_types.sol 21680 21190 +immutable/assign_at_declaration.sol 180 148 +immutable/assign_from_immutables.sol 852 736 +immutable/delete.sol 2711 2631 +immutable/fun_read_in_ctor.sol 2491 2434 +immutable/getter.sol 174 142 +immutable/immutable_signed.sol 238 160 +immutable/immutable_tag_too_large_bug.sol 1300 1275 +immutable/increment_decrement.sol 238 160 +immutable/inheritance.sol 22 5 +immutable/internal_function_pointer.sol 420 346 +immutable/multi_creation.sol 352 304 +immutable/read_in_ctor.sol 2289 2247 +immutable/small_types_in_reverse.sol 8476 7599 +immutable/stub.sol 273 194 +immutable/uninitialized.sol 534 202 +immutable/use_scratch.sol 2657 2539 inheritance/access_base_storage.sol 2451 2403 inheritance/address_overload_resolution.sol 230 216 inheritance/base_access_to_function_type_variables.sol 27165 27004 @@ -624,6 +641,7 @@ inheritance/inherited_function.sol 22 5 inheritance/inherited_function_calldata_calldata_interface.sol 89 81 inheritance/inherited_function_calldata_memory.sol 109 81 inheritance/inherited_function_calldata_memory_interface.sol 109 63 +inheritance/inherited_function_from_a_library.sol 33 5 inheritance/inherited_function_through_dispatch.sol 22 5 inheritance/overloaded_function_call_resolve_to_first.sol 221 194 inheritance/overloaded_function_call_resolve_to_second.sol 221 186 @@ -740,8 +758,20 @@ libraries/internal_library_function_attached_to_struct.sol 887 578 libraries/internal_library_function_calling_private.sol 630 493 libraries/internal_library_function_pointer.sol 171 142 libraries/internal_library_function_return_var_size.sol 887 578 +libraries/internal_types_in_library.sol 124 78 +libraries/library_call_in_homestead.sol 200 162 +libraries/library_enum_as_an_expression.sol 33 5 +libraries/library_staticcall_delegatecall.sol 100 81 +libraries/library_stray_values.sol 100 81 +libraries/library_struct_as_an_expression.sol 33 5 +libraries/mapping_arguments_in_library.sol 462 70 +libraries/mapping_returns_in_library.sol 1452 220 +libraries/mapping_returns_in_library_named.sol 66 10 libraries/stub_internal.sol 729 615 libraries/using_for_storage_structs.sol 22426 22265 +libraries/using_library_mappings_public.sol 160 60 +libraries/using_library_mappings_return.sol 100 81 +libraries/using_library_structs.sol 172 78 literals/denominations.sol 171 142 literals/denominations_in_array_sizes.sol 406 268 literals/escape.sol 626 355 @@ -764,6 +794,8 @@ modifiers/continue_in_modifier.sol 29333 28547 modifiers/function_modifier.sol 361 288 modifiers/function_modifier_calling_functions_in_creation_context.sol 2296 2247 modifiers/function_modifier_for_constructor.sol 2277 2241 +modifiers/function_modifier_library.sol 33 5 +modifiers/function_modifier_library_inheritance.sol 33 5 modifiers/function_modifier_local_variables.sol 529 459 modifiers/function_modifier_loop.sol 897 693 modifiers/function_modifier_loop_viair.sol 897 693 @@ -965,6 +997,7 @@ storageLayoutSpecifier/inheritance_constructor_order_calling_revert.sol 0 0 storageLayoutSpecifier/inheritance_constructor_order_setting_storage_var.sol 194 162 storageLayoutSpecifier/inheritance_from_interface.sol 24804 24604 storageLayoutSpecifier/inheritance_from_same_base_state_var_slots.sol 345 324 +storageLayoutSpecifier/inheritance_immutables.sol 178 162 storageLayoutSpecifier/inheritance_modifier_calling_revert.sol 44 10 storageLayoutSpecifier/inheritance_simple.sol 2471 2403 storageLayoutSpecifier/inheritance_state_variable_slot_offset.sol 88 20 @@ -976,6 +1009,7 @@ storageLayoutSpecifier/mapping_storage_end.sol 24557437 24503311 storageLayoutSpecifier/multiple_inheritance.sol 2836 2679 storageLayoutSpecifier/multiple_inheritance_state_var_slots.sol 88 20 storageLayoutSpecifier/state_variable_arithmetic_expression.sol 103304 101488 +storageLayoutSpecifier/state_variable_constant_and_immutable.sol 446 405 storageLayoutSpecifier/state_variable_dynamic_array.sol 3145 2909 storageLayoutSpecifier/state_variable_enum.sol 27472 27114 storageLayoutSpecifier/state_variable_mapping.sol 88 20 @@ -1068,6 +1102,8 @@ types/convert_uint_to_fixed_bytes_smaller_size.sol 246 198 types/external_function_to_address.sol 509 367 types/mapping/copy_from_mapping_to_mapping.sol 182113 176038 types/mapping/copy_struct_to_array_stored_in_mapping.sol 98280 88477 +types/mapping_enum_key_library_v1.sol 3510 1620 +types/mapping_enum_key_library_v2.sol 3510 1620 types/mapping_enum_key_v1.sol 73226 72839 types/mapping_enum_key_v2.sol 73226 72839 types/mapping_simple.sol 79521 78921 @@ -1092,6 +1128,8 @@ userDefinedValueType/conversion_abicoderv1.sol 8402 6061 userDefinedValueType/dirty_slot.sol 31553 31239 userDefinedValueType/dirty_uint8_read.sol 7044 6934 userDefinedValueType/erc20.sol 55817 54454 +userDefinedValueType/fixedpoint.sol 363 55 +userDefinedValueType/immutable_signed.sol 759 385 userDefinedValueType/in_parenthesis.sol 229 160 userDefinedValueType/mapping_key.sol 34834 34579 userDefinedValueType/memory_to_storage.sol 143623 140329 @@ -1108,6 +1146,7 @@ using/calldata_memory_copy.sol 1403 957 using/free_function_braces.sol 818 648 using/free_function_multi.sol 818 648 using/free_functions_individual.sol 818 648 +using/private_library_function.sol 163 127 variables/delete_local.sol 170 141 variables/delete_locals.sol 229 160 variables/delete_transient_state_variable.sol 750 451 diff --git a/test/solidity-yul-object-compiler-gas-baseline.txt b/test/solidity-yul-object-compiler-gas-baseline.txt index de18d6ae..e9186393 100644 --- a/test/solidity-yul-object-compiler-gas-baseline.txt +++ b/test/solidity-yul-object-compiler-gas-baseline.txt @@ -12,6 +12,7 @@ identical_subobjects_full_debug_info.yul 92938 93190 identical_subobjects_no_debug_info.yul 92938 93190 identical_subobjects_partial_debug_info.yul 92938 93190 identical_subobjects_partial_debug_info_no_use_src.yul 92938 93190 +immutable_long_name_does_not_end_up_in_bytecode.yul 54 54 jump_tags.yul 168 432 long_object_name.yul 44330 44330 metadata.yul 162702 162684 diff --git a/test/solidity-yul-object-compiler-known-compile-failures.txt b/test/solidity-yul-object-compiler-known-compile-failures.txt index f2bac50a..88d42dc3 100644 --- a/test/solidity-yul-object-compiler-known-compile-failures.txt +++ b/test/solidity-yul-object-compiler-known-compile-failures.txt @@ -2,7 +2,6 @@ # Every fixture whose EVMVersion range includes Osaka is compiled. Keep exactly # the fixtures that do not parse/compile, including those the stack-overflow gate # (StackScalable) rejects as not provably stack-bounded (recursion / cycles). -immutable_long_name_does_not_end_up_in_bytecode.yul leading_and_trailing_dots.yul linkersymbol.yul prune_unreachable_function_recursion.yul diff --git a/test/solidity-yul-object-compiler-known-solc-differential-failures.txt b/test/solidity-yul-object-compiler-known-solc-differential-failures.txt index 5cd06b24..dc8e9067 100644 --- a/test/solidity-yul-object-compiler-known-solc-differential-failures.txt +++ b/test/solidity-yul-object-compiler-known-solc-differential-failures.txt @@ -10,7 +10,6 @@ dataoffset_data.yul datasize_code.yul datasize_self.yul identical_subobjects_with_subject_references.yul -immutable_long_name_does_not_end_up_in_bytecode.yul leading_and_trailing_dots.yul linkersymbol.yul manySubObjects.yul