Witness Column lookup - #228
Open
mariari wants to merge 16 commits into
Open
Conversation
This changes the trace length from 2,048 to 32,768
The floating branch = "main" dependency broke: crypto-primitives main now wants crypto-bigint >=0.7.1 while the workspace pins =0.7.0-rc.9, and rev 234f101 moved cfg() behind HasPrimeFieldConfig. 9ce6d87 is the newest rev this tree compiles against. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Ten agent worktrees were committed as submodule entries with no .gitmodules URL. cargo cannot fetch this repo as a git dependency while they remain: it tries to init every submodule and fails. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
On main-beta the combined lane preserves the true residue of an assert_zero constraint (CombinedPolyRowBuilder::assert_zero), while step 2 skips zero-ideal constraints assuming the claim is zero by construction. The CPR then adopts the claimed values as its expected sums, so nothing ever asks them to vanish: an honest prover run on a false witness verified. All-zero-ideal UAIRs always take this lane; the MLE_FIRST dispatch ignores zero-ideal constraints when it classifies. Step 3 now requires, for all-zero-ideal UAIRs only, that each claimed value vanish at the projecting element (drawn after the claims are absorbed). Mixed-ideal UAIRs (SHA/ECDSA) discharge assert_zero through their own lift semantics and keep their behavior. Found by tampered-witness examples at this pin. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The verifier-side pointer query of the FOL paper (Lemma 4.2's C_i(C_j(X)) obligation), designed against the lookup-methods menu: per-position reads need no multiset argument, so the check is M0 algebra - one extra step-4 group discharges R through the existing eval cascade, and two chained plain sumchecks push eq-mass through the pointer map to read V at the committed bit columns' position. Nothing new is committed; stage 1 pays two extra int-batch openings, the same shape GKR-LogUp shipped with before its reducer. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
ComposedReadSpec carries one pointer query: a value column, the address-bit columns that spell the cube position (low bit first), and the result column the dereference lands in. Shape validation at signature construction, the num_vars check deferred to proving time where the trace size is known. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
PointerHopUair: int columns [V, bits, R], bits on the booleanity sumcheck, one declared composed read, trivially-satisfied general constraint - the read carries the soundness work. Its broken twin forges one result entry off its dereference; the e2e test demands rejection and fails today, which is the point: nothing checks the pointer query yet. The design it drives is documentation/pointer-query-design.md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sumcheck A reads the value column against the eq-mass pushed through the pointer map, anchored to the result column's already-discharged evaluation at the step-4 point; sumcheck B discharges the bridge by evaluating the eqt product over the committed bit columns. Nothing committed, nothing new at step 4; the endpoint claims wait for the protocol layer to open the int batch at the two derived points. Absence is the protocol layer's to encode. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
step4c runs the two chained sumchecks after the lookup step; the result anchor reads off the resolver's up-evals at the step-4 point, so R costs nothing. Step 6 lifts the witness-int columns at the two derived points and absorbs them; step 7 discharges the endpoint claims with two extra int-batch openings, the shape GKR-LogUp first shipped with. The proof gains a presence-flagged pointer-query section; the fold paths carry it as absent. The hop UAIR proves end to end, the forged dereference rejects from the pointer query itself, and bridge and lifted-eval tampers reject; the full suite stays green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
tau collapsed into r* during implementation - the resolver already discharges every up-eval there, so the step-4 group vanished and the R side costs nothing. The transcript-order and staging sections now describe the protocol as wired, not as first sketched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
mariari
requested review from
ElijahVlasov,
albert-garreta and
frozenspider
as code owners
July 30, 2026 14:49
Between turning a column into chunk indices and taking the parent's lift, a lookup group's proof is a function of the chunk indices and the subtable alone: the multiplicities, the challenges, both fraction trees and both GKR runs never ask what the parent was made of. That half is now prove_fraction_phase, and prove_group calls it. Nothing changes for BitPoly. The point is the seam: a second table type needs its own extraction and its own lift, and nothing in between.
Word was declared, transcribed, and given its table, subtable and shift
when GKR-LogUp was ported, and then only BitPoly was implemented. A
Word spec has had no path to a proof since: both the prover's and the
verifier's table match fell through to WitnessNotInTable.
The parents differ and nothing else does. A BitPoly cell is a
polynomial, so its chunks are coefficient blocks, its lift walks D bits,
and the chunks recombine by X^{k·cw}. A Word cell is an integer, so a
chunk is a shift and a mask, the lift is one multilinear evaluation
carried as a degree-0 polynomial, and the chunks recombine by place
value, 2^{k·cw}, which is what word_shift was always for. In between,
the fraction phase counts chunk indices and cannot tell the difference.
An integer reaches its value through ConstTranscribable, the only
integer-shaped thing the trace's cells promise. That decides the
out-of-table case for free: a negative cell transcribes with its high
bits set, reads back above every 2^width, and is refused. A range check
that refuses negatives is the whole point, so it should fall out of the
representation rather than be tested for.
A lookup spec is grouped by its table type, so every column range-checked at one width and chunk width arrives as a single Word group. That group's parents are integer columns, counted past the binary and arbitrary ones, and it proves through prove_group_word. Its claim is discharged the way the pointer query discharges r_A and r_B: the witness-int lifted evaluations at the group's own r_inner, absorbed after the r_0 evals, and one more int-batch opening at that point. The comment beside the pointer query already calls an int multipoint reducer the symmetric future fold, and that is as true here -- one opening per group is stage one, not the end state. Stage one also takes a single Word group and refuses a second, since one width and chunk width is what a range check needs and more than one wants the fold rather than an opening apiece. The verifier half follows: the lifted evals still have to reach it, which is a proof field and its transcription, and the parent claim still has to be checked against them. Until a UAIR declares a Word spec nothing here runs, and BitPoly is untouched.
The proof carries the witness-int lifted evaluations at the Word group's
r_inner, the verifier binds the group's parent claim against them, and
the extra int opening at that point is checked. Without the binding the
lookup would prove a range for numbers unrelated to the committed
columns, so that check is the whole of what makes this sound.
Three asymmetries had to be fixed to get there, each found by the
end-to-end test rather than by reading:
The bin reducer keyed off the number of lookup groups, counting a Word
group that has no bin lifts to reduce. It now counts binary groups, on
both sides, and the verifier also allows for an empty bin batch, which
the prover already did by way of its absent commitment hint.
The r_inners handed to that reducer included the Word group's, so the
prover offered a bin claim with empty lifts while the verifier had
already dropped it. Both now pass only the binary groups' points.
The prover absorbed the word lifts into the transcript and the verifier
did not, so every challenge after that point diverged and the opening
failed its proximity check. The verifier now absorbs them in the same
place, before the pointer query's.
IntWordLookupUair is four integer columns declared as one Word{16,8}
group with a trivial constraint, so proving it is exactly the claim that
every cell lies in [0, 2^16). Its test proves, serializes, deserializes
and verifies; the companion test corrupts a lifted evaluation and
requires the verification to fail.
The witness fraction tree is built over num_chunks * witness_len leaves. Both paths only ever build power-of-two trees -- BitPoly because a table of width D chunked to divide it always gives a power-of-two count, and a trace is a power of two either way -- so the padded branch that exists for the other case has never run. Word takes an arbitrary width, which made that branch reachable, and it does not hold: a chunk count of five proved and then failed verification. Refusing the shape is the honest fix. The padding is untested rather than supported, and a range check needs no width whose chunking is awkward: 20 bits in chunks of five is four chunks, and that is the whole demand. The refusal names the count, where a verifier rejection named nothing.
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
1 participant
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.
Follows the design found here:
https://github.com/NethermindEth/zinc-plus/blob/main-beta-lookup/documentation/lookup-methods-design.md
This work is based off of #main-beta-lookup, which may have issues, I'm providing this patch mainly to demonstrate what features that are required to properly have pointers in witness data be chased without manually encoding it for the verifier
Adds a lookup whose table is a committed witness column:
ComposedReadSpec { value_col, bit_cols, result_col }declaresR(x) = V(b(x))over the cube. Discharged algebraically (M0 shape) — two chained sumchecks anchored at r*, nothing extra committed, two extra int openings pending a reducer. Details, transcript order, and soundness preconditions in documentation/pointer-query-design.md.Tested e2e with tamper-rejects (
PointerHopUairand its forged twin); existing suite unaffected.