# 🗡️ Trident Language Reference
Trident is a programming language for provable computation. One source
file is designed to compile to 20 virtual machines — from zero-knowledge
proof systems to EVM, WASM, and native x86-64. Write once. Prove anywhere.
---
# Part I — Universal Language (Tier 0 + Tier 1)
Everything here works on every target. A program that uses only Part I
features compiles for TRITON, MIDEN, SP1, OPENVM, CAIRO, and any
future target.
---
## 1. Programs and Modules
Every `.tri` file starts with exactly one of:
```trident
program my_program // Executable — must have fn main()
module my_module // Library — no fn main, provides reusable items
```
### Imports
```trident
use merkle // import module
use crypto.sponge // nested module (directory-based)
```
Rules:
- `use` imports a module by name, accessed via dot notation (`merkle.verify(...)`)
- No wildcard imports (`use merkle.*` is forbidden)
- No renaming (`use merkle as m` is forbidden)
- No re-exports — if A uses B, C cannot access B through A
- No circular dependencies — the dependency graph must be a DAG
### Visibility
Two levels only:
- `pub` — visible to any module that imports this one
- default — private to this module
No `pub(crate)`, no `friend`, no `internal`.
```trident
module wallet
pub struct Balance {
pub owner: Digest, // visible to importers
amount: Field, // private to this module
}
pub fn create(owner: Digest, amount: Field) -> Balance {
Balance { owner, amount }
}
```
### Project Layout
```text
my_project/
├── main.tri // program entry point
├── merkle.tri // module merkle
├── crypto/
│ └── sponge.tri // module crypto.sponge
└── trident.toml // project manifest
```
#### trident.toml
```toml
[project]
name = "my_project"
version = "0.1.0"
entry = "main.tri"
```
---
## 2. Types
### Primitive Types
| `Field` | 1 | Native field element of the target VM |
| `Bool` | 1 | Field constrained to {0, 1} |
| `U32` | 1 | Unsigned 32-bit integer, range-checked |
| `Digest` | D | Hash digest `[Field; D]` — universal content identifier |
`Field` means "element of the target VM's native field." Programs reason about
field arithmetic abstractly; the target implements it concretely.
`Digest` is universal — every target has a hash function and produces digests.
It is a content identifier: the fixed-width fingerprint of arbitrary data. The
width D varies by target (5 on TRITON, 4 on MIDEN, 8 on SP1/OPENVM, 1 on CAIRO).
No implicit conversions. `Field` and `U32` do not auto-convert. Use `as_field()`
and `as_u32()` (the latter inserts a range check).
For extension field types, see [Extension Field](#16-extension-field).
### Composite Types
| `[T; N]` | N * width(T) | Fixed-size array, N compile-time known |
| `(T1, T2, ...)` | sum of widths | Tuple (max 16 elements) |
| `struct S { ... }` | sum of field widths | Named product type |
Array sizes support compile-time expressions: `[Field; N]`, `[Field; M+N]`,
`[Field; N*2]`.
No enums. No sum types. No references. No pointers. All values are passed by
copy on the stack. Structs are flattened to sequential stack/RAM elements.
### Type Widths
All types have a compile-time-known width measured in field elements.
Widths marked with a variable are resolved from the target configuration.
| `Field` | 1 |
| `Bool` | 1 |
| `U32` | 1 |
| `Digest` | D (`digest_width` from target config) |
| `[T; N]` | N * width(T) |
| `(T1, T2)` | width(T1) + width(T2) |
| `struct` | sum of field widths |
---
## 3. Declarations
### Functions
```trident
fn private_fn(x: Field) -> Field { x + 1 }
pub fn public_fn(x: Field) -> Field { x + 1 }
```
- No default arguments, no variadic arguments
- No function overloading, no closures
- No recursion — call graph must be a DAG
- Maximum 16 parameters (stack depth)
- Tail expression is the return value
### Size-Generic Functions
```trident
fn sum<N>(arr: [Field; N]) -> Field {
let mut total: Field = 0
for i in 0..N { total = total + arr[i] }
total
}
fn concat<M, N>(a: [Field; M], b: [Field; N]) -> [Field; M+N] { ... }
```
Size parameters appear in angle brackets. Each unique combination of size arguments
produces a monomorphized copy at compile time.
```trident
let a: [Field; 3] = [1, 2, 3]
let total: Field = sum(a) // N=3 inferred from argument type
let total: Field = sum<3>(a) // N=3 explicit
```
Only integer size parameters — no type-level generics.
### Structs
```trident
struct Point { x: Field, y: Field }
pub struct PubPoint { pub x: Field, pub y: Field }
let p = Point { x: 1, y: 2 }
let x: Field = p.x
```
### Events
```trident
event Transfer { from: Digest, to: Digest, amount: Field }
```
Events are declared at module scope. Fields must be `Field`-width types.
Maximum 9 fields. Events are emitted with `reveal` (public) or `seal`
(committed) — see [Part II: Events](#10-events).
### Constants
```trident
const MAX_DEPTH: U32 = 32
pub const ZERO: Field = 0
```
Inlined at compile time. No runtime cost.
### I/O Declarations (program modules only)
```trident
pub input: [Field; 3] // public input (visible to verifier)
pub output: Field // public output
sec input: [Field; 5] // secret input (prover only)
sec ram: { 17: Field, 42: Field } // pre-initialized RAM slots
```
---
## 4. Expressions and Operators
### Operator Table
| `a + b` | Field, Field | Field | Field addition |
| `a + N` | Field, literal | Field | Immediate addition |
| `a * b` | Field, Field | Field | Field multiplication |
| `a == b` | Field, Field | Bool | Field equality |
| `a < b` | U32, U32 | Bool | Unsigned less-than |
| `a & b` | U32, U32 | U32 | Bitwise AND |
| `a ^ b` | U32, U32 | U32 | Bitwise XOR |
| `a /% b` | U32, U32 | (U32, U32) | Division + remainder |
No subtraction operator (`-`). No division operator (`/`). No `!=`, `>`, `<=`,
`>=`. No `&&`, `||`, `!`. Use builtins: `sub(a, b)`, `neg(a)`, `inv(a)`.
For extension field operators, see [Extension Field](#16-extension-field).
### Other Expressions
```trident
p.x // field access
arr[i] // array indexing
Point { x: 1, y: 2 } // struct initialization
[1, 2, 3] // array literal
(a, b) // tuple literal
{ let x: Field = 1; x + 1 } // block with tail expression
```
---
## 5. Statements
### Let Bindings
```trident
let x: Field = 42 // immutable
let mut counter: U32 = 0 // mutable
let (hi, lo): (U32, U32) = split(x) // tuple destructuring
```
### Assignment
```trident
counter = counter + 1
p.x = 42
arr[i] = value
(a, b) = some_function() // tuple assignment
```
### If / Else
```trident
if condition {
// body
} else {
// body
}
```
No `else if` — use nested `if/else`. Condition must be `Bool` or `Field`
(0 = false, nonzero = true).
### For Loops
```trident
for i in 0..32 { body } // constant bound — exactly 32 iterations
for i in 0..n bounded 64 { body } // runtime bound — at most 64 iterations
```
All loops must have a compile-time-known or declared upper bound. This guarantees
the compiler can compute exact trace length.
No `while`. No `loop`. No `break`. No `continue`.
### Match
```trident
match value {
0 => { handle_zero() }
1 => { handle_one() }
_ => { handle_default() }
}
```
Patterns: integer literals, `true`, `false`, struct destructuring, `_` (wildcard).
Exhaustiveness is enforced — wildcard `_` arm is required unless all values are covered.
```trident
// Struct pattern matching
match p {
Point { x: 0, y } => { handle_origin_x(y) }
Point { x, y: 0 } => { handle_origin_y(x) }
_ => { handle_general(p.x, p.y) }
}
```
### Return
```trident
fn foo(x: Field) -> Field {
if x == 0 { return 1 }
x + x // tail expression — implicit return
}
```
---
## 6. Builtin Functions
### I/O and Non-Deterministic Input
| `pub_read() -> Field` | Read 1 public input |
| `pub_read2()` ... `pub_read5()` | Read N public inputs |
| `pub_write(v: Field)` | Write 1 public output |
| `pub_write2(...)` ... `pub_write5(...)` | Write N public outputs |
| `divine() -> Field` | Read 1 secret input (prover only) |
| `divine3() -> (Field, Field, Field)` | Read 3 secret inputs |
| `divine5() -> Digest` | Read D secret inputs as Digest |
### Field Arithmetic
| `sub(a: Field, b: Field) -> Field` | Subtraction: a + (p - b) |
| `neg(a: Field) -> Field` | Additive inverse: p - a |
| `inv(a: Field) -> Field` | Multiplicative inverse |
### U32 Operations
| `split(a: Field) -> (U32, U32)` | Split field to (hi, lo) u32 pair |
| `as_u32(a: Field) -> U32` | Range-checked conversion |
| `as_field(a: U32) -> Field` | Type cast (zero cost) |
| `log2(a: U32) -> U32` | Floor of log base 2 |
| `pow(base: U32, exp: U32) -> U32` | Exponentiation |
| `popcount(a: U32) -> U32` | Hamming weight (bit count) |
### Assertions
| `assert(cond: Bool)` | Crash VM if false — proof generation impossible |
| `assert_eq(a: Field, b: Field)` | Assert equality |
| `assert_digest(a: Digest, b: Digest)` | Assert digest equality |
### Memory
| `ram_read(addr) -> Field` | Read 1 word |
| `ram_write(addr, val)` | Write 1 word |
| `ram_read_block(addr) -> [Field; D]` | Read D words (D = digest width) |
| `ram_write_block(addr, vals)` | Write D words |
### Hash
| `hash(fields: Field x R) -> Digest` | Hash R field elements into a Digest (R = target hash rate) |
`hash()` is the Tier 1 hash operation — available on every target. The rate R
and digest width D are target-dependent. The user-facing function name varies
by target: `vm.crypto.hash.tip5()` on TRITON, with other targets providing
their native hash function. All compile to the `Hash` TIR operation internally.
See [targets.md](targets.md) for per-VM hash functions.
For sponge, Merkle, and extension field builtins (Tier 2-3), see
[Part II](#part-ii--provable-computation-tier-2--tier-3) below.
### Portable OS (`os.*`)
The `os.*` modules provide portable OS interaction — neuron identity,
signals, state, and time. They are not builtins (they're standard library
functions), but they compile to target-specific lowerings just like
builtins do.
| `os.neuron` | `id() -> Digest`, `verify(expected: Digest) -> Bool`, `auth(credential: Digest) -> ()` | Target has identity |
| `os.signal` | `send(from: Digest, to: Digest, amount: Field)`, `balance(neuron: Digest) -> Field` | Target has native value |
| `os.state` | `read(key: Field) -> Field`, `write(key, value)`, `exists(key)` | Target has persistent state |
| `os.time` | `now() -> Field`, `step() -> Field` | All targets |
These sit between `std.*` (pure computation, all targets) and `os.<os>.*`
(OS-native, one target). A program using only `std.*` + `os.*` compiles
to any OS that supports the required concepts. The compiler emits clear
errors when targeting an OS that lacks a concept (e.g., `os.neuron.id()`
on UTXO chains, `os.signal.send()` on journal targets).
For full API specifications and per-OS lowering tables, see [os.md](os.md).
---
## 7. Attributes
| `#[cfg(flag)]` | Conditional compilation |
| `#[test]` | Test function — run with `trident test` |
| `#[pure]` | No I/O side effects allowed |
| `#[intrinsic(name)]` | Maps to target instruction (std modules only) |
| `#[requires(predicate)]` | Precondition — checked by `trident audit` |
| `#[ensures(predicate)]` | Postcondition — `result` refers to return value |
```trident
#[pure]
fn compute(a: Field, b: Field) -> Field { a * b + a }
#[requires(amount > 0)]
#[ensures(result == sub(balance, amount))]
fn withdraw(balance: Field, amount: Field) -> Field {
sub(balance, amount)
}
#[test]
fn test_withdraw() {
assert_eq(withdraw(100, 50), 50)
}
```
---
## 8. Memory Model
### Stack
The operational stack has 16 directly accessible elements. The compiler manages
stack layout automatically — variables are assigned stack positions, and when more
than 16 are live, the compiler spills to RAM via an LRU policy.
The developer does not manage the stack.
### RAM
Word-addressed memory. Each cell holds one Field element.
```trident
ram_write(17, value)
let v: Field = ram_read(17)
```
RAM is non-deterministic on first read — if an address hasn't been written,
reading returns whatever the prover supplies. Constrain with assertions.
### No Heap
No dynamic allocation. No `alloc`, no `free`, no garbage collector. All data
structures have compile-time-known sizes. This guarantees deterministic memory
usage and predictable trace length.
---
## 9. Inline Assembly
```trident
asm { dup 0 add } // zero net stack effect (default)
asm(+1) { push 42 } // pushes 1 element
asm(-2) { pop 1 pop 1 } // pops 2 elements
asm(triton)(+1) { push 42 } // target-tagged + effect
asm(miden) { dup.0 add } // MIDEN assembly
```
Target-tagged blocks are skipped when compiling for a different target.
A bare `asm { ... }` is treated as `asm(triton) { ... }` for backward
compatibility.
The compiler does not parse, validate, or optimize assembly contents. The effect
annotation `(+N)` / `(-N)` is the contract between hand-written assembly and
the compiler's stack model.
---
## 10. Events
Events are structured data output — the universal communication mechanism.
On provable targets, events are how programs talk to the OS. On native
targets, they're structured logging (like `console.log`).
### Declaration
Events are declared at module scope (see [Section 3](#3-declarations)):
```trident
event Transfer { from: Digest, to: Digest, amount: Field }
```
Fields must be `Field`-width types. Maximum 9 fields.
### Reveal (Public Output)
```trident
reveal Transfer { from: sender, to: receiver, amount: value }
```
Each field is written to public output. The verifier sees all data.
`reveal` is Tier 1 — it works on every target.
### Seal (Committed Secret)
```trident
seal Transfer { from: sender, to: receiver, amount: value }
```
Fields are hashed via the sponge construction. Only the commitment digest is
written to public output. The verifier sees the commitment, not the data.
`seal` requires sponge support (Tier 2).
---
## 11. Audit vs Verify
Two distinct commands share the "check correctness" concept:
| `trident audit` | Source code contracts | Symbolic execution, algebraic solver | Local (Trident) |
| `trident verify` | Proof artifacts | STARK/SNARK proof verification | Warrior (external) |
`audit` is static analysis — it checks `#[requires]`/`#[ensures]`
contracts without executing the program. It runs entirely within Trident.
`verify` checks a proof file produced by `trident prove`. It delegates
to a warrior binary that has the target-specific verifier (e.g. triton-vm's
`verify()` function). "Client" and "warrior" are two naming registers
for the same concept — geeky and gamy respectively. Both refer to the
external binary that handles execution, proving, and verification for a
specific battlefield (target). See [targets.md](targets.md#warriors).
---
## 12. Type Checking Rules
- No implicit conversions between any types
- No recursion — the compiler rejects call cycles across all modules
- Exhaustive match required (wildcard or all cases covered)
- `#[pure]` functions cannot perform I/O (`pub_read`, `pub_write`, `divine`,
`sponge_init`, etc.)
- `#[intrinsic]` only allowed in std modules
- `asm` blocks tagged for a different target are rejected
- Dead code after unconditional halt/assert is rejected
- Unused imports produce warnings
---
## 13. Permanent Exclusions
These are design decisions, not roadmap items.
| Strings | No string operations in any target VM ISA |
| Dynamic arrays | Unpredictable trace length |
| Heap allocation | Non-deterministic memory, no GC |
| Recursion | Unbounded trace; use bounded loops |
| Closures | Requires dynamic dispatch |
| Type-level generics | Compile-time complexity, audit difficulty |
| Operator overloading | Hides costs |
| Inheritance / Traits | Complexity without benefit |
| Exceptions | Use assert; failure = no proof |
| Floating point | Not supported by field arithmetic |
| Macros | Source-level complexity |
| Concurrency | VM is single-threaded |
| Wildcard imports | Obscures dependencies |
| Circular dependencies | Prevents deterministic compilation |
---
# Part II — Provable Computation (Tier 2 + Tier 3)
Proof-capable targets only. No meaningful equivalent on non-provable targets.
Two capabilities: incremental algebraic hashing (sponge + Merkle) and
extension field arithmetic. Programs using any Tier 2 feature cannot compile
for Tier 1-only targets (SP1, OPENVM, CAIRO).
See [targets.md](targets.md) for tier compatibility.
Note: `hash()` is Tier 1 (universal) and documented in
[Section 6](#6-builtin-functions). The builtins below are Tier 2+.
---
## 14. Sponge
The sponge API enables incremental hashing of data larger than R fields.
Initialize, absorb in chunks, squeeze the result. The rate R is
target-dependent: 10 on TRITON, 8 on MIDEN.
| `sponge_init()` | `SpongeInit` | Initialize sponge state |
| `sponge_absorb(fields: Field x R)` | `SpongeAbsorb` | Absorb R fields |
| `sponge_absorb_mem(ptr: Field)` | `SpongeLoad` | Absorb R fields from RAM |
| `sponge_squeeze() -> [Field; R]` | `SpongeSqueeze` | Squeeze R fields |
---
## 15. Merkle Authentication
| `merkle_step(idx: U32, d: Digest) -> (U32, Digest)` | `MerkleStep` | One tree level up |
| `merkle_step_mem(ptr, idx, d) -> (Field, U32, Digest)` | `MerkleLoad` | Tree level from RAM |
`merkle_step` authenticates one level of a Merkle tree. Call it in a loop
to verify a full Merkle path:
```trident
pub fn verify(root: Digest, leaf: Digest, index: U32, depth: U32) {
let mut idx = index
let mut current = leaf
for _ in 0..depth bounded 64 {
(idx, current) = merkle_step(idx, current)
}
assert_digest(current, root)
}
```
---
## 16. Extension Field
The extension field extends `Field` to degree E (E = 3 on TRITON and NOCK).
Only available on targets where `xfield_width > 0`.
### Type
| `XField` | E | Extension field element (E = `xfield_width` from target config) |
### Operator
| `a *. s` | XField, Field | XField | Scalar multiplication |
### Builtins
| `xfield(x0, ..., xE) -> XField` | *(constructor)* | Construct from E base field elements |
| `xinvert(a: XField) -> XField` | `ExtInvert` | Multiplicative inverse |
| `xx_dot_step(acc, ptr_a, ptr_b) -> (XField, Field, Field)` | `FoldExt` | XField dot product step |
| `xb_dot_step(acc, ptr_a, ptr_b) -> (XField, Field, Field)` | `FoldBase` | Mixed dot product step |
The dot-step builtins are building blocks for inner product arguments and FRI
verification — the core of recursive proof composition.
Note: The `*.` operator (scalar multiply) maps to `ExtMul` in the IR.
---
## 17. Proof Composition (Tier 3)
Proofs that verify other proofs. TRITON and NOCK only.
Tier 3 enables a program to verify another program's proof inside its own
execution. This is STARK-in-STARK recursion: the verifier circuit runs as
part of the prover's trace.
```trident
// Verify a proof of program_hash and use its public output
proof_block(program_hash) {
// verification circuit runs here
// public outputs of the inner proof become available
}
```
Tier 3 uses the extension field builtins above plus dedicated IR operations:
- ProofBlock — Wraps a recursive verification circuit
- FoldExt / FoldBase — FRI folding over extension / base field
- ExtMul / ExtInvert — Extension field arithmetic for the verifier
See [ir.md Part I, Tier 3](ir.md) for the full list of 5 recursive operations.
Only TRITON and NOCK support Tier 3. Programs using proof composition
cannot compile for any other target.
---
## 🔗 See Also
- [Agent Briefing](briefing.md) — AI-optimized compact cheat-sheet
- [Standard Library](stdlib.md) — `std.*` modules
- [OS Reference](os.md) — OS concepts, `os.*` gold standard, extensions
- [VM Reference](vm.md) — VM registry, lowering paths, cost models
- [CLI Reference](cli.md) — Compiler commands and flags
- [Grammar](grammar.md) — EBNF grammar
- [IR Reference](ir.md) — Compiler intermediate representation (54 ops, 4 tiers)
- [Target Reference](targets.md) — OS model, integration tracking, how-to-add checklists
- [Error Catalog](errors.md) — All compiler error messages explained
- [Tutorial](../docs/tutorials/tutorial.md) — Step-by-step developer guide
---
*Trident v0.5 — Write once. Prove anywhere.*