RISC-V Opcodes Under the Prover: Semantics, Arithmetization, and Proving-System Interactions

Every zkVM in production today asks to be judged as a processor: it names an ISA, promises architectural compliance, and invites developers to compile ordinary programs against it. That framing invites a particular reviewer — the person who has actually built pipelines, written ISA compliance suites, or argued about a bit in an encoding — and most writing about zkVMs is not addressed to them. This piece is. The claim we defend over the next several thousand words is that a zkVM is best understood as a machine implementation under a radically inverted cost model: the ISA semantics are unchanged to the bit, but nearly every intuition about what is cheap and what is expensive — carry chains, barrel shifters, comparators, dividers, register ports — is either neutralized or reversed. The instruction set survives; the microarchitectural folklore does not.

1 · The object being proven: a three-piece machine and its transition relation

Strip the machine to what the architecture actually specifies. A RISC-V hart, for the purposes of the unprivileged integer ISA, is three pieces of state:

        hart state
   +-------------------------------------------+          memory (one byte-addressed array)
   |  x0..x31 : 32 registers, XLEN bits each   |        +--------------------------+
   |    x0  = 0   (hardwired: writes discard,  |        | addr 0x0000: 0x00        |
   |               reads return zero)          |  load  | ...                      |
   |    x1..x31 = general purpose              | <----- | addr 0x2008: 0xCD        |
   |                                           | store  | addr 0x2009: 0xAB        |
   |  pc : XLEN bits, address of the next      | -----> | ...                      |
   |       instruction to execute              |        | addr 0x8000_0000: text   |
   +-------------------------------------------+        +--------------------------+

Everything else — pipelines, caches, register renaming, branch predictors — is implementation. The architecture is the transition relation: given a state s = (regs, pc, mem), fetch the instruction at mem[pc], decode it, and produce the unique successor state s' = δ(s). Execution is the orbit of δ. This is the standard operational-semantics view of an ISA, and it is worth stating because a zkVM takes it literally in a way silicon never has to: the zkVM's statement is precisely "here is a commitment to a trace s₀, s₁, …, s_T, and for every step, s_{i+1} = δ(s_i)," with the initial state bound to a committed program and its inputs and the final state bound to the claimed outputs. A hardware implementation must produce the orbit; a prover must certify it after the fact, to a verifier who will not re-execute.

A scoping note for the formally minded: δ-as-function is a deliberate simplification — adequate for this article, too strong for the machine as deployed. The moment the guest consumes a host-supplied word (an advice tape, the ECALL doorways of §4.10, Airbender's oracle CSR), the step is no longer a function of machine state alone. A more complete formalism replaces the function with a relation R(s_i, e_i, s_i+1), where e_i ranges over the environment's contribution at step i — nondeterministic input, host behavior crossed into by an environment call — and the proof statement then quantifies over an e that is committed, constrained, or deliberately left free. Everything below survives that refinement; we keep δ for the families where the environment stays silent.

That single sentence decomposes into the five obligations every zkVM discharges, whatever its proof system:

Two architectural points that recur throughout, stated here once. First, x0 is not a register with a zero in it; it is the absence of a register — a destination that discards and a source that manufactures zero. Silicon implements this with a read-port bypass; provers, as we will see, implement it with a constraint or by aliasing address 0 of a register-memory to a cell whose writes are discarded. Second, the base ISA has exactly one addressing mode — base register plus sign-extended 12-bit displacement, used by every load and store (the A extension's atomics are sparer still: register-direct through rs1, with no displacement at all) — and no instruction computes on memory directly. An address is an ordinary number that happens to sit in a register. This load-store discipline, a deliberate RISC inheritance, turns out to be a substantial gift to the prover: memory interaction is quarantined into two instruction families, so the expensive machinery (the consistency argument) attaches to a small, syntactically obvious subset of the trace.

One more preliminary, because it governs everything in §4: the width of the machine. RV32 gives XLEN=32, RV64 gives XLEN=64. All register arithmetic is modular — ADD is addition mod 2^XLEN, full stop. There are no flags: no carry, no overflow, no condition-code register anywhere in the integer architecture. Software that wants a carry reconstructs it from comparisons (sltu after an add), and the absence of flag state is one of the tidiest things about proving this ISA — a step's effect is entirely "one register changed, pc changed," never "and three sticky bits elsewhere also changed."

2 · Instruction anatomy: six formats and where the bits live

All standard RV32I/RV64I instructions are 32 bits, with the lowest two bits 11; the compressed extension occupies the other three values of those two bits with 16-bit encodings (§4.11). Six formats cover the base ISA, distinguished only by how they use the constant field:

 31          25 24    20 19    15 14  12 11          7 6      0
+--------------+--------+--------+------+-------------+--------+
|   funct7     |  rs2   |  rs1   |funct3|     rd      | opcode |  R : register-register ALU
+--------------+--------+--------+------+-------------+--------+
|      imm[11:0]        |  rs1   |funct3|     rd      | opcode |  I : ALU-immediate, loads, JALR
+--------------+--------+--------+------+-------------+--------+
|  imm[11:5]   |  rs2   |  rs1   |funct3|  imm[4:0]   | opcode |  S : stores
+--------------+--------+--------+------+-------------+--------+
|imm[12|10:5]  |  rs2   |  rs1   |funct3|imm[4:1|11]  | opcode |  B : branches (offset ×2)
+--------------+--------+--------+------+-------------+--------+
|                imm[31:12]             |     rd      | opcode |  U : LUI, AUIPC
+--------------+--------+--------+------+-------------+--------+
|        imm[20|10:1|11|19:12]          |     rd      | opcode |  J : JAL (offset ×2)
+--------------+--------+--------+------+-------------+--------+

Three regularities matter more than the formats themselves. The source registers rs1/rs2 and destination rd never move: whichever format an instruction uses, the same five-bit fields are in the same place, which is why a hardware decoder can start its register-file read before it knows what the instruction is. The immediate is always sign-extended (the sole exceptions in the whole unprivileged integer ISA: the shift amount — five bits on RV32, six on RV64 — and the five-bit CSR immediate, both unsigned by nature), and the sign bit is always instruction bit 31, so sign extension needs no decoding at all. And the B and J formats scatter their immediate bits into an order no human would choose precisely to preserve those two invariants — the scrambling is free in wires and saves a mux on the critical path.

For a prover, this hardware-shaped regularity is pleasant but the deeper observation is different: a zkVM can often refuse to pay for decode at execution time at all. The program is static and committed before proving; every distinct instruction can be decoded once, in preprocessing, into whatever internal tuple the proof system prefers — opcode kind, operand indices, expanded immediate, control flags — and the fetch obligation of §1 then reads from this predecoded table. The per-cycle question "what do these 32 bits mean" becomes the one-time question "is this table an honest decoding of the committed program," which can even be delegated to the verifier's preprocessing or a one-off argument. Chip-per-opcode designs make the same move differently, dispatching each fetched instruction to the circuit for its kind and letting a bus argument glue the pieces. Either way, one of silicon's per-cycle taxes — decode — largely vanishes from the marginal cost of a proven cycle. We will see in §4 which taxes replace it.

A reading note for the code fragments that follow: assembly syntax puts the destination first — add x5, x6, x7 is x5 ← x6 + x7; a trailing i marks an immediate variant; u marks unsigned interpretation; a trailing w on RV64 marks a 32-bit "word" operation. In sll x5, x6, x7 all three operands are registers; nothing in it is an address.

3 · The cost-model inversion

An ISA is a contract, and every contract is negotiated against an implementation technology. RISC-V's integer ISA was shaped by what CMOS charges for: it has no divide-step instruction because iterative dividers are microarchitecture, no flags because renaming flag state complicates wide issue, one addressing mode because address-generation adders are on the critical path. When the implementation technology becomes "polynomial commitments and a constraint system over a prime field," the price list is rewritten wholesale. The contract's text does not change; its economics do.

The inversion has a single root cause worth naming precisely. A circuit verifies; it does not compute. Silicon must produce the result of an operation from its inputs, so the cost of an instruction is the cost of the producing structure — the carry-lookahead tree, the barrel shifter, the iterative divider. A constraint system only needs the result to appear, from anywhere (the prover simply writes it into the witness), and then be checked. Where checking is cheaper than producing, the prover pockets the difference; this is nondeterminism as an engineering resource, and it is not available to hardware at any price. Division is the canonical beneficiary — §4.9 — but the resource is spent on nearly every family. The converse also bites: some things silicon gets for free by physically being made of bits (bitwise logic, truncation, wiring a bus in a permuted order) have no native meaning over a prime field, where the atoms are field elements, and must be bought back with decomposition and range proofs.

The recurring price list, before we meet the families that pay it:

Two systemic effects sit on top of the per-operation prices. First, the field is a second word size. Every zkVM carries two widths: the architectural XLEN and the field's capacity. When the field is large (Jolt's ~254-bit scalar field), a 64-bit word is a single field element and double-width products are native, but every bit-level claim needs decomposition arguments sized for 64 bits. When the field is small (the 31-bit fields of OpenVM and Airbender — Baby Bear and Mersenne31, respectively), a 32-bit word does not even fit one field element, so words live as limbs permanently — two 16-bit or four 8-bit pieces — and every operation is defined over limbs with explicit carries; in exchange, field arithmetic itself is fast and range checks are small. Neither regime dominates; they relocate the same costs. Second, uniformity has a price and so does its absence. A single universal row that can be any opcode (Jolt's stance) pays for generality with lookups into large structured tables; a dedicated circuit per opcode (Ceno's stance) pays nothing for generality but must glue heterogeneous chips into one trace with bus/permutation arguments and prove a chip even when it ran twice. This tension — one machine that does everything versus a federation of specialists — is the closest thing zkVM design has to the CISC/RISC argument, and §5 returns to it with the four concrete answers.

With the price list in hand, the families. For each: the architected behavior with its edge cases exactly as the manual fixes them, then the arithmetization obligations those semantics create, then what the four VMs at our pinned commits actually do.

4 · Family by family: semantics, then constraints

A note on vocabulary for readers arriving from the hardware side. A constraint is a polynomial equation over the field that every row of the committed trace must satisfy — the prover's analog of an assertion that is physically impossible to violate. A witness is a value the prover writes into the trace at its own discretion, trusted only insofar as constraints pin it down; "advice" is a witness with no defining equation, only checks. A lookup argument proves that each of millions of trace values appears in some table — where the table can be small and materialized (a 2¹⁶ byte-pair table) or astronomically large and never materialized, defined only by the low-degree polynomial that describes its entries (Jolt's 2¹²⁸-entry instruction tables, evaluated via sumcheck rather than stored). A range check is the workhorse lookup: "this value fits in N bits." With that, the families.

