generic traits for prime field elements and group elements#1
Merged
Merged
Conversation
and cleanup some group op traits
|
|
huitseeker
referenced
this pull request
in huitseeker/Nova
Jun 16, 2023
Refactor: needless clones of RecursiveSnark inputs
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 9, 2026
… per Corrigenda microsoft#2/microsoft#3/microsoft#4/microsoft#4-A Closes M.GH5.0 STAGE 0 hard gate per the GH-microsoft#5 design pin's Halpert ratification chain (Corrigenda microsoft#1 → microsoft#4-A) following Marcus's correctness-over-minimalism mandate (Core Principle 7, codified at `5e5e951`). ## Ratification chain The path from STAGE 0 first-attempt failure to close walked through five cryptographer rulings, each correcting a prior over-narrowing or implementation gap: - **Corrigendum microsoft#1** (2026-05-09): X-arity invariant `num_io == 1` + alloc fail-close. Closed the original STAGE 0 byte-disagreement at `num_io == 2` (DirectCircuit fixture). Empirically valid; ratified Path-X re-shape. (RETIRED by microsoft#2 under Principle 7.) - **Corrigendum microsoft#2** (2026-05-09): Path W. Extends `AllocatedFoldedInstance::X` from `AllocatedNum` to `Vec<AllocatedNum>` mirroring native. Retires the `num_io == 1` invariant on simplicity grounds (Principle 7 forbids simplicity-based rejection of more-general options). The 4 pre-existing M.6 / Stage G / Stage I.pri lookup-circuit tests are routed to STAY at single-IO via `MinimalSingleIOCircuit`. - **Corrigendum microsoft#3** (2026-05-09): γ.1 fold-arity invariant. `AllocatedFoldedInstance::fold` is N==1-only because U2 (`AllocatedNonnativeR1CSInstance`) is structurally single-IO per §1.6 anchor. Path W's Vec-shape applies to absorb_in_ro / select / alloc; fold fail-closes at N≥2 with twin-substring error message. - **Corrigendum microsoft#4** (2026-05-09): Path Y. Restores upstream microsoft/Nova's `let X = T.clone()` pattern in `default(cs, num_io)` and `default_with_lookup_k(cs, num_io, k)` X allocation. Path W's `AllocatedNum::alloc(... || Ok(ZERO))` lost the `(0)·(0) = T` binding constraint (`alloc_zero` emits the row; `T.clone()` shares the variable, inheriting the binding). Without this restoration, a malicious base-case prover could populate the unconstrained aux variable with any value — `.claude/rules/cryptography.md`'s "missing constraint is a forgery vector". - **Corrigendum microsoft#4-A** (2026-05-09): negative-test shape adaptation under Path Y's variable-aliasing semantics. Path W's malicious-X[0] test shape is structurally meaningless under Path Y because X[i] IS T (variable-aliased via T.clone()). Setting X[0]=N≠0 would require T=N≠0, which `alloc_zero` rejects directly. The negative test adapts to a structural-binding test asserting variable-identity (X[i].get_variable() == T.get_variable()) plus constraint-count floor plus positive is_satisfied — catches the only regression class capable of re-opening the forgery vector. ## Implementation surface (this commit) `vendor/nova/src/neutron/circuit/relation.rs`: - `AllocatedFoldedInstance::X`: `AllocatedNum<E::Scalar>` → `Vec<AllocatedNum<E::Scalar>>` (Path W). - `alloc(cs, inst)`: per-element from `inst.X.iter()` for `Some`; length-1 Vec of `AllocatedNum::alloc(... || Ok(ZERO))?` for `None` (alloc-None length-1 fix; restores byte-equivalence with prior single-AllocatedNum at outer base). - `default(cs, num_io)`: NEW signature with `num_io: usize` parameter. Body uses `T.clone()` per Path Y / Corrigendum microsoft#4 to share T's `alloc_zero`-bound variable into every X[i]. - `default_with_lookup_k(cs, num_io, k)`: same pattern. - `absorb_in_ro`: per-element X loop matching native `for x in &self.X { ro.absorb(x) }`. - `fold`: γ.1 fail-close at top of body returns `SynthesisError::Unsatisfiable("...self.X.len() != 1...§1.6...")` on `self.X.len() != 1`. Existing single-scalar fold algebra preserved at N==1, wrapped as length-1 Vec. - `conditionally_select`: per-element matched-shape select with length-mismatch fail-close. - STAGE 0 test module: 0a (NeutronAugmentedCircuit num_io==1 byte-equivalence — preserved); 0b (NEW direct-fixture num_io==2 byte-equivalence — Path W validation at non-trivial X-arity, exercises only absorb_in_ro); 0c (NEW γ.1 fold-arity fail-close negative test with twin-substring assertion); plus the NEW Path Y structural-binding test (`m_gh5_0_path_y_x_t_aliasing_binding`) asserting X[i].get_variable() == T.get_variable() across 5 cases × 3 engines = 15 invocations. Removed the Corrigendum-microsoft#1-era `m_gh5_0_alloc_rejects_x_arity_two` negative test (alloc no longer fail-closes on X.len() != 1). `vendor/nova/src/neutron/circuit/mod.rs`: - Single in-vendor call site of `AllocatedFoldedInstance::default` updated to pass `num_io: 1` per the augmented-circuit's structural invariant (`hash.inputize` once at line 431). `vendor/nova/src/neutron/circuit/lookup.rs`: - `MinimalSingleIOCircuit` introduced (test-only) to give the 4 pre-existing lookup-circuit tests a `num_io == 1` shape. Per Corrigendum microsoft#3 these tests STAY at single-IO; the `arity ≤ 1` workaround comment at the FS-replay site is now codified as the fold-arity invariant. - Tests re-shaped: `m6_in_circuit_per_table_c_binding_hard_rejects_corrupted_t_lookup`, `m6_in_circuit_verify_multi_table_matches_native_k2`, `stage_g_in_circuit_verify_with_lookup_matches_native`, `stage_i_pri_in_circuit_verify_multi_column_matches_native`. ## Test posture `cargo test --release --features lookup-fold -p nova-snark`: - **146 passed, 4 failed, 3 ignored** in 157.15s - 4 failures: all Cluster A (`MinimalSingleIOCircuit` + hyperkzg CK sizing mismatch — `assertion failed: ck.ck.len() >= v.len()`). Separate M.GH5.0b scope per Halpert's triage. `cargo check --tests --features lookup-fold`: clean. ## What this commit does NOT include - Cluster A fix (CK-floor sizing in the 4 lookup-circuit tests' fixtures). M.GH5.0b dispatch covers it. - UPDATE_EXPECT on `pp_digest` literals. The literals at `vendor/nova/src/neutron/mod.rs:553/558/563` already coincide with the post-Path-Y digest (LookupShape envelope refresh at `048ac29` happens to align with Path Y's clone-of-T shape). No refresh needed. ## Audit-trail Five Halpert dispatches across Corrigenda microsoft#1 → microsoft#4-A. Each ruling documented in pin §1.4 with original text preserved per override discipline. Path-W → Path-Y refinement chain demonstrates Core Principle 7 in action: simplicity arguments rejected at every step where a more-general or more-soundness-bearing option was available. Reviewed by `@nw-cryptographer` (Halpert) per the GH-microsoft#5 per-step pre-commit review pattern (5 dispatches, 5 ratifications). 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
…l≥2 fixture fixes Closes the 4 lookup-circuit test failures that were the only remaining Cluster A residue after M.GH5.0 (Path W + γ.1 + Path Y) closed at `fc0de8e`. Two structurally-distinct fixture fixes, applied together because they share a single fixture file and were exposed by the same M.GH5.0a-fix-up regression chain: ## M.GH5.0b — CK-floor sizing fix Per Halpert's third-dispatch Cluster A diagnosis: the M.GH5.0a fix-up re-shaped the 4 affected tests to use `MinimalSingleIOCircuit` (`num_cons=0`, `num_vars=1`, `num_io=1`), but kept the upstream CK construction `R1CSShape::commitment_key(&[&shape], &[&*S::ck_floor()])` which gives `max(0, 1, 0) = 1`. The tests then commit lookup tables of size 16, panicking at `hyperkzg.rs:567` with `assertion failed: ck.ck.len() >= v.len()`. Fix: replace the CK construction with explicit `setup` at size 16: ```rust let ck = <E as Engine>::CE::setup(b"lookup_test", 16).expect(...); ``` Applied uniformly across: - `m6_in_circuit_per_table_c_binding_hard_rejects_corrupted_t_lookup` - `m6_in_circuit_verify_multi_table_matches_native_k2` - `stage_g_in_circuit_verify_with_lookup_matches_native` - `stage_i_pri_in_circuit_verify_multi_column_matches_native` ## M.GH5.0c — `ell >= 2` α-fixture enrichment per Corrigendum microsoft#5 After M.GH5.0b unblocked the CK panic, the same 4 tests panicked at a STRUCTURALLY DISTINCT site: `vendor/nova/src/spartan/polys/power.rs:67` (`self.t_pow[0]` on empty Vec) reached via `nifs.rs:646` (`PowPolynomial::new(&tau, S.ell).split_evals(S.left, S.right)`). Root cause: `S.ell = num_cons.next_power_of_two().log_2()` per `relation.rs:492`. With `MinimalSingleIOCircuit`'s `num_cons == 0`, `ell == 0`, `t_pow.len() == 0`, indexing panics. The R1CS-side eq machinery requires `ell >= 2` to be panic-safe (at `ell == 1`, `right[1]` indexes a length-1 Vec; verified by reading `power.rs:62-86`). Halpert's fourth-dispatch ruling (Corrigendum microsoft#5, just landed in pin §1.4): `num_cons == 0` was INCIDENTAL to M.GH5.0a's narrowing, NOT pin-load-bearing. The pin's binding invariants on the fixture are `num_io == 1` (§1.6 anchor + Corrigendum microsoft#3 fold-arity) and `default()` body's variable-aliasing (Corrigendum microsoft#4 / microsoft#4-A) — neither is touched by enriching `num_cons`. Fix: emit ≥3 enforced constraints (`0 * 0 == 0` triples on freshly- allocated zero witnesses) so `next_power_of_two(num_cons) == 4` and `ell == 2`. Constraints are content-irrelevant — they exist only to size the R1CS hypercube. The fixture remains single-IO and trivially satisfiable across both `ShapeCS` (shape extraction) and `SatisfyingAssignment` (witness materialisation). Applied 4 dummy constraints (`z_0 == 0` through `z_3 == 0`) in `MinimalSingleIOCircuit::synthesize`. Each of the 4 affected tests now asserts both `shape.num_io == 1` AND `shape.num_cons >= 3` adjacent, with twin-substring `"ell >= 2"` AND `"Corrigendum microsoft#5"` per pin §3.5 discipline. ## Why these are fixture-side fixes, not soundness-class Halpert's third-dispatch Cluster A diagnosis: "The lookup verifier's algebra is unchanged; the tests cannot reach the algebra under their current fixture because the CK construction panics before any prove/verify runs. No constraint family is silently mis-shaped; nothing has been elevated to a different soundness reduction." Same applies to M.GH5.0c — `ell == 0` is a structural-shape underflow, not a constraint-system soundness gap. The pin's algebraic content (§1.4 absorption order, §1.5 soundness reduction, §1.6 single-IO anchor) is unchanged. Only the fixture's under-narrowing is corrected. ## Test posture `cargo test --release --features lookup-fold -p nova-snark`: - **150 passed, 0 failed, 3 ignored** in 88.51s. - All previously-failing Cluster A tests GREEN. - All M.GH5.0 STAGE 0 tests (0a/0b/0c + binding) still GREEN. - All `test_pp_digest` (3 engines) still GREEN — `TrivialCircuit`- shaped, not affected by `MinimalSingleIOCircuit` enrichment. - All IVC and recursive-circuit tests still GREEN. `cargo check --tests --features lookup-fold`: clean. `UPDATE_EXPECT=1` not needed — `test_pp_digest` baselines unchanged because the test uses `TrivialCircuit::default()`, not `MinimalSingleIOCircuit`. Halpert's hedged prediction ("likely needs refresh") was correctly cautious; the actual outcome is cleaner. ## Audit-trail - M.GH5.0a fix-up (uncommitted in working tree until this commit) re-shaped 4 tests to `MinimalSingleIOCircuit` per Corrigendum microsoft#1's `num_io == 1` invariant. - M.GH5.0b dispatch identified the CK-floor regression that the M.GH5.0a fix-up surfaced. - Halpert's fourth dispatch authored Corrigendum microsoft#5 ratifying α-fixture enrichment with `ell >= 2` precondition stated. - This commit lands both fixes together (M.GH5.0b CK + M.GH5.0c α-enrichment) plus the M.GH5.0a `MinimalSingleIOCircuit` introduction itself, since all three are scoped to the same fixture file and form a single coherent regression-fix unit. Reviewed by `@nw-cryptographer` (Halpert) per the GH-microsoft#5 per-step pre-commit review pattern (third-dispatch Cluster A diagnosis + fourth-dispatch Corrigendum microsoft#5 ratification). 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
…hape differential — Corrigendum microsoft#9 Per Pin Corrigendum microsoft#9 (2026-05-10) §5.5 row M.GH5.5 (re-scoped from RecursiveSNARK-IVC to direct-NIFS pattern after the 2026-05-10 dispatch verified that `RecursiveSNARK::prove_step` calls `NIFS::prove` not `prove_with_multi_table_lookup`, AND `with_multi_table_bundles` has zero callers, AND `chunk_index_in_z = U.X[0]` conflicts with standard IVC output-hash binding-via-hash semantics — the chunk_index_in_z routing question carries forward to GH-microsoft#7 / Stage K). This milestone delivers the FIRST end-to-end exercise of the augmented- circuit lookup-fold path at fold-depth ≥ 4 with multi-table k=2 absent- table coverage. M.GH5.0 STAGE 0 was 2-step; M.11 was 4-step but native- only (no augmented-circuit synthesis); M.GH5.5 combines them. ## What this commit adds Single new vendor-internal test at `vendor/nova/src/neutron/circuit/relation.rs::stage0_byte_equivalence_tests::m_gh5_5_fold_of_n_augmented_circuit_shape_differential` (lines 1785-2241; +535 lines into the existing module). The test drives 4 fold steps via direct `NIFS::prove_with_multi_table_lookup` + `verify_with_multi_table_lookup` (M.11 + M.GH5.0 STAGE 0 pattern), with k=2 multi-table absent-table shape (T_2 absent at steps 1 and 4, queried at steps 2 and 3 — M.11 §D.1). The R1CS shape comes from `NeutronAugmentedCircuit` so `num_io == 1` (production-shape invariant per pin §1.6 anchor). At each fold step ≥ 1 the test asserts: - (a) `cs.is_satisfied() == true` on in-circuit `absorb_in_ro` synthesis. - (b) `T_lookup_per_table` is `Some(&[..])` of length k=2 with at least one non-zero entry (empirically validates that the (W1) binding-via- hash extension is being exercised — not the trivial all-zero case). - (c) byte-equivalent native ↔ in-circuit hash output (the §1.4 absorption-order invariant survives at fold-depth ≥ 4). Plus a defensive cross-step audit assertion that T_1's running scalar visibly evolves across consecutive fold steps (T_1 is queried at every step with random per-step indices; all-equal T_1 across 4 steps would indicate the (W1) running-scalar pipeline silently dropped state). ## Discharges per pin §5.3 microsoft#1 - (W1) binding-via-hash extension: T_lookup_per_table absorption in `U.absorb_in_ro` AT fold-depth ≥ 1 with non-zero entries — assertion (b) at every step + assertion (c) ensures the per-table running scalar participates in the hash that becomes `u.X[0]`. - (W2) cross-table absorption order: T_lookup_per_table absorbed in `table_id`-canonical order; mismatched ordering between native `FoldedInstance::absorb_in_ro2` and in-circuit `AllocatedFoldedInstance::absorb_in_ro` would falsify (c) at the first fold step. - (W3) fold-depth ≥ 1 propagation: 4 sequential fold steps, with the running U from step n+1 carrying the cumulative T_lookup from steps ≤ n; the cross-step audit assertion confirms running-scalar evolution. ## Why this lives in the vendor (not in inumbra-spend-harness) The dispatch's "no vendor edits expected" expectation was unverified. Verify-don't-assume on the vendor public-API surface: - `mod circuit;` at `vendor/nova/src/neutron/mod.rs:25` is private (no `pub` modifier). `AllocatedFoldedInstance`, `circuit_absorb_squeeze`, `native_absorb_squeeze`, `NeutronAugmentedCircuit`, and `NeutronAugmentedCircuitInputs` are all vendor-internal. - `pub use` re-exports of `AllocatedFoldedInstance` are absent (verified via Grep across `vendor/nova/src/`). - The byte-equivalence assertion REQUIRES augmented-circuit synthesis through `AllocatedFoldedInstance` mirroring + `RO2Circuit` squeeze, which is structurally vendor-internal. The Halpert-authored M.11 file header established the precedent (Finding 1 ruling §1.4) of deferring vendor visibility bumps until consumers exist. The natural sequencing for M.GH5.5 — augmented-circuit- shape byte-equivalence at fold-depth ≥ 4 — is to extend the vendor- internal STAGE 0 fixture (which already has the helpers and the 2-step template) rather than introduce a new vendor public-API visibility surface that has no consumer outside this single test. ## Empirical signals - All four fold steps GREEN at first run; assertions (a), (b), (c) hold at every step. - T_lookup_per_table is non-zero at every fold-depth ≥ 1 (T_1's running scalar accumulates because T_1 is queried at every step with random per-step indices; T_2's running scalar accumulates from the n_j / r_logup_j contribution even on the absent-shape side). - Native ↔ in-circuit hash output byte-equivalent at every fold step (the §1.4 absorption-order pin survives at fold-depth ≥ 4). - Cross-step audit: T_1's running scalar visibly evolves across consecutive fold steps. ## Test results - New test: `cargo test --release --features lookup-fold --lib m_gh5_5_fold_of_n_augmented_circuit_shape_differential` → 1 passed, 0 failed. - Vendor `--release --features lookup-fold` baseline: 152/0/7 → 153/0/7 (+1 from this test). - inumbra-spend-circuits `--release --lib`: 87/0/9 (preserved). - inumbra-spend-harness `--release`: 13/0 (preserved; M.GH5.5 lives in vendor, not harness). ## Out of scope (per Corrigendum microsoft#9) - `RecursiveSNARK::prove_step` IVC integration (carry-forward to GH-microsoft#7). - chunk_index_in_z routing resolution (carry-forward to GH-microsoft#7 / Stage K). - Off-circuit running-scalar reference differential (M.GH5.6). - Negative-test discharge (M.GH5.7 / M.GH5.8). - Inumbra-side `pp_digest` baseline refresh (wrap pipeline isn't migrating).
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
… prove_step_with_lookup_fold sibling (positive-path; Corrigendum microsoft#14 + sub-ratifications microsoft#1+microsoft#2) Corrigendum microsoft#14 re-typed disposition (option β sibling method) for the M.GH7.3 trait + sibling-method + RecursiveSNARK field surface, refined by 2026-05-12 sub-ratification microsoft#1 (dropped decorative `r_logup_per_table` argument from trait method per r-independence audit at nifs.rs:202-227 + lookup_sumcheck.rs:146-221) and sub-ratification microsoft#2 (extended `PublicParams::setup` signature with `Option<LookupShape<E>>` parameter prerequisite + `running_lws` field on `RecursiveSNARK`). Positive-path implementation only; negative-test triple deferred to M.GH7.3b per the 2026-05-12 Option α split (Halpert-authoring pending). Vendor-side authoring: - `PublicParams::setup` + `setup_with_ptau_dir` (mod.rs:240-296, :360-418): extended `#[cfg(feature = "lookup-fold")]` variants with trailing `lookup_shape: Option<LookupShape<E1>>` parameter; body match-branch `Some → Structure::new_with_lookups(&r1cs_shape, shape)` vs `None → Structure::new(&r1cs_shape)`. Cascade: 6 vendor-internal callsites in mod.rs test module (test_pp_digest_with × 1, test_ivc_* × 3, test_setup × 2) supply `None`; 2 callsites in compressed_snark.rs STAGE 0 (HyperKZG + IPA-PC trivial-circuit) supply `None`. Non-lookup-fold cfg variants UNCHANGED. - `RecursiveSNARK::running_lws: Vec<LookupRunningWitness<E1>>` field (mod.rs:484-533): added under `#[cfg(feature = "lookup-fold")]`, bootstrap at `RecursiveSNARK::new` from `LookupRunningWitness::default(&shape)` per registered `multi_column_tables[j]` when `pp.lookup_fold_k > 0`; `vec![]` otherwise. `LookupRunningWitness<E>` is `Serialize, Deserialize` per relation.rs:409, so the existing `#[derive(Serialize, Deserialize)]` on `RecursiveSNARK` typechecks unchanged (sub-ratification microsoft#2 STOP-AND-ASK gate microsoft#3 clean). - `LookupStepCircuit<E: Engine>: StepCircuit<E::Scalar>` trait (mod.rs:838-913): two methods, NO `r_logup_per_table` argument per sub-ratification microsoft#1 (gate microsoft#1 dissolved by the r-independence audit). `per_table_bundles_at_step(&self, ck, i, prior_running_lws) -> Result< Vec<PerTableBundle<E>>, NovaError>` constructs fully-committed prover-side per-table bundles in `table_id`-canonical order; `public_bundles(bundles) -> Vec<LookupPayloadPublicMultiTable<E>>` projects to verifier-public hints. Trait dispatch accepts associated function without `&self` parameter — fallback free-function `public_bundles_of<E: Engine>(...)` not needed at M.GH7.3a (gate microsoft#4 clean). - `RecursiveSNARK::prove_step_with_lookup_fold` sibling method (mod.rs:914-1013): separate `#[cfg(feature = "lookup-fold")] impl<E1, E2, C> ... where C: StepCircuit + LookupStepCircuit<E1>` block, structurally parallel to the existing `impl ... where C: StepCircuit` block at line 514. Body per pin §5.5 row M.GH7.3a + sub-ratification microsoft#1: bootstrap at i=0 mirrors `prove_step:580-583` byte-identically; otherwise (i) construct bundles via `c.per_table_bundles_at_step(&pp.ck, self.i, &self.running_lws)`; (ii) invoke `NIFS::prove_with_multi_table_lookup` with the 9-arg public wrapper at nifs.rs:1301-1316; (iii) project bundles via `C::public_bundles(&bundles)`; (iv) build `NeutronAugmentedCircuitInputs` byte-identical to `prove_step:599-624` with `.with_multi_table_bundles(Some(public_bundles))`; (v) synthesise augmented circuit byte-identical to `prove_step:615-624` with same `with_lookup_fold` threading; (vi) update `self.{r_U, r_W, l_u, l_w, zi, ri, running_lws, i}`. Existing `prove_step` at mod.rs:578-637 is UNCHANGED (preserves vendor upstream-tracking + classical-Nova consumers + STAGE 0 non-lookup path per Corrigendum microsoft#13). Acceptance test (mod.rs `#[cfg(test)] mod tests`): `m_gh7_3a_prove_step_with_lookup_fold_sibling_threads_running_lws_witness_alloc_preserved_positive_path` — N=3 honest sibling-method invocations (bootstrap + 2 real folds) against a trivial `LookupStepCircuit` fixture mirroring the M.11 §D.1 absent-table pattern at vendor-test-fixture scope (does NOT depend on inumbra-side `build_canonical_lookup_shape` per gate microsoft#2 / STOP-AND-ASK microsoft#2 clean — the fixture inlines the absent-bundle constructor from m11_fold_of_four_absent_table_differential.rs:466-525). Assertions: 1. `prove_step_with_lookup_fold` returns Ok for each of 3 invocations. 2. `r_U.T_lookup` accumulates from `None` (outer base) to `Some(Vec)` of length K after fold microsoft#1, preserved after fold microsoft#2 (§1.2 algebra). 3. **Byte-equal threading**: at fold microsoft#2's `per_table_bundles_at_step`, the observed `prior_running_lws` is byte-equal to fold microsoft#1's `next_running_lws` output — the load-bearing `self.running_lws = next_running_lws;` field-mutation contract. 4. `prove_step` (non-lookup) regression invariant clean — captured by the `test_pp_digest` + `test_ivc_*` + `test_setup` tests continuing to pass byte-identically (verified at this commit). STOP-AND-ASK verdict (PREPARE-level, per pin §5.5 row M.GH7.3a): - Gate microsoft#1 (`pp_digest` byte-divergence at `lookup_fold_k = 0` + `lookup_shape = None`): **CLEAN**. `test_pp_digest_with` at mod.rs:830, :834, :838 pass unchanged with `None` appended. - Gate microsoft#2 (vendor-test fixture cannot construct minimal `LookupShape<E>`): **CLEAN**. The fixture inlines a one-off absent-bundle constructor at vendor-test-fixture scope (single-column-degenerate path: `multi_column_tables[0].columns = vec![]`, `payload.comm_values = vec![]` per nifs.rs:1404-1411 bundle-validation). - Gate microsoft#3 (`running_lws` field surfaces serialisation incompatibility): **CLEAN**. `LookupRunningWitness<E>` is `Serialize, Deserialize` per relation.rs:409; existing `#[derive(Serialize, Deserialize)]` on `RecursiveSNARK` typechecks unchanged. - Gate microsoft#4 (`LookupStepCircuit::public_bundles` ergonomic issues): **CLEAN**. Rust trait dispatch accepts the associated function without `&self` parameter — fallback to free-function lift not needed. - Gate microsoft#5 (production-shape `LookupStepCircuit` impl complication): N/A at M.GH7.3a (deferred to M.GH7.5a wrap-pipeline retarget). Vendor-test verdict (release-mode per `.claude/rules/testing.md`): - `cargo test --release -p nova-snark --features lookup-fold --lib neutron::tests`: 6 passed; 0 failed; 0 ignored — includes `test_pp_digest` (3 expect-tests at mod.rs:830-841), `test_ivc_trivial`, `test_ivc_base`, `test_ivc_nontrivial_neutron`, `test_setup`, AND `m_gh7_3a_*` acceptance test. Inumbra-side cascade (one-line cosmetic, supplied at superproject pointer-bump commit): `tests/gh7_stage_k_compressor.rs:149, :270` get trailing `None,` appended (STAGE 0 stays on non-lookup `prove_step` path per Corrigendum microsoft#13; the `Some(build_canonical_lookup_shape::<...>)` flip lands at M.GH7.5a per Corrigendum microsoft#5). Discharges AO 19 PARTIALLY (positive-path routing; full discharge at M.GH7.3b negative-test triple, cryptographer-authoring-pending). Negative-test triple deferred to M.GH7.3b per 2026-05-12 Option α split. See pin §5.5 row M.GH7.3a + §3.1 + Corrigendum microsoft#14 + sub-ratifications microsoft#1 + microsoft#2 in §0; roadmap step 02-02a. 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
…logup sumcheck engine + prove_with_T_claim_split_error_with_logup Spartan sibling (per Corrigendum microsoft#16; AO 23 discharge positive-path) Authors the M.GH7.4 subdivision's first sub-milestone (M.GH7.4a per Corrigendum microsoft#16 §5.5 row split). Two new vendor-side methods, both siblings to the existing β' / neutron-form Spartan-close machinery (preserves M.GH7.0.0b STAGE-0 byte-equivalence verbatim by leaving the existing methods unchanged): 1. `SumcheckProof::prove_neutron_outer_with_logup` at `src/spartan/sumcheck.rs` — new sumcheck-engine sibling. Extends the existing `prove_neutron_outer` with per-table LogUp (A)+(B) residue bodies composed additively under per-table `r_logup_j` per Corrigendum microsoft#16 Finding B (no gamma-RLC; matches the vendor NIFS-side parallel-univariate discipline at `nifs.rs:1497-1638`). Per-round univariate is degree-3 under additive composition per Finding C (verified empirically — see (3) below). `bind_poly_var_top` per Corrigendum microsoft#9 (2-A) preserved for ALL polynomials (R1CS-side AND per-table). Returns the new `PerTableOuterEvals<F>` struct carrying the seven per-table polynomial values at `r_x` for M.GH7.4b PCS-opening wiring. 2. `RelaxedR1CSSNARK::prove_with_T_claim_split_error_with_logup` at `src/spartan/snark.rs` — new Spartan-close sibling. FS-transcript discipline byte-identical to β' (Corrigendum microsoft#10 Primitive 5: absorb vk → U → T_claim before any squeeze); per-table `r_logup_j` are scalar inputs, NOT transcript squeezes, preserving Corrigendum microsoft#11 envelope-Spartan FS isolation. Inner sumcheck + batch-eval-reduce UNCHANGED from β' per Corrigendum microsoft#16 — per-table PCS-opening lands at M.GH7.4b. Returns `(Self, Vec<PerTableOuterEvals>)` exposing the per-table evals for downstream M.GH7.4b wiring. STOP-AND-ASK gates (Corrigendum microsoft#16 §5.5 row M.GH7.4a) — NONE RAISED: Gate microsoft#1 (sibling vs extend-in-place): SIBLING. Both new methods are authored alongside the existing β' / prove_neutron_outer paths verbatim; M.GH7.0.0b STAGE-0 byte-equivalence guaranteed by construction. Gate microsoft#2 (degree-3 empirical close): PASSED. Finding C's algebra-level disposition (eq-factor weighting IS the deg-1 contribution; (A)+(B) bodies are deg-3 under additive composition) is empirically confirmed by `m_gh7_4a_prove_neutron_outer_with_logup_degree_3_additive_composition_closes_correctly` — 1000 iterations × 2 engines (Bn256EngineKZG + PallasEngine) on seed `0xC1BE_5BAD_C0DE_704A`, falsifier-shape "4-eval-point degree-3 reconstruction at {0,1,∞,−1} must equal direct closed-form at t=2". The unified body under additive composition is exactly degree-3; no escalation to degree-4 needed; 4 eval points suffice. Gate microsoft#3 (per-table outer-sumcheck variable partition / Finding F): RESOLVED via flat embedding. Per-table polynomials and per-table eq-factors are pre-flattened onto the R1CS variable space at length `num_cons = left * right` by the caller (envelope-side at M.GH7.4c). `bind_poly_var_top` applies uniformly across R1CS-side and per-table polys. Corrigendum microsoft#9 (2-A) `r_x_high`/`r_x_low` partition preserved verbatim — per-table polys are additive residue terms, not factors of `full_E`, so they do NOT interact with the E1/E2 factorisation. Test coverage: - `m_gh7_4a_prove_with_T_claim_split_error_with_logup_round_trip`: HONEST-LogUp round-trip at fixture `num_cons=4, k=2`, seed `0xC1BE_5BAD_C0DE_704A`. Constructs per-table witnesses with `inv_w_j[i] = 1/(w_j[i] + r_logup_j)` and `inv_t_j[i] = ts_j[i]/(T_j[i] + r_logup_j)` (Haböck eprint 2022/1530 §3); per-table eq-factors via `PowPolynomial::new(tau, ell).evals()` (non-degenerate per Halpert sub-ratification 2026-05-12 late evening). Asserts (i) prover succeeds, (ii) `per_table_outer_evals.len() == k`, (iii) β' sibling regression: `prove_with_T_claim_split_error` continues to round-trip via verify byte-identically at the same fixture shape. - `m_gh7_4a_prove_neutron_outer_with_logup_degree_3_additive_composition_closes_correctly`: the empirical degree-3 close above (gate microsoft#2 discharge). - `m_gh7_4a_per_table_outer_evals_struct_field_shape`: structural sanity on `PerTableOuterEvals<F>` field shape — guards against accidental field rotation when M.GH7.4b extends `Self` with per-table commitment carry. Regression invariants preserved (release-mode `cargo test --release --features lookup-fold --lib <test_name>` per `.claude/rules/testing.md`): - M.GH7.0.5 STAGE 0: `test_pp_digest` (1/1 ok), `test_ivc_base` + `test_ivc_trivial` + `test_ivc_nontrivial_neutron` (3/3 ok), `test_setup` (1/1 ok). Hard-gate pass cardinality 10/10 STANDS. - M.GH7.0.0b: `m_gh7_0_0b_prove_with_T_claim_split_error_neutron_form_round_trip_byte_equal`, `m_gh7_0_0b_weighting_differential_1000_iter`, `m_gh7_0_0b_negative_T_corruption_rejected` (3/3 ok). - M.GH7.3a: `m_gh7_3a_prove_step_with_lookup_fold_sibling_threads_running_lws_witness_alloc_preserved_positive_path` (1/1 ok). - M.GH7.3b: `prove_step_with_lookup_fold_corrupt_t_at_index_in_consumed_u1_rejects_at_r1cs_c_binding`, `prove_step_with_lookup_fold_post_prove_mutate_poly_lookup_via_nifs_rebuild_rejects_at_lookup_c_binding`, `prove_step_with_lookup_fold_corrupt_t_lookup_at_index_in_consumed_u1_rejects_at_lookup_c_binding` (3/3 ok). LOC: ~+540 sumcheck.rs (sumcheck-engine sibling + `PerTableOuterEvals` struct); ~+820 snark.rs (Spartan-close sibling + M.GH7.4a test module + `pub(super)` visibility on two M.GH7.0.0b test helpers for sibling-module reuse). The crafter-side line target was ~+300 LOC across both files; actual is larger because the sumcheck-engine sibling does NOT abstract the R1CS-side body (it's inlined verbatim from `prove_neutron_outer` to keep the additive composition's per-round eval-point arithmetic literal and audit-readable — extraction to a shared helper is deferred to M.GH7.4b/c's final consolidation if a shared shape emerges). Discharges AO 23 (unified outer-sumcheck claim batches R1CS + per-table LogUp identities via additive composition under per-table `r_logup_j`). Positive-path only per Corrigendum microsoft#16 §5.5 row M.GH7.4a; corrupt- multiplicities negative-test lands at M.GH7.5 per AO 24. Refs: docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md Corrigendum microsoft#16 (M.GH7.4 subdivision into M.GH7.4a/b/c) §1.2, §2.2 Phase 4/5, §5.5 row M.GH7.4a, §6.1 row M.GH7.4a, §6.3 AO 23 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.
and cleanup some group op traits