Suppose you pose the following problem to me: solve a large sparse linear system Ax=b, where A and b are public and x is unknown. Can I convince you that I have a good x without sending the whole vector?
The answer turns out to be yes. I can solve the system by any method I like and send a proof whose validator uses only a few megabytes of memory, even when the solution has millions of entries. At one million unknowns my exact certificate was 779,326 bytes and the experimental floating-point certificate was 478,932 bytes. Sending x itself in fp64 would take 8,388,608 bytes.
This post describes the two proof paths in my research implementation. The first converts the numerical result to fixed point and proves exact integer identities in a 192-bit prime field. The second performs the proof arithmetic in binary64 and reports tolerance-normalized defects. The fast path is much cheaper, but it is a provisional metric certificate rather than a replacement for the exact path.
The ideas are closely related to SNARKs, STARKs, and zero-knowledge proofs, but I do not claim zero knowledge here. Hiding the complete vector is useful by itself, and succinct validation does not automatically imply the stronger simulation property required for zero knowledge.
The current benchmark family is simple. A is a strictly diagonally dominant tridiagonal matrix with 1/2 on the diagonal and 1/16 immediately above and below it. b is generated from a public seed. The prover solves this system with the Thomas algorithm in fp64.
The current implementation registers this tridiagonal generator, but tridiagonal structure is not integral to the validation argument. Every finite matrix, including an arbitrary CSR matrix, has a multilinear extension. The prover only needs a generator that can produce sparse rows in random-access form, and the matrix sumcheck can then be constructed by scanning those rows without materializing a dense matrix.
To keep the validator polylogarithmic, the public generator must also express its matrix multilinear extension A~(u,v) in a form the validator can evaluate succinctly. This still leaves a great deal of descriptive power: coefficients and sparsity patterns can come from seeded formulas, finite-state or periodic rules, or multiple seeds applied to different row ranges. Such matrices can be irregular and random-looking without requiring the validator to scan every row. This is a good fit for an open benchmark challenge: publish the generator version, seeds, and row ranges as the problem, then let the validator derive the same A~(u,v) endpoint from that compact description. A generator without such an evaluator would need a separate authenticated matrix-opening argument, but it would not require changing the sumcheck relation itself.
Both paths use the residual convention
R = A x - b, or equivalently A x = b + R.
They report a squared residual score. The proof establishes that the reported score belongs to the committed solution; the application using the proof decides whether that score is small enough. This distinction is important: a perfectly valid proof can describe a poor solution with a large residual.
The public problem file selects the matrix and RHS generators, dimension, scoring rule, and exact proof profile. Both parties parse it into a canonical typed form and hash it. The validator reconstructs the statement from its own copy. It does not accept a matrix, profile, dimensions, tolerances, or proof parameters merely because the prover put them in a proof file.
The recurring trick is to replace a table by its multilinear extension. If T has 2^k entries, define
T~(y) = sum_i eq_i(y) T[i],
eq_i(y) = product_h (y_h if bit_h(i)=1 else 1-y_h).
At a Boolean point y, this polynomial returns one table entry. At a general field point it mixes the whole table in a reproducible way. Sumcheck takes a sum over the Boolean hypercube and reduces it, one coordinate at a time, to one evaluation at a random point. After k=log2(n) rounds the validator no longer has an n-term claim; it has a claim about a handful of scalar polynomial evaluations.
That last scalar must still be tied to the original private table. This is the job of the polynomial commitment. The prover commits before learning the relevant challenge, and later opens the committed polynomial at the verifier-derived point. Random challenges can be sent by a live validator or derived locally from all prior transcript messages using Fiat–Shamir. The current exact proof uses Fiat–Shamir throughout. The fast proof uses an external nonce for its first challenge, then Fiat–Shamir for the rest; I explain why below.
The exact path is named whir-field192-l2-v4. It does not prove floating-point operations. It rounds the computed solution once to Q63.64 and then proves an exact statement about those fixed-point integers.
Suppose that X_j and B_i are signed 128-bit integers representing x_j and b_i at scale 2^-64. Write each dyadic matrix coefficient as
A_ij = m_ij 2^-f, with f = 4 in the current generator.
The exact residual integer is
R_i = sum_j m_ij X_j - 2^f B_i.
Therefore
(Ax-b)_i = R_i 2^-(64+f),
rho = sum_i R_i^2,
sum_i (Ax-b)_i^2 = rho / 2^136.
X occupies the full signed 128-bit interval. R is constrained to a signed 69-bit representation, [-2^68,2^68-1]. The proof arithmetic uses a 192-bit prime field, but the validator first checks public magnitude bounds showing that neither the row equation nor rho can wrap modulo the field prime. An accepted field identity is consequently the intended integer identity.
A field element by itself does not demonstrate that it encodes an in-range signed integer. I decompose X and R into small digits:
X = sum_(k=0)^30 2^(4k) d_k + 2^124 t - 2^127 s,
R = sum_(k=0)^16 2^(4k) e_k - 2^68 z.
Here each d_k and e_k is a nibble in 0..15, t is in 0..7, and s,z are bits. This gives 33 witness columns and 18 residual columns. The 51 columns are packed into one 64 x L table, where
L = next_power_of_two(max(number of rows, 64)).
The unused index tail is zero. Six Boolean coordinates select a digit column and the remaining coordinates select a row. One WHIR Reed–Solomon polynomial commitment binds the packed table.
The following is the high-level transcript implemented by v4. P -> V denotes a prover message. V -> P denotes a random challenge. Every V -> P line could be a literal interactive validator message. In the implemented proof it is instead a local Fiat–Shamir step: both sides hash the public statement and all messages above that line and obtain the same challenge.
# Public statement and fixed protocol configuration.
# The validator derives these independently from problem.json.
V: problem_digest, profile=whir-field192-l2-v4,
Field192 modulus, WHIR parameters, digit layout, dimensions
# One commitment binds all 51 private digit columns before challenges.
P -> V: WHIR commitment C to packed digit table D
P -> V: exact residual numerator rho
# Challenge may come from V, or FS(C, rho, statement, ...).
V -> P: random row point r and combiners alpha, beta_x, beta_r
# Sumcheck 1: every digit is in its exact domain and padded rows are zero.
# q_c has roots 0..15, 0..7, or 0..1 depending on the column.
P proves:
sum_Y eq(r,Y) [
sum_c alpha^c q_c(D_c(Y))
+ beta_x witness_tail(Y) X(Y)
+ beta_r residual_tail(Y) R(Y)
] = 0
for round h = 0 .. log2(L)-1:
P -> V: univariate round polynomial g_h
V -> P: challenge r_h # interactive or Fiat--Shamir
# The endpoint digit values are recorded now and authenticated by WHIR later.
P -> V: digit-column evaluations at the range endpoint
# Choose a random row compression point.
V -> P: u # interactive or Fiat--Shamir
V: evaluate public B~(u) from the registered RHS generator
# Sumcheck 2: compressed sparse matrix-vector identity.
P: scan sparse rows and form A_u[j] = sum_i eq_i(u) m_ij
P proves:
sum_j A_u[j] X_j = 2^f B~(u) + R~(u)
for round h = 0 .. log2(L)-1:
P -> V: degree-two round polynomial g_h
V -> P: challenge v_h # interactive or Fiat--Shamir
P -> V: digit evaluations reconstructing X~(v) and R~(u)
V: compute registered A~(u,v) in O(log n), without scanning rows
V: check final claim = A~(u,v) X~(v)
# Sumcheck 3: the reported score is the committed residual norm.
P proves:
rho = sum_i R_i R_i
for round h = 0 .. log2(L)-1:
P -> V: degree-two round polynomial g_h
V -> P: challenge w_h # interactive or Fiat--Shamir
P -> V: digit evaluations reconstructing R~(w)
V: check final claim = R~(w)^2
# Authenticate every private endpoint used above against C.
# V derives all 120 selector/index opening points; P does not choose them.
P -> V: one batched WHIR opening proof for the 120 claimed evaluations
V: verify WHIR's Reed--Solomon proximity/folding argument and Merkle paths
V: verify WHIR's deferred final claim and require strict end-of-file
There are three algebraic arguments because they establish different facts. The range/padding argument gives the field elements their integer meaning. The matvec argument binds R to AX-B. The norm argument binds rho to R. WHIR then binds every private scalar used at those endpoints to the one committed table. Omitting any one of these connections leaves a real gap.
The configured WHIR commitment uses BLAKE3 Merkle hashing, unique decoding, a starting inverse rate of two, folding factor four, no proof-of-work bits, and at least 128 bits of computed security. The proof artifact cannot ask the validator to weaken these parameters.
The exact path is far cheaper than my original wide STARK traces, but its prover still carries range digits, large field elements, Reed–Solomon codewords, and Merkle trees. For a quick check-in I wanted something closer to the arithmetic the solver already performs.
The fast path fixes a binary64 contract and proves approximate consistency under fixed tolerances. It rejects NaNs, infinities, negative zero, and source subnormals; uses round-to-nearest without fused multiply-add; and fixes the operation order. The current prover converts the Q63.64 witness deterministically to binary64 and computes
R = A x - b
in that contract. It pads x and R to N=next_power_of_two(n) and packs
W = [x_0,...,x_(N-1), R_0,...,R_(N-1)].
This transcript contains neither vector.
My first version used nodal Chebyshev interpolation. That was a useful route to a stable real code, but it did not preserve the tensor structure needed to open an arbitrary multilinear functional succinctly. The current policy uses a coefficient-aligned unit-circle code instead.
Let M=2N=2^k. I bit-reverse W into monomial coefficients,
coefficient[bit_reverse(i,k)] = W[i],
then evaluate the resulting degree-M-1 polynomial on all 2M-th roots of unity. This produces a rate-one-half codeword of 2M=4N complex binary64 values. A Merkle tree commits the codeword.
This is still closely connected to Chebyshev polynomials. On z=exp(i theta), Chebyshev terms are the symmetric Laurent terms (z^j+z^-j)/2. The complex lift is what makes the fold stable. For
p(z) = E(z^2) + z O(z^2),
the validator recovers
E(z^2) = (p(z)+p(-z))/2,
O(z^2) = (p(z)-p(-z)) conjugate(z)/2.
Since |z|=1, multiplication by conjugate(z) cannot amplify error through a small 1/x denominator. Bit reversal makes this even/odd coefficient fold agree with folding one coordinate of the multilinear table.
The fast path needs one extra ordering rule. The prover first sends a 204-byte precommitment containing the problem digest, dimensions, source digests, and packed codeword root. Only after the issuer has recorded those exact bytes does it issue a fresh one-shot nonce. This prevents the prover from regenerating commitments until it finds favorable sample paths and also gives the provisional check-in useful timestamp semantics.
After that nonce, every challenge is Fiat–Shamir derived. A pure noninteractive version could replace the issuer nonce with a hash of the initial root and public statement. It would have the same proof sequence, but no external timestamp and a weaker practical defense against grinding. Conversely, every Fiat–Shamir line below could be a fresh interactive validator challenge.
# Before the initial random challenge exists:
P -> V: precommitment SFCOM containing root C_0 of the rate-1/2 code of W
V: record SFCOM or its digest
V -> P: fresh one-shot nonce eta # or local FS for offline mode
# Bind the complete numerical policy before drawing algebraic challenges.
transcript <- problem digest, dimensions, binary64 contract,
fixed tolerances, q=64, C_0, eta
# Floating sumcheck 1: report and reduce the residual norm.
P -> V: rho = sum_i R_i^2
P proves approximately:
rho ~= sum_i R_i R_i
for round h = 0 .. log2(N)-1:
P -> V: degree-two binary64 round polynomial g_h
V -> P: dyadic challenge u_h # interactive or Fiat--Shamir
P -> V: claimed R~(u)
V: check the endpoint approximately against R~(u)^2
# Floating sumcheck 2: reduce Ax=b+R using the same row point u.
V: compute registered b~(u), without scanning n rows
P proves approximately:
sum_j [sum_i eq_u(i) A_ij] x_j ~= b~(u) + R~(u)
for round h = 0 .. log2(N)-1:
P -> V: degree-two binary64 round polynomial g_h
V -> P: dyadic challenge v_h # interactive or Fiat--Shamir
P -> V: claimed x~(v)
V: compute registered A~(u,v) in O(log n)
V: check the final product approximately
# These two endpoint claims are not yet authenticated merely because C_0 exists.
# Batch them into one linear functional of the committed W.
V -> P: alpha in [1/4,3/4) # interactive or Fiat--Shamir
claim = x~(v) + alpha R~(u)
L(W) = <W, [eq_v || alpha eq_u]>
# Floating sumcheck 3: prove that the claimed endpoints come from W.
P proves approximately:
claim ~= L(W)
for opening round h = 0 .. log2(2N)-1:
P -> V: degree-two binary64 round polynomial g_h
V -> P: dyadic challenge gamma_h # interactive or Fiat--Shamir
# Fold the committed coefficient oracle by this same challenge.
P: C_(h+1) = Merkle root of folded child oracle
P -> V: C_(h+1)
# The child root is bound before the next challenge is derived.
P -> V: claimed packed endpoint W~(gamma)
V: independently evaluate the structured covector at gamma
V: check the final linear-opening product approximately
# Only now derive the locations to inspect.
V: derive up to 64 recursive query trajectories from the transcript
P -> V: canonical Merkle multiproof for selected p_h(z), p_h(-z), and children
V: authenticate queried values against every C_h
V: recompute each expected unit-circle fold within its tolerance
V: recompute the final two-leaf root and compare its constant with W~(gamma)
The third sumcheck is not decorative. The first two arguments end at values R~(u) and x~(v) supplied by the prover. A Merkle root plus random codeword queries shows proximity to a low-degree object, but does not by itself prove an arbitrary linear functional of that object. The batched opening sumcheck is the bridge from those application claims to the committed W. This was also the step that allowed the validator to stop materializing x and R.
The query multiproofs carry selected complex values and one copy of every missing sibling subtree on their joint Merkle frontier. Indices are not sent by the prover; the validator derives, sorts, and deduplicates them. The validator rejects missing, extra, reordered, noncanonical, truncated, or trailing material.
The prover cannot choose its tolerances. Policy 2 fixes ordinary algebraic checks at
absolute tolerance = 2^-42,
relative tolerance = 4096 epsilon_binary64,
and recursive folds at
absolute tolerance = 2^-38,
relative tolerance = 131072 epsilon_binary64.
For each checked relation the validator computes
normalized defect = |observed defect| /
(absolute allowance + relative allowance * operand scale).
The operand scale includes the inputs to the operation, not only a possibly tiny result after cancellation. Fold scaling, for example, includes both authenticated parent magnitudes and the actual and expected child magnitudes. The transcript reports maximum absolute defect, maximum normalized defect, RMS normalized defect, and threshold exceedances separately for norm sumcheck, matvec sumcheck, linear opening, and unit-circle folds. The convenience Boolean passes only if every maximum normalized defect is at most one.
With q distinct queries, a fixed round whose relation is bad on fraction phi of its domain is missed with probability at most
(1-phi)^q.
The validator reports this conditional curve for hypothetical bad fractions of 1%, 5%, and 10%. I do not multiply those numbers across rounds: trajectories are reused, and the implementation does not yet have a theorem showing that every materially false opening creates a specified metric bad fraction.
The commitment ordering, Merkle binding, strict framing, independently evaluated public endpoints, and polylogarithmic validation are ordinary rigorous protocol properties. The global numerical soundness statement is the experimental part. Recent work on approximate sumcheck gives strong theoretical support for this direction—especially over the complex unit circle—but I have not proved that this particular composition of FFT error, dyadic challenges, folds, batching, and local tolerances inherits one final soundness-versus-defect bound. I therefore use this as a fast provisional check, followed by the exact certificate.
The benchmark problem at every size is the same seeded, diagonally dominant tridiagonal family with a reported squared-L2 residual. Proof / solution compares the proof file with the 8n bytes required to send x in fp64. This is the useful transport baseline even though the exact proof internally commits a 16-byte Q63.64 integer per solution entry.
These release runs used eight Rayon threads on an AMD EPYC 7B12 VM with 31 GiB RAM and no swap. GNU time measured peak RSS. All proofs passed independent validation.
n | Prove wall | Prover RSS | Validator RSS | Proof bytes | fp64 solution bytes | Proof / solution |
|---|---|---|---|---|---|---|
| 1,024 | 0.38 s | 16.92 MiB | 5.65 MiB | 361,958 | 8,192 | 44.184326 |
| 2,048 | 0.66 s | 31.05 MiB | 5.83 MiB | 385,742 | 16,384 | 23.543823 |
| 4,096 | 1.22 s | 48.98 MiB | 6.07 MiB | 407,150 | 32,768 | 12.425232 |
| 8,192 | 2.40 s | 90.29 MiB | 6.23 MiB | 430,046 | 65,536 | 6.561981 |
| 16,384 | 4.61 s | 147.39 MiB | 6.23 MiB | 523,054 | 131,072 | 3.990585 |
| 32,768 | 9.06 s | 344.76 MiB | 6.54 MiB | 551,670 | 262,144 | 2.104454 |
| 65,536 | 18.16 s | 575.40 MiB | 6.43 MiB | 579,382 | 524,288 | 1.105083 |
| 131,072 | 36.68 s | 1,363.24 MiB | 6.70 MiB | 607,654 | 1,048,576 | 0.579504 |
| 262,144 | 71.82 s | 2,287.03 MiB | 7.05 MiB | 716,630 | 2,097,152 | 0.341716 |
| 524,288 | 144.75 s | 4,569.60 MiB | 7.21 MiB | 750,686 | 4,194,304 | 0.178977 |
| 1,048,576 | 291.16 s | 9,133.25 MiB | 7.41 MiB | 779,326 | 8,388,608 | 0.092903 |
The exact proof becomes smaller than the fp64 solution between 65,536 and 131,072 unknowns. At 1,048,576, it is 9.29% of the solution. Validator RSS stays between 5.65 and 7.41 MiB while prover memory grows to about 8.9 GiB. At that largest size the validator performs no matrix-row queries; it evaluates the registered public matrix in 60 logarithmic steps and the fixed-period RHS in 1,024 terms.
The final policy-2 measurements used eight Rayon threads on an Intel Core i7-1360P with rustc 1.94.0-nightly. Fast prover RSS is the maximum of the separate fast-commit and fast-prove processes. Proof bytes exclude the independently retained 204-byte precommitment. Every case used 64 recursive query trajectories and passed the fixed consistency policy.
n | Commit | Prove | Fast prover RSS | Validator RSS | Proof bytes | fp64 solution bytes | Proof / solution |
|---|---|---|---|---|---|---|---|
| 1,024 | 0.01 s | 0.03 s | 4.01 MiB | 3.94 MiB | 64,036 | 8,192 | 7.816895 |
| 2,048 | 0.01 s | 0.05 s | 4.38 MiB | 4.16 MiB | 86,236 | 16,384 | 5.263428 |
| 4,096 | 0.02 s | 0.10 s | 4.67 MiB | 3.86 MiB | 117,428 | 32,768 | 3.583618 |
| 8,192 | 0.05 s | 0.21 s | 5.35 MiB | 4.00 MiB | 146,828 | 65,536 | 2.240417 |
| 16,384 | 0.09 s | 0.42 s | 7.42 MiB | 4.15 MiB | 184,612 | 131,072 | 1.408478 |
| 32,768 | 0.19 s | 0.82 s | 10.65 MiB | 4.12 MiB | 219,292 | 262,144 | 0.836533 |
| 65,536 | 0.38 s | 1.65 s | 18.09 MiB | 4.07 MiB | 265,300 | 524,288 | 0.506020 |
| 131,072 | 0.77 s | 3.34 s | 32.68 MiB | 4.37 MiB | 311,500 | 1,048,576 | 0.297070 |
| 262,144 | 1.57 s | 6.62 s | 61.32 MiB | 4.44 MiB | 358,212 | 2,097,152 | 0.170809 |
| 524,288 | 3.21 s | 13.31 s | 119.48 MiB | 4.50 MiB | 428,316 | 4,194,304 | 0.102118 |
| 1,048,576 | 6.50 s | 26.87 s | 235.48 MiB | 4.54 MiB | 478,932 | 8,388,608 | 0.057093 |
The fast proof becomes smaller than sending fp64 x at 32,768 unknowns. At one million unknowns it is 5.71% of the solution, the prover peaks at 235.48 MiB, and the validator peaks at 4.54 MiB. Validation takes about 0.01 seconds. It processes 61 sumcheck rounds, 183 sumcheck scalar values, 60 registered-matrix steps, 1,024 RHS terms, and 17,942 Merkle hashes while materializing zero solution, residual, or codeword elements.
The exact million-row run and fast million-row run used different processors, so I do not turn their wall times into a controlled speedup claim. Their scaling and artifact sizes are still the main point: the validator stays tiny, and both proofs eventually become much smaller than the vector they validate.
This appendix gives the role of each component without trying to reproduce the papers.
A multilinear extension turns a power-of-two table into a polynomial that agrees with the table on the Boolean hypercube. Equality polynomials eq_i(y) select one Boolean index and become random linear weights away from the hypercube. They let a validator compress rows, columns, and packed table selectors into a few scalar evaluations.
The important implementation detail is coordinate order. The exact packed digit table and fast packed [x||R] table use fixed, documented conventions. The fast code bit-reverses monomial coefficients specifically so its even/odd polynomial fold matches the first-coordinate fold of the MLE.
Sumcheck proves a hypercube sum of a low-degree multivariate polynomial. In each round the prover sends a univariate polynomial describing the sum over all remaining Boolean coordinates. The validator checks that its values at zero and one add to the previous claim, then chooses a random coordinate and continues. After log2(n) rounds only one point remains.
The exact path uses classical finite-field sumcheck. The fast path performs the same reductions in binary64 and replaces equality with a scale-aware defect test. Its dyadic challenges have 52 random fractional bits, so they are exactly representable as binary64 values.
The exact proof needs to know that committed field elements are really small signed digits. For a digit domain S, the polynomial
q(T) = product_(a in S) (T-a)
vanishes exactly on S. A random linear combination checks all digit columns in one sumcheck. Separate tail-selector terms force the padded witness and residual rows to zero. Applying q after multilinear extension would be unsound in general, so the endpoint check evaluates the nonlinear digit polynomials on authenticated digit openings exactly as specified.
A Reed–Solomon code evaluates a low-degree polynomial at more points than are needed to specify it. Different low-degree polynomials differ in many locations, which makes random queries useful for detecting a corrupted alleged codeword.
The exact path uses Reed–Solomon encoding inside WHIR. The fast path evaluates a binary64 coefficient polynomial on twice as many unit-circle points as coefficients. In exact real arithmetic this is still a linear polynomial code. Under tolerances, however, the useful interpretation is metric: sampling detects a defect in proportion to the fraction of the domain on which it exceeds the declared scale.
A Merkle root commits a large vector using one hash. An opening includes selected leaves and the sibling hashes needed to recompute the root. The fast path combines all selected leaves in a round into one canonical multiproof, so shared sibling subtrees appear once. The proof carries no query indices because the transcript already determines them.
Merkle binding says that the prover cannot change an authenticated leaf without a BLAKE3 collision. It does not by itself establish low degree or the value of an arbitrary linear functional; those are separate algebraic jobs.
FRI recursively folds a Reed–Solomon code and randomly checks consistency between parent and child oracles. WHIR is a constrained Reed–Solomon proximity protocol that directly supports multilinear queries and serves as the exact path’s polynomial commitment. My implementation pins one WHIR revision and configuration rather than accepting security parameters from the proof.
The fast path borrows the recursive-fold shape but uses its own complex binary64 unit-circle code and metric checks. It should not be described as inheriting the finite-field theorem merely because the transcript resembles FRI.
Chebyshev polynomials satisfy
T_j(cos theta) = cos(j theta) = (z^j + z^-j)/2,
z = exp(i theta).
This connects stable cosine/Chebyshev representations on [-1,1] with Laurent polynomials on the complex unit circle. My initial fast design used Chebyshev nodal interpolation. The implemented design retains the well-conditioned unit-circle fold but uses monomial coefficients aligned with the multilinear table. That alignment, rather than Chebyshev interpolation by itself, is what makes the final linear-functional opening succinct.
A polynomial commitment binds a polynomial and later proves its value at a point. The exact path delegates this to WHIR. The fast path builds the needed opening from a sumcheck plus recursively committed code folds and Merkle multiproofs.
This distinction caught a real bug in the first design: proving low-degree proximity does not authenticate a prover-supplied MLE endpoint. The third fast sumcheck proves the batched linear functional
x~(v) + alpha R~(u)
against the packed committed table.
An interactive validator can choose every challenge after receiving the message it depends on. Fiat–Shamir replaces that communication with a hash of the statement and transcript prefix. Changing an earlier message then changes every later challenge.
The exact proof is one self-contained Fiat–Shamir artifact. The fast path keeps an external initial nonce because it is intended for provisional timestamping and because it limits commitment grinding. Once the nonce is issued, the rest is Fiat–Shamir. An offline pure-Fiat–Shamir fast artifact is possible, but it would not establish that the root existed before an external event.
The exact path uses ordinary numerical fp64 to find a solution, rounds it once to Q63.64, and proves the resulting integer relation. Field192 is large enough for the range-constrained row identities and rho, but only because the validator checks the generator-derived no-wrap bounds first. “Exact proof” here means exact for the quantized witness, not that the original floating solve had no rounding error.
The fast path treats tolerance as protocol data, not a prover excuse. Absolute and relative allowances, the floating-point contract, challenge distribution, and query count are fixed before challenges. The score reports observed defect divided by the validator-computed allowance. This makes a fast transcript auditable even though its acceptance semantics are metric rather than an exact field identity.
Succinct sumcheck validation ends at evaluations such as A~(u,v) and b~(u). If the validator computed those by scanning the matrix and RHS, the proof would not be useful. The current tridiagonal and seeded-RHS generators have reviewed direct evaluators: matrix work is O(log n) and RHS work is bounded by its fixed 1,024-term period. General sparse matrices need an equivalent authenticated construction.
This project started by encoding the whole validation as a STARK. The validator was small and the STARK did what it promised, but the prover trace became very wide: hundreds of columns were needed for fixed-point limbs, carries, row slots, range checks, and lookup arguments. I reached dimension 4,096 with the compact trace profiles, but the prover constant was too large for the systems I wanted to test.
The current exact v4 path is STARK-free. It commits one packed digit table and uses three sumchecks plus WHIR openings. This is the version whose million-row numbers I report above.
The concrete result is that I can validate a sparse solve without sending or materializing the full solution on the validator. The exact path proves the Q63.64 matrix-vector identity and exact squared residual numerator with classical field soundness. The fast path checks an authenticated floating-point transcript, surfaces tolerance provenance, and reaches the committed table through a genuine linear-functional opening rather than trusting endpoint attestations.
For the tested family, the exact proof becomes smaller than an fp64 solution at 131,072 unknowns and the fast proof crosses over at 32,768. At one million unknowns both validators remain under 8 MiB RSS, despite the solution itself being 8 MiB and the conceptual encoded objects being much larger.
The project is still research code. WHIR is a pinned academic prototype, the current public matrix evaluator is generator-specific, neither path is zero knowledge, and the fast path still needs a global metric soundness theorem. But the basic system is working: a researcher can pose a problem larger than their validation machine, receive a small artifact, and check a claimed residual without first obtaining the entire answer.