superseded: this page was written against the retired zheng design (Merkle-free Brakedown, unchecked HyperNova fold), which was unsound; its old size and time figures do not hold. The body below now names the current design (Spartan over CCS, one WHIR opening, phase-3 ARC-style accumulation) and the goal (≤ 64 KB, verify ≤ 1 ms, constant in steps). The repair and the measured numbers live in soft3 proposals/proof-system-repair.
polynomial target — nox engine for the polynomial proof system
the opportunity
trident compiles to 20 VM targets. none of them is nox. adding nox as an engine target gives every trident program access to the polynomial proof system: proof-carrying execution, hash-based proofs with one WHIR opening (goal ≤ 64 KB, verify ≤ 1 ms), O(1) data access, 3-5 constraint state operations, and a decider that verifies all history as one WHIR opening of the final accumulator (phase 3 of the repair, landing this release; size and time TODO(F-numbers)).
no language change. no new syntax. one new compilation backend. the polynomial proof system becomes available to every .tri program.
what changes
new engine: nox
trident → NoxLowering → nox formula (16 patterns) → proof-carrying execution → done
NoxLowering is structurally similar to the existing TreeLowering (Nock target). both emit tree-structured combinators. the difference:
- Nock: 12 rules, natural number arithmetic, increment-based
- nox: 16 patterns, Goldilocks field arithmetic, inverse, hash, hint
the mapping:
| trident concept | Nock lowering | nox lowering |
|---|---|---|
| integer literal | Nock atom (natural number) | nox atom (field element) |
| addition | Nock increment loop | nox pattern 5 (add), O(1) |
| multiplication | Nock repeated addition | nox pattern 7 (mul), O(1) |
| comparison | Nock equals + increment | nox pattern 9 (eq) / 10 (lt), O(1) |
| conditional | Nock 6 (if-then-else) | nox pattern 4 (branch) |
| data access | Nock slot (tree walk) | nox pattern 0 (axis), O(1) via PCS |
| construction | Nock cons | nox pattern 3 (cons) |
| function call | Nock 9 (invoke) | nox pattern 2 (compose) |
| hash | not native | nox pattern 15 (hemera) |
| witness | not native | nox pattern 16 (hint) |
nox is a STRICT UPGRADE over Nock for trident: every Nock operation maps to a nox pattern, plus field arithmetic (O(1) instead of increment loops), cryptographic hash (native), and witness injection (privacy).
replace Tip5 with hemera
trident's stdlib uses Tip5 (5-round Goldilocks hash). the polynomial proof system uses hemera (24-round Poseidon2, x⁻¹ S-box). one hash across the entire stack:
current: trident uses Tip5, cyber stack uses hemera → two hashes, two security analyses
polynomial: everything uses hemera → one hash, one security analysis (Merkle trees, Fiat–Shamir, identity)
change: std.crypto.hash implementation switches from Tip5 to hemera. API unchanged. programs recompile without source changes.
replace Tier 2-3 TIR operations
12 of 54 TIR operations assume FRI/Merkle. replace with polynomial equivalents:
Tier 2 (provable) — hash tree operations → PCS operations:
| current TIROp | what it does | replacement | cost change |
|---|---|---|---|
| SpongeInit | initialize hash sponge | hemera_init | same |
| SpongeAbsorb | absorb field elements | hemera_absorb | same |
| SpongeSqueeze | squeeze hash output | hemera_squeeze | same |
| MerkleStep | verify one tree level | PCS.open (polynomial evaluation) | O(log N) → O(1) |
Tier 3 (recursion) — FRI operations → accumulation operations:
| current TIROp | what it does | replacement | cost change |
|---|---|---|---|
| ExtMul | cubic extension multiply | keep (soundness amplification) | same |
| ExtInvert | cubic extension inverse | keep | same |
| FoldExt | FRI folding (extension) | accumulation step (ARC-style, phase 3) | different algorithm |
| FoldBase | FRI folding (base) | accumulation step (ARC-style, phase 3) | different algorithm |
| ProofBlock | recursive verification container | accumulate_row (proof-carrying) | measured cost TODO(F-numbers) |
New TIROps:
| new TIROp | what it does | tier | cost |
|---|---|---|---|
| PCSCommit | lens.commit(polynomial) — WHIR, hemera Merkle | 2 | O(N log N) field ops + hashing |
| PCSOpen | lens.open(polynomial, point) — one WHIR opening | 2 | polylog(N) queries + Merkle paths |
| Accumulate | accumulation step: batch RS evaluation claims by sumcheck, commit one word, open a few queries (ARC-style, phase 3, landing this release) | 3 | TODO(F-numbers) |
| AccumulateRow | proof-carrying accumulation step during execution | 3 | TODO(F-numbers) |
state jet recognition
the NoxLowering backend recognizes common patterns in trident code and emits state jet annotations:
// trident source
fn transfer(ledger: State, from: Key, to: Key, amount: Field) {
let balance_from = ledger.read(from);
assert(balance_from >= amount);
ledger.write(from, balance_from - amount);
ledger.write(to, ledger.read(to) + amount);
}
the compiler recognizes: 2 reads + range check + 2 writes + conservation = TRANSFER pattern.
without state jet: nox trace of ~200 steps → ~1,600 constraints
with state jet: TRANSFER pattern recognized → 3 constraints
speedup: 530×
the programmer writes normal code. the compiler handles the optimization. state jets fire at the nox level, not the trident level — NoxLowering just needs to emit the pattern that nox's jet registry recognizes.
cost model update
trident's cost model (AIR table sizes for Triton) doesn't apply to the polynomial proof system. new cost model for nox engine:
nox cost model:
cost(program) = Σ pattern_costs
pattern 0 (axis): 1 field op (O(1) PCS opening)
patterns 1-4: 1 field op each
patterns 5-10: 1 field op each (field arithmetic)
patterns 11-14: 1 field op each (bitwise, but ~32 constraints in F_p)
pattern 15 (hash): 736 constraints (hemera)
pattern 16 (hint): 1 (witness injection)
accumulation: per-step cost TODO(F-numbers) (proof-carrying)
total proof cost: Σ (pattern_cost + accumulation) per step
decider: one WHIR opening of the final accumulator (once, at verification)
simpler than Triton's multi-table model. the cost IS the polynomial degree, which IS the evaluation table size.
trident build main.tri --engine nox --costs
function steps field_ops hemera accumulation
──────── ───── ───────── ────── ────────────
transfer() 12 12 0 TODO(F-numbers)
mint_card() 45 48 736 TODO(F-numbers)
verify_sig() 200 264 736 TODO(F-numbers)
total: 257 324 1,472 TODO(F-numbers)
decider: one WHIR opening
proof size: goal ≤ 64 KB (≤ 16–20 KB for small statements); measured TODO(F-numbers)
verify: goal ≤ 1 ms; measured TODO(F-numbers)
what trident programs gain
triton target (current) nox target (polynomial)
proof size: ~200 KiB goal ≤ 64 KB, constant in steps
verify: ~50 ms goal ≤ 1 ms (succinct profile today: 7.96 ms at hash.tri)
prover: O(N log N) O(N)
recursion: ~200K constraints/level accumulation step (ARC-style), cost TODO(F-numbers)
data access: O(log N) Merkle walk O(1) PCS opening
hash calls: thousands (sponge-heavy) hemera Merkle trees + Fiat–Shamir
state operations: full trace 3-5 constraints (state jets)
proving latency: separate phase (Trisha) zero (proof-carrying)
identity: Tip5 hash hemera(PCS.commit ‖ tag)
DAS: separate infrastructure native (polynomial extension)
every .tri program recompiled with --engine nox gets these improvements. source code unchanged.
std library impact
std.nn (neural networks)
current: neural ops in Goldilocks → prove via Triton STARK
polynomial: neural ops → polynomial nouns (model = polynomial)
quantized inference → Binius F₂ jets (1,400×)
model weights → PCS-committed, O(1) layer access
proof: carried during inference (zero latency)
std.private (FHE)
current: FHE primitives planned, no proving integration
polynomial: R_q = F_p[x]/(x^n+1) where p = Goldilocks
ring operations = nebu NTT (zero conversion)
proving FHE = proving polynomial ops = native
~1% proving overhead on top of FHE cost
trinity: quantum-safe + private + provable = enabled
std.quantum (quantum simulation)
current: quantum gates over Goldilocks extension fields
polynomial: same gates, proofs at the stack goal (≤ 64 KB) instead of ~200 KiB
long simulations accumulate step by step (phase 3 accumulation)
quantum error correction circuits → state jets
implementation plan
phase 1: NoxLowering backend ~4 sessions
add vm/nox/ engine config
implement NoxLowering trait (similar to TreeLowering)
map TIR operations to nox 16 patterns
emit nox formulas from trident AST
phase 2: hemera migration ~2 sessions
replace Tip5 with hemera in std.crypto.hash
update SpongeInit/Absorb/Squeeze TIROps for hemera parameters
update content addressing in package system
phase 3: Tier 2-3 TIROp update ~3 sessions
replace MerkleStep with PCSOpen
replace FoldExt/FoldBase with the accumulation step
replace ProofBlock with AccumulateRow
add PCSCommit, PCSOpen, Accumulate, AccumulateRow TIROps
phase 4: cost model ~2 sessions
implement NoxCostModel (polynomial degree-based)
integrate with trident build --costs
update trident bench for nox baselines
phase 5: state jet annotations ~2 sessions
pattern recognition in NoxLowering (TRANSFER, INSERT, UPDATE)
emit jet-recognizable nox formulas
test: trident transfer() → 3 constraints via state jet
total: ~13 sessions (~39 hours)
the 14 languages through polynomial proofs
trident's 14 algebraically irreducible languages ALL compile through nox:
| language | algebra | nox field | PCS | what polynomial proofs enable |
|---|---|---|---|---|
| Tri | $\mathbb{F}_{p^n}$ tower | Goldilocks | WHIR | native field tower proofs |
| Tok | UTXO conservation | Goldilocks | WHIR | state jets for transfers (3 constraints) |
| Arc | category theory | Goldilocks | WHIR | graph schema as polynomial |
| Seq | partial order | Goldilocks | WHIR | causal ordering via PCS |
| Inf | Horn clauses | Goldilocks | WHIR | logic as polynomial evaluation |
| Bel | distributions | Goldilocks | WHIR | probability as polynomial coefficients |
| Ren | Clifford algebra | Goldilocks | WHIR | geometric product as field ops |
| Dif | manifolds | Goldilocks | WHIR | continuous dynamics discretized |
| Sym | Hamiltonian | Goldilocks | WHIR | physics simulation proved |
| Wav | $R_q$ convolution | Goldilocks | WHIR | FHE native (R_q = Goldilocks NTT) |
| Ten | tensor contraction | Goldilocks/F₂ | WHIR/Binius | neural inference 1,400× |
| Bt | F₂ tower | F₂ | Binius | binary ops native |
| Rs | Z/2ⁿ words | split | split | systems programming proved |
14 languages → 16 nox patterns → 1 polynomial proof system → succinct profile today: hash.tri 15,921 B proof, verify 7.96 ms; a 2^20 relation 71,081 B, verify 270 ms (zheng audit/succinct-profile-2026-10.md). the goal is ≤ 64 KB, verify ≤ 1 ms, constant in the number of steps; it is not met yet.
see polynomial proof system for the proof architecture, nox for the 16 patterns, polynomial nouns for the data model, WHIR for the PCS, state-operations for CCS jets, hemera for the hash