[erkancamli]

Summary

MISC-MEM (opcode 0b0001111) is the only RV64 opcode whose funct3 neither decoder checks.

tracer's Instruction::decode passes the word straight to FENCE::new(.., validate = true, ..), but FENCE's MASK/MATCH (0x0000707f/0x0000000f) require funct3 == 0, so the debug_assert_eq! inside declare_riscv_instr!'s new fires: decode panics on fence.i (0x0000100f) and on the reserved funct3 >= 2 encodings instead of returning the Err its signature promises. With debug_assertions off the assertion disappears and those words silently decode as a plain FENCE.

jolt-program's image decoder has the matching gap (0b0001111 => SourceInstructionKind::FENCE, no funct3 check), so decode_text_section admits reserved MISC-MEM words into the committed image as no-op FENCE rows, and the tracer then either aborts on them (debug) or no-ops them (release).

FENCE.I belongs to Zifencei, which is outside RV64IMAC_JOLT, and funct3 >= 2 is reserved. Every other arm of both decoders already rejects out of profile and reserved encodings with a typed error (decode_op_imm, decode_amo, decode_system, the branch/load/store tables, and the F/D opcodes 0x07/0x27 that uncompress_rv64_instruction emits for C.FLD/C.FSD). tracer/src/instruction/csrrw.rs records the same contract for CSRs: decode must reject unsupported encodings with a typed error rather than panic.

The reachable path is Cpu::decode_and_cache, which calls Instruction::decode on every fetch: a guest containing fence.i (hand written asm!("fence.i"), an icache sync helper, a __builtin___clear_cache lowering) aborts inside FENCE::new rather than surfacing a decode error.

Changes

• tracer/src/instruction/mod.rs: the MISC-MEM arm matches on funct3 and returns Err("Invalid MISC-MEM funct3") for anything other than FENCE, so no out of profile word reaches FENCE::new.
• crates/jolt-program/src/image/decode.rs: the same gate on the image decoding side, returning ProgramError::MalformedImage("invalid MISC-MEM funct3").
• Tests: tracer/src/instruction/fence.rs asserts every funct3 != 0 MISC-MEM word decodes to an Err (not a panic) and that fence rw, rw still decodes to FENCE; misc_mem_decodes_only_fence covers the same range on the image decoder.

Testing

• Ran tests for modified crates: cargo test -p jolt-program 55 passed, --features image 57 passed, cargo test -p tracer 129 passed (the 12 failures are pre-existing in my environment: they shell out to the jolt CLI to build guests, and fail identically on unmodified main, which is 127 passed / 12 failed).
• cargo clippy -p tracer --all-targets -- -D warnings and cargo clippy -p jolt-program --features image --all-targets -- -D warnings are clean; cargo fmt --check is clean.
• Both new tests were confirmed to fail before the fix and to fail again when the fix alone is reverted.

Security Considerations

No proof soundness change: prover and verifier share one program image and one decoder, so the permissive decode did not let the two sides disagree. It tightens two robustness properties. The program image is the boundary deciding which .text byte patterns are legal RV64 for Jolt, and reserved MISC-MEM words were admitted as no-ops instead of rejected; and Instruction::decode is a public Result returning API reached on every fetch, which aborted through an internal assertion in debug builds. Both now fail the same way, in the same place, in every build profile.

Breaking Changes

Behavioral, not API: an ELF whose .text contains fence.i or a reserved MISC-MEM encoding now fails image decoding with MalformedImage("invalid MISC-MEM funct3") instead of silently becoming a no-op in release builds (and panicking in debug builds). Zifencei is outside RV64IMAC_JOLT, and no RISC-V ELF artifact in the tree contains such a word. If you would rather keep accepting fence.i as an architectural no-op, mapping funct3 = 001 to FENCE explicitly in both decoders is a one line change on top of this; the reserved values should be rejected either way.

[0xAndoroid]

Verified on top of current main: merges clean, and the new tests plus rejects_invalid_encodings_with_exact_messages pass on the merged tree. Two comments, neither blocking.

Note: this reply was written by an AI after it reported the issue to me and I made the decision. If anything here is wrong, reply and I will review it myself.

[erkancamli]

Thanks for checking it on top of main. Rebased on current main (f830b54) and folded both in: the funct3 = 001..111 rejections are now entries in rejects_invalid_encodings_with_exact_messages, one per funct3, and the dedicated test only keeps the fence positive case. The decoder comment, the tracer comment in tracer/src/instruction/mod.rs and the tracer test doc now say funct3 = 010 is Zicbom/Zicboz CBO and only 011..111 is reserved. Decode tests (with image, and with image,field-inline), the tracer fence tests and clippy pass; reverting the decoder arm makes the table test fail on the new entries.

[0xAndoroid]

Re-review of 79ecfae: both earlier threads are addressed and resolved. One doc nit below, not blocking.

Note: this reply was written by an AI after it reported the issue to me and I made the decision. If anything here is wrong, reply and I will review it myself.

[0xAndoroid]

LGTM