nox virtual machine specification

version: 0.2 status: canonical

overview

nox is a proof-native virtual machine. sixteen deterministic compute patterns parameterized by algebra, plus call (non-deterministic witness injection) and look (deterministic BBG read), and five jets for efficient recursive stark verification. 16 compute + call + look = 18 patterns.

every nox execution produces a trace that IS the stark witness. there is no separate arithmetization step.

algebra polymorphism

nox is parameterised over its algebra. a nox instance is:

nox<F, W, H> where:
  F = field        (determines patterns 5-10: add, sub, mul, inv, eq, lt)
  W = word width   (determines patterns 11-14: xor, and, not, shl)
  H = hash function (determines pattern 15: hash)

structural patterns (0-4) are identical across all instantiations. field patterns (5-10) dispatch to the instantiated field. bitwise patterns (11-14) dispatch to the instantiated word width. hash (15) dispatches to the instantiated hash function. jets are per-instantiation — each algebra has its own jet registry with its own formula hashes.

execution regimes

eight instantiations across five arithmetics. flat table — no hierarchy. each regime has its own field, costs, jets, and lens. see five algebras for the independence criteria.

mul cost = base F_p multiplications per one regime-native multiply. constraints/mul = STARK constraints per multiply with regime-native lens (with jets). jali batching: N individual commitments → 1 batch via Ikat.

per-regime cost table

"—" = operation not defined or not meaningful for this regime. n = ring degree (1024). deferred = hemera computed at settlement boundary (~766 constraints). all costs are execution budget; STARK constraint counts are per-instantiation (see patterns).

five arithmetics (repos): nebu (4 regimes), kuro (1), jali (1), trop (1), genies (1). five lenses (zheng): Brakedown (4 regimes), Binius (1), Ikat (1), Porphyry (1), Assayer (1).

type-driven regime dispatch

the programmer does not choose a regime. the TYPE SYSTEM chooses.

Trident type-checks every expression. the type of an expression determines its algebra. the algebra determines its regime. the regime determines its lens. the chain is fully automatic — zero annotations, zero configuration.

Trident type    →  regime   →  lens         →  nox patterns
───────────        ──────      ────────        ────────────
Field              nebu        Brakedown       add, mul, inv (native F_p)
Fp2, Fp3, Fp4      nebu²/³/⁴   Brakedown       extension jets (fp2_mul, ...)
Bit, Nibble, Byte  kuro        Binius          xor, and (native F₂)
Lattice, Eval      jali        Ikat      ring jets (ntt_batch, ...)
Cost, Gain         trop        Tropical        branch + lt (witness jets)
Iso, Shade         genies      Isogeny         isogeny jets (group_action, ...)

cross-regime boundary: where types change. the Trident compiler inserts hemera commitments at type transitions — no manual boundary management. nox VM executes uniformly (18 patterns). zheng partitions the trace by operand types and proves each partition through its native lens. HyperNova folds all into one accumulator.

boundary cost: ~766 F_p constraints per type transition (30 field ops + 1 hemera hash).

how the eight regimes enter nox

nebu (F_p): canonical instantiation. all patterns operate natively. all costs in this spec refer to this regime.

nebu², nebu³, nebu⁴: same nox parameterization, wider field elements. one F_p² mul = 3 base muls (Karatsuba). one F_p³ mul = 6 base muls. one F_p⁴ mul = 9 base muls (tower Fp2→Fp4). extension jets recognize these structured compositions. all use Brakedown with proportionally wider columns.

kuro (F₂): separate instantiation. field patterns (add = XOR, mul = AND) are native binary operations at 1 constraint each (vs ~32 in F_p). bitwise patterns collapse to field operations. hash deferred to hemera at settlement boundary.

jali (R_q): runs on the SAME nebu instantiation (F_p). R_q = F_p[x]/(x^n+1) is a polynomial RING over F_p. ring operations decompose to F_p operations via NTT. dedicated jets commit them as batched ring operations in zheng Ikat.

trop (min,+): runs on the SAME nebu instantiation (F_p). tropical operations decompose to existing patterns: min(a,b) = branch(lt(a,b), a, b). dedicated jets produce structured witnesses verified via zheng Assayer.

genies (F_q): separate instantiation with a DIFFERENT prime q. the only regime with a foreign field. F_q elements are multi-limb (8 × 64-bit for CSIDH-512). patterns 5-10 dispatch to F_q arithmetic. dedicated Porphyry in zheng.

cross-regime composition

a single Trident program can use multiple types from different algebras. the Trident compiler inserts hemera commitments at type transitions. nox executes uniformly. zheng partitions the trace by operand type and proves each partition through its native lens. HyperNova folds all into one F_p accumulator. one decider, one proof.

boundary cost: ~766 F_p constraints per type transition
               (30 field ops + 1 hemera hash)

example — FHE bootstrapping uses three types:
  Lattice → Bit (gadget_decomp)          ~766
  Bit → Lattice (blind rotation)         ~766
  Lattice → Field (key switching)        ~766
  total boundary:                        ~2,298

the programmer writes:
  fn bootstrap(ct: &Lattice) -> Lattice { ... }

the compiler sees type transitions and inserts boundaries automatically.

universal CCS with type selectors enables heterogeneous folding:

sel_Fp:   1 for Field operands (nebu, jali, trop)
sel_F2:   1 for Bit/Nibble/Byte operands (kuro)
sel_ring: 1 for Lattice/Eval operands (jali — NTT batch)
sel_Fq:   1 for Iso/Shade operands (genies)
sel_trop: 1 for Cost/Gain operands (trop)

algebra-polymorphic patterns

the 16 compute patterns are abstract operations parameterized by algebra, not tied to a specific field. the pattern semantics are universal — the algebra is a parameter. call (16) and look (17) are algebra-independent.

three groups map to algebraic domains:

structural (0-4):   algebra-independent — tree operations work over any leaf type
field (5-10):       parameterized by F — any field
bitwise (11-14):    parameterized by W — any word width
hash (15):          parameterized by H — any hash function

the same add(a, b) means:

• in F_p context: (a + b) mod p
• in F_{p³} context: extension field addition (3 base additions)
• in F₂ context: XOR (binary addition)

the same and(a, b) means:

• in Z/2^32 context: 32-bit bitwise AND
• in F₂ context: multiplication (AND = mul in characteristic 2)
• in Z/2^64 context: 64-bit bitwise AND

the operations are identical. the algebra is a parameter. the programmer writes one tree. the prover splits it by algebra. cross-algebra boundaries are Hemera commitments.

polynomial nouns and axis

every noun is a multilinear polynomial (see nouns.md polynomial representation). axis — the fundamental navigation operation — becomes polynomial evaluation at a binary point. a Lens opening proves the evaluation in O(1) (~75 bytes proof), replacing O(depth) tree traversal. the 16 compute patterns are unchanged semantically — axis still navigates nouns. the implementation changes from pointer-following to polynomial evaluation. this applies across all instantiations: the noun polynomial is over the instantiated field F, and the Lens commitment uses the same field.

proof-system polymorphism

the same nox program can be verified by different proof systems:

nox<F_p> program     → zheng STARK (field-native, 1 constraint per field op)
nox<F₂> program      → Binius/FRI (binary-native, 1 constraint per binary op)
nox<F_{p³}> program   → zheng STARK with extension (3× wider constraints)

a single nox program containing both field and bitwise operations can be partitioned by the prover into algebra-specific sub-trees, with cross-algebra boundaries using Hemera commitments.

constraint costs are per-instantiation:

and(a, b) in nox<F_p>:   ~32 STARK constraints (bit decomposition in prime field)
and(a, b) in nox<F₂>:    1 constraint (native multiplication in binary field)

the cost difference is the honest algebraic distance between fields. the patterns stay. the proof system chooses the cheapest verification path.

canonical instantiation: nox<Goldilocks, Z/2^32, Hemera>

this specification documents one instantiation. all concrete parameters, costs, and test vectors refer to:

