Resolve live linkersymbol against a supplied library link map

[leonardoalt]

Standalone. No dependency on any other PR and no change to the pinned semantics.

Why

A used linkersymbol("file.sol:Lib") is solc's placeholder for the address a
linker substitutes — the delegatecall target of a public/external library
function. With no linker there is no sound value for it, so compileSource
pruned the provably dead bindings and rejected everything else. Real Solidity
that calls an external library therefore could not be compiled at all.

In the in-repo fixtures this is not hypothetical: test/aave-v4/SpokeOperations.sol
has 11 live occurrences and test/aave-v4/LiquidationLogic.sol has 2. (The
existing pruner already covers PoolManager and HubOperations entirely — all
of their occurrences are dead placeholders.)

What

compileSource takes an optional LinkEnv — exactly the file.sol:Lib = 0xADDR
information solc's own --libraries flag carries — and yulc exposes it as
--libraries=NAME=0xADDR[,…] (splitting on the last =, since a library name
may itself contain :).

Resolution is a substitution on the source program, run before the optimizer
or the backend see anything: afterwards linkersymbol no longer occurs and what
is compiled is ordinary Yul. So the correctness statement does not move — it is
about the linked program, the same way dataoffset/datasize resolution
makes it about the concrete layout, and a different link map is a different
program.

Unresolved occurrences keep today's behavior exactly: pruned when provably dead,
rejected otherwise. No program is ever given a default address.

The second commit guards both paths on libraries.isEmpty, because the
substitution is an expensive identity on the default configuration and the
corpus runners feed this entry point megabytes of generated Yul.

Verification

• lake build clean; lake env lean Checks.lean still reports exactly
  propext, Classical.choice, Quot.sound.
• #guards pin: the used form compiles when linked, a different library is
  still rejected, and — the important one — the linked program compiles to
  exactly the bytecode of the program with the address written out by hand.
• End to end, yulc --libraries=file.sol:L=0xdead…beef on a delegatecall
  through a library emits …73 deadbeef…beef …f4… (PUSH20, DELEGATECALL),
  while the same file without the flag is still rejected.

🤖 Generated with Claude Code

[github-actions]

CI summary — ✅ All good

_{head 33a35ace0 · main b01ab78a6}

1. Parsing

• Syntax corpus: 106 expected successes, 213 expected failures over 319 tests; 0 known mismatches (0 false accepts, 0 false rejects).
  • Δ vs main: successes 0, expected failures 0, mismatches 0.
• Interpreter corpus: 28/53 passed (25 failed, 25 known; 1 skipped).
  • Δ vs main: passed 0, failed 0, known 0.

2. Correctness

Compilation (positive corpora):

corpus	compiled	Δ compiled	failed	Δ failed	known
EVM-code-transform	43/47	0	4	0	4
object-compiler	30/36	0	6	0	6
optimizer	593/643	0	50	0	50

Behaviour differential vs solc:

corpus	matched	Δ matched	failed	Δ failed	known
EVM-code-transform	42/47	0	5	0	5
object-compiler	21/36	0	15	0	15
optimizer	587/643	0	56	0	56

3. Gas

a) This compiler vs solc's optimized output — we compile solc's unoptimized --via-ir Yul; solc is fully optimized (--optimize --via-ir). The uniswap-v4 and aave-v4 corpora are real protocol code and upstream-derived scenarios (see test/uniswap-v4 and test/aave-v4).

corpus	compiled	comparable	our gas	Δ vs main	solc gas	ours/solc	Δ ratio vs main	regr	impr
aave-v4	1/4	10	16,733,564	0	18,236,226	91.8%	0.0 pp	0	0
gasTests	12/12	12	398,152	0	336,827	118.2%	0.0 pp	0	0
semanticTests	1322/1652	1263	182,391,188	0	170,710,935	106.8%	0.0 pp	0	0
uniswap-v4	14/15	44	1,042,109	0	907,063	114.9%	0.0 pp	0	0
total			200,565,013	0	190,191,051	105.5%	0.0 pp	0	0

_{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 --strict-assembly, no --optimize). This isolates code generation from optimization.

corpus	compiled	comparable	our gas	Δ vs main	solc gas	ours/solc	Δ ratio vs main	regr	impr
EVM-code-transform	—	40	677,798	0	676,813	100.1%	0.0 pp	0	0
object-compiler	—	21	842,590	0	841,792	100.1%	0.0 pp	0	0
optimizer	—	545	2,400,290,015	0	2,400,328,781	100.0%	0.0 pp	0	0
total			2,401,810,403	0	2,401,847,386	100.0%	0.0 pp	0	0

_{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 --ir Yul solc lowered the contract to; solc via --strict-assembly.

corpus	fixtures	this compiler	Δ vs main	per fixture	Δ/fixture vs main	solc	ours/solc
aave-v4	1	2.2 s	+10.4%	2.2 s	+10.4%	78 ms	2884.6%
gasTests	12	5.7 s	+9.6%	475 ms	+9.6%	268 ms	2127.2%
semanticTests	1,340	6.6 min	−2.4%	298 ms	−2.4%	29.7 s	1345.0%
uniswap-v4	14	2.1 min	−0.9%	8.8 s	−0.9%	838 ms	14774.3%
total	1,367	8.8 min	−1.9%	388 ms	−1.9%	30.8 s	1720.6%

_{Charged to neither column: 32.5 s of solc --ir front-end lowering, which produces the Yul both compile. Also not counted is solc's --optimize --via-ir compile that the gas comparison runs — it starts from Solidity and includes the Yul optimizer, so it is not the same job.}

b) Yul corpora — the fixtures are already Yul, so both compile it directly; there is no front-end on either side.

corpus	fixtures	this compiler	Δ vs main	per fixture	Δ/fixture vs main	solc	ours/solc
EVM-code-transform	43	43 ms	−45.6%	1 ms	−45.6%	272 ms	15.8%
object-compiler	30	144 ms	+14.3%	5 ms	+14.3%	153 ms	94.1%
optimizer	593	2.1 s	−3.7%	4 ms	−3.7%	7.6 s	27.6%
total	666	2.3 s	−4.1%	3 ms	−4.1%	8.0 s	28.5%

_{Excluded from both columns: 1.4 min this compiler spent on 303 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)

• No sorry in sources: ✅ clean
• Axiom footprint: ✅ sorry-free, standard axioms only
• Spec closure: ✅ audited spec surface pinned
• SPEC.md: ✅ up to date

6. Verdict

✅ All good

[leonardoalt]

Scope correction: this moves zero test results, and cannot until gas() lands

Flagging this because the PR as written implies more than it delivers.

Nothing in CI changed, by construction. Every runner calls
compileSource source; the new libraries parameter defaults to []; and the
empty-env path is explicitly short-circuited to a no-op. A live linkersymbol
is still rejected exactly as before. The #guards are the only thing exercising
the feature.

But wiring the harness up would not help either. I measured it rather than
assumed. Of the 1671 semanticTests fixtures, 44 need library linking (their
solc --bin carries __$…$__ placeholders, so they are currently unreachable
on both sides — parseBinaryAfter rejects the reference bytecode too).
Compiling all 44 with this branch, supplying every linkersymbol a dummy
address:

	compiles
without --libraries	1 / 44
with --libraries	1 / 44

The one that compiles does so either way. Linking unlocks nothing.

The reason is structural, not incidental: an external library call is
delegatecall(gas(), lib, …). A program that needs a live linkersymbol is
calling a public/external library function, which forwards gas — so it
necessarily also uses gas(), which this compiler rejects. 18 of the first 20
link-needing fixtures use gas(); the same coupling holds for the two in-repo
aave fixtures with live linker symbols (LiquidationLogic, SpokeOperations),
which need immutables as well.

So this is a prerequisite, not a win. It is small, sound and guarded, and it
is genuinely required before any linked program can compile — but it pays off
only jointly with gas() (powdr-labs/yul-semantics#41, currently parked). It
should be reviewed on that basis, and it may make more sense to land it
alongside the gas work than ahead of it.

The harness work (discover library names, deploy the libraries, pass matching
--libraries to solc so its reference bytecode links too) is still needed
eventually, but it is pointless until gas() is supported.