fix(error): reject executed instructions that differ from preprocessed bytecode

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:

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<JoltInstructionRow>,
+        actual: Box<JoltInstructionRow>,
+    },
 }

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<TraceOutput, TraceError> {
-        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<JoltDevice>,
     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::<Vec<_>>();
-                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 { .. })

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<JoltTraceRow, TraceError> {
     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,14 +201,26 @@ 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 {
                 address,
                 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,