Harden the Solidity verifier: bytecode certification and EVM replay - #6

Open

jtcoolen wants to merge 108 commits into

mainfrom

Commits on Jun 28, 2026

Mark PCS fixed windows Permanent in verifier memory planner

jtcoolen
and
factory-droid[bot]
committed
4f272f0
Model selector accumulator phase span
jtcoolen
committed
bb6f463
Use pairing batch hash size constant
jtcoolen
committed
4352a71
Account theta windows in trace scratch bound
jtcoolen
committed
bafd8d7
Reserve fused add-product constants early
jtcoolen
committed
de3bd7e
Reserve limb decomposition constants early
jtcoolen
committed
7b498f7
Guard rotated public instance queries in Solidity codegen
jtcoolen
committed
5d7afe9

Commits on Jul 18, 2026

Fix transcript buffer sizing and quotient VM const-table overflow

authored and
jtcoolen
committed
a01b1ea
Bound the Lagrange batch-invert input run in the memory planner

jtcoolen
and
factory-droid[bot]
committed
adc589f
Reject off-curve points in EIP-2537 G1/G2 encoders

jtcoolen
and
factory-droid[bot]
committed
b24be9e
Validate the SRS G1 base equals the canonical generator

jtcoolen
and
factory-droid[bot]
committed
fc42518
Invalidate reassigned variables in the limb7 chain rewriter

jtcoolen
and
factory-droid[bot]
committed
c80cbc8
Content-check embedded VK quotient program against the plan build

jtcoolen
and
factory-droid[bot]
committed
1fa3b41
Bounds-check quotient VM const-table slots in the offline validator

jtcoolen
and
factory-droid[bot]
committed
8db58be
Fail closed on zero KZG point sets in the PCS emitter

jtcoolen
and
factory-droid[bot]
committed
700af6d
Bound the unrolled PCS rotation-point walk at codegen

jtcoolen
and
factory-droid[bot]
committed
6e14bfe
Correct the KZG batch-inversion non-zero soundness comment

jtcoolen
and
factory-droid[bot]
committed
36fc616
Fix inverted pairing-orientation comment in the KZG emitter

jtcoolen
and
factory-droid[bot]
committed
66c32f9
Document the pointer-identity KZG query-grouping invariant

jtcoolen
and
factory-droid[bot]
committed
688efde
Harden rotated-instance guard in the quotient VM lowerer

jtcoolen
and
factory-droid[bot]
committed
098f6a1
Use checked u32 conversion for quotient VM memory pointers

jtcoolen
and
factory-droid[bot]
committed
16f43b5
Validate quotient VM memory pointers are word-aligned at construction

jtcoolen
and
factory-droid[bot]
committed
56f20be
Guard rotated non-committed instance queries in the Yul quotient emitter

jtcoolen
and
factory-droid[bot]
committed
2286dff
Use unsigned_abs in column_eval_var to avoid i32::MIN overflow

jtcoolen
and
factory-droid[bot]
committed
d149f96
Emit h_eval, not 0, for an empty lookup input chunk in the Yul emitter

jtcoolen
and
factory-droid[bot]
committed
e5f77f8
Guard against a lookup with zero helper chunks in the Yul emitter

jtcoolen
and
factory-droid[bot]
committed
33e183e
Floor quotient stack scratch at one word to cover the eval-scratch write

jtcoolen
and
factory-droid[bot]
committed
0b56186
Emit h_eval, not 0, for an empty lookup chunk in the structured path

jtcoolen
and
factory-droid[bot]
committed
d67a2e9
Assert lookup chunk/helper-eval count parity at both zip sites

jtcoolen
and
factory-droid[bot]
committed
63be029
Document the proxy selector_gap in native_identity_estimate_block

jtcoolen
and
factory-droid[bot]
committed
fd3842c
Fail closed on negative offset in Value::as_usize

jtcoolen
and
factory-droid[bot]
committed
b8b4c39
Assert VK fixed-commitment count matches meta in Data::new

jtcoolen
and
factory-droid[bot]
committed
a9032f8
Correct dummy_eval_words address formula in the field doc

jtcoolen
and
factory-droid[bot]
committed
822980e
Reject VK runtime exceeding the EIP-170 code-size limit at codegen

jtcoolen
and
factory-droid[bot]
committed
69889be
Harden accumulator fixed-base/scalar count check to a release assert

