Machine-check why gas() cannot enter the verified fragment yet

[leonardoalt]

Standalone, additive, and deliberately does not add gas() support.

opTable maps Op.gas to none, so every program reading gas() is rejected — which is every real solc contract, since call(gas(), …) is the idiomatic call. This records, as proofs rather than prose, exactly what blocks it, so the next attempt starts from a known position.

I did implement the feature first (fused GAS ; CALL Asm instruction, peephole rewrite, both simulation phases). It worked — the aave LiquidationLogic fixture compiled with it and was rejected without it. It is not in this PR, because the side condition it needed turned out to be false.

Obstacle 1 — the callee side condition cannot be weakened to something true

The working version assumed GasInsensitive: the callee behaves the same however much gas it is forwarded. That is false of real contracts — too little gas and any callee fails.

The natural repair is GasThreshold: for each request there is a G above which behavior stops changing. This is true of real contracts, and it fixes the part I expected to be fatal — G depends only on request and state, never on the gas field, so a phase-B bound can be chosen from it. GasInsensitive.gasThreshold shows flat insensitivity is just its G = 0 case.

It still does not suffice, because the pinned oracle may report any word:

• thresholdCalls — a callee that succeeds above 1000 gas and fails below;
• thresholdCalls_source_asteps — a genuine two-step op gas ; op call derivation where the oracle reports 0, so the call yields 0;
• thresholdCalls_no_admissible_allowance — no at-or-above-threshold allowance reproduces it.

So a fused rule quantifying its allowance as "some g ≥ G" has no matching step: its simulation would be false, not merely unproved. With an unconstrained oracle, flat insensitivity is not merely sufficient but necessary — which is why the fix must remove that reading at source (powdr-labs/yul-semantics#41) rather than constrain our own instruction.

Obstacle 2 — the phase-B gas bookkeeping cannot express a call's cost

Independent of any hypothesis. astep_sim carries ∃ bnd, ∀ s, … ∧ s.gasAvailable - bnd ≤ s'.gasAvailable. Under EIP-150 a call forwards 63/64 of what remains, so the loss scales with s.gasAvailable — unknown when bnd is fixed. no_additive_bound_under_eip150 proves no bnd covers it.

This is the shape of our own statement, not an environment assumption, so no side condition repairs it. The fix is to generalise from "subtract bnd" to a monotone gas transformer (g ↦ (g - c)/64 at a call, g ↦ g - c elsewhere): closed under composition, discharged by EIP-150 itself, needing no assumption. arun_halt_sim's conclusion has no gas conjunct, so headline statements would not change.

Prerequisites this establishes for a future attempt

1. land yul-semantics#41 (ExternalGas), then
2. generalise the phase-B gas bookkeeping, then
3. reinstate the fused instruction — at which point only GasThreshold remains, and that one is true of real contracts.

Scope

Additive: one new file plus its import. Nothing here is reachable from a headline theorem — audited surface, SPEC.md, Checks.lean, pinned semantics and every baseline are untouched, and gas() stays rejected exactly as before. lake build clean, Checks.lean clean, SpecClosure.lean clean and SPEC.md in sync, no sorry/axiom/unsafe.

🤖 Generated with Claude Code

[github-actions]

CI summary — ✅ All good

_{head 70a7fcac9 · main 6f53440dc}

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	1.9 s	+9.1%	1.9 s	+9.1%	81 ms	2296.3%
gasTests	12	4.4 s	−10.1%	365 ms	−10.1%	256 ms	1709.0%
semanticTests	1,340	6.3 min	+3.5%	281 ms	+3.5%	30.5 s	1234.4%
uniswap-v4	14	1.7 min	+4.0%	7.4 s	+4.0%	865 ms	12031.8%
total	1,367	8.1 min	+3.5%	356 ms	+3.5%	31.7 s	1535.5%

_{Charged to neither column: 33.2 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	57 ms	−5.0%	1 ms	−5.0%	277 ms	20.6%
object-compiler	30	153 ms	−20.3%	5 ms	−20.3%	155 ms	98.7%
optimizer	593	2.1 s	+0.5%	4 ms	+0.5%	7.7 s	27.3%
total	666	2.3 s	−1.3%	3 ms	−1.3%	8.1 s	28.4%

_{Excluded from both columns: 1.3 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