Move bytecode expansion into jolt-program and fix CSR-zero handling

[quangvdao]

Summary

Moves bytecode expansion and verifier-critical program preprocessing out of the tracer-owned path and into the new jolt-program / strengthened jolt-riscv boundary.

This PR now includes implementation plus specs:

• jolt-riscv owns the normalized instruction vocabulary, operands, kinds, static instruction metadata, and conversion marker traits without depending on tracer.
• jolt-program owns RV64 program-image decode, bytecode expansion, materialized program/RAM/bytecode preprocessing, and a backend-neutral execution contract.
• tracer, SDK host helpers, and proof setup call through those lower program-construction APIs instead of owning canonical expansion/preprocessing semantics.
• jolt-program::expand rejects CSRRW/CSRRS with CSR address 0 as UnsupportedCsr(0), replacing the historical default-row behavior that could produce an address-zero row skipped by bytecode PC mapping.
• The old tracer-vs-jolt-program expansion bridge test was removed because it became circular once tracer delegated expansion to jolt-program; remaining coverage uses direct expansion tests and non-circular decode/normalization checks.

Specs

• Updates specs/bytecode-expansion-crate.md to describe the implemented crate split, the CSR-zero behavior correction, and the post-cutover testing strategy.
• Adds/updates specs/compiler-native-bytecode-expansion.md for the next extraction-friendly rewrite: a compiler-native lowering core with typed recipes, explicit source/target legality, symbolic temp lifetimes, fixed buffers, and MLIR-ready concepts.
• Records the Hax/Aeneas motivation and why the next pass should redesign expansion as a small inspectable lowering grammar instead of extracting arbitrary recursive Rust builders.

Testing

• cargo fmt -q
• cargo nextest run -p jolt-program --cargo-quiet
• cargo nextest run -p tracer jolt_program_rv64_decode_matches_tracer_normalization --cargo-quiet
• cargo clippy -p jolt-program --all-targets -q -- -D warnings
• cargo clippy -p tracer --all-targets -q -- -D warnings
• git diff --check

---

Disclosure: This PR description was updated by Codex, an AI assistant based on GPT-5, on behalf of Quang Dao.

[github-actions]

Claude spec review session started: https://claude.ai/code/session_01C4HndRVK9e4cgFodersdgj

[0xAndoroid]

Spec Analysis: Bytecode Expansion Crate

Dimension	Score	Gap
Goal	0.70	Scope ambiguity — 1 crate or 4?
Constraints	0.75	"Minimum first pass" contradicts AC
Success Criteria	0.70	Post-cutover invariant semantics unclear
Context	0.75	One factual claim about jolt-riscv looks wrong
Ambiguity		~28%

Status: Questions remain — 6 ambiguities to resolve before one-shot implementation.

---

Questions:

1. [Goal] Is this PR a single-crate split or a four-crate split? The Acceptance Criteria require all four crates (jolt-riscv-instructions, jolt-program-image, jolt-bytecode-expand, jolt-verifier-preprocess) to "exist and be a workspace member". The Design section then says "If the full split is too large for one PR, the implementation should still make the intended boundaries explicit and avoid further coupling. A minimum acceptable first pass is: instruction representation / common types → jolt-bytecode-expand → tracer, jolt-trace." These two statements disagree on what merging this PR requires. Pick one as binding. If staged across PRs, list which crates land in this PR vs. follow-ups, and reword the AC accordingly.

2. [Goal] How does the Instruction / Cycle macro split work? The spec moves Instruction, per-instruction structs, and RISCVInstruction to jolt-riscv-instructions, but Cycle and RISCVCycle<T> carry execution state and presumably stay in tracer. Today both enums are macro-generated together in tracer/src/instruction/mod.rs (around lines 419, 433) via a shared for_each_instruction!-style dispatch. Concretely: does the macro itself move (and tracer re-invokes it for Cycle), or are the enums decoupled, or is the macro split in two? The spec gestures at "macro-generated dispatch behind a narrow boundary" but doesn't commit to a structure, and getting this wrong means duplicating a long instruction list across two crates.

3. [Success Criteria] How is bytecode_expansion_parity maintained after the old path is deleted? Step 5 of the parity process says "Delete the old production expansion implementation from tracer." Step 6 says "Keep the golden fixture tests and property/invariant tests after deletion." But the proposed jolt-eval invariant bytecode_expansion_parity is described as "compare the old expansion path to the new crate output" — once the old path is gone, what does the invariant compare against? Options: (a) checked-in golden fixtures (then it's a snapshot test, not a parity invariant); (b) a frozen reference implementation kept inside the test crate; (c) something else. Pick one and rename if needed (e.g. bytecode_expansion_golden). Same question applies to bytecode_pc_mapping_consistency.

4. [Constraints] What changes about the allocator's concurrency contract? Today VirtualRegisterAllocator (tracer/src/utils/virtual_registers.rs:55-56) wraps its state in Arc<Mutex<[bool; NUM_VIRTUAL_REGISTERS]>> and Arc<Mutex<Vec<u8>>>, and Instruction::inline_sequence(&self, &VirtualRegisterAllocator, Xlen) takes the allocator by shared reference. The proposed API is expand_instruction(instruction: &Instruction, allocator: &mut ExpansionAllocator, xlen: Xlen) (mutable, presumably no Arc<Mutex>); the "Formal Verification Readiness" section also calls for plain owned data. This is a behavioral change at every call site, including tracer::emulator::cpu paths. Confirm: (a) the new allocator is single-owner &mut, (b) all current callers can be converted, and (c) any place that relied on allocator sharing across threads becomes a per-thread allocator. If any caller cannot be converted, name it.

5. [Context] Does jolt-riscv actually depend on tracer today? The "Crate Placement And Dependency Direction" section says "the concrete Instruction, Cycle, RISCVInstruction, NormalizedInstruction, and per-instruction structs live in tracer, and jolt-riscv currently depends on tracer for those types. Therefore a new jolt-bytecode-expand crate cannot both depend on tracer::instruction::* and be imported by tracer without creating a dependency cycle." Inspection of crates/jolt-riscv/Cargo.toml shows dependencies only on jolt-riscv-derive, serde, and strum — no tracer. If the dependency is real (transitive through jolt-riscv-derive?), point to the edge that would form the cycle. If not, the cycle-avoidance argument needs revising — jolt-bytecode-expand could potentially live below tracer short-term without a cycle even if Instruction stays in tracer.

6. [Success Criteria] Which BytecodePreprocessing is canonical? crates/jolt-trace/src/bytecode.rs already defines its own BytecodePreprocessing and BytecodePCMapper (code_size, bytecode, pc_map, entry_address) duplicating the canonical version in jolt-core/src/zkvm/bytecode/mod.rs:22,74. The "Files To Modify" section mentions both (crates/jolt-trace/src/bytecode.rs: remove or delegate and jolt-core/src/zkvm/bytecode/mod.rs: move or reexport from jolt-verifier-preprocess) but does not declare which version is the source of truth, what the merged surface looks like, or how the Arc<BytecodePreprocessing> shape used by JoltSharedPreprocessing (jolt-core/src/zkvm/verifier.rs:1731,1815,1844) is preserved. Specify the canonical type, what fields it carries, and what jolt-trace keeps (if anything).

---

After addressing these questions, update the spec and re-add the claude-spec-review-request label.

---

Generated by Claude Code

[quangvdao]

@0xAndoroid another spec review round?

[github-actions]

Claude spec review session started: https://claude.ai/code/session_01DiZV7TFUjKjBXJHrMasDuW

[0xAndoroid]

Spec Analysis: Bytecode Expansion Crate (Round 2)

Dimension	Score	Gap
Goal	0.88	Clear
Constraints	0.85	Clear
Success Criteria	0.85	Clear
Context	0.88	Clear
Ambiguity		~14%

Status: Approved — The spec is clear enough for one-shot implementation.

---

What changed since round 1:

All six prior questions are addressed substantively:

1. Single vs four-crate split — committed: "The implementation PR should land the full crate cutover described here rather than a partial first pass" (no more "minimum first pass" escape hatch).
2. Instruction/Cycle macro split — jolt-riscv-instructions owns the canonical instruction list and Instruction enum; tracer reuses the same list "via an exported macro or generated table" to define Cycle/RISCVCycle<T>. Explicit no-duplication rule.
3. Post-cutover invariant semantics — renamed to bytecode_expansion_fixture_consistency and bytecode_pc_mapping_consistency; both are fixture-based with a transition-only dual-run mode.
4. Allocator concurrency contract — explicit: &mut ExpansionAllocator, no Arc<Mutex<_>>, single-owner state flow, per-expansion ownership.
5. jolt-riscv → tracer dependency — verified accurate. crates/jolt-riscv/Cargo.toml:17 does have tracer = { workspace = true, features = ["std"] }. The cycle-avoidance argument now stands.
6. Canonical BytecodePreprocessing — jolt-core/src/zkvm/bytecode/mod.rs is the source; crates/jolt-trace/src/bytecode.rs (a structural duplicate) is the one to remove/delegate.

Summary of what will be built:

• Four new crates/ libraries: jolt-riscv-instructions, jolt-program-image, jolt-bytecode-expand, jolt-program-preprocess
• tracer becomes execution-only and consumes the new crates
• jolt-core consumes jolt-program-preprocess for materialized program preprocessing; PCS setup + JoltVerifierPreprocessing stay in jolt-core
• Three new jolt-eval invariants + a Criterion benchmark for decode+expansion
• Old expansion path is fully deleted (no compatibility shims)

Key invariants:

• Bit-for-bit expansion parity vs. current Instruction::inline_sequence for all RV32/RV64 families, including rd = x0, recursive helpers, and compressed metadata
• BytecodePCMapper::get_pc(address, virtual_sequence_remaining) produces stable indices
• JoltProgramPreprocessing digest is deterministic across the modular path
• No new cycle in the dependency graph; cargo tree shows no tracer dependency in jolt-bytecode-expand/jolt-program-image/jolt-program-preprocess

Soft suggestions for the implementer (not blocking):

• The spec uses "JoltProgramPreprocessing or the renamed equivalent" in several places. Pick the final name during implementation and use it consistently — minor rename churn is fine.
• The InstrAssembler rework is implied by the allocator contract change (it currently clones the Arc<Mutex> allocator) but its new state shape isn't drawn explicitly. Plan to redesign it as borrowing &mut ExpansionAllocator rather than holding a clone.
• The conditional "move compute_min_ram_K if doing so does not drag prover-only modules" leaves a fallback unspecified. If it can't move cleanly, leave it in jolt-core and call into jolt-program-preprocess for the pure pieces — no need to halt on this.

Next step: Run /implement-spec to implement this spec:

• Open in Claude Code (cloud) — run /implement-spec on this branch
• Or run /implement-spec locally in Claude Code

---

Generated by Claude Code

[github-actions]

Claude spec review session started: https://claude.ai/code/session_018HpUv9885oDLhRJ5RmCk5u

[0xAndoroid]

Spec Analysis: jolt-program Crate (Round 3)

Dimension	Score	Gap
Goal	0.90	Clear
Constraints	0.88	Clear
Success Criteria	0.85	Clear
Context	0.90	Clear
Ambiguity		~12%

Status: Approved — The spec is clear enough for one-shot implementation.

---

What changed since Round 2 (re-approved):

The spec was restructured in two ways since the prior approval:

1. Four crates fused into one (fuse program crate design). The previous four-crate split (jolt-riscv-instructions, jolt-program-image, jolt-bytecode-expand, jolt-verifier-preprocess) is now a single jolt-program crate with three internal modules (image, expand, preprocess). The internal module boundary still enforces the same dependency rules — expand must remain pure and must not inherit image's object dep — and the spec explicitly states this. Less workspace churn for the same conceptual separation.
2. Reuses existing jolt-riscv (reuse jolt-riscv for instructions). Rather than creating a new jolt-riscv-instructions crate, the spec strengthens the existing jolt-riscv crate (which today depends on tracer — verified at crates/jolt-riscv/Cargo.toml:17) by inverting that dependency: instruction data, formats, normalize, decode, and uncompress move into jolt-riscv, and tracer reuses the same canonical instruction list to generate Cycle / RISCVCycle<T>.

Both changes tighten the design rather than loosen it. The "minimum acceptable first pass" escape hatch from earlier drafts is gone — the spec now commits: "The implementation PR should land the full crate cutover described here rather than a partial first pass."

Codebase verification:

• crates/jolt-riscv/Cargo.toml:17 does carry tracer = { workspace = true, features = ["std"] } — the cycle-avoidance argument stands.
• Instruction and Cycle are macro-generated together via define_rv32im_enums! at tracer/src/instruction/mod.rs:414. The spec's "exported macro or generated table" + explicit "must not duplicate the long instruction list" addresses this directly.
• VirtualRegisterAllocator at tracer/src/utils/virtual_registers.rs:54-67 uses Arc<Mutex<[bool; …]>> and is cloned in InstrAssembler::new() (tracer/src/utils/inline_helpers.rs:106). The new &mut ExpansionAllocator contract requires reworking InstrAssembler to borrow rather than clone, which the spec calls out.
• tracer::decode (tracer/src/lib.rs:655) returns raw instructions; expansion happens in crates/jolt-trace/src/program.rs:389-399 via flat_map(|i| i.inline_sequence(&allocator, xlen)). The proposed migration of that flat_map into jolt-program::expand::expand_program is straightforward.
• BytecodePreprocessing truly is structurally duplicated between jolt-core/src/zkvm/bytecode/mod.rs:21-33 and crates/jolt-trace/src/bytecode.rs:21-31. Same fields (code_size, bytecode, pc_map, entry_address); jolt-core has a richer error enum, jolt-trace uses unwrap patterns. Removing the jolt-trace copy is sound.
• JoltSharedPreprocessing (jolt-core/src/zkvm/verifier.rs:1730-1736) carries Arc<BytecodePreprocessing>, RAMPreprocessing, MemoryLayout, max_padded_trace_length — exactly the layer the spec promotes to JoltProgramPreprocessing.

Summary of what will be built:

• One new crate (crates/jolt-program) with image, expand, preprocess modules.
• Existing crates/jolt-riscv strengthened: gains Xlen, NormalizedInstruction, Instruction enum, format/, decode, uncompress, traits; loses its tracer dependency.
• tracer becomes execution-only and consumes both crates; Cycle / RISCVCycle<T> reuses the canonical instruction list (no duplication).
• jolt-core consumes jolt-program::preprocess for materialized program preprocessing; PCS setup + JoltVerifierPreprocessing stay in jolt-core.
• jolt-trace::decode calls jolt_program::image::decode_elf + jolt_program::expand::expand_program; the local BytecodePreprocessing duplicate is deleted.
• Three new jolt-eval invariants registered via JoltInvariants::all(): bytecode_expansion_fixture_consistency, program_preprocessing_determinism, bytecode_pc_mapping_consistency. Plus a Criterion benchmark decode_expand.
• Old expansion path fully deleted (no compatibility shims).

Key invariants:

• Bit-for-bit expansion parity vs. current Instruction::inline_sequence for all RV32/RV64 families, including rd = x0 (side-effect-free no-op vs. side-effecting temp register vs. CSR/trap), recursive helpers, and compressed-instruction metadata.
• is_first_in_sequence and virtual_sequence_remaining preserved exactly per row.
• BytecodePCMapper::get_pc(address, virtual_sequence_remaining) produces stable indices.
• JoltProgramPreprocessing digest is deterministic and matches the existing prover path.
• Final dependency graph: cargo tree -p jolt-program shows no tracer edge; jolt-program::expand does not pull object even with default features.

Soft suggestions for the implementer (not blocking):

• The conditional move of compute_min_ram_K is left open — if relocating it drags prover-only modules into jolt-program::preprocess, leave it in jolt-core and have it call into the pure RAM preprocessing surface. The spec already gives this fallback explicitly.
• The InstrAssembler rework is implied by the allocator contract change but its new field shape isn't drawn. Plan to redesign it to borrow &mut ExpansionAllocator for the duration of emission rather than holding a clone.
• The macro split between jolt-riscv (generates Instruction) and tracer (generates Cycle/RISCVCycle<T>) is the highest-risk piece because of the long instruction list. Consider exporting the canonical instruction list as a macro_rules! token tree from jolt-riscv (e.g., jolt_riscv::for_each_instruction!) and re-invoking it in tracer to generate execution dispatch — this is the "exported macro or generated table" the spec mentions, and it preserves the no-duplication invariant.

Next step: Run /implement-spec to implement this spec:

• Open in Claude Code (cloud) — run /implement-spec on this branch
• Or run /implement-spec locally in Claude Code

---

Generated by Claude Code

[moodlezoup]

We should just fully drop RV32 support

[moodlezoup]

This is something I was explicitly avoiding in my recent refactor -- we should decide whether the instruction/cycle data structures should be concrete or abstract. I can see arguments for both sides

[moodlezoup]

Suggested change

	let mut inline = INLINE {
	opcode: metadata & 0x7f,
	funct3: (metadata >> 7) & 0x7,
	funct7: (metadata >> 10) & 0x7f,
	address: instruction.address as u64,
	operands: instruction.operands.into(),
	virtual_sequence_remaining: instruction.virtual_sequence_remaining,
	is_first_in_sequence: instruction.is_first_in_sequence,
	is_compressed: instruction.is_compressed,
	};
	inline.virtual_sequence_remaining = instruction.virtual_sequence_remaining;
	inline.is_first_in_sequence = instruction.is_first_in_sequence;
	let inline = INLINE {
	opcode: metadata & 0x7f,
	funct3: (metadata >> 7) & 0x7,
	funct7: (metadata >> 10) & 0x7f,
	address: instruction.address as u64,
	operands: instruction.operands.into(),
	virtual_sequence_remaining: instruction.virtual_sequence_remaining,
	is_first_in_sequence: instruction.is_first_in_sequence,
	is_compressed: instruction.is_compressed,
	};

[moodlezoup]

should we panic here?

[moodlezoup]

might as well add some helper methods here

Suggested change

	pub trait JoltInstruction:
	Copy + Into<NormalizedInstruction> + TryFrom<NormalizedInstruction>
	{
	pub trait JoltInstruction:
	Copy + Into<NormalizedInstruction> + TryFrom<NormalizedInstruction>
	{
	fn normalize(&self) -> NormalizeInstruction {
	(*self).into()
	}
	fn is_virtual(&self) -> bool {
	self.normalize().virtual_sequence_remaining.is_some()
	}

[moodlezoup]

now that we've flipped the dependency, tracer can use jolt_program::execution::RamAccess directly

[moodlezoup]

this test doesn't do anything

[moodlezoup]

can we add a debug_assert here that instruction.rd is zero?

[moodlezoup]

let's add a doc comment to this field

[moodlezoup]

let's just fold this into assembler.rs

[moodlezoup]

I don't like this match statement; ideally "has side-effects" should be declared via the jolt_instruction! macro in jolt-riscv. This problem is downstream of the awkward relationship between InstructionKind and the individual instruction structs declared in jolt-riscv; I think we need to rethink it a bit.

[moodlezoup]

Similar for this match statement; ideally we'd be able to just do instruction.expand()

[moodlezoup]

and each instruction struct from jolt-riscv would implement a VirtualSequence trait

[moodlezoup]

afaict there's no reason to have both this JoltInstructions enum and InstructionKind.
We can add a generic to JoltInstructions:

pub enum JoltInstructions<T = ()> {
    Noop,
    Add(Add<T>),
    Addi(Addi<T>),
    Sub(Sub<T>),
    // ....
}

And then use JoltInstructions instead of InstructionKind everywhere.

[quangvdao]

Posted by Cursor assistant (model: GPT-5.4) on behalf of the user (Quang Dao) with approval.

Thanks, went through these. The mechanical items are now addressed:

• renamed DecodedProgramImage / ExecutableProgram to Rv64ProgramImage / JoltProgram with docs;
• folded jolt-trace into jolt-riscv::trace;
• moved side-effect classification into InstructionKind::has_side_effects();
• removed tracer’s separate side_effects = true metadata so tracer now delegates to jolt-riscv for side-effect classification;
• added the tracer RAMAccess -> jolt_program::execution::RamAccess adapter;
• split expansion files per instruction;
• cleaned up the PC mapper validation, metadata module, noop_for assertion, allocator docs, uncompress signature, and the inert test.

The remaining items seem broader than review-nit scope:

• Fully deleting RV32 from tracer: the new jolt-program path rejects ELF32/RV32, so verifier-facing program construction is RV64-only now. Actually deleting tracer’s legacy RV32 execution code is a separate cleanup with wider emulator/test fallout.

• Concrete vs abstract instruction/cycle data structures: this branch keeps tracer’s concrete Instruction / Cycle / RISCVCycle<T> execution model and adds lightweight normalized/cycle-view boundaries in jolt-riscv / jolt-program. Replacing tracer internals with the abstract types would touch execution, trace generation, witness code, and tests.

• InstructionKind vs JoltInstructions<T>: I agree this is the central design question. After digging into it more, I think the confusing part is that we currently blur at least three different concepts:

  • source-level RISC-V instruction kinds decoded from the ELF, including things like DIV/REM, atomics, CSR ops, etc.;
  • expanded Jolt bytecode rows, which are the rows allowed to appear after bytecode expansion and preprocessing;
  • lookup-backed instruction rows, which are the subset of expanded Jolt rows routed through the instruction lookup argument.

  The current JoltInstructions enum does not perfectly represent “instructions provable by Jolt” or “instructions with lookup tables.” For example, it includes DIV/REM, even though those are source instructions that expand into virtual/helper rows before proving. Atomics are decoded and expanded but omitted from JoltInstructions. And LD/SD/system-ish rows can be valid Jolt bytecode while still returning no lookup table because they are constrained elsewhere.

  Long-term, I think the cleanest split is probably something like:

  • RiscvInstructionKind: source program instruction identity;
  • JoltInstructionKind: executable expanded bytecode row identity;
  • LookupInstructionKind or JoltInstructionKind::lookup_kind() -> Option<LookupInstructionKind>: rows participating in lookup tables.

  With that framing, tracer is not purely a RISC-V tracer: it fetches/decodes the original ELF and uses source instructions as the control-flow driver, but in trace mode it expands those source instructions and emits witness rows for the expanded Jolt program. So tracer likely needs to bridge RiscvInstructionKind -> ExpandedInstructionSequence<JoltInstructionKind> -> JoltCycle, rather than being forced wholly into either source-level or Jolt-level types.

  I’d be hesitant to make JoltInstructions<T> replace InstructionKind everywhere until we first decide which phase that enum is supposed to represent. Otherwise we risk baking the current ambiguity into a more generic type. A good next refactor may be to introduce the phase-specific names/types first, then consider whether generic typed enums make sense once the boundaries are clear.

• instruction.expand() / VirtualSequence: expansion is still dispatched centrally from jolt-program::expand. I think this should follow the type split above. A near-term improvement would be to introduce an ExpandedInstructionSequence type in jolt-program to make the output of expanding one source instruction explicit, then later move toward per-instruction expansion traits once the RiscvInstructionKind / JoltInstructionKind boundary is settled.

[quangvdao]

Posted by Cursor assistant (model: GPT-5.4) on behalf of the user (Quang Dao) with approval.

Merged latest origin/main into this branch and resolved the conflict with #1503 (fix: reject unsupported CSRs and restrict LR/SC addresses to RAM region).

The important resolution detail: #1503 fixed the old tracer-local inline-sequence implementations for CSR/LR/SC, but this PR has moved expansion ownership into jolt-program::expand. So I did not reintroduce the tracer-local inline_sequence bodies. Instead:

• kept this PR’s new tracer structure, where tracer calls through Instruction::inline_sequence(...) and that delegates to jolt_program::expand::expand_instruction(...);
• preserved main’s SC.W/SC.D robustness fix by patching the success VirtualAdvice via a search over the expanded sequence, rather than assuming it is at index 0;
• ported the LR.W/LR.D/SC.W/SC.D RAM-region assertion into jolt-program::expand, via a shared prelude that emits LUI(RAM_START_ADDRESS) followed by VirtualAssertLTE(ram_start, rs1);
• left CSR unsupported handling in the new owner: jolt-program already rejects unsupported CSR expansion through ExpansionAllocator::csr_to_virtual_register(...).ok_or(UnsupportedCsr) while main’s tracer decode-side CSR rejection is also preserved from the merge.

Added focused jolt-program tests to make sure all four LR/SC expansions include the RAM-region prelude, and to cover that SC success advice is no longer position-dependent after the prelude is inserted.

Validation run after resolving the merge:

• cargo fmt -q
• cargo nextest run -p jolt-program --cargo-quiet --features image
• cargo nextest run -p tracer to_io_rejected --cargo-quiet
• cargo nextest run -p tracer inline_sequence --cargo-quiet
• cargo check -p tracer --features test-utils -q
• cargo check -p jolt-program --features image -q
• cargo clippy --all --features host -q --all-targets -- -D warnings
• cargo clippy --all --features host,zk -q --all-targets -- -D warnings
• cargo nextest run -p jolt-core muldiv --cargo-quiet --features host
• cargo nextest run -p jolt-core muldiv --cargo-quiet --features host,zk

[quangvdao]

Posted by Cursor assistant (model: GPT-5.4) on behalf of the user (Quang Dao) with approval.

Quick clarification on the relationship between the fixes after merging main/#1503.

There are two independent CSR protections now, and they cover different boundaries:

• Main/fix: reject unsupported CSRs and restrict LR/SC addresses to RAM region #1503 added tracer decode-side validation. tracer::Instruction::decode now checks is_supported_csr(csr_addr) for CSRRW/CSRRS and returns an error before tracing if the CSR is not one of the CSRs Jolt models. That fix is preserved on this branch.

• This PR also keeps expansion-side validation in jolt-program::expand. The CSR expansion code maps the CSR through ExpansionAllocator::csr_to_virtual_register(...) and returns ExpansionError::UnsupportedCsr(csr) if unsupported, including the historical csr == 0 case. This is not intended to replace main’s tracer decode fix; it protects the new canonical expansion API when the input is already a NormalizedInstruction / decoded program row rather than coming through tracer decode.

So the tracer path catches unsupported CSR earlier, while the jolt-program path still rejects unsupported CSR at the expansion boundary. Since this PR makes jolt-program own bytecode expansion, both checks are useful and they are not duplicates of the same boundary.

Separately, main/#1503 also added the LR/SC RAM-region fix: LR.W/LR.D/SC.W/SC.D expansions must assert rs1 >= RAM_START_ADDRESS, preventing LR/SC against the low/device/I/O region. Because this PR moves canonical expansion out of tracer, I ported that invariant into jolt-program::expand as well. The tracer now delegates expansion to jolt-program, so keeping the check only in the old tracer inline sequences would have effectively dropped the main fix.

Net result:

• main’s tracer decode CSR rejection is preserved;
• this PR’s jolt-program CSR expansion rejection is still needed for the new expansion boundary;
• main’s LR/SC RAM-region assertion is ported into jolt-program so it remains active after the expansion ownership move.

[moodlezoup]

This looks good to me. I do think we need to address the InstructionKind vs JoltInstructions issue, but I'm happy to do so in a follow-up

[moodlezoup]

to be more precise, this could be if new_sequence != previous_sequence - 1 right?

[moodlezoup]

fold this into normalized.rs