I built a Lisp VM in Rust that proves its own execution trace (STARKs + Winterfell)

#computerscience #performance #web3 #rust

Over the last few weeks I've been building an 8-register VM in Rust for a small Lisp-like DSL, plus a proof pipeline that turns programs into STARK proofs of execution.

The DSL is compiled by the zk-lisp-compiler crate into a compact Op sequence, and proofs are generated through a dedicated backend built on top of the winterfell crate.

A few details that might be interesting from a Rust/efficiency point of view:

Trace Layout & Generation

I defined a unified execution trace (VM registers, RAM tables, Merkle gadget, Poseidon2 lanes, ROM accumulator) in a single Columns layout. The VmTraceBuilder simulates the Op sequence, seeds registers, and fills a Winterfell TraceTable while keeping allocations predictable (pre-zeroed trace, cached Poseidon2 params, partition selection).

Multi-segment Execution

The backend implements a SegmentPlanner that cuts the padded trace into level-aligned segments under a max_segment_rows budget. The interesting part was remapping the unified Columns into per-segment traces and computing state hashes at boundaries for chaining—without fighting the borrow checker too much.

STARK-in-STARK Recursion

Recursion is expressed via generic traits (RecursionBackend, RecursionStepProver). The pipeline proves each execution segment, then runs an aggregation STARK over the resulting step proofs. This required some heavy generic bounds and type plumbing to keep the frontend (zk-lisp-proof::frontend) fully backend-agnostic.

Example

To prove the VM actually handles state transitions, here is a batch processor I wrote in zk-lisp. It calculates the new state root and total fees for a batch of transactions:

;; Simple rollup-style benchmark for zk-lisp:
;; - N_ACCOUNTS balances in RAM
;; - N_TXS transfers (from, to, amt, fee)
;; - compute new balances and hash the state

(def N_ACCOUNTS       8)
(def N_TXS            16)
(def HASH_BALANCES_IV 12345)

;; RAM layout:
;; [0 .. N_ACCOUNTS-1] = balances
;; [N_ACCOUNTS .. N_ACCOUNTS+4*N_TXS-1] =
;;     tx data (from, to, amt, fee) per tx

(def (init_state)
  ;; Initialize account balances [0 .. N_ACCOUNTS-1].
  (loop :max N_ACCOUNTS ((i 0))
    (begin
      (store i 0))
    (recur (+ i 1)))

  ;; Initialize tx table [tx_base .. tx_base + 4*N_TXS-1].
  (loop :max N_TXS ((i 0))
    (let ((base (+ (tx_base) (* i 4))))
      (begin
        (store base       0)   ;; from
        (store (+ base 1) 1)   ;; to
        (store (+ base 2) 1)   ;; amount
        (store (+ base 3) 0))) ;; fee
    (recur (+ i 1))))

(def (tx_base)
  N_ACCOUNTS)

(def (tx_from i)
  (load (+ (tx_base) (* i 4))))

(def (tx_to i)
  (load (+ (tx_base) (+ 1 (* i 4)))))

(def (tx_amount i)
  (load (+ (tx_base) (+ 2 (* i 4)))))

(def (tx_fee i)
  (load (+ (tx_base) (+ 3 (* i 4)))))

;; Safe arithmetic helpers (wrapping into field but
;; using safe-add/safe-sub to enforce non-negative balances).

(def (apply_tx i)
  (let ((from (tx_from i))
        (to   (tx_to i)))
    (begin
      ;; Debit sender: from_bal - (amt + fee)
      (store from
        (safe-sub (load from)
                  (safe-add (tx_amount i) (tx_fee i))))
      ;; Credit receiver: to_bal + amt
      (store to
        (safe-add (load to) (tx_amount i)))
      ;; Return fee
      (tx_fee i))))

;; Loop over all N_TXS, accumulate total fee
(def (apply_batch)
  (loop :max N_TXS ((i 0) (fee_sum 0))
    fee_sum
    (recur (+ i 1) (safe-add fee_sum (apply_tx i)))))

;; Simple Poseidon2-based hash chain over balances
(def (hash_balances)
  (loop :max N_ACCOUNTS ((i 0) (h HASH_BALANCES_IV))
    h
    (recur (+ i 1) (hash2 h (load i)))))

(typed-fn main ((let u64) (let u64)) -> u64)
(def (main expected_fee_sum expected_root)
  (begin
    (init_state)
    (let ((fee_sum (apply_batch))
          (root    (hash_balances)))
      (begin
        (assert (= fee_sum expected_fee_sum))
        (assert (= root expected_root))
        root))))

This program compiles down to the VM opcodes, and Winterfell generates a proof attesting that "I know a list of valid transactions that result in this state root" without revealing the transactions themselves.

It's still a prototype (AGPL-3.0), but I'd really appreciate feedback on: