the composition language and virtual machine of cyber. sixteen deterministic reduction patterns over the Goldilocks field, plus one non-deterministic hint pattern and five jets. every computation produces a stark proof of correct execution as a byproduct.

nox descends from Nock (Urbit), replacing natural numbers with Goldilocks field elements and decrement with field inverse. the execution trace IS the algebraic constraint system — there is no translation layer between the program and the proof.

five structural operations define how values compose regardless of what those values are:

the critical difference from Nock: Nox's tree is a Merkle tree by construction. every cons(a, b) computes hash(a, b) and stores the digest at the parent node. axis produces a Merkle proof as a side effect. the authentication scheme is abstract — pluggable backends (Hemera, SHA-256, Verkle, SMT).

nox is simultaneously the structural IR (the grammar all cyb/languages compile through), the node runtime (the production binary that runs the cyber blockchain), and the composition tier that orchestrates programs across all execution languages, manages proof aggregation, and defines the program structure of the whole system.

three layers

Layer 1: 16 deterministic patterns (structural + field arithmetic + bitwise + hash)
Layer 2: hint (non-deterministic witness injection, verified by Layer 1)
Layer 3: 5 jets (hash, poly_eval, merkle_verify, fri_fold, ntt)

Layer 1 defines truth. Layer 2 defines the prover-verifier boundary. Layer 3 defines performance. remove Layer 3: identical results, slower. remove Layer 2: no privacy, no ZK. remove Layer 1: nothing remains.

dependency graph

nebu (field)
  ↓
hemera (hash)
  ↓
nox (VM) ← this repo
  ↓
zheng (proofs)
  ↓
bbg (state)

computation as cyberlink

ask(ν, subject, formula, τ, a, v, t) → answer

the seven arguments of ask are the seven fields of a cyberlink. computation IS linking

1. compute order_axon = H(formula, subject)
2. lookup: does axon(formula, subject) have a verified result in the cybergraph? → yes: return cached result (zero computation — memoized) → no: reduce(subject, formula), prove via STARK
3. link order_axon → result (with proof)

the cybergraph is a universal, persistent, proven memo cache. every computation anyone ever did is reusable by everyone. the more the graph grows, the fewer computations actually execute

see cyber/nox for the full specification, zheng for the proof system, trident for the high-level language

from subgraph nox

nox

proof-native virtual machine for cyber. every execution produces a STARK proof as a byproduct — running a program and proving it ran correctly are the same act. there is no separate arithmetization step. the execution trace IS the algebraic constraint system.

lineage

combinatory logic (1924)   S, K combinators            pure abstraction
  → lambda calculus (1936) Church's untyped lambda      computable functions
  → Nock (2016)            natural numbers + decrement  deterministic virtual machine for Urbit
  → nox (2026)             field elements + inverse     proof-native virtual machine for cyber

nox replaces Nock's natural numbers with Goldilocks field elements and decrement with field inverse. this single substitution makes the virtual machine algebraically native — every operation maps directly to field constraints with zero translation overhead.

why nox is amazing

computation IS linking. ask(ν, subject, formula, τ, a, v, t) has seven arguments — the seven fields of a cyberlink. ordering a computation and asserting knowledge are the same act. the cybergraph is simultaneously a knowledge base and a universal memo cache. every computation anyone ever did is reusable by everyone. the more the graph grows, the fewer computations actually execute. nox does not just compute — it remembers.

proof-native execution. most virtual machines bolt proofs onto execution after the fact — run the program, then arithmetize the trace, then prove. nox skips the middle step. the execution trace is already a valid STARK witness. reduce(subject, formula) simultaneously computes the result and generates the proof artifact.

algebra polymorphism. the same 16 reduction patterns work over any field, any word width, any hash function. pattern semantics are universal — algebra is a parameter. a single nox program runs over Goldilocks (STARKs), F₂ (Binius), or F_{p³} (recursive composition) by selecting a different instantiation. one spec, many proof systems.

merkle by construction. every cons(a, b) builds a Merkle tree — the hash is computed and stored at the parent node. axis traversal produces Merkle proofs as a side effect. content addressing is not a feature layered on top — it is the data model itself. and because every noun is content-addressed, every reduction result has a unique identity — the foundation of global memoization.

cybergraph-native. nox is tightly coupled with the cybergraph and bbg. the memo cache IS the graph state. the proof IS a cyberlink. the focus budget IS the token payment. this coupling is not a dependency — it is the source of compounding returns. every computation enriches the graph. every enrichment accelerates future computation.

minimal irreducible design. 16 deterministic patterns, 1 non-deterministic hint, 5 optimization jets. remove the jets — identical results, ~8.5× slower. remove the hint — no privacy, no ZK, but still Turing-complete. remove Layer 1 — nothing remains. every pattern earns its place.

privacy at the boundary. the hint pattern (16) injects untrusted witness data that Layer 1 constraints verify. this is where privacy enters: the prover knows the secret, the verifier checks the math. no trusted setup. no MPC ceremony. the architecture separates knowledge from verification.

lazy evaluation. the branch pattern (4) evaluates only the taken path. the other branch is never touched. this prevents infinite-recursion DoS attacks structurally — a property of the reduction semantics, not a runtime check.

unified IR. nox is simultaneously the intermediate representation (all cyber languages compile through it), the node runtime (production blockchain binary), and the composition tier (orchestrating programs across execution contexts). one representation from source to proof.

architecture

ask(ν, subject, formula, τ, a, v, t) → answer

the seven arguments of ask are the seven fields of a cyberlink. computation IS linking. the function:

1. compute order_axon = H(formula, subject)
2. lookup: does axon(formula, subject) have a verified result in the cybergraph? → yes: return cached result (zero computation — memoized) → no: reduce(subject, formula, focus=(τ,a)), prove via STARK
3. link order_axon → result (with proof)
4. return result

the cybergraph is a universal, persistent, proven memo cache. every computation anyone ever did is reusable by everyone. the more the graph grows, the fewer computations actually execute

two cyberlinks per computation:

the order axon H(formula, subject) is itself a particle (axiom A6). anyone can query backlinks to it — "what results exist for this computation?" multiple devices can answer the same order. the ICBS market determines which answer the graph trusts

everything is a noun — a binary tree of Goldilocks field elements. programs are nouns. data is nouns. the result is a noun.

Layer 1: 16 deterministic patterns    Turing-complete + field arithmetic + bitwise + hash
Layer 2: 1 non-deterministic hint     witness injection, privacy boundary, verified by Layer 1
Layer 3: 5 jets                       hash, poly_eval, merkle_verify, fri_fold, ntt

the 16 patterns

canonical instantiation

F = Goldilocks       p = 2⁶⁴ - 2³² + 1
W = Z/2³²           32-bit words (fit cleanly in [0, p))
H = hemera           Poseidon2-Goldilocks sponge, 32-byte output

companion repos

license

Cyber License: Don't trust. Don't fear. Don't beg.