Skip to content

multi-stark: adopt flat quotient commitment (rev 678f8e1) #516

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gabriel-barrett merged 1 commit into from
Jul 25, 2026
Merged

multi-stark: adopt flat quotient commitment (rev 678f8e1) #516

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ libc = "0.2"
log = "0.4"
memmap2 = "0.9"
mimalloc = { version = "0.1", default-features = false }
multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "c178aaedaaea003331f0992d385266068cee32c8" }
multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "40092c160f51fdc2330b9e388873ece3fa4c12c2" }
num-bigint = "0.4.6"
quickcheck = "1.0.3"
quickcheck_macros = "1.0.0"
Expand Down
58 changes: 17 additions & 41 deletions Ix/MultiStark/Pcs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -678,12 +678,6 @@ def pcs := ⟦
}

-- ── reduced-opening buckets ───────────────────────────────────────────────
fn repeat_g(v: G, n: G) -> List‹G› {
match n {
0 => store(ListNode.Nil),
_ => store(ListNode.Cons(v, repeat_g(v, n - 1))),
}
}
-- 1 iff some circuit `i < rem` has log-height `log_degrees[i] + log_blowup == h`.
fn circ_has_height(log_degrees: List‹U8›, log_blowup: G, rem: G, i: G, h: G) -> G {
match rem {
Expand Down Expand Up @@ -781,29 +775,18 @@ def pcs := ⟦
}
}

-- The quotient batch: `qd` chunks per circuit, one opening point (ζ) each.
fn open_q_chunks(buckets: List‹Bucket›, idxbits: List‹G›, log_gmax: G, lh: G,
chunk: G, qrem: G, zeta: Ext, base_rows: List‹List‹U64››,
q_opened: OpenedRound, alpha: Ext) -> (List‹Bucket›, G) {
match qrem {
0 => (buckets, chunk),
_ =>
let b = ri_apply(buckets, lh, idxbits, log_gmax, zeta,
lanes_to_gl(list_lookup(base_rows, chunk)), list_lookup(list_lookup(q_opened, chunk), 0), alpha);
open_q_chunks(b, idxbits, log_gmax, lh, chunk + 1, qrem - 1, zeta, base_rows, q_opened, alpha),
}
}
-- The quotient batch: ONE wide matrix per circuit (all its coefficient
-- slices), on the trace domain, opened at the single point ζ.
fn open_quotient(buckets: List‹Bucket›, idxbits: List‹G›, log_gmax: G, log_blowup: G, ci: G,
rem: G, chunk: G, circuits: List‹SysCircuit›, log_degrees: List‹U8›, zeta: Ext,
rem: G, log_degrees: List‹U8›, zeta: Ext,
base_rows: List‹List‹U64››, q_opened: OpenedRound, alpha: Ext) -> List‹Bucket› {
match rem {
0 => buckets,
_ =>
let SysCircuit.Mk(_a, _cc, md, _ph, _pw, _w1, _w2) = list_lookup(circuits, ci);
let qd = quotient_degree_of(md);
let lh = to_field(list_lookup(log_degrees, ci)) + log_blowup;
let (b, chunk2) = open_q_chunks(buckets, idxbits, log_gmax, lh, chunk, qd, zeta, base_rows, q_opened, alpha);
open_quotient(b, idxbits, log_gmax, log_blowup, ci + 1, rem - 1, chunk2, circuits, log_degrees, zeta, base_rows, q_opened, alpha),
let b = ri_apply(buckets, lh, idxbits, log_gmax, zeta,
lanes_to_gl(list_lookup(base_rows, ci)), list_lookup(list_lookup(q_opened, ci), 0), alpha);
open_quotient(b, idxbits, log_gmax, log_blowup, ci + 1, rem - 1, log_degrees, zeta, base_rows, q_opened, alpha),
}
}

