Make traits public.#3
Closed
porcuquine wants to merge 1 commit into
Closed
Conversation
Contributor
Author
|
Aha, you fixed this while I was working. Thanks. |
asn-d6
pushed a commit
to asn-d6/Nova
that referenced
this pull request
Apr 23, 2023
…o/feature/construct_parallel_tree Add parallel prover with tree construction
huitseeker
pushed a commit
to huitseeker/Nova
that referenced
this pull request
Aug 19, 2023
* Rename r1cs_shape_with_commitmentkey to r1cs_shape_and_key. * Remove supernova feature. * Replace commitmentkey with commitment_key. * Replace publicparams with public_params. * Clippy * Fix constraint counts in supernova test. --------- Co-authored-by: porcuquine <porcuquine@users.noreply.github.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 8, 2026
… (pin §5.2 microsoft#3) Extends `lookup_sumcheck.rs:1106` (`prove_step_differential_against_naive`) per-table for the multi-table prove path. For each table j ∈ [0..k): 1. Drives `prove_with_multi_table_lookup_inner` with a pinned `r_E` 2. Re-derives `rho` and per-table `r_logup_j` by mirroring the FS schedule (steps 0/2/3/4/5a/5b) from `nifs.rs:1418-1467` 3. Computes the off-circuit (A)+(B)+(C) naive sub-claim summation at 10 fresh `Scalar::random` points using the bf linear-blend `(1-p)·v_running + p·v_fresh` 4. Asserts equality against `nifs.poly_lookup[j].evaluate(&p)` The (A)+(B)+(C) algebra is lifted verbatim from `lookup_sumcheck.rs:1141-1191` and indexed by table j; the pin §6 microsoft#4 falsifier is a soundness-class halt ("this should never fire because the extension is structural-only"). Three sibling tests cover the pin-mandated breadth: - `m12_lagrange_manual_check_k1_regression` (n=64, seed `0xC1BE_1A6E`) - `m12_lagrange_manual_check_k2_heterogeneous` (n_1=64, n_2=65_536, seed `0xC1BE_1A6F`) — the load-bearing fixture per ADR-0021 / pin §5.1 chunk-step table sizes - `m12_lagrange_manual_check_k3_broad` (n_1=32, n_2=64, n_3=128, seed `0xC1BE_1A70`) Vendor-only milestone (Option 2 ratified by orchestrator): no public-API expansion. All required state reachable via `pub(crate)` (NIFS::poly_lookup), `pub` (LookupRunningWitness fields, PerTableBundle fields, Structure::{ell,left,right}), or in-vendor helpers (`combine_columns_witness`, `combine_columns_table`, `crate::spartan::logup_inverses::batch_invert_plus_r`). Test count delta on `neutron::nifs::tests`: 13 → 16. Run with: cargo test --release -p nova-snark --features lookup-fold m12_ 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
… 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
…nobs feature + corrupt_t_lookup_at_index knob + AO 17 visibility bump Per design pin Corrigendum microsoft#10 (Halpert, 2026-05-10) and Corrigendum microsoft#11 (Halpert, 2026-05-10), this commit lands the vendor-side surface for M.GH5.7's three negative tests (cryptographer-gated soundness gating). Cargo.toml — adds `test-debug-knobs = []` opt-in feature flag. Strict additive; production builds without `test-debug-knobs` remain byte- identical to vendor HEAD. src/neutron/circuit/mod.rs: - `NeutronAugmentedCircuitInputs` gains `#[cfg(any(test, feature = "test-debug-knobs"))] pub corrupt_t_lookup_at_index: Option<(usize, E::Scalar)>` field + `with_corrupt_t_lookup_at_index` builder method. - Corruption injection at the augmented-circuit allocation site so the IN-CIRCUIT `t_lookup_running_per_table[idx]` allocation is perturbed AFTER honest U.T_lookup_per_table allocation but BEFORE feeding into `verify_with_multi_table_lookup` (Pin §3.5 shape (a) + Corrigendum microsoft#10 Q2 dispatch shape). - `let mut U` cfg-split so the production build (`lookup-fold` without `test-debug-knobs`) does not trip `#[deny(unused_mut)]`. src/neutron/mod.rs — re-exports `NeutronAugmentedCircuit`, `NeutronAugmentedCircuitInputs`, `AllocatedNIFS`, `AllocatedFoldedInstance`, `AllocatedLookupNIFSMultiTable`, `AllocatedLookupPayloadPublicMultiTable`, `AllocatedNonnativeR1CSInstance` so M.GH5.7's harness-side tests can construct fixtures via direct vendor-internal types per Pin §5.2 + Corrigendum microsoft#10 Q2 Option A.2. src/neutron/nifs.rs — `pub fn prove_with_multi_table_lookup_inner` visibility bump (Auditor Obligation 17 — byte-equivalence verification of synthetic-Some(vec![ZERO; k]) running U vs default-None running U). Lemma α-Q1 (Corrigendum microsoft#10) is exercised by the harness-side AO 17 smoke test asserting prove-call equivalence. src/neutron/relation.rs — exposes `Structure::shape()`, `FoldedInstance::comm_W()`, `FoldedInstance::comm_E()` accessors required by harness-side fixture construction. All `pub` visibility under existing crate-public types; no new layout / no soundness implications. Soundness disposition (Corrigendum microsoft#11): test (i) rejects via dual-path (Path A §1.5 binding-via-hash, Path B §3.3 clone → (C)-binding); per declaration-order at vendor HEAD, Path B declares first and is the asserted twin-substring. AO 9 / (W1)-direct discharged via end-to-end corruption-detection (both paths reject). Pin §5.3 microsoft#3, microsoft#4, microsoft#5 discharged. Pin §D.4 microsoft#5, microsoft#3' discharged. Auditor Obligations 9, 12, 14, 17 status: discharged at vendor HEAD. 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
…a z[F_arity-1] per ADR-0021 NIVC dispatcher (pin §3.2 + Corrigendum microsoft#4) Single-line production read-site reroute at the augmented circuit's lookup-fold-active branch. Per GH-microsoft#7 design pin §3.2 + Corrigendum microsoft#4 (Halpert ratified 2026-05-11; amended-criteria reframe Halpert re-ratified 2026-05-12): - Source of chunk_index_in_z at the production read-site: OLD: &U.X[0] (Corrigendum microsoft#9 interim) NEW: &z_i[z_i.len() - 1] (M.GH7.2; z_i[F_arity - 1]) - synthesize_non_base_case_lookup_fold signature extends with `z_i: &[AllocatedNum<E::Scalar>]` between `pp_digest` and `U` (forwarded from synthesize_non_base_case's existing arity-length z_i slice at circuit/mod.rs:572). The single-IO defensive check on U.X is retained (no longer load-bearing for the read-site but structurally meaningful per pin §1.4 Corrigendum microsoft#3); a new defensive z_i.is_empty() check mirrors it for the new read-site. Architectural M.7 binding-chain preservation per amended criteria (NOT byte-equal pp_digest under lookup_fold_k > 0). The M.7 shape- registry assertion (`crate::shape_registry::assert_pp_digest_matches_registry`) fires at the same internal site at the same FS-transcript point (before ro.absorb(pp_digest) → before the first post-absorb constraint emission at `absorb U2`, circuit/nifs.rs:700). The amended invariant — architectural ordering preservation — is the load-bearing soundness property; the topological pp_digest delta (R1CS variable-ID topology changes when the AllocatedNum source slot changes) is mechanical and not asserted. Z_ARITY = 6 → 7 cascade on the inumbra side is OUT-OF-SCOPE for M.GH7.2 (crafter-mechanical per Corrigendum microsoft#4 §5.2 amendment; deferred to M.GH7.5a wrap-pipeline retarget). The vendor-side read-site reroute is the cryptographer-gated work; the inumbra- side bump is mechanical-following. Regression test at vendor/nova/src/neutron/circuit/nifs.rs (m_gh7_2_chunk_index_in_z_routing_preserves_m7_binding_chain_architecturally): synthesises NeutronAugmentedCircuit<TrivialCircuit, _> with .with_lookup_fold(k=2, &[ZERO], index_n_bits=1) under TestShapeCS (shape-only — inputs=None tolerated). Walks cs.constraints in declaration order and asserts that the namespace path containing "M.7 shape-registry assertion" precedes the path containing "absorb U2" — the architectural FS-transcript point preservation invariant. Under the z-routed read-site, this invariant holds: m7_index < absorb_u2_index (verified PASS). Regression chain verified: - cargo test --release -p nova-snark --features lookup-fold m_gh7_2: 1 passed (new). - cargo test --release -p nova-snark --features lookup-fold neutron::tests::test_pp_digest: 1 passed (expect-fixture stays byte-equal under TrivialCircuit::default() + lookup_fold_k=0; rerouted branch unreachable). - cargo test --release -p inumbra-spend-harness --test gh7_stage_k_compressor: 3 passed (STAGE 0 happy-path at HyperKZG + IPA-PC + cross-PCS hard gate all stay PASS). - cargo test --release -p nova-snark --features lookup-fold m_gh7_1: 1 passed (M.GH7.1 typecheck regression preserved). Refs: pin §3.2 + Corrigendum microsoft#4 (docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md:1184-1210) pin §5.5 row M.GH7.2 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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…ce per-table Vec extension + absorb sites per Corrigendum microsoft#18 Path α (V-α ratified) M.GH7.5.0a vendor-side narrow sub-milestone: extend the in-circuit `AllocatedFoldedInstance` to mirror the off-circuit `FoldedInstance` per-table Vec fields, extend both absorb sites (in-circuit + off-circuit) to bind the per-table running commitments into the IVC public-input hash chain, leaving STAGE-0 at `lookup_fold_k = 0` byte-equivalent under the `Option::None`-skip pattern. In-circuit `AllocatedFoldedInstance` (`circuit/relation.rs`): - New fields under `cfg(lookup-fold)`: - `comm_L_per_table: Option<Vec<AllocatedNonnativePoint<E>>>` - `comm_ts_per_table: Option<Vec<AllocatedNonnativePoint<E>>>` Mirror off-circuit `FoldedInstance::comm_L` / `comm_ts` per M.GH7.0a widening at `relation.rs:273-278`. `comm_inv_w` / `comm_inv_t` intentionally NOT mirrored per Corrigendum microsoft#17 chicken-and-egg resolution. - `alloc_with_k_hint`: extended with Some/None+k-hint/None match analogous to `T_lookup_per_table` discipline at lines 183-215. Reads off-circuit `inst.comm_L.as_deref()` / `inst.comm_ts.as_deref()` (pub(crate) cross-module access within neutron module). Allocates `AllocatedNonnativePoint::alloc(...)` per element under Some-arm and `AllocatedNonnativePoint::alloc(..., None)` under k-hint arm. - `default_with_lookup_k`: extended with `comm_L_zero` / `comm_ts_zero` allocated via `AllocatedNonnativePoint::default(...)` and cloned across k slots, analogous to `T_lookup_zero` discipline. - `default`: outer-base `None` mirrors off-circuit `FoldedInstance::default` produces `comm_L = None` / `comm_ts = None`. - `fold`: passthrough `self.comm_L_per_table.clone()` / `self.comm_ts_per_table.clone()`, analogous to existing `T_lookup_per_table` passthrough. Post-fold per-table commitment update is M.GH7.5.0b scope (verify_with_multi_table_lookup in-circuit body). - `from_lookup_fold_output`: propagate `u_fold.comm_L_per_table` / `comm_ts_per_table` unchanged through. Signature widening (carrying explicit `comm_L_fold_per_table` / `comm_ts_fold_per_table` args analogous to `t_lookup_out_per_table`) deferred to M.GH7.5.0b. - `conditionally_select`: per-table shape-matched select with `(None,None) | (Some(==len), Some(==len)) | _` fail-close invariant identical to `T_lookup_per_table` discipline at line 619. - `absorb_in_ro`: insert per-table `comm_L` block + per-table `comm_ts` block AFTER existing `T_lookup_per_table` block and BEFORE `u` / `X` absorbs. Uses `c.absorb_in_ro(cs.namespace(...), ro)?` matching the existing `comm_W.absorb_in_ro(...)` invocation shape. `table_id`-canonical order preserved via Vec storage order. Off-circuit `FoldedInstance` (`relation.rs`): - `absorb_in_ro2`: byte-mirror — insert per-table `comm_L` + per-table `comm_ts` AFTER existing `T_lookup` block and BEFORE `u` / `X` absorbs. Uses `c.absorb_in_ro2(ro)` matching existing `comm_W.absorb_in_ro2(ro)` invocation shape. The FS-transcript ordering is byte-equivalent to the in-circuit `absorb_in_ro` extension. `pp_digest` baseline refresh: NONE required at this milestone. STAGE-0 at `lookup_fold_k = 0` is preserved byte-identical via the `Option::None` skip pattern; the `neutron::tests::test_pp_digest` engine-specific expect strings pass unchanged. `test_neutron_recursive_circuit_pasta` constraint counts pass unchanged. The `lookup_fold_k > 0` IVC paths that DO exercise the new absorbs (STAGE-0 byte-equivalence tests at `circuit/relation.rs:667+`) pass green — both in-circuit and off-circuit sequences extend in lockstep. Tests run (vendor-side, scoped per .claude/rules/testing.md): - neutron::tests::test_pp_digest: 1 passed (no digest drift at k=0) - neutron::circuit::tests::test_neutron_recursive_circuit_pasta: 1 passed (constraint count unchanged at k=0) - neutron::circuit::relation::stage0_byte_equivalence_tests: 5 passed (byte-equivalence at k>0 IVC preserved) - neutron::tests: 9 passed (full IVC integration) - neutron::circuit::lookup::tests: 4 passed - neutron::nifs::tests: 17 passed - neutron::lookup_sumcheck::tests: 9 passed - neutron::compressed_snark: 10 passed (Stage-K close pipeline) M.GH7.5.0b deferrals (intentional, narrow-sub-milestone discipline): - `verify_with_multi_table_lookup` in-circuit per-table fold body (per-`j` `(1-r_b)·U + r_b·b` mirror of off-circuit `relation.rs:862-884`) — Corrigendum microsoft#18 item 2. - `LookupVerifyOutputMultiTable` widening with `comm_L_fold_per_table` / `comm_ts_fold_per_table` Vec fields — Corrigendum microsoft#18 item 2. - `from_lookup_fold_output` signature widening (the M.GH7.5.0a passthrough-from-u_fold form is the structurally-only-correct path until M.GH7.5.0b lands the per-table fold computation). - Augmented-circuit final-step rewire in `synthesize_non_base_case_lookup_fold` (Corrigendum microsoft#18 item 3). - `AllocatedNonnativePoint::fold_with_scalar` authoring (if absent at vendor HEAD at M.GH7.5.0b dispatch). - Negative-test triple for binding discharge (M.GH7.5 scope). - Off-FS commitment-equality envelope check (M.GH7.5 scope). - Dead hint fields clean-up (`comm_L_fold`/etc on `NeutronAugmentedCircuitInputs`) — per Corrigendum microsoft#18 second-order issue microsoft#3, intentionally out-of-scope. Verify-don't-assume grounding (Phase 1 audit, vendor HEAD `1d67632`): - `AllocatedFoldedInstance` struct fields (comm_W, comm_E, T, T_lookup_per_table, u, X) — confirmed at `circuit/relation.rs:26-56`. - `FoldedInstance::comm_L` / `comm_ts` Vec fields — confirmed at `relation.rs:273-278`. - `absorb_in_ro` insertion site — confirmed `T_lookup_per_table` block at `:373-378`, `u` absorb at `:380`. - `absorb_in_ro2` insertion site — confirmed `T_lookup` block at `:926-931`, `u` absorb at `:933`. - `test_pp_digest` corrected line cite — confirmed at `mod.rs:1131-1146` (NOT Corrigendum microsoft#17's stale `:830, :834, :838`). - `AllocatedNonnativePoint::alloc` signature `Option<(E::Base, E::Base, bool)>` — confirmed at `gadgets/ecc.rs:891`. - `AllocatedNonnativePoint::absorb_in_ro` signature `fn(&self, mut cs, ro: &mut E::RO2Circuit) -> Result<()>` — confirmed at `gadgets/ecc.rs:952`. - `AllocatedNonnativePoint::conditionally_select` signature — confirmed at `gadgets/ecc.rs:979`. Cryptography rule grounding (.claude/rules/cryptography.md): The struct extension + absorb extension is a STORAGE + BINDING extension, not a constraint-family extension (no new R1CS constraints on per-`j` arithmetic — that lands at M.GH7.5.0b's `verify_with_multi_table_lookup` body). The Gadget contract's ≥1000-iter differential coverage requirement attaches at M.GH7.5.0b when the in-circuit per-table fold body is authored. M.GH7.5.0a's absorb extension preserves the existing STAGE-0 byte-equivalence coverage as the differential. References superproject HEAD `23ec6b3` Corrigendum microsoft#18 path α 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 16, 2026
…perKZG opening at r_x (KPI microsoft#3 envelope restoration) Implements Corrigendum microsoft#29 of the GH-microsoft#7 Stage K corrigenda chain per the ratified design pin at docs/research/cryptography/microsoftgh-7-stage-k-corrigendum-T-lookup-envelope-2026-05-16.md (Halpert, 2026-05-16; cryptographer-reviewer RATIFY). Mechanism (Path b ratified): replace the per_table_T_lookup: Vec<Vec<E::Scalar>> envelope field whose inner length num_cons is the linear-in-num_cons envelope-size regression at KPI microsoft#3 (slice-04 forecast ~12,289 bytes vs 12,288-byte ceiling; slice-06 multi-MB under k=2 at num_cons ~1.7M) with per_table_comm_T_lookup: Vec<Commitment<E>>. The verifier batched-opens T_j(r_x) via a 5th per-table PolyEvalInstance in the existing u_vec (extending 3 + 4*k -> 3 + 5*k); the claimed evaluation comes from the prover-published per_table_outer_evals[j].eval_T (already consumed by the unified outer-sumcheck residue identity per Corrigendum microsoft#16 Finding B). Affected sites: - vendor/nova/src/neutron/compressed_snark.rs: * Struct field per_table_T_lookup -> per_table_comm_T_lookup * build_per_table_commitments: 4-tuple -> 5-tuple * prove_with_lookup_fold: pass new commitment slice * prove_from_parts_with_logup: new parameter + envelope FS-absorb of per_table_comm_T_lookup under FS-tag b"comm_T_lookup_j" (was raw vec under b"T_lookup_j") * prove_from_parts (k=0 path): empty slice for the 5th param * verify body: cardinality check + FS-absorb + Spartan delegation * M.GH7.4c acceptance test: build the 5th commitment, drop the inner-length assertion (commitments have no inner length) - vendor/nova/src/spartan/snark.rs: * prove_with_T_claim_split_error_with_logup: new parameter per_table_comm_T_lookup + cardinality assert; w_vec and u_vec extended from 3 + 4*k to 3 + 5*k with the 5th per-table entry (PolyEvalWitness {p: per_table_T[j].clone()} + PolyEvalInstance {c: per_table_comm_T_lookup[j], x: r_x.clone(), e: per_table_outer_evals[j].eval_T}) * verify_with_T_claim_split_error_with_logup: signature change per_table_T: &[Vec<E::Scalar>] -> per_table_comm_T: &[Commitment<E>]; remove inner-length-num_cons check; remove MLE-eval cross-check (the binding migrates to the batched HyperKZG opening at the u_vec extension below); extend u_vec from 3 + 4*k to 3 + 5*k * Test-scope build_per_table_commitments: 4-tuple -> 5-tuple * M.GH7.4a + M.GH7.4b acceptance tests: build the 5th commitment; update call sites; verify still accepts FS-tag substitution b"T_lookup_j" -> b"comm_T_lookup_j" at BOTH the prover-side envelope absorb (prove_from_parts_with_logup step (7), compressed_snark.rs:2235) AND the verifier-side envelope absorb (CompressedSNARK::verify, compressed_snark.rs:2577). This is a forward-incompatible breaking change per design pin §4.4: no envelope back-compat shim. Same-tag-different-payload would silently re-derive a different challenge stream that the prover-side did not match (a Halpert-class forgery vector). Pre-flight gates (per design pin §7.3 / cryptographer-reviewer): - (a) HyperKZG batched-opening capacity: PASSED. EE::prove / EE::verify operate on a single combined polynomial built via batch_eval_reduce / batch_eval_verify (vendor/nova/src/spartan/mod.rs:393 / :452); proof overhead is O(log size_max), not O(k · log num_cons). 5th entry adds zero new opening proofs. - (b) PolyEvalInstance::batch_diff_size at length num_cons: PASSED. vendor/nova/src/spartan/mod.rs:320-362 accepts num_vars: &[usize] with L0 Lagrange-rescale; existing 4 per-table entries already at length num_cons (snark.rs:1554-1573); 5th entry is mechanically identical. - (c) Verifier cardinality check located at compressed_snark.rs:2400; updated to per_table_comm_T_lookup.len() != k. - (d) FS-tag substitution sites: 2 absorb call-sites (prover at line 2235, verifier at line 2577). Both changed. No stale b"T_lookup_j" references remain in any code path; only audit-trail commentary preserves the pre-corrigendum form. - (e) Commitment basis: PASSED. All 5 per-table commitments use prefix- basis ck.ck[..num_cons] (build_per_table_commitments delegates to E::CE::commit(ck, ..., &ZERO) identically for all 5). §7.3 acceptance gates: - (b) cargo test -p nova-snark --features lookup-fold --release --lib: 194 passed; 1 failed; 3 ignored. The single failure (neutron::tests::m_gh7_3a_prove_step_with_lookup_fold_sibling_threads_running_lws_witness_alloc_preserved_positive_path) is PRE-EXISTING on the lookup-fold baseline (verified by stashing Corrigendum microsoft#29 changes and re-running the same test; same failure) and belongs to the M.GH7.5 / Corrigendum microsoft#23 TRIAGE-ROUTED IVC-trace empirical investigation that is STRUCTURALLY ORTHOGONAL to the envelope-shape change per design pin §5.4 issue 4. Corrigendum microsoft#29 is the structural-correctness change against the current per_table_T_lookup field; Corrigendum microsoft#24+ owns the M.GH7.5 full-R1CS-sat empirical close. - Corrigendum microsoft#29-specific acceptance tests ALL PASS: * spartan::snark::tests::m_gh7_4a::m_gh7_4a_prove_with_T_claim_split_error_with_logup_round_trip ... ok * spartan::snark::tests::m_gh7_4a::m_gh7_4b_prove_with_T_claim_split_error_with_logup_pcs_opening_batched_round_trip ... ok * spartan::snark::tests::m_gh7_4a::m_gh7_4a_per_table_outer_evals_struct_field_shape ... ok * neutron::compressed_snark::tests::m_gh7_4c_compressed_snark_end_to_end_with_per_table_lookup_envelope_transcript ... ok These exercise the prover-side signature change, the verifier-side signature change, the 3+5*k u_vec extension, and the end-to-end envelope FS-tag substitution. - (c) No regression on existing vendor-side acceptance tests naming per_table_T_lookup: confirmed. The only sites are the M.GH7.4c acceptance test (which was updated to use per_table_comm_T_lookup and now asserts cardinality, not inner length) and audit-trail commentary referencing the pre-corrigendum form. Inumbra-side rebase + slice-04 envelope re-measurement is the follow-up dispatch per design pin §7.4. The forecast post-corrigendum is slice-04 ~9,810 bytes (band 9,500-10,500); the un-#[ignore] of the ceiling-asserting tests at arity_envelope_acceptance.rs:393 and :537 lands in that follow-up. 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
1 participant
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.
These modules need to be public so users of
novacan implement the traits and create circuits.