Add InputOutputMismatch error.#6
Merged
Merged
Conversation
porcuquine
force-pushed
the
mismatch-error
branch
from
October 6, 2021 04:41
956ef01 to
569c8ee
Compare
asn-d6
pushed a commit
to asn-d6/Nova
that referenced
this pull request
Apr 23, 2023
…o/fix/name_space_of_witness Fix namespace of the witness
huitseeker
added a commit
to huitseeker/Nova
that referenced
this pull request
Aug 23, 2023
* doc: Improve code comments by adding backticks for formatting - Back-ticks have been added around relevant technical terms, type names, and code references within the comments to better highlight them while reading. * refactor: Refactor Spartan polynomial file organization - Refactor the structure of Spartan SNARK related modules, mainly moving and renaming `polynomial.rs` to `polys/mlpoly.rs` and introducing three new submodules under `polys`: `eq_poly`, `mlpoly`, and `unipoly`. - Implement a new module `polys` that houses refactored and newly introduced polynomial types used in the Spartan SNARK, leading to import refactors across numerous files. - Establish a new file `unipoly.rs` responsible for housing the main structs `UniPoly` and `CompressedUniPoly` * refactor: Fix comment in UniPoly storage and enhance testing - Fix comment about ordering of coefficient storage protocol in `UniPoly` and `CompressedUniPoly` structures for improved processing. - Integrated unit tests for 'from_evals_quad' and 'from_evals_cubic' in context of `pallas::Scalar` and `bn256::Scalar` types, * test: Add multilinear polynomial evaluation test - Introduced new test for multilinear polynomial evaluation in the mlpoly.rs file. * chore: rename to eq / multilinear / univariate * chore: remove unnecessary qualificaitons
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 8, 2026
…_lookup Multi-table verify path per design pin §5.1 (API). Per-table (C)-binding `∀j: poly_lookup_j(0) + poly_lookup_j(1) == T_lookup_running_j` enforced HERE — this is what M.4 owes that M.2's fold did not. Per pin §2.2 the verifier mirrors the prover's transcript schedule step-by-step: per-table `comm_L`/value-cols/`comm_ts` loop at Step 2; gated per-table α at Step 5a; sequenced per-table `r_logup_j` at Step 5b (sequencing IS domain separation per §2.3 — no per-table separator scalar absorbed); batched `comm_inv_w[*]` then `comm_inv_t[*]` at Step 6. Verifier reads the multi-table NIFS extension fields (`Vec`-typed since M.1) directly; `LookupPayloadPublicMultiTable<E>` carries only the public projection per pin §5.1. Pin §1.3 cross-table-cancellation forgery is closed STRUCTURALLY: any single-table (C)-binding failure rejects the whole step, regardless of whether a hypothetical SUM-aggregate would have cancelled it. Tests: - k=1 round-trip (`m4_round_trip_k1_homogeneous`) — regression vs the existing single-table multi-column round-trip; confirms the multi-table path accepts on a satisfying witness at k=1. - k=2 round-trip (`m4_round_trip_k2_homogeneous`) — homogeneous random tables, n_1 = n_2 = 64, distinct queries per table, asserts the per-table running-scalar VECTOR threads independently (`T_lookup[0] != T_lookup[1]`). - k=2 hard-reject (`m4_per_table_c_binding_hard_rejects_corrupted_t_lookup`) — two honest fold steps; corrupt `folded_U_s1.T_lookup[1]` with a non-zero offset; step-2 verify with the corrupted U1 must fail at the per-table (C)-binding for table_id=1 (`InvalidSumcheckProof`). Smaller version of pin §5.2 microsoft#6 (full cross-table cancellation negative test lives at M.14 in inumbra harness). All 125 vendor/nova lib tests pass under --features lookup-fold --release per .claude/rules/testing.md (143s). GH-microsoft#2 sub-stage M.4 of M.1–M.16. M.6 (in-circuit AllocatedNIFS::verify_with_multi_table_lookup) follows in next dispatch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 8, 2026
…ect (pin §5.2 microsoft#6) Lands the canonical regression check that the VECTOR running-claim composition closes pin §1.3's cross-table cancellation forgery vector at the per-table (C)-binding inside `verify_with_multi_table_lookup`. Test: `m14_cross_table_cancellation_hard_rejects` (`vendor/nova/src/neutron/nifs.rs::tests`, `#[cfg(feature = "lookup-fold")]`). ## Pin §5.2 microsoft#6 obligation Synthesise a multi-table fold step where the prover supplies bundles for T_1 and T_2 with deliberately-corrupted witnesses such that `Σ inv_w_1 − Σ inv_t_1 = +Δ` and `Σ inv_w_2 − Σ inv_t_2 = −Δ`. A hypothetical SUM-aggregate (C)-binding `Σ_j (poly_j(0) + poly_j(1)) == Σ_j T_running_j` would succeed by cancellation; assert `verify_with_multi_table_lookup` REJECTS at the per-table (C)-binding for T_1. ## Test shape (mirrors the M.4 hard-reject pattern) 1. k=2 homogeneous-size random tables (n_1 = n_2 = 64). The cancellation property is size-independent per pin §1.3, so homogeneous sizes preserve narrative coherence with the M.4 sibling without weakening the obligation. 2. Honest step 1 prove → honest `folded_U_s1.T_lookup = [t1_HONEST, t2_HONEST]`. 3. Honest step 2 prove + verify (positive control: must accept). 4. **Direction A — forward cancellation** (+Δ on T_1, −Δ on T_2): pre-step-2-verify, mutate `folded_U_s1.T_lookup` to `[t1_HONEST + Δ, t2_HONEST − Δ]`. Aggregate `(t1+Δ) + (t2−Δ) = t1 + t2` is preserved by construction. Verify rejects with `NovaError::InvalidSumcheckProof` at the per-table (C)-binding loop (`nifs.rs:1977-1990`, first-fire at j=0). 5. **Direction B — reverse cancellation** (−Δ' on T_1, +Δ' on T_2): sign-swap symmetry control. Different Δ' ChaCha20Rng draw, distinct corruption payload, same per-table reject semantics. Both directions emit explicit `aggregate_honest == aggregate_corrupt` assertions before the verify call, making the structural property pin §1.3 names as the forgery condition (the SUM-aggregate cancellation invariant) audit-visible. ## VECTOR composition closure The per-table (C)-binding loop at `nifs.rs:1977-1990` checks `poly_lookup_j(0) + poly_lookup_j(1) == T_lookup_running_j` per j and returns `Err(InvalidSumcheckProof)` on the first failing table. M.4's sibling `m4_per_table_c_binding_hard_rejects_corrupted_t_lookup` covers single-table corruption (Δ on T_2 alone, T_1 honest); this M.14 test covers the symmetric cancellation pattern. M.4 closes "single-table corruption is caught"; M.14 closes "cross-table cancellation does not bypass the per-table check". The j=0 first-fire is structural (the loop is j-ascending). For documentation: T_2's check would also reject if reached, since `poly_lookup_2(0) + poly_lookup_2(1) = t2_HONEST` mismatches the corrupt running scalar `t2_HONEST − Δ` (or `t2_HONEST + Δ'` in Direction B). ## Determinism Seed `0xC1BE_CA1E` ("cancellation") via `ChaCha20Rng::seed_from_u64`, per `.claude/rules/cryptography.md` reviewer-reproducibility discipline (US-05). Both Δ values drawn from the same stream; `assert_ne!(delta, Scalar::ZERO)` guards against vacuous corruption. ## Audit-trail framing Test header cites pin §5.2 microsoft#6 (line 561), pin §1.3 forgery vector (line 90), and pin §3 VECTOR composition for the auditor's hand-off. The (C)-binding call-site is named explicitly (`vendor/nova/src/neutron/nifs.rs:1989`). ## Verification ``` cargo test --release -p nova-snark --features lookup-fold m14_cross_table_cancellation_hard_rejects ``` passes in 0.20s release-mode. Full neutron-suite regression (`cargo test --release -p nova-snark --features lookup-fold neutron::`) passes 40/40, no regressions in M.4 / M.6 / M.6.5 / M.12 family. ## Halt-and-ask trigger (per dispatch) If `verify_with_multi_table_lookup` ACCEPTS either corrupted bundle pair, this is a soundness-class incident — pin §1.3's forgery vector is open at vendor HEAD. The `assert!(matches!(... Err(...)))` panic IS the halt signal. (Did not fire; the per-table check rejects both directions as designed.) ## Refs - Pin: `docs/research/cryptography/c1-beta-multi-table-fold-design-pin-2026-05-08.md` §5.2 microsoft#6 (line 561), §1.3 (line 90), §3 (VECTOR composition). - Cryptography rule: `.claude/rules/cryptography.md` (Gadget contract, ≥1000-iter behavioural earned-trust adjacent layer; this single test is the *negative* arm complementing the M.8 ≥1000-iter positive arm). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 9, 2026
…h Y extension to T_lookup_per_table - default_with_lookup_k: allocate T_lookup_zero = alloc_zero(...) once, clone across k slots; each T_lookup_per_table[j] inherits (0)·(0) = T_lookup_zero zero-binding constraint - Variable-identity binding test (extends M.GH5.0 STAGE 0 module) - pp_digest baselines unchanged (default_with_lookup_k is #[allow(dead_code)] until M.GH5.3 wires synthesize_base_case through this constructor; the production augmented circuit's R1CS shape is not affected at this milestone — Pallas/Bn256IPA/Secp256k1 expects all hold) Closes the IVC-anchor constraint-binding gap surfaced during M.GH5.2 review. Same class as Corrigendum microsoft#4's X-side fix; same precedent for test-shape adaptation. Halpert-ratified per Corrigendum microsoft#6. Test extension (m_gh5_0_path_y_x_t_aliasing_binding): + Cases (1, Some(2)) and (2, Some(2)) — k=2 production arity per ADR-0021 + Variable-identity binding: T_lookup_per_table[j].get_variable() == T_lookup_per_table[0].get_variable() for all j ∈ [1, k) — intra-Vec aliasing form (TestConstraintSystem does not support post-allocation witness mutation; Corrigendum microsoft#4-A precedent for adapted assertion) + Distinctness from T: T_lookup_per_table[0].get_variable() != T.get_variable() — confirms Halpert's recommended SEPARATE T_lookup_zero (not aliased to T) + Constraint-count floor: default_with_lookup_k MUST emit ≥ 6 constraints (default(num_io) baseline 5 + 1 from T_lookup_zero alloc_zero), strictly exceeding the default(num_io) baseline Pre/post numbers (TestConstraintSystem at num_io=1, k=2, Bn256EngineKZG): pre-fix: num_constraints=5, T_lookup_per_table[0]=Aux(5), T_lookup_per_table[1]=Aux(6) — distinct fresh aux per slot, ZERO new constraints (the gap Corrigendum microsoft#6 closes) post-fix: num_constraints=6, T_lookup_per_table[0]=Aux(5), T_lookup_per_table[1]=Aux(5) — shared T_lookup_zero, (0)·(0) = T_lookup_zero constraint enforced Adversary-side: TestConstraintSystem does not expose post-allocation witness mutation; per Corrigendum microsoft#4-A precedent the witness-injection negative test is a structural counterfactual under Path Y. The variable-identity assertion algebraically subsumes it: a malicious prover attempting T_lookup_per_table[j] = N ≠ 0 would attempt T_lookup_zero = N, rejected directly by alloc_zero's row at synthesis. Pin: docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md §1.4 Corrigendum microsoft#6 Roadmap: docs/feature/microsoftgh-5-augmented-circuit-wireup/deliver/roadmap.json row 01-03 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 10, 2026
…p-fold wire-up Wires NeutronAugmentedCircuit::synthesize_non_base_case through verify_with_multi_table_lookup and synthesize_base_case through default_with_lookup_k under the lookup-fold cfg + runtime gate. Closes (W3) plumbing and (W4) confirmation per pin §1.4. Vendor-side surface: - NeutronAugmentedCircuitInputs: +public_bundles_multi_table field (Option<Vec<LookupPayloadPublicMultiTable<E>>>) per pin §3.1 - NeutronAugmentedCircuit struct: +shape_registry, +lookup_fold_k, +index_n_bits fields; with_lookup_fold(k, registry, bits) builder (#[allow(dead_code)] until M.GH5.4 inumbra-side wire-up) - alloc_with_k_hint: T_lookup_per_table allocation branches on inst.t_lookup() Some/None × k > 0 hint - synthesize_base_case: under #[cfg(feature = "lookup-fold")] dispatches to default_with_lookup_k(cs, 1, k) when lookup_fold_k > 0; else default(cs, 1) - synthesize_non_base_case: under same cfg dispatches to new private synthesize_non_base_case_lookup_fold method when lookup_fold_k > 0; else legacy nifs.verify - synthesize_non_base_case_lookup_fold: allocates chunk_index_in_z = U.X[0], shape_registry, AllocatedLookupNIFSMultiTable, per-bundle AllocatedLookupPayloadPublicMultiTable; invokes verify_with_multi_table_lookup; rebinds post-fold T_lookup_per_table via from_lookup_fold_output (no-constraint structural rewire) - AllocatedLookupPayloadPublicMultiTable::alloc helper Halpert ratification (2026-05-09 dispatch, all 6 questions RATIFY, High confidence): - Q1 Option B (cfg + runtime lookup_fold_k > 0 gate): selected per Principle 7 + ADR-0023 vendor-fork separability. lookup_fold_k is construction-time pinned and pp_digest-shape-bound; no downgrade attack possible. - Q2 Argument-order canonical, table_id-traversal mechanical (Vec iter preserves order at every fold depth). - Q3 lookup_fold_k as usize correct at M.GH5.3; per-position uniformity assertion deferred to M.GH5.4 per Auditor Obligation 10. - Q4 M.7 shape-registry assertion fires BEFORE pp_digest.absorb per pin §2.5 (vendor/nova/src/neutron/circuit/nifs.rs:689-698 direct verification). Dispatch text's "AFTER" formulation was a misstatement; STOP-AND-ASK NOT triggered. - Q5 (W4) Phase-1↔Phase-2 binding closed: clone() on AllocatedNum preserves Variable identity, so Phase-1 hash binding of U.T_lookup_per_table transitively binds Phase-2 verifier inputs. - Q6 from_lookup_fold_output no-constraint rewire is sound; (C)-binding at nifs.rs:872-897 takes the binding role at fold-depth ≥ 1 that alloc_zero plays at base case. Path Y / microsoft#4-A invariants are base-case-only. Test posture preserved at M.GH5.2 close baseline: - vendor --release --features lookup-fold: 152/0/7 - vendor --release (default): 80/0/6 - inumbra-spend-circuits: 87/0/9 lib + 4 RED scaffolds - inumbra-spend-harness: 13/0 - M.GH5.0 STAGE 0 + Corrigendum microsoft#4-A + Corrigendum microsoft#6 tests: pass - pp_digest baselines unchanged (vendor IVC tests on legacy path; refresh deferred to M.GH5.4 when inumbra-side wires with_lookup_fold(2, ...)) - Determinism verified across 2 consecutive runs. Pin: docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md §3.1 + §3.2 + §3.4 + §5.1 + §5.5 row M.GH5.3 Roadmap: docs/feature/microsoftgh-5-augmented-circuit-wireup/deliver/roadmap.json row 01-04 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 11, 2026
… threads shape_registry to NeutronAugmentedCircuit::new Per pin §5.5 row M.GH5.4 (post-Corrigendum-microsoft#8 reverted scope) sub- deliverable 2: - Extend `PublicParams::setup` and `setup_with_ptau_dir` under `feature = "lookup-fold"` to accept `(shape_registry: Vec<E1::Scalar>, lookup_fold_k: usize, index_n_bits: usize)`. Threaded to the shape- derivation `NeutronAugmentedCircuit::new` call via `with_lookup_fold(...)`. Non-`lookup-fold` builds keep the pre-M.GH5.4 signature (vendor examples / benches build unchanged). - Store the registry triple on `PublicParams` under `lookup-fold`, `#[serde(skip)]`-gated so the bincode encoding (and therefore `pp_digest`) is byte-equivalent to pre-M.GH5.4 at the default `(vec![], 0, 0)` state. Vendor-internal `test_pp_digest` baselines do NOT refresh — confirmed empirically: 152/0/7 release sweep matches pre-M.GH5.4 baseline byte-for-byte. - `RecursiveSNARK::new` (base case) and `RecursiveSNARK::prove_step` read the triple from `pp` and chain `with_lookup_fold(pp.lookup_fold_k, &pp.shape_registry, pp.index_n_bits)` on each `NeutronAugmentedCircuit::new`. This closes the four invocation sites the pin §3.1 binding requires (the augmented-circuit shape-derivation site + the prove-step site must emit byte-equivalent R1CS, which they do because both threads the same triple from `pp`). - Lift `#[allow(dead_code)] until M.GH5.4` on `NeutronAugmentedCircuit::with_lookup_fold` (vendor `circuit/mod.rs:268`). The `with_multi_table_bundles` annotation (`circuit/mod.rs:139`) stays — its per-step consumer wires up at M.GH5.5 (the inumbra-side fold-of-N happy-path differential). - Vendor-internal `TrivialCircuit` / `CubicCircuit` test sites updated to pass `(vec![], 0, 0)` under `lookup-fold` (the default lookup- fold-OFF state); shape and `pp_digest` byte-equivalent to pre-M.GH5.4. Sub-deliverable 1 (inumbra-side consumer wire-up) is a no-op at this milestone: there is no inumbra-side consumer of `neutron::PublicParams::setup` yet (wrap.rs is on `nova_snark::nova::*` per Corrigendum microsoft#8; will stay through M.GH5.9; Stage K migration dispatched as separate GH-microsoft#7). `build_chunk_step_registry` (M.10 / `shape_registry.rs:224`) is ready to be invoked by M.GH5.5 when the inumbra-side fold-of-N differential dispatches against the augmented-circuit IVC. Auditor Obligation 10 confirmed by construction at `shape_registry.rs:347`: `vec![merged_mc, chunk_mc]` (length 2) inside the `0..NUM_CHUNK_POSITIONS=16` loop — k=2 uniform across all 16 chunked-Strauss-Shamir positions per ADR-0021. Test results (release-mode per `.claude/rules/testing.md`): - vendor `cargo test --release -p nova-snark --features lookup-fold`: 152/0/7 (matches pre-M.GH5.4 baseline; no `pp_digest` refresh needed — the `#[serde(skip)]` design preserves the bincode encoding). - inumbra-spend-circuits lib: 87/0/9 + 4 RED scaffolds (baseline). - inumbra-spend-harness: 13/0 (baseline). - M.GH5.0 STAGE 0 + Corrigendum microsoft#4-A + Corrigendum microsoft#6 tests pass. Closes (W4) plumbing per pin §5.5. Wire-up consumer at M.GH5.5. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 12, 2026
…commitment Vec extension
Widens `FoldedInstance::{comm_L, comm_ts, comm_inv_w, comm_inv_t}` at
`vendor/nova/src/neutron/relation.rs:246-264` from scalar
`Option<Commitment<E>>` to per-table `Option<Vec<Commitment<E>>>`,
mirroring the already-landed `T_lookup: Option<Vec<E::Scalar>>` extension
at line 265 (GH-microsoft#2 M.2 structural mirror). Lifts the per-`X` scalar
`fold_one` body at `relation.rs:802-826` to a per-`j` loop running the
linear-combination `comm_X_j_fold = (1 - r_b) * comm_X_j_running + r_b *
payload_per_table[j].comm_X` independently for each
`(X, j) ∈ {L, ts, inv_w, inv_t} × {0, ..., k-1}` under common `r_b`.
This is a **HARD PREREQUISITE** for M.GH7.0 — without the per-table Vec
extension, the §1.2(b)/(c) Spartan bridge-reduction has no per-table
running commitments to consume.
## Soundness sketch (Corrigendum microsoft#6 §1.3 lines 166-241)
FoldedInstance-level per-table-independent-fold-under-common-`r_b`
binding reduces to four paper-grounded primitives composed:
1. **PCS binding at each `(X, j)` pair independently** — Pedersen
homomorphism (1991) + KZG eprint 2010/096.
2. **RO2 collision-resistance over `table_id`-canonical absorption
ordering** — Fischlin 2005 / Lasso §2.3 FS analysis. Per-step NIFS
absorbs `comm_inv_w_vec[0..k]` then `comm_inv_t_vec[0..k]` in
canonical order at `nifs.rs:1497-1556` BEFORE `r_b` is squeezed; the
FoldedInstance-level fold preserves the order.
3. **No cross-`j` term under common `r_b`** — the fold body
`comm_X_j_fold = (1 - r_b) * comm_X_j_1 + r_b * comm_X_j_2` is a
linear combination over a SINGLE table's commitments at each `j`
(Falsifier B verified-absent at the algebra).
4. **Path β per-step binding composes into FoldedInstance level** —
GH-microsoft#2 Path β at `c1-beta-multi-table-fold-design-pin-2026-05-08.md`
§A.2.4 (per-step ratified) extended upward via Nova binding-by-hash
composition (eprint 2021/370 v3 §4).
Both falsifiers verified-absent at vendor HEAD per Corrigendum microsoft#6: (A)
per-step NIFS-message Vec-typed inverse commitments persist across
steps at `nifs.rs:256-260`; (B) primitive 3's per-`j` independence is
structural at the algebra level. Confidence promoted Medium → Medium-
High per §6.1 row M.GH7.0a.
## Implementation
- `relation.rs:246-264`: four `comm_X` fields widened to
`Option<Vec<Commitment<E>>>`. `T_lookup_per_table` at line 265
unchanged (already Vec-typed since GH-microsoft#2 M.2).
- `relation.rs:fold_with_lookup`: signature change from singular
`payload: &LookupPayload<E>` to per-table `payload_per_table:
&[LookupPayload<E>]`; body lifted from per-`X` scalar to per-`(X, j)`
Vec loop. Length-mismatch fails-closed with `NovaError::InvalidStructure`.
- `relation.rs:fold` (R1CS-only): per-table Vecs passed through via
`.clone()` (Vec is not `Copy`).
- `nifs.rs:prove_with_multi_table_lookup_inner` + `verify_with_multi_table_lookup`:
replaced the singular `effective_payload = bundles[0]` collapse (k=1
byte-equivalence routing per pre-M.GH7.0a M.3 commentary at
`nifs.rs:2039-2045`) with per-table construction in `table_id`-canonical
order. K=1 single-table degenerates byte-identically via
`std::slice::from_ref(&effective_payload)`.
- Single-table callers (`prove_with_lookup`, `verify_with_lookup`,
`prove_with_multi_column_lookup`, `verify_with_multi_column_lookup`):
wrap singular `effective_payload` with `std::slice::from_ref` at the
fold-with-lookup call site.
**No `AllocatedFoldedInstance` extension needed** per Corrigendum microsoft#1 —
binding-via-hash at GH-microsoft#5 (W1) carries the four `comm_X` fields through
`u.X[0]`; `AllocatedFoldedInstance` at `circuit/relation.rs:26-56` does
not hold the four commitments and does not need to.
## Tests
Three tests added to `neutron::relation::tests` module
(`vendor/nova/src/neutron/relation.rs`):
- `test_folded_instance_per_table_vec_extension_binding` — k=2 single
fold from outer base; asserts `FoldedInstance::{comm_L, comm_ts,
comm_inv_w, comm_inv_t}` are populated as `Some(Vec<Commitment<E>>)`
of length 2; per-`j` outer-base body `comm_X_j_fold = r_b *
fresh_per_table[j].comm_X`.
- `fold_with_lookup_per_table_no_cross_j_interference` — Falsifier B
negative test: corrupting `fresh_per_table[1].comm_X` for each
`X ∈ {L, ts, inv_w, inv_t}` leaves `folded.comm_X_per_table[0]`
unchanged (Corrigendum microsoft#6 primitive 3). Includes counter-check that
`comm_X_per_table[1]` DOES change (homomorphic propagation of the
corrupted fresh input).
- `fold_with_lookup_per_table_differential_against_reference_1000_iter`
— 1000-iter ChaCha20Rng-seeded differential against the off-circuit
reference formula per Gadget contract (`.claude/rules/cryptography.md`
≥ 1000-iter behavioural earned-trust threshold). Single fixed seed
`0xC1BE_5BAD_C0DE_700A` for US-05 reviewer-reproducibility. Runs
~7.6s in release mode.
Pre-existing `fold_with_lookup_threads_per_table_running_scalars_k2`
test (GH-microsoft#2 M.2 regression) updated to pass per-table payload slice
through the new signature; semantics unchanged.
## Verification
- `cargo check -p nova-snark --features lookup-fold --all-targets
--release`: clean.
- `cargo check -p nova-snark --all-targets --release` (without
lookup-fold): clean — the widening is fully `#[cfg(feature =
"lookup-fold")]` gated; non-lookup-fold builds unaffected.
- `cargo test -p nova-snark --features lookup-fold --release`: 156
passed, 7 ignored, 0 failures. Includes all 5 tests in
`neutron::relation::tests`.
- `cargo test --workspace --release`: clean except 4 pre-existing
`arity_envelope_acceptance.rs` RED scaffold `unimplemented!()` panics
(verified pre-existing via `git stash` cross-check; unrelated to
M.GH7.0a; downstream feature work).
- `cargo test -p inumbra-spend-harness --release --test
m11_fold_of_four_absent_table_differential`: 2 passed (1000-iter
fold-of-four 21min).
- `cargo test -p inumbra-spend-harness --release --test
m_gh5_6_running_scalar_reference_differential`: 1 passed (1000-iter
running-scalar 6min).
- `cargo test -p inumbra-spend-harness --release --test
m_gh5_7_negative_test_triple`: 4 passed.
- `cargo test -p inumbra-spend-harness --release --test
multi_table_lookup_fold_differential --test
lookup_fold_differential`: 5 passed.
Step-ID: 01-01
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…ld negative-test triple per Corrigendum microsoft#15 + sub-ratification (Constraint hygiene §70-78 discharge; AO 19 FULL) Three #[test] functions in vendor/nova/src/neutron/mod.rs #[cfg(test)] mod tests, sibling to the M.GH7.3a positive-path acceptance test at mod.rs:1466-1900. Discharges .claude/rules/cryptography.md §70-78 ("Constraint hygiene; a missing constraint is a forgery vector") for the M.GH7.3a public prover API surface: RecursiveSNARK::prove_step_with_lookup_fold sibling + LookupStepCircuit<E> trait + RecursiveSNARK::running_lws field + PublicParams::setup lookup_shape parameter, landed at e3fe75d. Per Corrigendum microsoft#15 + 2026-05-12 late-evening Sub-ratification in docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md §0 entry 15 + §3.1.1 + §5.5 row M.GH7.3b: test (i) `prove_step_with_lookup_fold_corrupt_t_at_index_in_consumed_u1 _rejects_at_r1cs_c_binding` Corrupt verifier-input U1.T += Scalar::ONE; reject at R1CS-side (C)-binding (nifs.rs:2000-2001, Step 7). Anchored on Nova 2021/370 v3 §3 R1CS sumcheck soundness. (RE-TARGETED per Sub-ratification — Corrigendum microsoft#15's original bundles[j].running_lw corruption was structurally inadequate at the (C)-binding rejection mechanism because LookupSumcheckInstance::prove_step at lookup_sumcheck.rs:278-285 sets evals[1] := t_lookup_running − evals[0] BY CONSTRUCTION, making poly_lookup_j(0)+poly_lookup_j(1) = t_lookup_running_j a TAUTOLOGY for any honestly-produced polynomial. Fifth Halpert-class verify-don't-assume failure named.) test (ii) `prove_step_with_lookup_fold_post_prove_mutate_poly_lookup _via_nifs_rebuild_rejects_at_lookup_c_binding` Mutate nifs.poly_lookup[0].coeffs[0] += Scalar::ONE (ADDITIVE, per Sub-ratification — replaces Corrigendum microsoft#15's original multiplicative × 2 which preserved the (C)-binding tautology under all-zero T_lookup_running = 0); reject at lookup-side (C)-binding (nifs.rs:2025-2028, Step 8). Anchored on FS-NIZK soundness (Fischlin-Fischlin 2005). test (iii) `prove_step_with_lookup_fold_corrupt_t_lookup_at_index_in _consumed_u1_rejects_at_lookup_c_binding` Corrupt verifier-input U1.T_lookup[0] += Scalar::ONE; reject at lookup-side (C)-binding (nifs.rs:2025-2028, Step 8). Anchored on Nova 2021/370 v3 §4 binding-by-hash composition. (STANDS verbatim from Corrigendum microsoft#15.) All three reject with NovaError::InvalidSumcheckProof, asserted via the M.14 typed-variant pattern at nifs.rs:6140. Implementation pattern follows the M.14 precedent at nifs.rs:5719-6149 (direct NIFS::prove_with_multi_table_lookup at vendor-test scope) — per Sub-ratification Gap-2 clarification, RecursiveSNARK has no `nifs` field at vendor HEAD e3fe75d so extraction is structurally impossible; the direct-NIFS pattern routes through the same (C)-binding algebra that prove_step_with_lookup_fold invokes internally. Fixture: AbsentTableStepCircuit-style — K=1, TABLE_SIZE=4, TABLE_LOG2=2, Bn256EngineKZG + GrumpkinEngine, single empty-columns multi_column_table — inherited from the M.GH7.3a positive-path acceptance test. No fixture amendment required (NEITHER Option A NOR Option B from the original dispatch brief). The three algebraic preconditions (BN254 scalar field characteristic odd; rho ≠ ONE w.o.p. under RO-squeeze; prime field of size ≥ 2) hold under this fixture. Deterministic seeds 0xC1BE_5BAD_C0DE_703{1,2,3} per US-05. Test verdicts (release-mode, scoped, by name): test (i) 1 passed (0.19s) test (ii) 1 passed (0.19s) test (iii) 1 passed (0.18s) M.GH7.3a positive-path regression 1 passed (0.70s) Empirical-close of STOP-AND-ASK triggers: microsoft#1 accessor-surface gap verified absent (NIFS::poly_lookup and UniPoly::coeffs are pub; FoldedInstance.T and .T_lookup pub(crate) accessible from sibling test module). microsoft#2 rejection-variant divergence verified absent (all three reject with InvalidSumcheckProof). microsoft#3 loop-iteration-order verified absent (K=1, single iteration). microsoft#4 positive-baseline regression verified absent (M.GH7.3a positive-path still GREEN). microsoft#5 (NEW) test (i) rejection-locus empirically confirmed at R1CS-side (C)-binding (nifs.rs:2001:7) via distinguishing-panic probe (probe removed before commit; vendor working tree clean at nifs.rs). microsoft#6 (NEW) test (ii) additive-mutation effectiveness empirically confirmed (in-test assert that mutated_sum = honest_sum + 2·ONE in BN254 scalar field of odd characteristic). AO 19 FULL discharge: completes the partial discharge from M.GH7.3a's positive-path round-trip per Corrigendum microsoft#15 §6.3 AO 19 boundary refinement (unchanged by Sub-ratification). No new Pass Criterion at M.GH7.0.5; no new auditor obligation; no algebra change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…rewires for per-table FS-transcript per Corrigendum microsoft#16 sub-ratification (D-i); AO 22 discharge with IVC↔Spartan binding-deferral routed to M.GH7.5 path (b) Authors the M.GH7.4c envelope-side wire-up of the M.GH7.4a/4b Spartan- sibling-with-logup path through `CompressedSNARK<E, EE>` per the Corrigendum microsoft#16 sub-ratification (D-i)/(P1) at superproject `ce032d9`. Scope (per sub-ratification §5.5 row M.GH7.4c crisp scope): 1. Lift M.GH7.4b synthetic-data helpers `build_honest_logup_witnesses` and `build_per_table_commitments` from `#[cfg(test)] mod tests` at `vendor/nova/src/spartan/snark.rs:2780-2907` to `pub(crate)` envelope scope at `vendor/nova/src/neutron/compressed_snark.rs`. Gate microsoft#10 preservation: helpers preserved VERBATIM — LogUp- consistency-by-construction (the (A)+(B)+(C) Haböck §3 identities hold pointwise at the helper's internal `r_logup_j` via `batch_invert_plus_r`). 2. Extend `CompressedSNARK<E, EE>` envelope struct (NOT `BridgedNeutronInstance` per (D-i) gate microsoft#7 resolution) with six new fields carrying per-table commitments + `T_lookup` data + per-table `r_logup` scalars. Fields are empty `Vec::new()` at k=0 (STAGE-0 path) and populated by the prover at k>0. 3. Rewire `prove_from_parts` to invoke `prove_with_T_claim_split_error_with_logup` (M.GH7.4a/4b sibling) with empty per-table slices at k=0. The `_with_logup` sibling at k=0 is byte-functionally equivalent to the β' sibling (no per-table absorption; empty per-table residue body; identical batch_eval_reduce u_vec/w_vec at `3 + 4·0 = 3` entries). M.GH7.0.2 envelope regression tests pass under unconditional rewiring because verify-side is also rewired uniformly. 4. Author `pub(crate) fn prove_from_parts_with_logup(...)` — the M.GH7.4c acceptance-test entry point at k>0. Performs the envelope- side per-table FS-transcript discipline per dispatch authoring steps (6) + (7): - Absorb `comm_L_j`, `comm_ts_j`, `comm_inv_w_j`, `comm_inv_t_j`, `T_lookup_j` in `table_id`-canonical order at envelope-side transcript `b"NeutronCompressedSNARK_envelope"`. - Squeeze per-table `r_logup_j` sequentially (mirroring `nifs.rs:1492-1495` vendor NIFS-side discipline). - Invoke `_with_logup` sibling with prover-threaded per-table polynomial slices, per-table commitments, and (under (D-i)/(P1) binding-deferral disposition) the witness-construction `r_logup_per_table` (NOT the FS-squeezed value). 5. Rewire `CompressedSNARK::verify` to mirror the prover's per-table absorption + FS-squeeze sequence, then invoke `verify_with_T_claim_split_error_with_logup` (M.GH7.4b sibling) with the proof-envelope-carried `per_table_r_logup` scalars. 6. Add the M.GH7.4c end-to-end positive-path acceptance test at `vendor/nova/src/neutron/compressed_snark.rs::tests::m_gh7_4c_compressed_snark_end_to_end_with_per_table_lookup_envelope_transcript` — exercises `CompressedSNARK::prove_from_parts_with_logup → CompressedSNARK::verify` round-trip at `num_cons = 8, k = 2, table_size = 4` with envelope-built synthetic per-table data. Deterministic seed `0xC1BE_5BAD_C0DE_704Cu64`. IVC↔Spartan binding-deferral disposition under (D-i)/(P1) — Gate microsoft#11 narration discipline: Per-table commitments are envelope-fresh at length `num_cons` (R1CS- row domain), STRUCTURALLY DISTINCT from any IVC-layer `r_U.comm_L[j]` (witness-address domain, length `n_w`). The envelope FS squeeze of `r_logup_j` is STRUCTURALLY EXERCISED for transcript discipline (the audit-firm engagement can inspect the FS log) but the squeezed value is DISCARDED at M.GH7.4c — the sibling's LogUp-identity algebra closes against the prover-threaded `r_logup_per_table` (built INSIDE `build_honest_logup_witnesses`). The IVC↔Spartan binding between the envelope-fresh per-table commitments and the IVC-trace data lives at M.GH7.5 path (b) — to be crisped by Halpert authoring of the binding- discharge mechanism specification. Candidate mechanisms: (i) Two-round FS discipline: re-derive `r_logup_j` from FS during witness construction, with separate absorptions of `(L, ts, T)` and `(inv_w, inv_t)` either side of the per-`j` squeeze. (ii) Σ-protocol equality-of-opening between IVC-layer `r_U.comm_L[j]` and envelope-side `per_table_comm_L[j]` (analogous to Corrigendum microsoft#11's `SigmaE2EqualityProof`). (iii) Augmented-circuit-final-step absorption of envelope-side per-table commitments into the IVC public input. If M.GH7.5 path (b) cannot implement any of (i)/(ii)/(iii), the (D-i) ratification flips to (P3) per the sub-ratification's STOP-AND-ASK trigger #M.GH7.5.2. Regression invariants verified at vendor HEAD: - test_pp_digest (neutron + nova): 2/2 pass. - test_ivc_trivial (neutron + nova): 2/2 pass. - test_ivc_nontrivial_neutron: 1/1 pass. - test_ivc_base (neutron + nova): 2/2 pass. - test_setup (neutron + nova): 2/2 pass. - m_gh7_0_0b (3 tests including 1000-iter differential): 3/3 pass. - m_gh7_0_2 envelope regression (acceptance + negative + 1000-iter): 3/3 pass; the 1000-iter Pedersen-additive binding differential confirms the unconditional rewiring of `prove_from_parts` through `_with_logup` at k=0 is byte-functionally identical to the prior β' path. - m_gh7_3a positive-path: 1/1 pass. - m_gh7_4a/4a-degree-3-empirical/4b PCS-opening: 4/4 pass. - m_gh7_4c acceptance test: 1/1 pass — END-TO-END envelope-transcript round-trip at `num_cons = 8, k = 2, table_size = 4` closes. STOP-AND-ASK gate dispositions: Gate microsoft#6 FS-transcript independence: PRESERVED. Envelope-side absorbs happen on `b"NeutronCompressedSNARK_envelope"`; Spartan-side initialises FRESH `b"RelaxedR1CSSNARK"` per `snark.rs:1395`. The two transcripts NEVER share bytes — M.GH7.4a's note at `snark.rs:1755-1762` re-verified at vendor HEAD. Gate microsoft#7 STRUCT EXTENSION VS SIBLING: RESOLVED by sub-ratification — `BridgedNeutronInstance<E>` UNCHANGED; `CompressedSNARK<E, EE>` extended with six per-table Vec fields. Gate microsoft#8 KPI microsoft#2 proof-size: at fixture (num_cons=8, k=2), envelope grows by ~832 bytes (commitments + `r_logup` + length-8 T_lookup polys). Production-scale `T_lookup` carriage in `CompressedSNARK<E, EE>` is a future-milestone optimisation (move to `VerifierKey<E, EE>` or `pp`-level once binding-discharge mechanism is crisped at M.GH7.5). At M.GH7.4c fixture scale, growth is well under 12 KB. Gate microsoft#9 M.GH7.5 reachability: documented in acceptance test code comment + verify body comment + struct field doc-comments. M.GH7.5 path (b) is load-bearing for (D-i) soundness composition. Gate microsoft#10 LogUp-consistency of lifted helpers: PRESERVED VERBATIM from M.GH7.4b — helpers byte-equivalent at the algorithmic level. Gate microsoft#11 IVC↔Spartan binding-deferral narration: DOCUMENTED EXPLICITLY in acceptance test code comment (lines documenting "M.GH7.4c (D-i)/(P1) IVC↔Spartan binding-deferral disposition") + in verify body (binding-deferral discipline + three candidate mechanisms enumerated) + in struct field doc-comments. Per `.claude/rules/cryptography.md` (Gadget contract): the lifted helpers `build_honest_logup_witnesses` + `build_per_table_commitments` are the off-circuit reference for the M.GH7.4c synthetic-data construction; they live in production-shipped envelope code (NOT test scaffolding) so the wallet can derive the synthetic per-table data at envelope-build time under the (D-i)/(P1) disposition. The in-circuit half is the M.GH7.4a `prove_with_T_claim_split_error_with_logup` sibling (which the wallet's prover invokes via this M.GH7.4c envelope wire-up). The 1000-iter differential discipline is preserved by the M.GH7.0.2 envelope-binding differential (3/3 pass at 1000 iters under unconditional `_with_logup` rewiring). Sequencing: M.GH7.4c closes Phase 02. Phase 03 opens with M.GH7.5 (IVC↔Spartan binding-discharge mechanism specification + negative-test triple) — requires Halpert authoring per the sub-ratification's STOP-AND-ASK trigger #M.GH7.5.1 BEFORE crafter dispatch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…er-table fold propagation per Corrigendum microsoft#19 Wires post-fold per-table running commitments (comm_L, comm_ts) through the augmented circuit's verify_with_multi_table_lookup as untrusted hints, mirroring the existing comm_W_fold / comm_E_fold discipline at circuit/nifs.rs:46-55 / :649-664. Closes the IVC↔envelope binding by making the in-circuit Unew.comm_L_per_table[j] (absorbed at the final-step hash via M.GH7.5.0a's absorb_in_ro extension) byte-equal to the off-circuit r_U.comm_L[j] (absorbed at off-circuit RecursiveSNARK::verify via M.GH7.5.0a's absorb_in_ro2 extension). Changes: - Off-circuit NIFS<E> struct (src/neutron/nifs.rs): adds two new lookup-fold- gated hint fields, comm_L_fold_per_table and comm_ts_fold_per_table, each Option<Vec<Commitment<E>>>. Populated in prove_with_multi_table_lookup_inner by cloning U.comm_L / U.comm_ts from the off-circuit U1.fold_with_lookup output (the per-`j` independent fold body at relation.rs:862-884 per Corrigendum microsoft#6 primitive 3). Set to None on the non-multi-table prover paths (prove, prove_with_lookup, prove_with_multi_column_lookup) — those paths do not feed the augmented-circuit multi-table verifier. - In-circuit AllocatedLookupNIFSMultiTable (src/neutron/circuit/lookup.rs): adds Vec<AllocatedNonnativePoint<E>> fields comm_L_fold_per_table and comm_ts_fold_per_table; AllocatedLookupNIFSMultiTable::alloc allocates them from the per-step NIFS message's prover-supplied Vec hints (point-at-infinity default under shape-derivation `nifs == None`). - LookupVerifyOutputMultiTable (src/neutron/circuit/nifs.rs): widened to carry the per-table post-fold commitment hints. verify_with_multi_table_lookup clones the allocated hints from the AllocatedLookupNIFSMultiTable into the output — NO new constraint emission at this layer (pure passthrough); soundness via IVC hash-chain binding + envelope-side off-FS commitment- equality per Corrigendum microsoft#17 path (b). - from_lookup_fold_output (src/neutron/circuit/relation.rs): widened signature accepts comm_L_fold_per_table / comm_ts_fold_per_table Vec hints and OVERRIDES the M.GH7.5.0a passthrough of u_fold.comm_L_per_table / comm_ts_per_table. This is the load-bearing path α.2 wiring — without the override, Unew.comm_L_per_table[j] would carry PRE-fold (passthrough) values while r_U.comm_L[j] carries POST-fold values, and the IVC hash-chain check would reject the honest fold. - synthesize_non_base_case_lookup_fold (src/neutron/circuit/mod.rs): passes the new hint Vecs from lookup_output through to the widened from_lookup_fold_output. No prover-side wiring changes required — the data-flow is already in place via the NIFS message threading at prove_step_with_lookup_fold:976-988. - Acceptance tests (src/neutron/circuit/relation.rs stage0_byte_equivalence_tests): (a) Extends m_gh5_0_stage0_absorb_in_ro_byte_equivalence_at_fold_depth_1_and_2 with M.GH7.5.5 work-item 8 assertions: nifs1.comm_L_fold_per_table[j] and nifs2.comm_L_fold_per_table[j] MUST byte-equal folded_U_s1.comm_L[j] and folded_U_s2.comm_L[j] respectively (the hint-attachment locus sources from the POST-fold off-circuit U), plus the comm_ts variants plus a non-vacuity assertion that at least one entry is non-default (the k=2 multi-table fixture queries non-trivial table entries). (b) Adds m_gh7_5_0b_path_alpha2_from_lookup_fold_output_overrides_with_hint_vecs: directly synthesises from_lookup_fold_output with synthetic non-trivial hint Vecs distinct from the u_fold passthrough, then asserts (i) the result's comm_L_per_table x-limb-0 witness values match the HINTS (NOT the passthrough — falsifies a regression to M.GH7.5.0a behaviour); (ii) the in-circuit absorb_in_ro squeeze byte-equals the off-circuit absorb_in_ro2 squeeze on the same hint values. pp_digest baseline: test_pp_digest at lookup_fold_k = 0 is byte-identical (Vec-emptiness skip preserves the legacy R1CS-only shape); no expect refresh required since no production test_pp_digest fixture exercises lookup_fold_k > 0. Soundness anchors: parallel reasoning to vendor HEAD's existing comm_W_fold discipline (circuit/nifs.rs:46-55 / :649-664). The rejection mechanism for malicious post-fold per-table hints composes (i) IVC hash-chain divergence at the next step's Phase-1 hash check OR at the off-circuit RecursiveSNARK::verify hash reconstruction (M.GH7.5.0a-landed absorb extension + RO2 collision resistance per Nova 2021/370 v3 §4); (ii) envelope-side off-FS commitment- equality at CompressedSNARK::verify per Corrigendum microsoft#17 path (b), composed with Spartan-close Pedersen+LogUp identity binding (Haböck 2022/1530 §3 + Spartan 2019/550 §5). No new in-circuit constraint family is introduced; the Gadget contract from .claude/rules/cryptography.md is satisfied by parallel reasoning to the existing comm_W_fold discipline at vendor HEAD. Test scope: cargo test --release -p nova-snark --features lookup-fold (scoped): - test_pp_digest 1 passed - neutron::circuit::tests 1 passed - neutron::circuit::relation::stage0_byte_equivalence_tests 6 passed (5 pre-existing M.GH7.5.0a + 1 new M.GH7.5.0b consumer test) - neutron::circuit::nifs 1 passed - neutron::circuit::lookup::tests 4 passed - neutron::nifs::tests 17 passed - neutron::compressed_snark 10 passed - neutron::tests (incl. prove_step_with_lookup_fold IVC) 9 passed Refs: docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md Corrigendum microsoft#19 §"Revised implementation roadmap under path α.2" (work-items 1-9 discharged; STOP-AND-ASK trigger #M.GH7.5.5 byte-equivalence test explicitly authored at work-item 8). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…riment D-prime — diagnostic fixture for Obstruction 2 (n=1 hash-chain divergence locus); NOT a fix; PASSES as documented Obstruction 2 record Appends `m_gh7_5_obstruction2_experiment_d_prime_n1_hash_chain_divergence_locus` to `vendor/nova/src/neutron/compressed_snark.rs` at the test-module tail sibling to Experiments A and B. Mirrors the verifier-side hash-chain re-derive at `mod.rs:774-789` byte-for-byte AND a prover-equivalent reconstruction of the augmented circuit's base-case output-hash absorb sequence (`circuit/mod.rs:939-955` composed with `circuit/relation.rs: 502-570` on `default_with_lookup_k(cs, 1, k=1)` shape). Captures partial squeezes after each absorb step on both sides via fresh `PoseidonRO` re-absorb per prefix (since `PoseidonRO` is not `Clone`). Identifies the first divergence index and routes to D1/D2/D3/D4 per Corrigendum microsoft#24. Empirical close at vendor HEAD `b233301`: **D1 — (iv.γ) constant-shape- vs-Option-shape absorb-sequence drift at base case.** First divergence at prefix index 7, exactly at the `T_lookup` block: native verifier side skips (`r_U.T_lookup = None`), prover-equivalent side absorbs one zero scalar (mirroring `Unew_base.T_lookup_per_table = Some(vec![0; 1])` per `default_with_lookup_k`). Partials 0..=6 byte-equal across native and prover sides (`pp.digest`, `num_steps`/`i_new`, `z0`, `zi`/`z_next`, `comm_W`, `comm_E`, `T`). From index 7 onward streams diverge by one absorb-shift; final hash mismatch byte-for-byte matches the n=1 `Err(NovaError::ProofVerifyError { reason: "Invalid output hash in R1CS instance" })` reported by Experiment A. (iv.α) ruled OUT empirically: comm_W (idx=4) and comm_E (idx=5) partials byte-equal across native and prover sides — the `comm_E = comm_W.clone()` shared-variable circuit pattern does not produce an RO2-byte divergence against the native `Commitment::default()`-distinct-handle pattern at equal values. (iv.β) ruled OUT empirically: ri / r_next absorb (last position) is DOWNSTREAM of the (iv.γ) divergence — the divergence reaches that step already-corrupted by the (iv.γ) one-absorb-shift, so ri-allocation parity cannot be the root cause. Routes Corrigendum microsoft#25 to Fix-α: extend `FoldedInstance::default` to mirror constant-shape allocation under `lookup_fold_k > 0` (the strictly-more-general fix that closes the asymmetry without breaking Corrigendum microsoft#6's constant-shape FS-schedule discipline). Test asserts the divergence EXISTS (preferred pattern from Corrigendum microsoft#24 dispatch): PASSES at vendor HEAD `b233301` as a documented record of Obstruction 2's n=1 hash-chain divergence locus. If a future Corrigendum microsoft#25 fix-α lands and the divergence disappears, this fixture FAILS to signal that the obstruction has been resolved — at which point the fixture should be promoted into a positive single-step n=1 acceptance test (Corrigendum microsoft#23 layer 5b deferred deliverable). Read-only against vendor body: no modification to `RecursiveSNARK:: verify`, `FoldedInstance::default`, `AllocatedFoldedInstance::default`, `absorb_in_ro2`, or `absorb_in_ro`. Pure additive test fixture. Test invocation (release-mode mandatory per `.claude/rules/testing.md`): cargo test --release -p nova-snark --features lookup-fold --lib \ neutron::compressed_snark::tests::\ m_gh7_5_obstruction2_experiment_d_prime_n1_hash_chain_divergence_locus \ -- --nocapture Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Add a new error,
InputOutputMismatchfor the case in which the current input and previous output do not match, when folding instances.