Matrix multiplication

Checkpoint: CP-003 Status: COMPLETE. Run 2026-09-01. Mechanisms under test: Freivalds' algorithm (1977) — exact, floating-point, and (variant D, added after E009-pre) over a prime field Machine: Apple M5, 10 cores, 25.8 GB, NumPy 2.5.2 + Accelerate

Question — the programme's stated first research question

Can we verify a large matrix multiplication substantially more cheaply than recomputing it, while minimising trust assumptions?

Answer

Yes, by 43.7× at n = 8192, with soundness error ≤ 2^-40 and no cryptographic assumptions — but the clean guarantee holds only for exact arithmetic. In floating point the mechanism degrades to an approximate-correctness check whose real security is a measured perturbation threshold, not 2^-k.

Compare Experiment 001, same machine, same claim, level L5: R_verify between 49 and 8.2 × 10^7. Nine orders of magnitude on the same metric.

Files

Raw records: ../../benchmarks/results/003-matrix-multiplication.jsonl

Scope qualifier added after E016. R_verify = 0.023 is a compute ratio, and it assumes the verifier already holds A and B. That is true for a single matmul the coordinator owns, and false inside a pipeline, where operands live only on the provider's machine. E016 measured the cost of moving them and found it dominates by 3–5 orders of magnitude. See ../016-verification-bandwidth/.

The fix, also measured (variant D)

Exact arithmetic over F_p removes the tolerance and therefore the entire failure mode E009-pre exposed:

Exact arithmetic costs 2× and buys back the whole guarantee. See analysis-field.md.

The caveat that matters most — now measured

The floating-point tolerance was derived from one library on one device. E009-pre has since measured cross-backend divergence: the tolerance must inflate 191–381× to accept an honest GPU, and at that width a bfloat16 cheat is no longer detectable. The cost results above are unaffected; the float-domain security analysis holds only for a homogeneous CPU-class network. See ../009-probabilistic-verification/.

Research question (CP-003) — the programme's stated first research question

Can we verify a large matrix multiplication substantially more cheaply than recomputing it, while minimising trust assumptions?

Why matrix multiplication, and why now

Three independent reasons converge on it:

1. It is the primitive of neural inference. A transformer forward pass is overwhelmingly matmul.
2. ZIP's own measurements say so. In ZIP's mini-BERT pipeline, the linear layers cost 34.53 of 37.06 prover-hours — 93% — even though they are already handled by the cheap Freivalds-style method, and even though ZIP's contribution is an optimisation of the non-linear layers. Whatever remains expensive in ZKML is linear algebra.
3. It is the one place in this whole problem where a classical result gives R_verify ≪ 1 outright: Freivalds (1977) verifies A·B = C in O(n²) against O(n³) to recompute.

E001 measured a general zkVM at R_verify ≈ 10^7. If Freivalds delivers R_verify ≈ 10^-2 on the same machine, the two results together — a 9-order-of- magnitude spread on the same metric — are the strongest available argument that the architecture question is not "which proof system" but "which claim do we actually need".

Hypotheses

H3a. For exact arithmetic, Freivalds achieves R_verify < 0.1 at soundness error ≤ 2^-40, with the advantage growing linearly in n (since the ratio is k·n²/n³ = k/n).

H3b (the interesting one). The textbook guarantee does not survive floating point. Freivalds' soundness proof assumes exact field arithmetic. Real matmul rounds, so an honest prover produces a nonzero residual, so the verifier needs a tolerance τ, and any τ > 0 admits corruptions of C that hide inside it. The security statement therefore degrades from "soundness error 2^-k" to "C is within τ of A·B along k random directions".

• This is the hypothesis most likely to matter, and the one most likely to be glossed over in a system paper. If confirmed, then any float-domain probabilistic matmul check is an approximate-correctness mechanism, and it must be described that way.

H3c. The magnitude of a hideable corruption scales with ‖A‖·‖B‖·√n·ε (the rounding noise floor), not with the size of the corruption relative to the answer. If so, the mechanism is strong against gross cheating (returning garbage, using a much smaller model) and weak against subtle cheating (slightly wrong quantisation) — which is precisely the trade-off Nodus needs to know about, because gross cheating is what a rational provider actually does.

H3d. Freivalds cannot support Claims B, C, or D at all, and does not make the verifier weak: the verifier must still touch A and B, which is O(n²) memory traffic. It is cheap verification, not succinct verification. A third party who does not hold the operands gets nothing from it.

Predictions (recorded before running)

What a negative result would mean

If the float tolerance turns out to admit corruptions comparable to a real model-substitution error, then probabilistic matmul checking cannot police the attacks Nodus actually cares about (T3/T4/T7), and the L3 branch must be rebuilt around exact arithmetic — which in practice means quantised integer inference, which is a constraint on the whole network, not just on verification. That would be a major architectural finding and is worth the afternoon it costs to establish.

Implementation: implementation/freivalds.py. NumPy + the platform BLAS (Accelerate on Apple Silicon). No cryptography, deliberately: this measures the classical probabilistic mechanism so that later cryptographic mechanisms have something honest to be compared against.

The check

For A, B, C of size n×n, draw R of size n×k and accept iff

    A · (B · R)  ==  C · R

Cost O(k·n²) versus O(n³) to recompute A·B. Batching the k rounds into one n×k right-hand side keeps the verifier on BLAS-3 paths, so the comparison against the native matmul is fair on the same hardware and the same library rather than pitting an optimised matmul against a hand-rolled loop.

Variant A — exact

Operands are integers in [0, 2^13) stored as float64. Every intermediate value in both the matmul and the check stays below 2^53, so float64 arithmetic is exact and the classical soundness argument applies unmodified:

if A·B ≠ C, then for r uniform on {0,1}^n, Pr[A(Br) = Cr] ≤ 1/2; over k independent rounds, Pr[accept] ≤ 2^-k. One-sided: an honest C is always accepted.

Bound check for the largest configuration (n = 4096, 13-bit entries): A(Br) < 2^13 · (2^13 · 2^12) · 2^12 = 2^50 < 2^53. ✓

Negative control. Every exact run also verifies a C with a single entry corrupted by +1 — the smallest possible integer error — and requires it to be rejected. A run where the honest matrix passes but the corrupted one also passes is reported as a failure, not quietly dropped.

Variant B — floating point, with tolerance

Genuine float32 / float64 standard-normal operands. Because the arithmetic rounds, A(Br) − Cr ≠ 0 even for an honest C.

1. Measure the honest residual ‖A(Br) − Cr‖_∞ over 64 rounds.
2. Set τ = 4 × (worst honest residual). Arbitrary but stated; a real system would derive τ from a backend-specific error model.
3. Re-run the check with k rounds and confirm the honest C passes.

Variant C — adversary against the tolerance

With τ fixed by B, perturb one entry of C by τ·2^e for increasing e and record the smallest perturbation the check actually detects. This number, not 2^-k, is the security statement for the float variant, and reporting it is the whole point of the variant.

Metrics

Standard harness record. The decisive columns:

• native_seconds — recomputing A·B. This is the re-execution baseline.
• verify_seconds — the check.
• R_verify = verify / native. Below 1 means cheaper than re-execution.
• verifier_advantage = native / verify.
• soundness error, stated as a number for A and as a measured perturbation threshold for B/C.

Timings are best-of-3 to suppress scheduler noise. Sizes n ∈ {256 … 4096}, k = 40 (soundness error ≤ 2^-40 ≈ 9×10^-13 in the exact variant).

Known limitations, stated up front

