Compile immutables (loadimmutable / setimmutable) - #154
Conversation
CI summary — ✅ All goodhead 1. Parsing
2. CorrectnessCompilation (positive corpora):
Behaviour differential vs solc:
3. Gasa) This compiler vs solc's optimized output — we compile solc's unoptimized
Coverage change vs main — ours/solc > 100% is expected: this compiler has no Yul optimizer yet, so it spends more gas than solc's optimized output. This number is the size of that gap. It does not fail CI; only a regression above the pinned baseline does. b) Backend codegen parity — both this compiler and solc assemble the same, unoptimized Yul (solc
Coverage change vs main — Here ours/solc near 100% is expected — neither side optimizes, so this compares raw code generation on identical input, not optimizer quality. 4. Compiler runtime (informational)Both columns measure the same job on the same input: unoptimized Yul → EVM bytecode, no optimizer on either side, over the same fixtures — only those both compilers finished are counted, on either side. solc's Solidity→Yul front-end is charged to neither: it runs once, before both, and its output is what each then compiles. a) Solidity corpora — both compile the unoptimized
Charged to neither column: 32.8 s of solc b) Yul corpora — the fixtures are already Yul, so both compile it directly; there is no front-end on either side.
Excluded from both columns: 1.3 min this compiler spent on 247 fixture(s) it then rejected. solc is not asked for those. Each figure is the sum of that suite's per-fixture compile spans, added across shards — independent of worker count and sharding, but measured on shared CI runners under saturated parallelism. Treat single-digit percentage moves as noise. Nothing here affects the verdict. 5. Soundness (formal guarantee)
6. Verdict✅ All good |
leonardoalt
changed the title
loadimmutable / setimmutable)
powdr-labs/yul-semantics#42 models `loadimmutable` as an ordinary `Op` reading the environment's immutable map, keyed by the name's string-literal encoding — the same treatment `dataoffset`/`datasize` already get. Bump to it and adjust the front end accordingly. `loadimmutable` therefore stops being one of the solc extensions carried as a bare `.call` and becomes a real built-in: `parse` recognizes it, `specialBuiltin` drops it, it takes one input and one output, and — like the layout built-ins — its argument must be a direct string literal. `setimmutable` stays a `.call`, since it is eliminable at compile time and keeps the code-layout choice on the compiler's side. The immutable-name collector that pairs reads with writes is updated to the new shape. `opTable` still has no row for `.loadimmutable`, so programs reading it remain rejected at lowering; this commit only moves the front end onto the modeled operation. Every `cases op` proof absorbed the new constructor unchanged, and `Checks.lean` still reports exactly the three standard axioms. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The instruction an immutable read compiles to. It pushes the value the environment records for its key — mirroring the source built-in, which reads the same map on the same keying — but always as a full-width `PUSH32`. The fixed width is the entire point. Ordinary `push` takes the minimal `PUSHk` encoding, so its length varies with the value; an immutable's 32 immediate bytes have to sit at an offset the deploying constructor can compute and patch, which means that offset must not depend on the value stored there. `key` carries no runtime meaning: it exists so the object layer can report where each placeholder landed. Carried through both phases, with no `sorry` and no new axiom: - `Asm.size` = 33 and `lowerInstr` emits `Instr.push ⟨32⟩`, with `lowerInstr_length` extended, so every fixed-width location lemma keeps applying; - `AStep.pushImmutable` carries the premise that the baked constant *equals* the environment's recorded value, so a placeholder disagreeing with its layout simply cannot step; - both stack analyses (`StackBound`, `StackScalable`) treat it exactly as `push`; - the peephole can only `keep` it — Lean rejected the `window` branch as unreachable, which is the property we want: folding one would move the bytes the constructor patches; - `LowerCorrect.astep_sim` gains the Phase-B case, discharging the `PUSH32` well-formedness side condition from `v.isLt`. Nothing emits it yet, so compiler behavior is unchanged; `opTable` still has no row for `.loadimmutable` and such programs stay rejected. This is deliberate: emitting it before the simulation existed would have made the theorem vacuous for those programs rather than extending it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… lookups Rebasing onto main brought in the SSA-CFG backend and the bundled certificate API, both of which case on `Asm`. The placeholder behaves exactly as `push` in all of them: same stack effect, and `elideJumps` passes it through untouched.
`builtinWithExternal_immutable_eq` / `AStep.immutable_eq`: 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` of the same shape. None mentions `immutable`.
This is the fact the whole immutables design rests on. It is what lets the
layout-consistency obligation for immutables — the constants baked into the
emitted bytes are the ones the environment records, the exact counterpart of
`Layout.Consistent` for data segments — be stated once and carried along a
whole run rather than threaded as an invariant through the phase A induction.
The `SPEC.md` re-pin is a consequence of consuming powdr-labs/yul-semantics#42,
not of this lemma: `Op` gained a `loadimmutable` constructor, so the four
declarations that case on `Op` change content hash — `IsCallOp`, `IsCreateOp`,
`opTable` and `resolveForLayoutExpr`. No declaration is added or removed and no
theorem statement moves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`loadimmutable`/`setimmutable` now compile. Real solc output uses them in essentially every contract with an immutable, so this removes one of the three features that blocked the aave/uniswap integration fixtures. **Reads.** `loadimmutable(name)` compiles to `Asm.pushImmutable name`, which `lowerProg` emits as a full-width `PUSH32` of the assignment's value. The fixed width is the point: ordinary `push` takes the minimal `PUSHk` encoding, so its length varies with the value, but an immutable's 32 immediate bytes must sit where the deploying constructor can patch them — so that offset must not depend on the value stored there. The instruction names the immutable and nothing else; the *value* is supplied to `lowerProg`. That is what keeps phase A free of any new invariant: `AStep.pushImmutable` pushes what the environment records, matching the source built-in exactly, and the obligation that the emitted bytes agree with the environment lives in phase B's `ConfMatch.imms` — the compiler's layout-consistency obligation for immutables, the exact counterpart of `Layout.Consistent` for data segments. It survives a whole run because no step ever writes `env.immutable` (`AStep.immutable_eq`). **Writes.** `setimmutable(base, name, value)` is *eliminable*: it expands to one `mstore` per recorded placeholder offset, on the optimized tree immediately before `compileObject`, so the object layer and `compileObject_correct` never see the extension — exactly how `linkersymbol` resolution is handled. Offsets come from the plan of the very code that gets emitted, so they are the real ones. One front-end fix was needed: `decodeValueExpr` decodes string literals to words, which silently destroyed the immutable's *name*. Names now stay spelling-sensitive, as they already did for `dataoffset`/`datasize`. Verified: `lake build` clean, `Checks.lean` reports exactly the three standard axioms, no `sorry`. Corpora all exit 0 — interpreter 29/53 (24 known), optimizer 598/643 (45 known), object-compiler 32/36 (4 known), evm-code-transform 44/47 (3 known), syntax 0 mismatches — with more fixtures compiling than before; the one stale baseline entry it clears is, fittingly, `immutable_long_name_does_not_end_up_in_bytecode.yul`. `SPEC.md` re-pinned: `compile` gains the assignment parameter and the four correctness statements gain the consistency hypothesis. Nothing added, nothing removed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three CI gates, all consequences of the feature: - **`SpecClosure.lean`** pins the audited signature as a `#guard_msgs` docstring, which `scripts/update-spec.sh` regenerates alongside `SPEC.md`. I had only regenerated `SPEC.md`, so the closure gate stayed red. Both are now in sync. The moved hashes are `compile` (gains the assignment parameter), the four correctness statements (gain the layout-consistency hypothesis), and `IsCallOp`/`IsCreateOp`/`opTable`/`resolveForLayoutExpr` (`Op` gained a constructor upstream). Nothing added or removed. - **`solidity-semantic-gas-baseline.txt`**: 39 rows added, none changed or removed — `0 regressions, 1 improved`. 16 of the 39 are `immutable/` fixtures that this compiler previously rejected outright. - **object-compiler**: `immutable_long_name_does_not_end_up_in_bytecode.yul` now compiles *and* matches solc, so it leaves the known-differential list and gains a gas row. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adding the immutable assignment to `compile`/`lowerProg` touched ~180 call sites, and I did it with a blanket regex. It also rewrote the word "compile" inside English prose — "compile a complete Yul source program" became "compile zeroImmutables a complete Yul source program", and so on in 25 places across 16 files. Restores every one of those comments, including `Checks.lean`, which the rewrite had no business touching at all: it is a trust-boundary file, and it is now byte-identical to `main` again. Comment-only; the audited surface does not move. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
@codex review |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d50b76651b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| -- per code block); both artifacts are kept and the cheaper bytecode | ||
| -- (static stack-traffic cost) wins. | ||
| let ssaLayout := YulEvmCompiler.SsaCfg.compileObjectViaSsa optimized | ||
| let ssaLayout := YulEvmCompiler.SsaCfg.compileObjectViaSsa (expandSetImmutablesObject optimized) |
There was a problem hiding this comment.
When the SSA object candidate wins, expandSetImmutablesObject has computed every constructor patch offset through objectImmutableOffsets, which uses the classic planObject, while compileObjectViaSsa emits independently scheduled SSA bytecode and planAttemptWith leaves immOffsets := []. If SSA changes the width or order of any code preceding a loadimmutable, the constructor writes to the classic position rather than the SSA placeholder, leaving the immutable zero and potentially overwriting unrelated runtime bytes. Compute offsets from the same backend artifact that is selected, or exclude immutable-bearing objects from SSA selection.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed and fixed in 4c409a8 — this was a live miscompilation, not a missed optimization.
objectImmutableOffsets reads the offsets off the classic planObject, while compileObjectViaSsa goes through planAttemptWith, which leaves immOffsets := []. So when the SSA artifact won, the constructor patched at the classic backend's positions in SSA-scheduled bytes.
The fix withholds the SSA object candidate whenever the tree touches an immutable (usesImmutablesObject), so the artifact that wins is always the one the offsets were computed from.
It was reaching emitted bytecode. CI then reported a gas "regression" on immutable_long_name_does_not_end_up_in_bytecode.yul: ours 54 against a pinned 0, solc 54. The pinned 0 had been measured from the broken artifact — spending no gas is what the mispatch looked like from outside, on a fixture whose whole purpose is that the immutable's value reaches the runtime. With the candidate withheld we emit 54, exactly solc's figure, and the baseline is re-pinned in fde8cf2.
Separately, 72e3a57 makes the offsets a theorem so this class of bug cannot recur silently:
theorem immutableOffsets_correct (hlow : lowerProg imm p = some is)
(hmem : (key, off) ∈ immutableOffsets p 0) :
((assembleBytes is).drop off).take 32 = natToBE (conv (imm key)).toNat 32Re-enabling SSA for immutable-bearing objects is now a matter of having planAttemptWith record offsets from its own artifact; deliberately left out of this PR.
| let offsets := | ||
| subs.flatMap fun sub => | ||
| (YulEvmCompiler.objectImmutableOffsets sub).getD [] | ||
| .mk name (YulEvmCompiler.expandSetImmutablesStmts offsets code) subs segs |
There was a problem hiding this comment.
For every source containing setimmutable, this rewrites the parsed object before invoking compileObject, but setimmutable remains an unmodeled special .call and no semantic-preservation theorem relates the original object to expandSetImmutablesObject. Consequently, compileObject_correct proves only the generated mstore program, not the source accepted by compileSource; either add a dedicated source semantics and end-to-end theorem for this expansion or keep these inputs rejected.
AGENTS.md reference: AGENTS.md:L75-L75
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
You are right that there is no semantic-preservation theorem here, and that was under-stated. I have not gated setimmutable, but I have split the claim in two and made the load-bearing half a theorem — here is the reasoning, so the residue can be judged deliberately.
What the expansion can and cannot be. setimmutable is not an Op, so a source object containing it has no RunObject derivation — there is no source run to preserve, and compileObject_correct is vacuous for it either way. Rejecting it and expanding it are therefore not "unproved vs proved"; they are "no immutables" vs "the theorem covers the desugared program". This is the same shape as memoryguard, which is likewise desugared with no preservation theorem, and it is now said outright in the module doc and README.md rather than implied.
What actually carried risk was the offsets, not the meaning. The rewrite asserts that writing 32 bytes at offset X of the in-memory code copy is right; nothing checked X. That is exactly how the SSA/classic mismatch you flagged in the sibling comment slipped through the build. 72e3a57 closes it:
theorem immutableOffsets_correct (hlow : lowerProg imm p = some is)
(hmem : (key, off) ∈ immutableOffsets p 0) :
((assembleBytes is).drop off).take 32 = natToBE (conv (imm key)).toNat 32Every offset the expansion patches provably locates that immutable's immediate in the emitted code. Proved by induction over the fragment against lowerFrag — no semantics involved, since it is purely about where lowering puts things.
So: the silent-miscompilation class is gone; what remains unproved is setimmutable's meaning, which needs it modeled upstream in yul-semantics. That is recorded as the next step rather than left implicit.
| name = "yul-semantics" | ||
| git = "https://github.com/powdr-labs/yul-semantics" | ||
| rev = "4c6f9753cc0e5850f6bdaf6fb0df76457204699a" | ||
| rev = "90b33d7475e0c4fb2f67b72f3e151164ae8b4d6f" |
There was a problem hiding this comment.
This automated change bumps the pinned yul-semantics revision and also updates lake-manifest.json, SpecClosure.lean, and SPEC.md. These files define the audited external/specification boundary and are explicitly human-approval-only, so the feature change must stop at the boundary and have a maintainer separately review and repin these artifacts.
AGENTS.md reference: AGENTS.md:L316-L323
Useful? React with 👍 / 👎.
| -- 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) |
There was a problem hiding this comment.
This newly accepts loadimmutable, yet the current user-facing documentation still says that immutables are unsupported in README.md lines 328-329 and DESIGN.md lines 708-709. That sends users diagnosing stack-spill failures in the wrong direction and leaves the documented proof scope inconsistent with the implementation; update both documents as required for a supported syntax/scope change.
AGENTS.md reference: AGENTS.md:L340-L340
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Fixed in 4c409a8. Both documents said immutables were unsupported, which is exactly the wrong signal for someone diagnosing a spill failure.
README.md now has an Immutables entry describing the fixed-width PUSH32 placeholder, the front-end desugaring of setimmutable, and — kept explicit — which half is proved: the offsets (immutableOffsets_correct) and the layout-consistency obligation (ConfMatch.imms) are theorems, while setimmutable's meaning is not, since it has no source semantics.
DESIGN.md's spilling section no longer lists immutables and linker symbols among the operations spilling cannot rescue; it now points at their own entries and notes that neither is a consequence of spilling.
… it honestly Two problems with how the assignment was threaded, both mine. **It was `compile`'s first parameter**, so every existing call site had to name it — 40-odd `#guard`s and examples turned from `compile sumLoop` into `compile zeroImmutables sumLoop`, pure noise in files that have nothing to do with immutables. Moving it last, with a default, restores every one of them. Only code that genuinely supplies an assignment mentions one now: the two correctness statements and the backend instances. **The constant was called `zeroImmutables`**, which reads as "this compiler has no immutables". It is the opposite: the placeholders *are* emitted, and `immutableOffsets` records where — the assignment is what fills them *before* the deploying constructor patches the real values in. Renamed to `unpatchedImmutables` and documented as such. This also finishes repairing the blanket-regex damage: two occurrences had been rewritten inside *string literals* (`"Contracts that failed to compile …"` in the gas runner, and an IR-corpus error message), which the comment-only pass missed. `SPEC.md`/`SpecClosure.lean` re-pinned: the audited surface gains `unpatchedImmutables` (data defs 51 → 52) because `compile`'s default now references it, which usefully pins that the default is the all-zero map. `Checks.lean` remains byte-identical to `main`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…'s scope **Bug (Codex P1).** The constructor's patch offsets are read off the *classic* plan via `objectImmutableOffsets`, but the SSA object path schedules its code independently and `planAttemptWith` records no offsets at all. A winning SSA artifact would therefore be patched at the classic backend's positions — a miscompilation, not merely a missed optimization. Withhold the SSA object candidate whenever the tree touches an immutable, so the artifact that wins is always the one the offsets were computed from. **Scope (Codex P1).** `setimmutable` has no source semantics, so no semantic-preservation theorem relates the original object to the expanded one: the correctness theorem covers the *desugared* program. That was implied before and is now said outright, in the module doc and in `README.md`. It is a front-end desugaring in the same family as `memoryguard`, not a proved `Optimizer.Pass`; proving it needs `setimmutable` modeled upstream. **Docs (Codex P1).** `README.md` and `DESIGN.md` still listed immutables as unsupported. Both now describe what is accepted and on what terms. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`setimmutable` patches the emitted bytes at the offsets `immutableOffsets`
reports, and nothing checked that those offsets were right — a wrong one is a
silent miscompilation with no theorem to catch it. That is not hypothetical:
the SSA/classic offset mismatch fixed in the previous commit was exactly this
failure mode, found by review rather than by the build.
`immutableOffsets_correct` closes it. For an accepted program, every offset
reported for an immutable really does locate that immutable's 32-byte immediate
in `assembleBytes`:
lowerProg imm p = some is →
(key, off) ∈ immutableOffsets p 0 →
((assembleBytes is).drop off).take 32 = natToBE (conv (imm key)).toNat 32
Proved by induction over the fragment against `lowerFrag`, using
`lowerInstr_length` to step over each instruction's bytes — no semantics
involved, since this is purely a statement about where lowering puts things.
This does not prove what `setimmutable` *means* — it has no source semantics, so
the correctness theorem still covers the desugared program. But it removes the
class of bug that can actually bite, and the docs now separate the two claims
instead of blurring them.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CI reported a gas "regression" on `immutable_long_name_does_not_end_up_in_bytecode.yul`: ours 54 against a pinned 0, with solc at 54. The pinned 0 was measured before the SSA object candidate was withheld — that is, from the artifact patched at the *classic* backend's offsets while the SSA backend had emitted the bytes. Spending no gas is what that miscompilation looked like from the outside; the fixture's whole point is that the immutable's value reaches the runtime. With the candidate withheld, ours is 54 — exactly solc's figure. So this is the correctness fix surfacing in the numbers, and the baseline was recording the broken behavior. Re-pinned to 54; no other row in any suite moves. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fde8cf2ff6
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| let offsets := | ||
| subs.flatMap fun sub => | ||
| (YulEvmCompiler.objectImmutableOffsets sub).getD [] |
There was a problem hiding this comment.
When two direct child objects use the same immutable name but place its PUSH32 at different offsets, this flatMap merges both offset lists and every setimmutable(base, name, value) emits stores for both lists relative to the single base. Patching a copy of one child therefore also writes at the sibling's offsets, potentially overwriting that child's executable bytes. The validator permits duplicate immutable names across siblings, so either retain the child association when selecting offsets or reject this ambiguous input.
AGENTS.md reference: AGENTS.md:L75-L75
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed and fixed in 0e068a2. Reproduced first:
object "A" {
code { let s := datasize("B") codecopy(0, dataoffset("B"), s)
setimmutable(0, "x", caller()) return(0, s) }
object "B" { code { sstore(0, loadimmutable("x")) } }
object "C" { code { sstore(1, 1) sstore(2, 2) sstore(3, loadimmutable("x")) } }
}emitted two stores — 6001 82 01 52 and 600b 82 01 52, offsets 1 and 11 — while copying only B. B is ~35 bytes, so the second wrote 32 bytes at offset 11 straight over its code, exactly as you describe.
The name is now left unexpanded when more than one child declares it, so the raw .call "setimmutable" reaches the backend and the program is rejected.
Worth recording that filtering the ambiguous name out of the offset list is not sufficient, which is what I tried first: the expansion then produced a block with zero stores, so the immutable stayed zero — the same silent miscompilation wearing a different hat. The rejection has to be explicit, so expandSetImmutablesStmts now takes the ambiguous names and keeps the original statement for them.
Retaining the child association instead — your first suggestion — would be the better long-term fix, since it also lets sibling objects legitimately share a name. It needs setimmutable to identify which child base refers to, which the source does not say, so I took the conservative route here and left it noted.
#guards pin both the rejection and that ordinary single-child immutables still compile.
| 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 |
There was a problem hiding this comment.
For a block-root source such as { sstore(0, loadimmutable("x")) }, this branch accepts the expression, but validateBlockSource performs no matching-setimmutable check and the block arm of compileSource invokes compile with unpatchedImmutables. The resulting bytecode therefore silently hard-codes zero for every immutable rather than rejecting a source for which compileSource has no assignment mechanism; restrict this acceptance to object validation or reject block-root immutable reads.
AGENTS.md reference: AGENTS.md:L75-L75
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed and fixed in 0e068a2. { sstore(0, loadimmutable("x")) } compiled to
7f 0000…0000 5f 55 -- PUSH32 <zero> ; SSTORE
a hard-coded zero with no mechanism that could ever set it, exactly as you describe.
One correction to the suggested placement, which I hit by taking it literally first. Putting the check in validateBlockSource — "restrict this acceptance to object validation" — makes the grammar reject it, and upstream's syntax corpus has a loadimmutable.yul fixture that must still parse. That turned into a false reject:
Checked 319 Solidity Yul syntax tests: … 1 known parser mismatches (0 false accepts, 1 false rejects)
So the check now lives in compileSource's block arm instead: the program parses, and compilation returns none. That is the right layer anyway — this is a limitation of having no object tree to patch, not a syntax rule. Syntax corpus is back to 0 false accepts, 0 false rejects.
#guards pin both halves: parseSource still accepts it, compileSource rejects it.
Both from review, both reproduced before fixing.
**Sibling objects declaring the same immutable.** `setimmutable(base, name, value)`
names no child, and `base` points at a copy of *one* of them, but the expansion
merged every child's offsets. A tree with `B` and `C` both reading `"x"` emitted
two `mstore`s — at offsets 1 and 11 — while copying only `B`, so patching `B`
wrote 32 bytes at `C`'s offset, over `B`'s own code. Such a name is now left
unexpanded so the backend rejects the program.
Filtering the ambiguous name out of the offset list is *not* enough, and the
first attempt at this got it wrong: it then expanded to zero stores, leaving the
immutable at zero just as silently. Rejection has to be explicit.
**Block-rooted `loadimmutable`.** `{ sstore(0, loadimmutable("x")) }` compiled to
a hard-coded `PUSH32 0`: a block root has no object tree, so nothing can ever
patch the placeholder, and the block arm compiles against `unpatchedImmutables`.
Now rejected.
That check belongs in compilation, not parsing — upstream's syntax corpus has a
`loadimmutable.yul` fixture that must still *parse*. Putting it in
`validateBlockSource` turned that into a false reject; it now sits in
`compileSource`, and the syntax corpus is back to 0 mismatches.
Guards pin all three shapes. Corpora: syntax 0 mismatches, interpreter 29/53,
optimizer 600/643, object-compiler 32/36, evm-code-transform 44/47 — known
failures only.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review status — all six findings addressedEvery inline thread has a reply with detail; this is the summary. Two Codex rounds found four genuine bugs, three of them silent miscompilations that
The bugs were real, and one was already pinned into a baselineFinding 1 reached emitted bytecode. After fixing it, CI reported a gas regression on What is proved, and what is notThe offsets are no longer trusted — lowerProg imm p = some is →
(key, off) ∈ immutableOffsets p 0 →
((assembleBytes is).drop off).take 32 = natToBE (conv (imm key)).toNat 32Every offset Still unproved: Two corrections worth carrying forward
Local verification
Corpora: syntax 0 mismatches · interpreter 29/53 · optimizer 600/643 · object-compiler 32/36 · evm-code-transform 44/47 — known failures only. ScopeThis does not make the aave/uniswap fixtures compile. They also need |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0e068a2b75
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| let perChild := subs.map fun sub => | ||
| (YulEvmCompiler.objectImmutableOffsets sub).getD [] |
There was a problem hiding this comment.
When one child reads loadimmutable("x") but an unrelated sibling contains the only setimmutable(..., "x", ...), object validation accepts the tree because it matches names globally. This expansion gives the sibling setter no offsets, so it becomes an empty block, while the reading child's emitted PUSH32 remains zero; a root that copies and returns that child therefore silently deploys the wrong immutable value. Track reads and setters by object scope, or reject any reader that cannot be patched by its parent.
AGENTS.md reference: AGENTS.md:L75-L75
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed and fixed in 3d4e4c4. Reproduced exactly as described:
object "A" {
code { let s := datasize("B") codecopy(0, dataoffset("B"), s) return(0, s) }
object "B" { code { sstore(0, loadimmutable("x")) } }
object "C" { code { setimmutable(0, "x", caller()) stop() } }
}A copies and returns B, A's constructor emits no mstore at all, and C's setter expands against C's own children — of which there are none — so it collapses to 33 5f 50 50 (CALLER; PUSH0; POP; POP), patching nothing. B deploys with 7f 0000…0000 intact.
You named the root cause precisely: validation pairs reads with writes globally, but an immutable is patched by the parent of the object that reads it, since the parent is what copies that code into memory. I took the second of your two options — reject any reader its parent cannot patch — checked per scope during expansion:
let written := (collectImmutableCallsStmts code).2
if !(perChild.flatten.all fun p => written.contains p.1) then none else …expandSetImmutablesObject is now Option-valued and every candidate in compileSource's object chain binds through it, so the whole tree is rejected rather than any one candidate silently succeeding.
Tracking reads and setters by scope in the validator — your first option — would give a better diagnostic, but I kept the check in compilation deliberately: the same instinct applied to the block-root case in the sibling thread turned upstream's loadimmutable.yul syntax fixture into a false reject. This is a compilation limit, not a syntax rule.
A #guard pins the rejection; corpora are unchanged (syntax 0 mismatches, interpreter 29/53, optimizer 600/643, object-compiler 32/36, evm-code-transform 44/47).
That is now three distinct silent-miscompilation shapes in this expansion found by review — wrong-backend offsets, merged sibling offsets, and cross-scope setters — none of which the build, Checks.lean, or any corpus caught. Noted in the PR summary as the honest weak point: the offsets are a theorem, but the scoping around them is validated, not proved.
Reproduced first:
object "A" {
code { let s := datasize("B") codecopy(0, dataoffset("B"), s) return(0, s) }
object "B" { code { sstore(0, loadimmutable("x")) } }
object "C" { code { setimmutable(0, "x", caller()) stop() } }
}
`A` copies and returns `B`, but `A`'s constructor emits no `mstore` at all —
`C`'s setter expands against `C`'s own children, of which there are none, so it
becomes dead code — and `B` deploys with its placeholder still zero.
Validation pairs reads with writes *globally* across the tree, which is too
weak: an immutable is patched by the **parent** of the object that reads it,
because the parent is what copies that object's code into memory. The pairing is
now re-checked per scope during expansion, and a tree where some child reads an
immutable its parent never sets is rejected.
`expandSetImmutablesObject` is therefore `Option`-valued, and every candidate in
`compileSource`'s object chain binds through it.
Corpora unchanged: syntax 0 mismatches, interpreter 29/53, optimizer 600/643,
object-compiler 32/36, evm-code-transform 44/47 — known failures only.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3d4e4c4916
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| 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 |
There was a problem hiding this comment.
When the root object's own code contains loadimmutable("x") and a matching setimmutable, validation succeeds, but this check considers only perChild offsets and never rejects or patches the current object's placeholders. Because the root has no parent to patch its code, the emitted PUSH32 remains zero; for example, a root that stores its own loadimmutable("x") result silently stores zero despite the setter. Reject immutable reads in the root code or provide an assignment mechanism for them.
AGENTS.md reference: AGENTS.md:L73-L75
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed and fixed in c65c6b2.
Reproducer:
object "A" { code { setimmutable(0, "x", caller()) sstore(0, loadimmutable("x")) stop() } }compiled (exit 0) to 33 5f 50 50 7f 00…00 5f 55 — the setter collapses to CALLER POP POP because there is no child to patch, and the root's own placeholder stays zero, so it stores 0 instead of the caller. Exactly as you describe: my scope check only inspected perChild, and the root has no parent.
The fix rejects a loadimmutable in the root object's own code, mirroring the block-root rejection already in compileSource. The root can never be patched by anything, so no set of setters makes such a read meaningful. #guard added.
| return .mk name | ||
| (YulEvmCompiler.expandSetImmutablesStmts offsets ambiguous code) subs segs |
There was a problem hiding this comment.
When base or value is an escaped string literal, this expansion receives the escape-preserving spelling rather than its Yul word value: decodeValueExpr treats every argument of the pre-existing literalNameCall "setimmutable" case as name-valued and skips decodeValueArgs. Thus inputs such as setimmutable(0, "x", "\x01") patch the placeholder with the word derived from the characters of the escape spelling instead of byte 0x01; preserve only the middle name argument and decode the first and third arguments normally.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Confirmed and fixed in c65c6b2.
setimmutable(0, "x", "\x01") patched in bytes 5c 78 30 31 — the ASCII characters \, x, 0, 1, i.e. the escape spelling — instead of byte 0x01. decodeValueExpr's literalNameCall branch was skipping decoding for all three arguments, but only the middle one names the immutable; the target and the stored value are ordinary expressions.
Now only the name keeps its spelling. Verified "\x01" and hex"01" produce byte-identical bytecode (7f 01 00…00), and #guarded on that equality rather than on a hard-coded byte string.
Two silent-miscompilation shapes found in review, both reproduced before
fixing:
* A `loadimmutable` in the **root** object's own code compiled to a
`PUSH32 0` that nothing could ever patch: the root has no parent to
copy and patch it, so however many setters the tree contains, the read
returns zero. `object "A" { code { setimmutable(0, "x", caller())
sstore(0, loadimmutable("x")) stop() } }` stored zero. Now rejected,
mirroring the existing block-root rejection in `compileSource`.
* `decodeValueExpr` skipped escape decoding for *all three* arguments of
`setimmutable`, but only the middle one names the immutable — the
target and the stored value are ordinary expressions. `setimmutable(0,
"x", "\x01")` patched in bytes `5c 78 30 31`, the ASCII characters of
the escape spelling, instead of byte `0x01`. Now only the name keeps
its spelling; `"\x01"` and `hex"01"` compile identically.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
@codex review |
|
Codex Review: Didn't find any major issues. Chef's kiss. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
1 participant
Immutables compile.
loadimmutable/setimmutableappear in essentially every real solc contract with an immutable, so this removes one of the three features blocking the aave/uniswap integration fixtures.Consumes two merged yul-semantics changes: #42 (
loadimmutablemodeled as a read ofExecEnv.immutable, keyed likedataoffset/datasize) and #43 (Layoutcarries that map — #42 had left it missing, so under any layout the read returned zero and a compiler had no way to state what its code does).Reads
loadimmutable(name)compiles toAsm.pushImmutable name, emitted bylowerProgas a full-widthPUSH32of the assignment's value.The fixed width is the whole point. Ordinary
pushtakes the minimalPUSHkencoding, so its length varies with the value — but an immutable's 32 immediate bytes have to sit where the deploying constructor can compute and patch them, so that offset must not depend on the value stored there.The instruction names the immutable and nothing else; the value is supplied to
lowerProg. That is what keeps phase A free of any new invariant:AStep.pushImmutablepushes what the environment records, matching the source built-in exactly, so the simulation is immediate. The obligation that the emitted bytes agree with the environment then lives in phase B, where the bytes exist:This is the compiler's layout-consistency obligation for immutables — the exact counterpart of
Layout.Consistentfor data segments. It survives a whole run because no step ever writesenv.immutable: 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 aCallWorldof the same shape (AStep.immutable_eq, proved here).Writes
setimmutable(base, name, value)is eliminable: it expands to one ordinarymstoreper recorded placeholder offset. The expansion runs on the optimized tree immediately beforecompileObject, so the object layer, its layout-resolution proof andcompileObject_correctnever see the extension — exactly howlinkersymbolresolution is handled. Offsets come from the plan of the very code that gets emitted, so they are the real positions, not an approximation.Concretely, for a constructor storing
caller():base+1is precisely where thePUSH32immediate begins.One front-end fix was required:
decodeValueExprdecodes string literals to words, which silently destroyed the immutable's name. Names now stay spelling-sensitive, as they already did fordataoffset/datasize.Verification
lake buildclean;Checks.leanreports exactlypropext,Classical.choice,Quot.sound; nosorry, no new axiom.All corpora run locally, all exit 0, with more fixtures compiling than before:
The one stale baseline entry cleared is, fittingly,
immutable_long_name_does_not_end_up_in_bytecode.yul.#guards pin the constructor/deployed pair compiling, aloadimmutablewith no matchingsetimmutablebeing rejected, andsetimmutablealone being a no-op patch.Spec
SPEC.mdre-pinned.compilegains the assignment parameter and the four correctness statements gain the consistency hypothesis;IsCallOp/IsCreateOp/opTable/resolveForLayoutExprchange hash becauseOpgained a constructor upstream. Nothing added, nothing removed.Scope
This does not make the aave/uniswap fixtures compile on its own — they also need
gas()(see #148 for why that is blocked) and, for three of them, a further stack-pressure blocker.🤖 Generated with Claude Code