Expand Down Expand Up @@ -852,15 +835,6 @@ def pcs := ⟦
heights_all(log_degrees, log_blowup, rem - 1, i + 1))),
}
}
fn heights_quotient(circuits: List‹SysCircuit›, log_degrees: List‹U8›, log_blowup: G, rem: G, i: G) -> List‹G› {
match rem {
0 => store(ListNode.Nil),
_ =>
let SysCircuit.Mk(_a, _cc, md, _ph, _pw, _w1, _w2) = list_lookup(circuits, i);
list_concat(repeat_g(to_field(list_lookup(log_degrees, i)) + log_blowup, quotient_degree_of(md)),
heights_quotient(circuits, log_degrees, log_blowup, rem - 1, i + 1)),
}
}
fn heights_prep(log_degrees: List‹U8›, log_blowup: G, prep_indices: List‹OptIdx›, rem: G, i: G) -> List‹G› {
match rem {
0 => store(ListNode.Nil),
Expand Down Expand Up @@ -935,7 +909,7 @@ def pcs := ⟦
fn verify_one_query(idxbits: List‹G›, qp: QueryProof, alpha: Ext,
stage1: OpenedRound, stage2: OpenedRound, q_opened: OpenedRound,
prep_opt: PreprocessedOpt, s1c: MerkleCap, s2c: MerkleCap, qc: MerkleCap,
prep_commit: MerkleCap, circuits: List‹SysCircuit›, prep_indices: List‹OptIdx›,
prep_commit: MerkleCap, prep_indices: List‹OptIdx›,
log_degrees: List‹U8›, zeta: Ext, num_circuits: G, log_blowup: G, log_gmax: G,
betas: List‹Ext›, commit_phase_commits: List‹MerkleCap›, final_poly: List‹Ext›,
num_rounds: G) -> G {
Expand All @@ -954,9 +928,11 @@ def pcs := ⟦
assert_eq!(mmcs_verify(s2c, rows_s2, heights_all(log_degrees, log_blowup, num_circuits, 0), idxbits, proof_s2, log_gmax), 1);
let buckets = open_batch_2pt(buckets, idxbits, log_gmax, log_blowup, 0, num_circuits, log_degrees, zeta, rows_s2, stage2, alpha);
let BatchOpening.Mk(rows_q, proof_q) = list_lookup(input_proof, 2);
assert_eq!(eq_zero(list_length(rows_q) - list_length(q_opened)), 1);
assert_eq!(mmcs_verify(qc, rows_q, heights_quotient(circuits, log_degrees, log_blowup, num_circuits, 0), idxbits, proof_q, log_gmax), 1);
let buckets = open_quotient(buckets, idxbits, log_gmax, log_blowup, 0, num_circuits, 0, circuits, log_degrees, zeta, rows_q, q_opened, alpha);
-- one wide quotient matrix per circuit, on the trace domain, so the
-- quotient batch's heights are the same per-circuit heights as the stages
assert_eq!(eq_zero(list_length(rows_q) - num_circuits), 1);
assert_eq!(mmcs_verify(qc, rows_q, heights_all(log_degrees, log_blowup, num_circuits, 0), idxbits, proof_q, log_gmax), 1);
let buckets = open_quotient(buckets, idxbits, log_gmax, log_blowup, 0, num_circuits, log_degrees, zeta, rows_q, q_opened, alpha);
let buckets = open_prep_batch(buckets, input_proof, prep_commit, prep_opt, prep_indices, log_degrees, num_circuits, idxbits, log_gmax, log_blowup, zeta, alpha);
-- a height-`log_blowup` (constant-poly) reduced opening must be zero
let _cz = assert_blowup_zero(buckets, log_blowup);
Expand All @@ -976,7 +952,7 @@ def pcs := ⟦
fn query_loop(input: ByteStream, output: ByteStream, query_proofs: List‹QueryProof›,
alpha: Ext, stage1: OpenedRound, stage2: OpenedRound, q_opened: OpenedRound,
prep_opt: PreprocessedOpt, s1c: MerkleCap, s2c: MerkleCap, qc: MerkleCap,
prep_commit: MerkleCap, circuits: List‹SysCircuit›, prep_indices: List‹OptIdx›,
prep_commit: MerkleCap, prep_indices: List‹OptIdx›,
log_degrees: List‹U8›, zeta: Ext, num_circuits: G, log_blowup: G, log_gmax: G,
betas: List‹Ext›, commit_phase_commits: List‹MerkleCap›, final_poly: List‹Ext›,
num_rounds: G) -> G {
Expand All @@ -985,10 +961,10 @@ def pcs := ⟦
ListNode.Cons(qp, rest) =>
let (idxbits, input2, output2) = ch_sample_bits(input, output, log_gmax);
let _q = verify_one_query(idxbits, qp, alpha, stage1, stage2, q_opened, prep_opt,
s1c, s2c, qc, prep_commit, circuits, prep_indices, log_degrees, zeta, num_circuits,
s1c, s2c, qc, prep_commit, prep_indices, log_degrees, zeta, num_circuits,
log_blowup, log_gmax, betas, commit_phase_commits, final_poly, num_rounds);
query_loop(input2, output2, rest, alpha, stage1, stage2, q_opened, prep_opt,
s1c, s2c, qc, prep_commit, circuits, prep_indices, log_degrees, zeta, num_circuits,
s1c, s2c, qc, prep_commit, prep_indices, log_degrees, zeta, num_circuits,
log_blowup, log_gmax, betas, commit_phase_commits, final_poly, num_rounds),
}
}
Expand All @@ -999,7 +975,7 @@ def pcs := ⟦
fn pcs_fri_verify(post_zeta_input: ByteStream, stage1: OpenedRound, stage2: OpenedRound,
q_opened: OpenedRound, prep_opt: PreprocessedOpt, opening: FriProof,
s1c: MerkleCap, s2c: MerkleCap, qc: MerkleCap, prep_commit: MerkleCap,
circuits: List‹SysCircuit›, prep_indices: List‹OptIdx›, log_degrees: List‹U8›,
prep_indices: List‹OptIdx›, log_degrees: List‹U8›,
zeta: Ext, num_circuits: G, log_blowup: G, num_queries: G, commit_pow_bits: G,
query_pow_bits: G) -> G {
let FriProof.Mk(commit_phase_commits, pw, query_proofs, final_poly, qpw) = opening;
Expand Down Expand Up @@ -1030,7 +1006,7 @@ def pcs := ⟦
-- query indices + per-query verification (log_global_max_height = #rounds + log_blowup)
let log_gmax = num_rounds + log_blowup;
query_loop(input, output, query_proofs, alpha, stage1, stage2, q_opened,
prep_opt, s1c, s2c, qc, prep_commit, circuits, prep_indices, log_degrees, zeta,
prep_opt, s1c, s2c, qc, prep_commit, prep_indices, log_degrees, zeta,
num_circuits, log_blowup, log_gmax, betas, commit_phase_commits, final_poly, num_rounds)
}

Expand Down
117 changes: 38 additions & 79 deletions Ix/MultiStark/Verifier.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,9 @@ The Rust verifier runs these steps:
circuit it recomputes `composition(ζ)` by replaying the AIR constraint folder
(`VerifierConstraintFolder` + `LookupAir::eval`) over the deserialized
symbolic system and the opened values, recomputes `quotient(ζ)` from the
opened quotient chunks (barycentric `zps` weights over the split quotient
domains), and asserts `composition(ζ) · inv_vanishing(ζ) == quotient(ζ)`.
opened quotient coefficient slices (the power series
`Q(ζ) = Σᵢ ζ^(i·n)·cᵢ(ζ)`), and asserts
`composition(ζ) · inv_vanishing(ζ) == quotient(ζ)`.
Validated end-to-end against a real factorial proof (the `recursive-verifier`
test runner, `Tests/MultiStark.lean`): the verifier accepts the honest proof
and rejects a tampered claim.
Expand Down Expand Up @@ -475,14 +476,16 @@ def verifier := ⟦
fn verify(proof: Proof) -> G {
match proof {
Proof.Mk(_active, _commitments, accs, _log_degrees, _opening,
_quotient, _preprocessed, stage_1, stage_2) =>
quotient, _preprocessed, stage_1, stage_2) =>
-- Step 1 (shape, system-independent): the per-round opened-value lists
-- and the accumulator list all have the same length = the circuit count.
let num_circuits = list_length(accs);
-- there must be at least one circuit (Rust: InvalidSystem)
assert_eq!(eq_zero(num_circuits), 0);
assert_eq!(list_length(stage_1), num_circuits);
assert_eq!(list_length(stage_2), num_circuits);
-- one wide quotient matrix per active circuit
assert_eq!(list_length(quotient), num_circuits);

-- Step 2: accumulator balance — the last accumulator must be zero.
assert_eq!(last_acc_is_zero(accs), 1);
Expand All @@ -495,12 +498,12 @@ def verifier := ⟦
-- ==========================================================================
-- Step 5: out-of-domain (OOD) evaluation.
--
-- Mirrors the per-circuit loop in `verifier.rs::verify_multiple_claims`
-- (lines 329-434). For each circuit it recomputes the composition polynomial
-- Mirrors the per-circuit loop in `verifier.rs::verify_multiple_claims`.
-- For each circuit it recomputes the composition polynomial
-- `composition(ζ)` from the opened values by replaying the AIR constraint
-- folder (`VerifierConstraintFolder` + `LookupAir::eval`), recomputes the
-- quotient `quotient(ζ)` from the opened quotient chunks via the barycentric
-- weights `zps`, and asserts
-- quotient `quotient(ζ)` from the opened coefficient slices via the power
-- series `Q(ζ) = Σᵢ ζ^(i·n)·cᵢ(ζ)`, and asserts
-- composition(ζ) · inv_vanishing(ζ) == quotient(ζ).
--
-- The challenges (lookup, fingerprint, α, ζ) come from `fiat_shamir` above.
Expand Down Expand Up @@ -672,66 +675,28 @@ def verifier := ⟦
}

-- ==========================================================================
-- Quotient evaluation from the opened quotient chunks.
-- Quotient evaluation from the opened quotient row.
--
-- The trace domain is the order-2^L subgroup H (shift = 1). The quotient
-- domain is the disjoint coset `7·H'` of size `2^(L+log_qd)` (7 = Goldilocks
-- GENERATOR), split into `qd = 2^log_qd` chunk domains `Dⱼ` of size `2^L`,
-- shift `7·g_q^j` where `g_q = two_adic_gen(L + log_qd)`. Then
-- quotient(ζ) = Σⱼ zpsⱼ · from_ext_basis(chunkⱼ),
-- zpsⱼ = Πₖ≠ⱼ Z_{Dₖ}(ζ) / Z_{Dₖ}(first_point(Dⱼ)),
-- with `Z_{Dₖ}(x) = (x · shift_k⁻¹)^(2^L) - 1`.
-- The quotient is sliced by COEFFICIENTS — `Q(X) = Σᵢ X^(i·n)·cᵢ(X)` with
-- each `cᵢ` of degree < n = 2^L — and all `qd` slices of a circuit live in
-- one wide matrix on the trace domain, opened once at ζ. Recombination is
-- the plain power series
-- quotient(ζ) = Σᵢ ζ^(i·n) · cᵢ(ζ),
-- over the slice values reconstructed from the opened row
-- (`reconstruct_ext_row`, pairs of base coordinates → extension elements).
-- ==========================================================================

-- base-field power `base^e` (e small: the chunk index, < qd).
fn g_pow(base: Goldilocks, e: G) -> Goldilocks {
match e {
0 => 1,
_ => gl_mul(base, g_pow(base, e - 1)),
}
}

-- `Z_{Dⱼ}(x) = (x · shift_j⁻¹)^(2^L) - 1`, evaluated at extension point `x`.
fn vanish_chunk(x: Ext, l: G, shiftinv: Goldilocks) -> Ext {
eg_sub(ext_exp_pow2(eg_mul(x, [shiftinv, 0]), l), [1, 0])
}

-- `zpsₜ = Πⱼ≠ₜ Z_{Dⱼ}(ζ) / Z_{Dⱼ}(shift_t)`. Iterates j over `[jidx, jidx+rem)`.
fn zps_prod(acc: Ext, zeta: Ext, l: G, g_q: Goldilocks, shift_t: Goldilocks, jidx: G, rem: G, t: G) -> Ext {
match rem {
0 => acc,
_ =>
let shiftinv = gl_inverse(gl_mul(7, g_pow(g_q, jidx)));
-- skip the j = t factor (the chunk's own domain); branch in tail
-- position so the inner match is not a non-tail match.
match eq_zero(jidx - t) {
1 => zps_prod(acc, zeta, l, g_q, shift_t, jidx + 1, rem - 1, t),
_ =>
let factor = eg_mul(vanish_chunk(zeta, l, shiftinv),
eg_inverse(vanish_chunk([shift_t, 0], l, shiftinv)));
zps_prod(eg_mul(acc, factor), zeta, l, g_q, shift_t, jidx + 1, rem - 1, t),
},
}
}

-- `quotient(ζ) = Σₜ zpsₜ · from_ext_basis(chunkₜ)`, iterating the `qd` chunks
-- (`q_opened[idx][0] = [c0, c1]`).
fn quotient_sum(acc: Ext, zeta: Ext, l: G, qd: G, g_q: Goldilocks,
q_opened: OpenedRound, idx: G, rem: G, t: G) -> Ext {
match rem {
0 => acc,
_ =>
let shift_t = gl_mul(7, g_pow(g_q, t));
let zps_t = zps_prod([1, 0], zeta, l, g_q, shift_t, 0, qd, t);
let ch = list_lookup(q_opened, idx);
let row = list_lookup(ch, 0);
let qv = from_ext_basis(list_lookup(row, 0), list_lookup(row, 1));
quotient_sum(eg_add(acc, eg_mul(zps_t, qv)), zeta, l, qd, g_q,
q_opened, idx + 1, rem - 1, t + 1),
-- `Σᵢ powᵢ·sliceᵢ` with `powᵢ = zeta_pow_n^i` (`pow` threads the running
-- power, starting at 1).
fn quotient_eval(slices: List‹Ext›, zeta_pow_n: Ext, pow: Ext) -> Ext {
match load(slices) {
ListNode.Nil => [0, 0],
ListNode.Cons(c, rest) =>
eg_add(eg_mul(pow, c), quotient_eval(rest, zeta_pow_n, eg_mul(pow, zeta_pow_n))),
}
}

-- `quotient_degree = (max(md, 2) - 1).next_power_of_two()` and its log2.
-- `quotient_degree = (max(md, 2) - 1).next_power_of_two()`.
-- Tabulated for `max_constraint_degree ≤ 17` (covers all current circuits);
-- larger degrees fall through to the `_` arm.
fn quotient_degree_of(md: G) -> G {
Expand All @@ -744,16 +709,6 @@ def verifier := ⟦
_ => 32,
}
}
fn log_qd_of(md: G) -> G {
match md {
0 => 0, 1 => 0, 2 => 0,
3 => 1,
4 => 2, 5 => 2,
6 => 3, 7 => 3, 8 => 3, 9 => 3,
10 => 4, 11 => 4, 12 => 4, 13 => 4, 14 => 4, 15 => 4, 16 => 4, 17 => 4,
_ => 5,
}
}

-- The preprocessed opened row at ζ for circuit `i`, or `Nil` if the circuit
-- has no preprocessed trace (`preprocessed_indices[i] = None`).
Expand All @@ -772,11 +727,11 @@ def verifier := ⟦

-- Per-circuit OOD loop: for each circuit, recompute composition(ζ) and
-- quotient(ζ) and assert `composition · inv_vanishing == quotient`. Threads
-- the running lookup accumulator `accp` and the quotient-chunk offset `lastq`.
-- the running lookup accumulator `accp`.
fn ood_loop(circuits: List‹SysCircuit›, prep_indices: List‹OptIdx›,
log_degrees: List‹U8›, accs: List‹Ext›,
stage1: OpenedRound, stage2: OpenedRound, prep_opt: PreprocessedOpt,
q_opened: OpenedRound, i: G, accp: Ext, lastq: G,
q_opened: OpenedRound, i: G, accp: Ext,
lch: Ext, fch: Ext, alpha: Ext, zeta: Ext) -> G {
match load(circuits) {
ListNode.Nil => 1,
Expand All @@ -785,7 +740,6 @@ def verifier := ⟦
let SysLookupAir.Mk(air, lookups) = lair;
let l = to_field(list_lookup(log_degrees, i));
let qd = quotient_degree_of(md);
let log_qd = log_qd_of(md);
let naccp = list_lookup(accs, i);
let s1 = list_lookup(stage1, i);
let main = list_lookup(s1, 0);
Expand All @@ -797,11 +751,16 @@ def verifier := ⟦
let (isf, isl, ist, invv) = trace_selectors(zeta, l);
let comp = ood_composition(air, lookups, main, main_next, s2row, s2next,
prep, isf, isl, ist, lch, fch, accp, naccp, alpha);
let g_q = two_adic_gen(l + log_qd);
let quot = quotient_sum([0, 0], zeta, l, qd, g_q, q_opened, lastq, qd, 0);
-- circuit i's wide quotient row, its base-coordinate pairs folded back
-- into the `qd` slice values (Rust: `quotient_row.chunks_exact(D)`)
let slices = reconstruct_ext_row(list_lookup(list_lookup(q_opened, i), 0));
-- shape: `quotient_opened_values[pos][0].len() == quotient_degree · D`
-- (Rust `check_shapes`)
assert_eq!(eq_zero(list_length(slices) - qd), 1);
let quot = quotient_eval(slices, ext_exp_pow2(zeta, l), [1, 0]);
assert_eq!(eg_eq(eg_mul(comp, invv), quot), 1);
ood_loop(rest, prep_indices, log_degrees, accs, stage1, stage2, prep_opt,
q_opened, i + 1, naccp, lastq + qd, lch, fch, alpha, zeta),
q_opened, i + 1, naccp, lch, fch, alpha, zeta),
}
}

Expand Down Expand Up @@ -863,9 +822,9 @@ def verifier := ⟦
let acc0 = claims_acc([0, 0], claims, lch, fch);
-- Step 5: OOD composition/quotient identity for every active circuit.
let _ood = ood_loop(acirc, aprep, log_degrees, accs, stage1, stage2,
prep_opt, q_opened, 0, acc0, 0, lch, fch, alpha, zeta);
prep_opt, q_opened, 0, acc0, lch, fch, alpha, zeta);
pcs_fri_verify(post_zeta_input, stage1, stage2, q_opened, prep_opt, opening,
s1c, s2c, qc, prep_cap, acirc, aprep, log_degrees, zeta,
s1c, s2c, qc, prep_cap, aprep, log_degrees, zeta,
list_length(acirc), log_blowup, num_queries, commit_pow_bits,
query_pow_bits),
}
Expand Down
Loading