• The verifier must hold A and B. Freivalds does not let a third party who lacks the operands check anything. For Nodus this means the coordinator must hold the weights — true today, but it forecloses weight privacy, which is exactly the thing ZK buys.
• The randomness must be unpredictable to the prover and chosen after C is fixed. Otherwise the prover returns C + E for any E with E·R = 0. In a real deployment this is a commit-then-reveal problem, not a maths problem.
• No Claim B/C/D. A cached C passes forever.
• Single machine, one BLAS, one run per configuration.

Status: complete for the classical (non-cryptographic) mechanism. Date: 2026-09-01. Machine: Apple M5, 10 cores, 25.8 GB, NumPy 2.5.2 + Accelerate. Raw records: ../../benchmarks/results/003-matrix-multiplication.jsonl Tables: results/summary.md

---

1. Answer to CP-003

Yes. A 8192×8192 matrix multiplication can be verified 43.7× more cheaply than recomputing it, with a soundness error of ≤ 2^-40 and no cryptographic assumptions whatsoever.

(exact-arithmetic variant. The float64 variant converges to the same figures as n grows — 0.186 / 0.098 / 0.048 / 0.0234, i.e. within 2.2% at n=8192 — while float32 is consistently ~2× worse in ratio terms because its native matmul is faster but its check is bound by the same memory traffic.)

The advantage doubles as n doubles, exactly as the k·n² vs n³ scaling predicts. Extrapolating, a 32768×32768 product would verify ~175× cheaper.

Sanity checks that had to pass, and did: the honest product was accepted in every one of the 18 configurations, and in the exact variant a C with a single entry off by +1 — the smallest possible integer error — was rejected every time.

Set against Experiment 001

Same metric, same machine, same week:

That is a spread of roughly nine orders of magnitude on verification cost, between two mechanisms that both establish Claim A. The difference is not implementation quality. It is that Freivalds exploits the algebraic structure of the statement, while a zkVM proves a RISC-V execution trace and is charged for every load, branch and index computation on the way.

This is the single most decision-relevant result the programme has produced so far, and it did not require any cryptography.

---

2. The cost is not k/n — it is about 5× worse, and that is worth knowing

Theory says R_verify = k·n²/n³ = k/n. At n=8192, k=40 that is 0.0049. We measured 0.023, a 4.7× penalty, stable across every size.

The reason is instructive: A@B is the single most heavily optimised kernel in computing — blocked, vectorised, near-peak FLOPs. The Freivalds check is a chain of thin matrix products (n×n · n×40), which is memory-bandwidth bound: it reads all of A, B and C and does only ~40 useful operations per element read. So the check pays roughly full price for the memory traffic while getting none of matmul's arithmetic-intensity advantage.

Consequence for any future design: the theoretical asymptotic advantage of a verification scheme is an upper bound that hardware will erode. When quoting R_verify for anything, quote the measured one.

---

3. Floating point: H3b confirmed, H3c confirmed with numbers

This is the part that matters for a real network, and it is where the textbook result stops applying.

Freivalds' soundness proof assumes exact arithmetic. Real matmul rounds, so an honest prover already produces a nonzero residual ‖A(Br) − Cr‖, so the verifier needs a tolerance τ, and any τ > 0 admits corruptions that hide inside it. The clean claim "soundness error ≤ 2^-40" does not survive the move to floating point, and calling a float-domain check "Freivalds with 2^-40 soundness" would be wrong.

Measured honest residuals and what they permit (τ = 4× the worst honest residual over 64 rounds):

The adversary model matters by √n

The single-entry attacker is the weakest one. Because the check multiplies by a random R, corrupting m entries with random signs produces a residual growing like √m·δ while injecting m·δ of total error — so spreading buys the attacker a factor ≈ √m of hidden corruption. Measured, this is exactly what happens:

Had we only run the point attack — the obvious thing to test — we would have overstated the mechanism's security by ~1.5–2 orders of magnitude. Recorded here because it is a general lesson for this programme: the first adversary you think of is the weakest one, and quoting its threshold is not a security analysis.

The honest security statement

