From c5e9455cf218b1a8e98cf6b608a91fa8ec1648ad Mon Sep 17 00:00:00 2001 From: Matt Van Horn <455140+mvanhorn@users.noreply.github.com> Date: Sat, 24 Oct 2026 03:24:20 -0700 Subject: [PATCH] fix(error): reject executed instructions that differ from preprocessed bytecode Row conversion now compares the executed instruction with the full preprocessed row, including opcode, normalized operands, address, compression flag, and virtual-sequence metadata. A mismatch returns BytecodeInstructionMismatch with the bytecode PC and expected and actual instructions; missing addresses or expansion positions still return MissingBytecodePc. Both eager tracing and chunk replay perform this validation, and the documentation explains that mutable instruction fetch remains unchanged and chunked execution detects mismatches during replay. Fixes #1952. Refs #1952 --- book/src/how/architecture/bytecode.md | 6 ++ crates/jolt-program/src/execution/error.rs | 8 +- tracer/src/execution_backend.rs | 71 +++++++++++--- tracer/src/trace_row.rs | 106 +++++++++++++++++++-- 4 files changed, 170 insertions(+), 21 deletions(-) diff --git a/book/src/how/architecture/bytecode.md b/book/src/how/architecture/bytecode.md index 5967f53253..da53d2fb53 100644 --- a/book/src/how/architecture/bytecode.md +++ b/book/src/how/architecture/bytecode.md @@ -27,6 +27,12 @@ We start from some ELF file, compiled from the guest program. For each instructi Then, we compute a [Reed-Solomon fingerprint](https://publish.obsidian.md/matteo/3.+Permanent+notes/Reed-Solomon+Fingerprinting) of some subset of the values in the tuple, depending on what $\widetilde{\textsf{rv}}$ claims are being proven. These fingerprints serve as the coefficients of the $\widetilde{\textsf{Val}}$ polynomial for that read-checking instance. +### Trace-time validation + +The tracer's `cycle_to_trace_row` takes `BytecodePreprocessing` and checks each executed instruction against its preprocessed row before returning a trace row. The comparison includes the opcode, normalized operands, address, compression flag, and virtual-sequence metadata; runtime register values, memory observations, and advice are not part of this comparison. A difference returns `TraceError::BytecodeInstructionMismatch` with the bytecode PC and expected/actual instructions. An unavailable address or expansion position returns `MissingBytecodePc`. + +This is a host-side diagnostic in addition to the verifier's bytecode read-checking constraint. The emulator still fetches from mutable memory: self-modifying instructions that differ from the preprocessed ELF image remain unsupported. Eager tracing validates during row conversion; chunked execution validates during replay before returning the affected rows, not during its checkpoint-producing first pass. + ## $\widetilde{\textsf{raf}}$-evaluation $\widetilde{\textsf{raf}}$-evaluation claims for the program counter are folded into the multi-stage read-checking sumcheck rather than being handled separately. There are two $\widetilde{\textsf{raf}}$ claims: diff --git a/crates/jolt-program/src/execution/error.rs b/crates/jolt-program/src/execution/error.rs index 322355decc..bef1bf2ed8 100644 --- a/crates/jolt-program/src/execution/error.rs +++ b/crates/jolt-program/src/execution/error.rs @@ -1,4 +1,4 @@ -use jolt_riscv::{SourceInstructionKind, TraceRowError}; +use jolt_riscv::{JoltInstructionRow, SourceInstructionKind, TraceRowError}; use crate::preprocess::PreprocessingError; @@ -27,4 +27,10 @@ pub enum TraceError { InvalidFieldEvent { cycle: usize }, #[error("RAM minimum address exceeds maximum address")] InvalidRamBounds, + #[error("executed instruction differs from bytecode at PC {pc}: expected {expected:?}, actual {actual:?}")] + BytecodeInstructionMismatch { + pc: u32, + expected: Box, + actual: Box, + }, } diff --git a/tracer/src/execution_backend.rs b/tracer/src/execution_backend.rs index 11385cbe23..75abb09b50 100644 --- a/tracer/src/execution_backend.rs +++ b/tracer/src/execution_backend.rs @@ -5,7 +5,7 @@ use jolt_program::execution::{ ChunkedExecutionBackend, ExecutionBackend, ExecutionDimensions, ExecutionSummary, JoltProgram, MemoryImage, RamAddressBounds, TraceData, TraceError, TraceInputs, TraceOutput, }; -use jolt_program::preprocess::BytecodePCMapper; +use jolt_program::preprocess::BytecodePreprocessing; #[cfg(feature = "field-inline")] use jolt_program::{execution::FieldEvent, field_inline::FieldInlineTraceData}; use jolt_riscv::{CircuitFlags, JoltTraceRow}; @@ -81,7 +81,11 @@ impl ExecutionBackend for TracerBackend { program: &JoltProgram, inputs: TraceInputs, ) -> Result { - let bytecode = BytecodePCMapper::try_new(&program.expanded_bytecode)?; + let bytecode = BytecodePreprocessing::preprocess( + program.expanded_bytecode.clone(), + program.entry_address, + program.profile, + )?; let execution = self.trace_execution(program, inputs)?; let (data, dimensions) = collect_rows(&execution.cycles, &bytecode)?; Ok(TraceOutput::with_dimensions( @@ -104,7 +108,7 @@ struct ConvertedChunk { fn collect_rows( cycles: &[Cycle], - bytecode: &BytecodePCMapper, + bytecode: &BytecodePreprocessing, ) -> Result<(TraceData, ExecutionDimensions), TraceError> { let parallel = cycles.len() > PARALLEL_ROW_CONVERSION_THRESHOLD; let _span = tracing::info_span!( @@ -196,7 +200,7 @@ pub struct TracerChunkCheckpoint { struct WorkerSeed { device: Option, decode: DecodeCache, - bytecode: BytecodePCMapper, + bytecode: BytecodePreprocessing, } /// Boundary checkpoints are captured at chunk-mark crossings, but at most @@ -225,7 +229,11 @@ impl TracerBackend { return Err(TraceError::Backend("chunk_size must be nonzero")); } - let bytecode = BytecodePCMapper::try_new(&program.expanded_bytecode)?; + let bytecode = BytecodePreprocessing::preprocess( + program.expanded_bytecode.clone(), + program.entry_address, + program.profile, + )?; let emulator = crate::create_emulator( program.elf_bytes(), self.elf_path.as_ref(), @@ -397,6 +405,33 @@ mod chunked_tests { (program, inputs) } + #[test] + fn eager_and_replay_reject_bytecode_mismatches() { + let (mut program, inputs) = muldiv_setup(); + let mut backend = TracerBackend::new(); + let eager = backend + .trace(&program, inputs.clone()) + .expect("eager trace failed"); + let executed = eager.trace.rows()[0].instruction(); + let instruction = program + .expanded_bytecode + .iter_mut() + .find(|instruction| **instruction == executed) + .expect("executed instruction in program"); + instruction.operands.imm ^= 1; + assert!(matches!( + backend.trace(&program, inputs.clone()), + Err(TraceError::BytecodeInstructionMismatch { .. }) + )); + let summary = backend + .execute(&program, inputs, 100) + .expect("execute failed"); + assert!(matches!( + backend.replay_chunk(&summary.checkpoints[0]), + Err(TraceError::BytecodeInstructionMismatch { .. }) + )); + } + /// Invariant 3 of `specs/x86-tracer-backend.md` for the reference backend: /// the concatenation of `replay_chunk` outputs equals the eager `trace()` /// row stream for every chunk size, including degenerate ones, regardless @@ -590,7 +625,7 @@ mod tests { )); } #[cfg(feature = "field-inline")] - use jolt_riscv::{FieldInlineOp, FIELD_INLINE_OPCODE}; + use jolt_riscv::{FieldInlineOp, FIELD_INLINE_OPCODE, RV64IMAC_JOLT_FIELD_INLINE}; #[cfg(feature = "field-inline")] fn field_inline_word(op: FieldInlineOp, rd: u8, rs1: u8, rs2_or_imm: u16) -> u32 { @@ -617,8 +652,12 @@ mod tests { false, ) .unwrap(); - let bytecode = - BytecodePCMapper::try_new(&[instruction.try_jolt_instruction_row().unwrap()]).unwrap(); + let bytecode = BytecodePreprocessing::preprocess( + vec![instruction.try_jolt_instruction_row().unwrap()], + 0x8000_0000, + RV64IMAC_JOLT_FIELD_INLINE, + ) + .unwrap(); let positions = [ 0, PARALLEL_ROW_CONVERSION_THRESHOLD - 1, @@ -655,7 +694,7 @@ mod tests { mod conversion_tests { use super::*; use crate::instruction::{ld::LD, sd::SD, RISCVCycle}; - use jolt_riscv::{RamRead, RamWrite}; + use jolt_riscv::{RamRead, RamWrite, RV64IMAC_JOLT}; #[test] fn conversion_preserves_rows_and_reduces_bounds() { @@ -694,7 +733,9 @@ mod conversion_tests { .iter() .map(|cycle| cycle.instruction().try_jolt_instruction_row().unwrap()) .collect::>(); - let bytecode = BytecodePCMapper::try_new(&instructions).unwrap(); + let bytecode = + BytecodePreprocessing::preprocess(instructions, 0x8000_0000, RV64IMAC_JOLT) + .unwrap(); let (data, dimensions) = collect_rows(&cycles, &bytecode).unwrap(); assert_eq!(data.len(), length); assert_eq!(data.rows()[1].ram_address(), read); @@ -718,7 +759,15 @@ mod conversion_tests { .filter(|address| *address != 0) .max() ); - let empty_bytecode = BytecodePCMapper::try_new(&[]).unwrap(); + let mut mismatched_bytecode = bytecode.clone(); + mismatched_bytecode.bytecode[1].operands.imm = 8; + assert!(matches!( + collect_rows(&cycles, &mismatched_bytecode), + Err(TraceError::BytecodeInstructionMismatch { pc: 1, .. }) + )); + let empty_bytecode = + BytecodePreprocessing::preprocess(Vec::new(), 0x8000_0000, RV64IMAC_JOLT) + .unwrap(); assert!(matches!( collect_rows(&cycles, &empty_bytecode), Err(TraceError::MissingBytecodePc { .. }) diff --git a/tracer/src/trace_row.rs b/tracer/src/trace_row.rs index 4408da17fb..c034534cb0 100644 --- a/tracer/src/trace_row.rs +++ b/tracer/src/trace_row.rs @@ -3,28 +3,42 @@ //! Raw cycles retain instruction-specific observations. The unified row //! constructor owns validation and packing after source expansion. -use jolt_program::{execution::TraceError, preprocess::BytecodePCMapper}; +use jolt_program::{execution::TraceError, preprocess::BytecodePreprocessing}; use jolt_riscv::{JoltTraceRow, RegisterRead, RegisterState, RegisterWrite}; use crate::instruction::Cycle; /// Converts a completed final cycle, rejecting source-only instructions and -/// cycles absent from the program's expanded bytecode. +/// cycles absent from or differing from the program's expanded bytecode. pub fn cycle_to_trace_row( cycle: &Cycle, - bytecode: &BytecodePCMapper, + bytecode: &BytecodePreprocessing, ) -> Result { let instruction = cycle .instruction() .try_jolt_instruction_row() .map_err(TraceError::SourceOnlyCycle)?; let pc = bytecode - .get_instruction_pc(&instruction) + .get_pc(&instruction) .ok_or(TraceError::MissingBytecodePc { address: instruction.address as u64, virtual_sequence_remaining: instruction.virtual_sequence_remaining, })?; let bytecode_pc = u32::try_from(pc).map_err(|_| TraceError::BytecodePcTooWide { pc })?; + let expected = bytecode + .bytecode + .get(pc) + .ok_or(TraceError::MissingBytecodePc { + address: instruction.address as u64, + virtual_sequence_remaining: instruction.virtual_sequence_remaining, + })?; + if *expected != instruction { + return Err(TraceError::BytecodeInstructionMismatch { + pc: bytecode_pc, + expected: Box::new(*expected), + actual: Box::new(instruction), + }); + } let registers = RegisterState { rs1: cycle .rs1_read() @@ -56,7 +70,6 @@ mod tests { use crate::emulator::mmu::DRAM_BASE; use crate::emulator::terminal::DummyTerminal; use crate::instruction::{Instruction, RISCVCycle}; - use jolt_program::preprocess::BytecodePreprocessing; use jolt_riscv::{JoltInstructionKind, TraceRowError, RV64IMAC_JOLT}; const TEXT: u64 = 0x8000_0000; @@ -97,6 +110,69 @@ mod tests { cycles } + #[test] + fn executed_instruction_must_match_preprocessed_metadata() { + // Frozen RV64 words: ADD x3,x1,x2 and individual operand/opcode changes. + for (original, changed, rd, rs1, rs2, imm) in [ + (0x0020_81b3, 0x0020_8233, 4, 1, Some(2), 0), + (0x0020_81b3, 0x0022_81b3, 3, 5, Some(2), 0), + (0x0020_81b3, 0x0060_81b3, 3, 1, Some(6), 0), + (0x0020_81b3, 0x4020_81b3, 3, 1, Some(2), 0), + (0x0010_8193, 0x0020_8193, 3, 1, None, 2), + ] { + let original = Instruction::decode(original, TEXT, false).unwrap(); + let expected = original.try_jolt_instruction_row().unwrap(); + let bytecode = + BytecodePreprocessing::preprocess(vec![expected], TEXT, RV64IMAC_JOLT).unwrap(); + let mut cpu = Cpu::new(Box::new(DummyTerminal::default())); + let mut cycles = Vec::new(); + original.trace(&mut cpu, Some(&mut cycles)); + Instruction::decode(changed, TEXT, false) + .unwrap() + .trace(&mut cpu, Some(&mut cycles)); + assert_eq!(cycle_to_trace_row(&cycles[0], &bytecode).unwrap().pc(), 1); + let TraceError::BytecodeInstructionMismatch { + pc, + expected: reported, + actual, + } = cycle_to_trace_row(&cycles[1], &bytecode).unwrap_err() + else { + panic!("expected bytecode mismatch"); + }; + assert_eq!(pc, 1); + assert_eq!(*reported, expected); + assert_eq!(actual.address, TEXT as usize); + assert_eq!(actual.operands.rd, Some(rd)); + assert_eq!(actual.operands.rs1, Some(rs1)); + assert_eq!(actual.operands.rs2, rs2); + assert_eq!(actual.operands.imm, imm); + assert_ne!(*actual, expected); + } + + let bytecode = preprocessing(); + for compressed in [true, false] { + let mut instruction = Instruction::decode(ADD_WORD, TEXT, compressed).unwrap(); + instruction.set_is_first_in_sequence(!compressed); + let mut cpu = Cpu::new(Box::new(DummyTerminal::default())); + let mut cycles = Vec::new(); + instruction.trace(&mut cpu, Some(&mut cycles)); + assert!(matches!( + cycle_to_trace_row(&cycles[0], &bytecode), + Err(TraceError::BytecodeInstructionMismatch { .. }) + )); + if compressed { + let matching = BytecodePreprocessing::preprocess( + vec![instruction.try_jolt_instruction_row().unwrap()], + TEXT, + RV64IMAC_JOLT, + ) + .unwrap(); + assert_eq!(cycle_to_trace_row(&cycles[0], &matching).unwrap().pc(), 1); + } + } + assert_eq!(cycle_to_trace_row(&Cycle::NoOp, &bytecode).unwrap().pc(), 0); + } + #[test] fn source_only_cycles_are_rejected_at_the_phase_boundary() { // DIV never appears in final bytecode; its cycle must be refused. @@ -112,7 +188,7 @@ mod tests { } .into(); - let err = cycle_to_trace_row(&cycle, &preprocessing().pc_map).unwrap_err(); + let err = cycle_to_trace_row(&cycle, &preprocessing()).unwrap_err(); assert!(matches!(err, TraceError::SourceOnlyCycle(_))); } @@ -125,7 +201,7 @@ mod tests { let mut cycles = Vec::new(); stray.trace(&mut cpu, Some(&mut cycles)); - let err = cycle_to_trace_row(&cycles[0], &preprocessing.pc_map).unwrap_err(); + let err = cycle_to_trace_row(&cycles[0], &preprocessing).unwrap_err(); assert!(matches!( err, TraceError::MissingBytecodePc { @@ -133,6 +209,18 @@ mod tests { virtual_sequence_remaining: None, } if address == TEXT + 0x1000 )); + + let mut instruction = program()[0]; + instruction.set_virtual_sequence_remaining(Some(1)); + let mut cycles = Vec::new(); + instruction.trace(&mut cpu, Some(&mut cycles)); + assert!(matches!( + cycle_to_trace_row(&cycles[0], &preprocessing), + Err(TraceError::MissingBytecodePc { + virtual_sequence_remaining: Some(1), + .. + }) + )); } #[test] @@ -144,7 +232,7 @@ mod tests { panic!("expected an LD cycle"); }; ld_cycle.ram_access.value ^= 1; - let err = cycle_to_trace_row(&ld_cycle.into(), &preprocessing.pc_map).unwrap_err(); + let err = cycle_to_trace_row(&ld_cycle.into(), &preprocessing).unwrap_err(); assert!( matches!( &err, @@ -158,7 +246,7 @@ mod tests { panic!("expected an SD cycle"); }; sd_cycle.ram_access.post_value ^= 1; - let err = cycle_to_trace_row(&sd_cycle.into(), &preprocessing.pc_map).unwrap_err(); + let err = cycle_to_trace_row(&sd_cycle.into(), &preprocessing).unwrap_err(); assert!( matches!( &err,