Library linking, the gas() oracle prerequisite, and what actually blocks the aave/uniswap fixtures

[leonardoalt]

Draft. Depends on powdr-labs/yul-semantics#41 (this branch pins the commit from
that PR in lakefile.toml / lake-manifest.json, which are normally
human-approval-only — please review that bump explicitly).

What this delivers

1. Live library linking (linkersymbol) — complete.
compileSource takes an optional LinkEnv, the same file.sol:Lib = 0xADDR
information solc's --libraries carries; yulc exposes it as
--libraries=NAME=0xADDR[,…]. Resolution is a substitution on the source
program before the optimizer or backend run, so the correctness statement does
not move — it is about the linked program, the way dataoffset/datasize
resolution makes it about the concrete layout. A #guard pins that the linked
program compiles to exactly the bytecode of the program with the address
written out by hand. Unresolved occurrences keep today's behavior: pruned when
provably dead, rejected otherwise — never given a default address.

2. The gas() oracle, threaded — prerequisite only.
ExternalModel gains a gas field defaulting to ExternalGas.any, exactly
the oracle every theorem here was implicitly stated against, so nothing is
weakened. The one non-mechanical part: GuardedExternals gains
gas_insensitive, because guarded spilling transports a built-in across states
differing only in compiler-owned scratch bytes, and with the oracle a parameter
what it reports must demonstrably not depend on those bytes — exactly as
already required of the call and creation relations.

lake build is clean; lake env lean Checks.lean still reports exactly
propext, Classical.choice, Quot.sound for every headline theorem. No
sorry, no new axiom.

What this does not deliver, and why

The goal was to make test/aave-v4/{HubOperations,LiquidationLogic,SpokeOperations}.sol
and test/uniswap-v4/PoolManager.sol compile. Three findings changed that plan.

Finding 1 — it is three features, not two

Extracting solc's --ir for each fixture and mapping the object trees: every
one needs gas() (5–147 uses) and immutables (setimmutable in each
constructor object, loadimmutable in the matching _deployed object, in the
top-level pair and in nested CREATE'd objects) and, for two of them, live
linkersymbol. PoolManager and HubOperations turn out to be fully covered
by the existing dead-binding pruner; only LiquidationLogic (2 sites) and
SpokeOperations (11 sites) have genuinely live ones.

Finding 2 — gas() cannot enter the fragment under the current theorem

This is the blocker, and it needs a human decision.

Pinned yul-semantics modeled gas() as an unconstrained oracle (∃ g).
yul-semantics#41 makes that a parameter, which is necessary — but not
sufficient. The obligation a target realization has to discharge is: given a
source derivation that already picked g, produce a target run yielding g.
The target's GAS pushes s.gasAvailable - 2. Any oracle expressible as a
relation on the source state cannot pin that, because StateMatch yst s
admits many s with different remaining gas. So a GasRealized in the shape
of CallsRealized/CreatesRealized is satisfiable only by ExternalGas.none,
i.e. vacuously — which would silently hollow out compile_correct rather than
extend it. I stopped rather than land that.

The routes I can see, none of them small:

• (a) Source-side gas. Give EvmState an abstract gas component so
  StateMatch can relate it to the target. Contradicts yul-semantics
  DESIGN.md §1 ("gas is not modeled anywhere") and makes every built-in
  responsible for keeping it in sync.
• (b) Refinement. Restate correctness as a backward simulation for
  gas-reading programs, where the target's actual gas is one of the source's
  admitted choices. Fits ExternalGas.any naturally; a large theorem change.
• (c) Fuse the call pattern. Every one of the 154 gas() occurrences across
  all four fixtures is directly the first argument of
  call/staticcall/delegatecall — no exceptions. So call(gas(), …) could
  be compiled as a unit under a GasInsensitive hypothesis on the external
  relation (the response must not depend on the forwarded amount). The catch:
  ANF normalization rewrites this to let g := gas() … call(g, …) before the
  backend sees it, so the pattern would have to be recognized after the
  optimizer, or protected through it.

My preference is (c) if the ANF interaction can be contained, else (b). I did
not want to pick unilaterally — it moves the audited specification surface.

Finding 3 — the three features are not sufficient anyway

Control experiment: I textually stubbed all three features out of each
fixture's extracted IR (gas()→0, linkersymbol(…)→0,
loadimmutable(…)→0, setimmutable(…) deleted) and fed the result to
yulc. Three of the four still fail (exit=2 — parsed, unsupported feature):

fixture	stubbed compile	time
LiquidationLogic	REJECT	1252 s
PoolManager	REJECT	307 s
HubOperations	REJECT	420 s
SpokeOperations	REJECT	979 s

All four. So there is at least one further blocker per fixture, and "after this
PR everything compiles" was not reachable from immutables + linking + gas
alone, whatever we decide about gas().

Bisecting by sub-object, on the stubbed sources:

object	result	time
LiquidationLogic → PreviewHub_9270 (+ its child)	OK	0.13 s
LiquidationLogic → AGasTest_9431_deployed	OK	1216 s
PoolManager → TestToken_9344 (+ its child)	OK	0.12–0.16 s
PoolManager → PoolRouter_9288 (+ its child)	OK	2.6–2.7 s
PoolManager → AGasTest_8990_deployed	REJECT	229 s

The two fixtures fail for different reasons.

LiquidationLogic: a layout-key collision (root-caused, 12-line reproducer)

Every sub-object compiles, yet the assembled tree is rejected. Narrowing:
replacing the 190 KB runtime with code { stop() } still rejects, in 0.53 s
instead of 21 minutes; the top-level creation code alone compiles; a minimal
Wrap around the real PreviewHub_9270 subtree reproduces it.

object "Wrap" {
  code { stop() }
  object "PreviewHub_9270" {
    code { let s := datasize("PreviewHub_9270_deployed")
           datacopy(0, dataoffset("PreviewHub_9270_deployed"), s) return(0, s) }
    object "PreviewHub_9270_deployed" { code { sstore(0, 1) }
      data ".metadata" hex"a2646970667358221220"
    }
  }
}

compileResolvedObject keys every layout entry by litValue (.string name),
which holds only 32 bytes. At nesting depth ≥ 2 shiftChildEntries builds
compiler-internal qualified names, so the grandchild and its data segment
become

"PreviewHub_9270.PreviewHub_9270_deployed"            (40 bytes)
"PreviewHub_9270.PreviewHub_9270_deployed..metadata"  (50 bytes)

which share the 32-byte prefix PreviewHub_9270.PreviewHub_9270_. Their keys
collide, (plan.entries.map entryKey).Nodup fails, and the whole tree is
rejected. Pinned by a three-way discrimination — it needs two overflowing
keys, not one:

object / grandchild names	key lengths	result
long / short	18, 28	OK
short / long	26, 36 (one overflows)	OK
long / long	40, 50 (two overflow, same prefix)	REJECT

This is the name-aliasing caveat yul-semantics documents for string-literal
keying, reached by compiler-generated names rather than source ones — and it
fires on essentially every real contract, since solc always emits .metadata
and its object names (Contract_1234/Contract_1234_deployed) exceed 32 bytes
once qualified.

Fixed (shiftChildEntries): a qualified name whose key is not
representable is dropped rather than allowed to poison the tree. Such a name is
unusable anyway — litWF (.string s) requires s.toUTF8.size ≤ 32, so the
validator rejects any dataoffset/datasize naming it — so this removes only
dead weight. A program that does reference the name still fails to resolve and
is rejected, exactly as before, rather than being miscompiled. Direct data
segments come from dataEntries and are untouched, so Layout.Consistent
(which quantifies over an object's direct segments) is unaffected and the
object proofs went through unchanged; Checks.lean still reports exactly
the three standard axioms.

The reduced tree and the already-working short-name variant are pinned as
#guards. Confirming the diagnosis: keeping the real 190 KB runtime and
stubbing only the PreviewHub subtree already compiled (15304 bytes, 1081 s),
so for LiquidationLogic this key collision was the sole blocker — there is
no stack-pressure problem in that fixture at all.

PoolManager: a genuinely rejecting object

AGasTest_8990_deployed rejects on its own. Not recursion (zero call-graph
cycles), not msize or verbatim (zero occurrences), not a missing
reservation (it carries solc's memoryguard(128)). The visible difference from
the objects that compile is live-local count — PoolRouter_9288_deployed has
310 lets and compiles, this has 5657 and does not — which points at stack
pressure guarded spilling does not fully resolve. Whether the layout-key bug
also contributes here is untested.

Immutables

Not implemented. The design I had worked out, for the record: a dedicated
Asm.pushImmutable placeholder (fixed PUSH32 width, opaque to the peephole
and to source-level constant folding, which a magic-literal encoding would
not be), offsets collected from the child object's compiled layout in
planAttempt, and setimmutable(base, k, v) expanded into one mstore per
recorded offset in the parent's code. That much is ordinary Yul and reuses the
existing proofs; the new obligation is relating the returned patched deployed
bytes to the compilation of the program with loadimmutable(k) replaced by the
stored value.

Immutables are independent of Finding 3 — nothing about stack pressure
prevents implementing them. The only consequence of Finding 3 is that finishing
them will not by itself flip any fixture from REJECT to OK, since those same
objects are also rejected for pressure. (The one real interaction runs the
other way and is second-order: expanding setimmutable into one mstore per
recorded offset adds a few locals to the constructor object.)

Suggested next steps

1. Decide the gas() route (a/b/c above) — that unblocks the largest piece.
2. Let me finish the LiquidationLogic bisection to name the residual blocker
   precisely, so we know the true size of "everything compiles".
3. Immutables, once 1 and 2 are settled.

🤖 Generated with Claude Code

[github-actions]

CI summary — 🔴 Soundness unverified (build failed)

_{head 6f469367e · main b3ca1940a}

1. Parsing

• Syntax corpus: no result captured.
• Interpreter corpus: no result captured.

2. Correctness

• No correctness results captured.

3. Gas

• No gas results captured.

4. Compiler runtime (informational)

• No compiler runtime captured.

5. Soundness (formal guarantee)

• 🔴 Build failed before soundness checks ran — guarantee unverified.

6. Verdict

🔴 Soundness unverified (build failed)

See the failing job logs above for details.

[leonardoalt]

Superseded by the split, per review-sequencing with gas() parked:

• Drop unrepresentable qualified layout entries instead of rejecting the object tree #144 — object-layout-key-fix (standalone, no semantics change)
• Resolve live linkersymbol against a supplied library link map #145 — library-linking (standalone, no semantics change)

The remaining commit here — threading the ExternalGas oracle through the
compiler — is parked together with powdr-labs/yul-semantics#41 until the
gas() design question is settled. Dropping it also removes the
lakefile.toml / lake-manifest.json bump, so neither of the two split PRs
touches the pinned semantics.

The investigation write-up in this description (what actually blocks the four
aave/uniswap fixtures, and why gas() cannot enter the fragment under the
current forward-simulation theorem) is kept here for reference.