Skip to content

Feature/multithreading#4

Open
alinaT95 wants to merge 82 commits into
bump-halo2-lib-v0.4.1from
feature/multithreading
Open

Feature/multithreading#4
alinaT95 wants to merge 82 commits into
bump-halo2-lib-v0.4.1from
feature/multithreading

Conversation

@alinaT95

Copy link
Copy Markdown
Collaborator

No description provided.

alinaT95 and others added 30 commits June 26, 2026 21:37
WIP cryptographic spec for the multi-thread embodiment of the DEX
voucher circuit. Covers terminology (BWS=128, batches, key blocks,
GlobalHistoricalData) and details the block_id 8-leaf SHA-256 layout
with focus on L0 (Poseidon over 331-byte history_proofs preimage)
and L7 (Poseidon dense Merkle of [parent, refs...]) — the two slots
that carry all the multi-thread linkage. Sections 2-7 are stubs to
be filled in next.
The DEX circuit hides the concrete (block_id, height, thread_id) of
the event; the verifier sees only (finalLayerHistoricalHashRoot,
layerNumber). Anchoring at higher layer N is sometimes preferable
for a larger anonymity set even when layer-1 is still retrievable.
In multi-thread, the thread id is also part of the hidden witness —
proofs from thread t ≠ 0 are indistinguishable from thread-0 proofs.
- The "L0/L2/L3/L7 leaves are Poseidon" remark moved into §1 right
  after the block_id outer-tree definition, expanded to clarify
  leaf-construction hash vs outer-combine hash.
- The "per-layer batch tree is Poseidon dense Merkle of width
  BWS=128, prev #L1(M-1) prepended at index 0" sentence moved into
  §2 (Per-thread layer-N batch tree) where it belongs.
- Terminology section is now pure terminology (table only).
Fill in all stub sections (§2-§7) and add §8-§11:

