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