prototype: prove Glamsterdam write-prepayment liveness

[chugarchugarr]

Phase 1: executable falsification gate

Pinned base: ethereum/execution-specs@20f7f6271a720091e5fea0a82e7bc802866ae36a (forks/amsterdam).

This PR deliberately does not modify consensus semantics yet. It first proves the two invariants required before a write-voucher encoding is worth implementing:

1. identical immutable child budget: Osaka PASS -> Amsterdam FAIL -> Amsterdam + prepayment PASS;
2. relocating the EIP-8038 storage-write repricing delta outside the child preserves the full Amsterdam execution-resource charge.

Minimal case

Existing non-zero slot, two PUSHes + SSTORE, fixed child gas = 5,006.

• Osaka: 2,100 + 2,900 + 6 = 5,006 -> PASS
• Amsterdam: 2,100 + 10,000 + 6 = 12,106 -> FAIL
• Amsterdam prepaid local frame: 100 + 2,800 + 6 = 2,906 -> PASS

Conservation

STORAGE_WRITE delta = 10,000 - 2,800 = 7,200.

Ordinary Amsterdam storage work:
2,100 + 10,000 = 12,100.

Prepaid split:
2,000 access-list key + 100 warm runtime + 7,200 prepayment + 2,800 legacy write = 12,100.

Account access independently conserves:
3,000 = 2,900 access-list address + 100 warm runtime.

Total core call/storage resource charge therefore remains 15,100.

Gate

If CI passes, the next branch change will implement explicit opt-in voucher state/rollback semantics and test nested calls, reverts, restoration/refunds, duplicates, and EIP-8037 interaction. Mainnet bytecode/value scanning stays out of scope until those semantics survive.

[chugarchugarr]

Superseded by #2, which contains the four named proof assertions and the successful focused proof run: https://github.com/chugarchugarr/execution-specs/actions/runs/32996887596

Closing this earlier phase without deleting its branch or history. The active public record is chugarchugarr/-x402-resolution-receipt#2.