- §1.2 L0 extraction: lock N=1 on thread-t side; C is uniquely
  determined by X (next layer-1 key block of thread t after X's batch).
- §2 layer-N batch tree: 130 leaves (2 prepended + 128 block_leaves)
  padded to 256, depth 8 Poseidon dense Merkle; layer-N recursion shape.
- §3 single-thread baseline: 7-step current DEX flow + public-input
  vector.
- §4 L7 walk: hop primitive, what one hop constrains, chain direction
  (into the past), per-hop cost (3 SHA + Poseidon paths).
- §5 full multi-thread binding flow X -> finalLayerHistoricalHashRoot.
- §6 multi-proof design: HopCircuit gadget + MultiHopProof (K=16, H=5)
  + DexFinalProof (K=15). Salted endpoints with voucher-scoped
  salt = Poseidon(DOMAIN_TAG, voucher_secret_seed). RootPN orchestrates
  continuity on-chain via salt_commitment + salted endpoint equality.
  Fixed N_BUNDLE = 5 snarks per claim for thread-t / thread-0
  indistinguishability.
- §7 synthetic test fixtures across chain lengths 0, 1, 5, 6, 15, 20.
- §8 detailed rejection rationale for AggregationCircuit / axiom-eth
  approach (phone budget, SRS, parallelism, EVM gas, simplicity).
- §9 anonymity analysis: what is hidden, what leaks, subtle cases.
- §10 locked parameters + 8 open questions for the team.
- §11 6-phase implementation plan.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Resolves the §10.1 vs §1.3 / §4.2 inconsistency. Locked value
chosen by the team: 256 leaves (1 parent + up to 255 refs),
padded as a power-of-2 dense Poseidon Merkle of depth 8.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…rkDexCircuitNew

Vendors the canonical salt convention from Phase 2 (gosh-referenced-block-hop)
into src/salt.rs (DOMAIN_TAG_BYTES = b"acki-nacki:voucher-hop-salt:v1",
salt = Poseidon([DOMAIN_TAG_FR, sk_u]), salt_commitment = Poseidon([salt]),
salted_block_id = Poseidon([salt, bytes_to_fr(block_id)])).

DarkDexCircuitNew now exposes 7 instances (was 5):
  [5] salt_commitment
  [6] event_salted_block_id

This is the public-input pre-extension for the Phase 4 multi-thread
bundle. The single event_salted_block_id will later split into the
(salted_C_start, salted_Y_end) pair once C-extraction lands; the spec
records that in §6.9 Phase 3 status note.

Spec updates (MULTITHREAD_CIRCUIT_SPEC.md): refresh DOMAIN_TAG and
Poseidon-shape references to match the vendored salt.rs; salt.rs is
declared the source of truth.

halo2-proover + test_real_data + test_sk_commit_compatibility updated
to consume the new 7-instance layout.
…g tests

Adds bundle_verifier.rs implementing the four bundle-level checks that
RootPN.sol enforces on-chain, kept in pure Rust so Phase 4 can be
exercised end-to-end with no tvm-sdk / on-chain plumbing:

  1. The first proof must be a DexFinal (Phase 3).
  2. salt_commitment must match across all proofs in the bundle.
  3. The DexFinal's bundle-head salted endpoint must equal the first
     MultiHop snark's salted_start (head linkage).
  4. Each MultiHop's salted_end must equal the next MultiHop's
     salted_start (continuity across snark boundaries).

test_bundle_binding.rs covers the happy path plus one failing case
per check, with explicit BundleError variant assertions.
…pers

Adds multi_hop_witness.rs with:
  - HopWitness / MultiHopProofWitness / ProofBlock structs mirroring
    acki-nacki/helpers/proof_helper/src/gql_proof.rs 1:1 so the same
    synthetic generator can later be swapped for live GQL fixtures
    with no shape adapter.
  - Locked spec constants: H_HOPS_PER_PROOF = 5, N_BUNDLE = 4,
    MAX_PROOF_BLOCK_REFS = 16 (TODO bump to 256 for production cap).
  - Native SHA-256 8-leaf block-merkle helpers + Poseidon ref-tree
    helpers used by the synthetic chain generator.
  - pack_tag_chunks workaround: production tags exceed the 31-byte
    single-Fr limit, so the native ref-leaf hash splits the tag into
    31-byte chunks and absorbs them as a Vec<Fr> ahead of the block
    id absorb. Shape-only (NOT byte-equivalent to production's
    hash_bytes_flat); the byte-flat helpers are kept alongside for
    the deferred 2c-suffix parity work.
  - 5 unit tests covering the helpers.
Extends test_helpers.rs with the deterministic synthetic chain generator
used by every Phase 4 bundle test:

  - `synth_chain(seed, k_hops)` builds an `H_HOPS_PER_PROOF × N_BUNDLE`
    capacity chain (locked: 5×4 = 20) where each real hop's target
    block has a single-ref ref-tree opening to its predecessor.
    Inactive padding hops sit at the tail; `is_active` flag drives
    Phase-C gated equalities.
  - `split_into_bundle_snarks(chain)` chunks the flat hop list into
    `N_BUNDLE` `MultiHopProofWitness` snarks with intra-snark and
    cross-snark salted-endpoint continuity preserved.
  - Re-exposes `test_helpers` unconditionally from lib.rs so the
    `tests/` integration tests can reach it; dev-only items
    (`build_dense_chain`, `build_two_level_tree`) stay `#[cfg(test)]`.
  - 4 unit tests covering K=0, K=5, K=20, snark-split.
…rcuits

Per the additive-feedback rule, lands three sibling circuits side by side
rather than mutating a single shape:

  * `MultiHopProofCircuit` (Phase A): H=1, all-active, ref_index=0,
    leaf_index=7. K=19, 8 advice cols. ~2 s MockProver.
  * `MultiHopProofCircuitB` (Phase B): H=5, all-active with intra-snark
    continuity (`hops[i].salted_end == hops[i+1].salted_start`).
    K=19, 48 advice cols. ~13 s MockProver.
  * `MultiHopProofCircuitC` (Phase C): H=5 with `is_active` selector and
    explicit `salted_start` / `salted_end` witnesses. Gated equalities
    (ref-tree root, SHA-256 bytes, salted-endpoint derivation) ×
    `is_active`; inactive-gated `salted_start == salted_end` for padding.
    K=19, 56 advice cols. ~10 s mixed / ~10 s all-inactive.

Public layout is `[salted_start_first_hop, salted_end_last_hop,
salt_commitment]` (MULTI_HOP_PUBLIC_LEN = 3).

This is the shape-mirror Poseidon ref-tree variant; the byte-flat
Poseidon variant for live-GQL parity is deferred to Stage 2c-suffix
(helpers already in `multi_hop_witness.rs::*_bytes_flat_native`).
tests/test_bundle_e2e.rs::bundle_e2e_k5_happy_path drives the full Phase 4
shape end-to-end: 4 × MultiHopProofCircuitC snarks (real KZG proofs at
circuit K=19) plus one synthetic Phase-3 DexFinal instance vector → fed
to verify_bundle and accepted.

`#[ignore]`; run with
`cargo test --release --test test_bundle_e2e -- --ignored --nocapture`.

Timings on the dev box: keygen_vk 47s, keygen_pk 18s, prove ~101s per
snark (uniform across active vs all-inactive — gates are unconditional,
only equality is gated), verify 8ms each. Total ~7.8 min. Proof size
18 240 B at K=19 / 56 advice cols / 4 lookup advice.
tests/test_bundle_negative.rs::bundle_e2e_negatives exercises every
BundleError variant by reshuffling two real KZG proofs (one from chain
0xAAAA_5EED, one from 0xBBBB_5EED) across the bundle:

  * SaltCommitmentMismatch at idx 2 ([dex_a, multihop_a, multihop_b]).
  * HeadLinkBreak (dex_a with 0xDEADBEEF head + multihop_a).
  * ContinuityBreak between (1, 2) — same A.snark[0] at positions 1
    and 2, its salted_end != salted_start fires the gate.
  * DexFinalNotFirst ([multihop_a, dex_a]).
  * DuplicateDexFinal (count = 2).

Shared VK/PK across chains since topology is identical. `#[ignore]`;
run with `--ignored --release --nocapture`. Timings: keygen_vk 35s,
keygen_pk 15s, prove 97s + 112s = 260s total (~4.3 min). All five
BundleError variants matched with exact field assertions.
…rget)

tests/test_bundle_stress.rs::bundle_stress_k20_full_capacity drives the
MULTITHREAD_CIRCUIT_SPEC.md §6.5/§10.1 worst case the current spec is
designed for: K_HOPS = L_MAX = H × N_BUNDLE = 5 × 4 = 20, every hop
active in every snark, end-to-end salted continuity across all snark
boundaries.

`#[ignore]`; run with
`cargo test --release --test test_bundle_stress -- --ignored --nocapture`.

Timings: keygen_vk 47s, keygen_pk 15s, 4 × prove ~98 s each (uniform),
verify ~8 ms each. Total 458s (~7.6 min). Proof size unchanged
18 240 B. Confirms shared VK/PK works across all-active *and*
all-inactive snarks — gate body is unconditional, only equality
residuals × is_active.
Validates spec §10.2 Open Question #1 escape path A (raise N_BUNDLE)
all the way to the colleagues-reported worst-case chain length of 300.
Per-snark circuit (H = 5, circuit K = 19) and locked global
`N_BUNDLE = 4` constant are untouched; only the bundle width grows.

Adds two additive sibling helpers in `test_helpers.rs` so the stress
tests can take `n_bundle` at runtime without disturbing Stage 2d/2f:

  - `synth_chain_n(seed, k_hops, n_bundle)`
  - `split_into_bundle_snarks_n(chain, n_bundle)`

Three new `#[ignore]` integration tests, all passed:

  L = 50  / N_BUNDLE = 10: keygen 59s, 10 × prove ~104s, total 1099s
                           (~18.3 min). 11-proof bundle verified.
  L = 100 / N_BUNDLE = 20: keygen 64s, 20 × prove mean ~97s with 2
                           thermal outliers at idx 18/19 (415s/522s),
                           total 2765s (~46 min). 21-proof bundle
                           verified.
  L = 300 / N_BUNDLE = 60: keygen 89s, 60 × prove mean 105.6s
                           (min 89.3 / max 123.3, clean run no thermal
                           outliers), total 6427s (~107 min).
                           61-proof bundle verified.

Per-snark cost is constant across L = 5..300 (60× bundle width, same
per-snark cost) — linear N_BUNDLE scaling confirmed end-to-end. Proof
size unchanged 18 240 B. This establishes that the §10.2 path A escape
works at the absolute worst case, no recursive aggregation needed.

Run with e.g.
  cargo test --release --test test_bundle_stress_l50  -- --ignored --nocapture
  cargo test --release --test test_bundle_stress_l100 -- --ignored --nocapture
  cargo test --release --test test_bundle_stress_l300 -- --ignored --nocapture
The symbol K was overloaded in two roles:
  - halo2 circuit parameter (rows = 2^K), e.g. MultiHopProof at K = 16
  - chain length in hops, e.g. "a chain of K hops [hop_0..hop_{K-1}]"

Renames chain-length K to L everywhere in MULTITHREAD_CIRCUIT_SPEC.md
and adds an inline note in §4.4 calling out the convention. All
remaining K in the spec refers to the halo2 row exponent (or to
"K" as a kilo-suffix, e.g. "354 K cells"). L_MAX = 20 was already
named correctly and is unchanged.

Affected sections: §4.4 narrative + path diagram, §5 L7 walk arrow,
§6.2 snark-count formula, §6.5 case list, §6.8 bundle table header
and caption, §7 fixture table, §9.1 leak list.
§0, §1.2 and §3.6 now distinguish poseidon_dex semantics (per-thread
GlobalHistoryData; every-thread history_proofs producer; layerNumber
enforced at VM boundary; thread-0 effect comes from RootPN dapp pin)
from poseidon_profile_new (hardcoded thread 0; thread-0-only
history_proofs producer; layerNumber ignored at the callback).

The §1.2 divergence is structural: on poseidon_profile_new only thread-0
key blocks carry history_proofs (producer guard at block_producer.rs:1367
+ early-exit at history_proof.rs:189), which removes the cross-thread
C-extraction primitive of §5. Flagged inline so a future deployment
target switch is not silent.

Also fixes a stale line reference: history_proofs_l0 is at
node/libs/history-proof/src/lib.rs:181 (was :175).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Adds a small empirical section alongside the §6.8 phone-budget
estimates: dev-hardware wall times for bundle tests 2d/2e/2f/2g at
L = 5 / negatives / 20 / 50 / 100 / 300. Per-snark prove ~98-110 s
(K=19, 56 advice cols), verify ~8 ms, proof size 18 240 B constant.

Records two empirical findings useful for spec consumers:
- Linear N_BUNDLE scaling validated L=5..300 (the §10.2 OQ#1 escape
  path works at the worst case reported by the team)
- Active and all-inactive snarks have identical prove cost — §6.5
  anonymity-uniformity padding is free

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Delete circuit_helper.rs (fill_byte_range_table, sha256_pad) — leftover
  from the zkevm-hashes era; gosh-sha256-chip handles its own padding.
- Drop unused BOC parser helpers refs_count_from_repr_data,
  level_from_repr_data, data_range_in_repr_data — never called.
- Refactor boc_helper tests into mod tests, fold two duplicated
  parse-BOC tests into a single combined test.
- Remove trivial poseidon::test() that asserted nothing.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- crate::poseidon is now a thin `pub use` of
  `gosh_dense_balanced_tree::{poseidon_hash_native as poseidon_hash,
  R_F, R_P, RATE, T}`. The duplicated definitions are gone; all existing
  call-sites keep working through the unchanged `dex_halo2_circuit::poseidon::*`
  public path.
- salt.rs switches its `poseidon_hash_native` import to
  `crate::poseidon::poseidon_hash` for consistency with the rest of the
  crate.
- salt.rs module doc reworded to drop the stale references to
  `gosh-referenced-block-hop` (which doesn't live on this halo2-lib
  branch). The on-chain ABI invariant (`salt_commitment` equality across
  bundle snarks, checked by RootPN.sol) is now stated directly.
- Cargo.lock refreshed to the gosh-halo2-crypto-lib commit that exposes
  T/RATE/R_F/R_P publicly.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…tree directly

Following the previous commit's move to a single source of truth in
gosh-halo2-crypto-lib, the local re-export module in
`dex-halo2-circuit/src/poseidon.rs` was carrying zero behaviour. Removed:

- File deleted; `pub mod poseidon` line dropped from `lib.rs`.
- All in-crate uses of `crate::poseidon::*` migrated to
  `gosh_dense_balanced_tree::{poseidon_hash_native, T, RATE, R_F, R_P}`.
- External call-sites (sk-commit-tool main, halo2-proover lib,
  integration tests) updated to import from
  `gosh_dense_balanced_tree` directly; sk-commit-tool gains
  gosh-dense-balanced-tree as a dep and drops its now-unused
  dex-halo2-circuit dep.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Phase 4 (length-8 DexFinal) was speculative — never produced by any
circuit, prover, or integration test. Remove the dual-layout doc block,
match arms, offsets, helper, and unit test; rename DEX_FINAL_PHASE3_LEN
to DEX_FINAL_LEN across src + 7 test files.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ck_id

The MultiHopProof endpoint instances are salted block IDs
(Poseidon([salt, bytes_to_fr(parent_id|block_id)])). The bare
start/end names obscured that. Renamed consistently across src,
tests, and MULTITHREAD_CIRCUIT_SPEC.md; offset constants and
multihop_salted_{start,end} accessors follow suit.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace the implementation-history narrative ("Stage 1 …", "Stage 2c
will introduce …", scattered TODO(stage-2c) markers) with a compact
description aimed at a reader who only sees the current state.

The byte-flat Poseidon parity family already exists alongside the
shape-mirror family, so the TODO(stage-2c) markers were stale — each
shape-mirror doc-string now points at its byte-flat sibling instead.

TODO(phase-4-prod) on MAX_PROOF_BLOCK_REFS renamed to a stage-free
"TODO: bump to 256 for production".

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Module header no longer carries "Phase 4 / Stage 2c" project-stage
prefixes. The Phase A/B/C taxonomy stays because it maps directly to
the three circuit structs in this file. Front matter now lists the
three variants with L375/L655 line refs so a reader lands in the right
place.

Stale TODOs removed:
- TODO(stage-2c-phase-b)/TODO(stage-2c-phase-c) — variants exist in-file.
- "Phase C (later) will add …" in the Phase B section header.

The two live "Production-parity gaps" (byte-flat Poseidon chip,
MAX_PROOF_BLOCK_REFS=16 → 256) are kept under that name, no stage tag.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ess.block

Derive MAX_PROOF_BLOCK_REFS_DEPTH from MAX_PROOF_BLOCK_REFS via
next_power_of_two().ilog2() so bumping the cap (e.g. 16 → 256) needs
no second edit. The existing assert_eq!(1 << DEPTH, REFS) test now
acts as a power-of-2 invariant guard.

Rewrite HopWitness.block doc to spell out its directional role: it's
the hop's end block; the hop's start block appears inside its
proof_block_refs and is opened at ref_index via the inner path.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
`Fr::from_raw(32-byte block_id)` silently reduces mod p (BN254 Fr is
~254-bit). Distinct block_ids whose top bits cross Fr_modulus collapse to
the same Fr. Production (acki-nacki
node/libs/history-proof/src/lib.rs:159) avoids this by feeding the whole
byte stream through `PoseidonSponge::hash_bytes_flat`, which chunks at
31-byte boundaries (top byte zero ⇒ every absorbed Fr < Fr_modulus).

This commit makes the native helpers in `multi_hop_witness.rs` and
`salt.rs` match the production byte-flat rule:

- multi_hop_witness.rs:
  - delete `pack_tag_chunks` and the unsafe Fr-vector `ref_*_native` /
    `proof_block_refs_root_native` / `proof_block_ref_inner_path_native`
    / `verify_proof_block_ref_inner_path`
  - rename `*_bytes_flat_native` -> canonical `*_native`; these are now
    the sole helpers (formerly the staged production port)
  - rewrite module header to describe one rule, not two
- salt.rs: `compute_salted_block_id_native` now does
  `bytes_to_fr(hash_bytes_flat(fr_to_bytes(salt) || block_id_le))` over a
  64-byte concat
- test_helpers.rs: docstring updated to reflect the byte-flat rule

In-circuit verifiers in `multi_hop_proof.rs` and consumers in
`dark_dex_circuit_new.rs` still compute the old Fr-vector form, so any
test that runs MockProver / real-prover over them will fail until Phase
2/3 ports the in-circuit side. Native-only tests (`salt::tests`,
`multi_hop_witness::tests`, `test_helpers::synth_chain_tests`) all pass.
Phase A (`MultiHopProofCircuit`) now mirrors the byte-flat native rule.

In-circuit changes:

- `parent_id` is witnessed as 32 byte cells with explicit `range_check 8`.
  Byte-flat encoding needs byte-level access at two different split
  points (byte 25 for the ref-leaf chunking, byte 30 for the salted-
  start chunking), so the single `parent_id_fr` witness is dropped.

- Ref-leaf is now `Poseidon([c0, c1, c2])` over the byte-flat chunking
  of `tag(37 B) || parent_id(32 B)` at 31+31+7 boundaries. `c0` is a
  pure constant (`tag[0..31]` LE-packed); `c1` adds an
  `inner_product(parent_id[0..25], 256^[0..25])` (shifted by `256^6`)
  to a constant tail of `tag[31..37]`; `c2 =
  inner_product(parent_id[25..32], 256^[0..7])`.

- Ref-tree walk uses `gosh_dense_balanced_tree::dense_merkle_root_circuit`,
  fed by `preprocess_dense_proof_padded(ref_leaf_native_bytes,
  &proof_block_ref_inner_path, 0, MAX_PROOF_BLOCK_REFS_DEPTH)`. Internally
  each of the 4 levels chunks `cur(32) || sibling(32)` at 31+31+2 and
  Poseidons the 3 chunks — byte-for-byte equal to production's
  `dense_combine = hash_bytes_flat(left || right)`.

- Salted endpoints encode `fr_to_bytes(salt)(32 B) || other(32 B)` as
  `Poseidon([salt_chunk0, salt_hi + 256·other_lo30, other_hi2])`. The
  salt is decomposed once into `salt_chunk0(31 B) + salt_hi(1 B)·2^248`
  with range checks 248 / 8 and an algebraic equality back to
  `salt_assigned`. The decomposed parts are then reused for both
  `salted_start_block_id` (other = parent_id) and `salted_end_block_id`
  (other = block_id).

Helpers:

- `ref_leaf_tag_chunk0_fr` and `ref_leaf_tag_chunk1_lo_fr` replace
  `parent_tag_fr_chunks` for Phase A; the legacy `parent_tag_fr_chunks`
  is kept (with a comment) because Phase B and Phase C still consume
  it. Phase 3 removes it.

The Phase A `phase_a_single_hop_mock_prover` test passes against the
new byte-flat native helpers. Phase B and Phase C MockProver tests are
knowingly broken at this commit (native flipped in Phase 1, circuit
still Fr-vector) — Phase 3 ports them over.
Phase 3 ports MultiHopProofCircuitB and MultiHopProofCircuitC over to
the byte-flat Poseidon production rule (chunk byte stream at 31-byte
boundaries; top byte zero ⇒ every absorbed Fr < Fr_modulus), matching
the Phase 1 native helpers + Phase 2 Phase A circuit.

Per hop in both Phase B and Phase C:
- parent_id witnessed as 32 byte cells (range_check 8 each)
- Ref-leaf computed via byte-flat 31+31+7 chunks of tag(37) || parent_id(32):
  c0 = const(tag[0..31]), c1 = tag_lo_const + parent_id_lo25 · 256^6,
  c2 = inner_product(parent_id[25..32], powers_le_7) — then Poseidon([c0,c1,c2])
- Ref-tree walk delegated to gosh_dense_balanced_tree::dense_merkle_root_circuit
  fed by preprocess_dense_proof_padded for production-equivalent
  31+31+2 byte-flat Merkle hashing — no per-node 32-byte Fr decomposition
- Salted endpoints via byte-flat 31+31+2 chunks of salt(32) || other(32):
  salt decomposed once (chunk0 + hi · 2^248 = salt_assigned), other split
  into lo30 / hi2; chunk1 = salt_hi + 256 · other_lo30,
  chunk2 = inner_product(other[30..32], powers_le_2) —
  then Poseidon([salt_chunk0, chunk1, chunk2])

Phase C preserves the is_active gating semantics on all three equality
constraints (ref-tree root, SHA-256 byte equality, salted endpoint
match), plus the inactive-gated salted_start_block_id == salted_end_block_id
propagation. The internal range-checks and chunk-link constraints inside
dense_merkle_root_circuit are pure decomposition constraints and hold
for any leaf / sibling input (including zero-padded inactive hops).

Deleted: parent_tag_fr_chunks helper (legacy Fr-vector ref-leaf encoding,
no longer referenced).

MockProver tests:
- phase_b_five_hops_mock_prover ✓ (13.6 s)
- phase_c_mixed_hops_mock_prover ✓ (14.6 s)
- phase_c_all_inactive_mock_prover ✓ (12.7 s)

dark_dex_circuit_new test failures are pre-existing (legacy single-thread
circuit still uses unsafe Fr-vector Poseidon — Phase 4 scope question).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
alinaT95 and others added 30 commits July 1, 2026 21:56
Slot 0 of L7 is parent_block_id, which is same-thread by producer
construction (poseidon_dex: select_thread_last_finalized_block +
parent_height.next(&thread_id)). It cannot cross a thread boundary,
so the DEX circuit's L7 walk never opens it. Only refs[0..n]
(slots 1..n) are hop edges. Circuit simplification to follow.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…ongs to MultiHopProof

Previously misleading: labelled current_block_id/next_block_id/is_active
as "public" — they are not. Block IDs and L7 material must stay hidden
for DEX anonymity; they only leave the circuit boundary through the
enclosing MultiHopProof's salted endpoints (forward-ref to §7.3).
is_active is a MultiHopProof-level padding flag (forward-ref to §7.6),
not intrinsic to the hop primitive.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Opening L7 against block_id is a plain depth-4 Merkle path: 4 siblings,
4 SHA-256 compressions. The previous "+2 SHA to derive h8..15 from L8
and the zero-constants" was misplaced — hops do not bind L8, so h8..15
is left as an opaque witness sibling. L8 derivation is only relevant
in DexFinalProof, where the event block also opens L8.

Cascading updates:
  - §2.1: L7-opening description no longer claims h8..15 is derived
    from live L8 in general; that clause moved to DexFinalProof only.
  - §5.2 witness list: replaced "L0..L7_root, L8" with the minimal
    4-sibling set [L6, h45, h0..3, h8..15].
  - §7.1: 6→4 SHA/hop, 2.1M→1.42M cells, 42M→28.4M for 20-hop chain.
  - §7.6: H=5 budget 30→20 SHA, 10.6M→7.1M cells, margin 24%→49%.
  - §11.1: locked table reflects 4 SHA/hop.
  - §12.4: drop `l8: [u8; 32]` addition to MultiHopWitness (unneeded);
    depth-3→depth-4 delta is +1 SHA/hop (not +3).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…= 20 prototyping point

Node team specified L_MAX = 300 as the cross-thread walk-length ceiling
under the current threading design. Kept L_MAX = 20 as the current
prototyping target since §7 sizing text is written against it; noted
that N_BUNDLE = ceil(L_MAX / H) scales linearly (20 → 300 bumps
N_BUNDLE 4 → 60) without changing per-snark K. Stress path for
N_BUNDLE = 60 already exercised by test_bundle_stress_l300.rs.

Updates: §0 Terminology (L_MAX, N_BUNDLE rows), §5.4 L7-walk section,
§11.1 locked table, §11.2 open-question #6 (was "if p99 > 20"; now
reframed against the confirmed prod ceiling).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The gosh-referenced-block-hop repo is no longer a live upstream in this
workspace; the salt logic is defined locally in
dex-halo2-circuit/src/salt.rs, which remains the source of truth. The
reference dates back to the phase-3 vendoring history and is now
misleading.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…fore KZG verify

Phase 1 = cheap: salt binding, chain continuity, anchor check.
Phase 2 = expensive: N+1 Halo2 KZG verifications, only reached if
phase 1 passes.
Phase 3 = settle.

Any structural break (replay, salt mismatch, X/Y endpoint mismatch,
mid-chain break, wrong anchor layer) now bails before spending gas
on Halo2 verification.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Opening L8 in a depth-4 tree is one SHA compression per level:
  h89   = SHA(L8    ‖ 0×32)               // sibling: L9 = 0×32
  h8_11 = SHA(h89   ‖ H10_11_CONST)       // sibling: h10..11 constant
  h8_15 = SHA(h8_11 ‖ H12_15_CONST)       // sibling: h12..15 constant
  block_id = SHA(h07_witness ‖ h8_15)     // sibling: h0..7 witness

Previous formulation fused the middle two levels into one SHA and
dropped the h10..11 sibling, giving only 3 compressions — inconsistent
with §2.1 which correctly states depth-4 = 4 SHA. Cost budget in the
same section also reworded: constant siblings save witness cells but
not SHA compressions.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…, Y-side)

Reader-facing structural note before the witness/constraint block:
X-side (constraints 1-3) binds event → X.block_id via SHA-256; Y-side
(constraint 4) binds Y.block_id → finalLayerHistoricalHashRoot via
Poseidon. The two sides share no block-side witness when t ≠ 0. When
t = 0 the same block_id feeds both sides, but the two jobs remain
distinct — event→block vs block→anchor — so no crypto is repeated.
Uniformity is a shape property, not a wasted-work one.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…1-11 fixes

Recap up-front lists the corrections that shape the plan:
  * hop = 4 SHA (was 6); h8..15 opaque in hops
  * slot-0 (parent_block_id) pruned from hop primitive
  * DexFinalProof is two disjoint sub-proofs (X-side SHA, Y-side Poseidon)
  * L8 opening = 4 SHA, sibling chain h89 -> h8_11 -> h8_15 -> block_id
  * RootPN is fail-fast (cheap PI checks -> KZG verify -> settle)
  * L_MAX = 300 production ceiling (node team); prototyping still at 20

Per-section rewrites:
  * §12.1: split constants into "shared" (depth-4 shape, both circuits)
    vs "DexFinal-only" (L9..L15 zero-derived sibling constants).
  * §12.3 DarkDexCircuitV2: reorganised gates around the X/Y disjoint
    structure; L8 opening spelled out with the corrected 4-SHA chain
    and salt gates listed by instance index.
  * §12.4 MultiHopProof: two explicit changes -- (a) depth-3 to depth-4
    outer opening (+1 SHA/hop, not +3); (b) slot-0 pruning per §5.1
    (fixed tag, ref_index range 1..=N). Budget refreshed to 49% margin.
  * §12.5 bundle_verifier: aligned with §7.4 phase ordering; tail-link
    check called out as fixing a pre-existing bug independent of the
    protocol update.
  * §12.7: sizing acknowledges the 49% margin headroom (option to
    consider H=6) and references test_bundle_stress_l300.rs.
  * §12.8: RootPN item calls for parity between Solidity reverts and
    bundle_verifier errors; phone item calls for worst-case wall-time
    measurement at N_BUNDLE=60.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Replace the "corrections established earlier" bullet list with a
one-paragraph forward-looking description of the plan's dependency
shape (§12.1/§12.2 unblock §12.3; §12.4 parallel; §12.5/§12.6 feed
§12.8). Open-questions gating note retained.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…1 mention was misleading

Previous wording said "mirrors the existing L1 dense-Merkle pattern"
which conflated the X-side ext-out tree (under L8) with the Y-side
layer-1 batch tree that already lives in dark_dex_circuit_new.rs.
Reworded to keep the implementation-pattern lift note while making
it explicit that this gadget lives entirely on the X-side.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…s event_hash in-circuit

The X-side witness list previously listed event_hash as an opaque
input, skipping the fact that dark_dex_circuit_new.rs actually passes
the event BOC's two cells (root event cell + child voucher-payload
cell) as raw preimage bytes and rebuilds every hash in-circuit:

  * event_hash = SHA(root cell preimage)
  * child_hash = SHA(child cell preimage)
  * root preimage embeds child_hash at a known offset (parent→child link)
  * d1 descriptor bits check refs_count == 1 (root) / == 0 (child)
  * sk_u_commit / voucher_nominal / token_type byte-sliced from
    the child preimage with LE/BE inner-product recombines
  * ext_msg_leaf = Poseidon96(dapp_id, account_id, event_hash)
    is the ext-out-tree leaf (not event_hash directly)

parse_voucher_boc is only prover-side flattening; no crypto is
trusted from that step.

§12.3 rewritten into 7 X-side gates; §7.7 witness block + constraints
2–8 updated (old 4/5/6/7 → 5/6/7/8), lead-in bullet corrected, cell
budget refreshed to 6 SHA (2 BOC + 4 L8) + Poseidon ext-out walk
(was: 4 SHA + 8 "SHA" — the ext-out walk is Poseidon, not SHA).
§11.1 DexFinalProof K = 16 margin annotation updated to ~30 %.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Per corrected spec §§2.3, 5.1: the on-chain proof_block_refs[0] is
always same-thread by producer construction, so the DEX circuit's L7
walk never opens slot 0. Remove the dual parent/ref tag layouts and
the is_parent_slot select from hop_proof and multi_hop_proof, keep
only the 34-byte REFERENCED_REF_BLOCK_TAG layout, and range-check
ref_index to 1..MAX_PROOF_BLOCK_REFS (with an in-gate ref_index != 0
assertion). Update test_helpers::synth_chain* to build a two-slot
refs vector [placeholder, hop_predecessor] with ref_index = 1, and
add assert_ref_index_is_cross_thread for early native failure.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…block_id opening)

