Use bellperson v0.19.0.#18
Merged
Merged
Conversation
iontzialla
pushed a commit
to iontzialla/Nova
that referenced
this pull request
Apr 2, 2022
Co-authored-by: porcuquine <porcuquine@users.noreply.github.com>
marcus-sa
added a commit
to marcus-sa/Nova
that referenced
this pull request
May 15, 2026
…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>
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.
PR to use the latest bellperson, which supports 'instance aggregation' and is needed to allow Groth16 proofs somewhat structurally comparable to Nova proofs.