NodusLab

The numeric contract (NC-0.5)

The central artefact. Every clause traceable to a measurement.

Status: draft NC-0.5. Validated on a real model — Qwen2.5-0.5B (24 layers, vocab 151,936) produced bit-identical logits across CPU and GPU (E023) — and across four backends from two silicon vendors — Apple ARM CPU, Intel x86 CPU, Apple Metal GPU, and an NVIDIA L4 with TF32 both on and off (E021, E022) — and on a real transformer generating text (E018: 10/10 runs bit-identical over 300 tokens each). Last revised 2026-09-02.


Why this document exists

Nodus v1 specifies a job by model and model_version. That is not enough to determine a correct answer.

The same model, on the same input, run honestly on a CPU and on a GPU, produced results 1,500× further apart than float32 rounding would suggest (E009-pre) — close enough to a genuine precision cheat (3.7×) that no threshold separates them. A job specification that does not pin arithmetic leaves "correct" undefined, and no verification mechanism can repair that: a proof of the cheap circuit is a valid proof, an attestation of the cheap binary is a valid attestation.

E014 measured the fix. Constraining arithmetic to exact integers costs no supply — every honest backend tested, CPU and GPU, returns the bit-exact product — while separating cheats without bound.

Scope

A contract applies to a verifiable job class. Nodus may offer unverifiable classes too, more cheaply; this document does not require every job to be verifiable. It requires every job to say which it is.

NC-0.2 covers linear operations (matmul, convolution as matmul) and the non-linearities of a transformer layer (softmax, GELU, layernorm, requantisation). E015 ran a layer containing all of them across three backends and obtained bit-identical output on CPU and GPU.


Clauses

NC-1 — Operand domain

Operands are integers in a declared range [-M, M]. The job states M. Rationale: E014 — integer operands make CPU and GPU agree bit-exactly. Real-valued operands do not.

NC-2 — Accumulator

The job states the accumulator's exact-integer capacity E (float32 → E = 2^24; int32 → E = 2^31; int64 → E = 2^63). A provider may use any accumulator with capacity ≥ E.

NC-3 — Tiling bound

No single accumulation may exceed k terms, where

    k  ≤  E / M²

For int8 operands (M = 127) into a float32 accumulator (E = 2^24), this is k ≤ 1040. Jobs with a reduction dimension larger than k must be tiled, and the tile results summed exactly.

Rationale: E014 §3. Worst-case |C| is M²·n, but random data only reaches M²·√n — a 64× gap at n = 4096. Two honest backends that pass on random inputs fail on legitimate high-magnitude ones. This clause makes exactness hold by construction rather than by luck.

NC-3b — Operand magnitude bound (added after E018; the binding one)

No operand entering a matmul may exceed 2^m, where m is the matmul input mantissa of the backends the job class admits. The job states m.

Rationale: E018. MLX's Metal matmul is exact on integer operands up to 2^11 − 1 = 2047 and inexact from 2^12, regardless of accumulator magnitude. NC-3's accumulator bound of 2^24 was therefore never the binding constraint on that backend — it is 13 bits looser than the real one. Every experiment before E018 satisfied the real bound by accident, because int8 operands are ≤ 127. Attention probabilities carried at 2^15 were the first operand to exceed it, and the contract broke silently: CPU and GPU generations diverged at token 102.

A contract must state the bound it requires rather than inherit whatever a backend happens to provide, and implementations should assert it rather than assume it. Conformance is checked by NC-8.

Measured bounds, to be extended as hardware becomes available:

backend exact integer operand bound status
NumPy + Accelerate, Apple ARM none below 2^22 MEASURED (E021)
NumPy + OpenBLAS, Intel x86 none below 2^22 MEASURED (E021)
MLX, Metal GPU (fp32) 2^11 MEASURED (E018)
NVIDIA L4, TF32 ON 2^11 MEASURED (E022)
NVIDIA L4, TF32 off none below 2^19 MEASURED (E022)

Two vendors, one number. Apple's Metal and NVIDIA's TF32 share no design lineage and both land on an 11-bit effective mantissa. The bound is a property of how accelerators do float32 matmul, not a quirk of one framework — and it was predicted for NVIDIA from the Metal measurement before the hardware was available (E021 §3), then confirmed exactly (E022).

A job class that keeps operands at int8 (≤ 2^7) is four bits inside this bound on every backend measured, which is why the contract holds on an NVIDIA GPU even with TF32 left enabled. TF32 does not have to be turned off; NC-3b makes it irrelevant.

NC-4 — Reduction order is unconstrained

The provider may sum in any order, use any blocking, any parallel tree, and any instruction mix.

Rationale: once NC-1..NC-3 hold, the arithmetic is exact, and integer addition is associative. Order cannot change the result. This is a significant practical win — reduction order is effectively impossible to pin across hardware, and float contracts have to try.

NC-5 — Quantisation scheme (revised after E023)

Where the underlying computation is real-valued, the job states the mapping: scale granularity, zero point, rounding mode, and clipping behaviour.

Scales are per output channel for weights and per token for activations — not per tensor. MEASURED (E023, Qwen2.5-0.5B): per-tensor int8 gives perplexity 70.4 against a float baseline of 16.8, while per-channel gives 17.4. Per-tensor is unusable on a real model, and the earlier per-tensor clause survived only because it was written from a 2-layer character model.

Rounding is round-to-nearest, and this must be enforced rather than assumed. A right shift floors, biasing every requantisation downward by ~0.5 LSB. That is a systematic error and compounds through depth instead of averaging out; fixing it was worth 8 perplexity points at 24 layers.

NC-5b — Scales may not vary along a contracted axis

A scale that varies along an axis being summed over does not factor out of the sum. Per-channel weight scales do not survive q @ kᵀ; a per-token scale on v does not survive attn @ v. Such scales must be folded into the integers before the contraction, by an integer multiply-and-shift whose multiplier derives from the committed weights.

Rationale: E023 hit this three separate times before stating it as a rule.

NC-3c — Use the operand budget; int8 is a storage convention

NC-3b permits operands up to 2^11. Implementations habitually cap intermediate activations and lookup-table outputs at int8 (2^7), discarding four bits the contract allows. MEASURED (E023): carrying intermediates at the full budget was worth 27 perplexity points, and widening LUT outputs a further 1.5.

Where a value genuinely exceeds the budget — 16-bit softmax probabilities, or raw projection accumulators — decompose it into base-2^k limbs, each inside the bound, and recombine the exact cross products. Precision is then unlimited and the operand bound still holds.

NC-6 — Model binding

The job carries a commitment to the exact weight tensors (post-quantisation). Rationale: without this, model substitution is undetectable regardless of arithmetic (threat-model.md T3/T4).

NC-7 — Freshness

The job carries a coordinator-chosen value, unpredictable to the provider at assignment time, bound into the verified statement. Rationale: converts Claim A into Claim A ∧ B at ~zero cost. Note this does not address caching of genuinely identical jobs, which is a pricing problem (E013 §2).

NC-11 — Precision floor

A verifiable job class states its operand width, and 8 bits is the recommended floor. MEASURED (E017, MNIST MLP, 3 seeds): at 8 bits the extra accuracy cost of full integer determinism, over and above ordinary quantisation, is +0.0001 — one test image in ten thousand, sign-flipping across seeds. At 6 bits it is still zero; at 4 bits it becomes a real +0.0038. Below 8 bits a job class should expect to pay for determinism, and should say so.

NC-9 — Non-linearities are lookup tables, committed by hash

Every non-linear function is specified as an integer lookup table over a quantised domain, and the job carries a commitment to the table's contents. Formulas are not specifications: two backends evaluating tanh will disagree, two backends indexing the same table cannot.

Rationale: E015. A gather is memory indexing, not arithmetic — there is nothing to round, so divergence is structurally impossible rather than merely unlikely. The hash commitment matters: a contract that says "GELU via a lookup table" without fixing which table lets a provider be correct against its own cheaper one.

Table sizes measured as adequate for int8 activations: 256 entries for GELU, 2048 for the softmax exponential. Higher-precision activations require piecewise-polynomial approximation instead (the approach ZIP takes; see literature.md).

NC-10 — Reductions and roots

Reductions inside non-linearities (max, sum for softmax and layernorm) are integer and therefore exact and order-independent — NC-4 applies to them unchanged. Where an inverse square root is required, it is computed as an exact integer square root with an explicit correction step; a floating-point sqrt may be used as a seed but its result must be corrected, so that the output does not depend on the FPU.

NC-8 — Conformance vector

At registration, and at random intervals thereafter, a provider must reproduce a fixed reference product bit-exactly, including a magnitude-stressed case that exercises the NC-3 bound. Rationale: E014 §3 — a conformance test built only from random inputs passes backends that a legitimate input would fail.


Enforcement

The contract defines correctness; it does not detect violations. Those are separate jobs and neither substitutes for the other.

mechanism cost
define this document ~0
detect (linear) exact Freivalds over F_p, k = 2 (E003-D, E015) 0.3–4.6% of the matmuls, soundness 9.1 × 10^-13
detect (non-linear) direct recomputation 1.0× their cost, soundness zero
deter escrow, delayed settlement, stake economic

E015's governing relation: R_verify ≈ the fraction of the layer that is non-linear. The linear half is nearly free; the non-linear half is paid in full. Measured 47–96% in a numpy implementation whose overheads dominate; the true figure is between 0.5% and 20% and depends on the non-linear share of a real fused inference stack, which is UNKNOWN.

Worked example — a verifiable int8 linear layer

job_class:        verifiable-linear-v0
operand_domain:   int8,  M = 127                       # NC-1
accumulator:      float32 or wider, E = 2^24           # NC-2
max_reduction:    1040                                 # NC-3 = E / M^2
reduction_order:  unconstrained                        # NC-4
quantisation:     symmetric per-tensor, scale declared per job,
                  round-half-to-even, clip to [-127, 127]   # NC-5
weights:          sha256 commitment, post-quantisation  # NC-6
freshness:        coordinator nonce, bound into statement  # NC-7
verification:     Freivalds over F_p, p = 1048573, k = 2

Measured against this contract (E014): 5/5 honest backends conform on every operand regime; both cheating strategies excluded; verification 4.6% of native.


§6 — What this does not cover, stated plainly

  • Bandwidth. Verifying the non-linear operations requires the verifier to hold the layer's intermediate tensors. That is O(s·d) per operation, and it is not modelled anywhere. It is now the largest unmodelled cost in the scheme. (There is a plausible escape — the verifier may be able to re-derive the non-linearities from matmul outputs it has already checked — but that is untested.)
  • Multi-layer pipelines. Exact arithmetic means errors do not compound, but intermediate storage and transmission do.
  • The accuracy cost of quantised inference. MEASURED (E017) — effectively zero at 8 bits on an MNIST MLP, real at 4 bits. Caveat: MNIST is an easy task, and no transformer or generation task has been tested, so read it as "no measurable cost on this task".
  • Cross-vendor validation. DONE (E021, E022). The contract is bit-identical across Apple ARM CPU, Intel x86 CPU, Apple Metal GPU, and an NVIDIA L4 with TF32 both on and off.
  • Claims C and D. The contract constrains the answer, not the work (E013).
  • Anything below the linear-algebra layer: kernel fusion, memory layout, scheduling. Deliberately unconstrained, so providers keep their engineering freedom.

Open clauses

# question
O1 Exact integer semantics for softmax / layernorm / GELU? CLOSED by E015 — lookup tables plus exact integer reductions give bit-identical results across CPU and GPU.
O5 Can the verifier re-derive non-linearities from already-checked matmul outputs, avoiding the bandwidth cost of transmitting intermediates?
O2 Does NC-3's tiling bound survive real transformer shapes, where reduction dimensions are 4096–16384? (It forces ≥4–16 tiles; is that a real cost or free?)
O3 Can NC-8 conformance be gamed by a provider that detects test vectors and switches arithmetic? (Almost certainly yes — the test must be indistinguishable from real work.)
O4 What accuracy does the network lose? CLOSED by E017 and E018: ~0 on MNIST classification, +1.4% perplexity on character-level generation. Quote it per workload class, not as one number.
O6 The operand bound is measured for MLX/Metal only. CLOSED by E021/E022: 2^11 on Metal and on NVIDIA TF32; no operand limit on either CPU or on TF32-off.
O7 Sampling at temperature > 0 makes the RNG part of the computation. The contract must specify the generator and seed, or honest providers differ by construction. Untested.