# Research log

The findings in the order they were discovered, which is not the order they make
sense in. [`../README.md`](../README.md) presents the conclusions; this file
keeps the route, including the wrong turns.

Reading it in sequence shows the programme changing its mind four times: a
cryptographic answer abandoned on cost, a probabilistic one falsified by
hardware, a contract that dissolved the problem, and a bandwidth bill that
arrived after all of it and reopened the design.

---

### Headline finding: the same claim, nine orders of magnitude apart

Both of the mechanisms below establish **Claim A** (the output is correct).
Both were measured on the same machine in the same week, each against a native
baseline measured in the same run.

| mechanism | level | `R_prove` | `R_verify` | soundness error | provider cost |
|---|---|---:|---:|---|---|
| SP1 zkVM, `y = 3x + 5` | L5 | 1.6 × 10^10 | 8.2 × 10^7 | negligible | 11.2 s |
| SP1 zkVM, 20M cycles | L5 | 8.7 × 10^4 | 49 | negligible | 253 s |
| **Freivalds, 8192² matmul** | **L3** | **0** | **0.023** | **≤ 2^-40** | **none** |

The difference is not implementation quality. A zkVM proves a RISC-V execution
trace and pays for every load, branch and index computation; Freivalds exploits
the algebraic structure of the statement and makes the *verifier* do a small
amount of work instead. Verifying an 8192×8192 matrix product costs **2.3% of
recomputing it**, with no cryptographic assumptions at all.

### …and the catch, also measured

Freivalds' clean guarantee assumes **exact** arithmetic. In floating point it
degrades to an approximate-correctness check with a tolerance, and
[E009-pre](experiments/009-probabilistic-verification/) measured what that
tolerance has to be in a heterogeneous network:

| network composition | honest worst-case error | bf16 cheat error | separation |
|---|---:|---:|---:|
| CPU-class only | 1.0 × 10^-6 | 2.84 × 10^-3 | **≈ 2,800×** |
| CPU + Metal GPU | 7.7 × 10^-4 | 2.84 × 10^-3 | **≈ 3.7×** |

A 2,800× separation is a threshold anyone can set. **A 3.7× separation is not.**
The cause is the *device*: `mlx-cpu-f32` and `mlx-gpu-f32` — identical library,
identical dtype, one line of difference — diverge by 765–3,069×, with a constant
relative error that is the signature of operand rounding rather than
accumulation. **A backend advertising float32 may not be computing in float32.**

This falsified a conclusion we had written in E003 the same day, and it points
somewhere unexpected:

> The binding constraint on cheap verification is not its cost. It is the
> numerical agreement among *honest* providers. The decisive design lever may
> therefore be **specifying arithmetic** — mandating exact or quantised-integer
> semantics — rather than choosing a proof system.

What survives: the check still catches *gross* cheating (fabricated output,
substituted model, skipped layers — all 10^-2–10^0 relative error), which is to
say it catches the cheats that actually save a provider money.

### And then the problem dissolved

[E014](experiments/014-numeric-contract/) re-ran that comparison on **integer**
operands rather than real-valued ones:

| operands | worst honest backend | the cheat | usable window |
|---|---:|---:|---:|
| real-valued | 7.70 × 10^-4 *(GPU)* | 2.84 × 10^-3 | **3.7×** |
| **integer** | **0.0 — exact, every backend** | 1.41 × 10^-3 | **unbounded** |

> **The GPU's imprecision was never about the GPU. It was about representing
> real numbers.** Given integers in range, the same hardware that diverged by
> 1,500× returns the bit-exact product.

So the expected supply/security trade-off does not exist: the *strictest*
contract admits every honest backend we tested, CPU and GPU alike, while
separating cheats without bound. The heterogeneity problem did not need a
cleverer threshold — it needed different arithmetic. Deliverable:
**[`docs/numeric-contract.md`](docs/numeric-contract.md)**, draft NC-0.1.

### Which held for a whole layer

[E015](experiments/015-nonlinearities/) put a transformer-shaped layer — three
matmuls, softmax, GELU, layernorm, requantisation — under that contract. Output
was **bit-identical** on numpy-CPU, MLX-CPU and MLX-GPU at every shape tested.

The move that makes it work is specification, not arithmetic: **non-linearities
are specified as integer lookup tables** rather than as formulas. A gather is
memory indexing, so there is nothing to round — divergence becomes structurally
impossible rather than merely unlikely.

Verification splits cleanly, and yields a design rule:

| | how it is checked | cost | soundness error |
|---|---|---|---|
| matmuls | Freivalds, k=2 | **0.33%** of their MACs | 9.1 × 10^-13 |
| everything else | recomputed | **1.0×** their cost | **zero** |

> **`R_verify` ≈ the fraction of the layer that is non-linear.**

We predicted under 10% and measured 47–96% — most of which is our own numpy
overhead (our Freivalds runs 112× slower than its own arithmetic for want of a
BLAS path). The structure is confirmed; the absolute number is not yet
established, and the largest unmodelled cost is **bandwidth** — the verifier
needs the layer's intermediate tensors.

### And it holds on a transformer, doing generation

[E018](experiments/018-transformer-generation/) put a real char-level transformer
— attention, softmax, residuals, layernorm, GELU — under the contract and
generated text. 10 prompts × 300 tokens:

| comparison | runs identical |
|---|---:|
| **NC-0.3 contract, CPU vs GPU** | **10 / 10** |
| float, CPU vs GPU (both honest) | **9 / 10** |

**One honest float pair in ten diverged.** That is the number Nodus v1 has needed
since it was built — its replication check compares output hashes on evidence of
n=1, against a *simulated* node. A 10% false-positive rate means output-hash
replication **cannot be used for enforcement**: you would slash one honest
provider in ten. Under the contract the rate is zero, by construction.

Quality cost: **+1.4% perplexity** over ordinary quantisation — materially more
than the ~0 on MNIST, because a classifier's argmax absorbs perturbations and a
language model's perplexity does not.

**And the contract had a real bug, which the experiment found.** NC-3 bounded the
*accumulator* at 2^24. MLX's Metal matmul turns out to be exact only up to
**operands of 2^11**, regardless of accumulator size — 13 bits tighter, and the
binding constraint all along. Every earlier experiment satisfied it by accident
(int8 operands are ≤127); attention probabilities at 2^15 were the first to
exceed it, and CPU/GPU generation silently diverged at token 102. Fixed as clause
**NC-3b**, now asserted rather than assumed.

> A numeric contract is only as good as the quantity it bounds, and the binding
> constraint is backend-specific.

### And it holds on a real model

[E023](experiments/023-real-model/) ran the contract on **Qwen2.5-0.5B** — 24
layers, vocab 151,936, GQA, RMSNorm, SwiGLU, RoPE — the model Nodus v1 actually
serves, on wikitext-2.

**Five backends produced byte-identical logits** — Apple ARM CPU, Apple Metal
GPU, two Intel x86 CPUs on different operating systems, and an **NVIDIA L4 with
TF32 enabled** — with every next-token prediction matching. Two CPU vendors, two
GPU vendors, three OSes, three Python versions.

TF32 was left *on* deliberately: int8 operands sit four bits inside NC-3b's 2^11
bound, so the reduced-precision tensor-core path cannot lose anything. **The
contract never asks a provider to cripple their hardware.**

It also found a defect only a real model could reveal. Measured with *float*
accumulation, so this is about quantisation granularity alone:

| | perplexity |
|---|---:|
| float64 | 16.77 |
| int8, **per-tensor** — *what NC-5 specified* | **70.39** |
| int8, per-channel / per-token | 17.36 |

**Per-tensor quantisation destroys the model.** That clause was written from a
2-layer toy where it was harmless. The contract is now NC-0.5.

Six rounds of implementation fixes took the integer path from +47.6% to
**+10.3%** perplexity, and three of them were the same mistake: *int8 is a
storage convention, not the contract's limit.* NC-3b permits 2^11, and every
place we capped at 127 was discarding four bits for free.

Measured like for like, the cost decomposes cleanly: **quantisation itself costs
+6.9%, and full integer determinism adds +3.5% on top** (float 23.27 →
per-channel int8 with float accumulation 24.88 → contract 25.76).

*(Superseded by E025 below: those were point estimates from 4–6 chunks, and at
that sample size the interval contains zero. Paired over 120 chunks the costs
are +6.67% [5.95, 7.40] and +2.43% [1.63, 3.23].)*

That +3.5% is plausibly close to intrinsic. A float-accumulation pipeline
quantises matmul *inputs* and keeps accumulators exact between steps; a
fully-integer one cannot, so it has more rounding boundaries by construction.

### The protocol that fixes the bandwidth — and doesn't fit

[E019](experiments/019-interactive-proof/) implemented the sumcheck interactive
proof. On a two-layer chain of 2048² matmuls it replaces a 16.8 MB intermediate
with a **792-byte transcript** — 21,183×, and improving with scale because
communication grows logarithmically while the data it replaces grows
quadratically.

**On our transformer layer it saves nothing.** All three matmul outputs — 49.1
MB, exactly E016's figure — feed lookup-table non-linearities that the verifier
checks by recomputation. The chain breaks at the first non-linearity, and there
is one after every matmul.

> **NC-9** makes non-linearities lookup tables *because* a gather has no
> arithmetic and so cannot diverge across backends. **A sumcheck passes only
> through low-degree arithmetic.** The property that buys determinism is the
> property that blocks the proof.

That also explains SafetyNets' restriction to quadratic activations, which had
looked like an arbitrary compromise: `y = x²` is arithmetic, so the chain passes
through it. They changed the model because the protocol demanded it.

### And the price of fixing it is entirely in attention

[E020](experiments/020-polynomial-model/) asked the obvious follow-up: if our
lookup tables block the proof, what does changing the model cost?

| variant | FFN | attention | perplexity | sumcheck-ready |
|---|---|---|---:|:--:|
| A | GELU | softmax | 4.9939 | no |
| B | **x²** | softmax | **4.9703 (−0.5%)** | no |
| C | **x²** | **squared** | **5.2044 (+4.2%)** | **yes** |

**Replacing GELU with x² is free.** SafetyNets' famous activation restriction —
the thing that looks like the painful compromise — costs nothing here.

**Replacing softmax is what costs**, and it is the change that actually matters.
E019 had framed this as "adopt quadratic activations"; that was incomplete.
SafetyNets' networks had *no attention*, and their only softmax was the final
classification layer, which they explicitly exclude from the proof. A transformer
cannot make that exclusion.

So the trade is now measured: **roughly three extra points of perplexity buys a
~60,000× bandwidth reduction** — the difference, on E016's cost model, between a
scheme that loses money and one that is free. Both architectures are laid out in
[`docs/architecture.md`](docs/architecture.md) §6.

And that caveat was right — [E020b](experiments/020-polynomial-model/analysis-scaling.md)
measured it at scale:

| layers | softmax | squared | gap |
|---:|---:|---:|---:|
| 2 | 5.6240 | 6.0060 | +6.8% |
| 4 | 5.3730 | 5.7282 | +6.6% |
| 8 | 5.2468 | 6.2839 | **+19.8%** |

**Softmax improves with depth. Squared attention stops improving and then
regresses.** The gap is a divergence, not a fixed tax a larger model amortises.

> **Decision: the polynomial route is closed. Nodus keeps the model and pays the
> bandwidth** — NC-0.3 contract + one-random-layer audit + a stake equal to the
> job's compute value. Works on an unmodified transformer, +1.4% perplexity, 39%
> of the cost of re-execution at 32 layers.

This also says something about SafetyNets: its quadratic-activation restriction
is usually read as a dated compromise, but it looks load-bearing. Their networks
were CNNs with no attention to lose. A transformer's inductive bias lives in
exactly the operation a sumcheck cannot pass through.

### And the bill on all of it, paid

We had been recommending the network switch to exact integer arithmetic without
ever measuring what that costs in answer quality.
[E017](experiments/017-accuracy-cost/) measured it. The number that matters is
not "integer vs float" — ordinary quantisation is already integer and known to
work — but the **extra** cost of being integer *end to end*, with no float step
anywhere to reintroduce cross-backend divergence:

| bits | quantisation cost | **extra cost of determinism** |
|---:|---:|---:|
| 8 | +0.0002 | **+0.0001** — one test image in 10,000, sign flips across seeds |
| 6 | +0.0006 | **−0.0001** |
| 4 | +0.0086 | **+0.0038** |

**At 8 bits, full determinism is free within measurement noise.** CPU and Metal
GPU produced bit-identical logits on all 10,000 test images. It starts to bite
at 4 bits, which gives a usable precision floor rather than a blanket claim.

That closes the last blocking unknown on the contract — and it is the direct
answer to EigenAI's stated future work, *"portable numeric normalization to
enable heterogeneous verifier sets"*. Caveat we are not hiding: MNIST is an easy
task, and no transformer or generation workload has been tested.

### Then the bill we hadn't counted

[E016](experiments/016-verification-bandwidth/) measured the cost of getting the
verifier its data. **It dominates by three to five orders of magnitude.**

| | one layer, s=1024 d=2048 |
|---|---|
| the job's answer | 0.02 MB |
| intermediates the verifier needs | **49.1 MB** — 3,010× |
| break-even compute price (cloud egress) | **$164/hour** |
| actual price of a rented GPU-hour | **~$1** |

Every configuration loses. The earlier `R_verify` figures are **compute** ratios
resting on an assumption we hadn't stated — *the verifier already holds what it
needs*. True for one matmul the coordinator owns; false inside a pipeline.

**The rescue:** audit *one random layer* instead of every layer. Bandwidth stays
flat while compute saved scales with depth, so at 32 layers on cheap egress
verification costs 39% of re-executing. Soundness falls to `1/L` — and the
required stake falls out cleanly, because the `m` and `L` cancel:

> **A stake equal to the job's compute value makes layer-skipping
> negative-expected-value, at any depth and any level of greed.**

This also promotes **interactive proofs (GKR / SafetyNets)** from interesting to
the known answer: polylogarithmic communication is precisely what this cost
demands. We have not measured them yet.

### The fix, measured the same day

Every part of that failure traces to one cause: inexact arithmetic forces a
tolerance, and the tolerance is the attacker's budget. Running the same check
over a prime field on quantised-integer operands removes it:

| | float32, k=40 | **field, k=2** |
|---|---:|---:|
| `R_verify` at n=8192 | 0.023 | **0.046** |
| soundness | a tolerance, not a bound | **9.1 × 10^-13, exact** |
| tuning parameters | `τ`, chosen arbitrarily | **none** |
| survives heterogeneous hardware | no | **yes** |

**Exact arithmetic costs 2× and buys back the entire guarantee** — `R_verify`
moves from 2.3% to 4.6% of the computation being policed, and the mechanism
stops having a security parameter an attacker can aim at. It detects 64 entries
off by one (≈1 part in 10^8), which no float tolerance can see.

That yields the programme's first concrete architectural recommendation:
**mandate quantised-integer semantics for verifiable job classes.** It is a
constraint on the *workload specification*, arrived at from a verification
requirement — which is what hypothesis H7 predicts. Its price is the accuracy
cost of quantised inference, which we have not yet measured.

### Experiment 001 in detail

Proving `y = 3x + 5` in a general-purpose zkVM on an Apple M5:

| | |
|---|---|
| native computation | **0.69 ns** |
| proving | **11.2 s** |
| verification | **56 ms** |
| proof size | **2.78 MB** |
| `R_prove` | **1.6 × 10^10 ×** |
| `R_verify` | **8.2 × 10^7 ×** |

Proving ten thousand of those statements costs **the same 11 s**. The cost is
almost entirely a *fixed* per-proof charge, not a charge for the work — which
means the interesting economic question is not "how expensive is ZK" but "how
much work can you amortise a proof over". Full analysis:
[`experiments/001-simple-arithmetic/analysis.md`](experiments/001-simple-arithmetic/analysis.md).

---

### And the question underneath all of it

Nodus does not pay for correct answers. It pays for **compute units**. Those are
different things, and almost all of the verifiable-computation literature
addresses the first.

[Experiment 013](experiments/013-work-vs-output/) ran seven provider strategies
against our strongest checker. Every cheat that changes the answer is rejected.
Exactly one strategy is accepted while doing materially less work — **returning a
cached correct answer** — and no checker of any strength can object to it,
because the answer is right. It is a pricing bug, closed by a hash lookup.

The other low-work strategy that passes is **Strassen's algorithm**: 67% of the
arithmetic, exactly correct, accepted. Correctly accepted — a verifier cannot
tell "cleverer" from "lazier", because at the level of the output there is no
difference.

> **A shortcut is only an attack if you are paying for effort rather than
> output.**

Literature checked before concluding: forcing *useful* work in software is not
an open problem (there is a proof-of-useful-work for matrix multiplication at
1+o(1) overhead), but every such construction rests on an **unproven hardness
conjecture** — we have no unconditional superlinear lower bounds, and ω is still
falling. A 50-scheme SoK concludes proof-of-useful-work "is actually not as
useful as expected". Proof-of-Learning, the direct ML analogue, was published and
then broken.

**Claim C (work performed) is conditionally achievable in software. Claim D
(physical resource expenditure) is not.** On our evidence Nodus should not need
either: price the job from its specification, verify the output, dedup repeats,
and let efficient providers keep their margin.

### And the audit design is now a working protocol

[E024](experiments/024-layer-audit/) builds what E016 derived — Merkle
commitment, uniform post-commitment challenge, opening, recomputation — and runs
it against Qwen2.5-0.5B.

| | |
|---|---|
| honest provider, all 24 layers challenged | **accepted** |
| cheating on 1 of 24 layers (200 trials) | detected **4.5%** (1/L = 4.2%) |
| cheat everywhere, then answer the challenge honestly | **REJECTED by the commitment** |
| audit traffic vs verifying every layer | **4.2%** |

Building it corrected the paper design twice. **The layer's output never needs
transmitting** — the verifier recomputes it and checks its *own* digest against
the root, which halves the opening and is strictly more secure, because the
provider never gets to say what the output was. And **layer 0 is free**: its
input is the embedding the verifier already derives, so the opening is two
Merkle paths and nothing else — 160 bytes.

It is not a proof, and shouldn't be called one: a single-layer cheat escapes
with probability 1 − 1/L. **The defence is the stake, not the probability.**

## The one metric

```
        cost of obtaining trustworthy evidence
  R  =  ──────────────────────────────────────
             cost of the native computation
```

with `R_verify` — the *verifier's* share — treated as decisive, because the
verifier always has the option of simply re-running the job (`R_verify = 1`).
Any mechanism above that line has to justify itself with something re-execution
cannot provide: succinctness for a third party, privacy of the weights, or
tolerance of non-determinism.

Every experiment reports `R` alongside a mandatory statement of **what the
evidence actually proves** and **what a malicious provider can still get away
with**.

---

### And then we put error bars on the headline

[E025](../experiments/025-accuracy-error-bars/) went back to the accuracy claim
with the question a reviewer asks first: *how do you know?*

E023's "+3.5% for determinism" was a difference of two point estimates from 4–6
chunks. Re-measured over **120 paired chunks** — every pipeline seeing identical
tokens, intervals by bootstrap over chunks:

| gap | estimate | 95% CI | sign holds |
|---|---:|---|---:|
| quantisation | +6.67% | [+5.95%, +7.40%] | 113/120 |
| **determinism** | **+2.43%** | **[+1.63%, +3.23%]** | 83/120 |

Two things came out of it, and the second matters more.

**The number was wrong in our favour: +3.5% → +2.43%**, with the old estimate
outside the new interval.

**And the old evidence could not have supported it.** Resampling at five chunks
gives [−1.36%, +6.47%] — an interval containing zero. E023's conclusion was
right and its evidence did not establish it, which are different things, and the
difference is invisible unless you go and check.

The design lesson is the pairing. Absolute perplexity here ranges from 8.6 to
43.3 across chunks — a 5× spread against effects of a few percent — so an
unpaired study would have needed an enormous sample to see anything. Because
every pipeline sees the same chunks, chunk difficulty cancels, and the interval
on the *gap* is 1.6 points wide against ~5 on either endpoint.

One nuance worth keeping: the determinism gap holds its expected sign in only
83 of 120 chunks. The contract is worse **on average by a little**, not worse on
every input — which is what a small rounding difference should look like.

### And the prover turned out not to be the problem

[E026](../experiments/026-sumcheck-prover-cost/) went after the last
unquantified number in the paper: what the sumcheck prover pays. E019 could not
measure it, because its `sumcheck()` runs both parties in one loop.

First answer: **36.1%** at n = 4096. That looked like a second reason sumcheck
does not transfer to transformers, on top of the bandwidth one.

It was wrong, and the breakdown said so. Two thirds of the cost was forming the
multilinear extensions, so we looked at why. numpy has **no BLAS path for
int64**, so the extension products were running at 733× the per-element cost of
a float64 multiply-add. And two of the three field reductions were being applied
to operands that were already residues, because NC-3b bounds them at 2^11 and
the prime is 2^25.

Fixing both: **3.5× faster, bit-identical output, 10.4%** at n = 4096, scaling
as n^−0.92 against a predicted n^−1, reaching 5% by n ≈ 8,800.

> **The sumcheck rounds are 0.5% of the prover's overhead.** The protocol is
> free. Everything else is the multilinear extensions and getting into the
> field, split about evenly.

Two things came out of this. The paper got *stronger* by losing an argument: the
prover is not what blocks sumcheck for transformers, so the non-linearity
structure is the only obstacle, which is a cleaner and more falsifiable claim.

And for the second time in three experiments, a number that looked settled was
a measurement of our own code rather than of the thing we meant to measure.
E017 taught this once, E025 taught it again, and E026 makes it three. It is now
the default assumption.

Also falsified along the way: verification costs **more** than simply recomputing
a single matmul at every size up to n = 2048, crossing below only at 4096.
Sumcheck's advantage is bandwidth, not compute.

### And then the audit got a conclusive sibling

E024's audit catches a single-layer cheat 4.2% of the time and leans on the
stake. The economics are sound, but the verdict is never *"this provider
cheated"*, only *"cheating loses money"*.

[E027](../experiments/027-bisection-fraud-proof/) borrows Arbitrum's fraud
proof. Two parties who disagree binary-search to the first layer where their
committed digests differ; an arbiter recomputes that one layer and rules.

| | random audit | bisection |
|---|---|---|
| bandwidth | 4.2% | **4.24%** |
| detection | 4.2% | **certain** |
| requires | stake > job value | a challenger who ran the job |

Same bandwidth, same arbiter cost, conclusive instead of probabilistic. The
extra cost is entirely the challenger's re-execution, which is the same trade
Arbitrum makes: full work off-chain so the arbiter does O(1).

The hypothesis worth worrying about was H5 — does the search land on the layer
that was actually cheated, or merely on the first place the digests happen to
diverge? Blaming the wrong layer would mean slashing honest work.

**24 of 24 correct**, and the reason is the contract again. Under exact integer
semantics a perturbation propagates to every later layer instead of being
rounded away, so the first divergence *is* the cheat. **The exactness that makes
heterogeneous verification possible is also what makes the fraud proof point at
the right layer.**

Both properties also scale the right way: rounds grow as log2(L) while the
arbiter's share is 1/L, so a deeper model makes adjudication cheaper.