4.1 · Addition and subtraction: buying back the wrap

Architected behavior. ADD rd,rs1,rs2 / ADDI rd,rs1,imm / SUB rd,rs1,rs2 compute mod 2^XLEN; overflow is silently discarded, no exception exists, and there is no SUBI (add a negative immediate). On RV64 the *W variants compute on the low 32 bits and sign-extend the 32-bit result — the RV64 convention that all 32-bit values, even unsigned ones, live sign-extended in 64-bit registers ^[1].

The obligation. Field addition is exact — 2⁶⁴−1 plus 1 is 2⁶⁴ in the field, not 0 — so the entire proving content of ADD is the truncation. Every zkVM proves ADD as "add somewhere it cannot wrap, then prove the claimed result is the low XLEN bits," and the differences are only in where the carry lives:

• Jolt adds the two 64-bit operands natively in its ~254-bit field inside R1CS, then looks the 65-bit sum up in a RangeCheck table whose entries are "identity on the low 64 bits" — truncation as a lookup ^[9]. SUB is the same machinery with a two's-complement bias: the lookup operand is formed as left − right + 2⁶⁴, and the same table drops the borrow ^[9].
• OpenVM, whose 31-bit Baby Bear field cannot hold even one 32-bit word, keeps words as four 8-bit limbs and witnesses a boolean carry per limb: carry_i = (b_i + c_i + carry_i−1 − a_i)/2⁸, constrained to {0,1}, with result limbs byte-range-checked through the bitwise lookup bus ^[42].
• Ceno does the same over two 16-bit limbs, and proves SUB by re-arranging the addition — constrain rs1 = rd + rs2, so the subtraction circuit is the addition circuit with the roles rotated and only rd freshly range-checked ^[25].
• Airbender shares one AddSubRelation across both opcodes: two degree-2 constraints over 16-bit limbs with a boolean middle carry and carry-out ^[55]. Its relation slots are pooled: because at most one instruction family executes per row, the same physical add-sub relation is reused by whichever family is live, selected by mutually exclusive execution flags ^[55].

The hardware translation: the carry chain's timing problem is gone, but its truth must now be purchased, either as one lookup against a truncation table (large field) or as N boolean-carry witnesses plus N range checks (small field). Note what this makes of ADDI: identical datapath, and the immediate costs nothing at all, because it is a constant of the committed program — decoded once, materialized in the fetched instruction tuple, never witnessed per cycle (§2).

4.2 · Bitwise logic: the field's blind spot

Architected behavior. AND/OR/XOR and immediate forms, bit-parallel, no edge cases beyond the immediate being sign-extended (so andi rd,rs,-1 is identity and xori rd,rs,-1 is bitwise NOT) ^[1].

The obligation. This is the purest case of the inversion: the operation silicon performs with one gate per bit has no algebraic expression over a prime field of any size. All four VMs answer with lookups, differing in granularity:

• Jolt gives each of AND/OR/XOR (and ANDN) a dedicated virtual table over the bit-interleaved pair of 64-bit operands — 2¹²⁸ conceptual entries, never materialized, evaluated through the structure of the table's multilinear extension ^[8][10].
• Ceno splits words into four bytes and constrains each output byte against materialized 2¹⁶-row And/Or/Xor tables keyed by the input byte pair ^[26].
• OpenVM ships only a XOR table and derives the rest by identity: for OR it checks that x⊕y equals 2a−b−c, for AND that it equals b+c−2a (both consequences of a = op(b,c) bytewise); the same table's second multiplicity column doubles as the byte range check for arithmetic outputs — one preprocessed 2⁸×2⁸ table serving three opcodes and the range-check bus ^[42].
• Airbender makes one byte-table query per operand byte and indexes the table family directly by the instruction's funct3 — its AND/OR/XOR table ids are literally 7, 6, 4, the RISC-V funct3 encodings, so decode and dispatch collapse into the lookup key ^[56]. The byte tables also make separate range checks unnecessary: a value that answers a byte-table query is a byte ^[56].

Cost intuition for the hardware reader: bitwise ops are no longer free, but they are not the disaster naive bit-decomposition (XLEN boolean constraints per operand per op) suggests — the lookup amortizes them to a handful of bus interactions per instruction. The residual asymmetry is real, though, and it is why every zkVM pushes hash functions — thousands of XOR/rotate steps — out of the ISA into precompiles, delegation circuits, or constraint-native inlines rather than proving them opcode by opcode.

4.3 · Shifts: the barrel shifter has no algebra

Architected behavior. SLL/SRL/SRA shift by the low 5 bits (RV32) or low 6 bits (RV64) of rs2 — upper bits ignored, so there is no "shift by ≥ width" undefined behavior at the ISA level, ever. Immediate forms carry the amount in a shamt field, with reserved code points policing the width: on RV32, SLLI/SRLI/SRAI with inst[25]=1 is reserved encoding space, and on RV64 the *W immediate shifts with imm[5]≠0 are reserved ^[1]. SRL zero-fills; SRA replicates the sign bit; the W variants shift within the low 32 bits (amount from rs2[4:0] only) and sign-extend the word result.

The obligation. A data-dependent shift is a permutation of bits selected by a runtime value — a barrel shifter is a log-depth mux tree, and mux trees are exactly what constraint systems do badly. Three distinct strategies appear across our four VMs, which is the widest divergence of any family:

• Materialize 2^shamt and multiply (Jolt). SLL expands at trace time into VirtualPow2 — a lookup whose table is 2^{(index mod XLEN)}, the mod performing the architectural masking — followed by an ordinary MUL ^[11]. Right shifts go through a bitmask table (((1<<(XLEN−s))−1)<<s) and dedicated VirtualSRL/VirtualSRA lookups, SRA's table adding a sign-extension term gated by the operand's top bit — arithmetic shift as table structure, not as a mux ^[11]. Immediate shifts collapse further: SLLI becomes a single multiply-by-constant row, the constant 1<<(imm&63) baked in at expansion ^[11]. The word shifts are small puzzles in 64-bit space — SRLW first multiplies by 2³² to move the word into the high half, ORs 32 into the shift amount, then reuses the 64-bit right-shift path and sign-extends ^[11].
• One-hot select over limbs (OpenVM, and Ceno's default circuit, which its comments attribute to OpenVM's design). Boolean marker vectors — one over the bit-shift within a limb, one over the limb displacement — each constrained to sum to 1; a bit_multiplier witness is forced to equal 2^bit_shift under the marked position; limb equations then relate input and output limbs with per-limb carry witnesses, sign-filling the vacated limbs with sign·0xFF(FF) for SRA ^[43][27]. The architectural masking becomes a range check that (c₀ − limb_shift·L − bit_shift) is divisible by 32 — i.e. only c mod 32 matters ^[43].
• Precomputed shift table (Airbender). A 2²²-entry table keyed by (16-bit limb, 5-bit amount, direction) returns each limb's two partial contributions, recombined by direction muxes; left shift is modeled as right shift with adjusted amount; SRA adds one more lookup — a sign-filler table returning the high-ones mask for the (sign, amount) pair ^[57]. The masking is a literal AND-table query of the amount against 0b11111 ^[57].

Two observations a VM designer should not miss. First, all three strategies get the ISA's masking rule for free from structure — a table indexed mod XLEN, a divisibility range check, an AND lookup — rather than by trusting the toolchain never to emit an oversized amount; this matters because the claim being proven is about arbitrary register values, not about well-behaved compilers. Second, the immediate forms are dramatically cheaper than the register forms in Jolt's strategy (one row versus a two-row expansion), and identically priced in the limb strategies — a cost asymmetry with no silicon analog, where the barrel shifter neither knows nor cares where the amount came from.

4.4 · Comparisons: signedness is an interpretation

Architected behavior. SLT/SLTU/SLTI/SLTIU write 1 or 0. The bit patterns are compared under two interpretations — and the ISA's one genuinely counterintuitive corner here is SLTIU: its immediate is sign-extended to XLEN first, then compared unsigned, which is why sltiu rd,rs1,1 (compare against 1) is the canonical seqz and an immediate of −1 compares against 2^XLEN−1 ^[1].

