Lost in Translation

The Problem

A user gives Jolt a program written in the RISCV assembly language with the IMAC extension. Jolt in turn compiles this program to Jolt Assembly, and executes (and proves correctness for) this program written in the Jolt ISA.

Jolt assembly is essentially a strict subset of RISCV instructions + some extra instructions, referred to as virtual instructions. For example, some RISCV instructions (such as LW) are replaced with a sequence of instructions written in the Jolt ISA (see below). For Jolt to be correct, the program written in Jolt assembly must be "equivalent" to the original user program. Otherwise, we have just executed and proven correctness of execution for some arbitrary program. Equivalence here means that the RISC-CPU state before and after executing these sequence of instructions is identical to the RISC-CPU state before and after the execution of the RISC-V instruction. Below are the code blocks that simulate the RISC and Jolt CPU:

32fn exec(&self, cpu: &mut Cpu, ram_access: &mut <LW as RISCVInstruction>::RAMAccess) {
33    let value = match cpu
34        .mmu
35        .load_word(cpu.x[self.operands.rs1 as usize].wrapping_add(self.operands.imm) as u64)
36    {
37        Ok((word, memory_read)) => {
38            *ram_access = memory_read;
39            word as i32 as i64
40        }
41        Err(_) => panic!("MMU load error"),
42    };
43    cpu.write_register(self.operands.rd as usize, value);
44}

The inline_sequence describes the equivalent Jolt CPU state transitions¹.

 90fn inline_sequence_64(&self, allocator: &VirtualRegisterAllocator) -> Vec<Instruction> {
 91    let v0 = allocator.allocate();
 92    let v1 = allocator.allocate();
 93
 94    let mut asm = InstrAssembler::new(self.address, self.is_compressed, Xlen::Bit64, allocator);
 95
 96    asm.emit_align::<VirtualAssertWordAlignment>(self.operands.rs1, self.operands.imm);
 97    asm.emit_i::<ADDI>(*v0, self.operands.rs1, self.operands.imm as u64);
 98    asm.emit_i::<ANDI>(*v1, *v0, -8i64 as u64);
 99    asm.emit_ld::<LD>(*v1, *v1, 0);
100    asm.emit_i::<SLLI>(*v0, *v0, 3);
101    asm.emit_r::<SRL>(*v1, *v1, *v0);
102    asm.emit_i::<VirtualSignExtendWord>(self.operands.rd, *v1, 0);
103
104    asm.finalize()
105}

Naturally, the RISC-CPU does not have virtual registers, so equivalence between the two blocks of code is measured by equivalence of RISC CPU state, whose fields are a strict subset of the Jolt CPU state.

With equivalence defined, how does one prove that the two states are equivalent? One way would be to enumerate all possible inputs for all instructions, feed them into the two blocks, and check if the states are the same. This works but it's computationally infeasible. Instead, we prove equivalence mathematically, formally in a theorem proving language such as Lean 4.

Here is roughly how we go about such a thing. As a first step we define a RISCV CPU State in Lean³. The details of this code block are not so important. The takeaway here is that - it is possible to model a CPU formally in Lean².

-- This models a general object that stores data
-- The locations are of type α; and the values are of type β
abbrev DataStore α β := α → β

-- In Jolt Memory has
-- α : BitVec 64
-- β : Bitvec 8
abbrev Memory := DataStore (BitVec 64) (BitVec 8)

-- The RISC-V ISA has 32 general purpose registers
-- α : BitVec 64
-- β : Bitvec 8
abbrev RegFile := DataStore (BitVec 5) (BitVec 64)

-- CSR address space is 12-bit in RISC-V (4096 possible CSRs)
abbrev CsrFile := DataStore (BitVec 12) (BitVec 64)


-- This models a data store where the input is a bit vector and the output
-- is a byte of data (more specifically a bit vector of size 8).
abbrev ByteDataStore addr_bits := BitVec addr_bits → BitVec 8

-- Given a location of type α, return what is stored in the store at the location α.
def read {α β : Type} [DecidableEq α] (a : α) (datastore : DataStore α β) : β :=
  datastore a

-- takes a datastore, an address a, and a new value b (to be written at address a)
-- returns a new datastore that returns the same values as the original datastore at
-- all addresses except a, where it returns b
def write {α β : Type} [DecidableEq α] (a : α) (b : β) (datastore : DataStore α β) : DataStore α β :=
  fun x => if x = a then b else (datastore x)

