Derive more traits. by porcuquine · Pull Request #7 · microsoft/Nova

porcuquine · 2021-10-07T23:12:11Z

This PR derives Clone, Debug, Eq, and PartialEq where possible on the R1CS structs. This makes some downstream debugging, development, and consistency checking easier.

…o/feature/dummy_test_of_parallel_prover Add dummy test for parallel prover

* refactor: removed ROConstantsTrait - trait refactored to Default in associated type, - obviates the need for a separate trait, - refactored call sites and only implementation * fix: remove uneeded Sized bounds

….8 reopen-pin (Stage 1.B-halt) Implements the §B.4 amendment (2026-05-07) closed-form prove_step / verify_step / lookup_running_claims_from per the spec, byte-for-byte where the spec is unambiguous. Adds: - src/neutron/lookup_sumcheck.rs: - LookupSumcheckInstance<E> struct (§B.4.4 fields, split-tensor eq) - new(ck, witness, table, multiplicities, eq_*, r) (§B.3 simplified per amendment; running_claims param dropped per §B.6 revised) - prove_step(rho, t_lookup_running) (§B.4.5 canonical) - compute_a/b/c_hypercube_evals helpers (§B.4.6, with the `(cell, cell, cell)` constants-in-p simplification) - verify_step(rho, r_b, poly_lookup, t_lookup_running) (§B.5 revised) - lookup_running_claims_from(U1) (§B.6 revised; single scalar) - src/spartan/logup_inverses.rs: - batch_invert_plus_r helper (§B.7; minimal extraction, no PPSNARK migration at this stage to avoid risking the row-half differential) HALT-EVIDENCE: §B.4.8 reopen-pin fires. The §B.4.5 amendment claims the resulting `poly_lookup` is degree 2 (four prover-supplied evals at {0,1,2,3} should lie on a degree-2 polynomial). Empirically, on satisfying inputs under the `(cell, cell, cell)` constants-in-p simplification of §B.4.6, the polynomial is generically degree 3. Algebraic derivation: Per §B.4.6, sum_a, sum_b, sum_c are CONSTANT in `p` pre-ρ-factor. Then for `S = sum_a + sum_b + sum_c`: e_0 = (1−ρ) · S e_2 = (3ρ−1) · S e_3 = (5ρ−2) · S Lagrange interpolation at points {0,2,3} with degree 2 gives: P(1) = e_0/3 + e_2 − e_3/3 = ((1−ρ) + 3(3ρ−1) − (5ρ−2)) · S / 3 = ρ · S But the prover supplies (per §B.4.5): e_1 = t_running − e_0 = (ρ−1) · S at outer base (t_running = 0) So `e_1 ≠ P(1)` whenever `S ≠ 0` — i.e., the four points are NOT co-degree-2 and `from_evals` produces a true degree-3 polynomial. `S` is non-zero on satisfying inputs because the (B) sub-claim sum_b = Σ eq_t · (1 − ts) is non-zero in general (Σ ts = |w|, not |T|). Cf. PPSNARK `MemorySumcheckInstance::running_claims[2]` at `ppsnark.rs:514`, which is the analogous (B)-running-claim in a multi-round reduction and is not assumed zero on satisfying inputs. Reproducible halt-evidence test: prove_step_degree_two_claim_fires_b48_reopen_pin in `src/neutron/lookup_sumcheck.rs::tests`, deterministic seed `ChaCha20Rng::seed_from_u64(0xC1BE_9E01)`. Marked `#[ignore]` to keep the green bar; runs with `cargo test ... -- --ignored` reproduces the failure (`coeffs[3] = 0x1a01..172d`, expected ZERO). Per §B.4.8 amendment language and §J open microsoft#7 (alignment correctness uncertainty), this is a soundness halt-gate trigger requiring cryptographer re-derivation. The §B.4.5 amendment is the specification under test — per `.claude/rules/cryptography.md`, the spec is the suspect, not the implementation. Halt scope: - Sub-step B (this commit): LANDED as halt-evidence; no further Stage 1 sub-step work proceeds (sub-step C/D/E/F blocked). - Inumbra HEAD: stays at `bec22a5` (§B.4 amendment); NO submodule SHA bump in this halt cycle (a SHA bump would signal progress and is incorrect under §A.6 halt discipline). Other work landed in this commit (independent of the halt): - LookupShape accessors (§B.4.3): committed at 5e9ef0c, soundness- neutral, retained. - batch_invert_plus_r: minimal helper, soundness-neutral (Lasso §6.2 / Haböck 2022 directly), unit-tested with round-trip + zero-denominator rejection. - verify_step round-trip + rejection unit tests: green, exercise the (C)-binding STRUCTURAL identity (which holds by from_evals algebra regardless of the §B.4.8 issue). Next action: orchestrator forwards this commit + the §B.4.8 evidence to the cryptographer for §B.4 re-derivation. The four-eval shape needs either: (a) a different (C)-binding formula for evals[1] that is consistent with the degree-2 claim, OR (b) acknowledgment that the closed-form is degree 3 (matching PPSNARK's MemorySumcheckInstance::degree() = 3), with a revised verifier-side eval-shape, OR (c) a different per-cell helper formulation that makes the `(cell, cell, cell)` constants-in-p simplification correct. Step-ID: C1β-spike (sub: 1-B-halt)

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

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

…_split_error sibling (factorised outer sumcheck) Introduces `RelaxedR1CSSNARK<E, EE>::prove_with_split_error` / `verify_with_split_error` sibling methods at `vendor/nova/src/spartan/snark.rs` for the GH-microsoft#7 Stage K post-IVC compressed-SNARK bridge. The sibling consumes the rank-1 factor pair `(E1, E2)` such that `W.E[i*left+j] = E2[i] * E1[j]` and the matching split-error commitments `(comm_E1, comm_E2)`, instead of consuming `W.E` and opening `U.comm_E` at a single point. Algebra (Corrigenda microsoft#7 + microsoft#8 + microsoft#9, all already ratified at superproject HEAD `a8191d0`): - Factorised outer-sumcheck identity per Corrigendum microsoft#7: `Az·Bz - u·Cz - E1_MLE(r_x_low) * E2_MLE(r_x_high)`. The lookup `gamma`-batched term is ZEROED at STAGE 0; M.GH7.4 reinstates it. - Variable-order partition per Corrigendum microsoft#9 (2-A): `r_x_high = r_x[..ell2]` (TOP `ell2` challenges → bind E2's outer index `i`); `r_x_low = r_x[ell2..]` (BOTTOM `ell1` challenges → bind E1's inner index `j`). Matches the `bind_poly_var_top` MSB-first binding semantics at `vendor/nova/src/spartan/sumcheck.rs:489-497` for the flat layout `k = i*left + j` at `vendor/nova/src/neutron/lookup_sumcheck.rs:308-322`. - Prover-side `full_E` one-shot materialisation per Corrigendum microsoft#9 (3-A): one-shot heap allocation of `Vec<E::Scalar>` of length `num_cons` (`~num_cons * 32` bytes, parallel to existing `Az`/`Bz`/`Cz` allocations). The sumcheck engine runs UNCHANGED against the flat `poly_uCz_E = U.u*Cz + full_E`; the rank-1 factorisation is enforced ONLY at the verifier via `eval_E_combined = eval_E1 * eval_E2`. - Heterogeneous batch-open via `super::batch_eval_reduce` (`vendor/nova/src/spartan/mod.rs:384-438`): three claims at different polynomial sizes — (comm_W, r_y[1..], eval_W) length 1 << (num_rounds_y - 1) (comm_E1, r_x_low, eval_E1) length left = 2^ell1 (comm_E2, r_x_high, eval_E2) length right = 2^ell2 combined via `PolyEvalInstance::batch_diff_size` / `PolyEvalWitness::batch_diff_size` (the `L_0(x_lo)` rescaling trick for heterogeneous sizes). Soundness-anchor empirical close: `m_gh7_0_0_factorisation_byte_equivalence_1000_iter` (>1000-iter ChaCha20Rng-seeded differential per `.claude/rules/cryptography.md` behavioural earned-trust threshold, ADR-0013 §4) confirms `MultilinearPolynomial::new(full_E).evaluate(&r_x) == E1_MLE(r_x[ell2..]) * E2_MLE(r_x[..ell2])` byte-for-byte across (ell1, ell2) ∈ {(1,1), (2,1), (2,2)} including the asymmetric ell1 > ell2 case. The companion `m_gh7_0_0_variable_order_partition_convention` test pins (2-A) as the correct partition by exhibiting a falsifier for the rejected (2-B) `r_x_low = r_x[..ell1]` alternative. End-to-end acceptance: `m_gh7_0_0_prove_with_split_error_factorised_outer_sumcheck_byte_equal` constructs a small satisfying `RelaxedR1CS` instance (num_cons=4, rank-1 `W.E`), invokes the new sibling on the derandomized witness and instance (per the canonical `vendor/nova/src/spartan/direct.rs:159-175` flow), and verifies. Exercises both `Bn256EngineKZG` (HyperKZG) and `PallasEngine` (IPA-PC) paths. Derandomization contract: the Spartan-side `prove_with_split_error` consumes DERANDOMIZED commitments (zero blindings) exactly like the standard `prove` — see `vendor/nova/src/spartan/direct.rs:165-166`. The Pedersen-additive binding `comm_E1 + comm_E2 == U.comm_E` per Corrigendum microsoft#8 (iv-B) is the responsibility of the M.GH7.0.2 CompressedSNARK envelope where blindings are restored, NOT this Spartan-close-only sibling. The reserved `_r_E1`/`_r_E2` parameters are pass-through for the envelope helper. Backward serialisation: `RelaxedR1CSSNARK::split_eval_E: Option<(E::Scalar, E::Scalar)>` is gated by `#[serde(default = "Option::default")]`, preserving the existing serialised proof shape verbatim. The standard `prove` body sets `split_eval_E = None`. Test results: 25 Spartan tests pass (no regression on existing `prove`/`verify` body), 157 nova-snark --lib tests pass with `--features lookup-fold` in release mode. Discharges AO 18 (partial) and AO 21 (prep). M.GH7.0.1 builds on this sibling with the Pedersen-MSM split-commit helper; M.GH7.0.2 wires it into the CompressedSNARK envelope. Anchors: - `vendor/nova/src/spartan/snark.rs:74-103` — struct field + serde - `vendor/nova/src/spartan/snark.rs:436-668` — prove_with_split_error - `vendor/nova/src/spartan/snark.rs:670-846` — verify_with_split_error - `vendor/nova/src/spartan/snark.rs:848-1166` — test module (3 tests) - `docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md` §1.2(a) (Corrigendum microsoft#7), §iv-B (Corrigendum microsoft#8), §1.3 (Corrigendum microsoft#9). Step-ID: 01-02 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…split-E commitment helper Per GH-microsoft#7 / Stage K design pin Corrigendum microsoft#8 §1.2(a). Adds a NEW `neutron::compressed_snark` module exposing `split_E_commitments`, which splits a `FoldedWitness<E>`'s flat `E: Vec<E::Scalar>` of length `structure.left + structure.right` into halves `(E1, E2)` and emits commitments `(comm_E1, comm_E2)` against disjoint prefix/suffix slices of the same flat commitment-key generator vector that the existing `commit(ck, &W.E, &W.r_E)` consumes, plus a blinding split `r_E1 + r_E2 == W.r_E`. # Soundness anchor Pedersen MSM-linearity at `vendor/nova/src/provider/pedersen.rs:285-292`: Commitment { comm: E::GE::vartime_multiscalar_mul(v, &ck.ck[..v.len()]) + <E::GE as DlogGroup>::group(&ck.h) * r, } MSM-linear over flat `ck.ck` ⇒ for `v = [E1 || E2]` of length `left + right`: MSM([E1 || E2], ck.ck[..left+right]) = MSM(E1, ck.ck[..left]) + MSM(E2, ck.ck[left..left+right]) Combined with `h*r_E1 + h*r_E2 = h*(r_E1 + r_E2) = h*W.r_E`, this gives `comm_E1 + comm_E2 == U.comm_E` whenever `r_E1 + r_E2 == W.r_E` — the Pedersen-additive identity holds by construction. Discharges AO 21 prep. # Generator-vector-alignment construction The helper calls `CE::commit(ck, v, r)` which uses `ck.ck[..v.len()]` in flat order. `comm_E1 = CE::commit(ck, E1, r_E1)` selects `ck.ck[..left]` directly. `comm_E2 = CE::commit(ck, [zeros(left) || E2], r_E2)` passes a length-(left+right) vector whose zero-prefix contributes zero to the MSM, leaving exactly `MSM(E2, ck.ck[left..left+right]) + h*r_E2`. Both halves commit against the same flat generator slice that `U.comm_E` is committed against — STOP-AND-ASK trigger 2 (generator-vector misalignment) resolves in the negative; the construction uses the public `CE::commit` API and never reaches into private `ck.ck[..]` slices. # Blinding-split discipline `r_E1` drawn fresh from `OsRng` (matching the `RecursiveSNARK::{new, prove_step}` precedent at `neutron/mod.rs:479, 550`); `r_E2 = W.r_E - r_E1`. Sum identity holds algebraically; both halves uniformly distributed in the exponent space (Pedersen hiding preserved on both halves independently — STOP-AND-ASK trigger 3 (hiding obstruction) resolves in the negative; the simpler split is sufficient and no fallback to independent fresh blindings was required). # Tests (3, within the 3-behavior × 2 = 6 budget) 1. `m_gh7_0_1_split_E_commitments_pedersen_additive_binding_byte_equal` — acceptance test asserting `comm_E1 + comm_E2 == U.comm_E` byte-equal AND `r_E1 + r_E2 == W.r_E` over a satisfying `(Structure, FoldedInstance, FoldedWitness)` triple built against `NonTrivialCircuit{num_cons=16}` (matching the `test_sat_inner` precedent at `relation.rs:942-1017`; `left = right = 4`). 2. `msm_linearity_prefix_suffix_decomposition_byte_equal_1000_iter` — 1000-iter ChaCha20Rng-seeded differential over random `(E_flat, r_E)` triples; structural identity holds for every input. 3. `blinding_split_sum_identity_independent_of_random_draw` — 8-draw sanity asserting the sum identity is preserved across distinct fresh `r_E1` values AND the random draws differ (negligible collision probability pinned). STOP-AND-ASK trigger 1 (Pedersen-additive identity divergence) resolves in the negative — the byte-equal acceptance assertion holds. # M.GH7.0.0 consumer integration The Spartan-side `prove_with_split_error` sibling at `vendor/nova/src/spartan/snark.rs` operates on DERANDOMIZED commitments (`spartan/direct.rs:159-175` derandomization precedent). This helper emits BLINDED commitments preserving `r_E1 + r_E2 == W.r_E`. The M.GH7.0.2 envelope owns the derandomize-before-Spartan-prove dance: it will call `split_E_commitments`, then `CE::derandomize` each result with `(r_E1, r_E2)`, then feed the derandomized commitments into `prove_with_split_error`. Keeping the helper blinded preserves the Pedersen-additive identity at the M.GH7.0.1 acceptance-test callsite (where `U.comm_E` is also blinded), and gives M.GH7.0.2 the information it needs to derandomize correctly. Documented in the helper docstring and module-level header. # Visibility bump `FoldedWitness::{r_W, r_E}` bumped from fully-private to `pub(crate)` so the sibling `neutron::compressed_snark` module can read them when computing the blinding split and constructing test fixtures. Co-classified with the M.GH5.1 / M.GH5.7 lookup-fold-surface visibility-bump bracket noted at `neutron/mod.rs:30-32`. # Test results cargo test --release --features lookup-fold --lib → 160 passed, 3 ignored (pre-existing), 0 failures → 3 new tests added vs. M.GH7.0.0's 157 baseline → zero regressions Pin Corrigenda microsoft#7 + microsoft#8 + microsoft#9 active; M.GH7.0a + M.GH7.0.0 landed upstream. Next: M.GH7.0.2 envelope composes this helper with `prove_with_split_error` (derandomize-before-Spartan-prove). Step-ID: 01-03 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ng prove_with_T_claim_split_error + prove_neutron_outer engine method Authored per GH-microsoft#7 / Stage K compressed-SNARK design pin Corrigendum microsoft#10 (commit c8f154c, superproject) — the NEW Spartan-side sibling that proves the *neutron-form* satisfying relation directly: sum_x full_E(x) · (Az(x) · Bz(x) − Cz(x)) = T with three structural divergences from M.GH7.0.0's `prove_with_split_error`: (a) outer-sumcheck claim = T (NOT zero) — the running NIFS sumcheck claim from FoldedInstance::T (lineage nifs.rs:519 → relation.rs:748); (b) tensor-form `(E1, E2)` weighting (vendor-grounded by lookup_sumcheck.rs:46-55 LookupSumcheckInstance::verify_step at the fold-step granularity analogue) INSTEAD OF EqSumCheckInstance built from fresh `tau` squeezes — NO `tau` is squeezed at the β' transcript; (c) residue `Az · Bz − Cz` with NO `u`-factor on Cz (Δ2 absorbed structurally — the slack lives in T, not in u). M.GH7.0.0 already-on-disk sibling at snark.rs:436-852 (commit d845468) is RETAINED VERBATIM; Corrigendum microsoft#10 ADDS a sibling, does not modify the existing one. The M.GH7.0.2 envelope routes to the new sibling instead of the old one under β'. Three production loci (per dispatch): (1) src/neutron/compressed_snark.rs: - NEW `BridgedNeutronInstance<E>` struct carrying `(comm_W, comm_E1, comm_E2, u, X, T)`, the envelope-published bridge shape the new sibling consumes. Implements TranscriptReprTrait<E::GE> mirroring RelaxedR1CSInstance's at r1cs/mod.rs:1255-1265, with `comm_E` replaced by `(comm_E1, comm_E2)` in flat concatenation order. `T` is absorbed under a distinct label `b"T_claim"` by the prover/verifier (NOT in the body) to keep the Primitive 5 binding observation explicit at audit time. (2) src/spartan/sumcheck.rs: - NEW `SumcheckProof::prove_neutron_outer(claim: T, E1, E2, Az, Bz, Cz, ts) -> (Self, r_x, (claim_Az, claim_Bz, claim_Cz, eval_E1, eval_E2))`. Mirrors `prove_cubic_with_three_inputs` at sumcheck.rs:446-507 structurally (degree-3 univariate per round, bind_poly_var_top per Corrigendum microsoft#9 (2-A), claim-per-round accumulator) but with two structural divergences: (i) tensor-form `full_E = E1 ⊗ E2` weighting instead of EqSumCheckInstance::<E>::new(taus); (ii) degree-3 residue `A · B − C` body (NO `u`-factor — Δ2 absorbed). Per Corrigendum microsoft#9 (3-A), materialises `full_E` once at the engine start (num_cons * 32 bytes parallel to existing Az/Bz/Cz allocations); rank-1 factorisation enforced ONLY at the verifier via `eval_E_combined = eval_E1 · eval_E2`. (3) src/spartan/snark.rs: - NEW `RelaxedR1CSSNARK::prove_with_T_claim_split_error` + `verify_with_T_claim_split_error` (gated on `experimental` feature because BridgedNeutronInstance lives in the `neutron` module which is `experimental`-gated; `lookup-fold` transitively enables `experimental`). FS-transcript discipline: ts.absorb(b"vk", &vk_digest) ts.absorb(b"U", U_bridged) ts.absorb(b"T_claim", &T) ← Primitive 5 binding, STRICTLY before any squeeze // NO `tau` squeeze prove_neutron_outer(T, E1, E2, Az, Bz, Cz, ts) ts.absorb(b"claims_outer", &[claim_Az, claim_Bz, claim_Cz, eval_E_combined]) // inner sumcheck + batch-eval-reduce UNCHANGED from M.GH7.0.0 Variable-order partition per Corrigendum microsoft#9 (2-A): r_x_high = r_x[..ell2] (top, binds E2); r_x_low = r_x[ell2..] (bottom, binds E1). Verifier rejects if claim_outer_final ≠ eval_E1 · eval_E2 · (claim_Az · claim_Bz − claim_Cz) — NO u-factor on Cz (Falsifier F verified-absent). Unit-test obligations discharged (3 tests within budget 6 = 2×3 behaviors, at src/spartan/snark.rs::tests::m_gh7_0_0b, gated on `experimental`): (a) `m_gh7_0_0b_prove_with_T_claim_split_error_neutron_form_round_trip_byte_equal`: Round-trip byte-equal across HyperKZG (Bn256EngineKZG) and IPA-PC (PallasEngine) at non-zero T. NOTE shape-floor: round-trip and negative tests use num_cons = 4 (matching M.GH7.0.0 precedent) — the dispatch's num_cons = 16 triggers pre-existing vendor batch_diff_size index-bounds at spartan/mod.rs:188 when chunk_size > 0 AND polynomials are heterogeneous (W.W length num_vars = num_cons vs E1/E2 lengths left/right < num_cons). The M.GH7.0.0 sibling test sized to num_cons = 4 for the same reason (chunk_size = 0 falls to the safe non-chunked branch at line 200); the algebra is identical at any (left, right) > (1, 1). (b) `m_gh7_0_0b_weighting_differential_1000_iter`: 1000-iter ChaCha20Rng-seeded byte-equal differential against `MultilinearPolynomial::new(full_E).evaluate(&r_x) == E1_MLE(r_x[ell2..]) * E2_MLE(r_x[..ell2])` across the dispatch's four shapes (2,2), (4,2), (2,4), (4,4) — Falsifier D coverage. Pure-algebra MLE comparison, independent of the batch path; covers the shape-floor gap of (a). (c) `m_gh7_0_0b_negative_T_corruption_rejected`: T' = T + 1 injected at verify time. Verifier rejects per Primitive 5 binding — `claim_outer_final` reconstruction fails because the FS transcript diverges as soon as `b"T_claim"` is absorbed with the wrong value. Falsifier audit at dispatch (per Corrigendum microsoft#10 §4): - Falsifier C (bind-poly-var-top vs bind-poly-var-bottom): NOT FIRED — `prove_neutron_outer` calls `bind_poly_var_top(&r_i)` per round on all four polynomials, mirroring sumcheck.rs:489-497 verbatim. - Falsifier D (tensor-form weighting divergence vs flat full_E): NOT FIRED — 1000-iter differential PASS across (2,2), (4,2), (2,4), (4,4) at both Bn256EngineKZG and PallasEngine. The engine's debug_assert_eq! at end-of-sumcheck additionally checks `poly_E[0] == eval_E1 * eval_E2` byte-equal. - Falsifier E (r_U.T post-IVC inconsistent with running claim closed during fold): NOT FIRED — re-verified at dispatch time that nifs.rs:519 computes `T_out = poly.evaluate(&r_b) * eq_rho_r_b.invert()` and relation.rs:748 sets `T: *T_out` in U1.fold()'s return. No intermediate reassignment of T elsewhere in the IVC layer. - Falsifier F (Δ2 re-emergence — u-factor on Cz at the outer sumcheck): NOT FIRED — both `prove_neutron_outer` and `verify_with_T_claim_split_error` use residue `Az·Bz − Cz` (NO u-scaling). The inner sumcheck's `claim_inner_joint = claim_Az + r·claim_Bz + r²·claim_Cz` also has no u-scaling — `u` enters only via `z = [W.W, u, X]` per snark.rs:765-774's `eval_X` reconstruction, byte-identical to M.GH7.0.0. Test count delta: 160 → 163 (+3 / 160) under `cargo test --release --features lookup-fold -p nova-snark --lib`. No regressions. Discharges AO 18 partial + AO 21 prep. Anchored at: pin §5.5 row M.GH7.0.0b + Corrigendum microsoft#10 §1.2(a) + §4. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…_commitments returns SplitECommitments three-commitment struct per Corrigendum microsoft#11 Per GH-microsoft#7 / Stage K design pin Corrigendum microsoft#11 (commit 40b17cd, superproject). Reworks the Corrigendum-microsoft#8-only `split_E_commitments` helper (vendor commit 5cbc0e9) from a 4-tuple `(Commitment<E>, Commitment<E>, E::Scalar, E::Scalar)` return shape to a `SplitECommitments<E>` struct carrying THREE commitments and THREE blinding factors, breaking the basis-collision diagnosed at the M.GH7.0.2-attempt-2 GREEN halt (STOP-AND-ASK gate A; execution-log 2026-05-11T16:31:00Z). # What changes (signature + body) New `SplitECommitments<E>` struct (carrying the three commitments + three blindings in disciplined roles): comm_E1 = MSM(E1, ck.ck[..left]) + h · r_E1 (BOTH binding AND Spartan PCS at r_x_low — no basis divergence on E1) comm_E2_bind = MSM(E2, ck.ck[left..left+right]) + h · r_E2_bind (suffix-basis; ONLY off-FS Pedersen-additive binding) comm_E2_pcs = MSM(E2, ck.ck[..right]) + h · r_E2_pcs (prefix-basis; ONLY Spartan PCS opening at r_x_high) Blinding-split discipline: - r_E1 + r_E2_bind == W.r_E (preserves Corrigendum microsoft#8 (iv-B) on the binding side verbatim) - r_E2_pcs is FRESH-INDEPENDENT from OsRng (does NOT enter the binding identity; the Σ-protocol at M.GH7.0.1b ties comm_E2_bind and comm_E2_pcs together at the algebraic value of E2) The helper signature changes accordingly: pub fn split_E_commitments<E: Engine>( ck: &CommitmentKey<E>, W: &FoldedWitness<E>, _U: &FoldedInstance<E>, structure: &Structure<E>, ) -> SplitECommitments<E> where E::GE: DlogGroup # Why three commitments (Corrigendum microsoft#11) The pre-Corrigendum-microsoft#11 single `comm_E2` had to serve two disjoint contracts simultaneously: (1) off-FS Pedersen-additive binding `comm_E1 + comm_E2 == U.comm_E` requires the suffix basis `ck.ck[left..left+right]`; (2) Spartan-sibling PCS opening at r_x_high requires the prefix basis `ck.ck[..right]` (HyperKZG EE::verify at hyperkzg.rs:1080-... and IPA-PC EE::verify at ipa_pc.rs:286-... both consume Commitment<E> against ck.ck[..v.len()] — no API for non-prefix slices). These are distinct group elements in general. Emitting both (comm_E2_bind, comm_E2_pcs) lets each contract consume its required shape; the Σ-protocol at M.GH7.0.1b (next milestone) ties them at the algebraic value of E2. # Soundness anchors Binding side (unchanged from Corrigendum microsoft#8): - Pedersen-1991 MSM-linearity at provider/pedersen.rs:285-292 - Zero-padded-vector trick for suffix-basis MSM via CE::commit PCS side (NEW per Corrigendum microsoft#11): - Standard prefix-basis Pedersen commit via CE::commit(ck, E2, &r_E2_pcs) selects ck.ck[..right] directly (provider/pedersen.rs:285-292) - This is the canonical contract consumed by HyperKZG EE::verify (provider/hyperkzg.rs:1080-...) and IPA-PC EE::verify (provider/ipa_pc.rs:286-...) # Test rework The three existing M.GH7.0.1 tests are re-authored at the new signature (NOT deleted — the binding-side algebra is preserved verbatim, only the helper API shape changes): 1. m_gh7_0_1_split_E_commitments_three_commitments_pedersen_additive_binding_byte_equal (acceptance test renamed per dispatch — adds the (3) PCS-basis assertion: comm_E2_pcs == CE::commit(ck, E2, r_E2_pcs)) 2. msm_linearity_prefix_suffix_decomposition_byte_equal_1000_iter (1000-iter differential — adds the PCS-side shape check comm_E2_pcs == MSM(E2, ck.ck[..right]) + h · r_E2_pcs alongside the binding-side identity) 3. blinding_split_sum_identity_independent_of_random_draw (now also asserts r_E2_pcs is fresh-random across calls — pins OsRng-actually-used for the PCS-side blinding) NEW Falsifier-I test (1000-iter): 4. falsifier_i_r_E2_pcs_independent_from_r_E2_bind_1000_iter (asserts r_E2_pcs != r_E2_bind on every iteration — surfaces the RNG-misuse failure mode where the helper reuses the same OsRng draw for both, which would collapse Corrigendum microsoft#11's basis-collision break and trivially satisfy the Σ-protocol) # Test count delta cargo test --release -p nova-snark --features lookup-fold --lib: baseline (HEAD = 893fc70): 163 passed / 3 ignored / 0 failed rework HEAD: 164 passed / 3 ignored / 0 failed delta: +1 net new passing test cargo test --release -p nova-snark --features lookup-fold (all targets): 166 passed / 8 ignored / 0 failed across 2 suites The 3 original M.GH7.0.1 tests are renamed-and-re-authored, not added; the +1 net delta is the new Falsifier-I independence test. Zero regressions across the full nova-snark sweep. # STOP-AND-ASK falsifiers verified-absent - Pedersen-additive identity divergence under blinding-split: verified by the acceptance test (assertion 1) + 1000-iter differential. PASS. - Falsifier I (r_E2_pcs == r_E2_bind RNG-misuse): verified by the new 1000-iter independence test. PASS on every iteration (zero collisions). - Locus deviation: helper remains at vendor/nova/src/neutron/compressed_snark.rs as required by the dispatch. No compile-cascade pressure to move it. # What is NOT in this commit - BridgedNeutronInstance::comm_E2 field rename to comm_E2_pcs — this is M.GH7.0.2 REWIRE scope (step 01-04 re-execution per Corrigendum microsoft#11). The struct's docstring narrative is touched minimally to forward-reference the upcoming rewire; the field name remains comm_E2 for now. - Σ-protocol equality-of-opening helper SigmaE2EqualityProof / prove_sigma_E2_equality / verify_sigma_E2_equality — this is M.GH7.0.1b scope (step 01-03b NEW per Corrigendum microsoft#11). - Envelope CompressedSNARK<E, EE> body rewire — this is M.GH7.0.2 REWIRE scope. # References - Pin: docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md §0 Corrigendum microsoft#11 + §1.2(a) append + §5.5 row M.GH7.0.1 + §6.2 Pass Criterion microsoft#9 - Roadmap: docs/feature/microsoftgh-7-stage-k-compressed-snark/deliver/roadmap.json step 01-03 (criteria authoritative) - Superseded vendor commit: 5cbc0e9 (Corrigendum-microsoft#8-only helper) - Soundness anchors: provider/pedersen.rs:285-292 (Pedersen MSM linearity); provider/hyperkzg.rs:1080-... (HyperKZG EE::verify prefix-basis); provider/ipa_pc.rs:286-... (IPA-PC EE::verify prefix-basis) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…f-opening prove + verify per Corrigendum microsoft#11 NEW Σ-protocol primitive (Corrigendum microsoft#11 Primitive 6) closing the basis-collision between `comm_E2_bind` (suffix basis, off-FS Pedersen- additive binding side) and `comm_E2_pcs` (prefix basis, Spartan-sibling PCS-opening side) emitted by the M.GH7.0.1 REWORKED helper. Asserts the two commitments open to the same algebraic E2 ∈ F^{right} under different bases via a Fiat-Shamir-NIZK transformation of Schnorr 1989 + Cramer-Damgård-Schoenmakers 1994 + Maurer 2009 generalised one-shot Σ-protocol for linear relations over two group-homomorphisms sharing a witness. # Three new symbols at vendor/nova/src/neutron/compressed_snark.rs - `SigmaE2EqualityProof<E: Engine>` struct (Serialize + Deserialize) carrying (T_bind, T_pcs, z, z_r_bind, z_r_pcs). - `prove_sigma_E2_equality<E: Engine>(ck, structure, E2, r_E2_bind, r_E2_pcs, comm_E1, comm_E2_bind, comm_E2_pcs, r_U_comm_E, &mut transcript) -> Result<SigmaE2EqualityProof<E>, NovaError>` prover; samples (ρ, σ_bind, σ_pcs) from OsRng, computes T_bind via the existing zero-padded suffix-basis trick (mirroring lines 436-438 of split_E_commitments) and T_pcs via canonical CE::commit prefix basis, absorbs (r_U_comm_E, comm_E1, comm_E2_bind, comm_E2_pcs, sigma_T_bind, sigma_T_pcs) in fixed order per pin §1.2(a) lines 259-265, squeezes α under b"sigma_E2_equality_alpha", emits responses z = ρ + α·E2, z_r_bind = σ_bind + α·r_E2_bind, z_r_pcs = σ_pcs + α·r_E2_pcs. - `verify_sigma_E2_equality<E: Engine>(ck, structure, comm_E1, comm_E2_bind, comm_E2_pcs, r_U_comm_E, &proof, &mut transcript) -> Result<(), NovaError>` verifier; re-derives α from same absorb order, checks (a) MSM(z, suffix) + h·z_r_bind == T_bind + α·comm_E2_bind via zero-padded trick AND (b) CE::commit(ck, &z, &z_r_pcs) == T_pcs + α·comm_E2_pcs; rejects with NovaError::ProofVerifyError reasons "Sigma E2 equality-of-opening rejected at bind-side" / "pcs-side" / structural-length-mismatch. # Transcript-isolation discipline (pin §1.2(a) Falsifier H) The envelope-side transcript MUST be initialised by the caller with b"NeutronCompressedSNARK_envelope" — distinct from the Spartan sibling's b"RelaxedR1CSSNARK". The helper itself is domain-sep- agnostic at the API surface; the FS-isolation discipline lives at the caller (M.GH7.0.2's prove_from_parts / verify). The vk_digest absorb is the caller's responsibility — pin §1.2(a) line 258 places it BEFORE the helper's absorb sequence. # Falsifier J guard (vector arithmetic truncation) Prover asserts E2.len() == structure.right BEFORE sampling ρ; verifier rejects with NovaError::ProofVerifyError if proof.z.len() != structure.right BEFORE reaching the group equation. Mismatched lengths would otherwise produce a silently-accepted forge against a forged comm_E2_*. # Tests (5 behaviors × 2 budget = 10; 2 test functions consolidate) - m_gh7_0_1b_sigma_E2_equality_round_trip_and_negative_byte_equal: (a) honest prove → verify round-trip; (c) negative E2'-forgery against comm_E2_pcs (E2[0] += ONE) — verifier rejects at pcs-side or bind-side equation; (d) negative α-substitution forge (responses constructed under α' = α + ONE with same first-message (T_bind, T_pcs); verifier squeezes α from transcript and rejects); (e) negative FS-isolation forge (prover uses b"RelaxedR1CSSNARK" domain separator; verifier uses b"NeutronCompressedSNARK_envelope"; α_prover ≠ α_verifier; verifier rejects). Empirical close for Falsifier H. - m_gh7_0_1b_sigma_E2_equality_round_trip_1000_iter: ChaCha20Rng [1u8;32] deterministic-seeded 1000-iter round-trip at fixed shape (left = right = 4) per .claude/rules/cryptography.md threshold + US-05 reviewer-reproducibility. Tests enter through the helper's pure-function driving ports (prove_sigma_E2_equality, verify_sigma_E2_equality are their own driving ports per Mandate 2 — function signature IS the public interface). No mocks inside hexagon. Helpers AND tests live in the same file by dispatch's authoritative locus. # Test count delta vs M.GH7.0.1 REWORKED tip (commit ed41d12) - --release --features lookup-fold --lib: 164 → 166 (+2) - --release --features lookup-fold (all targets, 2 suites): 166+0=166 → 166+2=168 (+2 on lib suite; integration unchanged at 2) - 3 ignored / 8 ignored unchanged; 0 failed. # STOP-AND-ASK Falsifier outcomes — NONE FIRED - G (Σ-protocol soundness regression under composition with Pedersen- additive binding): verified-absent at algebra level (binding constrains BLINDING fields r_E1 + r_E2_bind == W.r_E; Σ-protocol constrains E2 field-value identity across two opening bases — disjoint contracts). 1000-iter differential GREEN confirms no cross-contamination. - H (envelope-side and Spartan-side transcripts share state): empirical close via test case (e) FS-isolation negative; production helper takes &mut E::TE so each caller passes its own instance. - J (vector arithmetic truncation on z = ρ + α·E2): prover assert at top + verifier length check at top guard the truncation surface; did not fire under any test shape. # Soundness anchors - Schnorr 1989 (CRYPTO '89) — original discrete-log identification. - Cramer-Damgård-Schoenmakers 1994 (CRYPTO '94 §3) — Σ-protocol special-soundness analysis under parallel composition. - Maurer 2009 (Africacrypt 2009 §4) — generalised one-shot protocol for linear relations over arbitrary group-homomorphisms f_1, f_2 : F^n → G with shared witness. - Pedersen 1991 — MSM linearity at provider/pedersen.rs:285-292 (vendor-verified). - Fiat-Shamir-NIZK soundness bound ≤ 2^{-128} for the keccak transcript at the workspace threat-model level. # Discharges Corrigendum microsoft#11 §1.2(a) Primitive 6 authored at the envelope layer. §6.2 Pass Criterion microsoft#9 honest-prover acceptance + injected-E2'-forgery rejection empirical close at the algebra level (the STAGE 0 end-to-end empirical close still owed at M.GH7.0.3 via Bn256EngineKZG + HyperKZG happy-path). AO 21 prep (envelope-level commitment-equality primitive for the bridge reduction). Pin §5.5 row M.GH7.0.1b. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…K envelope T-form bridge integration with Σ-protocol equality binding Authors `neutron::CompressedSNARK<E, EE>` envelope at `vendor/nova/src/neutron/compressed_snark.rs` per GH-microsoft#7 / Stage K design pin Corrigenda microsoft#8 + microsoft#10 + microsoft#11 REWIRE. Composes the M.GH7.0.0b Spartan T-claim sibling (`prove_with_T_claim_split_error` / `verify_with_T_claim_split_error`), the M.GH7.0.1 REWORKED three-commitment helper (`split_E_commitments → SplitECommitments<E>`), and the M.GH7.0.1b Σ-protocol equality-of-opening helper (`prove_sigma_E2_equality` / `verify_sigma_E2_equality`) into a single-curve 2-parameter envelope. # Surface pub struct CompressedSNARK<E, EE> { pub U_bridged: BridgedNeutronInstance<E>, pub r_U_derand_comm_E: Commitment<E>, pub comm_E2_bind: Commitment<E>, pub sigma_E2_equality: SigmaE2EqualityProof<E>, pub snark_spartan: RelaxedR1CSSNARK<E, EE>, pub zn: Vec<E::Scalar>, } pub struct ProverKey<E, EE> { pk_spartan } pub struct VerifierKey<E, EE> { vk_spartan, dk, F_arity, structure, ck } CompressedSNARK::setup(pp) -> (ProverKey, VerifierKey) CompressedSNARK::prove(pp, pk, recursive_snark) -> Self CompressedSNARK::verify(&self, vk, _num_steps, _z0, zn) -> Vec<E::Scalar> # Field-rename (Corrigendum microsoft#11) `BridgedNeutronInstance.comm_E2` → `comm_E2_pcs`. The pre-Corrigendum-microsoft#11 field was suffix-basis and could not simultaneously serve the off-FS binding identity AND the Spartan PCS-opening shape (those need different generator slices). Per Corrigendum microsoft#11 the envelope now ships three commitments: `comm_E1` (prefix-basis, dual-use), `comm_E2_bind` (suffix-basis, binding only — held separately on `CompressedSNARK`), `comm_E2_pcs` (prefix-basis, PCS-opening only — held on `BridgedNeutronInstance`). The Σ-protocol equality-of-opening proof ties `comm_E2_bind` and `comm_E2_pcs` at the algebraic value of `E2`. Rename is byte-stream-length-preserving in `to_transcript_bytes` (same field order, same field types). Single consumer at `spartan/snark.rs` `bridged_from` test helper updated. # Visibility bumps Co-classified with M.GH7.0.1 `FoldedWitness::{r_W, r_E}` bracket (`relation.rs:233/245`) and the M.GH5.1 / M.GH5.7 lookup-fold-surface bracket (`neutron/mod.rs:30-32`). Vendor-side only; no inumbra surface impact. - `neutron::RecursiveSNARK::{r_U, r_W, zi}` → `pub(crate)` - `neutron::PublicParams::{F_arity, ro_consts, ck, structure}` → `pub(crate)` - `spartan::snark::ProverKey::vk_digest` → `pub(crate)` # Prove flow (Corrigendum microsoft#10 + microsoft#11) 1. `split_E_commitments(ck, r_W, r_U, structure)` → `SplitECommitments { comm_E1, comm_E2_bind, comm_E2_pcs, r_E1, r_E2_bind, r_E2_pcs }`. 2. Bridge `(FoldedWitness, FoldedInstance) → (RelaxedR1CSWitness, RelaxedR1CSInstance)` by field-copy. 3. `RelaxedR1CSWitness::derandomize()` + `RelaxedR1CSInstance:: derandomize(&dk, &blind_W, &blind_E)` (mirror of `vendor/nova/src/nova/mod.rs:841-848`). 4. `E::CE::derandomize` on all three split-E commitments. Pedersen- additive identity preserved at derandomized layer because the `h·r` term is stripped symmetrically: comm_E1_derand + comm_E2_bind_derand = MSM(E1, ck[..left]) + MSM(E2_pad, ck[..left+right]) = MSM([E1||E2], ck[..left+right]) = r_U_derand.comm_E. 5. Initialise envelope-side transcript with the FS-isolation domain separator `b"NeutronCompressedSNARK_envelope"`. Absorb `vk_digest` under `b"vk"` per pin §1.2(a) Primitive 6 line 258. 6. `prove_sigma_E2_equality(..., r_E2_bind = 0, r_E2_pcs = 0, ...)` with the DERANDOMIZED commitments. Zero blindings match the derandomized published commitments (h·r terms stripped). Helper continues the absorb sequence (`b"r_U_comm_E"` → `b"comm_E1"` → `b"comm_E2_bind"` → `b"comm_E2_pcs"` → `b"sigma_T_bind"` → `b"sigma_T_pcs"` → squeeze `b"sigma_E2_equality_alpha"`). 7. Build `U_bridged = BridgedNeutronInstance { comm_W_derand, comm_E1_derand, comm_E2_pcs_derand, u, X, T }`. 8. `RelaxedR1CSSNARK::prove_with_T_claim_split_error(ck, &pk_spartan, &structure.S, &U_bridged, &W_derand, comm_E1_derand, comm_E2_pcs_derand, &E1, &E2, T, ZERO, ZERO)`. Sibling owns its own fresh `b"RelaxedR1CSSNARK"` transcript at entry — FS-isolated from the envelope-side transcript at the dom-sep stage (Falsifier H structurally absent). # Verify flow (Corrigenda microsoft#8 + microsoft#10 + microsoft#11) (1) Off-FS Pedersen-additive binding check (Corrigendum microsoft#8 (iv-B)): `comm_E1 + comm_E2_bind == r_U_derand_comm_E` at the group level. Reject with reason "off-FS Pedersen-additive binding rejected". (2) Σ-protocol equality-of-opening verify (Corrigendum microsoft#11 Primitive 6): build FRESH `E::TE` at SAME `b"NeutronCompressedSNARK_envelope"` dom-sep + SAME `b"vk"` absorb of `vk.vk_spartan.digest()`. Invoke `verify_sigma_E2_equality(...)`. Helper-side rejections ("Sigma E2 equality-of-opening rejected at bind-side" / "...pcs-side") propagate up. (3) Spartan T-claim sibling verify (Corrigendum microsoft#10): delegate to `verify_with_T_claim_split_error(&vk_spartan, &U_bridged, comm_E1, comm_E2_pcs)`. Sibling owns its own `b"RelaxedR1CSSNARK"` transcript (FS-isolation enforced at snark.rs:1149). (4) IVC final state check: `zn == self.zn` against caller-supplied. # Sub-GREEN-halt diagnosis (resolved without STOP-AND-ASK) First `cargo test --release` run rejected the honest round-trip with `ProofVerifyError { reason: "Sigma E2 equality-of-opening rejected at bind-side" }`. Root cause: blinding-consistency mismatch — the original sketch passed `(r_E2_bind, r_E2_pcs)` from the M.GH7.0.1 REWORKED helper to `prove_sigma_E2_equality` while publishing DERANDOMIZED commitments. The Σ-protocol bind-side equation MSM(z, ck.ck[left..left+right]) + h·z_r_bind == T_bind + α·comm_E2_bind requires the published `comm_E2_bind` to be a commit-with-blinding- `r_E2_bind` Pedersen value, but the derandomized commitment has zero effective blinding. LHS exceeded RHS by `α·h·r_E2_bind` deterministically on honest inputs. Fix: pass `ZERO` blindings to `prove_sigma_E2_equality` to match the derandomized commitments. Co-applied to the Spartan sibling call (formal params underscored in body; ZERO matches M.GH7.0.0b sibling test pattern at `snark.rs:1822-1823`). NOT a STOP-AND-ASK gate trigger: gate A specifically calls out the OFF-FS BINDING check rejecting honest prover (helper or derandomize- dance asymmetry). The rejection here was on the Σ-protocol bind-side, a different equation, with a mechanically clear root cause and a fix that preserves all algebra: off-FS binding still holds at the derandomized layer because derandomize strips h·r symmetrically. Documented inline in `prove_from_parts` step (6) for reviewer traceability. # Falsifiers verified-absent - A (off-FS binding rejecting honest prover): not fired — honest round-trip and 1000-iter differential GREEN. - H (envelope/Spartan transcript shared state): structurally absent — envelope-side transcript `b"NeutronCompressedSNARK_envelope"` NEVER threaded into the Spartan sibling; sibling owns its own `b"RelaxedR1CSSNARK"` transcript at `snark.rs:944/1149`. - Σ-protocol absorption-order deviation: not fired — envelope's `b"vk"` prefix-absorb matches pin §1.2(a) line 258; helper-internal absorb order matches docstring lines 656-662. - T_claim absorb-before-squeeze: not fired — envelope NEVER absorbs T into its own transcript; the T_claim absorb is owned by the Spartan sibling at `snark.rs:954`. - Type-cascade beyond compressed_snark.rs: rename `comm_E2 → comm_E2_pcs` cascaded ONLY to the `bridged_from` test helper at `snark.rs:1773` (one-line field-init update) as expected. # Test results cargo test --release -p nova-snark --features lookup-fold --lib m_gh7_0_2: 2 passed / 0 failed / 169 filtered (15.66s) cargo test --release -p nova-snark --features lookup-fold --lib: 168 passed / 3 ignored / 0 failed (163.70s) DELTA: +2 vs baseline 166 (M.GH7.0.1b) cargo test --release -p nova-snark --features lookup-fold (all targets): 170 passed / 8 ignored / 0 failed across 2 suites (184.29s) DELTA: +2 vs baseline 168 (M.GH7.0.1b) Zero regressions. 1000-iter ChaCha20Rng-seeded differential at `(left, right) = (2, 2)` GREEN — per `.claude/rules/cryptography.md` behavioral earned-trust threshold. # Test coverage m_gh7_0_2_compressed_snark_envelope_off_fs_pedersen_binding_and_sigma_E2_equality (acceptance + 1000-iter differential): - honest prove → verify round-trip returns Ok(zn); - INDEPENDENT structural assertion of Pedersen-additive binding at the group level (NOT just inside verify happy-path); - 1000-iter ChaCha20Rng differential per US-05 reviewer- reproducibility. m_gh7_0_2_compressed_snark_envelope_rejects_corrupted_binding_and_sigma (composite negative): - off-FS binding check: perturb `comm_E2_bind` by +δ, assert verify rejects with "off-FS Pedersen-additive binding rejected"; - Σ-protocol check: perturb `sigma_E2_equality.z[0]` by +ONE, assert verify rejects with "Sigma E2 equality-of-opening rejected at bind-side" or "...pcs-side". Shape floor `left = right = 2, num_cons = 4` — sidesteps the pre-existing vendor `batch_diff_size` panic at `spartan/mod.rs:175-189` (`chunk_size = 0` heterogeneous polynomials case). Same shape choice as the M.GH7.0.0b sibling test at `snark.rs:1797-1810` for the same reason. Cross-shape coverage at the algebra layer is provided by M.GH7.0.1 REWORKED's `msm_linearity_prefix_suffix_decomposition_*` and M.GH7.0.1b's `m_gh7_0_1b_sigma_E2_equality_round_trip_1000_iter`. # Discharges - Corrigendum microsoft#8 (iv-B) — off-FS Pedersen-additive binding enforced at the envelope (LOAD-BEARING; load-bearing-status pinned by the perturbation negative test). - Corrigendum microsoft#10 §1.2(a) β′ — bridge architecture composing the Spartan T-claim sibling under the envelope's derandomize-then-prove discipline. - Corrigendum microsoft#11 §1.2(a) Primitive 6 — Σ-protocol equality-of-opening binding `comm_E2_bind` ↔ `comm_E2_pcs` at the algebraic value of E2. The §6.2 Pass Criterion microsoft#9 STAGE-0 empirical close (HyperKZG end-to- end) lands at M.GH7.0.3. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ogeneous-size chunked-path fix per Corrigendum microsoft#12 PolyEvalWitness::batch_diff_size at vendor/nova/src/spartan/mod.rs:166-230 promises zero-pad-to-size_max semantics for heterogeneous-length input polynomials (docstring lines 166-171). The non-chunked fallback (lines 200-227) correctly implements this via `vec![ZERO; size_max]` + length-aware accumulation. The chunked fast path (lines 180-199) did not: it indexed `poly.p[chunk_index * chunk_size..]` unconditionally, panicking with "range start index N out of range for slice of length M" whenever a smaller polynomial's length did not extend to the chunk's start offset. Trigger condition: any caller of batch_eval_reduce (snark.rs:255, snark.rs:658, snark.rs:1098) supplying witnesses with size_max >= num_chunks (`rayon::current_num_threads().next_power_of_two()`) AND any input shorter than size_max. On an M-class macOS host (num_chunks=16), shapes like [16, 4, 4] reach chunks at byte offsets 4..15 of the length-4 polynomials — panic at line 188. Fix: option β per Corrigendum microsoft#12 — replace `poly.p[chunk_index * chunk_size..]` with `poly.p.get(chunk_index * chunk_size..).unwrap_or(&[])`. Chunks past a smaller polynomial's end yield empty iterators (the `chunk` accumulator already holds zeros, so the contribution from that polynomial in this chunk is correctly 0 — exactly the zero-pad semantic the docstring promises). Chunks straddling the boundary use natural `.zip` truncation on the per-element pair iterator (already correct in the prior code; preserved verbatim). Soundness preservation argument (per Corrigendum microsoft#12 ratification by Halpert): zero-padding a polynomial with trailing zeros is a no-op on (i) inner-product / MLE evaluation at any point (the contributions at indices >= original length are zero · anything = zero) and (ii) commitment under any linear PCS used in this stack (Pedersen, KZG, HyperKZG — the commitment of a zero-padded polynomial equals the commitment of the original polynomial, since the extra basis elements are scaled by zero scalars). The chunked path's RLC accumulation `chunk[k] += coeff · poly.p[chunk_offset + k]` therefore must read the value as zero whenever `chunk_offset + k >= poly.p.len()` — which the bounds-safe substitution achieves structurally. Why options α (pre-padding inside the chunked branch) and γ (force the non-chunked branch unconditionally) were rejected at Corrigendum microsoft#12: option α imposes O(N) allocation per chunk to pre-pad each smaller polynomial up to size_max, defeating the purpose of the chunked fast path; option γ regresses the homogeneous-size fast path that the existing batch() helper at lines 232-285 deliberately preserves. Option δ (pre-pad at the three batch_eval_reduce call sites) was rejected on locus grounds: the contract is owned by batch_diff_size's docstring, the fix must live where the contract is asserted, not in each consumer. Regression test: batch_diff_size_tests::m_gh7_0_2c_batch_diff_size_heterogeneous_size_zero_pad_byte_equal at src/spartan/mod.rs. Constructs heterogeneous input [16, 4, 4] (size_max=16 forces chunk_size>=1 on any reasonable num_chunks <= 16), sweeps 1000 ChaCha20Rng-seeded iterations (US-05 reviewer-reproducibility), asserts byte-equality of the chunked path's output against an explicit zero-pad-then-RLC reference. Parametrised across both production curve families: Bn256EngineKZG (HyperKZG path) and PallasEngine (IPA-PC path). PRE-FIX: panics at vendor/nova/src/spartan/mod.rs:188:26 with "range start index N out of range for slice of length 4" across all 16 threads. POST-FIX: 1000-iter differential GREEN on both engines. Cascade verification (the three prior milestone acceptance tests must still pass; the existing tests use uniform-size input shapes — left=right=2, all witnesses length 4 — but the fix's substitution is byte-equivalent to the old indexing on every k < poly.p.len(), so byte-equality is preserved on homogeneous shapes too): - m_gh7_0_0_prove_with_split_error_factorised_outer_sumcheck_byte_equal: PASS - m_gh7_0_0b_prove_with_T_claim_split_error_neutron_form_round_trip_byte_equal: PASS - m_gh7_0_2_compressed_snark_envelope_off_fs_pedersen_binding_and_sigma_E2_equality: PASS - m_gh7_0_2_compressed_snark_envelope_rejects_corrupted_binding_and_sigma: PASS Full --release --features lookup-fold --lib sweep: 169 passed / 3 ignored / 0 failed (delta +1 vs baseline 168 — the new regression test). Full --release --features lookup-fold all-targets sweep: 171 passed / 8 ignored / 0 failed across 2 suites (delta +1 vs baseline 170). Zero regressions. batch_eval_reduce call-site audit (verify-don't-assume per dispatch): the three existing consumers at spartan/snark.rs:255, :658, :1098 all assert `w.p.len() == 1 << num_rounds` at batch_eval_reduce's entry (line 408 of spartan/mod.rs in this file) with `num_rounds` derived per-instance from the caller's `u_vec`, so the existing call sites currently feed homogeneous-size shapes and the bug did not surface in any prior test. A future fourth consumer that feeds heterogeneous shapes (e.g., at M.GH7.4) is now safe by construction. STOP-AND-ASK gates per roadmap step 01-04c criteria — NONE FIRED: - byte-divergence between fixed chunked path and reference: not observed (1000-iter differential GREEN byte-for-byte). - implementation deviation from option β: not observed (the substitution is a literal one-line change to the existing indexing expression; no pre-padding introduced inside the chunked branch or at call sites). - fourth batch_eval_reduce call site emerging in this milestone: confirmed N/A — `grep -n "batch_eval_reduce" vendor/nova/src/spartan/snark.rs` returns exactly the three known sites (lines 255, 658, 1098). Discharges Corrigendum microsoft#12 disposition (option β bounds-safe substitution at chunked-path locus). Pin §5.5 row M.GH7.0.2c empirically closed.

…erifierKey polish per pin §3.3 Type-signature finalisation for `neutron::compressed_snark` per the authoritative GH-microsoft#7 Stage K design pin §3.3 (lines 1212-1336 at `docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md`). M.GH7.0.2 (commit cb275be) authored the envelope's setup/prove/verify body and the M.GH7.0.2c batch_diff_size fix (commit ab4c524) closed the heterogeneous-size chunked-path; this M.GH7.1 polish extends the verifier-key surface to the pin's full named field set. ## Scope per roadmap step 01-08 + dispatch This commit is the vendor-side half of the two-commit discipline. It contains: (1) VerifierKey<E, EE> extended with four pin-§3.3 fields: - F_arity: usize (already present, reordered) - ro_consts: RO2Constants<E> (NEW; sourced from pp.ro_consts.clone()) - pp_digest: E::Scalar (NEW; sourced from pp.digest()) - lookup_fold_k: usize (NEW; sourced from pp.lookup_fold_k under feature = "lookup-fold") - shape_registry_digest: E::Scalar (NEW; ZERO at STAGE 0 / non-lookup-fold default) The M.GH7.0.2 pragmatic fields (dk, structure, ck) are retained under pin §3.3's `...` trail — they are load-bearing for the off-FS Pedersen-additive binding check and the Σ-protocol equality-of-opening verifier. Relocating them would change the verify_sigma_E2_equality signature, which is non-mechanical algebra-touching change and out of M.GH7.1 scope ("no new algebra; this is type-signature finalisation"). Pin §5.5 row M.GH7.1 closes at type-finalisation level; M.GH7.2 / M.GH7.4 will wire the authoritative shape_registry digest construction binding the M.7 shape-registry assertion. (2) ProverKey<E, EE> unchanged. Pin §3.3 lines 1312-1315 name only pk_spartan + `...` trail; the polish is on the verifier side. (3) CompressedSNARK::setup body extended to populate the new fields. cfg-gates on lookup_fold_k match the cfg-gates on the corresponding PublicParams field at neutron/mod.rs:130-132. (4) PublicParams visibility bumps on shape_registry + lookup_fold_k (private → pub(crate)) so the sibling compressed_snark module can read them at setup. Co-classified with the M.GH7.0.2 visibility bumps on F_arity / ro_consts / ck / structure (neutron/mod.rs:91-105 visibility bracket). (5) Module export hygiene at neutron/mod.rs: pub use compressed_snark::{ BridgedNeutronInstance, CompressedSNARK, ProverKey as CompressedSNARKProverKey, SigmaE2EqualityProof, SplitECommitments, VerifierKey as CompressedSNARKVerifierKey } with #[doc(inline)]. Renamed VK/PK exports because the `nova::CompressedSNARK` precedent at nova/mod.rs already exposes {ProverKey, VerifierKey} at the `nova::` module root, and an un-renamed `pub use compressed_snark::ProverKey` would collide on the rare-but-possible glob-import path. Fully-qualified `neutron::compressed_snark::CompressedSNARK` continues to work unchanged — the harness-side imports at `crates/inumbra-spend-harness/tests/gh7_stage_k_compressor.rs:106` do not need modification. (6) New typecheck test m_gh7_1_compressed_snark_prover_key_verifier_key_typecheck_both_ees in the in-crate test module. Structural typecheck only — invokes PublicParams::setup + CompressedSNARK::setup at BOTH production EE choices (HyperKZG via Bn256EngineKZG + provider::hyperkzg, IPA-PC via Bn256EngineIPA + provider::ipa_pc) on the TrivialCircuit / non-lookup-fold (vec![], 0, 0) shape per Corrigendum microsoft#13 STAGE 0 disambiguation. Asserts vk.F_arity == 1, vk.lookup_fold_k == 0, vk.shape_registry_digest == ZERO, and that vk.pp_digest type-binds to E::Scalar. Parametrised inline as two sections per Mandate 5 (HyperKZG + IPA-PC are SAME-behavior input variations of the same setup shape). (7) Three existing in-crate test VK constructions (m_gh7_0_2_compressed_snark_envelope_off_fs_pedersen_binding_and_sigma_E2_equality happy + 1000-iter differential paths; m_gh7_0_2_compressed_snark_envelope_rejects_corrupted_binding_and_sigma) updated to populate the four new VK fields with the parts-based-test defaults. Rationale documented inline: the parts-based test path bypasses PublicParams, so F_arity = 1 (test-shape) + ro_consts = Default (matches PublicParams::setup precedent) + pp_digest = ZERO (no PublicParams) + lookup_fold_k = 0 + shape_registry_digest = ZERO (non-lookup-fold). pp_digest = ZERO is benign at the envelope verifier because the verify body uses vk_spartan.digest() (not pp_digest) for the b"vk" absorb at the Σ-protocol site (compressed_snark.rs:1385). ## Test verdicts - cargo test --release -p nova-snark --features lookup-fold m_gh7_1 → 1 passed / 172 filtered out (1 suite, 0.99s). Exit 0. - cargo test --release -p nova-snark --features lookup-fold m_gh7_0_2 → 3 passed / 170 filtered out (1 suite, 156.56s). Exit 0. (Includes the 1000-iter Pedersen-additive differential test; bulk of wall-clock is release-mode 1000-iter MSM throughput at structure- shape left=right=2.) - cargo test --release -p inumbra-spend-harness --test gh7_stage_k_compressor → 3 passed (1 suite, 1.35s). Exit 0. M.GH7.0.3 + M.GH7.0.4 + M.GH7.0.5 regression unchanged. Full-crate sweeps deliberately NOT invoked per .claude/rules/testing.md commit 7b9ee32 (the M.GH7.0.2 1000-iter differential + the harness integration tests are sufficient regression coverage for this type- signature polish). ## STOP-AND-ASK gates per dispatch — NONE FIRED The dispatch named one gate ("single-curve E2-phantom collapse compile- error cascade beyond obvious"): not triggered because the M.GH7.0.2 envelope had already collapsed E2/S2; M.GH7.1 only adds VK fields, no phantom-removal cascades. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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

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

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

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

…rewires for per-table FS-transcript per Corrigendum microsoft#16 sub-ratification (D-i); AO 22 discharge with IVC↔Spartan binding-deferral routed to M.GH7.5 path (b) Authors the M.GH7.4c envelope-side wire-up of the M.GH7.4a/4b Spartan- sibling-with-logup path through `CompressedSNARK<E, EE>` per the Corrigendum microsoft#16 sub-ratification (D-i)/(P1) at superproject `ce032d9`. Scope (per sub-ratification §5.5 row M.GH7.4c crisp scope): 1. Lift M.GH7.4b synthetic-data helpers `build_honest_logup_witnesses` and `build_per_table_commitments` from `#[cfg(test)] mod tests` at `vendor/nova/src/spartan/snark.rs:2780-2907` to `pub(crate)` envelope scope at `vendor/nova/src/neutron/compressed_snark.rs`. Gate microsoft#10 preservation: helpers preserved VERBATIM — LogUp- consistency-by-construction (the (A)+(B)+(C) Haböck §3 identities hold pointwise at the helper's internal `r_logup_j` via `batch_invert_plus_r`). 2. Extend `CompressedSNARK<E, EE>` envelope struct (NOT `BridgedNeutronInstance` per (D-i) gate microsoft#7 resolution) with six new fields carrying per-table commitments + `T_lookup` data + per-table `r_logup` scalars. Fields are empty `Vec::new()` at k=0 (STAGE-0 path) and populated by the prover at k>0. 3. Rewire `prove_from_parts` to invoke `prove_with_T_claim_split_error_with_logup` (M.GH7.4a/4b sibling) with empty per-table slices at k=0. The `_with_logup` sibling at k=0 is byte-functionally equivalent to the β' sibling (no per-table absorption; empty per-table residue body; identical batch_eval_reduce u_vec/w_vec at `3 + 4·0 = 3` entries). M.GH7.0.2 envelope regression tests pass under unconditional rewiring because verify-side is also rewired uniformly. 4. Author `pub(crate) fn prove_from_parts_with_logup(...)` — the M.GH7.4c acceptance-test entry point at k>0. Performs the envelope- side per-table FS-transcript discipline per dispatch authoring steps (6) + (7): - Absorb `comm_L_j`, `comm_ts_j`, `comm_inv_w_j`, `comm_inv_t_j`, `T_lookup_j` in `table_id`-canonical order at envelope-side transcript `b"NeutronCompressedSNARK_envelope"`. - Squeeze per-table `r_logup_j` sequentially (mirroring `nifs.rs:1492-1495` vendor NIFS-side discipline). - Invoke `_with_logup` sibling with prover-threaded per-table polynomial slices, per-table commitments, and (under (D-i)/(P1) binding-deferral disposition) the witness-construction `r_logup_per_table` (NOT the FS-squeezed value). 5. Rewire `CompressedSNARK::verify` to mirror the prover's per-table absorption + FS-squeeze sequence, then invoke `verify_with_T_claim_split_error_with_logup` (M.GH7.4b sibling) with the proof-envelope-carried `per_table_r_logup` scalars. 6. Add the M.GH7.4c end-to-end positive-path acceptance test at `vendor/nova/src/neutron/compressed_snark.rs::tests::m_gh7_4c_compressed_snark_end_to_end_with_per_table_lookup_envelope_transcript` — exercises `CompressedSNARK::prove_from_parts_with_logup → CompressedSNARK::verify` round-trip at `num_cons = 8, k = 2, table_size = 4` with envelope-built synthetic per-table data. Deterministic seed `0xC1BE_5BAD_C0DE_704Cu64`. IVC↔Spartan binding-deferral disposition under (D-i)/(P1) — Gate microsoft#11 narration discipline: Per-table commitments are envelope-fresh at length `num_cons` (R1CS- row domain), STRUCTURALLY DISTINCT from any IVC-layer `r_U.comm_L[j]` (witness-address domain, length `n_w`). The envelope FS squeeze of `r_logup_j` is STRUCTURALLY EXERCISED for transcript discipline (the audit-firm engagement can inspect the FS log) but the squeezed value is DISCARDED at M.GH7.4c — the sibling's LogUp-identity algebra closes against the prover-threaded `r_logup_per_table` (built INSIDE `build_honest_logup_witnesses`). The IVC↔Spartan binding between the envelope-fresh per-table commitments and the IVC-trace data lives at M.GH7.5 path (b) — to be crisped by Halpert authoring of the binding- discharge mechanism specification. Candidate mechanisms: (i) Two-round FS discipline: re-derive `r_logup_j` from FS during witness construction, with separate absorptions of `(L, ts, T)` and `(inv_w, inv_t)` either side of the per-`j` squeeze. (ii) Σ-protocol equality-of-opening between IVC-layer `r_U.comm_L[j]` and envelope-side `per_table_comm_L[j]` (analogous to Corrigendum microsoft#11's `SigmaE2EqualityProof`). (iii) Augmented-circuit-final-step absorption of envelope-side per-table commitments into the IVC public input. If M.GH7.5 path (b) cannot implement any of (i)/(ii)/(iii), the (D-i) ratification flips to (P3) per the sub-ratification's STOP-AND-ASK trigger #M.GH7.5.2. Regression invariants verified at vendor HEAD: - test_pp_digest (neutron + nova): 2/2 pass. - test_ivc_trivial (neutron + nova): 2/2 pass. - test_ivc_nontrivial_neutron: 1/1 pass. - test_ivc_base (neutron + nova): 2/2 pass. - test_setup (neutron + nova): 2/2 pass. - m_gh7_0_0b (3 tests including 1000-iter differential): 3/3 pass. - m_gh7_0_2 envelope regression (acceptance + negative + 1000-iter): 3/3 pass; the 1000-iter Pedersen-additive binding differential confirms the unconditional rewiring of `prove_from_parts` through `_with_logup` at k=0 is byte-functionally identical to the prior β' path. - m_gh7_3a positive-path: 1/1 pass. - m_gh7_4a/4a-degree-3-empirical/4b PCS-opening: 4/4 pass. - m_gh7_4c acceptance test: 1/1 pass — END-TO-END envelope-transcript round-trip at `num_cons = 8, k = 2, table_size = 4` closes. STOP-AND-ASK gate dispositions: Gate microsoft#6 FS-transcript independence: PRESERVED. Envelope-side absorbs happen on `b"NeutronCompressedSNARK_envelope"`; Spartan-side initialises FRESH `b"RelaxedR1CSSNARK"` per `snark.rs:1395`. The two transcripts NEVER share bytes — M.GH7.4a's note at `snark.rs:1755-1762` re-verified at vendor HEAD. Gate microsoft#7 STRUCT EXTENSION VS SIBLING: RESOLVED by sub-ratification — `BridgedNeutronInstance<E>` UNCHANGED; `CompressedSNARK<E, EE>` extended with six per-table Vec fields. Gate microsoft#8 KPI microsoft#2 proof-size: at fixture (num_cons=8, k=2), envelope grows by ~832 bytes (commitments + `r_logup` + length-8 T_lookup polys). Production-scale `T_lookup` carriage in `CompressedSNARK<E, EE>` is a future-milestone optimisation (move to `VerifierKey<E, EE>` or `pp`-level once binding-discharge mechanism is crisped at M.GH7.5). At M.GH7.4c fixture scale, growth is well under 12 KB. Gate microsoft#9 M.GH7.5 reachability: documented in acceptance test code comment + verify body comment + struct field doc-comments. M.GH7.5 path (b) is load-bearing for (D-i) soundness composition. Gate microsoft#10 LogUp-consistency of lifted helpers: PRESERVED VERBATIM from M.GH7.4b — helpers byte-equivalent at the algorithmic level. Gate microsoft#11 IVC↔Spartan binding-deferral narration: DOCUMENTED EXPLICITLY in acceptance test code comment (lines documenting "M.GH7.4c (D-i)/(P1) IVC↔Spartan binding-deferral disposition") + in verify body (binding-deferral discipline + three candidate mechanisms enumerated) + in struct field doc-comments. Per `.claude/rules/cryptography.md` (Gadget contract): the lifted helpers `build_honest_logup_witnesses` + `build_per_table_commitments` are the off-circuit reference for the M.GH7.4c synthetic-data construction; they live in production-shipped envelope code (NOT test scaffolding) so the wallet can derive the synthetic per-table data at envelope-build time under the (D-i)/(P1) disposition. The in-circuit half is the M.GH7.4a `prove_with_T_claim_split_error_with_logup` sibling (which the wallet's prover invokes via this M.GH7.4c envelope wire-up). The 1000-iter differential discipline is preserved by the M.GH7.0.2 envelope-binding differential (3/3 pass at 1000 iters under unconditional `_with_logup` rewiring). Sequencing: M.GH7.4c closes Phase 02. Phase 03 opens with M.GH7.5 (IVC↔Spartan binding-discharge mechanism specification + negative-test triple) — requires Halpert authoring per the sub-ratification's STOP-AND-ASK trigger #M.GH7.5.1 BEFORE crafter dispatch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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

…er-table fold propagation per Corrigendum microsoft#19 Wires post-fold per-table running commitments (comm_L, comm_ts) through the augmented circuit's verify_with_multi_table_lookup as untrusted hints, mirroring the existing comm_W_fold / comm_E_fold discipline at circuit/nifs.rs:46-55 / :649-664. Closes the IVC↔envelope binding by making the in-circuit Unew.comm_L_per_table[j] (absorbed at the final-step hash via M.GH7.5.0a's absorb_in_ro extension) byte-equal to the off-circuit r_U.comm_L[j] (absorbed at off-circuit RecursiveSNARK::verify via M.GH7.5.0a's absorb_in_ro2 extension). Changes: - Off-circuit NIFS<E> struct (src/neutron/nifs.rs): adds two new lookup-fold- gated hint fields, comm_L_fold_per_table and comm_ts_fold_per_table, each Option<Vec<Commitment<E>>>. Populated in prove_with_multi_table_lookup_inner by cloning U.comm_L / U.comm_ts from the off-circuit U1.fold_with_lookup output (the per-`j` independent fold body at relation.rs:862-884 per Corrigendum microsoft#6 primitive 3). Set to None on the non-multi-table prover paths (prove, prove_with_lookup, prove_with_multi_column_lookup) — those paths do not feed the augmented-circuit multi-table verifier. - In-circuit AllocatedLookupNIFSMultiTable (src/neutron/circuit/lookup.rs): adds Vec<AllocatedNonnativePoint<E>> fields comm_L_fold_per_table and comm_ts_fold_per_table; AllocatedLookupNIFSMultiTable::alloc allocates them from the per-step NIFS message's prover-supplied Vec hints (point-at-infinity default under shape-derivation `nifs == None`). - LookupVerifyOutputMultiTable (src/neutron/circuit/nifs.rs): widened to carry the per-table post-fold commitment hints. verify_with_multi_table_lookup clones the allocated hints from the AllocatedLookupNIFSMultiTable into the output — NO new constraint emission at this layer (pure passthrough); soundness via IVC hash-chain binding + envelope-side off-FS commitment- equality per Corrigendum microsoft#17 path (b). - from_lookup_fold_output (src/neutron/circuit/relation.rs): widened signature accepts comm_L_fold_per_table / comm_ts_fold_per_table Vec hints and OVERRIDES the M.GH7.5.0a passthrough of u_fold.comm_L_per_table / comm_ts_per_table. This is the load-bearing path α.2 wiring — without the override, Unew.comm_L_per_table[j] would carry PRE-fold (passthrough) values while r_U.comm_L[j] carries POST-fold values, and the IVC hash-chain check would reject the honest fold. - synthesize_non_base_case_lookup_fold (src/neutron/circuit/mod.rs): passes the new hint Vecs from lookup_output through to the widened from_lookup_fold_output. No prover-side wiring changes required — the data-flow is already in place via the NIFS message threading at prove_step_with_lookup_fold:976-988. - Acceptance tests (src/neutron/circuit/relation.rs stage0_byte_equivalence_tests): (a) Extends m_gh5_0_stage0_absorb_in_ro_byte_equivalence_at_fold_depth_1_and_2 with M.GH7.5.5 work-item 8 assertions: nifs1.comm_L_fold_per_table[j] and nifs2.comm_L_fold_per_table[j] MUST byte-equal folded_U_s1.comm_L[j] and folded_U_s2.comm_L[j] respectively (the hint-attachment locus sources from the POST-fold off-circuit U), plus the comm_ts variants plus a non-vacuity assertion that at least one entry is non-default (the k=2 multi-table fixture queries non-trivial table entries). (b) Adds m_gh7_5_0b_path_alpha2_from_lookup_fold_output_overrides_with_hint_vecs: directly synthesises from_lookup_fold_output with synthetic non-trivial hint Vecs distinct from the u_fold passthrough, then asserts (i) the result's comm_L_per_table x-limb-0 witness values match the HINTS (NOT the passthrough — falsifies a regression to M.GH7.5.0a behaviour); (ii) the in-circuit absorb_in_ro squeeze byte-equals the off-circuit absorb_in_ro2 squeeze on the same hint values. pp_digest baseline: test_pp_digest at lookup_fold_k = 0 is byte-identical (Vec-emptiness skip preserves the legacy R1CS-only shape); no expect refresh required since no production test_pp_digest fixture exercises lookup_fold_k > 0. Soundness anchors: parallel reasoning to vendor HEAD's existing comm_W_fold discipline (circuit/nifs.rs:46-55 / :649-664). The rejection mechanism for malicious post-fold per-table hints composes (i) IVC hash-chain divergence at the next step's Phase-1 hash check OR at the off-circuit RecursiveSNARK::verify hash reconstruction (M.GH7.5.0a-landed absorb extension + RO2 collision resistance per Nova 2021/370 v3 §4); (ii) envelope-side off-FS commitment- equality at CompressedSNARK::verify per Corrigendum microsoft#17 path (b), composed with Spartan-close Pedersen+LogUp identity binding (Haböck 2022/1530 §3 + Spartan 2019/550 §5). No new in-circuit constraint family is introduced; the Gadget contract from .claude/rules/cryptography.md is satisfied by parallel reasoning to the existing comm_W_fold discipline at vendor HEAD. Test scope: cargo test --release -p nova-snark --features lookup-fold (scoped): - test_pp_digest 1 passed - neutron::circuit::tests 1 passed - neutron::circuit::relation::stage0_byte_equivalence_tests 6 passed (5 pre-existing M.GH7.5.0a + 1 new M.GH7.5.0b consumer test) - neutron::circuit::nifs 1 passed - neutron::circuit::lookup::tests 4 passed - neutron::nifs::tests 17 passed - neutron::compressed_snark 10 passed - neutron::tests (incl. prove_step_with_lookup_fold IVC) 9 passed Refs: docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md Corrigendum microsoft#19 §"Revised implementation roadmap under path α.2" (work-items 1-9 discharged; STOP-AND-ASK trigger #M.GH7.5.5 byte-equivalence test explicitly authored at work-item 8). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…working tree — IdentityStepCircuit + Corrigendum microsoft#22 F2 fixture + 1000-iter empirical close + Falsifier G record Preserves the working-tree state authored at the previous M.GH7.5 third PREPARE (Corrigendum microsoft#21 Path 2 + Corrigendum microsoft#22 F2 single-setup-with- post-mutation fixture-construction algebra). Capture-only commit by the Corrigendum microsoft#23 experiment-protocol crafter dispatch — none of this content is authored by the dispatch crafter; preserved verbatim so the Experiment A/B diagnostic fixtures can stack cleanly on top. Content captured: - `IdentityStepCircuit` + `gh75_lookup_shape` + `gh75_build_honest_fixture` helpers (`compressed_snark.rs` lines ~4191-4472) — Corrigendum microsoft#21 Path 2 fixture algebra implemented via Corrigendum microsoft#22's surgical single-setup-with-post-construction-mutation fix. - `m_gh7_5_b_envelope_verify_ivc_trace_round_trip_byte_equivalence` (the M.GH7.5 acceptance test, line ~4485) — currently FAILS at vendor HEAD inside `gh75_build_honest_fixture`'s `recursive_snark.verify` call with `Err(NovaError::UnSat { sum != U.T })` at n=4. This is Obstruction 2 surfaced under Corrigendum microsoft#23. The test is preserved as-is per the dispatch ("DO NOT commit the failing existing M.GH7.5 acceptance test — that one stays as-is in the working tree until Corrigendum microsoft#24 lands a fix"). - Three negative tests `m_gh7_5_b_corrupted_envelope_per_table_comm_L_rejects`, `m_gh7_5_b_corrupted_envelope_per_table_comm_ts_rejects`, `m_gh7_5_b_corrupted_snapshot_r_U_comm_L_rejects` (preserved; do not pass under the current Obstruction 2 fire because they call `gh75_build_honest_fixture` which itself panics in the verify-side check). - `m_gh7_5_3_build_per_table_synthetic_data_closes_by_construction_1000_iter` (PASSES at vendor HEAD per the 2026-05-13 baseline re-confirmation by the experiment-protocol dispatch — 238s release-mode runtime, 1000 fresh fixtures, n=2 IVC, asserts `envelope.per_table_comm_L[j] == r_U.comm_L[j]` byte-equal). - `m_gh7_5_falsifier_g_obstruction_record_two_pass_ck_non_determinism` (PASSES — Corrigendum microsoft#22 record-the-obstruction discipline). - `src/neutron/mod.rs` visibility bumps to `pub(crate)` on the `RecursiveSNARK` fields `z0`, `ri`, `l_u`, `i`, `running_lws` and `#[serde(skip, default)]` on `shape_registry` — supporting the fixture algebra above. Empirical state recorded by the dispatch at this commit: - `m_gh7_5_3_build_per_table_synthetic_data_closes_by_construction_1000_iter` PASSES (238.50s release-mode, vendor HEAD `39aaec4`). - `m_gh7_5_b_envelope_verify_ivc_trace_round_trip_byte_equivalence` FAILS with `UnSat { sum != U.T, sum: 0x0639af1c..., U.T: 0x0f73deec... }` at `recursive_snark.verify(&pp, GH75_N_STEPS=4, &z0)`. The specific sum/U.T byte values differ across runs (HyperKZG OsRng-sampled tau per Falsifier G obstruction) but the failure class is stable. The Corrigendum microsoft#23 experiment fixtures (A: n=1, B: n=2) follow as separate commits on top of this capture. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…riment A — diagnostic fixture for Obstruction 2 (n=1 IVC verify); NOT a fix; FAILS with ProofVerifyError variant Authors the Experiment A fixture from Corrigendum microsoft#23's Experiment Protocol (pin lines 2989-2993). Empirically observes the verify-side outcome at the smallest possible IVC step count (n=1) so authoring Halpert can triage Obstruction 2's root cause from a structurally minimal witness. **Recorded outcome at vendor HEAD `cc59f57` (preserved-PREPARE parent commit) + this commit, 2026-05-13 release-mode, 0.67s runtime**: test result: FAILED Err(NovaError::ProofVerifyError { reason: "Invalid output hash in R1CS instance" }) Maps to dispatch outcome class **A3** (Corrigendum microsoft#23's "FAIL with different error variant"). The error fires from `vendor/nova/src/ neutron/mod.rs:791-794`'s IVC-hash-chain check, NOT from the `relation.rs:601-604` `sum != U.T` check that fires at n=4 in the existing acceptance test. Code path: ```rust // vendor/nova/src/neutron/mod.rs:780-794 let hash = { let mut hasher = <E1 as Engine>::RO::new(pp.ro_consts.clone()); hasher.absorb(<E1 as Engine>::Scalar::from(num_steps as u64)); for e in &self.z0 { hasher.absorb(*e); } for e in &self.zi { hasher.absorb(*e); } self.r_U.absorb_in_ro2(&mut hasher); hasher.absorb(self.ri); hasher.squeeze(NUM_HASH_BITS, false) }; if hash != self.l_u.X[0] { return Err(NovaError::ProofVerifyError { reason: "Invalid output hash in R1CS instance".to_string(), }); } ``` This means the IVC public-input hash that the verifier re-derives from the post-step `(num_steps, z0, zi, r_U, ri)` does NOT match the hash committed in `self.l_u.X[0]` (which is the fresh-instance public-input slot the augmented circuit's M.1 hash-chain rule computed *inside* the circuit at the previous step's end). The hash-chain check fires BEFORE the `pp.structure.is_sat` invocation at `mod.rs:798-805`, so the failing acceptance test's `UnSat { sum != U.T }` signature at n=4 is downstream of a *different* verifier check. **Routing implication for Halpert.** Corrigendum microsoft#23 enumerated three candidate root-cause families: (i) witness-side defect in the `LookupStepCircuit::per_table_bundles_at_step` impl; (ii) constraint- side defect in `verify_with_multi_table_lookup`; (iii) multi-step accumulation defect from i=1→2 transition. None of those three is the family that fires at n=1 — at n=1 there IS no multi-step accumulation (rules out (iii) for the n=1 surface). The IVC-hash- chain mismatch at n=1 suggests either: - (α) `RecursiveSNARK::new` bootstraps `self.l_u` with a hash that doesn't match what `prove_step_with_lookup_fold` re-computes at step 0, OR - (β) `prove_step_with_lookup_fold` updates `self.l_u.X[0]` with a hash derived from `(num_steps, z0, z1, r_U_post_fold, ri_post_fold)` that differs from the verifier's later re-derivation, OR - (γ) Some component of `(self.r_U, self.zi, self.ri)` is mutated between the prover's hash-committing step and the verifier's hash-re-derivation step. None of (α)/(β)/(γ) is in Corrigendum microsoft#23's (i)/(ii)/(iii) taxonomy — this is a fourth candidate family that the dispatch protocol explicitly flags as STOP-AND-ASK trigger ("Any experiment surfaces `Err(NovaError::ProofVerifyError)` ... different variant routes to a different root cause family"). Diagnostic fixture for Corrigendum microsoft#23 Experiment A — NOT a fix for Obstruction 2; FAILS as recorded above. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…riment B — diagnostic fixture for Obstruction 2 (n=2 IVC verify); NOT a fix; FAILS with R1CS-unsat variant Authors the Experiment B fixture from Corrigendum microsoft#23's Experiment Protocol (pin lines 2995-2998). Empirically observes the verify-side outcome at n=2 to triage the multi-step accumulation locus. **Recorded outcome at vendor HEAD `804325b` (Experiment A parent commit) + this commit, 2026-05-13 release-mode, 0.70s runtime**: test result: FAILED Err(NovaError::UnSat { reason: "R1CS is unsatisfiable" }) The variant is `UnSat { reason: "R1CS is unsatisfiable" }` — distinct from both Experiment A's `ProofVerifyError` at n=1 and the existing acceptance test's `UnSat { sum != U.T }` at n=4. The error fires from `vendor/nova/src/r1cs/mod.rs:516-519`, which is the **plain R1CS satisfiability check** (`Az[i] * Bz[i] == Cz[i]` for all i) inside `R1CSShape::is_sat` — invoked at `mod.rs:800` against the fresh `l_u/l_w` slot: ```rust // vendor/nova/src/neutron/mod.rs:798-800 let (res_r, res_l) = rayon::join( || pp.structure.is_sat(&pp.ck, &self.r_U, &self.r_W), || pp.structure.S.is_sat(&pp.ck, &self.l_u, &self.l_w), ); ``` The `res_l` arm is the fresh-instance plain-R1CS check (no eq-weighting, no folding); it's the un-folded R1CS slot for the LATEST step's augmented-circuit witness. At n=2 this slot corresponds to the augmented-circuit witness produced by the SECOND `prove_step_with_lookup_fold` call (i.e., the i=1→2 step). That witness does NOT satisfy plain R1CS — which means `prove_step_with_lookup_fold` at step i=1 produces an augmented- circuit witness that fails its own augmented-circuit R1CS structure (NOT a folded-sum identity failure). **Routing implication for Halpert.** At n=2 the IVC-hash-chain check (n=1's `ProofVerifyError` family) does NOT fire — so whatever hash-chain bug surfaces at n=1, it's somehow recovered (or different in shape) at n=2. But the plain-R1CS check now fires on the fresh slot, suggesting: - The augmented circuit emits some constraint at step i≥1 that the `prove_step_with_lookup_fold` witness assignment violates structurally. Candidates: M.7 reflexive identity at i=1 reads a DIFFERENT `chunk_index_in_z` than at i=0 (but the IdentityStepCircuit's `z_next = z` keeps `z_i[F_arity-1]` constant at ZERO, so this should hold) — OR — some constraint family in the augmented circuit's `with_lookup_fold` branch (line ranges in `circuit/mod.rs` / `circuit/nifs.rs`) expects a witness that `IdentityStepCircuit` does not allocate. Cross-reference with Experiment A's outcome: three distinct error variants surface across n ∈ {1, 2, 4} on the SAME fixture algebra: - n=1: `ProofVerifyError { "Invalid output hash in R1CS instance" }` (hash-chain check at `mod.rs:791-794`) - n=2: `UnSat { "R1CS is unsatisfiable" }` (fresh-slot plain R1CS at `r1cs/mod.rs:516-519`) - n=4: `UnSat { "sum != U.T" }` (running-side eq-weighted sumcheck at `relation.rs:601-604`) This variant-multiplicity is a much stronger diagnostic signal than Corrigendum microsoft#23 anticipated. The taxonomy (i)/(ii)/(iii) in the pin assumed a single failure-mode signature; the empirical record shows the fixture has at LEAST THREE structurally distinct failure surfaces, suggesting either (a) multiple latent bugs in the fixture algebra layered on top of each other, or (b) a single root-cause bug whose downstream manifestation depends on which verifier check fires first at each n. Diagnostic fixture for Corrigendum microsoft#23 Experiment B — NOT a fix for Obstruction 2; FAILS as recorded above. NOTE: Experiments C and D were NOT executed per the dispatch's STOP-AND-ASK rule ("Any experiment surfaces `Err(NovaError:: ProofVerifyError)` ... different variant routes to a different root cause family"). Experiment A triggered the rule at n=1; Experiment B was authored as cheap additional data (it costs ~1s to run) but authoring Halpert should consume both outcomes into Corrigendum microsoft#24 before any further empirical work proceeds. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…riment D-prime — diagnostic fixture for Obstruction 2 (n=1 hash-chain divergence locus); NOT a fix; PASSES as documented Obstruction 2 record Appends `m_gh7_5_obstruction2_experiment_d_prime_n1_hash_chain_divergence_locus` to `vendor/nova/src/neutron/compressed_snark.rs` at the test-module tail sibling to Experiments A and B. Mirrors the verifier-side hash-chain re-derive at `mod.rs:774-789` byte-for-byte AND a prover-equivalent reconstruction of the augmented circuit's base-case output-hash absorb sequence (`circuit/mod.rs:939-955` composed with `circuit/relation.rs: 502-570` on `default_with_lookup_k(cs, 1, k=1)` shape). Captures partial squeezes after each absorb step on both sides via fresh `PoseidonRO` re-absorb per prefix (since `PoseidonRO` is not `Clone`). Identifies the first divergence index and routes to D1/D2/D3/D4 per Corrigendum microsoft#24. Empirical close at vendor HEAD `b233301`: **D1 — (iv.γ) constant-shape- vs-Option-shape absorb-sequence drift at base case.** First divergence at prefix index 7, exactly at the `T_lookup` block: native verifier side skips (`r_U.T_lookup = None`), prover-equivalent side absorbs one zero scalar (mirroring `Unew_base.T_lookup_per_table = Some(vec![0; 1])` per `default_with_lookup_k`). Partials 0..=6 byte-equal across native and prover sides (`pp.digest`, `num_steps`/`i_new`, `z0`, `zi`/`z_next`, `comm_W`, `comm_E`, `T`). From index 7 onward streams diverge by one absorb-shift; final hash mismatch byte-for-byte matches the n=1 `Err(NovaError::ProofVerifyError { reason: "Invalid output hash in R1CS instance" })` reported by Experiment A. (iv.α) ruled OUT empirically: comm_W (idx=4) and comm_E (idx=5) partials byte-equal across native and prover sides — the `comm_E = comm_W.clone()` shared-variable circuit pattern does not produce an RO2-byte divergence against the native `Commitment::default()`-distinct-handle pattern at equal values. (iv.β) ruled OUT empirically: ri / r_next absorb (last position) is DOWNSTREAM of the (iv.γ) divergence — the divergence reaches that step already-corrupted by the (iv.γ) one-absorb-shift, so ri-allocation parity cannot be the root cause. Routes Corrigendum microsoft#25 to Fix-α: extend `FoldedInstance::default` to mirror constant-shape allocation under `lookup_fold_k > 0` (the strictly-more-general fix that closes the asymmetry without breaking Corrigendum microsoft#6's constant-shape FS-schedule discipline). Test asserts the divergence EXISTS (preferred pattern from Corrigendum microsoft#24 dispatch): PASSES at vendor HEAD `b233301` as a documented record of Obstruction 2's n=1 hash-chain divergence locus. If a future Corrigendum microsoft#25 fix-α lands and the divergence disappears, this fixture FAILS to signal that the obstruction has been resolved — at which point the fixture should be promoted into a positive single-step n=1 acceptance test (Corrigendum microsoft#23 layer 5b deferred deliverable). Read-only against vendor body: no modification to `RecursiveSNARK:: verify`, `FoldedInstance::default`, `AllocatedFoldedInstance::default`, `absorb_in_ro2`, or `absorb_in_ro`. Pure additive test fixture. Test invocation (release-mode mandatory per `.claude/rules/testing.md`): cargo test --release -p nova-snark --features lookup-fold --lib \ neutron::compressed_snark::tests::\ m_gh7_5_obstruction2_experiment_d_prime_n1_hash_chain_divergence_locus \ -- --nocapture Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ror per Corrigendum microsoft#25; PARTIAL-DISCHARGE; n=1 PASS + n=2/n=4 RED (Claim 2 falsified at i=1→2 transition) Corrigendum microsoft#25 Fix-α: NEW constructor FoldedInstance::default_with_lookup_k(S, k) co-existing with legacy default(S). Single production-call-site update at mod.rs:665 under #[cfg(feature = "lookup-fold")]. Empirical outcomes (release-mode, --features lookup-fold): PASS: m_gh7_5_n1_hash_chain_consistency_post_fix_alpha_resolved (NEW, n=1 IVC verify) m_gh7_5_obstruction2_experiment_d_prime (inverted assert_eq!, partial-squeezes byte-equal) m_gh7_5_obstruction2_experiment_a_n1_ivc_verify (inverted, n=1 PASS) m_gh7_5_0c_default_with_lookup_k_differential_1000_iter_byte_equivalence (NEW, 1002 iters) test_pp_digest (pp_digest preservation CONFIRMED per Corrigendum microsoft#25 finding 5) m_gh7_5_falsifier_g_obstruction_record (Corrigendum microsoft#22 record preserved) m_gh7_5_3_build_per_table_synthetic_data_closes_by_construction_1000_iter (246s) FAIL: m_gh7_5_obstruction2_experiment_b_n2_ivc_verify — UnSat { R1CS is unsatisfiable } at r1cs/mod.rs:516-519 (fresh-slot plain Az*Bz!=Cz at i=1 verify) m_gh7_5_b_envelope_verify_ivc_trace_round_trip_byte_equivalence — UnSat { sum != U.T } at relation.rs:601-604 (eq-weighted-sumcheck running-accumulator at n=4 verify) STOP-AND-ASK trigger #M.GH7.5.0c.3 FIRED: Corrigendum microsoft#25 Claim 1 (base-case byte-equivalence) — TRUE (n=1 + D-prime + 1002-iter) Corrigendum microsoft#25 Claim 2 (non-base-case fold preservation) — FALSE at n=2 Corrigendum microsoft#25 Claim 4 (verifier hash-chain at i >= 0) — partially violated at n=2+n=4 Diagnostic hypothesis: the i=1 prove-step produces r_W.W/r_W.E witness vectors against a running-instance shape that DIVERGES from Fix-α'd Some(vec![..; k]) at some prove-path site not enumerated in Corrigendum microsoft#25 finding 4 (which only counted FoldedInstance::default call sites, NOT prove-path shape-production sites like fold_with_lookup or NIFS::prove_with_multi_table_lookup). Files changed: src/neutron/relation.rs — NEW default_with_lookup_k at :686-744 src/neutron/mod.rs — call-site update at :665 + cfg-gating src/neutron/compressed_snark.rs — D-prime assert inversion + Experiment A/B inversion + NEW n=1 acceptance test + NEW 1002-iter differential test Disposition: PARTIAL-DISCHARGE committed to preserve empirical evidence (Fix-α IS correct at base case; n=2/n=4 failures are NEW obstructions masked by Obstruction 2 firing at n=1 first). Routed to Halpert for Corrigendum microsoft#26 Claim 2/3 re-derive. Refs: design pin Corrigendum microsoft#25 lines 3296-3666. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…riment E — TestCS which_is_unsatisfied diagnostic at step i=1; NOT a fix Diagnostic fixture for Corrigendum microsoft#26 Experiment E. Manually replicates RecursiveSNARK::new base-case synthesis with deterministic ri=ZERO, then mirrors prove_step_with_lookup_fold step i=1 but synthesizes into TestConstraintSystem instead of SatisfyingAssignment. RESULT: ALL 10,131 constraints SATISFIED at step i=1 with ri=ZERO. The n=2 IVC verify failure (Experiment B) is NOT caused by an unsatisfied R1CS constraint in the augmented circuit at step i=1 under deterministic ri=ZERO. The failure must be either: (a) specific to the production random ri path (OsRng at mod.rs:605), or (b) in the verify-side hash-chain re-derive, not circuit satisfaction. This narrows the Obstruction 2 locus away from in-circuit constraint violations and toward the ri-dependent hash-chain path. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…riment E-prime — TestCS random r_next diagnostic Experiment E-prime: byte-for-byte clone of Experiment E except r_next drawn from OsRng (production path) instead of GH75Scalar::ZERO. Result: E-prime-2 — ALL 10,131 constraints SATISFIED with random r_next. The R1CS violation observed in Experiment B (n=2 IVC verify UnSat) is NOT r_next-dependent. The failure must be in SatisfyingAssignment vs TestCS witness extraction or the verify-side hash-chain re-derive, not in the augmented circuit's constraint satisfaction at step i=1. r_next sampled: 0x2b50081c10881f8d8b35fad559a0ff25424b67eae89570ad3e060102c52edde9 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…— MISMATCH CONFIRMED Shape triple (num_cons, num_vars, num_io) comparison across three sources: (A) pp.structure.S (padded): (16384, 16384, 1) (C) TestShapeCS shape-derivation: (11272, 11400, 1) — matches (A) pre-pad (B) TestCS step i=1: (10131, 10252, 1) — MISMATCH Delta (C)-(B): +1141 constraints, +1148 aux variables, +0 io. Root cause: num_value_columns divergence in circuit/mod.rs:771-782 AllocatedLookupPayloadPublicMultiTable::alloc. Shape-derivation (None inputs) defaults num_value_columns=1; step i=1 reads bundle.comm_values.len()=0 from IdentityStepCircuit's absent-table bundle (LookupPayload.comm_values: vec![]). Each AllocatedNonnativePoint for comm_values[j] allocates ~1148 aux + ~1141 constraints (nonnative field decomposition), producing the exact observed delta. Consequence: SatisfyingAssignment at step i=1 allocates 10252 aux variables but pp.structure.S.num_vars (padded) expects 16384. The R1CSWitness::new call in r1cs_instance_and_witness will fail on length check. This is the root cause of the n=2 verify failure. Fix direction: IdentityStepCircuit must supply comm_values.len()==1 in its per_table_bundles_at_step (matching the shape-derivation default), OR the shape-derivation default must read num_value_columns from the LookupShape::multi_column_tables[j].columns.len() instead of hardcoding 1. Also adds num_aux() and num_inputs() accessors to TestConstraintSystem. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…(1)→unwrap_or(0) per Corrigendum microsoft#27; Obstruction 2 FULLY RESOLVED The verify-side augmented circuit allocated a synthetic 1-column LookupPayloadPublicMultiTable for absent tables (bundle_j = None), producing a shape mismatch against the prove-side zero-column allocation. Fix: `unwrap_or(0)` — absent bundle means zero value commitments, not one phantom commitment. Verified (all PASS, release-mode): - m_gh7_5_n1_hash_chain_consistency_post_fix_alpha_resolved (n=1) - m_gh7_5_obstruction2_experiment_a_n1_ivc_verify (n=1) - m_gh7_5_obstruction2_experiment_b_n2_ivc_verify (n=2) — key test - m_gh7_5_b_envelope_verify_ivc_trace_round_trip_byte_equivalence (n=4) — acceptance - m_gh7_5_obstruction2_experiment_d_prime_n1_hash_chain_divergence_locus - m_gh7_5_0c_default_with_lookup_k_differential_1000_iter_byte_equivalence (1002-iter) - m_gh7_5_falsifier_g_obstruction_record_two_pass_ck_non_determinism - test_pp_digest (pp_digest preservation) Co-Authored-By: Claude <noreply@anthropic.com>

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

Derive more traits.

29d8044

srinathsetty merged commit 3e80c5c into microsoft:main Oct 8, 2021

porcuquine deleted the derive-traits branch October 19, 2021 00:22

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

Merge pull request microsoft#7 from privacy-scaling-explorations/chir…

9826aba

…o/feature/dummy_test_of_parallel_prover Add dummy test for parallel prover

Sun-Jc mentioned this pull request Jul 23, 2026

feat(ppsnark): Batch the Logup-GKR last layer with the Inner sumcheck batch #502

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Derive more traits.#7

Derive more traits.#7
srinathsetty merged 1 commit into
microsoft:mainfrom
porcuquine:derive-traits

porcuquine commented Oct 7, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

porcuquine commented Oct 7, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants