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,