Restructures the DEX voucher circuit to conform to MULTITHREAD_CIRCUIT_SPEC §7.7:

* X-side (SHA family): adds `block_id_tree` module — a depth-4 SHA-256 tree
  gadget that opens `x_l8_tracked_ext_out_messages_root` (leaf-8, Poseidon
  root of the ext-out messages tree) under an opaque `h07` left sibling to
  derive `x_block_id`. Four SHA compressions on top of the existing two BOC
  hashes, plus the padded Poseidon dense Merkle from ext_msg_leaf to L8.

* Y-side (Poseidon family): opaque byte-cell witnesses for `y_block_id`,
  `y_envelope_hash`, `y_tracked_ext_out_messages_root` → `block_leaf_Y` via
  `poseidon_hash_96_circuit_bytes` → depth-8 Poseidon dense-Merkle → dense
  chain → `finalLayerHistoricalHashRoot`.

* Publics (§7.3): 8 slots — `[depositIdentifierHash, finalLayerHistoricalHashRoot,
  voucherNominalFr, tokenTypeFr, ephemeralPubkey, salted_X_start,
  salted_Y_end, salt_commitment]`. Replaces the old 7-slot layout
  (`event_salted_block_id` → `salted_X_start`/`salted_Y_end` pair).

* `TwoLevelWitnesses.block_id` now derives from `v2_x_block_id` (SHA-tree
  root) so X == Y in the uniform t=0 case.

* `base_circuit_params()`: 4 → 10 advice, 1 → 2 lookup-advice at K=19 to fit
  the added SHA compressions and byte-flat Poseidon absorbs.

* Tests: rewritten via `make_v2_circuit` / `make_v2_prover_circuit` /
  `make_v2_instances` helpers. Adds `test_dark_dex_circuit_new_cross_thread`
  (X ≠ Y positive) and three negatives (`bad_h07_sibling`,
  `bad_ephemeral_pubkey`, `bad_salted_x_start`).

Verified: 39 fast tests + all 4 slow release tests pass. Real-proof at K=19
takes ~16s prove / ~2ms verify with a 4160-byte proof. VK/proof/instances
export at W=128 writes 1674-byte VK, 4160-byte proofs, 256-byte instances
(up from 224 B due to the extra salted endpoint).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Drops the historical `_new` / `V2` suffixes now that the circuit is a
single variant: no `V1` predecessor coexists in-tree and no
`DarkDexCircuitV2` alt-branch was ever landed.

* `src/dark_dex_circuit_new.rs` → `src/dark_dex_circuit.rs`
* `DarkDexCircuitNew` → `DarkDexCircuit` (and any stale
  `DarkDexCircuitV2` references)
* `dark_dex_circuit_new` module identifier → `dark_dex_circuit`

Consumers updated: `halo2-proover/src/lib.rs`, `MULTITHREAD_CIRCUIT_SPEC.md`,
in-tree `readme.md`, and every downstream module inside
`dex-halo2-circuit/` (bundle_verifier, hop_proof, salt, test_helpers,
block_id_tree, lib, integration tests).

Pure symbol / path rename — no semantic change to the circuit.

Note: `halo2-proover` currently uses the pre-§7.7 (14-arg / 15-arg V1)
constructor call sites and is unrelated to this rename — its build was
already broken by the earlier §7.7 refactor commit and needs a separate
migration pass. The rename here keeps its imports pointing at the
correct module so that migration can proceed without a path fix.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- DexFixtureJson: optional `x_block_id_h07_sibling_hex` (serde default so
  existing fixture files still parse for stateless helpers)
- ParsedFixture: new fields `y_tracked_ext_out_root` (computed once,
  reused by pad-chain + compute_instances) and `x_block_id_h07_sibling`
- ProofOutput / InstanceValues: replace `event_salted_block_id` with
  `salted_x_start` + `salted_y_end`; `salt_commitment` stays
- compute_instances: produce 8-slot vec [poseidon_commit, final_root,
  voucher, token, eph, salted_x_start, salted_y_end, salt_commit];
  under uniform t=0, salted_x_start == salted_y_end (both from block_id)
- generate_proof: reject fixtures without h07 sibling; native depth-4
  SHA sanity check that (H07 || x_l8) reconstructs block_id
- Both DarkDexCircuit::new / ::new_for_proving call sites use the 17/18-arg
  V2 signature with X-side / Y-side split (uniform t=0 → Y_block_id ==
  X_block_id == parsed.block_id)
- base_circuit_params: bump to num_advice_per_phase=10,
  num_lookup_advice_per_phase=2 to match dex-halo2-circuit
- pub_inputs_bytes capacity: 224 → 256 (7×32 → 8×32)
- test_compute_instances_l1: checks new salted_x_start / salted_y_end
  fields and asserts equality under uniform t=0

Also: rename `block_leaf_fr` → `y_block_leaf_fr` in
dark_dex_circuit.rs (Y-side clarity; matches x_/y_ split naming used
elsewhere in the V2 refactor).

Existing fixture JSONs need regeneration with `x_block_id_h07_sibling_hex`
before generate_proof will work — stateless helpers still work.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…public_fields

Consolidates event-layout constants and the public field extractor into a
single voucher-event module. dark_dex_circuit re-imports the constants.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…_HASH_LEN

- Field + constructor param renamed for clarity (voucher-event BOC entries).
- SHA256_HASH_LEN centralised in boc_helper (tied to tvm_types::SHA256_SIZE);
  removed the three local duplicates in dark_dex_circuit, hop_proof, and
  multi_hop_proof.