F = Goldilocks field, F_p where p = 2^64 - 2^32 + 1
W = Z/2^32 (32-bit words, fitting cleanly in [0, p))
H = Hemera (Poseidon2-Goldilocks sponge)

field — Goldilocks (canonical)

nox operates over the Goldilocks field, provided by nebu (~/git/nebu/).

p = 2^64 - 2^32 + 1 = 18446744069414584321
primitive root: 7
2^32-th root of unity: 1753635133440165772
efficient reduction: a mod p = a_lo - a_hi × (2^32 - 1) + correction

in this instantiation, nox arithmetic IS Goldilocks arithmetic. the execution trace IS a table of Goldilocks elements. the stark proof IS over Goldilocks. there is no impedance mismatch at any layer.

nebu provides: field element type, addition, subtraction, multiplication, Fermat inversion, NTT-friendly roots of unity, Montgomery/Barrett reduction. nox imports the field — it does not reimplement it.

hash — Hemera (canonical)

nox<_, _, Hemera> uses Hemera (~/git/hemera/) for all hashing: structural hash, Fiat-Shamir challenges, Merkle trees, content addressing.

HASH: Hemera (Poseidon2-Goldilocks, hemera)
  state: 16 field elements
  rate: 8 elements
  capacity: 8 elements
  rounds: 8 full (4+4) + 16 partial = 24 total
  s-box (full rounds): x^7
  s-box (partial rounds): x^{-1} (field inversion, 0^{-1} = 0)
  output: 4 field elements (32 bytes)
  cost: ~736 stark constraints per permutation

hemera provides: sponge construction, domain-separated hashing, Merkle-compatible mode. nox imports the hash — it does not reimplement it.

the Hemera anchor

all algebras settle through Goldilocks via Hemera (Poseidon2 over Goldilocks). this creates a permanent F_p dependency:

• nox<F₂> programs must defer Hemera to settlement (~10 constraints deferred, ~736 at settlement)
• nox<F_{p³}> programs compute Hemera natively (Hemera operates over base field F_p)
• nox<F_p> programs compute Hemera natively (200 budget cost)

the polymorphism is real for computation but asymmetric for commitment. Goldilocks is the anchor field. all algebras settle through it.

domain separation

COMMITMENT = 0x4E4F582020524543   "NOX  REC"
NULLIFIER  = 0x4E4F5820204E554C   "NOX  NUL"
MERKLE     = 0x4E4F5820204D524B   "NOX  MRK"
OWNER      = 0x4E4F5820204F574E   "NOX  OWN"

domain separation tags are injected into Hemera's sponge capacity[11] (the domain tag slot) before permutation. they ensure that hashes computed for different purposes are cryptographically distinct — a commitment hash cannot collide with a nullifier hash, even for identical input data.

nox programs invoke domain-separated hashing via pattern 15 (hash) with the tag as a capacity parameter. the tag is a protocol constant — it is not user-configurable. the VM sets capacity[11] based on the calling context:

• structural hash of nouns: capacity[11] = DOMAIN_HASH (Hemera default, 0x00)
• record commitment: capacity[11] = COMMITMENT
• nullifier derivation: capacity[11] = NULLIFIER
• Merkle tree operations: capacity[11] = MERKLE
• owner address derivation: capacity[11] = OWNER

three layers

Layer 1: 16 deterministic compute patterns — the ground truth of computation
Layer 2: call (non-deterministic) + look (deterministic BBG read)
Layer 3: 30+ jets across 5 algebras       — optimization without changing meaning

remove Layer 3: identical results, orders of magnitude slower. remove Layer 2: no privacy (call), no state access (look). remove Layer 1: nothing remains. see jets/ for the full jet registry.

adding new instantiations

the 5-bit encoding, the trace layout, the budget metering, the confluence property — all are properties of the abstract pattern set, not of a specific field. a new instantiation reuses the same spec with different F, W, H parameters. see the five algebras section for the current instantiation table and cross-algebra composition.

specification index

dependencies