Conversation
37b9a59 to
d162e9b
Compare
…te fixtures
Add a recursive-aggregation soundness gate to ZKHALO2VERIFYWITHVK and the ETH
beacon light-client opcode fixtures (deposit `step` + committee `rotate`).
Problem: a snark-verifier aggregation proof defers its inner KZG opening checks
into a 12-limb accumulator exposed as instances[0..12]. The stock opcode runs a
plain SHPLONK verify_proof (SingleStrategy, Blake2b), which proves the
aggregation relation but never pairs that accumulator — so a recursive-rotate
proof is accepted without checking the folded inner shard/step proofs.
Change:
- VkBlob: repurpose reserved byte 11 as `accumulator_limbs` (0 = none, 12 = KZG
accumulator @ instances[0..12]). Backward-compatible: legacy all-zero-reserved
blobs keep meaning "no decider".
- Opcode: when accumulator_limbs == 12, after the SHPLONK verify additionally run
the decider e(lhs, g2) == e(rhs, s_g2) over instances[0..12] against the SRS
G2 points the opcode already embeds (Hermez [1]G2 / [s]G2). Both must hold.
The accumulator is decoded from the snark-verifier layout (lhs.x‖lhs.y‖rhs.x‖
rhs.y, each 3 little-endian 88-bit limbs) via byte-window assembly, avoiding
the multi-halo2 Field-trait tangle in this crate's dep graph.
- Fixtures: add halo2_test_data/{step,rotate}_light_client (real Hermez proofs
from acki-nacki-bridge/eth-light-client-prover, M6). The rotate VkBlob header
carries accumulator_limbs = 12.
- Tests: decider unit tests on the real rotate accumulator (honest PASS,
tampered limb + swapped lhs/rhs REJECT) mirroring the native reference
examples/rotate_decider_check.rs; plus round-trip step (10 PI, 2-level
committee commitment) and rotate (15 PI) opcode tests through the handler.
Native reference for the decode+pairing convention:
acki-nacki-bridge/eth-light-client-prover/examples/rotate_decider_check.rs
Co-authored-by: Cursor <cursoragent@cursor.com>
d162e9b to
812a87b
Compare
|
Retargeted to This turned out to cost nothing. The two sources the decider actually touches are byte-identical on Re-verified on
The reason for aiming at mainline rather than the integration branch: |
|
@SeHor05 review request — this is the PR you flagged as unmerged in gosh-sh/bridge#36, the one that makes recursive What it does. A What changed since you looked. It was stacked on Evidence. 13 tests on What I need. An approving review — One thing to be clear about so this does not read as more than it is: merging this closes the gap in mainline |
Summary
Closes the recursive-aggregation soundness gap in
ZKHALO2VERIFYWITHVKand lands the ETH beacon light-client opcode fixtures (depositstep+ committeerotate, milestone M6 ofacki-nacki-bridge/eth-light-client-prover).Problem. A
snark-verifieraggregation proof defers its inner KZG opening checks into a 12-limb accumulator exposed asinstances[0..12]. The stock opcode runs a plain SHPLONKverify_proof(SingleStrategy, Blake2b): it proves the aggregation relation but never pairs that accumulator, so a recursive-rotateproof is accepted without checking the folded inner shard/step proofs. A BN254-only in-circuit decider is impossible (the check is a BN254 pairing), so the fix must live verifier-side — in the opcode.Change.
zk_halo2_with_vk_bundle.rs): repurpose reserved byte 11 asaccumulator_limbs(0= none,12= KZG accumulator @instances[0..12]). Backward-compatible — legacy all-zero-reserved blobs keep meaning "no decider".zk_halo2_with_vk.rs): whenaccumulator_limbs == 12, after the SHPLONK verify additionally run the decidere(lhs, g2) == e(rhs, s_g2)overinstances[0..12]against the SRS G2 points the opcode already embeds (KZG_G2_BYTES/KZG_S_G2_BYTES, i.e. Hermez[1]G2/[s]G2). Both must hold. The accumulator is decoded from the snark-verifier layout (lhs.x‖lhs.y‖rhs.x‖rhs.y, each 3 little-endian 88-bit limbs) via byte-window assembly, avoiding the multi-halo2Field-trait tangle in this crate's dependency graph.halo2_test_data/{step,rotate}_light_client(real Hermez proofs). TherotateVkBlob header carriesaccumulator_limbs = 12;stepis 10 PI with a 2-level committee commitment.Native reference for the decode + pairing convention (honest PASS, tampered/swapped REJECT):
acki-nacki-bridge/eth-light-client-prover/examples/rotate_decider_check.rs.Test plan
cargo test -p tvm_vm --lib decider_tests— decider on the real rotate accumulator: honest decidestrue; tampered limb and swappedlhs/rhsare rejected (4 tests).cargo test -p tvm_vm --lib -- rotate_light_client— round-trip through the handler now runs verify and decider; honest returnstrue, flipped proof / tweaked accumulator limb / tweaked rotate PI returnfalse(5 tests).cargo test -p tvm_vm --lib -- step_light_client— deposit step (10 PI, 2-level commitment) round-trip + negatives (4 tests).rustfmt(reporustfmt.toml, style_edition 2024) clean on all three sources.Made with Cursor