Input checks by srinathsetty · Pull Request #5 · microsoft/Nova

srinathsetty · 2021-10-04T23:06:52Z

No description provided.

* Separate types for Relaxed R1CS and R1CS instances and witnesses * Allows creating default values for Relaxed R1CS types * StepSNARK now folds a regular R1CS instance-witness into a running Relaxed R1CS instance-witness * We additionally enforce input chaining checks: the incoming instance must have input that matches the output of the incremental computation thus far

…et/bug/test_fix Fixes a bug with the tests

* abomonation for public params * update .gitignore * remove unneeded file * fix: adjust to upstream --------- Co-authored-by: François Garillot <francois@garillot.net>

…rameter (microsoft#5) * feat: Make commitment key generation configurable with an optional parameter - Implemented the `Len` trait within `CommitmentKey` to allow length quantification in terms of group generators. Made ppSnark fail setup if given commitment key with insufficient length, as measured by its own commitment_key_floor() (see below) - Made RelaxedR1CSTrait include a fn commitment_key_floor() -> Box<dyn for<'a> Fn(&'a R1CSShape<G>) -> usize> with default implementation to quantify the Snark's commitment key size requirements in the shape of a closure, - Made PublicParameters accept optional Box<dyn for<'a> Fn(&'a R1CSShape<G>) -> usize> parameters for each circuit's group, to parametrize the CommitmentKey creation. Implementation details: - defined type alias CommitmentKeyHint<G> = Box<dyn Fn(&R1CSShape<G>) -> usize>; - Modified numerous function calls and parameter setups to include optional parameter `CommitmentKeyHint` that gives a more flexible commitment key generation. - Added the `CommitmentKeyHint` to the `r1cs` import list and expanded `NovaShape` trait to optionally accept it. * fix: rename Len::len -> Len::length to avoid unrelated clippy lint

…ookup_per_table absorb extension Lands the (W1) §1.4 binding fix per the GH-microsoft#5 design pin (`docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md`). Vendor surface changes (both gated `#[cfg(feature = "lookup-fold")]`): `src/neutron/circuit/relation.rs::AllocatedFoldedInstance`: - New field: `T_lookup_per_table: Option<Vec<AllocatedNum<E::Scalar>>>` per pin §3.2 (W3 verdict). - `alloc(...)` extended to populate from `inst.t_lookup()` (length implicit, `None` at outer base). - New `default_with_lookup_k(cs, k)` constructor allocating `[alloc_zero(); k]` per pin §2.3 / §3.2; marked `#[allow(dead_code)]` until M.GH5.3 wires it into `synthesize_base_case`. - `default()` extended with `T_lookup_per_table: None`. - `absorb_in_ro` extended (the W1 §1.4 binding fix): each `T_lookup_per_table[j]` absorbed in `table_id`-canonical order BETWEEN `T` and `u`, empty-not-skipped at outer base. - `fold(...)` extended with passthrough. - `conditionally_select` extended with per-element select on matched-shape `Option<Vec<...>>`; mismatched shapes return `SynthesisError::Unsatisfiable` (fail-closed). `src/neutron/relation.rs::FoldedInstance`: - `AbsorbInRO2Trait::absorb_in_ro2` mirror: each `T_lookup[j]` absorbed in `table_id`-canonical order BETWEEN `T` and `u`, empty-not-skipped at outer base. Native side byte-equivalent to in-circuit by construction. Cryptographer (Halpert / `@nw-cryptographer`) ratification 2026-05-09: APPROVE byte-order parity per pin §1.4 (verbatim contract: comm_W → comm_E → T → T_lookup_per_table[*] → u → X). High confidence on parity. Empty-not-skipped behavior at outer base structurally identical on both sides. No corrigendum required on §1.4. Test posture: 146/146 vendor lib tests pass + 3 ignored release-only. 40/40 `neutron::*` tests with `--features lookup-fold` pass. Zero regression — existing tests use outer-base running U (`T_lookup == None` / `T_lookup_per_table == None`); the new branch absorbs no extra scalars and the existing FS-transcript schedule is preserved verbatim. Empirical validation of the (W1) binding-via-hash claim follows in M.GH5.0 STAGE 0 spike (next dispatch). Per pin §6.2 / §6.1 W1 falsifier: STAGE 0 byte-equivalence test is the hard gate before any further GH-microsoft#5 milestone proceeds. Reviewed by `@nw-cryptographer` (Halpert) per the GH-microsoft#5 per-step pre-commit review pattern. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…alloc fail-close + X-arity invariant Closes M.GH5.0 STAGE 0 hard gate per the GH-microsoft#5 design pin (`docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md`), honoring the §1.4 + §6.2 corrigenda (Halpert ruling 2026-05-09 on the prior-dispatch's empirical falsifier). ## Background First M.GH5.0 dispatch (vendor commit absent — uncommitted) authored a STAGE 0 fixture using `DirectCircuit::<E, NonTrivialCircuit<Scalar>>` which produces `num_io == 2`. The byte-equivalence test failed at step 1: `cs.is_satisfied() == true` but `h_native != h_circuit`. Halpert re-derivation 2026-05-09 (case (a) — pin §1.4 incompleteness): the (W1) binding-via-hash extension implicitly required `FoldedInstance::X.len() == 1` to hold byte-equivalence between native (`for x in &self.X { ro.absorb(*x); }`) and in-circuit (single `AllocatedNum`). The pin §1.4 pseudocode elided this precondition; the silent `inst.X[0]` truncation in `AllocatedFoldedInstance::alloc` made the violation undetectable. The (W1) soundness reduction at §1.5 holds at the production shape (`circuit/mod.rs:428` calls `hash.inputize` exactly once → `num_io == 1`). No soundness-class halt; pin amendment + impl fail-close + fixture re-shape closes STAGE 0. ## Vendor changes (this commit) `src/neutron/circuit/relation.rs`: 1. **Fail-closed `AllocatedFoldedInstance::alloc`** (lines ~69-86): when `inst.is_some() && inst.X.len() != 1`, return `SynthesisError::Unsatisfiable("...num_io == 1...")`. Outer-base (`inst == None`) unchanged. Mirrors `conditionally_select`'s T_lookup_per_table shape-mismatch fail-close. 2. **STAGE 0 fixture re-shape** (path A per pin §6.2 + §1.4 corrigendum): `m_gh5_0_stage0_absorb_in_ro_byte_equivalence_at_fold_depth_1_and_2` uses `NeutronAugmentedCircuit<'_, E, NonTrivialCircuit<Scalar>>` for shape build (production shape). Asserts `shape.num_io() == 1` at fixture-build. Preserves k=2 multi-table fold-of-two structure, T_lookup pre-check (`Some(&[non-zero, non-zero])`) at both steps, and squeeze-output equality framing (per Halpert Q3 ratification) — `h_native == h_circuit_witness_value` AND `cs.is_satisfied() == true` at both fold steps. 3. **Negative-arity sibling test** `m_gh5_0_alloc_rejects_x_arity_two`: constructs `FoldedInstance` with `X.len() == 2`, asserts `Err(SynthesisError::Unsatisfiable(msg))` with `msg.contains("num_io == 1")`. Documents the X-arity invariant fail-closed at the impl level. ChaCha20Rng seed: `0xC1BE_5BAD_C0DE_0050` (preserved from prior dispatch for reproducibility). ## Empirical results (release-mode mandatory) ``` cd vendor/nova && cargo test --release --features lookup-fold \ stage0_byte_equivalence_tests -- --nocapture ``` `m_gh5_0_stage0_absorb_in_ro_byte_equivalence_at_fold_depth_1_and_2`: PASS `m_gh5_0_alloc_rejects_x_arity_two`: PASS `cargo check --tests --features lookup-fold` clean. ## Wider regression surfaced (handled in sibling commit M.GH5.0a) The fail-close correctly (per the §6.2 corrigendum) rejects 4 pre-existing tests in `src/neutron/circuit/lookup.rs` that use `DirectCircuit::<NonTrivialCircuit>` (`num_io == 2`) and silently relied on the prior allocator truncating `inst.X[0]`: - `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` Per Halpert ruling Q2 (Path Z) + §6.2 propagation corrigendum: these re-shape on a sibling **M.GH5.0a** commit ahead of M.GH5.1, with attribution to this M.GH5.0 dispatch. Mirror's the spike-era latent-failure discipline (`.claude/rules/testing.md`). Reviewed by `@nw-cryptographer` (Halpert) per the GH-microsoft#5 per-step pre-commit review pattern. APPROVE-FOR-COMMIT verdict, High confidence on the fix's faithfulness to the §1.4 + §6.2 corrigenda. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… 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>

…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>

… §5.5 row M.GH5.1 - src/neutron/mod.rs: pub mod lookup_sumcheck (was pub(crate)) - src/neutron/nifs.rs: pub on NIFS::{poly, poly_lookup, comm_E, comm_inv_w, comm_inv_t} (was pub(crate); added missing-docs comments per vendor #![deny(missing_docs)]) Closes (W6) prerequisite for M.GH5.6 off-circuit running-scalar reference differential. Zero-algebra / zero-FS / zero-digest — visibility surface only. Roadmap: docs/feature/microsoftgh-5-augmented-circuit-wireup/deliver/roadmap.json row 01-02 Pin: docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md §5.5 row M.GH5.1 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…h Y extension to T_lookup_per_table - default_with_lookup_k: allocate T_lookup_zero = alloc_zero(...) once, clone across k slots; each T_lookup_per_table[j] inherits (0)·(0) = T_lookup_zero zero-binding constraint - Variable-identity binding test (extends M.GH5.0 STAGE 0 module) - pp_digest baselines unchanged (default_with_lookup_k is #[allow(dead_code)] until M.GH5.3 wires synthesize_base_case through this constructor; the production augmented circuit's R1CS shape is not affected at this milestone — Pallas/Bn256IPA/Secp256k1 expects all hold) Closes the IVC-anchor constraint-binding gap surfaced during M.GH5.2 review. Same class as Corrigendum microsoft#4's X-side fix; same precedent for test-shape adaptation. Halpert-ratified per Corrigendum microsoft#6. Test extension (m_gh5_0_path_y_x_t_aliasing_binding): + Cases (1, Some(2)) and (2, Some(2)) — k=2 production arity per ADR-0021 + Variable-identity binding: T_lookup_per_table[j].get_variable() == T_lookup_per_table[0].get_variable() for all j ∈ [1, k) — intra-Vec aliasing form (TestConstraintSystem does not support post-allocation witness mutation; Corrigendum microsoft#4-A precedent for adapted assertion) + Distinctness from T: T_lookup_per_table[0].get_variable() != T.get_variable() — confirms Halpert's recommended SEPARATE T_lookup_zero (not aliased to T) + Constraint-count floor: default_with_lookup_k MUST emit ≥ 6 constraints (default(num_io) baseline 5 + 1 from T_lookup_zero alloc_zero), strictly exceeding the default(num_io) baseline Pre/post numbers (TestConstraintSystem at num_io=1, k=2, Bn256EngineKZG): pre-fix: num_constraints=5, T_lookup_per_table[0]=Aux(5), T_lookup_per_table[1]=Aux(6) — distinct fresh aux per slot, ZERO new constraints (the gap Corrigendum microsoft#6 closes) post-fix: num_constraints=6, T_lookup_per_table[0]=Aux(5), T_lookup_per_table[1]=Aux(5) — shared T_lookup_zero, (0)·(0) = T_lookup_zero constraint enforced Adversary-side: TestConstraintSystem does not expose post-allocation witness mutation; per Corrigendum microsoft#4-A precedent the witness-injection negative test is a structural counterfactual under Path Y. The variable-identity assertion algebraically subsumes it: a malicious prover attempting T_lookup_per_table[j] = N ≠ 0 would attempt T_lookup_zero = N, rejected directly by alloc_zero's row at synthesis. Pin: docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md §1.4 Corrigendum microsoft#6 Roadmap: docs/feature/microsoftgh-5-augmented-circuit-wireup/deliver/roadmap.json row 01-03 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…p-fold wire-up Wires NeutronAugmentedCircuit::synthesize_non_base_case through verify_with_multi_table_lookup and synthesize_base_case through default_with_lookup_k under the lookup-fold cfg + runtime gate. Closes (W3) plumbing and (W4) confirmation per pin §1.4. Vendor-side surface: - NeutronAugmentedCircuitInputs: +public_bundles_multi_table field (Option<Vec<LookupPayloadPublicMultiTable<E>>>) per pin §3.1 - NeutronAugmentedCircuit struct: +shape_registry, +lookup_fold_k, +index_n_bits fields; with_lookup_fold(k, registry, bits) builder (#[allow(dead_code)] until M.GH5.4 inumbra-side wire-up) - alloc_with_k_hint: T_lookup_per_table allocation branches on inst.t_lookup() Some/None × k > 0 hint - synthesize_base_case: under #[cfg(feature = "lookup-fold")] dispatches to default_with_lookup_k(cs, 1, k) when lookup_fold_k > 0; else default(cs, 1) - synthesize_non_base_case: under same cfg dispatches to new private synthesize_non_base_case_lookup_fold method when lookup_fold_k > 0; else legacy nifs.verify - synthesize_non_base_case_lookup_fold: allocates chunk_index_in_z = U.X[0], shape_registry, AllocatedLookupNIFSMultiTable, per-bundle AllocatedLookupPayloadPublicMultiTable; invokes verify_with_multi_table_lookup; rebinds post-fold T_lookup_per_table via from_lookup_fold_output (no-constraint structural rewire) - AllocatedLookupPayloadPublicMultiTable::alloc helper Halpert ratification (2026-05-09 dispatch, all 6 questions RATIFY, High confidence): - Q1 Option B (cfg + runtime lookup_fold_k > 0 gate): selected per Principle 7 + ADR-0023 vendor-fork separability. lookup_fold_k is construction-time pinned and pp_digest-shape-bound; no downgrade attack possible. - Q2 Argument-order canonical, table_id-traversal mechanical (Vec iter preserves order at every fold depth). - Q3 lookup_fold_k as usize correct at M.GH5.3; per-position uniformity assertion deferred to M.GH5.4 per Auditor Obligation 10. - Q4 M.7 shape-registry assertion fires BEFORE pp_digest.absorb per pin §2.5 (vendor/nova/src/neutron/circuit/nifs.rs:689-698 direct verification). Dispatch text's "AFTER" formulation was a misstatement; STOP-AND-ASK NOT triggered. - Q5 (W4) Phase-1↔Phase-2 binding closed: clone() on AllocatedNum preserves Variable identity, so Phase-1 hash binding of U.T_lookup_per_table transitively binds Phase-2 verifier inputs. - Q6 from_lookup_fold_output no-constraint rewire is sound; (C)-binding at nifs.rs:872-897 takes the binding role at fold-depth ≥ 1 that alloc_zero plays at base case. Path Y / microsoft#4-A invariants are base-case-only. Test posture preserved at M.GH5.2 close baseline: - vendor --release --features lookup-fold: 152/0/7 - vendor --release (default): 80/0/6 - inumbra-spend-circuits: 87/0/9 lib + 4 RED scaffolds - inumbra-spend-harness: 13/0 - M.GH5.0 STAGE 0 + Corrigendum microsoft#4-A + Corrigendum microsoft#6 tests: pass - pp_digest baselines unchanged (vendor IVC tests on legacy path; refresh deferred to M.GH5.4 when inumbra-side wires with_lookup_fold(2, ...)) - Determinism verified across 2 consecutive runs. Pin: docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md §3.1 + §3.2 + §3.4 + §5.1 + §5.5 row M.GH5.3 Roadmap: docs/feature/microsoftgh-5-augmented-circuit-wireup/deliver/roadmap.json row 01-04 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… threads shape_registry to NeutronAugmentedCircuit::new Per pin §5.5 row M.GH5.4 (post-Corrigendum-microsoft#8 reverted scope) sub- deliverable 2: - Extend `PublicParams::setup` and `setup_with_ptau_dir` under `feature = "lookup-fold"` to accept `(shape_registry: Vec<E1::Scalar>, lookup_fold_k: usize, index_n_bits: usize)`. Threaded to the shape- derivation `NeutronAugmentedCircuit::new` call via `with_lookup_fold(...)`. Non-`lookup-fold` builds keep the pre-M.GH5.4 signature (vendor examples / benches build unchanged). - Store the registry triple on `PublicParams` under `lookup-fold`, `#[serde(skip)]`-gated so the bincode encoding (and therefore `pp_digest`) is byte-equivalent to pre-M.GH5.4 at the default `(vec![], 0, 0)` state. Vendor-internal `test_pp_digest` baselines do NOT refresh — confirmed empirically: 152/0/7 release sweep matches pre-M.GH5.4 baseline byte-for-byte. - `RecursiveSNARK::new` (base case) and `RecursiveSNARK::prove_step` read the triple from `pp` and chain `with_lookup_fold(pp.lookup_fold_k, &pp.shape_registry, pp.index_n_bits)` on each `NeutronAugmentedCircuit::new`. This closes the four invocation sites the pin §3.1 binding requires (the augmented-circuit shape-derivation site + the prove-step site must emit byte-equivalent R1CS, which they do because both threads the same triple from `pp`). - Lift `#[allow(dead_code)] until M.GH5.4` on `NeutronAugmentedCircuit::with_lookup_fold` (vendor `circuit/mod.rs:268`). The `with_multi_table_bundles` annotation (`circuit/mod.rs:139`) stays — its per-step consumer wires up at M.GH5.5 (the inumbra-side fold-of-N happy-path differential). - Vendor-internal `TrivialCircuit` / `CubicCircuit` test sites updated to pass `(vec![], 0, 0)` under `lookup-fold` (the default lookup- fold-OFF state); shape and `pp_digest` byte-equivalent to pre-M.GH5.4. Sub-deliverable 1 (inumbra-side consumer wire-up) is a no-op at this milestone: there is no inumbra-side consumer of `neutron::PublicParams::setup` yet (wrap.rs is on `nova_snark::nova::*` per Corrigendum microsoft#8; will stay through M.GH5.9; Stage K migration dispatched as separate GH-microsoft#7). `build_chunk_step_registry` (M.10 / `shape_registry.rs:224`) is ready to be invoked by M.GH5.5 when the inumbra-side fold-of-N differential dispatches against the augmented-circuit IVC. Auditor Obligation 10 confirmed by construction at `shape_registry.rs:347`: `vec![merged_mc, chunk_mc]` (length 2) inside the `0..NUM_CHUNK_POSITIONS=16` loop — k=2 uniform across all 16 chunked-Strauss-Shamir positions per ADR-0021. Test results (release-mode per `.claude/rules/testing.md`): - vendor `cargo test --release -p nova-snark --features lookup-fold`: 152/0/7 (matches pre-M.GH5.4 baseline; no `pp_digest` refresh needed — the `#[serde(skip)]` design preserves the bincode encoding). - inumbra-spend-circuits lib: 87/0/9 + 4 RED scaffolds (baseline). - inumbra-spend-harness: 13/0 (baseline). - M.GH5.0 STAGE 0 + Corrigendum microsoft#4-A + Corrigendum microsoft#6 tests pass. Closes (W4) plumbing per pin §5.5. Wire-up consumer at M.GH5.5. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…e-tag — Corrigendum microsoft#9 Re-tag #[allow(dead_code)] from "until M.GH5.4" to "until GH-microsoft#7" per Halpert Corrigendum microsoft#9 (2026-05-10). The chunk_index_in_z routing question carry-forwards to GH-microsoft#7 (Stage K); inumbra-side wiring of RecursiveSNARK::prove_step through with_multi_table_bundles is GH-microsoft#7 scope, not M.GH5.4 / M.GH5.5. Pin: docs/research/cryptography/microsoftgh-5-augmented-circuit-wireup-design-pin-2026-05-08.md §1.4 Corrigendum microsoft#9 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…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).

…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>

…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>

… 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>

…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>

…ing via batch_eval_reduce extension (per Corrigendum microsoft#16; AO 15 Tier-2 part 1 discharge positive-path) Authors the M.GH7.4 subdivision's second sub-milestone (M.GH7.4b per Corrigendum microsoft#16 §5.5 row split). Two new vendor-side surfaces; one struct extension; one new helper. Inner sumcheck + outer sumcheck UNCHANGED from M.GH7.4a — M.GH7.4b extends the batch-eval-reduce PCS-opening layer only. 1. `RelaxedR1CSSNARK::per_table_outer_evals: Option<Vec<PerTableOuterEvals>>` at `src/spartan/snark.rs` — new struct field on the existing Spartan-side SNARK struct under `#[serde(default = "Option::default")]` (preserves the existing serialised proof shape for β'/M.GH7.0.0 paths verbatim). Populated by `prove_with_T_claim_split_error_with_logup`; read by `verify_with_T_claim_split_error_with_logup` to reconstruct the unified outer-sumcheck residue claim. `PerTableOuterEvals<F>` at `src/spartan/sumcheck.rs` gains `Serialize`/`Deserialize` derives under `#[serde(bound = "F: Serialize + serde::de::DeserializeOwned")]`. 2. `RelaxedR1CSSNARK::prove_with_T_claim_split_error_with_logup` extended at `src/spartan/snark.rs` — signature appends four per-table commitment slices (`per_table_comm_L`, `per_table_comm_ts`, `per_table_comm_inv_w`, `per_table_comm_inv_t`); `u_vec`/`w_vec` extended from 3 entries to `3 + 4·k` entries by appending per-table openings at evaluation point `r_x` (full length-`ell` outer-sumcheck challenge, per Corrigendum microsoft#16 Finding F flat-embedding disposition). PCS-opened subset per j is `(w_j, ts_j, inv_w_j, inv_t_j)` consuming the four corresponding `PerTableOuterEvals` fields as `PolyEvalInstance::e` values. The `batch_eval_reduce` call site is otherwise byte-identical; the Corrigendum microsoft#12 zero-pad fix at `PolyEvalWitness::batch_diff_size` handles the heterogeneous-size openings (W.W at length `num_vars`; E1 at `left`; E2 at `right`; per-table polys at `num_cons`; W.W and the per-table polys are the asymmetric pair at the test fixture where `num_vars < num_cons`). Per-table outer evals are duplicated into the proof envelope via `per_table_outer_evals: Some(per_table_outer_evals .clone())` so the verifier can deserialise them without a separate out-of-band carry; the existing pass-through return tuple is preserved verbatim for M.GH7.4a byte-identical regression. 3. `RelaxedR1CSSNARK::verify_with_T_claim_split_error_with_logup` at `src/spartan/snark.rs` — new verifier-side sibling, the M.GH7.4b dual of the prover. FS-transcript discipline byte-identical to β'/with-logup prover (Primitive 5: absorb vk → U → T_claim before any squeeze). Verifies outer sumcheck at degree-3 with claim = `U_bridged.T` (matches prover under Corrigendum microsoft#16 Finding C additive composition degree-3). Reconstructs `claim_outer_final_expected` as the additive composition of the R1CS-side residue (`eval_E1·eval_E2·(claim_Az·claim_Bz − claim_Cz)`) plus per-table (A) `eval_eq_w_j·(eval_inv_w_j·(eval_w_j + r_logup_j) − 1)` and (B) `eval_eq_t_j·(eval_inv_t_j·(eval_T_j + r_logup_j) − eval_ts_j)` residues per Corrigendum microsoft#16 Finding B (no gamma-RLC). Verifies the prover-supplied `eval_T_j` against the public table-data MLE at `r_x` (rejecting a forged `eval_T_j` is the discipline that pins (B)-side correctness — without this check, an adversarial prover could supply any `eval_T_j` and trivially satisfy (B)). Extends batch_eval_verify u_vec to `3 + 4·k` entries symmetric with the prover. 4. `build_per_table_commitments` test helper at the `m_gh7_4a` module — commits the four PCS-opened per-table polys against the test `CommitmentKey` with zero blindings (matches the M.GH7.4a fixture's derandomised E1/E2 commitment discipline). STOP-AND-ASK gates (Corrigendum microsoft#16 §5.5 row M.GH7.4b) — NONE RAISED: Gate microsoft#4 (PCS opening evaluation-point partition / Finding F): RESOLVED via flat embedding at `r_x`. M.GH7.4a's `prove_neutron_outer_with_logup` binds per-table polys uniformly with R1CS-side polys via `bind_poly_var_top` over the full `ell = log2(num_cons)` rounds; after the outer sumcheck closes, each per-table poly reduces to a single scalar at `r_x` (full length-`ell` challenge). `batch_eval_reduce` requires `w.p.len() == 1 << x.len()` per `mod.rs:417`; for per-table polys `(num_cons, ell)`, the equality `num_cons = 1 << ell` holds by construction. No sub-vector partition needed; Corrigendum microsoft#9 (2-A) `r_x_high`/`r_x_low` partition is preserved verbatim and is consumed ONLY by `comm_E1`/`comm_E2` (rank-1 tensor factorisation), NOT by the per-table entries (which open at full `r_x`). Gate microsoft#5 (`batch_eval_reduce` heterogeneous-size capacity): RESOLVED at the algebra + via empirical close. The existing β' u_vec already carries heterogeneous-size openings (comm_W at length `num_vars`; comm_E1 at `left`; comm_E2 at `right`). M.GH7.4b appends `4·k` per-table entries at length `num_cons`. The Corrigendum microsoft#12 zero-pad fix at `PolyEvalWitness::batch_diff_size` (`src/spartan/mod.rs:186-198`) uses `.get(..).unwrap_or(&[])` bounds-checking on chunks past a smaller polynomial's end; chunks that straddle the boundary use `.zip` truncation; both handle the per-table extensions structurally without re-authoring. Verifier-side `PolyEvalInstance::batch_diff_size` (`mod.rs:320-362`) Lagrange-extends the smaller-domain claims via the `(1 − r_lo).product()` correction so the heterogeneity is bookkept symmetrically. Empirically closed by the M.GH7.4b acceptance test below (both Bn256EngineKZG + PallasEngine engines round-trip). Additional structural STOP-AND-ASK gates raised by the dispatch: - `FoldedWitness<E>` per-table blindings: NOT NEEDED. The dispatch assumed `PolyEvalWitness<E>` carries blindings (`r:` field) and that M.GH7.4b would need per-table `r_L_per_table`/etc. Verified at vendor HEAD: `PolyEvalWitness<E>` is `{ p: Vec<E::Scalar> }` — blinding-less. No `FoldedWitness` extension required. - Per-table commitment source / dispatch's "r_U.comm_L.as_ref()" claim: INCONSISTENT with M.GH7.4a's authored signature. M.GH7.4a's sibling consumes `BridgedNeutronInstance` (which lacks per-table fields per Corrigendum microsoft#16 Finding D — M.GH7.4c lands envelope-struct extensions). Resolution: M.GH7.4b accepts per-table commitments as direct slice parameters (parallel to per-table polynomial slices). Envelope-Spartan FS isolation per Corrigendum microsoft#11 preserved (commitments NOT absorbed into this transcript; envelope absorbs them BEFORE squeezing the `r_logup_j` scalars passed in). Routing via `BridgedNeutronInstance` extension fields is M.GH7.4c scope; M.GH7.4b is invariant under that decision. Test coverage: - `m_gh7_4b_prove_with_T_claim_split_error_with_logup_pcs_opening_batched_round_trip`: Positive-path round-trip at fixture `num_cons=4, k=2, table_size=4`, seed `0xC1BE_5BAD_C0DE_704B`. Constructs honest per-table LogUp witnesses, commits the four PCS-opened polys, invokes prover and asserts (i) prover succeeds with the extended 3+4·k=11 PCS-opening entries, (ii) verifier accepts the proof (closes STOP-AND-ASK gates microsoft#4 + microsoft#5), (iii) β' sibling regression — `prove_with_T_claim_split_error` + `verify_with_T_claim _split_error` continue to round-trip byte-identically at the same fixture shape. 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` (2/2 ok), `test_ivc_*` family (9 passed + 1 ignored byte-identically), `test_setup` (2/2 ok). - M.GH7.0.0b: 3 tests ok (round-trip byte-equal + weighting differential 1000-iter + negative T corruption rejected). - M.GH7.3a + M.GH7.3b: 4 tests ok (`prove_step_with_lookup_fold` family). - M.GH7.4a: 4 tests ok (round-trip + degree-3 empirical close + `PerTableOuterEvals` field shape + the M.GH7.4b co-located test). LOC: ~+700 lines in `snark.rs` (verifier sibling + extended prover signature + struct field + new acceptance test + `build_per_table_commitments` helper); ~+18 lines in `sumcheck.rs` (serde derives + documentation cascade). Discharges AO 15 Tier-2 part 1 positive-path (PCS opening of `comm_L_j` against the witness `w_j` at the Spartan-FS-head per pin §3.4 + §1.2(c)). Negative-path (corrupt-`comm_L_1` test, AO 15 Tier-2 part 2) lands at M.GH7.5 per Corrigendum microsoft#16 §5.5 row M.GH7.5. 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) §5.5 row M.GH7.4b, §6.1 row M.GH7.4b, §6.3 AO 15 Tier-2 part 1 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

srinathsetty added 2 commits October 4, 2021 16:00

bump the version number for crates.io

5c179bf

srinathsetty merged commit 5829da7 into main Oct 4, 2021

srinathsetty deleted the input_checks branch October 4, 2021 23:07

asn-d6 pushed a commit to asn-d6/Nova that referenced this pull request Apr 23, 2023

Merge pull request microsoft#5 from privacy-scaling-explorations/viol…

bdcbbfa

…et/bug/test_fix Fixes a bug with the tests

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Input checks#5

Input checks#5
srinathsetty merged 2 commits into
mainfrom
input_checks

srinathsetty commented Oct 4, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

srinathsetty commented Oct 4, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant