TRZK compiles Lean specifications of zero-knowledge primitives to optimized low-level implementations via equality saturation with hardware-aware cost models.
This cut is a deliberately minimal end-to-end pipeline. Future growth happens on a working foundation.
- Expression language:
ArithExpr = Const Int | Var Nat | Add ArithExpr ArithExpr - One rewrite rule:
e + 0 → e(right-identity) - Rust emitter targeting
isizearithmetic - CLI
trzkthat turns a.leanspec file into a Rust function - Integration test with crafted and fuzz vectors
Multiplication, left-identity of +, commutativity, constant folding, finite
fields, ZK primitives. All deferred to future iterations.
Saturation is delegated to optisat / LambdaSat, a formally verified e-graph + saturation engine. We plug in via typeclass instances; we do not reimplement the engine.
# Build
lake build
# Compile a spec to Rust
cat > /tmp/spec.lean <<'EOF'
open TRZK (ArithExpr)
def spec : ArithExpr := .add (.var 0) (.const 0)
EOF
./.lake/build/bin/trzk /tmp/spec.lean --output /tmp/out.rs
cat /tmp/out.rs
# → pub fn arith_spec(x0: isize) -> isize { x0 }
# Run the integration test
./integration_tests/run.sh --op add0
./integration_tests/run.sh --op add0 --fuzz -n 1000Four stages, each with one owner:
- Parse — Lean itself. The user writes
def spec : ArithExpr := ...in a.leanfile; the CLI runs it vialake env lean --run. - Saturate — optisat. Our
ArithOptype plugs in viaNodeOpsandExtractabletypeclass instances. - Emit — hand-rolled Rust emitter (
TRZK/Emit.lean). - Execute — scripted harness (
integration_tests/).
See docs/pipeline.md for details.
| Path | Purpose |
|---|---|
TRZK/ArithExpr.lean |
AST users write specs in |
TRZK/ArithOp.lean |
e-graph node + optisat typeclass instances |
TRZK/Rule.lean |
rewrite rule registry |
TRZK/Pipeline.lean |
embed + optimize |
TRZK/Emit.lean |
Rust emitter |
Compile.lean |
trzk CLI |
Tests/*.lean |
#guard tests |
integration_tests/ |
end-to-end harness |
docs/ |
pipeline, saturation, onboarding, glossary |
See LICENSE.