-- The simplified state of a computer
-- Memory
-- Register
-- Program Counter
-- Flags
-- Componentwise equality -> Equality Of State
@[ext]
structure State where
  mem : Memory
  reg : RegFile
  csr : CsrFile := fun _ => 0#64
  pc  : BitVec 64 := 0#64
  error : Bool := false

Then we define how the RISCV instruction would change state⁴.

/-- RISC-V LW semantics -/
def lw (rs1 rd : BitVec 5) (imm : BitVec 12) (s : State) : State :=
  let base := read rs1 s.reg
  let addr := imm.setWidth 64 + base
  if addr &&& 3#64 ≠ 0#64 then { s with error := true }
  else
    let word := read_word addr s
    let new_reg := write rd (word.signExtend 64) s.reg
    { s with reg := new_reg }

The Jolt sequence is also defined in Lean.

/-- Jolt LW semantics -/
def jolt_lw (rs1 rd : BitVec 5) (imm : BitVec 12) (s : State) : State :=
  let base              := read rs1 s.reg
  let v_address         := Riscv.addi base imm
  let (v_address, s)    := Jolt.virtualAssertWordAlignment v_address s
  if s.error then s
  else
    let v_dword_addr    := Riscv.andi v_address (-8#64)
    let v_dword         := read_dword v_dword_addr s
    let v_shift         := Riscv.slli v_address 3
    let v_word          := Riscv.srl v_dword v_shift
    let result          := Jolt.virtualSignExtendWord v_word
    let new_reg         := write rd result s.reg
    { s with reg := new_reg }

Then, finally we prove they are equivalent by writing it as a theorem.

theorem lw_eq (rs1 rd : BitVec 5) (imm : BitVec 12) (s : State)
    (h_no_error : s.error = false) :
    Riscv.lw rs1 rd imm s = jolt_lw rs1 rd imm s := by

We actually have a full Lean proof for the above theorem, but we skip it here as it distracts from the main goal of the post.

What's The Drama?

So we can take Rust code, express it meaningfully in Lean and prove theorems about it. Great! What's the drama? The issue here -- is that the way I came up with the above Lean code is by hand-translating Rust code into Lean. Firstly, this is error prone, but as the code snippets are small and regular one could forgive such a manual procedure. Secondly, and more importantly, tomorrow if someone changes the Jolt ISA spec, how do we keep the code aligned? This manual process will not scale, and will be a nightmare to maintain.

The naive approach is to parse the exec Rust code directly and translate it to Lean. But this is a plan with a very slippery slope. A general Rust-to-Lean translator would need to handle every valid way of expressing the same logic — variable shadowing, closures, method chains, trait dispatch, control flow. This is essentially writing a Rust compiler frontend. We do NOT want to re-write the Rust compiler.

Tools like Hax take a different approach. Hax hooks into rustc as a compiler plugin and extracts Rust's own THIR (Typed High-level Intermediate Representation), then translates it into verification languages like F*, Coq, or Lean (see the Hax architecture docs and the Lean backend). For our purposes this is certainly overkill. Firstly, we want to model in Lean the high-level Rust function description, not a compiler IR lowering of it. Secondly, the interface to these tools is janky. We cannot give it a Rust function and say write this in Lean. It needs a full crate — cargo hax into lean operates on an entire cargo project, not individual functions.

This is not what we really want to do. What we really want is to go through each instructions/*.rs file, extract just the exec (and inline) blocks, and model them in Lean like we did earlier. The exec blocks are simple: read operands, compute, write results.

For example, the same LW code written in a custom grammar might look like this

46#[tracer_macros::gen_exec]
47impl LW {
48    fn ast() -> Stmt {
49        Seq([
50            Load("v", W32, Add(Rs1, Imm)),
51            WriteRd(Cast { from: W32, to: W64, sign: Signed, expr: Var("v") }),
52        ])
53    }
54}

But what should this grammar look like?

A Custom AST

We need a grammar rich enough to express every Jolt instruction. Each instruction reads operands, computes a value, and writes the result — to a register, to memory, or to the program counter. The grammar must capture all of this.

A first attempt — one enum for everything:

enum Node {
    // Terminals — leaves of the tree
    Rs1,
    Imm,
    // Expression — computes a value from children
    Add(Box<Node>, Box<Node>),
    // Statement — writes to CPU state
    WriteRd(Box<Node>),
}

This lets us write WriteRd(Add(Rs1, Imm)). But it also lets us write garbage like WriteRd(WriteRd(Rs1)) or Add(WriteRd(Rs1), Imm).

The problem is that there's no distinction between nodes that change state (writing to a register) and nodes that compute intermediate values (adding two numbers). We'll call the first kind statements and the second kind expressions⁵. The single enum conflates them.

To make this work with one type, we need a runtime check that classifies each variant — something the enum itself doesn't encode:

fn is_statement(node: &Node) -> bool {
    match node {
        Node::WriteRd(_) => true,
        // Every new statement variant must be added here:
        // Node::Store(..) => true,
        // Node::WritePc(_) => true,
        // Node::Branch(..) => true,
        _ => false,
    }
}

This has to be kept in sync with the enum — every time a statement variant is added, is_statement must be updated. Forget one, and garbage trees slip through silently.

Now the translation function uses it to check every child:

fn generate(node: &Node) -> TokenStream {
    match node {
        // Terminals
        Node::Rs1 => quote! { rs1 },
        Node::Imm => quote! { imm },
        // Expression — must guard against statement children
        Node::Add(a, b) => {
            assert!(!is_statement(a), "Add cannot contain a statement");
            assert!(!is_statement(b), "Add cannot contain a statement");
            let a = generate(a);
            let b = generate(b);
            quote! { #a + #b }
        }
        // Statement — must also guard against statement children
        Node::WriteRd(child) => {
            assert!(!is_statement(child), "WriteRd cannot contain a statement");
            let val = generate(child);
            quote! { rd = #val; }
        }
    }
}

Every variant that expects a value has to guard against receiving a statement. This works, but the checks are repetitive and easy to forget.

A simpler solution — split into two types:

enum Expr {
    // Terminals
    Rs1,
    Imm,
    // Expression — children are Expr, not Stmt
    Add(Box<Expr>, Box<Expr>),
}

enum Stmt {
    // Statement — takes an Expr, so no statement can sneak in
    WriteRd(Expr),
}

The garbage trees don't compile — WriteRd takes an Expr, not a Stmt. The translation becomes:

fn generate_expr(expr: &Expr) -> TokenStream {
    match expr {
        // Terminals — no recursion
        Expr::Rs1 => quote! { rs1 },
        Expr::Imm => quote! { imm },
        // Expression — recurse into generate_expr, guaranteed to return a value
        Expr::Add(a, b) => {
            let a = generate_expr(a);
            let b = generate_expr(b);
            quote! { #a + #b }
        }
    }
}

fn generate_stmt(stmt: &Stmt) -> TokenStream {
    match stmt {
        // Statement — generate_expr returns a value, safe to assign
        Stmt::WriteRd(expr) => {
            let val = generate_expr(expr);
            quote! { rd = #val; }
        }
    }
}

No runtime checks. generate_expr always returns a value. generate_stmt always returns an assignment. The compiler enforces it.

The above was a minimal example. Here is the full AST used by Jolt (tracer/src/ast.rs):

20enum AstExpr {
21    // Terminals
22    Rs1, Rs2, Imm, Pc,
23    Reg(u8),
24    Lit(i128),
25    Advice,
26    MostNegative,
27
28    // Arithmetic — children are AstExpr
29    Add(Box<AstExpr>, Box<AstExpr>),
30    Sub(Box<AstExpr>, Box<AstExpr>),
31    Mul(Box<AstExpr>, Box<AstExpr>),
32    MulHigh(Box<AstExpr>, Box<AstExpr>),
33    MulHighSU(Box<AstExpr>, Box<AstExpr>),
34    MulHighU(Box<AstExpr>, Box<AstExpr>),
35    Div(Box<AstExpr>, Box<AstExpr>),
36    DivU(Box<AstExpr>, Box<AstExpr>),
37    Rem(Box<AstExpr>, Box<AstExpr>),
38    RemU(Box<AstExpr>, Box<AstExpr>),
39
40    // Bitwise
41    And(Box<AstExpr>, Box<AstExpr>),
42    Or(Box<AstExpr>, Box<AstExpr>),
43    Xor(Box<AstExpr>, Box<AstExpr>),
44    Not(Box<AstExpr>),
45
46    // Shifts
47    Sll(Box<AstExpr>, Box<AstExpr>),
48    Srl(Box<AstExpr>, Box<AstExpr>),
49    Sra(Box<AstExpr>, Box<AstExpr>),
50
51    // Comparison
52    Eq(Box<AstExpr>, Box<AstExpr>),
53    Ne(Box<AstExpr>, Box<AstExpr>),
54    Lt(Box<AstExpr>, Box<AstExpr>),
55    LtU(Box<AstExpr>, Box<AstExpr>),
56    Ge(Box<AstExpr>, Box<AstExpr>),
57    GeU(Box<AstExpr>, Box<AstExpr>),
58
59    // Type conversion
60    Cast { from: Width, to: Width, sign: SignMode, expr: Box<AstExpr> },
61
62    // Unary
63    TrailingZeros(Box<AstExpr>),
64
65    // Conditional
66    If(Box<AstExpr>, Box<AstExpr>, Box<AstExpr>),
67
68    // Xlen-dependent
69    XlenMatch { bit32: Box<AstExpr>, bit64: Box<AstExpr> },
70
71    // Bindings
72    Let(String, Box<AstExpr>, Box<AstExpr>),
73    Var(String),
74}
75
76enum AstStmt {
77    WriteRd(AstExpr),
78    WriteReg(u8, AstExpr),
79    Store(Width, AstExpr, AstExpr),
80    WritePc(AstExpr),
81    Branch(AstExpr, AstExpr),
82    Assert(AstExpr, AstExpr),
83    Load(String, Width, AstExpr),
84    Seq(Vec<AstStmt>),
85    LetStmt(String, AstExpr),
86    Nop,
87}

What this really defines is a grammar. Each enum variant is a production rule — it says what a valid tree can look like. Written as a grammar:

Expr ::=
    | Rs1 | Rs2 | Imm | Pc | Reg(u8) | Lit(i128) | Advice | MostNegative
    | Add(Expr, Expr) | Sub(Expr, Expr) | Mul(Expr, Expr)
    | MulHigh(Expr, Expr) | MulHighSU(Expr, Expr) | MulHighU(Expr, Expr)
    | Div(Expr, Expr) | DivU(Expr, Expr) | Rem(Expr, Expr) | RemU(Expr, Expr)
    | And(Expr, Expr) | Or(Expr, Expr) | Xor(Expr, Expr) | Not(Expr)
    | Sll(Expr, Expr) | Srl(Expr, Expr) | Sra(Expr, Expr)
    | Eq(Expr, Expr) | Ne(Expr, Expr)
    | Lt(Expr, Expr) | LtU(Expr, Expr) | Ge(Expr, Expr) | GeU(Expr, Expr)
    | Cast(Width, Width, SignMode, Expr)
    | TrailingZeros(Expr)
    | If(Expr, Expr, Expr)
    | XlenMatch(Expr, Expr)
    | Let(String, Expr, Expr) | Var(String)

Stmt ::=
    | WriteRd(Expr) | WriteReg(u8, Expr)
    | Store(Width, Expr, Expr) | WritePc(Expr)
    | Branch(Expr, Expr) | Assert(Expr, Expr)
    | Load(String, Width, Expr)
    | Seq(Stmt*) | LetStmt(String, Expr) | Nop

The two-type split is visible here: Expr only produces Expr children. Stmt takes Expr children for values, and Stmt children only via Seq.

The syn Crate

Now that we have a grammar, how do we parse it? The ast function is valid Rust syntax — Seq([...]) is a function call, Cast { from: W32, ... } is a struct literal, Rs1 is a bare identifier. None of these names exist in Rust's standard library, but syn doesn't care — it parses syntax, not semantics.

syn is a Rust library that parses Rust source code into a typed tree. A proc macro receives raw tokens; syn turns them into structured types we can pattern-match on.

Consider this Rust function:

impl Calculator {
    fn compute(&self) -> i32 {
        let base = max(self.x, 10);
        Point { x: base, y: -1 }
    }
}

syn parses this into a tree. Here is what each piece becomes:

syn::ItemImpl                          ← impl Calculator { ... }
└── method: compute
    └── syn::Block                     ← { ... }
        ├── syn::Stmt::Local           ← let base = max(self.x, 10);
        │   └── syn::Expr::Call        ← max(self.x, 10)
        │       ├── .func: Expr::Path  ← max
        │       └── .args:
        │           ├── Expr::Field    ← self.x
        │           └── Expr::Lit      ← 10
        └── syn::Stmt::Expr           ← Point { x: base, y: -1 }  (no semicolon = return value)
            └── syn::Expr::Struct      ← Point { x: base, y: -1 }
                ├── .path              ← Point
                └── .fields:
                    ├── x: Expr::Path  ← base
                    └── y: Expr::Unary ← -1

Official docs:

• syn::Stmt: here,
• syn::Expr: here.

Our LW ast function produces exactly the same kinds of nodes:

syn::ItemImpl                                         ← impl LW { ... }
└── method: ast
    └── syn::Block                                    ← { ... }
        └── syn::Stmt::Expr(_, None)                  ← the return expression
            └── syn::Expr::Call                        ← Seq([...])
                ├── .func: Expr::Path                  ← "Seq"
                └── .args[0]:
                    syn::Expr::Array                   ← [Load(...), WriteRd(...)]
                    ├── [0]: Expr::Call                 ← Load("v", W32, Add(Rs1, Imm))
                    │   ├── .func: Expr::Path           ← "Load"
                    │   └── .args:
                    │       ├── [0]: Expr::Lit           ← "v"
                    │       ├── [1]: Expr::Path          ← "W32"
                    │       └── [2]: Expr::Call          ← Add(Rs1, Imm)
                    │           ├── .func: Expr::Path    ← "Add"
                    │           └── .args:
                    │               ├── [0]: Expr::Path  ← "Rs1"
                    │               └── [1]: Expr::Path  ← "Imm"
                    └── [1]: Expr::Call                 ← WriteRd(Cast { ... })
                        ├── .func: Expr::Path           ← "WriteRd"
                        └── .args[0]:
                            Expr::Struct                ← Cast { from: W32, ... }
                            ├── .path                    ← "Cast"
                            └── .fields:
                                ├── from: Expr::Path     ← "W32"
                                ├── to:   Expr::Path     ← "W64"
                                ├── sign: Expr::Path     ← "Signed"
                                └── expr: Expr::Call     ← Var("v")
                                    ├── .func: Expr::Path ← "Var"
                                    └── .args[0]: Expr::Lit ← "v"

Compare with the Calculator example. The structure is the same:

• Seq(...) and WriteRd(...) are function calls, just like max(...)
• Cast { from: W32, ... } is a struct literal, just like Point { x: 1 }
• Rs1 is a bare identifier, just like base
• [Load(...), WriteRd(...)] is an array literal

syn doesn't assign any meaning to these names. It just builds a tree of syn::Expr nodes. Our proc macro walks this tree, recognises the grammar's production rules by name, and emits code.

Auto-generating Rust from the AST

So what do we gain by defining instruction semantics as an AST? The original motivation was Lean — compile the AST into Lean definitions for formal verification. But we get much more than that. We write the semantics once in the grammar, and backends compile it to anything — Rust for the CPU emulator, documentation, or whatever else we need tomorrow. One definition, many outputs.

To see this in action, let's compare the original hand-written exec for LW with the auto-generated ast_exec. Before comparing them, there is one difference that needs explaining.

Look at cpu.mmu.load_word(...) in the hand-written exec. It returns two things: the loaded value (word) and a record of the memory access (memory_read). The loaded value is the instruction's result — it gets sign-extended and written to rd. The memory access record is bookkeeping for Jolt's proof system — it captures what was read and from where, so the prover can later verify the memory access.

The hand-written exec stores this record with *ram_access = memory_read. The ram_access parameter is passed in specifically for this — it's a mutable reference that the caller uses to collect proof data.

In the AST, the author writes Load("v", W32, Add(Rs1, Imm)) — pure semantics, no bookkeeping. The code generator must emit the recording automatically. But there is a problem: the proc macro operates on tokens, not types.

Each instruction declares its RAM type in declare_riscv_instr!:

declare_riscv_instr!(
    name = LW,
    ...
    ram  = RAMRead      // ← LW's RAMAccess type is RAMRead
);

declare_riscv_instr!(
    name = ADD,
    ...
    ram  = ()           // ← ADD does not access memory
);

This sets the associated type <LW as RISCVInstruction>::RAMAccess = RAMRead. But syn parses syntax, not types. When generate_ast_stmt sees Load(...), it does not know whether this instruction's RAMAccess is RAMRead, RAMWrite, or (). So it cannot emit *ram_access = memory_read — that only compiles if ram_access is a RAMRead. It cannot emit nothing — that silently drops the recording. It cannot branch on the type — it doesn't know the type.

We introduced a trait to solve this (tracer/src/instruction/mod.rs:348):

348pub trait RecordRead {
349    fn record_read(&mut self, read: RAMRead);
350}

With an impl for each possible RAM type:

352impl RecordRead for RAMRead {
353    fn record_read(&mut self, read: RAMRead) {
354        *self = read;
355        // self is ram_access, read is memory_read
356        // this does exactly: *ram_access = memory_read
357    }
358}
359impl RecordRead for RAMWrite {
360    fn record_read(&mut self, _: RAMRead) {}  // write-only: nothing to record
361}
362impl RecordRead for () {
363    fn record_read(&mut self, _: RAMRead) {}  // no RAM: nothing to record
364}

Now the code generator emits the same call for every Load:

let (v, _ram_read) = cpu.mmu.load_word(addr).expect("MMU load error");
RecordRead::record_read(_ram_access, _ram_read);

_ram_read is the memory access record returned by load_word — the same value as memory_read in the hand-written exec. For LW, _ram_access has type RAMRead, so the first impl fires: *self = read stores the record. For an instruction with ram = (), the third impl fires: it does nothing. The Rust compiler resolves the correct impl at compile time. The proc macro never needs to know the type — it emits one line, and trait dispatch handles the rest.

Compare the original exec with the auto-generated ast_exec:

fn exec(&self, cpu: &mut Cpu,
    ram_access: &mut <LW as
        RISCVInstruction>::RAMAccess)
{
    let value = match cpu.mmu.load_word(
        cpu.x[self.operands.rs1 as usize]
            .wrapping_add(self.operands.imm)
            as u64)
    {
        Ok((word, memory_read)) => {
            *ram_access = memory_read;
            word as i32 as i64
        }
        Err(_) => panic!("MMU load error"),
    };
    cpu.write_register(
        self.operands.rd as usize, value);
}

fn ast_exec(&self, cpu: &mut Cpu,
    _ram_access: &mut <LW as
        RISCVInstruction>::RAMAccess)
{
    let (v, _ram_read) = cpu.mmu.load_word(
        cpu.x[self.operands.rs1 as usize]
            .wrapping_add(self.operands.imm)
            as u64)
        .expect("MMU load error");
    crate::instruction::RecordRead
        ::record_read(
            _ram_access, _ram_read);
    let v = v as i64;
    let _rd_val = (v as i32 as i64);
    cpu.write_register(
        self.operands.rd as usize, _rd_val);
}

Decoding: Rust backend

Above we saw the auto-generated Rust code side by side with the hand-written version. But how do we actually get from the grammar to that Rust code?

The #[tracer_macros::gen_exec] attribute triggers the proc macro. It receives the entire impl LW { ... } block as a token stream, parses it with syn into a syn::ItemImpl, finds the method named ast, and passes its body — a syn::Block — to generate_exec_body (tracer-macros/src/rust_backend.rs:14).

generate_exec_body (tracer-macros/src/rust_backend.rs:14) is where parsing begins. It receives the syn::Block and iterates over its Vec<syn::Stmt>:

14pub fn generate_exec_body(block: &syn::Block) -> Result<TokenStream2, syn::Error> {
15    let stmts = &block.stmts;
16    if stmts.is_empty() {
17        return Err(syn::Error::new_spanned(block, "ast() body is empty"));
18    }
19
20    let mut parts = Vec::new();
21    for stmt in stmts {
22        match stmt {
23            // let addr = Add(Rs1, Imm);  →  process RHS as an expression
24            syn::Stmt::Local(local) => {
25                let name = &local.pat;
26                let init = local.init.as_ref()
27                    .ok_or_else(|| syn::Error::new_spanned(local,
28                        "let binding must have an initializer"))?;
29                let val = generate_ast_expr(&init.expr)?;
30                parts.push(quote! { let #name = #val; });
31            }
32            // Expression with semicolon  →  process as a statement
33            syn::Stmt::Expr(expr, Some(_semi)) => {
34                parts.push(generate_ast_stmt(expr)?);
35            }
36            // Expression without semicolon (return)  →  process as a statement
37            syn::Stmt::Expr(expr, None) => {
38                parts.push(generate_ast_stmt(expr)?);
39            }
40            _ => return Err(syn::Error::new_spanned(stmt,
41                "unsupported statement in ast() body")),
42        }
43    }
44
45    Ok(quote! { #(#parts)* })
46}

Three cases:

Case 1: syn::Stmt::Local — a let binding.

fn ast() -> Stmt {
    let addr = Add(Rs1, Imm);   // ← syn::Stmt::Local
    WriteRd(addr)
}

syn::Stmt::Local has two parts we care about: local.pat (the pattern — here, the identifier addr) and local.init (the initializer — here, Add(Rs1, Imm)). The code extracts both:

syn::Stmt::Local(local) => {
    let name = &local.pat;                    // LHS, e.g. `addr`
    let init = local.init.as_ref()            // RHS, e.g. `Add(Rs1, Imm)`
        .ok_or_else(|| syn::Error::new_spanned(local,
            "let binding must have an initializer"))?;
    let val = generate_ast_expr(&init.expr)?; // process RHS as an expression
    parts.push(quote! { let #name = #val; }); // re-emit as a Rust let binding
}

The right-hand side init.expr goes to generate_ast_expr — it computes a value. The result is re-emitted as a Rust let binding with the same name. A let without an initializer (e.g. let addr;) is an error.

Case 2: syn::Stmt::Expr(expr, Some(_)) — an expression followed by a semicolon.

Processed by generate_ast_stmt (it modifies state).

fn ast() -> Stmt {
    Seq([
        Store(W32, Rs1, Rs2);   // ← syn::Stmt::Expr(_, Some(;))
        WriteRd(Rs1)
    ])
}

Case 3: syn::Stmt::Expr(expr, None) — the final expression with no semicolon (the return value).

Also processed by generate_ast_stmt.

fn ast() -> Stmt {
    WriteRd(Add(Rs1, Imm))      // ← syn::Stmt::Expr(_, None)
}

_ => Err(syn::Error::new_spanned(call, format!("unknown Expr variant: {}", func_name))),

generate_ast_expr (tracer-macros/src/rust_backend.rs:183)

This function receives a syn::Expr and returns a TokenStream2 that computes a value. It never modifies CPU state.

The full function is at tracer-macros/src/rust_backend.rs:183-350.

The outer match is on the syn::Expr variant:

• Expr::Path(p) — a bare identifier. These are the terminals.
• Expr::Call(call) — a function call. These are the compound expressions.
• Expr::Struct(s) — a struct literal. Cast and XlenMatch use this form.
• Expr::Unary(u) — prefix operator like -1. For example, -8 in And(Rs1, -8) is parsed as syn::Expr::Unary and emitted as (-8 as i64).
• Expr::Lit(lit) — a literal like 42. For example, 3 in Sll(Rs1, 3) is parsed as syn::Expr::Lit and emitted as (3 as i64).
• Anything else — error.

Terminals (Expr::Path)

The last case is how let bindings work. If the user writes let addr = Add(Rs1, Imm); WriteRd(addr), then addr in WriteRd(addr) hits the catch-all and is emitted as the Rust identifier addr — which refers to the let binding emitted earlier by generate_exec_body.

Compound expressions (Expr::Call)

All binary operations go through a helper binary_op (tracer-macros/src/rust_backend.rs:401) which calls generate_ast_expr on both arguments and combines them with the given operator.

Struct expressions (Expr::Struct)

Two variants use struct literal syntax:

Cast { from, to, sign, expr } — type conversion. Handled by generate_ast_cast (tracer-macros/src/rust_backend.rs:353). Reads four named fields: from (source width), to (target width), sign (Signed or Unsigned), expr (the inner expression). The (from, to, sign) triple selects the Rust cast chain.

AST:

Cast { from: W32, to: W64, sign: Signed, expr: Var("v") }

Generated Rust:

(v as i32 as i64)

Sign-extend from 32-bit to 64-bit: cast to i32 (interpret as signed 32-bit), then widen to i64.

AST:

Cast { from: W64, to: W32, sign: Unsigned, expr: Rs2 }

Generated Rust:

((cpu.x[self.operands.rs2 as usize] as u32) as i64)

Truncate to 32-bit: cast to u32 (drop upper bits), then back to i64.

XlenMatch { bit32, bit64 } — runtime dispatch on the CPU's word size.

AST:

XlenMatch {
    bit32: Cast { from: W32, to: W32, sign: Unsigned, expr: Rs1 },
    bit64: Rs1,
}

Generated Rust:

match cpu.xlen {
    crate::emulator::cpu::Xlen::Bit32 => ((cpu.x[self.operands.rs1 as usize] as u32) as i64),
    crate::emulator::cpu::Xlen::Bit64 => cpu.x[self.operands.rs1 as usize],
}

Each branch is processed by generate_ast_expr independently.

generate_ast_stmt (tracer-macros/src/rust_backend.rs:44)

This function receives a syn::Expr and matches on the function name to determine which AstStmt variant it is. Every variant's arguments that represent values are processed by generate_ast_expr. The output is always a TokenStream2 that modifies CPU state.

The outer match is on the syn::Expr variant:

• Expr::Call(call) — the common case. Extract the function name from call.func, then match on it.
• Expr::Path(p) — a bare identifier. Only Nop is valid here.
• Anything else — error: "expected a Stmt variant".

The full function is at tracer-macros/src/rust_backend.rs:44-179.

The Expr::Call match table:

More Examples

We already saw LW above. Here are a few more instructions to show how the AST scales to different patterns — stores, atomics, and mixed read-write operations.

SW (Store Word)

A store is the reverse of a load: compute an address, write a value to memory. The AST is a single line.

fn ast() -> Stmt {
    Store(W32, Add(Rs1, Imm), Rs2)
}

fn exec(&self, cpu: &mut Cpu,
    ram_access: &mut <SW as
        RISCVInstruction>::RAMAccess)
{
    *ram_access = cpu.mmu.store_word(
        cpu.x[self.operands.rs1 as usize]
            .wrapping_add(self.operands.imm)
            as u64,
        cpu.x[self.operands.rs2 as usize]
            as u32,
    ).ok().unwrap();
}

fn ast_exec(&self,
    cpu: &mut crate::emulator::cpu::Cpu,
    _ram_access: &mut <SW as
        crate::instruction::RISCVInstruction>::RAMAccess)
{
    crate::instruction::RecordWrite
        ::record_write(
            _ram_access,
            cpu.mmu.store_word(
                cpu.x[self.operands.rs1 as usize]
                    .wrapping_add(self.operands.imm)
                    as u64,
                cpu.x[self.operands.rs2 as usize]
                    as u32,
            ).ok().unwrap(),
        );
}

AMOADDW (Atomic Add Word)

An atomic read-modify-write: load a word, add rs2 to it, store the result back, and write the original value to rd. This exercises most of the grammar — Load, LetStmt, Store, Cast, and WriteRd all in one Seq.

fn ast() -> Stmt {
    Seq([
        Load("raw", W32, Rs1),
        LetStmt("orig", Cast { from: W32, to: W64, sign: Signed, expr: Var("raw") }),
        Store(W32, Rs1, Cast { from: W64, to: W32, sign: Unsigned, expr:
            Add(Var("orig"), Cast { from: W64, to: W32, sign: Signed, expr: Rs2 })
        }),
        WriteRd(Var("orig")),
    ])
}

fn exec(&self, cpu: &mut Cpu,
    _: &mut <AMOADDW as
        RISCVInstruction>::RAMAccess)
{
    let address =
        cpu.x[self.operands.rs1 as usize]
            as u64;
    let add_value =
        cpu.x[self.operands.rs2 as usize]
            as i32;
    let load_result =
        cpu.mmu.load_word(address);
    let original_value = match load_result {
        Ok((word, _)) => word as i32 as i64,
        Err(_) => panic!("MMU load error"),
    };
    let new_value = (original_value as i32)
        .wrapping_add(add_value) as u32;
    cpu.mmu.store_word(address, new_value)
        .expect("MMU store error");
    cpu.write_register(
        self.operands.rd as usize,
        original_value);
}

fn ast_exec(&self,
    cpu: &mut crate::emulator::cpu::Cpu,
    _ram_access: &mut <AMOADDW as
        crate::instruction::RISCVInstruction>::RAMAccess)
{
    let (raw, _ram_read) = cpu.mmu
        .load_word(
            cpu.x[self.operands.rs1 as usize]
                as u64)
        .expect("MMU load error");
    crate::instruction::RecordRead
        ::record_read(
            _ram_access, _ram_read);
    let raw = raw as i64;
    let orig = (raw as i32 as i64);
    crate::instruction::RecordWrite
        ::record_write(
            _ram_access,
            cpu.mmu.store_word(
            cpu.x[self.operands.rs1 as usize]
                as u64,
            ((orig.wrapping_add(
                (cpu.x[self.operands.rs2 as usize]
                    as i32 as i64))
                as u32) as i64) as u32,
        ).ok().unwrap(),
    );
    let _rd_val = orig;
    cpu.write_register(
        self.operands.rd as usize, _rd_val);
}

What About Lean Code Generation?

The same AST can also be compiled to Lean. The Lean backend (tracer-macros/src/lean_backend.rs) walks the same syn tree and emits Lean 4 definitions instead of Rust code.

Here is the hand-written Lean for LW (from earlier in the post) alongside the auto-generated version:

def lw (rs1 rd : BitVec 5)
    (imm : BitVec 12)
    (s : State) : State :=
  let base := read rs1 s.reg
  let addr := imm.setWidth 64 + base
  if addr &&& 3#64 ≠ 0#64 then
    { s with error := true }
  else
    let word := read_word addr s
    let new_reg :=
      write rd (word.signExtend 64) s.reg
    { s with reg := new_reg }

def lw (rs1 rs2 rd : BitVec 5)
    (imm : BitVec 12)
    (s : State) : State :=
  if (read rs1 s.reg + imm.signExtend 64)
      &&& 3#64 ≠ 0#64 then
    { s with error := true }
  else
  let v :=
    read_word
      (read rs1 s.reg + imm.signExtend 64) s
  let new_reg :=
    write rd
      (((v).truncate 32).signExtend 64) s.reg
  { s with reg := new_reg }