op_load should fail even with rd = x0 (VMX-CPU-002)

bitcoin-script-riscv/src/riscv/instruction_mapping.rs

@@ -50,7 +50,7 @@ fn name_or_nop<X: RdZero>(x: &X, name: &str) -> String {
 }
 
 fn name_or_nop_with_micro<X: RdZero>(x: &X, name: &str, micro: u8) -> String {
-    if x.is_rd_zero() {
+    if micro > 1 && x.is_rd_zero() {
         "nop".to_string()
     } else {
         format!("{}_{}", name, micro)

bitcoin-script-riscv/src/riscv/instructions.rs

@@ -793,7 +793,7 @@ pub fn execute_step(
         )),
 
         Lh(x) | Lhu(x) | Lw(x) | Lbu(x) | Lb(x) => {
-            if x.rd() == 0 {
+            if micro > 1 && x.rd() == 0 {
                 Ok(op_nop(stack, trace_read))
             } else {
                 Ok(op_load(

bitcoin-script-riscv/src/riscv/instructions_load.rs

@@ -1,4 +1,4 @@
-use bitcoin_script_stack::stack::{StackTracker, StackVariable};
+use bitcoin_script_stack::{stack::{StackTracker, StackVariable}};
 use bitvmx_cpu_definitions::memory::{MemoryAccessType, MemoryWitness};
 use riscv_decode::Instruction::{self, *};
 
@@ -18,10 +18,10 @@ pub fn op_load(
     base_register_address: u32,
 ) -> STraceStep {
     match micro {
-        0 => op_load_micro_0(instruction, stack, trace_read, micro, base_register_address),
-        1 => op_load_micro_1(instruction, stack, trace_read, micro, base_register_address),
-        2 => op_load_micro_2(instruction, stack, trace_read, micro, base_register_address),
-        3 => op_load_micro_3(instruction, stack, trace_read, micro, base_register_address),
+        0 => op_load_micro_0(instruction, stack, trace_read, base_register_address),
+        1 => op_load_micro_1(instruction, stack, trace_read, base_register_address),
+        2 => op_load_micro_2(instruction, stack, trace_read, base_register_address),
+        3 => op_load_micro_3(instruction, stack, trace_read, base_register_address),
         _ => panic!("Unreachable"),
     }
 }
@@ -30,7 +30,6 @@ pub fn op_load_micro_0(
     instruction: &Instruction,
     stack: &mut StackTracker,
     trace_read: &STraceRead,
-    micro: u8,
     base_register_address: u32,
 ) -> STraceStep {
     let (func3, aligned_if_less_than) = match instruction {
@@ -49,16 +48,6 @@ pub fn op_load_micro_0(
     let (imm, rs1, rd, bit_extension) =
         decode_i_type(stack, &tables, trace_read.opcode, func3, 0x3, None);
 
-    verify_memory_witness(
-        stack,
-        trace_read.mem_witness,
-        MemoryWitness::new(
-            MemoryAccessType::Register,
-            MemoryAccessType::Memory,
-            MemoryAccessType::Register,
-        ),
-    );
-
     stack.move_var(trace_read.micro);
     let expected_micro = stack.number(0);
     stack.equals(trace_read.micro, true, expected_micro, true);
@@ -92,7 +81,6 @@ pub fn op_load_micro_0(
         aligned,
         alignment,
         trace_read,
-        micro,
         base_register_address,
     );
     op_load_micro_0_missaligned(
@@ -103,14 +91,13 @@ pub fn op_load_micro_0(
         aligned,
         alignment,
         trace_read,
-        micro,
         base_register_address,
     );
 
     let ret = stack.end_if(
         if_true,
         if_false,
-        11,
+        12,
         vec![
             (8, "write_add".to_string()),
             (8, "write_value".to_string()),
@@ -132,9 +119,18 @@ pub fn op_load_micro_0_missaligned(
     aligned: StackVariable,
     alignment: StackVariable,
     trace_read: &STraceRead,
-    _micro: u8,
     base_register_address: u32,
 ) -> STraceStep {
+    verify_memory_witness(
+        stack,
+        trace_read.mem_witness,
+        MemoryWitness::new(
+            MemoryAccessType::Register,
+            MemoryAccessType::Memory,
+            MemoryAccessType::Register,
+        ),
+    );
+
     let (nibs, max_extra, prepad, unsigned) = match instruction {
         Lb(_) => (2, 0, 6, false),
         Lh(_) => (4, 2, 4, false),
@@ -193,7 +189,6 @@ pub fn op_load_micro_0_aligned(
     aligned: StackVariable,
     alignment: StackVariable,
     trace_read: &STraceRead,
-    _micro: u8,
     base_register_address: u32,
 ) -> STraceStep {
     let (nibs, max_extra, prepad, unsigned) = match instruction {
@@ -205,23 +200,52 @@ pub fn op_load_micro_0_aligned(
         _ => panic!("Unreachable"),
     };
 
-    //save the alignment
-    stack.to_altstack();
-    //assert read_2_add with expected memory read
+    stack.move_var(trace_read.mem_witness);
+    stack.move_var(trace_read.read_2_value);
 
+    //assert read_2_add with expected memory read
     stack.equals(trace_read.read_2_add, true, aligned, true);
 
-    //generate the write address
-    let write_addr = number_u32_partial(stack, base_register_address, 6);
-    stack.move_var(rd);
-    stack.join(write_addr);
-    stack.rename(write_addr, "write_add");
+    let register_zero = stack.byte(0);
+    stack.equality(register_zero, true, rd, false, true, false);
+    let (mut if_is_register_zero, mut if_false) = stack.open_if();
+
+    verify_memory_witness(
+        &mut if_is_register_zero,
+        trace_read.mem_witness,
+        MemoryWitness::new(
+            MemoryAccessType::Register,
+            MemoryAccessType::Memory,
+            MemoryAccessType::Unused,
+        ),
+    );
 
+    if_is_register_zero.drop(trace_read.read_2_value);
+    if_is_register_zero.drop(alignment);
+    if_is_register_zero.drop(rd);
+    if_is_register_zero.number_u32(0);
+    if_is_register_zero.number_u32(0);
+
+    verify_memory_witness(
+        &mut if_false,
+        trace_read.mem_witness,
+        MemoryWitness::new(
+            MemoryAccessType::Register,
+            MemoryAccessType::Memory,
+            MemoryAccessType::Register,
+        ),
+    );
+
+    //generate the write address
+    let write_addr = number_u32_partial(&mut if_false, base_register_address, 6);
+    if_false.move_var(rd);
+    if_false.join(write_addr);
+
     //calculate the byte to be stored (with proper bit extension)
-    stack.move_var(trace_read.read_2_value);
-    stack.from_altstack(); //restore alignment
-    let write_value = choose_nibbles(
-        stack,
+    if_false.move_var(trace_read.read_2_value);
+    if_false.move_var(alignment); //restore alignment
+    choose_nibbles(
+        &mut if_false,
         trace_read.read_2_value,
         alignment,
         nibs,
@@ -230,13 +254,23 @@ pub fn op_load_micro_0_aligned(
         unsigned,
         0,
     );
-    stack.rename(write_value, "write_value");
+
+    let ret = stack.end_if(
+        if_is_register_zero,
+        if_false,
+        4,
+        vec![
+            (8, "write_add".to_string()),
+            (8, "write_value".to_string()),
+        ],
+        0,
+    );
 
     let write_pc = pc_next(stack, tables, trace_read.program_counter);
     let micro = stack.number(0);
     stack.rename(micro, "write_micro");
 
-    let trace = STraceStep::new(write_addr, write_value, write_pc, micro);
+    let trace = STraceStep::new(ret[0], ret[1], write_pc, micro);
     trace.to_altstack(stack);
     tables.drop(stack);
     trace.from_altstack(stack);
@@ -248,7 +282,6 @@ pub fn op_load_micro_1(
     instruction: &Instruction,
     stack: &mut StackTracker,
     trace_read: &STraceRead,
-    _micro: u8,
     base_register_address: u32,
 ) -> STraceStep {
     let (func3, nibs, max_extra, pre_pad, post, unsigned) = match instruction {
@@ -336,7 +369,6 @@ pub fn op_load_micro_2(
     instruction: &Instruction,
     stack: &mut StackTracker,
     trace_read: &STraceRead,
-    _micro: u8,
     base_register_address: u32,
 ) -> STraceStep {
     let func3 = match instruction {
@@ -398,7 +430,6 @@ pub fn op_load_micro_3(
     instruction: &Instruction,
     stack: &mut StackTracker,
     trace_read: &STraceRead,
-    _micro: u8,
     base_register_address: u32,
 ) -> STraceStep {
     let func3 = match instruction {

emulator/src/decision/challenge.rs

@@ -1357,4 +1357,76 @@ mod tests {
             ForceChallenge::No,
         );
     }
+
+    #[test]
+    fn test_challenge_load_to_x0_aligned() {
+        init_trace();
+
+        let fail_execute = FailExecute {
+            step: 9,
+            fake_trace: TraceRWStep::new(
+                9,
+                TraceRead::new(4026531900, 2852134912, 8),
+                TraceRead::new(2852134912, 0, LAST_STEP_INIT),
+                TraceReadPC::new(ProgramCounter::new(2147483796, 0), 499715),
+                TraceStep::new(TraceWrite::default(), ProgramCounter::new(2147483800, 0)),
+                None,
+                MemoryWitness::new(
+                    MemoryAccessType::Register,
+                    MemoryAccessType::Memory,
+                    MemoryAccessType::Unused,
+                ),
+            ),
+        };
+
+        let fail_execute = Some(FailConfiguration::new_fail_execute(fail_execute));
+
+        test_challenge_aux(
+            "audit_02_aligned",
+            "audit_02_aligned.yaml",
+            0,
+            false,
+            fail_execute,
+            None,
+            true,
+            ForceCondition::No,
+            ForceChallenge::No,
+        );
+    }
+
+    #[test]
+    fn test_challenge_load_to_x0_unaligned() {
+        init_trace();
+
+        let fail_execute = FailExecute {
+            step: 10,
+            fake_trace: TraceRWStep::new(
+                10,
+                TraceRead::new(4026531900, 2852134912, 8),
+                TraceRead::new(2852134912, 0, LAST_STEP_INIT),
+                TraceReadPC::new(ProgramCounter::new(2147483796, 1), 4292321283),
+                TraceStep::new(TraceWrite::new(4026531972, 0), ProgramCounter::new(2147483796, 2)),
+                None,
+                MemoryWitness::new(
+                    MemoryAccessType::Register,
+                    MemoryAccessType::Memory,
+                    MemoryAccessType::Register,
+                ),
+            ),
+        };
+
+        let fail_execute = Some(FailConfiguration::new_fail_execute(fail_execute));
+
+        test_challenge_aux(
+            "audit_02_unaligned",
+            "audit_02_unaligned.yaml",
+            0,
+            false,
+            fail_execute,
+            None,
+            true,
+            ForceCondition::No,
+            ForceChallenge::No,
+        );
+    }
 }

emulator/src/executor/fetcher.rs

@@ -980,7 +980,9 @@ pub fn op_load(
     x: &IType,
     program: &mut Program,
 ) -> Result<(TraceRead, TraceRead, TraceWrite, MemoryWitness), ExecutionResult> {
-    if x.rd() == REGISTER_ZERO as u32 {
+    let micro = program.pc.get_micro();
+
+    if micro > 1 && x.rd() == REGISTER_ZERO as u32 {
         program.pc.next_address();
         return Ok((
             TraceRead::default(),
@@ -990,8 +992,6 @@ pub fn op_load(
         ));
     }
 
-    let micro = program.pc.get_micro();
-
     let (read_1, mut src_mem, alignment) = get_src_mem(&program.registers, x);
     let (_word, _half, _byte, reads) = get_type_and_read_from_instruction(instruction, alignment);
 
@@ -1029,6 +1029,18 @@ pub fn op_load(
 
             let write_1 = if reads == 1 {
                 program.pc.next_address();
+                if x.rd() == REGISTER_ZERO as u32 {
+                    return Ok((
+                        read_1,
+                        read_2,
+                        TraceWrite::default(),
+                        MemoryWitness::new(
+                            MemoryAccessType::Register,
+                            MemoryAccessType::Memory,
+                            MemoryAccessType::Unused,
+                        ),
+                    ));
+                }
                 program.registers.set(x.rd(), shifted, program.step);
                 program.registers.to_trace_write(x.rd())
             } else {