jtcoolen
and
factory-droid[bot]
committed
01f4549
Use checked arithmetic when reserving VK payload sections

jtcoolen
and
factory-droid[bot]
committed
b2e99e8
Range-check accumulator scalars where they are read

jtcoolen
and
claude
committed
68adb90
Leave batch_invert immediately on a failed modexp

jtcoolen
and
claude
committed
2e49d03
Make the verifier's accept path fail closed locally

jtcoolen
and
claude
committed
636c7ec
Reject non-reduced inputs in the Fr inversion helpers

jtcoolen
and
claude
committed
d870dd1
Check spilled-stack balance in the quotient VM epilogue

jtcoolen
and
claude
committed
b680bf2
Initialize the y^0 slot in the selector power table

jtcoolen
and
claude
committed
3f95c05
Count quotient limbs in absorb bytes in eval_run_bytes

jtcoolen
and
claude
committed
14cb772
Assert VK permutation commitment count matches meta in Data::new

jtcoolen
and
claude
committed
79dd945
Panic instead of rendering a negative pointer as sub(0, N)

jtcoolen
and
claude
committed
9d7081b
Reject non-canonical scalars in the proof repacking shim

jtcoolen
and
claude
committed
b4319da
Correct the pairing-batch domain tag comment

jtcoolen
and
claude
committed
55d548b
Move final pairing scratch past the accumulator batch frame

jtcoolen
and
claude
committed
a1bb2c4
Order MemoryPhase to match generated-verifier execution order

jtcoolen
and
claude
committed
914c61c

Commits on Jul 19, 2026

Register the trace-only linearization MSM scratch with the arena

jtcoolen
and
claude
committed
ed547ae
Compile the accumulator render arm in the default EVM gate

jtcoolen
and
claude
committed
5912061
Regenerate tracked verifier fixture artifacts

jtcoolen
and
claude
committed
48a6f0c
Reject an accumulator fixed-base tail the VK cannot supply bases for

jtcoolen
and
claude
committed
54907b5
Fail loudly when the EVM gate is requested but cannot run

jtcoolen
and
claude
committed
bea362e
Require the pairing precompile to return exactly one

jtcoolen
and
claude
committed
9e714b7
Fix an always-false guard in the accumulator limb decoder

jtcoolen
and
claude
committed
72bc1b2
Report unsupported constraint systems from try_new instead of panicking

jtcoolen
and
claude
committed
58824e8
Bound the public instance count at generator construction

jtcoolen
and
claude
committed
75f9f99
Pin the phase ordering the Lagrange denominator cap depends on

jtcoolen
and
claude
committed
06e46be
Add a known-answer vector to the EIP-2537 constructor smoke test

jtcoolen
and
claude
committed
896fd04
Base the generated layout above solc's via-IR spill reservation

jtcoolen
and
claude
committed
6333673
Enforce the EIP-170 runtime size limit on the verifier contracts

jtcoolen
and
claude
committed
a30fef4
Propagate the TranscriptInputBytes bound to LightAggregator::verify

jtcoolen
and
claude
committed
2938a40
Add a CI replay that adversarially exercises the accumulator decoder

jtcoolen
and
claude
committed
70dd1a8
Cover point_pair accumulators and port calldata attacks to the replays

jtcoolen
and
claude
committed
6f78686
Record deployment status and bytecode verification for moonlight-wrap

jtcoolen
and
claude
committed
29b4eb9
Regenerate tracked verifier fixture artifacts

jtcoolen
and
claude
committed
9bf8c51
Self-certify emitted quotient VM bytecode at render time

jtcoolen
and
factory-droid[bot]
committed
0b27485
Refresh moonlight-wrap fixture calldata

jtcoolen
and
factory-droid[bot]
committed
94dfe37

Commits on Jul 20, 2026

Move the pairing-batch and final-pairing frames above solc's spill window

authored and
Julian
committed
60f842b
Reject non-canonical scalars in batch_invert's general path

authored and
Julian
committed
aa62d19
Harden quotient certification and spill-window coverage

authored and
Julian
committed
0cd1bdb

Commits on Aug 3, 2026

Run the Solidity verifier test suite in root CI

jtcoolen
and
claude
committed
ffd39db
Refresh the lowering architecture spec's stale references

jtcoolen
and
claude
committed
277c096
Bounds-check the quotient VM's emitted memory pointers

jtcoolen
and
claude
committed
20766cb
Unblock the clippy gate for the Solidity verifier package