Taking the spread attacker as the reference, at n=8192/float32 the check detects any corruption above ≈ 6×10^-3 per entry against entries whose typical magnitude is ~72 — i.e. it detects systematic relative deviations above roughly 10^-4 per element. Therefore:

• Gross cheating is comfortably detected. Substituting a different or smaller model, skipping layers, or fabricating output produces relative errors of 10^-2–10^0. Detection margin: 2–4 orders of magnitude.
• Precision cheating: detected, but not by much — RETRACTED. This paragraph originally claimed a provider computing in bfloat16 while claiming float32 would be caught with ~40× margin. E009-pre measured that directly and falsified it. Against a real Metal GPU backend, τ must inflate 191–381× to accept the honest GPU, and at that width the bfloat16 cheat passes at every size tested. Honest CPU-vs-GPU divergence is within a factor of 3.7 of the divergence a precision cheat produces — no threshold separates them. The claim holds only for a homogeneous CPU-class network, where the separation is ~2,800×. See ../009-probabilistic-verification/analysis.md.
• Sub-noise-floor cheating is undetectable, and is also worthless to the attacker: an error the check cannot see is an error that saves no compute.

That last point was the reassuring one, and it is partly still true: gross cheating pays and gross cheating is caught. But E009-pre showed the middle of the range is real — reduced-precision computation both pays and hides — so "the attacks that pay are exactly the attacks that produce large errors" is too strong and is withdrawn.

The caveat that undermines all of it — since measured, and it was worse than feared

τ here was derived from honest residuals produced by one library on one device. Nodus is deliberately heterogeneous, so τ must be raised to cover cross-backend divergence, which raises the corruption an attacker can hide by the same factor. When this was written the factor was UNKNOWN and flagged as the programme's highest-priority open measurement.

It has now been measured (E009-pre): the factor is 191–381×, driven almost entirely by the device rather than the library or summation order. At that tolerance the bfloat16 cheat is no longer detectable. The exact-arithmetic results in §1–2 are unaffected; the floating-point security analysis in this section holds only for a homogeneous CPU-class network, and is superseded by ../009-probabilistic-verification/analysis.md.

---

4. What this does not establish

Per docs/verification-taxonomy.md, Freivalds supports Claim A at level L3 and nothing else:

• Not Claim B. Nothing binds C to a fresh execution. A cached C passes forever. Fixable cheaply with a freshness nonce folded into the statement, but not fixed by this mechanism.
• Not Claims C or D. The check says nothing about resources consumed. A provider who obtained C by any cheaper means passes.
• Not succinct. The verifier must read A, B and C — O(n²) work and O(n²) memory traffic. A third party who does not hold the operands gets nothing. This forecloses weight privacy, which is precisely what ZK buys and Freivalds cannot.
• Requires unpredictable randomness chosen after C is fixed. If the prover learns R first, it returns C + E for any E with E·R = 0. In deployment this is a commit-then-reveal problem.

5. What a malicious provider can still get away with

1. Returning a cached C for a repeated (A, B) — undetected, and profitable.
2. Any corruption below the tolerance floor — detected as harmless above.
3. Sub-contracting the computation and relaying the result.
4. Everything about billing: the check constrains the answer, not the work.
5. If it can predict or influence R: complete forgery.

6. Economic implication

At n=8192 the check costs 57 ms against 2.49 s to recompute. At the declared local rate of 1.2×10^-6 USD/machine-second, verifying costs 6.8×10^-8 USD against 3.0×10^-6 USD to re-execute. Verification is ~2% of the compute it polices, so a network could afford to verify every single matmul rather than sampling — which changes the design from "audit a fraction and rely on stake" to "check everything cheaply", a materially different and much stronger posture.

For comparison, the same Claim A via SP1 at 20M cycles costs 49× the native computation to verify and 87,000× to prove.

7. Next

See next_steps.md.

Status: complete. Date: 2026-09-01 (run after E009-pre). Implementation: implementation/freivalds_field.py. Raw records: ../../benchmarks/results/003-matrix-multiplication.jsonl (variant = "field-mod-p").

---

1. Why this exists

E009-pre falsified the float-domain security story: honest CPU-vs-GPU divergence is within ~3.7× of the divergence a precision cheat produces, so no tolerance separates them. Every part of that failure traces to one cause — the arithmetic is inexact, so the check needs a tolerance, and the tolerance is the attacker's budget.

Exact arithmetic removes the tolerance and therefore removes the entire failure mode. The only question left is what it costs.

2. Result

Operands are int8-valued (as in quantised inference); the check runs over F_p with p = 1048573, the largest prime below 2^20.

Against the float variant, at n=8192:

Exact arithmetic costs 2× the floating-point check and buys back the entire guarantee.

A 2× verification cost is nothing — it moves R_verify from 2.3% to 4.6% of the computation being policed. In exchange the mechanism stops having a tunable security parameter that an attacker can aim at, and stops depending on which hardware the honest providers happen to own.

3. Two implementation findings worth recording

The operand reduction was unnecessary, and it was 92% of the cost

The first implementation reduced A, B and C into F_p before checking. That cost 1.33 s of a 1.44 s verification at n=8192 — R_verify = 0.58, a mere 1.7× advantage, which would have made the mechanism look barely worthwhile.

It is entirely avoidable. With |A|,|B| ≤ 127, |C| < 2^27 and residues r < 2^20, every intermediate fits in int64 without any reduction of the n×n matrices:

  B@R    : |term| < 2^27, summed 2^13 times  ->  < 2^40
  A@(BR) : |term| < 2^27, summed 2^13 times  ->  < 2^40
  C@R    : |term| < 2^47, summed 2^13 times  ->  < 2^60      (int64 max 2^63)

Reduction therefore only ever touches n×k intermediates. Choosing p < 2^20 rather than the more obvious p = 2^31−1 is what makes this work: a smaller prime costs one extra round and saves an entire O(n²) pass.

The superseded measurements are retained in the results file with status = "superseded" rather than deleted.

Field arithmetic needs 20× fewer rounds

The float/exact variants in E003 draw r from {0,1}^n, giving soundness ≤ 1/2 per round and needing k = 40 for 2^-40. Drawing r uniformly from F_p gives soundness ≤ 1/p ≈ 2^-20 per round, so k = 2 suffices. The field version does 20× less work per unit of soundness; it is slower here only because int64 matmul has no BLAS path, while the {0,1} version rides float64 BLAS.

That is an optimisation target, not a property of the mechanism. An int8/int32 GEMM (which every inference accelerator already has, since it is what quantised inference runs on) should close most of the 2× gap.

4. What it detects that the float check cannot

Both negative controls pass at every size:

• ±1 on a single entry — the smallest possible corruption.
• 64 entries off by one, i.e. ~1 part in 10^8 of the row — orders of magnitude below any float32 tolerance, and invisible to the E003 float check at any n.

There is no threshold to set and no false-positive rate to trade off. A corruption is either present or it is not, and the check finds it with probability ≥ 1 − 9.1 × 10^-13.

5. What a malicious provider can still get away with

Unchanged from E003, and it is important that this list did not get shorter:

• Caching. A stale C for a repeated (A, B) passes forever. No Claim B.
• Claims C and D. No information about resources consumed.
• Any cheaper exact method. The provider may obtain C however it likes.
• Quantisation of the model, as opposed to the matmul. This verifies the multiplication that was specified. If the specification does not pin the quantisation scheme, a provider can still substitute a coarser one and be correct with respect to its own specification. Exact arithmetic makes the check sharp; it does not make the specification complete.
• Predictable randomness ⇒ total forgery, as before.

6. What this means for Nodus

The programme now has a concrete, measured architectural recommendation:

Mandate quantised-integer semantics for verifiable job classes. Then matmul verification costs ~4.6% of the computation, carries an exact 9.1 × 10^-13 soundness bound, needs no tuning, and is immune to the hardware heterogeneity that breaks the floating-point version.

Note what this is: a constraint on the workload specification, arrived at from a verification requirement. It is the clearest evidence so far for hypothesis H7 — that the decisive design lever is specifying arithmetic rather than choosing a proof system.

The obvious cost is accuracy: quantised inference is not free, and that trade-off has not been measured here. It is the next thing to measure.

7. Limitations

• Matmul only. A chain of layers with non-linearities between them is not covered, and the activations are where quantisation error compounds.
• int8 operands and one prime. No sweep over quantisation width or p.
• The int64 path has no BLAS; on an accelerator with int8 GEMM the comparison against the float variant would likely improve.
• Single run per size, one machine.
• Says nothing about the accuracy cost of quantised inference, which is the price of the recommendation in §6.

Ordered by (information gained) / (cost to get it).

1. E009-pre — heterogeneous honest divergence [blocking, do first]

Everything in §3 of the analysis rests on a tolerance τ derived from one library on one machine. Nodus is heterogeneous by design. Measure:

• the same matmul on CPU (Accelerate), Metal/MPS, and a plain unoptimised loop;
• the distribution of ‖A(Br) − Cr‖ across backends, not within one;
• the same for a real llama.cpp forward pass at temperature 0, which also gives the replication false-positive rate v1 needs (mvp-analysis.md §7).

Deliverable: the factor by which τ must grow for a heterogeneous network, and therefore the factor by which the detectable-corruption floor rises. Until this exists, no threshold in a deployed audit can be justified.

This is now the highest-priority measurement in the whole programme. It is cheap, it requires no cryptography, and both E003 and the entire L2/L3 branch of the taxonomy are gated on it.

2. Freivalds over a prime field — recover the clean guarantee

The float tolerance is the only reason the 2^-40 bound was lost. Quantised integer inference computed mod a prime p restores exact arithmetic and with it the textbook soundness. Measure the cost of doing the check in modular arithmetic (the native matmul stays in floats or ints as the workload dictates).

If this is affordable, it is a strong argument that Nodus should prefer quantised integer inference — not for accuracy or speed, but because it is the regime in which verification has a real guarantee rather than a tolerance. That would be a network-wide architectural consequence derived from a verification requirement, which is exactly the kind of finding this programme exists to produce.

3. Extend from one matmul to a chain of them

A forward pass is C₁ = A·W₁, C₂ = f(C₁)·W₂, … Verifying each matmul independently requires the verifier to hold every intermediate activation, which is O(layers · n²) of data movement and may erase the advantage. Measure the whole-chain R_verify, not the per-matmul one. Also test whether the non-linearity f between layers can be checked cheaply or whether it forces full re-execution of the activations — which would collapse the advantage.

This is the bridge to E004 and the first point at which "verify a matmul" becomes "verify an inference".

4. Add the freshness binding and re-measure

Fold an unpredictable coordinator-chosen nonce into the statement so that a cached C no longer passes. Measure the cost (expected: ~0). This converts Claim A into Claim A ∧ B and is, on current evidence, the cheapest security improvement available anywhere in the system.

5. Compare against a specialised cryptographic argument

Sumcheck/GKR for matmul gives a verifier that does not need to hold A and B in full, restoring succinctness and enabling weight privacy — the two things Freivalds cannot do. Measure its R_verify against the 0.023 baseline established here. This is the honest test of whether cryptography buys anything for matrix multiplication, and it now has a demanding baseline to beat.

6. Larger n, and GPU

n = 16384 and 32768 to confirm the k/n trend holds and to see whether the 4.7× bandwidth penalty grows. Also run on the M5 GPU via MPS, where the arithmetic intensity gap between matmul and matrix-vector is larger, so the penalty may be worse — the mechanism's advantage may be smaller on the hardware that actually runs inference.