feat: --yul-backend option to compile Yul with libyulc

[leonardoalt]

What

Adds a CLI option that routes stand-alone Yul compilation through libyulc, our Yul → EVM compiler written and proved correct in Lean, instead of solc's own code generator:

solc --strict-assembly --yul-backend yulc input.yul

--yul-backend=solc remains the default, so nothing changes for anyone who does not pass the option.

Why this shape

libyulc's C entry point (yulc_compile, see yulc.h) takes a complete Yul program — block- or object-rooted, with child objects and data segments resolved during compilation — and returns finished creation bytecode. That is exactly the contract of --strict-assembly, so the integration is a single alternative branch in processInput(); the source is handed over verbatim and the resulting bytes are printed. No changes to libyul, libevmasm or the Solidity pipeline.

Because the backend has no intermediate representation to expose and optimizes according to its own proofs, the parser narrows what is accepted rather than silently doing something else:

• only --bin is available (no --asm, --asm-json, AST, CFG, ethdebug or source maps);
• --optimize, --optimize-runs, --optimize-yul, --no-optimize-yul, --yul-optimizations, --via-ssa-cfg and --libraries are rejected;
• a program outside the verified fragment is an error, not a fallback to the default backend.

Build system

-DUSE_YULC=ON (off by default) links solc against libyulc and defines SOLC_HAVE_YULC. Without it the option still parses but reports that the binary was built without support, so the CLI surface stays identical across builds and the parser tests are configuration-independent.

libyulc is a Lean build and is not compiled from source here. cmake/yulc.cmake downloads a pinned release tarball, or uses -DYULC_ROOT=<dir> to point at a local yul-compiler/.lake/build/c. The merged static archive is linked in, so solc stays a single self-contained binary with no runtime library search path to arrange — at the cost of size (see below). This is only supported on x86-64 Linux, and is incompatible with -DSOLC_LINK_STATIC=ON.

Verification

Built and exercised both configurations locally against the real libyulc-v0.0.2 release:

	solc size	+ SOLC_STRIP_SYMBOLS=ON	--yul-backend yulc
USE_YULC=OFF (default)	19.4 MiB	16.4 MiB	clean "built without libyulc support" error
USE_YULC=ON	208.9 MiB	144.1 MiB	compiles

$ solc --strict-assembly --yul-backend yulc t.yul     # { let x := 2 let y := 40 sstore(0, add(x, y)) }

======= t.yul (EVM) =======

Binary representation:
602a5f55

602a5f55 is PUSH1 0x2a; PUSH0; SSTORE — the two locals folded into sstore(0, 42). An object-rooted input produces creation bytecode whose runtime length matches its datasize.

• new CommandLineParserTest/yul_backend_option{,_invalid} unit tests pass, and the full CommandLineParserTest suite (22 cases) is green;
• four new test/cmdlineTests fixtures cover the rejection paths; all pass. They are all parser-level, so they behave the same with or without libyulc linked in.

Notes for review

• fix: build the yulc executable before collecting the C-library archives yul-compiler#136, ICE when using struct name for array argotorg/solidity#137, Parse error when using type from other library/contract argotorg/solidity#138 and Narrow the two bare import Mathlib to the modules actually used yul-semantics#40 are all merged; libyulc-v0.0.2 is cut from yul-compiler main and includes the Mathlib link-closure reduction (see the sizing comment below).
• Docs: a "Choosing the Code Generator" section in docs/yul.rst and a build section in docs/installing-solidity.rst.

🤖 Generated with Claude Code

[leonardoalt]

Pinning verified against the published release

libyulc-v0.0.1 is released. Configured a clean build directory with no YULC_ROOT, so the FetchContent path ran for real:

-- Found libyulc: .../build-dl/_deps/yulc-src/libyulc.a
[285/285] Linking CXX executable solc/solc

======= obj.yul (EVM) =======

Binary representation:
6024600b5f3960245ff3005f3560e01c8063371303c0141561001d575060015f54015f55610022565b505f5ffd5b00

Tarball downloaded, SHA-256 matched, bytecode identical to the YULC_ROOT build.

On the binary size

USE_YULC=ON takes solc from 20 MB to 340 MB. Breaking the binary down by symbol origin:

Origin	Size
Lean runtime + stdlib	80.9 MB
Mathlib	62.2 MB
solc + boost + libc++	22.2 MB
Mathlib tooling deps (Aesop, ProofWidgets, Qq, ImportGraph, Plausible, LeanSearchClient, Batteries)	14.4 MB
yul-compiler's own compiled code	8.1 MB

plus 23.7 MB .eh_frame, 8 MB relocations, and ~114 MB of symbol table (strip alone gets it to 226 MB).

Mathlib is present because Lean's initialize_M calls the initializer of every module M imports, which is a real symbol reference the linker cannot discard. import Mathlib therefore drags in all of it, including things that plainly never run: 3,103 symbols from Mathlib.Tactic.ClickSuggestions, 9,314 from Mathlib.Analysis, 6,892 from Mathlib.CategoryTheory.

It traces to one line — YulParser/Canon.lean:1 is a bare import Mathlib, and YulParser.lean imports Canon. Every other Mathlib import in that repo is already narrow. Narrowing it is a yul-compiler change (the proofs have to still build), tracked separately from this PR.

[leonardoalt]

Added -DSOLC_STRIP_SYMBOLS=ON (7b02e8e).