The obligation. "a < b" over field elements is meaningless — a prime field has no order compatible with its arithmetic — so comparison must be reduced to range facts about a difference, or to a table. The four answers:

• Jolt: one lookup per comparison into SignedLessThan / UnsignedLessThan virtual tables; the 0/1 output is written to rd. Signedness is a property of the table's defining polynomial, not of any circuit branch ^[12].
• OpenVM and Ceno (shared design): find the most significant differing limb with a one-hot marker vector, prove the marker is correctly placed by prefix constraints, then range-check (diff_val − 1) to force the difference nonzero and correctly signed. Signed comparison re-reads the top limb through a witnessed "MSB field value" allowed to lie in [−2^L−1, 2^L−1) instead of [0, 2^L) — the two's-complement bias applied at the witness level, one datapath for both signednesses ^[44][28].
• Airbender: comparison is a by-product of subtraction — the shared sub relation's borrow bit is unsigned-less-than; an is-zero relation on the difference gives equality; and a 128-entry resolution table keyed by (funct3, borrow, eq, sign₁, sign₂) decides both "should branch" and "should store," folding the entire SLT-and-branch family's control logic into one lookup ^[58].

The bias trick deserves one sentence of respect from the hardware audience: it is exactly the observation that signed comparison is unsigned comparison with the top bit flipped, executed here not as an XOR gate on two wires but as a relaxation of a range constraint on a witness. Same identity, different substrate.

4.5 · Branches: both futures are constrained

Architected behavior. Six conditional branches (BEQ/BNE/BLT/BGE/BLTU/BGEU), B-format, no destination register, 13-bit signed byte offset with an implicit zero low bit, target = branch's own PC + offset. The precise trap semantics matter to compliance reviewers: an instruction-address-misaligned exception is raised only if the branch is taken and the target violates IALIGN, is reported on the branch rather than the target, and cannot occur at all when the C extension (IALIGN=16) is present ^[1].

The study note this article grew from carries a worked trace that is worth keeping — a three-iteration loop, printed as the machine steps:

// x5 = running sum, x6 = counter, x7 = limit (=3)
// loop:  add x5,x5,x6 ; addi x6,x6,1 ; bge x7,x6,loop
step  PC       instr              after
 1    0x20     add  x5,x5,x6      x5=1  x6=1
 2    0x24     addi x6,x6,1       x6=2
 3    0x28     bge  x7,x6,0x20    3>=2 -> PC=0x20 (taken)
 4    0x20     add  x5,x5,x6      x5=3  x6=2
 5    0x24     addi x6,x6,1       x6=3
 6    0x28     bge  x7,x6,0x20    3>=3 -> PC=0x20 (taken)
 7    0x20     add  x5,x5,x6      x5=6  x6=3
 8    0x24     addi x6,x6,1       x6=4
 9    0x28     bge  x7,x6,0x20    3>=4 -> PC=0x2C (fall through)   // x5 = 6

Nine rows of a witness. The prover does not predict step 9's outcome; it already happened. What must be proven is that the recorded outcome is the only one the ISA permits — which is two constraints, not one: that the condition bit is the correct function of the operands (§4.4's machinery), and that next-PC took the branch iff the bit says so. Every VM constrains both arms:

• OpenVM writes it in one line: to_pc = from_pc + cond·imm + (1−cond)·4 ^[44]. Ceno's is algebraically identical (next_pc = pc + taken·imm − taken·4 + 4), with the immediate coming out of the committed program record rather than a witness ^[28].
• Jolt computes the condition as a lookup output, multiplies it by the Branch flag into a ShouldBranch product wire, and lets R1CS rows force NextUnexpandedPC to PC+imm under ShouldBranch and to the sequential successor otherwise ^[9][12]. Equality itself is the textbook multilinear product ∏(x_iy_i+(1−x_i)(1−y_i)) — notably not the inverse-witness trick — because in a lookup-central design equality is just one more table ^[12].
• Ceno and OpenVM prove BEQ/BNE with the multiplicative-inverse marker: cmp_eq + Σ(a_i−b_i)·inv_i = 1 with cmp_eq·(a_i−b_i) = 0 per limb — the classic "a nonzero difference has an inverse, zero does not" certificate ^[28][44]. Airbender resolves the whole family through its conditional table (§4.4) and then enforces alignment negatively: the target's bit 1 is extracted by lookup, and taken·bit1 = 0 is a constraint — a taken misaligned branch is not a trap but an unsatisfiable proof ^[58], a compliance divergence §5 returns to.

The economics, once more against silicon: no predictor, no flush, no fetch bubble — a taken branch costs identically to a fall-through, and a data-dependent unpredictable branch costs identically to a perfectly biased one. The entire branch-handling apparatus of a modern front end exists to hide a latency that the proving model does not have. What the proving model has instead is the obligation to constrain the road not taken: the (1−cond) arm, which hardware simply never executes, must appear in the constraint system so that the prover cannot claim a fall-through where the ISA demands a jump.

4.6 · Jumps: the link, the low bit, and the compressed adjustment

Architected behavior. JAL rd,off: rd ← PC+4, PC ← PC + sext(21-bit offset). JALR rd,rs1,imm: target = (rs1 + sext(imm)) with bit 0 cleared, rd ← PC+4, PC ← target; the byte-granular immediate (unlike B/J offsets, not premultiplied by 2) and the bit-clearing are both deliberate, the latter making function-pointer targets robust to odd addresses ^[1]. Because the target is computed from the old rs1, jalr rd,rs1 with rd = rs1 is well-defined. The link value is the address of the next sequential instruction — PC+4, or PC+2 when the jump was a compressed encoding, the one place where the C extension's existence leaks into the semantics of another family ^[4].