jtcoolen
and
claude
committed
743d5da
Apply rustfmt to the quotient pointer validator

jtcoolen
and
claude
committed
11928d1
Make the gated EVM tests work under --all-features

jtcoolen
and
claude
committed
0aab0cf
Correct the I-12 challenge-sampling bias analysis

jtcoolen
and
claude
committed
3f89a98

Commits on Aug 6, 2026

Register the Lagrange denominator run as planner-owned scratch

jtcoolen
and
claude
committed
6753679
Regenerate the IVC replay fixture on the registered Lagrange scratch layout

jtcoolen
and
claude
committed
78556d0
Refresh the tracked IVC bench dump for the Lagrange scratch layout

jtcoolen
and
claude
committed
3fb6d84
Regenerate the Moonlight wrap fixture on the registered Lagrange scratch layout

jtcoolen
and
claude
committed
d6b248e
ci: fix changelog, formatting, and docs
jtcoolen
authored
bee1833

Commits on Aug 7, 2026

Cover instance binding and the two unreachable accumulator decode guards

jtcoolen
and
claude
committed
07d9a9d

Commits on Aug 8, 2026

docs: add independent architecture review and redesign proposals (2026-08)

jtcoolen
and
claude
committed
4ae8053

Commits on Aug 10, 2026

fmt: apply nightly rustfmt (import grouping, comment wrap)

jtcoolen
and
claude
committed
ac9604d

Commits on Aug 12, 2026

docs: add independent Solidity verifier review and audit (2026-08)

jtcoolen
and
claude
committed
513fa87
fix(solidity-verifier): harden memory invariant, pin pragma, strengthen precompile probes

jtcoolen
and
claude
committed
460a666

Commits on Aug 13, 2026

fix(solidity-verifier): stop forcing truncated-challenges through the aggregation dep

jtcoolen
and
claude
committed
6f229c1
fix(solidity-verifier): exact precompile gas bounds, SRS tau binding, MSM comment truth

jtcoolen
and
claude
committed
f1840bd
docs+scripts(solidity-verifier): reproducibility, SRS provenance, audit-trail truth

jtcoolen
and
claude
committed
5246b21
chore(solidity-verifier): regenerate fixture dumps on the current templates

jtcoolen
and
claude
committed
ca636ca
fix(solidity-verifier): planner and codegen assertions for the silent-drift findings

jtcoolen
and
claude
committed
7cc22e0
feat(solidity-verifier): runtime hardening — VM operand clamps, typed errors, alpha vk-binding

jtcoolen
and
claude
committed
86b262e
feat(solidity-verifier): on-chain BUILD_ID provenance and a template-tree digest gate

jtcoolen
and
claude
committed
ed9f455
docs(solidity-verifier): deployment/incident-response requirements and accepted-risk records

jtcoolen
and
claude
committed
faa8ef4
chore(solidity-verifier): regenerate dumps on the hardened templates, re-measure, pin digest

jtcoolen
and
claude
committed
f894f75
chore(solidity-verifier): regenerate both replay fixtures on the hardened codegen

jtcoolen
and
claude
committed
85b7fa3
fix(ci): restore exec bit on install_pinned_solc.sh, clear clippy and fmt

jtcoolen
and
claude
committed
6fc3ee8
fix(solidity-verifier): price modexp for EIP-7883 and probe it at deploy (MF-1)

jtcoolen
and
claude
committed
8e65c96
fix(solidity-verifier): type the layout guard, harden the quotient VM, split precompile faults from rejections (MF-2/3/4)

jtcoolen
and
claude
committed
580a912
docs(solidity-verifier): record the MF review, its two withdrawals, and the operational gaps it exposed

jtcoolen
and
claude
committed
fefbd61
test(solidity-verifier): run the EVM suite against the MF fixes, and fix what it caught

jtcoolen
and
claude
committed
03f1f7e
test(solidity-verifier): prove the modexp probe rejects an under-priced bound (MF-1)

jtcoolen
and
claude
committed
564865e
docs(solidity-verifier): correct the "Sepolia is bricked" claim, and measure the WASM/native compiler gap

jtcoolen
and
claude
committed
d7b246a
clean
jtcoolen
committed
fbfdeae

Commits on Aug 14, 2026

docs(solidity-verifier): remove the truncated-challenge security-parameter analysis

jtcoolen
and
claude
committed
dc70d6f