Update rust.yml#11
Merged
Merged
Conversation
huitseeker
added a commit
to huitseeker/Nova
that referenced
this pull request
Aug 23, 2023
* refactor: Remove R1CS struct to direct commitment_key calls - Removed the `R1CS` struct and its associated types from `r1cs.rs` as well as its public use in `lib.rs`. - Updated the program's `commitment_key` and `commitment_key_size` functions to require explicit Group type parameter, instead of being derived from the `R1CS` struct. - Adapted functions to the removal of `R1CS` struct, using `commitment_key` directly. * refactor: Simplify NIFS struct and remove PhantomData usage - Simplified the NIFS struct in `nifs.rs` file by removing extraneous elements. * refactor: Refactor ipa_pc.rs to use InnerProductArgument directly - Removed `EvaluationArgument` struct from `ipa_pc.rs` file, replacing it with direct usage of `InnerProductArgument`. - Updated `EvaluationEngineTrait` type declarations to accommodate the change. - Reworked `prove` and `verify` methods to work directly with `InnerProductArgument`. - Made `InnerProductArgument` visibility public. * refactor: Refactor PoseidonROCircuit struct trait bound - Trait bound changed from `PrimeField + PrimeFieldBits` to `PrimeField` in `poseidon.rs`. * refactor: mutualize macro for secp/bn256 cycles
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 11, 2026
…nobs feature + corrupt_t_lookup_at_index knob + AO 17 visibility bump Per design pin Corrigendum microsoft#10 (Halpert, 2026-05-10) and Corrigendum microsoft#11 (Halpert, 2026-05-10), this commit lands the vendor-side surface for M.GH5.7's three negative tests (cryptographer-gated soundness gating). Cargo.toml — adds `test-debug-knobs = []` opt-in feature flag. Strict additive; production builds without `test-debug-knobs` remain byte- identical to vendor HEAD. src/neutron/circuit/mod.rs: - `NeutronAugmentedCircuitInputs` gains `#[cfg(any(test, feature = "test-debug-knobs"))] pub corrupt_t_lookup_at_index: Option<(usize, E::Scalar)>` field + `with_corrupt_t_lookup_at_index` builder method. - Corruption injection at the augmented-circuit allocation site so the IN-CIRCUIT `t_lookup_running_per_table[idx]` allocation is perturbed AFTER honest U.T_lookup_per_table allocation but BEFORE feeding into `verify_with_multi_table_lookup` (Pin §3.5 shape (a) + Corrigendum microsoft#10 Q2 dispatch shape). - `let mut U` cfg-split so the production build (`lookup-fold` without `test-debug-knobs`) does not trip `#[deny(unused_mut)]`. src/neutron/mod.rs — re-exports `NeutronAugmentedCircuit`, `NeutronAugmentedCircuitInputs`, `AllocatedNIFS`, `AllocatedFoldedInstance`, `AllocatedLookupNIFSMultiTable`, `AllocatedLookupPayloadPublicMultiTable`, `AllocatedNonnativeR1CSInstance` so M.GH5.7's harness-side tests can construct fixtures via direct vendor-internal types per Pin §5.2 + Corrigendum microsoft#10 Q2 Option A.2. src/neutron/nifs.rs — `pub fn prove_with_multi_table_lookup_inner` visibility bump (Auditor Obligation 17 — byte-equivalence verification of synthetic-Some(vec![ZERO; k]) running U vs default-None running U). Lemma α-Q1 (Corrigendum microsoft#10) is exercised by the harness-side AO 17 smoke test asserting prove-call equivalence. src/neutron/relation.rs — exposes `Structure::shape()`, `FoldedInstance::comm_W()`, `FoldedInstance::comm_E()` accessors required by harness-side fixture construction. All `pub` visibility under existing crate-public types; no new layout / no soundness implications. Soundness disposition (Corrigendum microsoft#11): test (i) rejects via dual-path (Path A §1.5 binding-via-hash, Path B §3.3 clone → (C)-binding); per declaration-order at vendor HEAD, Path B declares first and is the asserted twin-substring. AO 9 / (W1)-direct discharged via end-to-end corruption-detection (both paths reject). Pin §5.3 microsoft#3, microsoft#4, microsoft#5 discharged. Pin §D.4 microsoft#5, microsoft#3' discharged. Auditor Obligations 9, 12, 14, 17 status: discharged at vendor HEAD. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 12, 2026
…_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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 12, 2026
…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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 12, 2026
…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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…logup sumcheck engine + prove_with_T_claim_split_error_with_logup Spartan sibling (per Corrigendum microsoft#16; AO 23 discharge positive-path) Authors the M.GH7.4 subdivision's first sub-milestone (M.GH7.4a per Corrigendum microsoft#16 §5.5 row split). Two new vendor-side methods, both siblings to the existing β' / neutron-form Spartan-close machinery (preserves M.GH7.0.0b STAGE-0 byte-equivalence verbatim by leaving the existing methods unchanged): 1. `SumcheckProof::prove_neutron_outer_with_logup` at `src/spartan/sumcheck.rs` — new sumcheck-engine sibling. Extends the existing `prove_neutron_outer` with per-table LogUp (A)+(B) residue bodies composed additively under per-table `r_logup_j` per Corrigendum microsoft#16 Finding B (no gamma-RLC; matches the vendor NIFS-side parallel-univariate discipline at `nifs.rs:1497-1638`). Per-round univariate is degree-3 under additive composition per Finding C (verified empirically — see (3) below). `bind_poly_var_top` per Corrigendum microsoft#9 (2-A) preserved for ALL polynomials (R1CS-side AND per-table). Returns the new `PerTableOuterEvals<F>` struct carrying the seven per-table polynomial values at `r_x` for M.GH7.4b PCS-opening wiring. 2. `RelaxedR1CSSNARK::prove_with_T_claim_split_error_with_logup` at `src/spartan/snark.rs` — new Spartan-close sibling. FS-transcript discipline byte-identical to β' (Corrigendum microsoft#10 Primitive 5: absorb vk → U → T_claim before any squeeze); per-table `r_logup_j` are scalar inputs, NOT transcript squeezes, preserving Corrigendum microsoft#11 envelope-Spartan FS isolation. Inner sumcheck + batch-eval-reduce UNCHANGED from β' per Corrigendum microsoft#16 — per-table PCS-opening lands at M.GH7.4b. Returns `(Self, Vec<PerTableOuterEvals>)` exposing the per-table evals for downstream M.GH7.4b wiring. STOP-AND-ASK gates (Corrigendum microsoft#16 §5.5 row M.GH7.4a) — NONE RAISED: Gate microsoft#1 (sibling vs extend-in-place): SIBLING. Both new methods are authored alongside the existing β' / prove_neutron_outer paths verbatim; M.GH7.0.0b STAGE-0 byte-equivalence guaranteed by construction. Gate microsoft#2 (degree-3 empirical close): PASSED. Finding C's algebra-level disposition (eq-factor weighting IS the deg-1 contribution; (A)+(B) bodies are deg-3 under additive composition) is empirically confirmed by `m_gh7_4a_prove_neutron_outer_with_logup_degree_3_additive_composition_closes_correctly` — 1000 iterations × 2 engines (Bn256EngineKZG + PallasEngine) on seed `0xC1BE_5BAD_C0DE_704A`, falsifier-shape "4-eval-point degree-3 reconstruction at {0,1,∞,−1} must equal direct closed-form at t=2". The unified body under additive composition is exactly degree-3; no escalation to degree-4 needed; 4 eval points suffice. Gate microsoft#3 (per-table outer-sumcheck variable partition / Finding F): RESOLVED via flat embedding. Per-table polynomials and per-table eq-factors are pre-flattened onto the R1CS variable space at length `num_cons = left * right` by the caller (envelope-side at M.GH7.4c). `bind_poly_var_top` applies uniformly across R1CS-side and per-table polys. Corrigendum microsoft#9 (2-A) `r_x_high`/`r_x_low` partition preserved verbatim — per-table polys are additive residue terms, not factors of `full_E`, so they do NOT interact with the E1/E2 factorisation. Test coverage: - `m_gh7_4a_prove_with_T_claim_split_error_with_logup_round_trip`: HONEST-LogUp round-trip at fixture `num_cons=4, k=2`, seed `0xC1BE_5BAD_C0DE_704A`. Constructs per-table witnesses with `inv_w_j[i] = 1/(w_j[i] + r_logup_j)` and `inv_t_j[i] = ts_j[i]/(T_j[i] + r_logup_j)` (Haböck eprint 2022/1530 §3); per-table eq-factors via `PowPolynomial::new(tau, ell).evals()` (non-degenerate per Halpert sub-ratification 2026-05-12 late evening). Asserts (i) prover succeeds, (ii) `per_table_outer_evals.len() == k`, (iii) β' sibling regression: `prove_with_T_claim_split_error` continues to round-trip via verify byte-identically at the same fixture shape. - `m_gh7_4a_prove_neutron_outer_with_logup_degree_3_additive_composition_closes_correctly`: the empirical degree-3 close above (gate microsoft#2 discharge). - `m_gh7_4a_per_table_outer_evals_struct_field_shape`: structural sanity on `PerTableOuterEvals<F>` field shape — guards against accidental field rotation when M.GH7.4b extends `Self` with per-table commitment carry. Regression invariants preserved (release-mode `cargo test --release --features lookup-fold --lib <test_name>` per `.claude/rules/testing.md`): - M.GH7.0.5 STAGE 0: `test_pp_digest` (1/1 ok), `test_ivc_base` + `test_ivc_trivial` + `test_ivc_nontrivial_neutron` (3/3 ok), `test_setup` (1/1 ok). Hard-gate pass cardinality 10/10 STANDS. - M.GH7.0.0b: `m_gh7_0_0b_prove_with_T_claim_split_error_neutron_form_round_trip_byte_equal`, `m_gh7_0_0b_weighting_differential_1000_iter`, `m_gh7_0_0b_negative_T_corruption_rejected` (3/3 ok). - M.GH7.3a: `m_gh7_3a_prove_step_with_lookup_fold_sibling_threads_running_lws_witness_alloc_preserved_positive_path` (1/1 ok). - M.GH7.3b: `prove_step_with_lookup_fold_corrupt_t_at_index_in_consumed_u1_rejects_at_r1cs_c_binding`, `prove_step_with_lookup_fold_post_prove_mutate_poly_lookup_via_nifs_rebuild_rejects_at_lookup_c_binding`, `prove_step_with_lookup_fold_corrupt_t_lookup_at_index_in_consumed_u1_rejects_at_lookup_c_binding` (3/3 ok). LOC: ~+540 sumcheck.rs (sumcheck-engine sibling + `PerTableOuterEvals` struct); ~+820 snark.rs (Spartan-close sibling + M.GH7.4a test module + `pub(super)` visibility on two M.GH7.0.0b test helpers for sibling-module reuse). The crafter-side line target was ~+300 LOC across both files; actual is larger because the sumcheck-engine sibling does NOT abstract the R1CS-side body (it's inlined verbatim from `prove_neutron_outer` to keep the additive composition's per-round eval-point arithmetic literal and audit-readable — extraction to a shared helper is deferred to M.GH7.4b/c's final consolidation if a shared shape emerges). Discharges AO 23 (unified outer-sumcheck claim batches R1CS + per-table LogUp identities via additive composition under per-table `r_logup_j`). Positive-path only per Corrigendum microsoft#16 §5.5 row M.GH7.4a; corrupt- multiplicities negative-test lands at M.GH7.5 per AO 24. Refs: docs/research/cryptography/microsoftgh-7-stage-k-compressed-snark-design-pin-2026-05-11.md Corrigendum microsoft#16 (M.GH7.4 subdivision into M.GH7.4a/b/c) §1.2, §2.2 Phase 4/5, §5.5 row M.GH7.4a, §6.1 row M.GH7.4a, §6.3 AO 23 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…rewires for per-table FS-transcript per Corrigendum microsoft#16 sub-ratification (D-i); AO 22 discharge with IVC↔Spartan binding-deferral routed to M.GH7.5 path (b) Authors the M.GH7.4c envelope-side wire-up of the M.GH7.4a/4b Spartan- sibling-with-logup path through `CompressedSNARK<E, EE>` per the Corrigendum microsoft#16 sub-ratification (D-i)/(P1) at superproject `ce032d9`. Scope (per sub-ratification §5.5 row M.GH7.4c crisp scope): 1. Lift M.GH7.4b synthetic-data helpers `build_honest_logup_witnesses` and `build_per_table_commitments` from `#[cfg(test)] mod tests` at `vendor/nova/src/spartan/snark.rs:2780-2907` to `pub(crate)` envelope scope at `vendor/nova/src/neutron/compressed_snark.rs`. Gate microsoft#10 preservation: helpers preserved VERBATIM — LogUp- consistency-by-construction (the (A)+(B)+(C) Haböck §3 identities hold pointwise at the helper's internal `r_logup_j` via `batch_invert_plus_r`). 2. Extend `CompressedSNARK<E, EE>` envelope struct (NOT `BridgedNeutronInstance` per (D-i) gate microsoft#7 resolution) with six new fields carrying per-table commitments + `T_lookup` data + per-table `r_logup` scalars. Fields are empty `Vec::new()` at k=0 (STAGE-0 path) and populated by the prover at k>0. 3. Rewire `prove_from_parts` to invoke `prove_with_T_claim_split_error_with_logup` (M.GH7.4a/4b sibling) with empty per-table slices at k=0. The `_with_logup` sibling at k=0 is byte-functionally equivalent to the β' sibling (no per-table absorption; empty per-table residue body; identical batch_eval_reduce u_vec/w_vec at `3 + 4·0 = 3` entries). M.GH7.0.2 envelope regression tests pass under unconditional rewiring because verify-side is also rewired uniformly. 4. Author `pub(crate) fn prove_from_parts_with_logup(...)` — the M.GH7.4c acceptance-test entry point at k>0. Performs the envelope- side per-table FS-transcript discipline per dispatch authoring steps (6) + (7): - Absorb `comm_L_j`, `comm_ts_j`, `comm_inv_w_j`, `comm_inv_t_j`, `T_lookup_j` in `table_id`-canonical order at envelope-side transcript `b"NeutronCompressedSNARK_envelope"`. - Squeeze per-table `r_logup_j` sequentially (mirroring `nifs.rs:1492-1495` vendor NIFS-side discipline). - Invoke `_with_logup` sibling with prover-threaded per-table polynomial slices, per-table commitments, and (under (D-i)/(P1) binding-deferral disposition) the witness-construction `r_logup_per_table` (NOT the FS-squeezed value). 5. Rewire `CompressedSNARK::verify` to mirror the prover's per-table absorption + FS-squeeze sequence, then invoke `verify_with_T_claim_split_error_with_logup` (M.GH7.4b sibling) with the proof-envelope-carried `per_table_r_logup` scalars. 6. Add the M.GH7.4c end-to-end positive-path acceptance test at `vendor/nova/src/neutron/compressed_snark.rs::tests::m_gh7_4c_compressed_snark_end_to_end_with_per_table_lookup_envelope_transcript` — exercises `CompressedSNARK::prove_from_parts_with_logup → CompressedSNARK::verify` round-trip at `num_cons = 8, k = 2, table_size = 4` with envelope-built synthetic per-table data. Deterministic seed `0xC1BE_5BAD_C0DE_704Cu64`. IVC↔Spartan binding-deferral disposition under (D-i)/(P1) — Gate microsoft#11 narration discipline: Per-table commitments are envelope-fresh at length `num_cons` (R1CS- row domain), STRUCTURALLY DISTINCT from any IVC-layer `r_U.comm_L[j]` (witness-address domain, length `n_w`). The envelope FS squeeze of `r_logup_j` is STRUCTURALLY EXERCISED for transcript discipline (the audit-firm engagement can inspect the FS log) but the squeezed value is DISCARDED at M.GH7.4c — the sibling's LogUp-identity algebra closes against the prover-threaded `r_logup_per_table` (built INSIDE `build_honest_logup_witnesses`). The IVC↔Spartan binding between the envelope-fresh per-table commitments and the IVC-trace data lives at M.GH7.5 path (b) — to be crisped by Halpert authoring of the binding- discharge mechanism specification. Candidate mechanisms: (i) Two-round FS discipline: re-derive `r_logup_j` from FS during witness construction, with separate absorptions of `(L, ts, T)` and `(inv_w, inv_t)` either side of the per-`j` squeeze. (ii) Σ-protocol equality-of-opening between IVC-layer `r_U.comm_L[j]` and envelope-side `per_table_comm_L[j]` (analogous to Corrigendum microsoft#11's `SigmaE2EqualityProof`). (iii) Augmented-circuit-final-step absorption of envelope-side per-table commitments into the IVC public input. If M.GH7.5 path (b) cannot implement any of (i)/(ii)/(iii), the (D-i) ratification flips to (P3) per the sub-ratification's STOP-AND-ASK trigger #M.GH7.5.2. Regression invariants verified at vendor HEAD: - test_pp_digest (neutron + nova): 2/2 pass. - test_ivc_trivial (neutron + nova): 2/2 pass. - test_ivc_nontrivial_neutron: 1/1 pass. - test_ivc_base (neutron + nova): 2/2 pass. - test_setup (neutron + nova): 2/2 pass. - m_gh7_0_0b (3 tests including 1000-iter differential): 3/3 pass. - m_gh7_0_2 envelope regression (acceptance + negative + 1000-iter): 3/3 pass; the 1000-iter Pedersen-additive binding differential confirms the unconditional rewiring of `prove_from_parts` through `_with_logup` at k=0 is byte-functionally identical to the prior β' path. - m_gh7_3a positive-path: 1/1 pass. - m_gh7_4a/4a-degree-3-empirical/4b PCS-opening: 4/4 pass. - m_gh7_4c acceptance test: 1/1 pass — END-TO-END envelope-transcript round-trip at `num_cons = 8, k = 2, table_size = 4` closes. STOP-AND-ASK gate dispositions: Gate microsoft#6 FS-transcript independence: PRESERVED. Envelope-side absorbs happen on `b"NeutronCompressedSNARK_envelope"`; Spartan-side initialises FRESH `b"RelaxedR1CSSNARK"` per `snark.rs:1395`. The two transcripts NEVER share bytes — M.GH7.4a's note at `snark.rs:1755-1762` re-verified at vendor HEAD. Gate microsoft#7 STRUCT EXTENSION VS SIBLING: RESOLVED by sub-ratification — `BridgedNeutronInstance<E>` UNCHANGED; `CompressedSNARK<E, EE>` extended with six per-table Vec fields. Gate microsoft#8 KPI microsoft#2 proof-size: at fixture (num_cons=8, k=2), envelope grows by ~832 bytes (commitments + `r_logup` + length-8 T_lookup polys). Production-scale `T_lookup` carriage in `CompressedSNARK<E, EE>` is a future-milestone optimisation (move to `VerifierKey<E, EE>` or `pp`-level once binding-discharge mechanism is crisped at M.GH7.5). At M.GH7.4c fixture scale, growth is well under 12 KB. Gate microsoft#9 M.GH7.5 reachability: documented in acceptance test code comment + verify body comment + struct field doc-comments. M.GH7.5 path (b) is load-bearing for (D-i) soundness composition. Gate microsoft#10 LogUp-consistency of lifted helpers: PRESERVED VERBATIM from M.GH7.4b — helpers byte-equivalent at the algorithmic level. Gate microsoft#11 IVC↔Spartan binding-deferral narration: DOCUMENTED EXPLICITLY in acceptance test code comment (lines documenting "M.GH7.4c (D-i)/(P1) IVC↔Spartan binding-deferral disposition") + in verify body (binding-deferral discipline + three candidate mechanisms enumerated) + in struct field doc-comments. Per `.claude/rules/cryptography.md` (Gadget contract): the lifted helpers `build_honest_logup_witnesses` + `build_per_table_commitments` are the off-circuit reference for the M.GH7.4c synthetic-data construction; they live in production-shipped envelope code (NOT test scaffolding) so the wallet can derive the synthetic per-table data at envelope-build time under the (D-i)/(P1) disposition. The in-circuit half is the M.GH7.4a `prove_with_T_claim_split_error_with_logup` sibling (which the wallet's prover invokes via this M.GH7.4c envelope wire-up). The 1000-iter differential discipline is preserved by the M.GH7.0.2 envelope-binding differential (3/3 pass at 1000 iters under unconditional `_with_logup` rewiring). Sequencing: M.GH7.4c closes Phase 02. Phase 03 opens with M.GH7.5 (IVC↔Spartan binding-discharge mechanism specification + negative-test triple) — requires Halpert authoring per the sub-ratification's STOP-AND-ASK trigger #M.GH7.5.1 BEFORE crafter dispatch. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.