A USE_YULC=ON binary is 339 MiB, but only 227 MiB of that is loadable content. The rest is the symbol table — 1,001,102 defined symbols, almost all Lean mangled names, .strtab alone being 90 MiB. Dropping it at link time:

build	SOLC_STRIP_SYMBOLS=OFF	SOLC_STRIP_SYMBOLS=ON	saved
USE_YULC=ON	355,502,216 B (339.0 MiB)	236,446,528 B (225.5 MiB)	113.5 MiB (33%)
USE_YULC=OFF	20,353,680 B (19.4 MiB)	17,214,536 B (16.4 MiB)	3.0 MiB (15%)

All Release, measured in this worktree. The linked-with--s binary is byte-for-byte the same size as running strip on the unstripped one, and still works:

$ ./build/solc/solc --strict-assembly --yul-backend yulc min.yul
Binary representation:
602a5f55

To enable:

cmake .. -DUSE_YULC=ON -DSOLC_STRIP_SYMBOLS=ON

Notes on the design:

• Off by default, and not tied to the build type. -s throws away DWARF along with the symbol table, and the top-level CMakeLists.txt defaults CMAKE_BUILD_TYPE to RelWithDebInfo for a git checkout, so making this automatic would quietly cost every developer their debug info.
• --strip-debug is not an alternative. Confirmed on the actual binary: there are no .debug_* sections in a Release build, and strip --strip-debug saves 0.3 MB against strip's 113.5 MiB.
• Link-time flag, not a post-build strip. The executable is written once and the build stays incremental. It uses target_link_options() rather than the LINK_FLAGS property that SOLC_LINK_STATIC/SOLC_STATIC_STDLIBS set, so it composes with them instead of clobbering them.
• Nothing in solidity symbolizes backtraces. No crash handler, no boost::stacktrace, no execinfo.h anywhere in the tree — grepped. So solc's own diagnostics are unaffected. What you lose is gdb/perf/addr2line being able to name functions; the docs say so and suggest keeping an unstripped copy.

Documented as a new "Stripping Symbols" section under "CMake Options" in docs/installing-solidity.rst, cross-linked from the libyulc section.

[leonardoalt]

Correction to the size analysis above

I claimed the Mathlib bloat traced to a single bare import Mathlib at YulParser/Canon.lean:1. That was wrong — I grepped the yul-compiler repo but not its .lake/packages. The pinned yul-semantics dependency has bare import Mathlib in two files (YulSemantics/Basic.lean, YulSemantics/Dialect/EVM.lean), and Dialect/EVM is imported by YulParser/Expr.lean, YulEvmCompiler/Value.lean and much of the optimizer, so all of Mathlib stays in the link closure regardless of what Canon.lean does.

Narrowing Canon.lean alone (powdr-labs/yul-compiler#137) moves the yulc executable by +536 bytes — noise. Same 8,724 objects.

Sizing the real prize, by narrowing the dependency locally and recomputing the closure:

	objects	Mathlib modules	object input
today	8,724	8,170	335.5 MB
dependency narrowed too	996	555	117.2 MB

That is roughly 31.6 MB (19%) off yulc, and correspondingly off libyulc and this binary. It requires a change in powdr-labs/yul-semantics plus a rev bump, so it is out of scope here and does not block this PR.

The SOLC_STRIP_SYMBOLS measurements in the previous comment are unaffected and were verified directly on the linked binaries.

[leonardoalt]

Repinned to libyulc 0.0.2 — solc is now 144 MiB stripped, down from 339 MiB

The Mathlib work in yul-compiler has landed (powdr-labs/yul-compiler#137, argotorg#138, powdr-labs/yul-semantics#40 — all merged), and libyulc-v0.0.2 is cut from that. Rebuilt solc against both releases on this branch:

	0.0.1	0.0.2	delta
solc	355,502,216	219,069,328	−136.4 MB
solc, SOLC_STRIP_SYMBOLS=ON	236,446,528	151,078,184	−85.4 MB
.text	185,199,409	121,448,177	−63.8 MB
.eh_frame	23,688,712	14,218,448	−9.5 MB
.rodata	8,679,320	3,982,576	−4.7 MB
defined symbols	1,001,102	570,826	−430,276

End to end, -DUSE_YULC=ON -DSOLC_STRIP_SYMBOLS=ON now costs 144.1 MiB against a 19.4 MiB baseline solc, where the first working version cost 339.0 MiB. Both 0.0.1 and 0.0.2 binaries compile the block-rooted and object-rooted test inputs to byte-identical bytecode.

Worth noting the reduction is ~3x what extrapolating from the yulc executable predicted (that suggested ~29 MiB). I have not chased down why the executable and the static-archive link differ by that much; the solc numbers above are measured directly on the linked binaries rather than extrapolated.

Two mechanical notes:

• The release tarball shrank 242.8 MB → 211.4 MB, and the bundled libyulc.so 198 MB → 79.8 MB, but libyulc.a is 759 MB, slightly larger than before. That is expected: build-c-lib.sh archives every object under each package's build/ir, and Mathlib's objects still exist on disk — they are simply no longer referenced, so the linker no longer pulls them.
• Reconfiguring an existing build directory across this bump needs the cached pins cleared: -UYULC_VERSION -UYULC_RELEASE_SHA256 -UYULC_LIBRARY -UYULC_HEADER.