Trident on EVM
Context
EVM is declared in the target registry at integration level L1 — engine
evm has vm/evm/target.toml and a reference page; union ethereum
has os/ethereum/target.toml and a reference page. Lowering is
unimplemented, os.ethereum.* has zero .tri modules, no cost model,
no tests. EvmLowering is listed as a planned specialized trait
alongside WasmLowering, AcirLowering, MoveLowering.
Ethereum already has a saturated language market: Solidity in production, Vyper for the security-conscious minority, Fe v0.4-alpha from Argot as the long-bet Rust-flavored successor, Yul as the IR. The question this proposal answers: what does Trident bring to that market that none of the incumbents structurally can?
What Trident gives Ethereum
Six capabilities that Solidity, Vyper, Fe, and Yul cannot deliver, ordered by which payoff Trident lands first.
1. One source for the zk circuit and its on-chain verifier
The same .tri file proves off-chain on any provable engine (Triton,
Miden, RISC Zero, SP1, OpenVM, Jolt) and emits the matching Ethereum
verifier contract from the same normalized AST. One identity (the
content hash) covers both the prover and the verifier. The current
pipeline needs Circom or Noir for the circuit plus an auto-generated
Solidity verifier as a separate artifact — two languages, two trust
surfaces, no shared identity. Trident collapses them.
2. Decidable automatic formal verification in the compiler
#[requires] / #[ensures] annotations are discharged by
trident audit at compile time. Bounded loops + no recursion +
finite-field arithmetic make the verification problem decidable, so
the compiler ships a proof or a counterexample on every commit.
SMTChecker is best-effort, Certora is external and paid, Halmos is
symbolic execution that times out. Every contract deployed to
Ethereum could carry a machine-checked proof of its declared
properties — generated by the same toolchain that builds the bytecode.
3. Content-addressed function identity that survives the chain
A function's identity is the hash of its normalized AST, computed before lowering. The same function deployed to Ethereum, Neptune, Solana, Cosmos has the same identity. Solidity's bytecode hash differs per compiler version and per chain; Fe inherits the same problem. Cross-chain code reuse becomes addressable instead of "trust this redeployment is the same."
4. STARK-proven compilation
The compiler self-hosts and produces a STARK proof that emitted bytecode corresponds to source. Etherscan "Verified Contract" is a re-compilation trust ritual; the Trident claim is mathematical. Solves Thompson's trust-chain problem at the level of the compiler, not the social layer.
5. Static, exact cost analysis before deployment
trident build --cost reports the cycle budget in the build log. For
zk verifier contracts on Ethereum (where prover cost dominates) and
for L2 execution (where prover cost is the actual bill), this changes
the development loop from "deploy, simulate, pray" to "the cost is in
the artifact."
6. Trinity composition — FHE + neural + hashing + quantum in one trace
Any of these can land on Ethereum today as a verifier contract receiving a proof. None of the existing EVM languages can express the combination in a single source — none have field-native types or a proof model to host it. If private AI inference, encrypted DeFi, or post-quantum-secure logic ever reaches Ethereum mainnet via verifier contracts, the source for the verified thing can be Trident.
Which payoffs need which mode
| Capability | Mode A (Solidity-replacement) | Mode B (verifier generator) | Mode C (rollup app) |
|---|---|---|---|
| 1. One source, both ends | -- | Y | Y |
| 2. Decidable verification | Y | Y | Y |
| 3. Content-addressed identity | Y | Y | Y |
| 4. STARK-proven compilation | Y | Y | Y |
| 5. Static cost analysis | Y | Y | Y |
| 6. Trinity composition | -- | Y | Y |
Mode A ships Tier 0 only; competes with Fe head-on. Mode B unifies circuit and verifier — the unique claim. Mode C runs and proves on Triton/Neptune; Ethereum is settlement glue.
Design Questions
Q1: Word size and field
EVM word is 256 bits; Trident's Field is Goldilocks (64 bits). Three
implementations exist and the target file should pick one:
| Option | Field | Tradeoff |
|---|---|---|
| A. Goldilocks emulated | uint256 constrained to < 2^64 - 2^32 + 1 |
Source-identical to Triton. ~5x mulmod cost vs native u64. Single conditional subtract for reduction. |
| B. Curve-scalar prime | uint256 mod r where r = BN254 scalar |
Matches what existing EVM zk verifiers use. Pays off when contract is a verifier for a Trident-proven program. |
| C. Per-target field | Declared in vm/evm/target.toml [field] section |
Already matches the five-layer architecture. Compiler reduces all Field ops mod the target prime. |
C subsumes A and B and is the only forward-compatible choice. The target declares one prime; the user picks the deployment.
Q2: Digest
Parametric. Digest = bytes32 on EVM, hash() lowers to Keccak256
precompile (30 gas + 6/word). std.crypto.keccak256 is already Done
in the stdlib. No new work for the type system.
Q3: Tier 1 on EVM
divine() requires a prover; EVM has no prover. Two paths:
- Drop Tier 1. Trident-on-EVM = Mode A. Loses zk story.
- Compile Tier 1 to a verifier contract. Same
.trisource: prove off-chain on Triton (or any provable engine), emit a Solidity verifier from the proof shape. Mode B — the novel claim.
Both can coexist. The build flag selects.
Q4: EVM idioms that don't translate
Trident's bounded-execution rules exclude common Solidity patterns:
delegatecallproxies — dynamic dispatch is not bounded- Recursive calls — Trident forbids recursion
- Heap allocation — Trident has none
- Dynamic storage layouts — Trident sizes are static
The proposal: do not chase parity with Solidity idioms. Trident contracts are provable functions over typed state. Patterns that violate that get rejected at compile time with a clear error pointing at the offending construct.
Q5: ABI and tooling integration
A Trident contract must be callable from existing Solidity code, must appear on Etherscan, must be testable from Foundry. Minimum surface:
- ABI emission —
trident build --target ethereum --emit abi - Solidity FFI header — auto-generated
.solinterface for callers - Forge-compatible artifacts —
forge buildcan pick up Trident output if it lives inout/
Engineering plan
Phase 1: EvmLowering trait (NOW — 6 sessions)
EVM is a stack machine, so the closest analog is tir/lower/triton.rs.
Most of the structure transfers; the difference is instruction
selection (PUSH/DUP/SWAP/ADD/MUL/SSTORE/SLOAD/CALL/JUMP) and word
size (256-bit, not field).
| Task | Pomodoros |
|---|---|
src/tir/lower/evm.rs — StackLowering impl |
8 |
| Field-on-EVM lowering (addmod/mulmod, target-declared prime) | 4 |
| Keccak256 builtin lowering (precompile call) | 2 |
| Bigint passthrough (std.crypto.bigint maps to native uint256) | 2 |
| Control flow (if/for → JUMP/JUMPI with stack discipline) | 4 |
Register in create_stack_lowering() factory |
1 |
| Lowering tests (~30) | 6 |
src/cost/model/evm.rs — gas cost model |
4 |
| Total | 31 pomodoros = 5.2 sessions |
Deliverable: trident build --target evm hello.tri produces EVM
bytecode that runs in a geth EVM.
Phase 2: os.ethereum.* bindings (NOW — 3 sessions)
Zero modules today. Minimum surface:
| Module | What |
|---|---|
os.ethereum.storage |
slot-keyed SSTORE/SLOAD |
os.ethereum.account |
address, balance, nonce, code |
os.ethereum.event |
LOG0–LOG4 |
os.ethereum.call |
CALL, STATICCALL, DELEGATECALL (rejected at audit), CREATE |
os.ethereum.context |
msg.sender, msg.value, block.number, block.timestamp |
os.ethereum.abi |
encode/decode for Solidity ABI v2 |
| Task | Pomodoros |
|---|---|
| storage.tri + account.tri | 3 |
| event.tri + call.tri | 3 |
| context.tri + abi.tri | 3 |
| Tests (compilation + e2e) | 4 |
| Docs (reference/os/ethereum.md expansion) | 2 |
| Bring union to L2 | 1 |
Set [status] level = 2, ext_modules = 6 |
1 |
| Total | 17 pomodoros = 2.8 sessions |
Phase 3: Verifier-codegen path (Mode B) (NEXT — 4 sessions)
The novel claim. From a Tier-1 .tri source plus a chosen proving
backend (Triton, default), emit a Solidity verifier contract that
checks proofs of that program's execution. Content-addressed by the
same hash as the prover.
| Task | Pomodoros |
|---|---|
| Proof-shape extraction from zheng output | 4 |
Verifier template in os/ethereum/verifier.tri |
6 |
trident build --target ethereum --emit verifier CLI |
2 |
| Gas-cost estimation for emitted verifier | 2 |
| End-to-end test: prove on Triton, deploy verifier, verify on geth | 6 |
| Documentation: explanation/verifier-codegen.md | 4 |
| Total | 24 pomodoros = 4 sessions |
Phase 4: Tooling glue (NEXT — 2 sessions)
| Task | Pomodoros |
|---|---|
| ABI emission from typed AST | 4 |
| Solidity FFI header auto-generation | 3 |
| Foundry artifact compatibility (out/ layout) | 3 |
| Etherscan verification helper (source + metadata bundle) | 2 |
| Total | 12 pomodoros = 2 sessions |
Phase 5: Audit pass for EVM-specific patterns (NEXT — 1 session)
EVM has its own footguns. Extend trident audit to catch them when
the target is ethereum:
| Pattern | What audit catches |
|---|---|
| Reentrancy | external call between state read and state write |
| Unbounded gas | loop without #[bound(N)] |
| Integer over/underflow in non-Field types | u32 / u256 arithmetic without explicit checked op |
| Storage collision | two modules writing the same slot |
| Delegatecall | rejected outright (violates bounded execution) |
| Task | Pomodoros |
|---|---|
| Reentrancy detector | 3 |
| Storage-collision detector | 2 |
| Audit rule docs in errors/ | 1 |
| Total | 6 pomodoros = 1 session |
Total estimate
| Phase | Status | Pomodoros | Sessions |
|---|---|---|---|
| 1. EvmLowering | NOW | 31 | 5.2 |
| 2. os.ethereum.* | NOW | 17 | 2.8 |
| 3. Verifier-codegen | NEXT | 24 | 4.0 |
| 4. Tooling glue | NEXT | 12 | 2.0 |
| 5. EVM audit pass | NEXT | 6 | 1.0 |
| Total | 90 | 15.0 |
Phases 1+2 are the minimum to claim Mode A (Solidity-replacement at Tier 0). Phase 3 is the minimum to claim Mode B (verifier-codegen) — the only mode that delivers all six unique capabilities.
Risks
-
Gas economics for Field-on-EVM. A
Field::mulis 8 gas (mulmod). A circuit that takes 10K rows on Triton lowers to ~50Kmulmods on EVM ≈ 400K gas. Acceptable for verifier contracts (already 200K–500K gas). Painful for direct execution. Mitigation: Mode B is the primary positioning; Mode A is a secondary outcome of the same lowering work. -
Stack-depth limit (1024) on EVM. Trident programs already compile to stack machines (Triton), but EVM's depth is shallower than Triton's effective depth with RAM. Mitigation: spill to storage or memory; the existing StackManager handles this.
-
Solidity ABI compatibility. Solidity ABI v2 has corner cases (dynamic arrays of dynamic structs, function-type selectors). Mitigation: support the common subset in Phase 4; document unsupported patterns.
-
Audit reachability.
trident auditis decidable on Tier 1. On Tier 0 withos.ethereum.call(external calls escape the sandbox), full reachability is undecidable. Mitigation: audit discharges everything inside the contract; external calls are modeled as adversarial. -
Competing with Fe. Mode A overlaps with Fe's positioning. Fe has Argot, alpha status, and a first-mover head start under Solidity's parent organization. Mitigation: lean on Mode B — verifier-codegen is the dimension Fe structurally cannot match.
-
Verifier-template maintenance. Phase 3 ties an EVM contract template to the zheng proof system. If zheng changes proof shape, the template must be regenerated. Mitigation: emit the template from the proof system's own claim format; do not hand-maintain it.
Decision
Open question for the engineer:
-
Pursue Mode B as the primary deliverable (Phases 1+2+3+4). Trident becomes "the language for both ends of zk on Ethereum." No incumbent EVM language can match this.
-
Or pursue Mode A only (Phases 1+2+4+5). Trident becomes "safer Solidity with multi-target source and content-addressed code." Real but undifferentiated against Fe's trajectory.
Recommendation: Mode B. Mode A falls out of it for free.