- Extra doc-comment on x_block_id_h07_sibling explaining the h07 naming
  and why a single sibling suffices for the depth-4 opening.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Renames in dark_dex_circuit.rs:
- root_input_bytes / root_hash_bytes / root_child_hash_byte_offset
  -> event_root_* (they operate on the event BOC's root cell)
- block_leaf_native / block_proof -> y_block_leaf_native / y_block_proof
  (they belong to the Y-side dense-Merkle path)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The variable is the first Y-side dense-Merkle root (before the optional
chain of proofs) and the surrounding comment already calls it the
"history window root". Rename it accordingly for consistency with the
other Y-side prefixed locals.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Consistent with the other Y-side prefixed locals; this is the Y-side
finalLayerHistoricalHashRoot exposed as public instance 1.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Deduplicates the byte-flat Poseidon(salt_chunk0 ‖ block_id) sponge that
was inlined in dark_dex_circuit (salted_x_start / salted_y_end) and
duplicated as a local closure in hop_proof and multi_hop_proof. The
shared helper lives alongside its native twin compute_salted_block_id_native.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…..12]

Adds 4 public instances (LE lo/hi 128-bit halves of the two 32-byte
account fields) so the on-chain verifier can pin every DexFinalProof to
the fixed RootPN contract address. Each half is < 2^128 < p, so no
V<p canonicality gadget is required. Publics grow 8 -> 12.

Also fixes pre-existing layout drift in bundle_verifier.rs: DEX_FINAL_LEN
7 -> 12, dexfinal_offset::SALT_COMMITMENT 5 -> 7, replaces obsolete
HEAD_BLOCK_ID with explicit SALTED_X_START (5) / SALTED_Y_END (6) and
the four new account-id offsets. dex_final_head now reads from
SALTED_X_START (which is what the module doc always meant by the chain
"head"). Tail-link (salted_y_end continuity) noted as a separate TBD.

New negative test `test_dark_dex_circuit_bad_x_account_dapp_id_lo`
confirms the LE packing is copy-constrained to the byte cells feeding
`x_ext_msg_leaf`.

ABI-breaking: VK changes; tvm-sdk DEX verifier must be regenerated.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Consolidate voucher/event parsing into voucher_event_helper.rs as the
single source of truth. Moves bytes_to_fr_be, parse_voucher_boc,
VoucherFields, extract_voucher_fields, and load_first_voucher out of
test_helpers.rs. Drops the unused extract_event_public_fields (fully
subsumed by extract_voucher_fields).

test_helpers.rs loses the now-redundant EVENT_* re-import, tvm_block
Message deps, poseidon_hash_native, PrimeField, and boc_helper::*.
dark_dex_circuit.rs tests module gains a targeted import of the
moved items.
The DarkDexCircuit spec §7.7 layout is now the one and only design;
the old V1 form is gone. Purge the leftover V2/v2_ scaffolding:

* Struct fields on TwoLevelWitnesses: v2_x_block_id_h07_sibling → x_block_id_h07_sibling,
  v2_x_l8 → x_l8, v2_x_block_id → x_block_id.
* Type: V2CrossThreadWitness → CrossThreadWitness.
* Function: build_v2_cross_thread_witness → build_cross_thread_witness.
* Test-only helpers in dark_dex_circuit tests module: make_v2_circuit →
  make_circuit, make_v2_prover_circuit → make_prover_circuit,
  make_v2_instances → make_instances, make_v2_circuit_cross_thread →
  make_circuit_cross_thread.
* Comments/doc strings: strip "V2", "V1", "V2-only additions" banners.
* Fix stale `assert_eq!(instance_fr.len(), 8)` (comment still said §7.3
  V2: 8 Fr publics) — publics were extended to 12 when
  x_account_dapp_id/x_account_id lo/hi were added.
Both structs were doing the same job with confusing overlap: `block_id`
was ambiguous (was it X or Y?), `envelope_hash_bytes` didn't say which
side, and having two separate constructors forced an extra branch in
make_circuit.

Consolidated into a single DexFinalWitness with strict x_* / y_* field
prefixes aligned to spec §7.7 (X = event block on thread t, Y = anchor
block on thread 0). The uniform t=0 builder just collapses y_block_id
= x_block_id and y_tracked_ext_out_root = x_l8; the cross-thread
builder fills them independently.

- Renamed build_two_level_tree -> build_dex_final_witness_uniform.
- Renamed build_cross_thread_witness -> build_dex_final_witness_cross_thread.
- Merged make_circuit_cross_thread into make_circuit.
- make_instances now handles both cases (salted_X / salted_Y computed
  from x_/y_block_id independently).
- SynthChain::block_ids doc claimed `hops[i]` proves
  `b_i.proof_block_refs[0] == b_{i-1}`, but spec §2.3 reserves slot 0
  for the same-thread parent and §5.1 forbids opening it as a hop edge.
  Correct doc: `b_{i-1}` sits at some cross-thread `ref_index >= 1`
  slot. The code was already correct (ref_index=1, slot-0 filled with
  a placeholder).

- Renamed `DexFinalWitness::y_blocks_root_level_0` to
  `y_blocks_root_layer_1` to match spec §3 terminology (`#L1(M_Y)` is
  the *layer-1* batch root; layer numbering starts at 1). All
  callsites in dark_dex_circuit.rs updated.
The two builders were ~140 lines of near-identical code; only the Y-side
sampling differed (Uniform reuses X-side values; CrossThread draws Y
fields independently). Consolidated into a single
`build_dex_final_witness(mode, ...)` gated by a new `DexFinalMode` enum.

Callsites in dark_dex_circuit.rs updated to pass `DexFinalMode::Uniform`
or `DexFinalMode::CrossThread` explicitly.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant