Skip to content

Update version#12

Merged
srinathsetty merged 1 commit into
mainfrom
srinathsetty-patch-1
Oct 20, 2021
Merged

Update version#12
srinathsetty merged 1 commit into
mainfrom
srinathsetty-patch-1

Conversation

@srinathsetty

Copy link
Copy Markdown
Collaborator

No description provided.

@srinathsetty
srinathsetty merged commit 5e5dd65 into main Oct 20, 2021
@srinathsetty
srinathsetty deleted the srinathsetty-patch-1 branch October 20, 2021 17:31
huitseeker added a commit to huitseeker/Nova that referenced this pull request Aug 23, 2023
* Optimize generator creation in provider module

- Refactored the `from_label` function in pasta.rs removing redundant collect, flatten operations and Vec<usize> creation,

* fix: rename VanillaRO -> NativeRO

* refactor: Optimize circuit methods and enhance trait compatibility

- Replaced the `.map()` function with the `.map_or()` function in `r1cs.rs` for efficiency.
- Added `Eq` trait derivation to `NovaAugmentedCircuitParams` in `circuit.rs` to enable comparisons.
- Introduced `Eq` trait to `TrivialTestCircuit` struct in `traits/circuit.rs` without altering its input or output.
- Optimized performance by refactoring the use of iterator `into_iter()` to the iterator itself in `gadgets/r1cs.rs`.
huitseeker added a commit to huitseeker/Nova that referenced this pull request Sep 19, 2023
* Optimize generator creation in provider module

- Refactored the `from_label` function in pasta.rs removing redundant collect, flatten operations and Vec<usize> creation,

* fix: rename VanillaRO -> NativeRO

* refactor: Optimize circuit methods and enhance trait compatibility

- Replaced the `.map()` function with the `.map_or()` function in `r1cs.rs` for efficiency.
- Added `Eq` trait derivation to `NovaAugmentedCircuitParams` in `circuit.rs` to enable comparisons.
- Introduced `Eq` trait to `TrivialTestCircuit` struct in `traits/circuit.rs` without altering its input or output.
- Optimized performance by refactoring the use of iterator `into_iter()` to the iterator itself in `gadgets/r1cs.rs`.
srinathsetty pushed a commit that referenced this pull request Sep 25, 2023
* Small perf items (#12)

* Optimize generator creation in provider module

- Refactored the `from_label` function in pasta.rs removing redundant collect, flatten operations and Vec<usize> creation,

* fix: rename VanillaRO -> NativeRO

* refactor: Optimize circuit methods and enhance trait compatibility

- Replaced the `.map()` function with the `.map_or()` function in `r1cs.rs` for efficiency.
- Added `Eq` trait derivation to `NovaAugmentedCircuitParams` in `circuit.rs` to enable comparisons.
- Introduced `Eq` trait to `TrivialTestCircuit` struct in `traits/circuit.rs` without altering its input or output.
- Optimized performance by refactoring the use of iterator `into_iter()` to the iterator itself in `gadgets/r1cs.rs`.

* ci: Bring clippy standards lurk-rs -> arecibo (#13)

* ci: Bring clippy standards lurk-rs -> arecibo

- Added a new .cargo/config file with a custom alias "xclippy" to execute Clippy lints for code quality assurance,
- Fixed code correspondingly when necessary,
- Added xclippy to CI

* chore: add dbg_macro to ci's clippy

- Implemented a new clippy lint for the dbg_macro in the cargo config file

* test: Extend tests to add missing curve variants (#33)

- Enhanced testing for multiple modules, including bellpepper, spartan, and provider, focusing on the addition and multiplication of multi-linear polynomials and the Keccak transcript.
- Introduced usage of secp256k1::Scalar (and sometimes bn256_grumpkin::bn256::Scalar) into tests for improved coverage.
marcus-sa added a commit to marcus-sa/Nova that referenced this pull request May 12, 2026
…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.
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant