Fix CS::one() bug in solver.#24
Merged
Merged
Conversation
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…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>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 16, 2026
…perKZG opening at r_x (KPI microsoft#3 envelope restoration) Implements Corrigendum microsoft#29 of the GH-microsoft#7 Stage K corrigenda chain per the ratified design pin at docs/research/cryptography/microsoftgh-7-stage-k-corrigendum-T-lookup-envelope-2026-05-16.md (Halpert, 2026-05-16; cryptographer-reviewer RATIFY). Mechanism (Path b ratified): replace the per_table_T_lookup: Vec<Vec<E::Scalar>> envelope field whose inner length num_cons is the linear-in-num_cons envelope-size regression at KPI microsoft#3 (slice-04 forecast ~12,289 bytes vs 12,288-byte ceiling; slice-06 multi-MB under k=2 at num_cons ~1.7M) with per_table_comm_T_lookup: Vec<Commitment<E>>. The verifier batched-opens T_j(r_x) via a 5th per-table PolyEvalInstance in the existing u_vec (extending 3 + 4*k -> 3 + 5*k); the claimed evaluation comes from the prover-published per_table_outer_evals[j].eval_T (already consumed by the unified outer-sumcheck residue identity per Corrigendum microsoft#16 Finding B). Affected sites: - vendor/nova/src/neutron/compressed_snark.rs: * Struct field per_table_T_lookup -> per_table_comm_T_lookup * build_per_table_commitments: 4-tuple -> 5-tuple * prove_with_lookup_fold: pass new commitment slice * prove_from_parts_with_logup: new parameter + envelope FS-absorb of per_table_comm_T_lookup under FS-tag b"comm_T_lookup_j" (was raw vec under b"T_lookup_j") * prove_from_parts (k=0 path): empty slice for the 5th param * verify body: cardinality check + FS-absorb + Spartan delegation * M.GH7.4c acceptance test: build the 5th commitment, drop the inner-length assertion (commitments have no inner length) - vendor/nova/src/spartan/snark.rs: * prove_with_T_claim_split_error_with_logup: new parameter per_table_comm_T_lookup + cardinality assert; w_vec and u_vec extended from 3 + 4*k to 3 + 5*k with the 5th per-table entry (PolyEvalWitness {p: per_table_T[j].clone()} + PolyEvalInstance {c: per_table_comm_T_lookup[j], x: r_x.clone(), e: per_table_outer_evals[j].eval_T}) * verify_with_T_claim_split_error_with_logup: signature change per_table_T: &[Vec<E::Scalar>] -> per_table_comm_T: &[Commitment<E>]; remove inner-length-num_cons check; remove MLE-eval cross-check (the binding migrates to the batched HyperKZG opening at the u_vec extension below); extend u_vec from 3 + 4*k to 3 + 5*k * Test-scope build_per_table_commitments: 4-tuple -> 5-tuple * M.GH7.4a + M.GH7.4b acceptance tests: build the 5th commitment; update call sites; verify still accepts FS-tag substitution b"T_lookup_j" -> b"comm_T_lookup_j" at BOTH the prover-side envelope absorb (prove_from_parts_with_logup step (7), compressed_snark.rs:2235) AND the verifier-side envelope absorb (CompressedSNARK::verify, compressed_snark.rs:2577). This is a forward-incompatible breaking change per design pin §4.4: no envelope back-compat shim. Same-tag-different-payload would silently re-derive a different challenge stream that the prover-side did not match (a Halpert-class forgery vector). Pre-flight gates (per design pin §7.3 / cryptographer-reviewer): - (a) HyperKZG batched-opening capacity: PASSED. EE::prove / EE::verify operate on a single combined polynomial built via batch_eval_reduce / batch_eval_verify (vendor/nova/src/spartan/mod.rs:393 / :452); proof overhead is O(log size_max), not O(k · log num_cons). 5th entry adds zero new opening proofs. - (b) PolyEvalInstance::batch_diff_size at length num_cons: PASSED. vendor/nova/src/spartan/mod.rs:320-362 accepts num_vars: &[usize] with L0 Lagrange-rescale; existing 4 per-table entries already at length num_cons (snark.rs:1554-1573); 5th entry is mechanically identical. - (c) Verifier cardinality check located at compressed_snark.rs:2400; updated to per_table_comm_T_lookup.len() != k. - (d) FS-tag substitution sites: 2 absorb call-sites (prover at line 2235, verifier at line 2577). Both changed. No stale b"T_lookup_j" references remain in any code path; only audit-trail commentary preserves the pre-corrigendum form. - (e) Commitment basis: PASSED. All 5 per-table commitments use prefix- basis ck.ck[..num_cons] (build_per_table_commitments delegates to E::CE::commit(ck, ..., &ZERO) identically for all 5). §7.3 acceptance gates: - (b) cargo test -p nova-snark --features lookup-fold --release --lib: 194 passed; 1 failed; 3 ignored. The single failure (neutron::tests::m_gh7_3a_prove_step_with_lookup_fold_sibling_threads_running_lws_witness_alloc_preserved_positive_path) is PRE-EXISTING on the lookup-fold baseline (verified by stashing Corrigendum microsoft#29 changes and re-running the same test; same failure) and belongs to the M.GH7.5 / Corrigendum microsoft#23 TRIAGE-ROUTED IVC-trace empirical investigation that is STRUCTURALLY ORTHOGONAL to the envelope-shape change per design pin §5.4 issue 4. Corrigendum microsoft#29 is the structural-correctness change against the current per_table_T_lookup field; Corrigendum microsoft#24+ owns the M.GH7.5 full-R1CS-sat empirical close. - Corrigendum microsoft#29-specific acceptance tests ALL PASS: * spartan::snark::tests::m_gh7_4a::m_gh7_4a_prove_with_T_claim_split_error_with_logup_round_trip ... ok * spartan::snark::tests::m_gh7_4a::m_gh7_4b_prove_with_T_claim_split_error_with_logup_pcs_opening_batched_round_trip ... ok * spartan::snark::tests::m_gh7_4a::m_gh7_4a_per_table_outer_evals_struct_field_shape ... ok * neutron::compressed_snark::tests::m_gh7_4c_compressed_snark_end_to_end_with_per_table_lookup_envelope_transcript ... ok These exercise the prover-side signature change, the verifier-side signature change, the 3+5*k u_vec extension, and the end-to-end envelope FS-tag substitution. - (c) No regression on existing vendor-side acceptance tests naming per_table_T_lookup: confirmed. The only sites are the M.GH7.4c acceptance test (which was updated to use per_table_comm_T_lookup and now asserts cardinality, not inner length) and audit-trail commentary referencing the pre-corrigendum form. Inumbra-side rebase + slice-04 envelope re-measurement is the follow-up dispatch per design pin §7.4. The forecast post-corrigendum is slice-04 ~9,810 bytes (band 9,500-10,500); the un-#[ignore] of the ceiling-asserting tests at arity_envelope_acceptance.rs:393 and :537 lands in that follow-up. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
This PR adds tests that @srinathsetty provided in
tests/num.rs. Prior to the fixes here,test_use_cs_onewas failing.It passes now, and I believe the fix is correct. The problem was that the 'one' input was not being added, so constraints referencing it were trying to index into the 0th position of a 0-element vector if no other inputs had yet been added.
test_use_cs_one_after_inputizewas not failing becauseinputizeincidentally allocates an input.The fix is to add the 'one' input when creating the constraint system. We then discard it when creating the witness, since Nova doesn't require it to be there.
This leaves the question: why or how was this correct before? The answer is that the
enforcefunction was actually doing unnecessary work in computing unused linear-combination evaluations. Nova only needs the witness assignments from the constraint system, so I also removed them. This would also fix the problem we notice, but for the sake of remaining as consistent with bellperson as possible, we should also apply the other fixes.