
Tabula
Zero-knowledge kernel for tabular state transition
Demo
About
The problem it solves # Tabula Thesis Tabula moves the abstraction boundary from ISA-level execution to schema-typed state transitions. Memory consistency scales with state accesses, not total computation. ## 1. The Problem General-purpose zkVMs (SP1, RISC Zero, etc.) prove machine execution: a RISC-V program runs, and the prover generates a STARK that the execution trace is correct. This is general and powerful, but structurally wasteful for stateful applications. **Every state access goes through the full ISA pipeline.** A database read — conceptually, "look up a value by key" — becomes: load address into register, call memory-read syscall, decode result bytes, store to stack. Each step is a RISC-V instruction, each instruction is a row in the execution trace, each row is constrained in the AIR. **Memory consistency covers everything.** The sorted-memory argument that ensures "every read returns the last-written value" must cover *all* memory accesses: stack frames, heap allocations, function arguments, temporaries — not just application state. The proving cost scales with total memory operations, most of which are infrastructure. **Memory is untyped and flat.** The prover sees a byte array. It cannot exploit the fact that a column contains only u64 values, or that a table has 50 rows. Type information is lost at the ISA boundary, and with it, any opportunity for type-aware optimization. **State root computation is application-level.** zkVMs do not manage state commitment — they prove execution. When a rollup needs a state root, the application computes it: hashing leaves, building Merkle paths, updating the tree — all as RISC-V instructions (or precompiles), all proven through the ISA. Updating 100 accounts in a depth-20 Merkle tree requires on the order of 2000 hash invocations, all proven as ISA execution. For a batch of 100 balance transfers, the business logic is trivial: read, compare, subtract, add, write. The proving cost is ISA overhead, memory consistency over stack+heap+state, and ~2000 hashes for the state root. The actual application semantics are a small fraction of the total constraint count. ## 2. The Approach Computation in ZK has two categories with fundamentally different cost structures: - **Stateful** — reads and writes to persistent storage. Expensive because of infrastructure: ISA overhead, memory consistency, state root hashing. - **Stateless** — pure computation: arithmetic, comparisons, hashing. Localized: a fixed number of constraints per operation, no memory consistency overhead. Cost is predictable and scales with op count alone. General-purpose zkVMs do not distinguish between the two. Both go through the same ISA trace, paying the same per-instruction overhead. The ISA abstraction layer artificially equalizes the marginal proving cost of an arithmetic operation and a state access — a balance comparison and a database read both become sequences of RISC-V instructions, each constrained identically in the AIR. Tabula separates them: - **State lives in tables** — typed, column-partitioned, key-addressed. The IR, commitment scheme, and AIR constraints are co-designed around this structure. State root computation is a native protocol concern handled by purpose-built AIR chips, not application code proven through an ISA. - **Computation lives in chips** — each operation type (arithmetic, hashing, comparison) is constrained by its own AIR chip, connected via a LogUp bus protocol. No ISA intermediary. The rest of this document argues why tables are the right structure for state, and how the co-design around them enables optimizations that are impossible in a flat memory model. ## 3. Tables for State Tables — typed, column-partitioned, key-addressed state — are not an arbitrary choice. They emerge from the requirements of efficient ZK proving. ### 3.1 Per-Type Chip Specialization Each column has a known type from the schema. This lets the constraint system specialize per type: a Bool column uses 1-FE-wide AIR chips, a U64 column uses 3-FE-wide chips with limb decomposition, a Bytes32 column uses 8-FE-wide native digest chips. Type information directly reduces trace width, constraint degree, and lookup table size — each width class has its own optimized constraint set with no branching and no dynamic dispatch. An untyped memory model must either use the widest encoding for all values, or pay constraint overhead to dispatch on type at runtime. ### 3.2 Per-Column Commitment Not all state is equal. A 50-row config table and a 10M-row ledger need different commitment strategies: - **Small columns:** Sorted Sparse Map Commitment (SSMC) — a sorted list with streaming Poseidon. O(n) commitment, no tree overhead. - **Large columns:** Sparse Merkle Tree (SMT) — O(log n) per access, amortized over the batch. Columns are declared in the schema, so the prover pre-selects the optimal strategy at compile time. Multiple transactions in a batch that touch the same column shar Use of AI tools and agents ## Use of AI tools and agents I heavily use AI coding agents throughout the project, with **Claude Code** as the primary tool. (Also used Codex when token ran out.) ### How I use agents during development The codebase is organized as a set of **Rust crates** that are cleanly separated by logical responsibility (core logic, interfaces, utilities, etc.). I also designed the **dependency graph** intentionally so that multiple agents can work in parallel with minimal merge conflicts and clear boundaries. * **Parallel implementation (2–3 agents):** I typically run 2–3 coding agents simultaneously to implement new features, perform refactors, and fix bugs across different crates. Because the modules are well-isolated, each agent can work independently while still aligning with a shared architecture. * **Review, documentation, and design (1–3 agents):** In parallel, I run 1–3 additional agents focused on tasks that are not “writing code,” such as: * reviewing the newly written code and suggesting improvements, * writing and updating documentation, * discussing architecture changes and feature direction with us, * exploring new research ideas or alternative designs before implementation. * **Demo and presentation phase (1–2 agents):** In the latter stage of the hackathon, I add 1–2 agents dedicated to shipping a polished demo: * building and iterating on the web UI, * helping with visual/design choices, * drafting the pitch narrative, presentation strategy, slide content, and script. ### How they work together I treat the agents as a **parallel team** operating over a shared plan and crate-level boundaries. The human role is to **orchestrate**: define scope and priorities, keep the architecture consistent, integrate changes, and verify correctness (tests, code review, and end-to-end validation). This workflow lets me focus on high-leverage decisions and verification while the agents maximize throughput across implementation, review, documentation, and presentation—resulting in significantly higher productivity during the hackathon.
How it's made
Challenges we ran into ## Challenges I ran into ### 1) Removing “RAM consistency checking” A big hurdle was: **how do we avoid paying a full RAM-consistency argument for everything** (locals, temporaries, repeated reads, last-write tracking), and instead exploit what is **statically knowable at compile time**? I addressed this by designing the IR around a strict **Normal Form (NF)** and **True SSA**: * NF makes state access patterns canonical and decidable from the public program structure. * SSA makes locals wire-like rather than memory-like. Together, this removes the need for *intra-transaction* RAM consistency and pushes the remaining consistency problem to the **inter-transaction / batch** layer where it’s smaller and more structured. ### 2) SMT-everywhere was too expensive for small state Another hurdle was that **SMT openings/updates are overkill when a column is small** (e.g., config tables, compact registries). Using SMT for everything makes the “small state” case pay a huge fixed overhead. So I introduced **SSMC (Small Sparse Map Commitment)** as an alternative column commitment for small columns, and built a **hybrid commitment model** where each `(table, column)` can use the best strategy for its size/access pattern. This was a meaningful design + implementation lift, because it needed: * membership / non-membership handling * update correctness (so the prover can’t silently change unrelated entries) * clean composition back into a single global state root ### 3) Soundness and crypto engineering were hard Implementing cryptographic components (hashing/commitments/openings) correctly is full of sharp edges: domain separation, canonical encodings (especially null/absence), update proofs, and “no hidden degrees of freedom” in the witness. I got through it with: * lots of iterative testing and refactoring, * and heavy use of AI coding agents for implementation assistance, code review, and catching consistency issues. That said, **the current build is hackathon-grade**: it works end-to-end as a prototype, but **soundness/security is not fully finalized**, and there are known issues to harden after the hackathon (more tests, benchmarks, spec/impl alignment, and likely an audit pass).