Point yul-semantics at the Mathlib-narrowed rev; 29 MB off yulc

[leonardoalt]

Summary

Removes Mathlib from the yulc / libyulc link closure. A Lean module's initialize_M calls the initializer of every module M imports, which is a real symbol reference the linker cannot discard, so one bare import Mathlib anywhere in the runtime closure links all of compiled Mathlib into the binary.

PR #137 (this PR's base) removed this repo's only bare import Mathlib and measured no effect, because the pinned yul-semantics had two of its own. Those are narrowed in powdr-labs/yul-semantics#40; this PR points rev at that work and fixes the downstream cascade. The two changes are mutually blocking: neither one alone does anything.

Measured on .lake/build/bin/yulc, an ordinary runnable link (no --unresolved-symbols=ignore-all):

	bytes	objects in yulc.rsp
base (canon-narrow-mathlib-import)	165,277,392	8,724
this PR	134,841,520	1,112
delta	-30,435,872 (-29.0 MiB, -18.4%)	-7,612

The .c.o.export input to the link is 19.7 MB after. The resulting binary was run and compiles a small Yul object to byte-identical output vs the baseline binary.

Changes

• lakefile.toml + lake-manifest.json: yul-semantics rev 81b9e3e -> 4c6f975. Nothing else in lakefile.toml is touched.
• Narrow imports in the six modules that were getting Mathlib transitively through YulSemantics.Dialect.EVM (Value.lean, Simplify.lean, Decode.lean, Asm.lean, ObjectResolve.lean, YulIR/FrameCongr.lean). FrameCongr needed only Batteries.
• 72 explicit («D» := D) dialect annotations across the optimizer proofs. Step, EquivExpr, VEnv.set_keys and friends take [DecidableEq D.Value], and these terms elaborate before the expected type fixes D. With Mathlib in scope, DecidableEq (Dialect.Value ?D) was inconclusive rather than failing (LinearOrder.toDecidableEq and the chain below it leave the search stuck on metavariables), so Lean postponed it until ?D was known. Without Mathlib there are no candidate instances at all, so it is a hard failure. The guillemets are required because these files declare local notation "D" => evmWithExternal calls creates, which makes bare D a token rather than an identifier. No proof term content changed.

Two things a reviewer should look at closely

1. Six decreasing_by blocks changed. all_goals simp_wf <;> omega -> all_goals simp_wf; omega in five places, which is literally what the Batteries unnecessarySeqFocus linter demands (it fires because simp_wf now leaves one goal per invocation rather than several). DeadPureResolve's bare all_goals simp_wf gained ; omega, because simp_wf alone no longer closes 2 * sizeOf body ≤ 2 * (1 + sizeOf body).

2. One audited spec hash moved. SpecClosure.lean's pin for YulEvmCompiler.opTable changed from e1b0c299397baebd to 58d5b129f84835ed, and SPEC.md is regenerated. The value is identical; only the elaboration of the five Fin 5 literals in the LOG rows changed. With all of Mathlib in scope they were resolving through SimplexCategory.instOfNatToTypeOrderHomFinHAddNatLenOfNat, the OfNat instance on the simplicial-category object [4], which happens to be defeq to Fin 5. They now use core's Fin.instOfNat. Verified by diffing the fully elaborated opTable term between the two trees (that instance is the only difference anywhere in the term) and by evaluating the table on log0..log4 in both trees: both give Operation.Log { topics := 0..4 }. The other 88 audited hashes and the 155-declaration external boundary hash are unchanged. The rest of the SPEC.md diff is line numbers shifted by the added imports.

Testing

Everything CI's build job runs, all against Solidity develop 510b2a1:

• lake build (all default targets): pass
• lake build yulc: pass; binary runs
• sorry scan: pass
• lake env lean Checks.lean (axiom footprint): pass
• lake env lean SpecClosure.lean: pass after the opTable re-pin above; SPEC.md committed and up to date
• lake env lean YulIR/CheckBaseline.lean: YulIR OK: 59 programs
• syntax corpus: 319 tests: 106 expected successes, 213 expected failures, 0 known parser mismatches
• interpreter tests: 53 tests: 28 passed, 25 failed (25 known); skipped 1
• optimizer corpus: 643 tests: 593 compiled, 50 failed (50 known); skipped 8
• object-compiler corpus: 36 tests: 30 compiled, 6 failed (6 known); skipped 0
• EVM-code-transform corpus: 47 tests: 43 compiled, 4 failed (4 known); skipped 0
• scripts/YulIRCorpus.lean check: gated 43 categories, 0 drifted/new, 0 regressions

Not run: the gas-runner / solidity-gas / solc-differential legs (they need the pinned solc and hours of corpus execution). Nothing here changes emitted bytecode, and the compile corpora above cover the compile path.

Notes

Both blockers are cleared:

• Narrow the two bare import Mathlib to the modules actually used yul-semantics#40 is merged. rev now points at 4c6f9753cc0e5850f6bdaf6fb0df76457204699a on that repository's main. That merge commit has the identical tree (6f559621) to the branch commit everything above was measured and tested against, so every result in this PR carries over unchanged -- the repoint moved a SHA, not a source byte.
• YulParser.Canon: narrow import Mathlib to the two modules it needs #137 is merged, so this PR is now based on main.

🤖 Generated with Claude Code

[github-actions]

CI summary — ✅ All good

_{head f92a5052c · main 23a52453c}

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	18,391,475	0	18,236,226	100.9%	0.0 pp	0	0
gasTests	12/12	12	398,210	0	336,827	118.2%	0.0 pp	0	0
semanticTests	1317/1652	1259	183,009,358	0	170,351,455	107.4%	0.0 pp	0	0
uniswap-v4	14/15	44	1,062,224	0	907,063	117.1%	0.0 pp	0	0
total			202,861,267	0	189,831,571	106.9%	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	678,404	0	676,813	100.2%	0.0 pp	0	0
object-compiler	—	21	842,590	0	841,792	100.1%	0.0 pp	0	0
optimizer	—	545	2,400,292,545	0	2,400,328,781	100.0%	0.0 pp	0	0
total			2,401,813,539	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. 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

5. Verdict

✅ All good