PVM2 — per-instruction gas cost table

PVM2’s gas accounting uses the single-pass pipeline model. The canonical definition is the Rust source (gas_sim.rs + gas_cost.rs) plus this reference doc. (An older Lean formalization under spec/Jar/JAVM/ is stale — it predates microkernel v3 and the 15-register file — and is not authoritative.) For each basic block, predecode walks the instructions once, feeding each through GasSimulator; the final block cost is max(max_done − 3, 1). This block cost is the #1 (execution) component only, and it is charged once per block, at block entry (the charging discipline — pre-reservation, OOG never charges, gas never goes negative — is specified in gas-cost.md §1). The block cost is further scaled by the #2 memory-access-latency footprint multiplier (×1–4) before it is charged; that multiplier is defined in gas-cost.md §2. The per-instruction cost table (rv_fast_cost) and the block-driver (rv_gas_cost_for_block) live in rust/javm-exec/src/gas_cost.rs — next to PVM’s table, so when PVM is eventually retired the file shrinks rather than fragments.

The Lean spec for an earlier flat-per-instruction-sum PVM2 gas model (spec/Jar/JAVM/GasCostPVM2.lean) was removed; the canonical PVM2 gas table is now the Rust source plus this reference doc.

Pipeline model (single-pass)

State per block: reg_done[15] (cycle when each register’s value is ready) + cycle (current decode cycle) + decode_used (slots consumed this cycle) + max_done (running max completion).

For each instruction in program order:

1. Decode throughput. If decode_used >= 4, advance cycle by 1 and reset decode_used = decode_slots. Else decode_used += decode_slots.
2. Move-reg fast path. is_move_reg instructions propagate reg_done[dst] = reg_done[src] and skip the rest.
3. Data dependency. start = max(cycle, max(reg_done[r] for r in src_mask)).
4. Completion. done = start + cycles.
5. Write back. reg_done[r] = done for every r in dst_mask.
6. Track. max_done = max(max_done, done).

Block cost = max(max_done − 3, 1). The “−3” normalizes the steady-state pipeline depth (3 stages: decode, dispatch, execute).

Each instruction’s FastCost carries:

• cycles — execution latency
• decode_slots — front-end cost (1–4)
• exec_unit — informational only; the single-pass model doesn’t model EU contention (decode throughput subsumes ALU/LOAD/STORE contention; MUL/DIV are rare enough that latency already serializes them via data deps)
• src_mask / dst_mask — 15-bit register bitmasks (PVM2’s 15 architectural regs map to bits 0..14, ordered x1, x2, x5..x15, then x3, x4 in the two high slots)
• is_terminator — ends the block; nothing is decoded after it
• is_move_reg — handled in the decode-cycle path; propagates reg_done without consuming a ROB-equivalent slot

Why single-pass (and not the full ROB / EU-contention model in GasCostFull.lean):

• Speed. O(n) per block, one pass over the instructions, no inner cycle-by-cycle loop.
• No slot limit. Real PVM2 basic blocks can have 100+ RV instructions (crypto inner loops). A 32-entry ROB simulator would need slot recycling and is a lot more code.
• EU contention subsumed. The 4-wide decode bandwidth already caps the rate at which ALU/LOAD/STORE-class ops can begin. The only contended units in a ROB model are MUL/DIV, and those are rare + high-latency enough that data dependencies serialize them in practice.

Per-instruction cost table

The columns below are: op (PVM2 mnemonic), cycles, decode_slots (range when overlap-dependent), EU, src (which RvInst fields contribute to src_mask), dst (likewise for dst_mask), term (terminator flag), PVM equiv (the PVM byte opcode this row mirrors, if any).

Loads and stores

Upper / load-immediate

(addi rd, x0, imm — used by the linker as the small-immediate load — bills as the general addi row below; there’s no special fast-path.)

Integer ALU (64-bit)

decode_slots = 1 when rd overlaps a source register, else 2 (matches PVM’s overlap rule).

Integer ALU (32-bit)

M extension (multiply / divide)

Zbb — basic bit manipulation

Zba — shift-add

x86’s LEA family folds these into one cycle.

Zbs — single-bit

Zicond — conditional move

Control flow

Note: PVM has a 1-cycle fast-path for branches whose target is opcode 0 (trap) or 2 (unlikely). The PVM2 linker rewrites trap targets to direct traps, so this fast-path rarely fires; we use a flat 20 (the PVM default for “live” branches).

Custom-0 (PVM2-specific)

Note: funct3=011 (the former br_table) is reserved — see “Reserved encoding” below. PVM2 routes indirect jumps through plain jalr (see “Control flow” above), not a custom table op.

Note: ecall.jar and ecalli each form their own gas block (a forced block start) and are charged dynamically by the kernel, not through the static per-block preamble — their true cost (a CALL frame, a host op’s work) is unknowable at compile time. The 100-cycle row above is only the static instruction component (a floor); the kernel adds the actual materialization cost at runtime, with out-of-gas re-attempting at the ecall’s own PC. For an in-kernel CALL this dynamic charge now also includes the callee’s JIT compile (O(code), per declared code page) and its eager read-only page-in (one charge per declared 2 MiB unit), computed statically from the callee Image. See gas-cost.md §3 “ecall/ecalli blocks”.

Fences (no-op)

Reserved encoding

If a reserved encoding is reached at runtime it traps. The simulator still needs a cost row so a pathological program can’t be “free”.

Register mapping

PVM2 has 15 architectural registers (RV64E’s full GPR file): x1, x2, x5..x15, plus x3, x4 (with x0 = zero). They map to FastCost::src_mask / dst_mask bits as follows:

x3/x4 occupy the two high slots so the 13 commonly-used registers keep mask bits 0..12 unchanged — every conformant program (which never references x3/x4) produces bit-for-bit identical masks, and therefore identical gas, as before the file grew to 15.

x3/x4 spill cost

x3 and x4 are real registers the runtime executes, but they are not guaranteed host-register-resident: a host with exactly 13 registers (today’s x86-64 JIT) holds them in memory and spills on each access (see Register model in rv64e-xjar-eei.md and the host contract in portability.md).

Because the worst-case conforming host spills them, the gas model charges the memory-spill cost for every x3/x4 operand unconditionally (on every host, whether or not it actually spills — gas is a spec-fixed upper bound, so a register-rich host runs faster than charged without affecting consensus). Concretely: each instruction operand position (rs1, rs2, rd) that names x3 or x4 adds mem_cycles (= the LOAD/STORE latency, default 25) to that instruction’s cycles before it is fed to the simulator — matching the load/op/store the recompiler’s spill path emits. An instruction touching no x3/x4 operand is charged exactly as its table row above.

Footprint scaling (#2). The mem_cycles = 25 here is the base LOAD/STORE latency at the smallest footprint tier (×1). It is scaled by the memory-access footprint multiplier (×1–4, from the Instance’s total accessible pages) before the block cost is charged — so a memory-heavy block in a large declared footprint pays proportionally more. The multiplier and tiers are normative in gas-cost.md §2; the x3/x4 spill charge above scales with it like any other memory operand.

Reasoning for the non-PVM rows

Some PVM2 instructions have no PVM byte-opcode equivalent (notably Zba/Zbs and the 32-bit Zbb rotates). Their costs were chosen to match the underlying x86 native cost the recompiler emits:

• Zba shift-add maps directly to a 1-cycle LEA form on x86. ALU, 1 cycle, decode_slots follows the overlap rule.
• Zbs single-bit lowers to BMI2 bzhi/pdep-class instructions on x86 (single-cycle ALU on Skylake+).
• Zbb 32-bit rotates (rolw, rorw, roriw) are symmetric with their 64-bit counterparts at +1 cycle (matches PVM 32-bit ALU convention).

Sync between Rust and this doc

The source of truth is rust/javm-exec/src/gas_cost.rs::rv_fast_cost. Any change to a row above must update the Rust function and vice versa. Drift between the two should fail a future conformance test (TODO once we have one).