The obligation and the four answers. Three claims per jump: the target arithmetic (an add, §4.1's machinery), the bit-0 clearing (JALR only), and the link write.

• Jolt makes the target a lookup output — JAL through the plain truncation table on PC+imm, JALR through a RangeCheckAligned table whose entries are (index & mask) & ~1, so the bit-clearing is a property of the table rather than a constraint ^[13]. The link is an R1CS row: rd = PC + 4 − 2·IsCompressed under the Jump flag — the compressed adjustment carried as a per-row decode flag ^[13][21].
• Ceno witnesses rs1+imm limb-wise, holds the target in an address gadget that separately witnesses its low bits as booleans, and forms next_pc by subtracting the witnessed bit 0 — alignment and bit-clearing expressed as controlled decomposition ^[29]. JAL is cheaper by construction: the committed program stores the J-immediate as (next_pc − pc), so the fetch record itself pins the target and the circuit adds nothing ^[29]. Both link writes decompose PC+4 into range-checked pieces bounded to the 30-bit PC space ^[29].
• OpenVM computes rs1+imm as two 16-bit limbs plus an explicitly witnessed boolean least-significant bit that is then dropped: to_pc = 2·limb₀ + 2¹⁶·limb₁, with limbs range-checked to 15 and PC_BITS−16 bits — its comment cites the spec's bit-clearing sentence directly ^[45]. The JAL/LUI shared chip range-caps the link's top limb via a XOR-table trick to keep it inside the 30-bit PC space ^[45].
• Airbender merges JAL and JALR into one family, muxing src1 between PC and rs1, then passes the target's low word through a cleanup lookup returning (bit 1, word & ~3): bit 0 is forced off — the JALR clear — and bit 1 set under execution makes the circuit unsatisfiable, which is also how it enforces 4-byte targets with no C extension ^[59].

Note the compliance shading on the link value: Jolt proves PC+4−2·IsCompressed because it accepts RVC; Ceno, OpenVM and Airbender prove PC+4 unconditionally because they reject RVC at build time (§4.11) — each is exactly correct for the ISA profile it actually claims.

4.7 · LUI and AUIPC: constants and position

Architected behavior. A 12-bit immediate cannot carry a large constant, so the U-format pair sets the upper bits: LUI rd,imm is imm<<12 (low 12 bits zero; on RV64 the 32-bit value is sign-extended), and AUIPC rd,imm is this instruction's own PC + sext(imm<<12) — the primitive from which all PC-relative addressing, and therefore all position-independent code, is built ^[1].

Under the prover, these are the cheapest instructions in the ISA, and instructive for that reason. Jolt proves LUI as a lookup of the immediate itself and AUIPC as the PC+imm truncation lookup ^[9]. Airbender writes the decoder-assembled immediate straight to rd with no arithmetic at all, and its AUIPC add needs no alignment check since a U-immediate cannot disturb the low bits ^[60]. Ceno's default build gives each a small dedicated circuit (with the program table storing the immediate in a limb-friendly pre-shifted form) ^[30] — but its Goldilocks build does something more interesting: it transpiles them away, LUI into an internal ADDI from x0 with the full shifted constant (its internal immediate field is not limited to 12 bits), and AUIPC into an ADDI whose immediate has the link-time PC already folded in — legal precisely because a static program's PC-relative constants are static ^[30]. OpenVM pre-shifts the U-immediate at transpile time and shares one chip between LUI and JAL ^[45].

The lesson generalizes: an instruction whose result is a static function of the instruction word and its address is not really a runtime instruction to a zkVM — it is a constant the committed program carries, and the VM's only job is to route it. Hardware cannot make this move because hardware does not get to preprocess the program it will run.

4.8 · Loads and stores: where the machine touches the world

Architected behavior. The only addressing mode: EA = rs1 + sext(imm12). Loads sign-extend (LB/LH/LW) or zero-extend (LBU/LHU, and RV64's LWU) into rd; stores truncate rs2 to the access width. RV64 adds LD/SD. The fine print a compliance reviewer will probe: a load to x0 must still raise its exceptions and perform its side effects even though the value is discarded; naturally aligned accesses never raise address-misaligned and are guaranteed atomic; misaligned accesses are EEI-defined — they may complete (possibly slowly, via invisible trap), raise address-misaligned, or raise access-fault ^[1]. Memory is byte-addressed; endianness is EEI-chosen with little-endian the standard convention.

The obligation splits in two. The consistency half — every read returns the latest write — is global machinery (§5), priced per access. The per-instruction half is address arithmetic, alignment, and sub-word extraction, and here the four VMs diverge on a genuine design axis: what is the unit the memory argument sees?

• Jolt: the doubleword. Its RAM argument (Twist) addresses 8-byte-aligned doublewords only; LD/SD are the only memory instructions that survive into proven bytecode. Every narrower access is expanded at trace time into an aligned-doubleword sequence: LB becomes align-the-address (ANDI −8), LD the containing doubleword, XOR/shift the selected byte into the top, then SRAI 56 or SRLI 56 — sign extension performed by the arithmetic-shift lookup, with the byte-lane selection done by XORing the low address bits ^[15]. Sub-word stores become masked read-modify-writes: LD, build the lane mask, merge rs2 by XOR/AND/XOR, SD the whole doubleword back ^[15]. Halfword and word forms additionally assert alignment through dedicated lookup tables (1 iff addr mod 2/4 = 0) ^[15]. The R1CS glue is five rows: address = rs1+imm when a memory flag is set, load ⇒ read = write = rd, store ⇒ rs2 = written value ^[9].
• OpenVM: the aligned 4-byte block, with the shift as an opcode. One adapter always accesses the aligned word containing the EA, and the core chip treats each (operation, byte-offset) pair as a distinct internal opcode — LoadBu0 through LoadBu3, StoreH0/2, and so on — muxing limbs between read data and prior contents ^[48]. Alignment is a divisibility range check on (EA − shift)/4; sign-extending loads are routed to a separate chip that extracts the top bit by range-checking (top_limb − bit·128) to 7 bits and fills upper limbs with bit·0xFF ^[48]. Misaligned access is simply outside the execution environment's contract — guest-invalid, host-fatal ^[48].
• Ceno: the word, one circuit per width. Five load circuits and three store circuits; EA witnessed limb-wise with boolean carries; an address gadget witnesses the low bits as booleans and range-checks the middle, enforcing per-width alignment (align4 for LW, align2 for LH/LHU, none for bytes) with the actual memory read always at the aligned word ^[33]. Byte extraction muxes on the witnessed address bits; SB/SH stores decompose the previous word into range-checked bytes and splice ^[33]. Misalignment is a trap in the emulator, which simply never produces a provable trace for it ^[33].
• Airbender: the word, with ROM carved out of the address space. EA = rs1+imm through the shared add relation; the low two bits come from a lookup, and alignment is enforced negatively — (bit0+bit1)·exec_word = 0 makes a misaligned word access unsatisfiable ^[60]. A high-bits lookup classifies the address as ROM or RAM: ROM loads are served by the committed-program table (with the cycle's RAM query then pinned to a harmless x0 access), stores into ROM are unsatisfiable, and one lookup keyed (halfword, bit0, funct3) performs all four sub-word extensions at once ^[60]. Sub-word stores are read-modify-write splices on the cycle's single load/store slot ^[60].

The unifying observation: no VM proves a misaligned access, and none needs the EEI's permissive language — each picks the strictest reading (align or be unprovable/trapped) because supporting misalignment would poison the sub-word extraction machinery for a case compilers essentially never emit. This is an EEI choice the spec explicitly authorizes, but a reviewer should know it is being made, and that it is load-bearing: an attacker-supplied address is checked by constraints, not by trust in the compiler. And the x0 fine print — exceptions still fire on a discarded load — is quietly honored in OpenVM's needs_write mechanism, which suppresses only the register write, never the access itself ^[40].

4.9 · Multiply and divide: nondeterminism's showcase

Architected behavior (M extension). MUL returns the low XLEN bits of the 2·XLEN-bit product — identical under either signedness, which is why one instruction suffices. The high half needs its own instruction per signedness combination: MULH (s×s), MULHU (u×u), MULHSU (s×u, roles fixed). Division truncates toward zero, and the M extension is deliberately trap-free — the spec's own rationale — with fully defined degenerate results: divide by zero gives quotient all-ones (−1 signed, 2^XLEN−1 unsigned) and remainder = dividend; the unique signed overflow (−2^XLEN−1 ÷ −1) gives quotient = dividend, remainder = 0 ^[2]. RV64 adds W variants, all sign-extending their 32-bit results — including DIVUW/REMUW, which sign-extend an unsigned 32-bit result, the corner most likely to catch an emulator author ^[2].

Multiplication is where field size speaks loudest. Jolt multiplies two 64-bit operands natively in its 254-bit field — the 128-bit product is one field multiplication — then extracts low or high half by lookup (truncation table for MUL, an upper-word table for MULHU), and expands MULH/MULHSU into the standard sign-correction identity (sign masks via a lookup, two corrective MULs, a MULHU, two ADDs) rather than proving them directly ^[17]. The small-field VMs run schoolbook limb convolution with carry chains: OpenVM checks each (limb, carry) pair against a two-dimensional range table sized [2⁸, 8·2⁸] ^[46], Ceno's carries are range-checked to 18 bits over 16-bit limbs ^[31], and both witness the MULH sign correction as ext/sign fields entering the upper convolution ^[46][31]. Airbender's single MulDivRelation — op1·op2 + additive = lo + 2³²·hi with per-operand sign fields, enforced as four 16-bit-chunk constraints with byte-plus-bit carry witnesses — serves the whole family ^[61].

Division is the family where every VM plays the same card, because it is the best card in the deck: the proving relation verifies division without representing a divider inside the arithmetic circuit. The prover's witness generator still performs the division the ordinary way — quotient and remainder are computed, once, outside the constraint system — and then enters them as advice for the circuit to check against the division contract. Stated fully — and this is the checklist a soundness reviewer should carry, because each clause has been a real bug class somewhere in this industry's history:

How each VM discharges the checklist: Jolt takes q and r as VirtualAdvice rows (range-checked to 64 bits by their own lookup ^[18]), then runs an assert-sequence: a ValidDiv0 table forces q = 2⁶⁴−1 whenever d = 0 (clause 4); a ChangeDivisor table substitutes d→1 exactly on the overflow input pair so the same recomposition covers clause 5; MULH/MUL of q against the adjusted divisor with an asserted sign-extension high half discharges clause 3; recomposition + AssertEQ gives clause 1; and absolute values via SRAI/XOR/SUB feed a ValidUnsignedRemainder table — entry true iff r < d or d = 0 — for clause 2 ^[18]. The DIVU sequence is the same skeleton with an explicit no-overflow table and an unsigned q·d ≤ dividend assert ^[18]. OpenVM folds all five clauses into one core chip: carry-checked convolution for clause 1/3, an r′ = |r| negation path and one-hot unsigned comparison against d for clause 2, a zero_divisor flag whose constraints force every q limb to 255 (clause 4), and an r_zero flag that absorbs the overflow input as "the r = 0 special case," with execution returning q = dividend there (clause 5) ^[47]. Ceno's circuit is the same architecture over 16-bit limbs (its comments credit the OpenVM core), with inverse witnesses proving divisor ≠ 0 on the main path and both special-case flags mutually exclusive ^[32]. Airbender reuses its MulDivRelation as the recomposition, pins q's limbs to 0xffff under a divisor-is-zero flag, enforces r < d through the sub relation's borrow with (1−div0)·(1−borrow)·exec = 0, and — a detail we found nowhere else — ships a Z3 script in-tree that machine-checks its signed-remainder sign logic ^[61]. Its shipped prover configuration, note, simply drops signed division: the NoSignedMulDiv machine variant decodes MULH/MULHSU/DIV/REM as invalid, and the toolchain must not emit them ^[64].

Step back and appreciate what happened to the cost model. In silicon, DIV is the slowest integer instruction ever shipped — tens of cycles of iterative subtract-shift, or acres of SRT lookup logic. Under a prover it is two advice values and a handful of checks, cheaper than the shifts. The saving is precisely the witness-generation-versus-constraint-verification distinction: the division still happens — once, in the prover's unconstrained witness generator, at ordinary software cost — and what disappears is any need to represent the dividing inside the constraint system, which only re-checks the result. Constraint count is the scarce resource; native computation is not. The flip side is that the entire soundness burden concentrates into the checklist above — silicon's divider can be slow but cannot be argued with, whereas a missing clause 2 is not a performance bug but a forgery vector.

4.10 · ECALL, EBREAK, FENCE, CSRs: the system boundary

Architected behavior. ECALL and EBREAK raise precise exceptions — environment call and breakpoint — and the base ISA assigns them no register side effects; everything else (cause codes, xepc pointing at the instruction itself, parameter passing in a0–a7) belongs to the privileged architecture and the EEI ^[1]. FENCE orders memory/IO accesses between predecessor and successor sets encoded in pred/succ fields (with fm=1000, pred=succ=RW as FENCE.TSO, and reserved configurations required to execute as normal fm=0000 fences honoring the encoded pred/succ sets); on one hart with one memory, it orders nothing ^[1]. The Zicsr instructions atomically read-modify-write one of 4096 CSRs, with precisely specified read/write suppression: CSRRW with rd=x0 skips the read (and its side effects); CSRRS/C with rs1=x0 skip the write entirely — the asymmetry that makes csrr and csrs safe idioms ^[5].

Under the prover, this family is where ISA compliance genuinely forks, because a zkVM has no privileged software stack to trap into — the "environment" is the host, outside the proof. Four different answers, from most to least architectural:

• Jolt models the trap. ECALL expands into a genuine M-mode entry sequence: materialize the faulting PC into a shadow mepc, write cause 11 and mtval 0, compose mstatus (MPP=M, interrupts off), and jump through the shadow mtvec — all against CSR shadow copies living in virtual registers; MRET returns through mepc symmetrically ^[19]. CSRRW/CSRRS expand to register moves against those shadows, with read-before-write order preserved and unmapped CSRs rejected at expansion ^[19]. FENCE survives to final bytecode as a decoded instruction with no lookup and no flags — proven, as a no-op ^[19]. EBREAK becomes JAL +0, a self-jump the tracer reads as termination ^[19].
• Ceno keeps exactly one door. ECALL is the only surviving SYSTEM instruction — dispatched per syscall number (read from x5, SP1-compatible codes) to dedicated circuits: halt (exit code to public values, next_pc forced to the exit sentinel), I/O commit, and the precompile fleet (Keccak, SHA extend, secp256k1/r1, BN254, uint256) ^[36]. EBREAK, every CSR instruction, FENCE, MRET and WFI all transpile to an unimplemented kind whose execution traps — no CSR file exists at all ^[22].
• OpenVM replaces the door. ECALL, EBREAK and all CSR encodings transpile to unimp — a TERMINATE with panic exit code 2 — except the one CSR idiom its comment calls out (CSRRW x0,x0: a counter reset with no CSR file behind it) which becomes a NOP; termination and hints instead use custom instructions on the custom-0 major opcode — encoding space the spec designates for exactly this use, and FENCE transpiles to NOP ^[49]. The system boundary is thus not RISC-V at all — it is OpenVM's own ISA, entered from RISC-V by transpilation.
• Airbender inverts the CSR's meaning. ECALL/EBREAK have no decoder match — SYSTEM funct3=000 simply does not decode, so their appearance makes the trace unprovable ^[62]. What remains of Zicsr is CSRRW alone, aimed at a whitelist table over the 4096-CSR space: CSR 0x7c0 is the non-determinism oracle (reads return unconstrained host words, range-checked only), and designated CSRs above it are the precompile interface — a CSRRW to 0x7c7 emits a delegation request that a Blake2 circuit must answer through a set-equality argument ^[62]. FENCE's opcode arm is commented out in the simulator ("nothing to do in fence, our memory is linear") making it illegal ^[64]; the ROM is padded with 0xc0001073 — csrrw x0, cycle, x0 — which is unprovable precisely because cycle is not on the whitelist: the padding word is a semantic booby trap ^[53].

For the hardware reviewer, the honest summary is: the unprivileged compute core is proven bit-exactly everywhere; the privileged and environment layer is nowhere proven as the spec writes it — it is modeled (Jolt), narrowed to one syscall (Ceno), transpiled away (OpenVM), or repurposed as a bus to co-processors (Airbender). All four choices are defensible under the EEI escape hatch the spec itself provides; none of them is what a compliance suite for silicon would accept without a profile document saying so. §7 returns to why this is the correct engineering outcome and not a corner cut.

4.11 · Atomics and compressed encodings: extensions as lowering problems

A extension. Architecturally: LR registers a reservation; SC writes only if the reservation survived, returning 0 on success or a nonzero failure code (canonically 1), and always invalidates the reservation; nine AMOs atomically load-op-store returning the old value; all require natural alignment (misalignment is an exception — unconditionally for LR/SC, and for AMOs absent the optional misaligned-atomicity-granule PMA); aq/rl bits order; a constrained 16-instruction LR/SC loop carries an eventual-success guarantee ^[3]. On a single-hart machine with no interrupts, every one of these guarantees is satisfied by doing nothing special — atomicity against nobody is free. Jolt is the only VM of the four that accepts the A extension, and its treatment is the correct minimal one: AMOs expand to plain LD, op, SD sequences (its comment noting that sequential traces make the read-modify-write order the whole of atomicity), with min/max computed branch-free via a comparison-then-blend ^[20]. LR/SC is subtler and Jolt actually models the reservation: LR records the address into a dedicated virtual register (asserting it points into RAM); SC takes its success bit as Boolean advice, constrained so that success ⇒ address matches the reservation, stores old + success·(rs2−old), and returns the architectural 0/1 ^[20]. Note the fine grain: the ISA permits spurious SC failure, so "success is advice, constrained only when claimed" is not a shortcut — it is exactly the specification. Ceno, OpenVM and Airbender reject the extension outright (build-time transpile error or undecodable), pushing the problem into the toolchain — the lower-atomic story our companion article documents at length.

C extension. Architecturally: ~30 sixteen-bit encodings, each expanding to exactly one base instruction, with register fields restricted (3-bit specifiers address x8–x15), immediates zero-extended and scaled for loads/stores, a lattice of reserved and HINT code points, and the mapping's only non-identities at its linking jumps — C.JALR, and RV32's C.JAL, link PC+2 where their 32-bit expansions would link PC+4 ^[4]. For a prover, RVC is a fetch-and-decode problem, not an execute problem: Jolt statically expands every 16-bit encoding to its 32-bit form before decode, and carries a single per-row IsCompressed flag whose only constraint effects are the −2 in the link value and the +2 in the sequential-PC update ^[21] — the entire extension reduced to one bit of decode metadata. The other three reject RVC at build time (OpenVM's transpiler consumes the text segment as strict 32-bit words ^[37]; Ceno walks the ELF four bytes at a time ^[22]; Airbender fetches from a 4-aligned ROM and hard-wires PC+4 ^[64]), which is why their jump circuits may verify only bit 1 of targets: in a world without 2-byte instructions, bit 1 is the whole alignment question. The C extension is also why a VM that does accept it must never raise the misaligned-target exception (IALIGN=16 makes it architecturally impossible) — a spec interaction Jolt's expanded-PC bookkeeping absorbs silently.

5 · System-level interactions: where the opcodes meet the argument

5.1 · Registers are memory; ports are free; consistency is the tax

All four VMs make the same move, from four directions: the register file is not a separate structure but a small address range inside the same memory-consistency argument as RAM. Jolt runs a Twist instance over 128 register cells — 32 architectural plus 96 virtual scratch registers its expansions and inlines use (reservation slots, CSR shadows, temporaries) ^[16]. Ceno tags register accesses as a RAM type with per-access timestamps, four sub-cycle ticks per instruction (rs1, rs2, rd, and an optional memory slot), plus a 33rd phantom register that absorbs writes from rd-less instructions ^[34]. OpenVM gives registers address space 1 — 32 registers × 4 byte-limbs at pointers [0,128) — inside its offline-checking bus ^[39][41]. Airbender's only persistent machine state between cycles is the PC; the 32 GPRs live in the shuffle-RAM argument, three fixed-timestamp queries per cycle (rs1, rs2-or-load, rd-or-store) ^[63].

The consequences invert several decades of register-file lore. Read ports are free — a fourth register read would cost one more multiset tuple, not quadratic area. Register pressure still matters (spills are memory traffic and memory traffic is tuples) but renaming, banking, and port scheduling simply have no referent. The one hardware intuition that transfers intact is x0: every VM must actively enforce its zero-ness, and the mechanisms are a nice cross-section of each design's character — OpenVM refuses at transpile time to ever write it (rd=x0 side-effect-free instructions become NOPs; JAL/loads carry a needs_write flag) ^[40], Airbender masks the writeback value to zero through an is-zero gadget on the rd index ^[63], and Jolt/Ceno pin cell 0 / route rd-less writes to a sink cell in the memory argument itself ^[16][34].

Timestamps are the other quiet load-bearing element. Ceno enforces prev_ts < ts per access with a limb-decomposed less-than gadget under a 29-bit budget ^[34]; OpenVM does the same with timestamps in [1, 2²⁹] ^[41]; Airbender packs two 19-bit limbs with the low two bits encoding the three per-cycle accesses, budgeting 2³⁶ cycles ^[63]. These bounds are real ISA-visible capacity limits — a trace longer than the timestamp budget is not slow, it is unprovable in one segment — and they are why every production VM shards long executions into continuation segments glued by carrying the machine state (or a commitment to it) across segment boundaries as public values ^[36].

5.2 · Fetch and decode: the program as a table

§2 promised decode could amortize to zero; here is the mechanism in each VM. Jolt commits the fully expanded bytecode — virtual sequences included — as a lookup table; each cycle's fetch is a lookup, with a dual PC bookkeeping (the ELF address for architectural semantics, the expanded index for sequencing) and constraints forcing virtual sequences to execute from their first row without interleaving ^[14][9]. Ceno commits a decoded program table — (pc, kind, rd, rs1, rs2, imm, imm_sign) — as fixed columns with a witnessed multiplicity per row; each instruction circuit's fetch is one lookup of its full decoded tuple, which is why its immediates can live in circuit-friendly encodings (pre-shifted U-immediates, pow2-encoded shift amounts in one build) chosen per opcode at preprocessing ^[35]. OpenVM commits the transpiled program as a cached trace and fetches over a program bus keyed (pc, opcode, seven operands), with an execution bus chaining (pc, timestamp) between chips and a connector AIR pinning initial and final PC to public values ^[50]. Airbender is the outlier that decodes per cycle — but even its in-circuit decoder is mostly preprocessing in disguise: one 2¹⁷-entry fixed table keyed opcode‖funct3‖funct7 returns a bitmask of format and family flags, two fixed decomposition tables validate the operand chunks, and the ROM itself is a preprocessed lookup table padded with an unprovable sentinel ^[52][64].

The structural fork worth a hardware analogy: Jolt/Ceno/OpenVM decode at preprocessing — the analog of a trace cache or predecoded I-cache, paid once per static instruction — while Airbender decodes per cycle in constraints, the analog of hardwired decode, paid per dynamic instruction but requiring no per-program preprocessing of the proving key beyond the ROM table. Both positions are coherent; they trade setup cost against cycle cost, and Airbender's choice fits a system whose one guest (an L2 block executor) is fixed and whose cycles are astronomically many.

5.3 · The field is an architectural parameter

No hardware ISA document has a chapter on "the field," but for a zkVM it determines more than XLEN does. The four data points:

One correction to our own study notes, worth making publicly since we made the error publicly available to ourselves: the note this article grew from tabulated Airbender's field as Baby Bear. The pinned source is unambiguous — Mersenne31Field with order 2³¹−1 ^[54]. Two 31-bit fields, easy to conflate, materially different in reduction cost and FFT structure; the kind of cell-level error a table invites and a source pin catches.

The deeper point for an ISA audience: field size versus word size is the zkVM's word-size decision, and it does not track the guest's XLEN. Jolt proves a 64-bit ISA in a 254-bit field (word ⊂ field, comfortably); the other three prove a 32-bit ISA in 31-bit fields (word ⊄ field, permanently limbed). The apparent coincidence that everyone's ratio lands near "word ≈ field or word = 2 × 16-bit limbs" is not a coincidence at all — it is the same engineering pressure that gave hardware its power-of-two register widths: range-check tables want power-of-two sizes, and limb counts want to be small.

5.4 · Four answers to opcode heterogeneity

Finally, the architecture-level taxonomy, which §3 promised. The ISA hands every implementer the same problem: ~50 operations of wildly different character must somehow share one execution substrate. Microarchitects answer with functional units and issue queues; these four proof systems answer with:

The trade is the CISC/RISC argument reincarnated with different physics. The universal-row design pays a fixed per-cycle overhead so that rare opcodes cost nothing extra to support; the chip-per-opcode design pays nothing for uniformity but must commit, prove, and verify a chip even for opcodes the program barely uses, and its proving-key surface grows with the ISA. Delegation splits the difference by class: keep the base integer core small and uniform, and let anything with internal structure (hash rounds, big-integer ops) be a separate argument connected by a bus — which is, of course, exactly what the ISA itself did when it pushed those same operations out to extensions.

6 · The opcode encyclopedia

The reference deliverable. Every instruction of RV32I, RV64I, M, A, C, Zicsr, and Zifencei, with its encoding, exact semantics, the spec-mandated edge cases an implementation answers for, and the proving considerations attached to it in a zkVM. Conventions: sext/zext = sign-/zero-extension; edge cases states normative ISA behavior per the ratified manual ^{[1][2][3][4][5]}; proving considerations distills the obligations of §4 and names the four VMs' concrete treatments where they differ, with citations carried by the corresponding §4 discussion unless a claim appears here only. The encoding line gives format · major opcode · funct fields. Where an entry says "as row X," the obligation is identical and only the noted delta applies — the table is normalized the way an ISA manual is, not the way a tutorial is.

6.1 · Integer register–immediate (OP-IMM = 0010011)

6.2 · Integer register–register (OP = 0110011, funct7 = 0000000 / 0100000)

6.3 · Upper-immediate (LUI = 0110111, AUIPC = 0010111)

6.4 · Control transfer (JAL = 1101111, JALR = 1100111, BRANCH = 1100011)

6.5 · Loads and stores (LOAD = 0000011, STORE = 0100011)

6.6 · RV64I additions (OP-IMM-32 = 0011011, OP-32 = 0111011, plus widths)

These twelve exist to keep 32-bit arithmetic exact on a 64-bit machine, and they all share one invariant a prover must internalize: every *W result is the sign-extension of a 32-bit value, so bits 63:31 are equal — an invariant the RV64 ABI extends even to unsigned 32-bit values ^[1]. Of our four VMs only Jolt (RV64) proves them; its uniform recipe is: compute in 64-bit space, then apply a word-sign-extension lookup — with per-family wrinkles noted below ^[11][17].

6.7 · M extension (OP funct7 = 0000001; W variants on OP-32)

6.8 · System: MISC-MEM (0001111), SYSTEM (1110011), Zicsr, Zifencei

6.9 · A extension (AMO = 0101111; f3 = 010 (.W) / 011 (.D); Zalrsc + Zaamo)

Context for every row: of the four VMs only Jolt decodes this opcode space ^[6] — elsewhere atomics are a build-time rejection and a toolchain problem (the lower-atomic story of our companion survey). Alignment here is mandatory: unlike ordinary loads/stores, a misaligned LR/SC always raises an exception, and a misaligned AMO does too absent the optional misaligned-atomicity-granule PMA ^[3]. On a single-hart, non-preemptive machine, every atomicity and ordering guarantee below is discharged by sequential execution itself; what remains provable is the data flow and the reservation logic.

6.10 · C extension (Zca; quadrants 00/01/10)

Every RVC instruction expands to exactly one base instruction; the table gives the expansion, the encoding constraints (which are the extension's entire semantic content), and what — if anything — is left for a prover. The global answer to the last column: for a VM that statically expands (Jolt, the only acceptor among our four ^[21]), each row's proving obligations are identical to its expansion's row above, plus exactly two deltas visible in constraints: sequential next-PC is +2, and the linking jumps write PC+2. Reserved code points and the ×4/×8-scaled zero-extended offsets are decode-time facts, checked where decode is checked.

7 · What survives contact with a hardware review

Summing up for the reviewer this piece is addressed to — the seven claims we would defend at a whiteboard:

1. The unprivileged compute semantics are preserved to the bit, and that claim is checkable. Wraparound, shift masking, SLTIU's sext-then-unsigned, division's trap-free degenerate results, DIVUW's sign-extended unsigned quotient, JALR's cleared bit 0, the C.JALR link exception — every one is a constraint or table property in at least one pinned codebase cited here, not a testing outcome. The compliance methodology differs from silicon's in kind: not "ran the suite," but "the constraint system admits no other answer." When we found our own study notes wrong (Airbender's field), the pin settled it in one file read.

2. Compliance ends at the system boundary, uniformly, and honesty requires saying so. No VM here implements the trap model, the CSR file, FENCE's ordering sets, or misaligned access as the manual writes them. The unprivileged spec's own EEI parameterization makes each choice legal — but "we prove RISC-V" always means "we prove an EEI," and the EEIs differ enough that identical guests are portable across these four VMs only at the level our companion article covers (toolchain and runtime), not at the level of raw traces.

3. Illegal instructions mark the deepest divergence: trap versus unsatisfiability. Silicon must define behavior for every bit pattern; a prover may instead make bad patterns unprovable (Airbender constrains the decoder's invalid flag to zero and pads its ROM with a booby-trapped CSRRW; Ceno traps in the emulator so no trace exists; OpenVM and Jolt reject at build). This is sound for the "an honest run of this program" statement a zkVM actually makes — but a hardware reviewer should recognize that the ISA's totality (δ defined on all inputs) has been traded for a partial function plus the meta-claim that the program stays inside it.

4. Nondeterminism is the resource that redraws the price list. Division cheaper than shifting; SC's spurious failure encoded exactly by an advice bit; sub-word extraction steered by witnessed address bits. Every "compute the answer" obligation that silicon carries becomes "check an answer someone already wrote down" — and the residual engineering discipline is that every advice value must be pinned by range checks and defining constraints, because unconstrained advice is not an optimization but a forgery. The division checklist of §4.9 is the pattern in miniature.

5. The microarchitectural vocabulary does not transfer; the invariants do. Ports, predictors, barrel shifters, carry-lookahead, store buffers — none has a referent here. What transfers untouched: x0's hardwiredness (actively enforced in four different ways), the sign-extension invariant of RV64 words, alignment discipline, and the load-store architecture's quarantine of memory traffic — which proves to be the ISA design decision the proving model rewards most.

6. The four architectures are one design space, and it is the control-unit argument again. Universal row + tables (microcode), chip per opcode (hardwired control), chip per class on open buses (chiplet fabric), family multiplexing + delegation (minimal core + co-processors). The forty-year-old trade between uniformity and specialization reappears intact, with constraint-degree and commitment count as the new area and timing.

7. The encyclopedia's per-row lesson compresses to one sentence: an instruction's proving cost is set not by its computational depth but by how much non-algebraic structure — bit selection, ordering, interpretation — its semantics smuggle in. ADD is nearly free; ADDI freer; DIV is advice; but a byte load is a small protocol and a variable shift is a genuine design problem. That inversion, applied instruction by instruction down the encyclopedia, is what it means to implement an ISA under a prover.

References

All GitHub citations are permalinks pinned to full commit SHAs, verified to exist publicly; line numbers refer to the files at those exact revisions and were extracted by reading each repository at its pinned commit during July 27, 2026. Specification citations pin the riscv-isa-manual sources at a main-branch commit fetched the same day; the semantics cited are those of the ratified Unprivileged ISA. The four zkVM pins are the same revisions used by our companion survey of guest compilation, so the two articles cite one consistent snapshot of each codebase.

1. RISC-V Instruction Set Manual, Vol. I: Unprivileged ISA — base integer chapters at riscv-isa-manual@4757308 · src/unpriv/rv32.adoc, rv64.adoc, intro.adoc, rv-32-64g.adoc (encoding tables). Immediate layouts, x0, HINTs, alignment and misalignment norms, taken-branch exception rules, W-op sign extension.
2. M extension — src/unpriv/m-st-ext.adoc: division-by-zero and overflow semantics table, trap-free rationale, MULH/fusion notes, W-variant sign extension.
3. A extension — src/unpriv/zalrsc.adoc, zaamo.adoc, a-st-ext.adoc: reservation rules, SC failure codes, forward-progress constraint, mandatory alignment, aq/rl.
4. C extension — src/unpriv/zca.adoc, c-st-ext.adoc: per-instruction expansions, register/immediate restrictions, reserved and HINT code points, the C.JALR pc+2 link note, IALIGN=16 consequences.
5. Zicsr — src/unpriv/zicsr.adoc: read/write gating and side-effect table, uimm zero-extension, CSR-vs-FENCE I/O classification.
6. Jolt decoder — jolt@e0d5d7e · crates/jolt-program/src/image/decode.rs L15–L74 (major-opcode dispatch), L143–L169 (22 AMO forms), L171–L180 (SYSTEM: exact ECALL/EBREAK/MRET words, CSRRW/CSRRS only), L70–L73 and L524–L526 (unknown encodings fail at image load).
7. Jolt instruction inventory — crates/jolt-riscv/src/lib.rs L22–L273: 135 decoded source kinds; L187–L215: the 29 real RV64 opcodes surviving into proven bytecode; instructions/mod.rs L331–L336: kinds deliberately proven only by expansion.
8. Jolt field and lookup architecture — crates/jolt-field/src/arkworks/bn254.rs L15–L22 (BN254 scalar field); book · instruction_execution.md L8–L44 (2¹²⁸-entry tables via prefix-suffix Shout); jolt-lookup-tables/src/traits.rs L93–L110 (interleaved vs combined operands).
9. Jolt R1CS — crates/jolt-r1cs/src/constraints/rv64.rs: memory-link rows L272–L318, SUB bias L360–L371, PC/branch/jump rows L414–L505, product constraints L518–L531, 22-constraint/38-variable summary L1–L69, L551–L558; tables/range_check.rs L13–L31 (truncation table); instructions/i/add.rs L3–L8.
10. Jolt lookup-table inventory — crates/jolt-lookup-tables/src/tables/mod.rs L115–L156: the 40 tables enumerated.
11. Jolt shift expansions — expand/shifts/sll.rs (Pow2+MUL), slli.rs (single MULI row), srl.rs, shared.rs (bitmask immediates), srlw.rs, sllw.rs; tables pow2.rs L10–L17 (mod-XLEN masking), virtual_sra.rs L15–L54 (sign term in the MLE); expand/arithmetic/addw.rs L9–L30 (ADDW lowering).
12. Jolt comparison/branch lookups — instructions/riscv/slt.rs L6–L23, beq.rs L6–L21 (per-branch table mapping), tables/equal.rs L14–L33 (product-form equality MLE).
13. Jolt jumps — instructions/riscv/jal.rs L6–L34; tables/range_check_aligned.rs L13–L16 (JALR bit-0 clearing in the table); link/next-PC rows in [9].
14. Jolt bytecode fetch — book · bytecode.md L3–L54: expanded bytecode as a committed Shout table, dual PC bookkeeping.
15. Jolt RAM — book · ram.md L3–L59 (doubleword Twist cells, address remap); sub-word lowerings expand/memory/shared.rs L29–L139 (LB/LH), L478–L550 (SB/SH RMW), lw.rs L7–L53; instructions/i/ld.rs L3–L8 (LD/SD the only memory bytecode).
16. Jolt registers — common/src/constants.rs L2–L5 (128 = 32 + 96 virtual); book · registers.md L8–L29 (reservation slots, CSR shadows, scratch layout).
17. Jolt multiplication — product constraint and UpperWord extraction in rv64.rs L373–L379 and tables/upper_word.rs L13–L16; MULH sign-correction expansion expand/arithmetic/mulh.rs L3–L63.
18. Jolt division — expand/division/shared.rs L3–L45 (advice entry), L113–L263 (64-bit signed sequence), L286–L402 (word variants' extra asserts); divu.rs L3–L69; tables valid_div0.rs, virtual_change_divisor.rs, valid_unsigned_remainder.rs; instructions/virt/advice.rs L3–L8 (advice is range-checked and rd-written).
19. Jolt system ops — expand/control_flow/ecall.rs L3–L66 (M-mode trap entry), ebreak.rs (JAL+0 self-jump), mret.rs, csrrs.rs L3–L77 (shadow-register moves, UnsupportedCsr); instructions/i/fence.rs L3–L6 (FENCE proven as flagless no-op).
20. Jolt atomics — AMO lowering and branch-free min/max expand/memory/shared.rs L176–L319; lrw.rs L5–L47 (reservation registers); scw.rs L3–L90 (Boolean-advice success, conditional store).
21. Jolt compressed — crates/jolt-riscv/src/uncompress.rs L1–L12 (static expansion before decode); flags.rs L47–L48 (IsCompressed flag), flag derivation lib.rs L335–L356.
22. Ceno instruction set and rejections — ceno@cb03807 · ceno_emul/src/rv32im.rs L168–L219 (InsnKind enum), L298–L310 (Invalid-category trap); disassemble/mod.rs L348–L430 (EBREAK/CSR/FENCE/MRET/WFI → unimp; 4-byte ELF walk, no RVC).
23. Ceno chip-per-opcode registration — ceno_zkvm/src/instructions/riscv/rv32im.rs L282–L338 (one circuit per InsnKind), L426–L435 (table circuits).
24. Ceno field and limbs — e2e.rs L102–L128 (BabyBear default, Goldilocks alternative); constants.rs L24–L37 (2×16-bit limbs, PC_BITS=30); Cargo.toml L77–L88 (u16limb default); uint.rs L102–L156 (limb range checks on creation).
25. Ceno ADD/SUB — instructions/riscv/arith.rs L55–L99: carry-witnessed add; SUB as re-arranged addition.
26. Ceno logic — logic/logic_circuit.rs L46–L133 (byte-wise table constraint); gkr_iop/src/tables/ops.rs L3–L91 (2¹⁶-row And/Or/Xor/Ltu tables).
27. Ceno shifts — shift/shift_circuit_v2.rs L26–L198 (one-hot markers, mod-32 masking, XOR-extracted sign; comments crediting the OpenVM core), L431–L480 (immediate wrapper); shift_circuit.rs L55–L141 (v1 pow2 design).
28. Ceno comparisons and branches — slt/slt_circuit_v2.rs L47–L84; gadgets/signed_limbs.rs L45–L149 (one-hot diff marker, biased MSB witnesses); branch/branch_circuit_v2.rs L56–L130 (inverse-marker equality); b_insn.rs L29–L90 (two-arm next-PC).
29. Ceno jumps — jump/jal_v2.rs L59–L97; jalr_v2.rs L59–L135 (align2 target, range-checked link); j_insn.rs L19–L56 (target pinned via program record); emulator bit-0 clear rv32im.rs L320–L357.
30. Ceno LUI/AUIPC — lui.rs L51–L97, auipc.rs L29–L110 (default circuits); disassemble/mod.rs L256–L335 (Goldilocks build transpiles both into widened ADDI, PC folded in).
31. Ceno MUL family — mulh/mulh_circuit_v2.rs L55–L211: schoolbook limb product, 18-bit carry range checks, sign-extension witnesses per signedness variant.
32. Ceno division — div/div_circuit_v2.rs L31–L363 (advice q/r, recomposition, divisor-zero forcing q limbs to 0xFFFF, |r|<|d| one-hot comparison, sign constraints), L623–L699 (special-case witness enumeration incl. signed overflow); emulator semantics rv32im.rs L392–L419.
33. Ceno memory — memory/load_v2.rs L61–L171 (per-width circuits, limb/byte muxing, sign extension), store_v2.rs L59–L136 (RMW splice); insn_base.rs L684–L800 (MemAddr alignment gadget); emulator misalignment traps rv32im.rs L465–L547.
34. Ceno registers/timestamps — insn_base.rs L26–L59 (state in/out records); tracer.rs L127–L131 (four subcycle ticks); gkr_iop/src/circuit_builder/ram.rs L12–L119 (paired records, prev_ts < ts under 29 bits); gadgets/is_lt.rs L181–L212; tables/ram.rs L26–L252 (init/final tables); vm_state.rs L19 (33 registers, RD_NULL sink).
35. Ceno program table — tables/program.rs L85–L228 (fixed decoded columns, per-kind immediate encodings, multiplicities); fetch lookups r_insn.rs L31–L65.
36. Ceno ECALL/precompiles — ecall_insn.rs L18–L70; ecall/halt.rs L44–L75 (exit code public, next_pc = 0); circuit fleet and dispatch rv32im.rs L340–L424, L924–L1044; syscalls.rs L15–L62 (SP1-compatible codes).
37. OpenVM opcodes/transpilation — openvm@425913b · transpiler/src/instructions.rs L30–L266 (38 VM opcodes with class offsets); rrs.rs L20–L363 (1-to-1 transpile); transpiler.rs L45–L75 (32-bit-word consumption; unrecognized → ParseError at build).
38. OpenVM executors — circuit/src/extension/mod.rs L94–L173: 10 Rv32I + 3 Rv32M + HintStore chips; LOADB/LOADH routing.
39. OpenVM field/limbs/address spaces — docs · specs/openvm/isa.mdx L30–L44 (Baby Bear 15·2²⁷+1), L113–L131 (registers = address space 1, pointers [0,128)); instructions/src/riscv.rs L1–L9 (4×8-bit limbs); program.rs L13–L17 (PC_BITS=30).
40. OpenVM x0 handling — transpiler/src/util.rs L24–L47 (rd=x0 → NOP for side-effect-free ops); adapters/rdwrite.rs L37–L101 (needs_write); adapters/loadstore.rs L145–L158 (suppression only for loads to x0 — the access still happens).
41. OpenVM memory argument — docs · architecture/memory.mdx L18–L106 (BEGKN92 offline checking, timestamps in [1,2²⁹], split/merge access adapters); offline_checker/bridge.rs L297–L307 (per-access timestamp ordering); bus.rs L77–L103; volatile/mod.rs L45–L58 (boundary rows).
42. OpenVM ALU and bitwise lookup — base_alu/core.rs L93–L139 (boolean limb carries; OR/AND via XOR identities; XOR lookup as range check); bitwise_op_lookup/mod.rs L30–L80 (2⁸×2⁸ preprocessed table, dual multiplicities).
43. OpenVM shifts — shift/core.rs L108–L213: one-hot bit/limb markers, forced bit_multiplier, mod-32 masking range check, XOR-verified sign bit.
44. OpenVM comparisons/branches — less_than/core.rs L95–L147 (one-hot diff marker, biased MSB witnesses); branch_eq/core.rs L79–L112 (inverse-marker equality; two-arm to_pc); branch_lt/core.rs L100–L164; adapters/branch.rs L67–L99.
45. OpenVM jumps and upper-immediates — jal_lui/core.rs L88–L118 (shared chip; XOR-trick PC cap); jalr/core.rs L90–L149 (witnessed-and-dropped LSB, range-bounded target and link); auipc/core.rs L80–L152; transpile-time immediate pre-shifts rrs.rs L248–L285.
46. OpenVM multiplication — mul/core.rs L73–L92 (schoolbook convolution, RangeTupleChecker pairs); mulh/core.rs L92–L156 (dual carry chains, sign-extension limbs); tuple-checker sizing extension/mod.rs L78–L80.
47. OpenVM division — divrem/core.rs L122–L314 (advice q/r, carry-checked recomposition, zero_divisor and r_zero flags, |r|<|c| one-hot comparison, sign constraints), L586–L610 (signed-overflow execution path).
48. OpenVM loads/stores — adapters/loadstore.rs L170–L250 (aligned-block adapter, divisibility alignment check, pointer bounds); loadstore/core.rs L25–L48 ((opcode, shift) as internal opcodes); load_sign_extend/core.rs L109–L150; misalignment contract riscv-custom-code.mdx L45–L50.
49. OpenVM system boundary — transpiler/src/lib.rs L48–L62 (ECALL/EBREAK/CSR → unimp; the CSRRW-counter-reset NOP carve-out); util.rs L13–L58 (i12→u24 sign-extension), L151–L166 (unimp = TERMINATE code 2); custom system opcodes riscv-custom-code.mdx L31–L43 and guest/src/lib.rs L12–L26; FENCE → NOP rrs.rs L359–L362; hint writes byte-checked hintstore/mod.rs L169–L219.
50. OpenVM fetch and buses — arch/execution.rs L394–L455 (execution bus, default PC step); program/bus.rs L26–L48 (fetch lookup keyed pc+opcode+operands); program/trace.rs L38–L72 (cached program commitment); connector/mod.rs L171–L178 (initial/final PC as public values).
51. Airbender operations and machines — zksync-airbender@7e05fe2 · cs/src/devices/risc_v_types.rs L18–L59 (36 executor operations); full_isa_with_delegation_no_exceptions/mod.rs L23–L39 (13 op-family circuits); ops/constants.rs L1–L12 (no FENCE/AMO major opcodes exist).
52. Airbender decoder — cs/src/machine/mod.rs L271–L348 (2¹⁷-entry opcode‖funct3‖funct7 bitmask table); decoder/decode_optimized_must_handle_csr.rs L47–L161 (chunk decomposition + fixed check tables), L192–L259 (immediate assembly), L287–L394 (flag allocation).
53. Airbender illegal = unsatisfiable — decode_and_read_operands.rs L147–L157 (is_invalid constrained to zero under trusted code); docs/philosophy_and_logic.md L7; machine/mod.rs L29–L32 (UNIMP = 0xc0001073 = csrrw x0, cycle, x0; NON_DETERMINISM_CSR = 0x7c0).
54. Airbender field — field/src/base.rs L14–L24 (Mersenne31, order 2³¹−1); cs/src/types.rs L905–L919 (Register = 2×16-bit range-checked limbs); philosophy_and_logic.md L11–L14 (degree-≤2 AIR, ~2²²-cycle circuit chunks).
55. Airbender ADD/SUB and relation pooling — cs/src/devices/utils.rs L6–L79 (AddSubRelation); optimization_context.rs L755–L871 (shared relation slots selected by orthogonal exec flags).
56. Airbender bitwise ops — ops/binops.rs L98–L219 (four byte-table queries, funct3-indexed; range checks come free from the byte tables); definitions/table_type.rs L4–L7 (AND=7, OR=6, XOR=4 = the funct3 values).
57. Airbender shifts — ops/shift.rs L142–L265 (AND-table masking, two ShiftImplementation queries, SRA filler, rotates todo!()); tables tables.rs L1609–L1650 (2²²-entry shift table) and L1200–L1240 (SRASignFiller).
58. Airbender conditional family — ops/conditional.rs L23–L253 (SLT*+branches unified; borrow+is-zero; taken-misaligned unprovable; branches write 0 to x0); tables.rs L1242–L1383 (128-entry resolver); cs/circuit.rs L583–L611 (inverse-witness is-zero).
59. Airbender jumps — ops/jump.rs L24–L125 (JAL/JALR one family; cleanup lookup clears bit 0, bit 1 unsatisfiable); tables.rs L1123–L1146 (JumpCleanupOffset).
60. Airbender memory and upper-immediates — ops/load.rs L160–L355 (alignment unsatisfiability, ROM/RAM split, query repurposing), store.rs L180–L273 (no stores into ROM; byte/halfword splice), lui_auipc.rs L54–L148; tables L1386–L1416 (ROM/RAM separator) and L1735–L1801 (combined sub-word extension lookup).
61. Airbender multiply/divide — ops/mul_div.rs L37–L68 (one MUL family), L272–L373 (advice-based DIV/REM, remainder bound via borrow), L499–L545 (overflow witness path), L580–L691 (signed remainder logic — verified by the in-tree z3/div_optim_signextension.z3 script — and div-by-zero quotient pinning); optimization_context.rs L37–L47 and L1104–L1400 (MulDivRelation and its chunked carry constraints).
62. Airbender CSR/delegation — ops/csr.rs L35–L89 (CSRRW only; ECALL/EBREAK undecodable); csr_with_delegation.rs L31–L102 (whitelist trap, delegation requests, range-checked oracle reads); csr_properties.rs L4–L41; docs/subarguments_used.md L48–L62 (set-equality delegation argument); delegation ids u256_ops_with_control.rs L6–L7.
63. Airbender registers/memory argument — minimal_state.rs L6–L33 (PC is the only persistent state); decode_and_read_operands.rs L161–L240 (3 shuffle-RAM queries, fixed in-cycle timestamps; write-side range checking induction L171–L173); ram_access.rs L3–L18; constants.rs L7–L54 (2×19-bit timestamps, 2³⁶-cycle budget); writeback_no_exceptions.rs L38–L101 (is-zero x0 masking); subarguments_used.md L15–L46 (read/write-set permutation argument, lazy init/teardown).
64. Airbender fetch/ROM/variants — machine/utils.rs L50–L127 (next-PC carry constraint), L253–L282 (ROM-range fetch lookup); machine_configurations/mod.rs L125–L215 (ROM table padded with UNIMP); devices/diffs.rs L9–L110 (PC selection; PC_INC_STEP=4, no RVC); …no_signed_mul_div/mod.rs L22–L38 (shipped variant drops MULH/MULHSU/DIV/REM); ops/mop.rs L30–L106 (Mersenne31 field ops in SYSTEM space); risc_v_simulator/src/cycle/state.rs L1139–L1158 (FENCE arm commented out — illegal).