From a82a9597cf44496798c7bf5e93d4e349e8d8959b Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 2 Jul 2025 14:30:36 -0300
Subject: [PATCH 01/34] Add challenges for uninitialized and initialized non
 modified data reads

---
 bitcoin-script-riscv/src/riscv/challenges.rs  | 392 ++++++++++++------
 .../src/riscv/script_utils.rs                 | 209 ++++++++--
 definitions/src/challenge.rs                  |   7 +-
 definitions/src/lib.rs                        |   2 +-
 definitions/src/memory.rs                     |  15 +
 docker-riscv32                                |   2 +-
 emulator/src/decision/challenge.rs            | 235 +++++++----
 emulator/src/executor/fetcher.rs              |   2 +-
 emulator/src/loader/program.rs                | 213 ++++------
 9 files changed, 690 insertions(+), 387 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index e2c44c7..a5dce64 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -3,16 +3,15 @@ use bitcoin_script_stack::stack::{StackTracker, StackVariable};
 use bitvmx_cpu_definitions::{
     challenge::ChallengeType,
     constants::LAST_STEP_INIT,
-    memory::{MemoryAccessType, SectionDefinition},
+    memory::{Chunk, MemoryAccessType, SectionDefinition},
     trace::{generate_initial_step_hash, hashvec_to_string},
 };
 
 use crate::riscv::{
     memory_alignment::{is_aligned, load_lower_half_nibble_table, load_upper_half_nibble_table},
-    operations::sub,
     script_utils::{
-        address_not_in_sections, is_equal_to, is_lower_than, nibbles_to_number, shift_number,
-        witness_equals, StackTables, WordTable,
+        address_in_range, address_in_sections, address_not_in_sections, get_chosen_read,
+        verify_wrong_chunk_value, witness_equals, StackTables,
     },
 };
 
@@ -66,46 +65,6 @@ pub fn input_challenge(stack: &mut StackTracker, address: u32) {
     stack.op_verify();
 }
 
-// One rom value equivocation challenge
-// [WOTS_PROVER_READ_ADD_1|WOTS_PROVER_READ_VALUE_1|WOTS_PROVER_LAST_STEP_1|WOTS_PROVER_READ_ADD_2|WOTS_PROVER_READ_VALUE_2|WOTS_PROVER_LAST_STEP_2]
-// If STEP_1 == INIT && ADD_1 == const_address && VALUE_1 != const_value || STEP_2 == INIT && ADD_2 == const_address && VALUE_2 != const_value  => verifier wins
-pub fn rom_challenge(stack: &mut StackTracker, address: u32, value: u32) {
-    assert_ne!(address, 0x0000_0000);
-    stack.clear_definitions();
-    let add_1 = stack.define(8, "prover_read_add_1");
-    let read_1 = stack.define(8, "prover_read_value_1");
-    let prover_step_1 = stack.define(16, "prover_last_step_1");
-
-    let add_2 = stack.define(8, "prover_read_add_2");
-    let read_2 = stack.define(8, "prover_read_value_2");
-    let prover_step_2 = stack.define(16, "prover_last_step_2");
-
-    //compares agaisnt read_2
-    let init = stack.number_u64(LAST_STEP_INIT);
-    stack.equality(prover_step_2, true, init, true, true, false);
-    let const_value = stack.number_u32(value);
-    stack.equality(read_2, true, const_value, true, false, false);
-    let const_address = stack.number_u32(address);
-    stack.equality(add_2, true, const_address, true, true, false);
-    stack.op_booland();
-    stack.op_booland();
-
-    //compares agaisnt read_1
-    let init = stack.number_u64(LAST_STEP_INIT);
-    stack.equality(prover_step_1, true, init, true, true, false);
-    let const_value = stack.number_u32(value);
-    stack.equality(read_1, true, const_value, true, false, false);
-    let const_address = stack.number_u32(address);
-    stack.equality(add_1, true, const_address, true, true, false);
-
-    stack.op_booland();
-    stack.op_booland();
-
-    //one of the two needs to be right
-    stack.op_boolor();
-    stack.op_verify();
-}
-
 // If the prover executes step = 1 and entry_point != valid entry point
 // the verifier can execute this equivocation and win the challenge
 // [WOTS_PROVER_TRACE_PC:8 | WOTS_PROVER_TRACE_MICRO:2 | WOTS_PROVER_TRACE_STEP:16]
@@ -418,43 +377,59 @@ pub fn addresses_sections_challenge(
     stack.drop(memory_witness);
 }
 
-pub fn opcode_challenge(stack: &mut StackTracker, chunk_base: u32, opcodes_chunk: &Vec<u32>) {
+pub fn opcode_challenge(stack: &mut StackTracker, chunk: &Chunk) {
     stack.clear_definitions();
 
     let pc = stack.define(8, "prover_pc");
     let opcode = stack.define(8, "prover_opcode");
     let tables = StackTables::new(stack, true, false, 0, 0, 0);
 
-    let start = stack.number_u32(chunk_base);
-    let end = stack.number_u32(chunk_base + 4 * opcodes_chunk.len() as u32);
+    address_in_range(stack, &chunk.range(), &pc);
+    stack.op_verify();
 
-    let start_copy = stack.copy_var(start);
-    let pc_copy = stack.copy_var(pc);
-    is_equal_to(stack, &start_copy, &pc_copy);
-    is_lower_than(stack, start_copy, pc_copy, true);
-    stack.op_boolor();
+    verify_wrong_chunk_value(stack, &tables, chunk, pc, opcode);
+    tables.drop(stack);
+}
 
-    let pc_copy = stack.copy_var(pc);
-    is_lower_than(stack, pc_copy, end, true);
-    stack.op_booland();
+pub fn initialized_challenge(stack: &mut StackTracker, chunk: &Chunk) {
+    get_chosen_read(stack);
+
+    let read_addr = stack.define(8, "prover_read_addr");
+    let read_value = stack.define(8, "prover_read_value");
+    let read_step = stack.define(16, "prover_read_step");
 
+    address_in_range(stack, &chunk.range(), &read_addr);
     stack.op_verify();
 
-    let opcodes_table = WordTable::new(stack, opcodes_chunk.clone());
+    let init = stack.number_u64(LAST_STEP_INIT);
+    stack.equality(read_step, true, init, true, true, true);
 
-    let to_shift = stack.number(2);
-    let opcode_offset = sub(stack, &tables, pc, start);
-    let opcode_index = shift_number(stack, to_shift, opcode_offset, true, false);
+    let tables = &StackTables::new(stack, true, false, 0, 0, 0);
+    verify_wrong_chunk_value(stack, tables, chunk, read_addr, read_value);
 
-    let index_nibbles = stack.explode(opcode_index);
-    nibbles_to_number(stack, index_nibbles);
+    tables.drop(stack);
+}
 
-    let real_opcode = opcodes_table.peek(stack);
+pub fn uninitialized_challenge(
+    stack: &mut StackTracker,
+    uninitialized_sections: &SectionDefinition,
+) {
+    get_chosen_read(stack);
 
-    stack.equality(real_opcode, true, opcode, true, false, true);
+    let read_addr = stack.define(8, "prover_read_addr");
+    let read_value = stack.define(8, "prover_read_value");
+    let read_step = stack.define(16, "prover_read_step");
 
-    opcodes_table.drop(stack);
-    tables.drop(stack);
+    address_in_sections(stack, &read_addr, uninitialized_sections);
+    stack.op_verify();
+
+    let init = stack.number_u64(LAST_STEP_INIT);
+    stack.equality(read_step, true, init, true, true, true);
+
+    let zero = stack.number_u32(0);
+    stack.equality(read_value, true, zero, true, false, true);
+
+    stack.drop(read_addr);
 }
 
 //TODO: memory section challenge
@@ -496,28 +471,52 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
             stack.number_u32(prover_pc_read.pc.get_address());
             stack.byte(prover_pc_read.pc.get_micro());
 
-            stack.hexstr_as_nibbles(&prover_step_hash);
+            stack.hexstr_as_nibbles(prover_step_hash);
 
             program_counter_challenge(&mut stack);
         }
+        ChallengeType::Opcode(pc_read, _, chunk) => {
+            stack.number_u32(pc_read.pc.get_address());
+            stack.number_u32(pc_read.opcode);
+            opcode_challenge(&mut stack, chunk.as_ref().unwrap());
+        }
         ChallengeType::InputData(read_1, read_2, address, input_for_address) => {
             stack.number_u32(*input_for_address); //TODO: this should make input_wots[address]
             stack.number_u32(read_1.address);
             stack.number_u32(read_1.value);
             stack.number_u64(read_1.last_step);
+
             stack.number_u32(read_2.address);
             stack.number_u32(read_2.value);
             stack.number_u64(read_2.last_step);
+
             input_challenge(&mut stack, *address);
         }
-        ChallengeType::RomData(read_1, read_2 ,address, input_for_address ) => {
+        ChallengeType::InitializedData(read_1, read_2, read_selector, _, chunk) => {
+            stack.number_u32(read_1.address);
+            stack.number_u32(read_1.value);
+            stack.number_u64(read_1.last_step);
+
+            stack.number_u32(read_2.address);
+            stack.number_u32(read_2.value);
+            stack.number_u64(read_2.last_step);
+
+            stack.byte(*read_selector);
+
+            initialized_challenge(&mut stack, chunk.as_ref().unwrap());
+        }
+        ChallengeType::UninitializedData(read_1, read_2, read_selector, uninitialized_sections) => {
             stack.number_u32(read_1.address);
             stack.number_u32(read_1.value);
             stack.number_u64(read_1.last_step);
+
             stack.number_u32(read_2.address);
             stack.number_u32(read_2.value);
             stack.number_u64(read_2.last_step);
-            rom_challenge(&mut stack, *address, *input_for_address);
+
+            stack.byte(*read_selector);
+
+            uninitialized_challenge(&mut stack, uninitialized_sections.as_ref().unwrap());
         }
         ChallengeType::AddressesSections(
             read_1,
@@ -544,11 +543,6 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
                 code_sections.as_ref().unwrap(),
             );
         }
-        ChallengeType::Opcode(pc_read, _, chunk_base, opcodes_chunk) => {
-            stack.number_u32(pc_read.pc.get_address());
-            stack.number_u32(pc_read.opcode);
-            opcode_challenge(&mut stack, chunk_base.unwrap(), opcodes_chunk.as_ref().unwrap());
-        }
         _ => {
             return false;
         }
@@ -785,55 +779,6 @@ mod tests {
         ));
     }
 
-    fn test_rom_aux(read_1: &TraceRead, read_2: &TraceRead, rom_add: u32, rom_value: u32) -> bool {
-        let mut stack = StackTracker::new();
-
-        stack.number_u32(read_1.address);
-        stack.number_u32(read_1.value);
-        stack.number_u64(read_1.last_step);
-        stack.number_u32(read_2.address);
-        stack.number_u32(read_2.value);
-        stack.number_u64(read_2.last_step);
-
-        rom_challenge(&mut stack, rom_add, rom_value);
-
-        stack.op_true();
-        stack.run().success
-    }
-
-    #[test]
-    fn test_rom() {
-        //can't challenge not init state
-        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, 1);
-        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, 2);
-        assert!(!test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x0000_0000));
-
-        //can't challenge if value is right
-        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        assert!(!test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_5678));
-
-        //can't challenge if address is different
-        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        assert!(!test_rom_aux(&read_1, &read_2, 0x0000_0003, 0x1234_0000));
-
-        //challenge is valid if the address is the same but the value differs in both
-        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        assert!(test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_0000));
-
-        //challenge is valid if the address is the same but the value differs in read_1
-        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        let read_2 = TraceRead::new(0x0000_0005, 0x1234_0000, LAST_STEP_INIT);
-        assert!(test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_0000));
-
-        //challenge is valid if the address is the same but the value differs in read_2
-        let read_1 = TraceRead::new(0x0000_0005, 0x1234_0000, LAST_STEP_INIT);
-        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
-        assert!(test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_0000));
-    }
-
     fn test_input_aux(
         read_1: &TraceRead,
         read_2: &TraceRead,
@@ -1246,7 +1191,13 @@ mod tests {
         stack.number_u32(pc);
         stack.number_u32(opcode);
 
-        opcode_challenge(&mut stack, chunk_base, opcodes_chunk);
+        opcode_challenge(
+            &mut stack,
+            &Chunk {
+                base_addr: chunk_base,
+                data: opcodes_chunk.to_vec(),
+            },
+        );
 
         stack.op_true();
         let r = stack.run();
@@ -1268,4 +1219,199 @@ mod tests {
         assert!(test_opcode_aux(0xab00_0000, 8888, 0xab00_0000, opcodes));
         assert!(test_opcode_aux(0xab00_0004, 8888, 0xab00_0000, opcodes));
     }
+
+    fn test_initialized_aux(
+        read_1: &TraceRead,
+        read_2: &TraceRead,
+        read_selector: u8,
+        chunk: &Chunk,
+    ) -> bool {
+        let mut stack = StackTracker::new();
+
+        stack.number_u32(read_1.address);
+        stack.number_u32(read_1.value);
+        stack.number_u64(read_1.last_step);
+
+        stack.number_u32(read_2.address);
+        stack.number_u32(read_2.value);
+        stack.number_u64(read_2.last_step);
+
+        stack.byte(read_selector);
+
+        initialized_challenge(&mut stack, chunk);
+
+        stack.op_true();
+        stack.run().success
+    }
+
+    #[test]
+    fn test_initialized() {
+        let chunk = &Chunk {
+            base_addr: 0x1000_0000,
+            data: vec![0x1111_1111, 0x2222_2222, 0x3333_3333, 0x4444_4444],
+        };
+
+        //can't challenge not init state
+        let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, 1);
+        let read_2 = TraceRead::new(0x1000_0004, 0x1234_5678, 2);
+        assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
+        assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
+
+        //can't challenge if value is right
+        let read_1 = TraceRead::new(0x1000_0000, 0x1111_1111, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x1000_0004, 0x2222_2222, LAST_STEP_INIT);
+        assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
+        assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
+
+        //can't challenge if address is outside chunk
+        let read_1 = TraceRead::new(0x0000_0004, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x0000_0008, 0x1234_5678, LAST_STEP_INIT);
+        assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
+        assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
+
+        //challenge is valid if the address is the same but the value differs in both
+        let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x1000_0004, 0x1234_5678, LAST_STEP_INIT);
+        assert!(test_initialized_aux(&read_1, &read_2, 1, chunk));
+        assert!(test_initialized_aux(&read_1, &read_2, 2, chunk));
+
+        //challenge is valid if the address is the same but the value differs in read_1 and uses correct selector
+        let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x1000_0004, 0x2222_2222, LAST_STEP_INIT);
+        assert!(test_initialized_aux(&read_1, &read_2, 1, chunk));
+        assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
+
+        //challenge is valid if the address is the same but the value differs in read_2 and uses correct selector
+        let read_1 = TraceRead::new(0x1000_0000, 0x1111_1111, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x1000_0004, 0x1234_5678, LAST_STEP_INIT);
+        assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
+        assert!(test_initialized_aux(&read_1, &read_2, 2, chunk));
+    }
+
+    fn test_uninitialized_aux(
+        read_1: &TraceRead,
+        read_2: &TraceRead,
+        read_selector: u8,
+        sections: &SectionDefinition,
+    ) -> bool {
+        let mut stack = StackTracker::new();
+
+        stack.number_u32(read_1.address);
+        stack.number_u32(read_1.value);
+        stack.number_u64(read_1.last_step);
+
+        stack.number_u32(read_2.address);
+        stack.number_u32(read_2.value);
+        stack.number_u64(read_2.last_step);
+
+        stack.byte(read_selector);
+
+        uninitialized_challenge(&mut stack, sections);
+
+        stack.op_true();
+        stack.run().success
+    }
+
+    #[test]
+    fn test_uninitialized() {
+        let uninitialized_sections = &SectionDefinition {
+            ranges: vec![(0x1000_0000, 0x2000_0000), (0xA000_0000, 0xB000_0000)],
+        };
+
+        //can't challenge not init state
+        let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, 1);
+        let read_2 = TraceRead::new(0xA000_0000, 0x1234_5678, 2);
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            1,
+            uninitialized_sections
+        ));
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            2,
+            uninitialized_sections
+        ));
+
+        //can't challenge if value is right
+        let read_1 = TraceRead::new(0x1000_0000, 0, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0xA000_0000, 0, LAST_STEP_INIT);
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            1,
+            uninitialized_sections
+        ));
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            2,
+            uninitialized_sections
+        ));
+
+        //can't challenge if address is outside uninitialized sections
+        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            1,
+            uninitialized_sections
+        ));
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            2,
+            uninitialized_sections
+        ));
+
+        //challenge is valid if the address is the same but the value differs in both
+        let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0xA000_0000, 0x1234_5678, LAST_STEP_INIT);
+        assert!(test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            1,
+            uninitialized_sections
+        ));
+        assert!(test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            2,
+            uninitialized_sections
+        ));
+
+        //challenge is valid if the address is the same but the value differs in read_1 and uses correct selector
+        let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0xA000_0000, 0, LAST_STEP_INIT);
+        assert!(test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            1,
+            uninitialized_sections
+        ));
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            2,
+            uninitialized_sections
+        ));
+
+        //challenge is valid if the address is the same but the value differs in read_2 and uses correct selector
+        let read_1 = TraceRead::new(0x1000_0000, 0, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0xA000_0000, 0x1234_5678, LAST_STEP_INIT);
+        assert!(!test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            1,
+            uninitialized_sections
+        ));
+        assert!(test_uninitialized_aux(
+            &read_1,
+            &read_2,
+            2,
+            uninitialized_sections
+        ));
+    }
 }
diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs
index 4f5e1b6..2149f49 100644
--- a/bitcoin-script-riscv/src/riscv/script_utils.rs
+++ b/bitcoin-script-riscv/src/riscv/script_utils.rs
@@ -3,7 +3,7 @@ use bitcoin_script_stack::stack::{StackTracker, StackVariable};
 pub use bitcoin_script::{define_pushable, script};
 define_pushable!();
 pub use bitcoin::ScriptBuf as Script;
-use bitvmx_cpu_definitions::memory::{MemoryAccessType, SectionDefinition};
+use bitvmx_cpu_definitions::memory::{Chunk, MemoryAccessType, SectionDefinition};
 
 use super::operations::{sort_nibbles, sub};
 
@@ -1418,32 +1418,105 @@ pub fn witness_equals(
     stack.op_equal();
 }
 
-pub fn address_not_in_sections(
+pub fn verify_wrong_chunk_value(
     stack: &mut StackTracker,
-    address: &StackVariable,
-    sections: &SectionDefinition,
+    tables: &StackTables,
+    chunk: &Chunk,
+    address: StackVariable,
+    value: StackVariable,
 ) {
-    for range in &sections.ranges {
-        assert!(range.0 + 3 <= range.1);
-        let section_start = stack.number_u32(range.0);
-        let address_copy: StackVariable = stack.copy_var(*address);
+    let chunk_table = WordTable::new(stack, chunk.data.clone());
 
-        is_lower_than(stack, address_copy, section_start, true);
+    let base_addr = stack.number_u32(chunk.base_addr);
+    let offset = sub(stack, &tables, address, base_addr);
 
-        // when we do a read on an address, we also read the 3 addresses after
-        let section_end = stack.number_u32(range.1 - 3);
-        let address_copy = stack.copy_var(*address);
+    let to_shift = stack.number(2);
+    let index = shift_number(stack, to_shift, offset, true, false);
 
-        is_lower_than(stack, section_end, address_copy, true);
+    let index_nibbles = stack.explode(index);
+    nibbles_to_number(stack, index_nibbles);
 
-        stack.op_boolor();
+    let real_opcode = chunk_table.peek(stack);
+
+    stack.equality(real_opcode, true, value, true, false, true);
+    chunk_table.drop(stack);
+}
+
+pub fn get_chosen_read(stack: &mut StackTracker) {
+    stack.clear_definitions();
+
+    let read_1_addr = stack.define(8, "prover_read_1_addr");
+    let read_1_value = stack.define(8, "prover_read_1_value");
+    let read_1_step = stack.define(16, "prover_read_1_step");
+
+    let read_2_addr = stack.define(8, "prover_read_2_addr");
+    let read_2_value = stack.define(8, "prover_read_2_value");
+    let read_2_step = stack.define(16, "prover_read_2_step");
+
+    let read_selector = stack.define(2, "read_selector");
+    let one = stack.byte(1);
+
+    stack.equality(read_selector, true, one, true, true, false);
+
+    let (mut challenge_read_1, mut challenge_read_2) = stack.open_if();
+
+    challenge_read_1.drop(read_2_step);
+    challenge_read_1.drop(read_2_value);
+    challenge_read_1.drop(read_2_addr);
+
+    challenge_read_2.move_var(read_1_addr);
+    challenge_read_2.drop(read_1_addr);
+
+    challenge_read_2.move_var(read_1_value);
+    challenge_read_2.drop(read_1_value);
+
+    challenge_read_2.move_var(read_1_step);
+    challenge_read_2.drop(read_1_step);
+
+    stack.end_if(challenge_read_1, challenge_read_2, 3, vec![], 0);
+    stack.clear_definitions();
+}
+
+pub fn address_in_range(stack: &mut StackTracker, range: &(u32, u32), address: &StackVariable) {
+    let start = stack.number_u32(range.0);
+    let end = stack.number_u32(range.1);
+    let address_copy = stack.copy_var(*address);
+
+    is_equal_to(stack, &start, &address_copy);
+    is_lower_than(stack, start, address_copy, true);
+    stack.op_boolor();
+
+    let address_copy = stack.copy_var(*address);
+    is_equal_to(stack, &end, &address_copy);
+    is_lower_than(stack, address_copy, end, true);
+    stack.op_boolor();
+
+    stack.op_booland();
+}
+
+pub fn address_in_sections(
+    stack: &mut StackTracker,
+    address: &StackVariable,
+    sections: &SectionDefinition,
+) {
+    for range in &sections.ranges {
+        address_in_range(stack, range, address);
     }
 
     for _ in 0..sections.ranges.len() - 1 {
-        stack.op_booland();
+        stack.op_boolor();
     }
 }
 
+pub fn address_not_in_sections(
+    stack: &mut StackTracker,
+    address: &StackVariable,
+    sections: &SectionDefinition,
+) {
+    address_in_sections(stack, address, sections);
+    stack.op_not();
+}
+
 pub fn nibbles_to_number(stack: &mut StackTracker, nibbles: Vec<StackVariable>) -> StackVariable {
     let mut result = stack.number(0);
 
@@ -1790,12 +1863,12 @@ mod tests {
         test_witness_equals_aux(memory_witness, 1, false, MemoryAccessType::Unused);
     }
 
-    fn test_address_not_in_sections_aux(address: u32, sections: &SectionDefinition) -> bool {
+    fn test_address_in_range_aux(address: u32, range: &(u32, u32)) -> bool {
         let mut stack = StackTracker::new();
 
         let address = stack.number_u32(address);
 
-        address_not_in_sections(&mut stack, &address, sections);
+        address_in_range(&mut stack, range, &address);
 
         stack.op_verify();
         stack.drop(address);
@@ -1804,27 +1877,18 @@ mod tests {
     }
 
     #[test]
-    fn test_address_not_in_sections() {
-        const START_1: u32 = 0x0000_00f0;
-        const START_2: u32 = 0x000f_00f0;
-        const END_1: u32 = 0x0000_f003;
-        const END_2: u32 = 0x000f_f003;
-
-        let sections = &SectionDefinition {
-            ranges: vec![(START_1, END_1), (START_2, END_2)],
-        };
+    fn test_address_in_range() {
+        const START: u32 = 0x0000_00f0;
+        const END: u32 = 0x0000_f003;
 
-        assert!(!test_address_not_in_sections_aux(START_1, sections));
-        assert!(!test_address_not_in_sections_aux(0x0000_0f00, sections));
-        assert!(!test_address_not_in_sections_aux(END_1 - 3, sections));
-        assert!(!test_address_not_in_sections_aux(START_2, sections));
-        assert!(!test_address_not_in_sections_aux(0x000f_0f00, sections));
-        assert!(!test_address_not_in_sections_aux(END_2 - 3, sections));
+        let range = &(START, END);
 
-        assert!(test_address_not_in_sections_aux(START_1 - 1, sections));
-        assert!(test_address_not_in_sections_aux(END_1 - 2, sections));
-        assert!(test_address_not_in_sections_aux(START_2 - 1, sections));
-        assert!(test_address_not_in_sections_aux(END_2 - 2, sections));
+        assert!(test_address_in_range_aux(START, range));
+        assert!(test_address_in_range_aux((START + END) / 2, range));
+        assert!(test_address_in_range_aux(END, range));
+
+        assert!(!test_address_in_range_aux(START - 1, range));
+        assert!(!test_address_in_range_aux(END + 1, range));
     }
 
     #[test]
@@ -1839,4 +1903,77 @@ mod tests {
         stack.op_true();
         assert!(stack.run().success);
     }
+
+    fn test_get_chosen_read_aux(read_selector: u8) {
+        let mut stack = StackTracker::new();
+
+        stack.number_u32(0x1111_1111);
+        stack.number_u32(0x2222_2222);
+        stack.number_u64(0x3333_3333_3333_3333);
+
+        stack.number_u32(0x4444_4444);
+        stack.number_u32(0x5555_5555);
+        stack.number_u64(0x6666_6666_6666_6666);
+
+        stack.byte(read_selector);
+
+        get_chosen_read(&mut stack);
+
+        let address = stack.define(8, "address");
+        let value = stack.define(8, "value");
+        let step = stack.define(16, "step");
+
+        let expected_address;
+        let expected_value;
+        let expected_step;
+
+        if read_selector == 1 {
+            expected_address = stack.number_u32(0x1111_1111);
+            expected_value = stack.number_u32(0x2222_2222);
+            expected_step = stack.number_u64(0x3333_3333_3333_3333);
+        } else {
+            expected_address = stack.number_u32(0x4444_4444);
+            expected_value = stack.number_u32(0x5555_5555);
+            expected_step = stack.number_u64(0x6666_6666_6666_6666);
+        };
+
+        stack.equality(address, true, expected_address, true, true, true);
+        stack.equality(value, true, expected_value, true, true, true);
+        stack.equality(step, true, expected_step, true, true, true);
+
+        stack.op_true();
+        assert!(stack.run().success);
+    }
+
+    #[test]
+    fn test_get_chosen_read() {
+        test_get_chosen_read_aux(1);
+        test_get_chosen_read_aux(2);
+    }
+
+    fn test_verify_wrong_chunk_value_aux(address: u32, value: u32, chunk: &Chunk) -> bool {
+        let mut stack = StackTracker::new();
+
+        let address = stack.number_u32(address);
+        let value = stack.number_u32(value);
+        let tables = &StackTables::new(&mut stack, true, false, 0, 0, 0);
+
+        verify_wrong_chunk_value(&mut stack, tables, chunk, address, value);
+        tables.drop(&mut stack);
+        stack.op_true();
+        stack.run().success
+    }
+
+    #[test]
+    fn test_verify_wrong_chunk_value() {
+        let chunk = &Chunk {
+            base_addr: 0x1000_0000,
+            data: vec![0x1111_1111, 0x2222_2222],
+        };
+
+        assert!(test_verify_wrong_chunk_value_aux(0x1000_0000, 0x1234_5678, chunk));
+        assert!(test_verify_wrong_chunk_value_aux(0x1000_0004, 0x1234_5678, chunk));
+        assert!(!test_verify_wrong_chunk_value_aux(0x1000_0000, 0x1111_1111, chunk));
+        assert!(!test_verify_wrong_chunk_value_aux(0x1000_0004, 0x2222_2222, chunk));
+    }
 }
diff --git a/definitions/src/challenge.rs b/definitions/src/challenge.rs
index 38bcee1..b948c6c 100644
--- a/definitions/src/challenge.rs
+++ b/definitions/src/challenge.rs
@@ -2,7 +2,7 @@ use serde::{Deserialize, Serialize};
 use thiserror::Error;
 
 use crate::{
-    memory::{MemoryWitness, SectionDefinition},
+    memory::{Chunk, MemoryWitness, SectionDefinition},
     trace::{ProgramCounter, TraceRWStep, TraceRead, TraceReadPC, TraceStep, TraceWrite},
 };
 
@@ -12,9 +12,10 @@ pub enum ChallengeType {
     TraceHashZero(TraceStep, String),     // PROVER_TRACE_STEP, PROVER_STEP_HASH
     EntryPoint(TraceReadPC, u64, Option<u32>), // (PROVER_READ_PC, PROVER_READ_MICRO), PROVER_TRACE_STEP, ENTRYPOINT (only used on test)
     ProgramCounter(String, TraceStep, String, TraceReadPC),
-    Opcode(TraceReadPC, u32, Option<u32>, Option<Vec<u32>>), // (PROVER_PC, PROVER_OPCODE), CHUNK_INDEX, CHUNK_BASE_ADDRESS, OPCODES_CHUNK
+    Opcode(TraceReadPC, u32, Option<Chunk>), // (PROVER_PC, PROVER_OPCODE), CHUNK_INDEX, CHUNK_BASE_ADDRESS, OPCODES_CHUNK
     InputData(TraceRead, TraceRead, u32, u32),
-    RomData(TraceRead, TraceRead, u32, u32),
+    InitializedData(TraceRead, TraceRead, u8, u32, Option<Chunk>),
+    UninitializedData(TraceRead, TraceRead, u8, Option<SectionDefinition>),
     AddressesSections(
         TraceRead,
         TraceRead,
diff --git a/definitions/src/lib.rs b/definitions/src/lib.rs
index 20c37e8..a3a683b 100644
--- a/definitions/src/lib.rs
+++ b/definitions/src/lib.rs
@@ -4,5 +4,5 @@ pub mod trace;
 
 pub mod constants {
     pub const LAST_STEP_INIT: u64 = 0xFFFF_FFFF_FFFF_FFFF;
-    pub const CODE_CHUNK_SIZE: u32 = 500;
+    pub const CHUNK_SIZE: u32 = 500;
 }
diff --git a/definitions/src/memory.rs b/definitions/src/memory.rs
index ca0e0fd..7ac209e 100644
--- a/definitions/src/memory.rs
+++ b/definitions/src/memory.rs
@@ -110,6 +110,21 @@ impl MemoryWitness {
     }
 }
 
+#[derive(Clone, Debug, Serialize, Deserialize)]
+pub struct Chunk {
+    pub base_addr: u32,
+    pub data: Vec<u32>,
+}
+
+impl Chunk {
+    pub fn range(&self) -> (u32, u32) {
+        (
+            self.base_addr,
+            self.base_addr + self.data.len() as u32 * 4 - 1,
+        )
+    }
+}
+
 //create tests for the functions
 #[cfg(test)]
 mod tests {
diff --git a/docker-riscv32 b/docker-riscv32
index 3907b2d..177cfec 160000
--- a/docker-riscv32
+++ b/docker-riscv32
@@ -1 +1 @@
-Subproject commit 3907b2d44881037183351adb5d96075069fc7dee
+Subproject commit 177cfec547dcec240634a34737b9ecf0256f8b8f
diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 02e92e7..17e432d 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -1,6 +1,7 @@
 use bitvmx_cpu_definitions::{
     challenge::ChallengeType,
-    constants::{CODE_CHUNK_SIZE, LAST_STEP_INIT},
+    constants::{CHUNK_SIZE, LAST_STEP_INIT},
+    memory::{Chunk, SectionDefinition},
     trace::{generate_initial_step_hash, hashvec_to_string, validate_step_hash, TraceRWStep},
 };
 
@@ -108,10 +109,10 @@ pub fn verifier_check_execution(
             warn!("Do not challenge (as the challenge is not waranteed to be successful)");
             warn!("Report this case to be evaluated by the security team");
             should_challenge = force_condition == ForceCondition::ValidInputWrongStepOrHash
-                || force_condition == ForceCondition::Allways;
+                || force_condition == ForceCondition::Always;
         } else {
             should_challenge = force_condition == ForceCondition::ValidInputStepAndHash
-                || force_condition == ForceCondition::Allways;
+                || force_condition == ForceCondition::Always;
         }
     }
 
@@ -243,7 +244,8 @@ pub enum ForceChallenge {
     ProgramCounter,
     Opcode,
     InputData,
-    RomData,
+    InitializedData,
+    UninitializedData,
     AddressesSections,
     No,
 }
@@ -253,10 +255,17 @@ pub enum ForceChallenge {
 pub enum ForceCondition {
     ValidInputStepAndHash,
     ValidInputWrongStepOrHash,
-    Allways,
+    Always,
     No,
 }
 
+fn find_chunk_index(chunks: &[Chunk], address: u32) -> Option<usize> {
+    chunks.iter().position(|Chunk { base_addr, data }| {
+        let chunk_size = data.len();
+        *base_addr <= address && address < *base_addr + chunk_size as u32 * 4
+    })
+}
+
 pub fn verifier_choose_challenge(
     program_definition_file: &str,
     checkpoint_path: &str,
@@ -283,11 +292,11 @@ pub fn verifier_choose_challenge(
         || force == ForceChallenge::TraceHashZero
     {
         if trace.step_number == 1 {
-            info!("Veifier choose to challenge TRACE_HASH_ZERO");
+            info!("Verifier choose to challenge TRACE_HASH_ZERO");
             return Ok(ChallengeType::TraceHashZero(trace.trace_step, next_hash));
         }
 
-        info!("Veifier choose to challenge TRACE_HASH");
+        info!("Verifier choose to challenge TRACE_HASH");
         return Ok(ChallengeType::TraceHash(
             step_hash,
             trace.trace_step,
@@ -334,8 +343,7 @@ pub fn verifier_choose_challenge(
         && force == ForceChallenge::No)
         || force == ForceChallenge::AddressesSections
     {
-        info!("Verifier choose to challenge invalid ADDRESS SECTION");
-
+        info!("Verifier choose to challenge invalid ADDRESS_SECTION");
         return Ok(ChallengeType::AddressesSections(
             trace.read_1,
             trace.read_2,
@@ -358,16 +366,17 @@ pub fn verifier_choose_challenge(
         || force == ForceChallenge::ProgramCounter
     {
         if trace.step_number == 1 {
-            info!("Veifier choose to challenge ENTRYPOINT");
+            info!("Verifier choose to challenge ENTRYPOINT");
             return Ok(ChallengeType::EntryPoint(
                 trace.read_pc,
                 trace.step_number,
                 return_script_parameters.then_some(program.pc.get_address()), //this parameter is only used for the test
             ));
         } else {
-            info!("Veifier choose to challenge PROGRAM_COUNTER");
+            info!("Verifier choose to challenge PROGRAM_COUNTER");
             let pre_pre_hash = my_execution[0].1.clone();
             let pre_step = my_execution[1].0.clone();
+
             return Ok(ChallengeType::ProgramCounter(
                 pre_pre_hash,
                 pre_step.trace_step,
@@ -381,60 +390,94 @@ pub fn verifier_choose_challenge(
         || force == ForceChallenge::Opcode
     {
         info!("Verifier choose to challenge invalid OPCODE");
-
         let pc = trace.read_pc.pc.get_address();
-
-        let (chunk_index, chunk_base_addr, chunk_start) = program.get_chunk_info(pc, CODE_CHUNK_SIZE);
-
-        let section = program.find_section(pc).unwrap();
-        let chunk_end = (chunk_start + CODE_CHUNK_SIZE as usize).min(section.data.len());
-
-        let opcodes_chunk: Vec<u32> = section.data[chunk_start..chunk_end]
-            .iter()
-            .map(|opcode| u32::from_be(*opcode))
-            .collect();
+        let code_chunks = program.get_code_chunks(CHUNK_SIZE);
+        let chunk_index = find_chunk_index(&code_chunks, pc).unwrap();
 
         return Ok(ChallengeType::Opcode(
             trace.read_pc,
-            chunk_index,
-            return_script_parameters.then_some(chunk_base_addr),
-            return_script_parameters.then_some(opcodes_chunk),
+            chunk_index as u32,
+            return_script_parameters.then_some(code_chunks[chunk_index].clone()),
         ));
     }
 
     // check const read value
-    let conflict_read_1 =
-        trace.read_1.value != my_trace.read_1.value && trace.read_1.last_step == LAST_STEP_INIT;
-    let conflict_read_2 =
-        trace.read_2.value != my_trace.read_2.value && trace.read_2.last_step == LAST_STEP_INIT;
-    if conflict_read_1 || conflict_read_2 {
-        let conflict_address = if conflict_read_1 {
-            trace.read_1.address
+    let conflict_read_1 = trace.read_1.value != my_trace.read_1.value;
+    let conflict_read_2 = trace.read_2.value != my_trace.read_2.value;
+
+    if (conflict_read_1 || conflict_read_2 && force == ForceChallenge::No)
+        || force == ForceChallenge::InputData
+        || force == ForceChallenge::InitializedData
+        || force == ForceChallenge::UninitializedData
+    {
+        let (conflict_trace, read_selector) = if conflict_read_1 {
+            (trace.read_1.clone(), 1)
         } else {
-            trace.read_2.address
+            (trace.read_2.clone(), 2)
         };
+
+        let conflict_address = conflict_trace.address;
         let section = program.find_section(conflict_address)?;
-        //TODO: Check if the address is in the input section rom ram or registers
-        let value = program.read_mem(conflict_address)?;
-        if (section.name == program_def.input_section_name && force == ForceChallenge::No)
+
+        if (conflict_trace.last_step == LAST_STEP_INIT && force == ForceChallenge::No)
             || force == ForceChallenge::InputData
+            || force == ForceChallenge::InitializedData
+            || force == ForceChallenge::UninitializedData
         {
-            info!("Verifier choose to challenge invalid INPUT DATA");
-            return Ok(ChallengeType::InputData(
-                trace.read_1.clone(),
-                trace.read_2.clone(),
-                conflict_address,
-                value,
-            ));
-        } else if (!section.is_write && force == ForceChallenge::No) || force == ForceChallenge::RomData {
-            info!("Verifier choose to challenge invalid ROM DATA");
-            
-            return Ok(ChallengeType::RomData(
-                trace.read_1.clone(),
-                trace.read_2.clone(),
-                conflict_address,
-                value,
-            ));
+            let input_size = program_def
+                .inputs
+                .iter()
+                .fold(0, |acc, input| acc + input.size);
+
+            if (section.name == program_def.input_section_name
+                && conflict_address < section.start + input_size as u32
+                && force == ForceChallenge::No)
+                || force == ForceChallenge::InputData
+            {
+                info!("Verifier choose to challenge invalid INPUT DATA");
+                let value = program.read_mem(conflict_address).or_else(|_| {
+                    Ok::<u32, ExecutionResult>(
+                        program
+                            .registers
+                            .get(program.registers.get_original_idx(conflict_address)),
+                    )
+                })?;
+
+                return Ok(ChallengeType::InputData(
+                    trace.read_1,
+                    trace.read_2,
+                    conflict_address,
+                    value,
+                ));
+            } else if (section.initialized && force == ForceChallenge::No)
+                || force == ForceChallenge::InitializedData
+            {
+                info!("Verifier choose to challenge invalid INITIALIZED DATA");
+                let initialized_chunks = program.get_initialized_chunks(CHUNK_SIZE);
+                let chunk_index = find_chunk_index(&initialized_chunks, conflict_address).unwrap();
+
+                return Ok(ChallengeType::InitializedData(
+                    trace.read_1,
+                    trace.read_2,
+                    read_selector,
+                    chunk_index as u32,
+                    return_script_parameters.then_some(initialized_chunks[chunk_index].clone()),
+                ));
+            } else if (!section.initialized && force == ForceChallenge::No)
+                || force == ForceChallenge::UninitializedData
+            {
+                info!("Verifier choose to challenge invalid UNINITIALIZED DATA");
+                let uninitilized_ranges = program.get_uninitialized_ranges(program_def);
+
+                return Ok(ChallengeType::UninitializedData(
+                    trace.read_1,
+                    trace.read_2,
+                    read_selector,
+                    return_script_parameters.then_some(SectionDefinition {
+                        ranges: uninitilized_ranges,
+                    }),
+                ));
+            }
         }
     }
 
@@ -629,7 +672,7 @@ mod tests {
 
         let challenge = verifier_choose_challenge(
             pdf,
-            &chk_verifier_path,
+            chk_verifier_path,
             final_trace,
             force,
             fail_config_verifier,
@@ -791,7 +834,7 @@ mod tests {
         let fail_args = vec![
             "1106",
             "0xaa000000",
-            "0x11111111",
+            "0x11111100",
             "0xaa000000",
             "0xffffffffffffffff",
         ]
@@ -805,34 +848,15 @@ mod tests {
         test_challenge_aux(
             "11",
             "hello-world.yaml",
-            0,
+            17,
             false,
-            fail_read_2,
+            fail_read_2.clone(),
             None,
             true,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
         );
 
-        // if we use the same fail_read as before, the prover won't challenge
-        // because there is no hash difference, the previous fail_read reads
-        // the value 0x11111111 and that's what we are already reading
-        // because we pass 17 as input instead of 0
-        let fail_args = vec![
-            "1106",
-            "0xaa000000",
-            "0x11111100", // different input value
-            "0xaa000000",
-            "0xffffffffffffffff",
-        ]
-        .iter()
-        .map(|x| x.to_string())
-        .collect::<Vec<String>>();
-        let fail_read_2 = Some(FailConfiguration::new_fail_reads(FailReads::new(
-            None,
-            Some(&fail_args),
-        )));
-
         test_challenge_aux(
             "12",
             "hello-world.yaml",
@@ -841,7 +865,7 @@ mod tests {
             None,
             fail_read_2,
             false,
-            ForceCondition::ValidInputStepAndHash,
+            ForceCondition::No,
             ForceChallenge::InputData,
         );
     }
@@ -1200,7 +1224,7 @@ mod tests {
             None,
             fail_execute,
             false,
-            ForceCondition::ValidInputWrongStepOrHash,
+            ForceCondition::No,
             ForceChallenge::AddressesSections,
         );
     }
@@ -1249,7 +1273,7 @@ mod tests {
             None,
             fail_execute,
             false,
-            ForceCondition::ValidInputWrongStepOrHash,
+            ForceCondition::No,
             ForceChallenge::AddressesSections,
         );
     }
@@ -1292,7 +1316,7 @@ mod tests {
     }
 
     #[test]
-    fn test_challenge_rom() {
+    fn test_challenge_initialized() {
         init_trace();
         let fail_execute = FailExecute {
             step: 32,
@@ -1301,7 +1325,10 @@ mod tests {
                 TraceRead::new(4026531900, 2952790016, 31),
                 TraceRead::new(2952790016, 0, LAST_STEP_INIT), // read a different value from ROM
                 TraceReadPC::new(ProgramCounter::new(2147483708, 0), 509699),
-                TraceStep::new(TraceWrite::new(4026531896, 0), ProgramCounter::new(2147483712, 0)),
+                TraceStep::new(
+                    TraceWrite::new(4026531896, 0),
+                    ProgramCounter::new(2147483712, 0),
+                ),
                 None,
                 MemoryWitness::new(
                     MemoryAccessType::Register,
@@ -1334,7 +1361,51 @@ mod tests {
             fail_execute,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
-            ForceChallenge::RomData,
+            ForceChallenge::InitializedData,
+        );
+    }
+
+    #[test]
+    fn test_challenge_uninitialized() {
+        init_trace();
+
+        let fail_args = vec![
+            "9",
+            "0xa0001004",
+            "0x11111100",
+            "0xa0001004",
+            "0xffffffffffffffff",
+        ]
+        .iter()
+        .map(|x| x.to_string())
+        .collect::<Vec<String>>();
+        let fail_read_2 = Some(FailConfiguration::new_fail_reads(FailReads::new(
+            None,
+            Some(&fail_args),
+        )));
+
+        test_challenge_aux(
+            "31",
+            "hello-world-uninitialized.yaml",
+            0,
+            false,
+            fail_read_2.clone(),
+            None,
+            true,
+            ForceCondition::No,
+            ForceChallenge::No,
+        );
+
+        test_challenge_aux(
+            "32",
+            "hello-world-uninitialized.yaml",
+            17,
+            false,
+            None,
+            fail_read_2,
+            false,
+            ForceCondition::ValidInputWrongStepOrHash,
+            ForceChallenge::UninitializedData,
         );
     }
 }
diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs
index aebe2e5..2484a8f 100644
--- a/emulator/src/executor/fetcher.rs
+++ b/emulator/src/executor/fetcher.rs
@@ -38,7 +38,7 @@ pub fn execute_program(
     let mut traces = Vec::new();
 
     if !input.is_empty() {
-        if let Some(section) = program.find_section_by_name(input_section_name) {
+        if let Some(section) = program.find_section_by_name_mut(input_section_name) {
             let input_as_u32 = vec_u8_to_vec_u32(&input, little_endian);
             for (i, byte) in input_as_u32.iter().enumerate() {
                 section.data[i] = *byte;
diff --git a/emulator/src/loader/program.rs b/emulator/src/loader/program.rs
index a3e8960..901fe24 100644
--- a/emulator/src/loader/program.rs
+++ b/emulator/src/loader/program.rs
@@ -5,7 +5,7 @@ use bitcoin_script_riscv::riscv::instruction_mapping::{
 };
 use bitvmx_cpu_definitions::{
     constants::LAST_STEP_INIT,
-    memory::{MemoryAccessType, SectionDefinition},
+    memory::{Chunk, MemoryAccessType, SectionDefinition},
     trace::{generate_initial_step_hash, ProgramCounter, TraceRead, TraceWrite},
 };
 use elf::{abi::SHF_EXECINSTR, abi::SHF_WRITE, endian::LittleEndian, ElfBytes};
@@ -13,7 +13,9 @@ use serde::{Deserialize, Serialize};
 use serde_big_array::BigArray;
 use tracing::{error, info};
 
-use crate::{constants::*, EmulatorError, ExecutionResult};
+use crate::{
+    constants::*, loader::program_definition::ProgramDefinition, EmulatorError, ExecutionResult,
+};
 
 #[derive(Debug, Serialize, Deserialize, PartialEq)]
 pub struct Section {
@@ -76,17 +78,12 @@ impl Section {
         (self.start, self.start + self.size - 1)
     }
 
-    pub fn contains(&self, address: u32) -> bool {
-        let (start, end) = self.range();
-        return address >= start && address <= end - 3;
-    }
-
     pub fn is_merge_compatible(&self, other: &Self) -> bool {
-        return self.is_code == other.is_code
+        self.is_code == other.is_code
             && self.is_write == other.is_write
             && self.initialized == other.initialized
             && self.registers == other.registers
-            && self.start + self.size == other.start;
+            && self.start + self.size == other.start
     }
 
     pub fn merge_in_place(&mut self, other: Self) {
@@ -256,7 +253,7 @@ impl Program {
         self.sections = merged;
     }
 
-    pub fn generate_sections_definitions(&mut self) {
+    fn generate_sections_definitions(&mut self) {
         for section in &self.sections {
             let section_range = section.range();
 
@@ -302,8 +299,7 @@ impl Program {
 
     fn find_section_idx(&self, address: u32) -> Result<usize, ExecutionResult> {
         // Binary search to find the appropriate section
-        Ok(self
-            .sections
+        self.sections
             .binary_search_by(|section| {
                 if address < section.start {
                     Ordering::Greater
@@ -318,7 +314,7 @@ impl Program {
                     "Address 0x{:08x} not found in any section",
                     address
                 ))
-            })?)
+            })
     }
 
     // Find the section that contains the given address
@@ -351,7 +347,11 @@ impl Program {
         Ok(section)
     }
 
-    pub fn find_section_by_name(&mut self, name: &str) -> Option<&mut Section> {
+    pub fn find_section_by_name(&self, name: &str) -> Option<&Section> {
+        self.sections.iter().find(|section| section.name == name)
+    }
+
+    pub fn find_section_by_name_mut(&mut self, name: &str) -> Option<&mut Section> {
         self.sections
             .iter_mut()
             .find(|section| section.name == name)
@@ -454,88 +454,77 @@ impl Program {
         }
     }
 
-    pub fn get_chunks(&self, chunk_size: u32) -> Vec<(u32, Vec<u32>)> {
-        let mut chunks = Vec::new();
-
-        for section in &self.sections {
-            if !section.is_code {
-                continue;
-            }
-
-            for (index, chunk) in section.data.chunks(chunk_size as usize).enumerate() {
-                chunks.push((
-                    section.start + index as u32 * chunk_size,
-                    chunk
-                        .to_vec()
-                        .iter()
-                        .map(|opcode| u32::from_be(*opcode))
-                        .collect(),
-                ));
-            }
-        }
-
-        chunks
+    pub fn get_chunks(&self, chunk_size: u32, filter: impl Fn(&&Section) -> bool) -> Vec<Chunk> {
+        self.sections
+            .iter()
+            .filter(filter)
+            .flat_map(|section| {
+                section
+                    .data
+                    .chunks(chunk_size as usize)
+                    .enumerate()
+                    .map(|(index, chunk)| {
+                        let offset = section.start + index as u32 * chunk_size;
+                        let data = chunk.iter().map(|opcode| u32::from_be(*opcode)).collect();
+                        Chunk {
+                            base_addr: offset,
+                            data,
+                        }
+                    })
+            })
+            .collect()
     }
 
-    // Avoids calling get_chunks().len() to prevent unnecessary Vec allocations and cloning
-    pub fn get_chunk_count(&self, chunk_size: u32) -> u32 {
-        let mut chunk_count = 0;
-
-        for section in &self.sections {
-            if !section.is_code {
-                continue;
-            }
-
-            let section_instrs = section.size / 4;
-            // only counts full chunks
-            let mut section_chunks = section_instrs / chunk_size;
-
-            // if section_instrs isn't a multiple of chunk_size that means that there is a non-full chunk we have to count
-            if section_instrs % chunk_size != 0 {
-                section_chunks += 1;
-            }
-
-            chunk_count += section_chunks;
-        }
-
-        chunk_count
+    pub fn get_initialized_chunks(&self, chunk_size: u32) -> Vec<Chunk> {
+        self.get_chunks(chunk_size, |section| {
+            section.initialized && !section.is_code
+        })
     }
 
-    pub fn get_chunk_info(&self, address: u32, chunk_size: u32) -> (u32, u32, usize) {
-        let mut chunk_index = 0;
-
-        for section in &self.sections {
-            if !section.is_code {
-                continue;
-            }
-
-            if section.contains(address) {
-                let section_start = section.start;
-                let offset = address - section_start;
-                let instr_index = offset / 4;
+    pub fn get_code_chunks(&self, chunk_size: u32) -> Vec<Chunk> {
+        self.get_chunks(chunk_size, |section| section.is_code)
+    }
 
-                chunk_index += instr_index / chunk_size;
+    pub fn get_uninitialized_ranges(
+        &self,
+        program_definition: ProgramDefinition,
+    ) -> Vec<(u32, u32)> {
+        let mut uninitialized: Vec<(u32, u32)> = self
+            .sections
+            .iter()
+            .filter(|section| {
+                // we do inputs separately
+                !section.initialized && section.name != program_definition.input_section_name
+            })
+            .map(|section| section.range())
+            .collect();
 
-                let chunk_start_instr = instr_index - (instr_index % chunk_size);
-                let chunk_base_addr = section_start + chunk_start_instr * 4;
-                let chunk_start_index = chunk_start_instr as usize;
+        let input_section = self
+            .find_section_by_name(&program_definition.input_section_name)
+            .expect("Input section not found");
 
-                return (chunk_index, chunk_base_addr, chunk_start_index);
-            }
+        // input section is usually bigger than the actual input of the program, so the remaining space should be uninitialized
+        let input_size = program_definition
+            .inputs
+            .iter()
+            .fold(0, |acc, input| acc + input.size);
 
-            let section_instrs = section.size / 4;
-            // only counts full chunks
-            let mut section_chunks = section_instrs / chunk_size;
+        let (start, end) = input_section.range();
+        let uninit_start = start + input_size as u32;
 
-            // if section_instrs isn't a multiple of chunk_size that means that there is a non-full chunk we have to count
-            if section_instrs % chunk_size != 0 {
-                section_chunks += 1;
-            }
+        assert!(
+            uninit_start <= end,
+            "Input size ({}) exceeds input section size ({}..{})",
+            input_size,
+            start,
+            end
+        );
 
-            chunk_index += section_chunks;
+        if uninit_start < end {
+            uninitialized.push((uninit_start, end));
         }
 
-        unreachable!("Non-executable address: 0x{:08X}", address);
+        uninitialized
     }
 }
 
@@ -814,60 +803,4 @@ mod tests {
         // there are no new sections
         assert_eq!(program.sections.len(), 4);
     }
-
-    #[test]
-    fn test_chunk_info() {
-        let mut program = Program::new(0, 0, 0);
-
-        // first section has 3 chunks, two full chunks of 500 instructions and half a chunk of 250 instructions
-        program.add_section(Section::new(
-            "code_1",
-            1000,
-            500 * 4 * 2 + 250 * 4,
-            true,
-            false,
-            false,
-        ));
-        program.add_section(Section::new("code_2", 10000, 500 * 4, true, false, false));
-
-        // start of first chunk
-        let (chunk_index, chunk_base_addr, chunk_start_index) = program.get_chunk_info(1000, 500);
-        assert_eq!(chunk_index, 0);
-        assert_eq!(chunk_base_addr, 1000);
-        assert_eq!(chunk_start_index, 0);
-
-        // middle of first chunk
-        let (chunk_index, chunk_base_addr, chunk_start_index) =
-            program.get_chunk_info(1000 + 250 * 4, 500);
-        assert_eq!(chunk_index, 0);
-        assert_eq!(chunk_base_addr, 1000);
-        assert_eq!(chunk_start_index, 0);
-
-        // start of second chunk
-        let (chunk_index, chunk_base_addr, chunk_start_index) =
-            program.get_chunk_info(1000 + 500 * 4, 500);
-        assert_eq!(chunk_index, 1);
-        assert_eq!(chunk_base_addr, 1000 + 500 * 4);
-        assert_eq!(chunk_start_index, 500);
-
-        // middle of second chunk
-        let (chunk_index, chunk_base_addr, chunk_start_index) =
-            program.get_chunk_info(1000 + 500 * 4 + 250 * 4, 500);
-        assert_eq!(chunk_index, 1);
-        assert_eq!(chunk_base_addr, 1000 + 500 * 4);
-        assert_eq!(chunk_start_index, 500);
-
-        // start of first chunk of the second section
-        let (chunk_index, chunk_base_addr, chunk_start_index) = program.get_chunk_info(10000, 500);
-        assert_eq!(chunk_index, 3);
-        assert_eq!(chunk_base_addr, 10000);
-        assert_eq!(chunk_start_index, 0);
-
-        // middle of first chunk of the second section
-        let (chunk_index, chunk_base_addr, chunk_start_index) =
-            program.get_chunk_info(10000 + 250 * 4, 500);
-        assert_eq!(chunk_index, 3);
-        assert_eq!(chunk_base_addr, 10000);
-        assert_eq!(chunk_start_index, 0);
-    }
 }

From 9b31463883249926954ad4e682d4d5888b310f21 Mon Sep 17 00:00:00 2001
From: Martin Jonas <martinjonas@gmail.com>
Date: Fri, 4 Jul 2025 12:53:39 -0300
Subject: [PATCH 02/34] update docker

---
 docker-riscv32 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docker-riscv32 b/docker-riscv32
index 177cfec..7936217 160000
--- a/docker-riscv32
+++ b/docker-riscv32
@@ -1 +1 @@
-Subproject commit 177cfec547dcec240634a34737b9ecf0256f8b8f
+Subproject commit 7936217786c0e3d297e884ec47435101dbf17422

From 5258ab4a69790576cef653c478359ee98cb48556 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 12:53:35 -0300
Subject: [PATCH 03/34] Fix section retrieval and memory read

---
 emulator/src/decision/challenge.rs | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 17e432d..c12d842 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -416,8 +416,8 @@ pub fn verifier_choose_challenge(
             (trace.read_2.clone(), 2)
         };
 
-        let conflict_address = conflict_trace.address;
-        let section = program.find_section(conflict_address)?;
+        let section_idx = program.find_section_idx(conflict_address)?;
+        let section = program.sections.get(section_idx).unwrap();
 
         if (conflict_trace.last_step == LAST_STEP_INIT && force == ForceChallenge::No)
             || force == ForceChallenge::InputData
@@ -435,13 +435,7 @@ pub fn verifier_choose_challenge(
                 || force == ForceChallenge::InputData
             {
                 info!("Verifier choose to challenge invalid INPUT DATA");
-                let value = program.read_mem(conflict_address).or_else(|_| {
-                    Ok::<u32, ExecutionResult>(
-                        program
-                            .registers
-                            .get(program.registers.get_original_idx(conflict_address)),
-                    )
-                })?;
+                let value = program.read_mem(conflict_address)?;
 
                 return Ok(ChallengeType::InputData(
                     trace.read_1,

From 0a3e55860c9baf12acd0ffd1a009aba5b5175e29 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 12:58:49 -0300
Subject: [PATCH 04/34] Fix initial value challenges logic

---
 emulator/src/decision/challenge.rs | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index c12d842..0173d60 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -402,24 +402,30 @@ pub fn verifier_choose_challenge(
     }
 
     // check const read value
-    let conflict_read_1 = trace.read_1.value != my_trace.read_1.value;
-    let conflict_read_2 = trace.read_2.value != my_trace.read_2.value;
+    let is_read_1_conflict = trace.read_1.value != my_trace.read_1.value;
+    let is_read_2_conflict = trace.read_2.value != my_trace.read_2.value;
 
-    if (conflict_read_1 || conflict_read_2 && force == ForceChallenge::No)
+    if ((is_read_1_conflict || is_read_2_conflict) && force == ForceChallenge::No)
         || force == ForceChallenge::InputData
         || force == ForceChallenge::InitializedData
         || force == ForceChallenge::UninitializedData
     {
-        let (conflict_trace, read_selector) = if conflict_read_1 {
-            (trace.read_1.clone(), 1)
+        let (conflict_read, my_conflict_read, read_selector) = if is_read_1_conflict {
+            (trace.read_1.clone(), my_trace.read_1.clone(), 1)
         } else {
-            (trace.read_2.clone(), 2)
+            (trace.read_2.clone(), my_trace.read_2.clone(), 2)
         };
 
+        let conflict_address = conflict_read.address;
+        let conflict_last_step = conflict_read.last_step;
+        let my_conflict_last_step = my_conflict_read.last_step;
+
         let section_idx = program.find_section_idx(conflict_address)?;
         let section = program.sections.get(section_idx).unwrap();
 
-        if (conflict_trace.last_step == LAST_STEP_INIT && force == ForceChallenge::No)
+        if (conflict_last_step == LAST_STEP_INIT
+            && my_conflict_last_step == LAST_STEP_INIT
+            && force == ForceChallenge::No)
             || force == ForceChallenge::InputData
             || force == ForceChallenge::InitializedData
             || force == ForceChallenge::UninitializedData

From 7e16660582c440eb9b72d72fbcbc724b95353346 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 13:04:42 -0300
Subject: [PATCH 05/34] Rename and fix get_selected_vars function

---
 bitcoin-script-riscv/src/riscv/challenges.rs  |  42 +++++--
 .../src/riscv/script_utils.rs                 | 114 +++++++++---------
 2 files changed, 92 insertions(+), 64 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index a5dce64..53f436d 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -392,11 +392,24 @@ pub fn opcode_challenge(stack: &mut StackTracker, chunk: &Chunk) {
 }
 
 pub fn initialized_challenge(stack: &mut StackTracker, chunk: &Chunk) {
-    get_chosen_read(stack);
+    stack.clear_definitions();
+
+    let read_addr_1 = stack.define(8, "prover_read_addr_1");
+    let read_value_1 = stack.define(8, "prover_read_value_1");
+    let read_step_1 = stack.define(16, "prover_read_step_1");
+
+    let read_addr_2 = stack.define(8, "prover_read_addr_2");
+    let read_value_2 = stack.define(8, "prover_read_value_2");
+    let read_step_2 = stack.define(16, "prover_read_step_2");
 
-    let read_addr = stack.define(8, "prover_read_addr");
-    let read_value = stack.define(8, "prover_read_value");
-    let read_step = stack.define(16, "prover_read_step");
+    let read_selector = stack.define(2, "read_selector");
+
+    let [read_addr, read_value, read_step] = get_selected_vars(
+        stack,
+        [read_addr_1, read_value_1, read_step_1],
+        [read_addr_2, read_value_2, read_step_2],
+        read_selector,
+    );
 
     address_in_range(stack, &chunk.range(), &read_addr);
     stack.op_verify();
@@ -414,11 +427,24 @@ pub fn uninitialized_challenge(
     stack: &mut StackTracker,
     uninitialized_sections: &SectionDefinition,
 ) {
-    get_chosen_read(stack);
+    stack.clear_definitions();
+
+    let read_addr_1 = stack.define(8, "prover_read_addr_1");
+    let read_value_1 = stack.define(8, "prover_read_value_1");
+    let read_step_1 = stack.define(16, "prover_read_step_1");
+
+    let read_addr_2 = stack.define(8, "prover_read_addr_2");
+    let read_value_2 = stack.define(8, "prover_read_value_2");
+    let read_step_2 = stack.define(16, "prover_read_step_2");
 
-    let read_addr = stack.define(8, "prover_read_addr");
-    let read_value = stack.define(8, "prover_read_value");
-    let read_step = stack.define(16, "prover_read_step");
+    let read_selector = stack.define(2, "read_selector");
+
+    let [read_addr, read_value, read_step] = get_selected_vars(
+        stack,
+        [read_addr_1, read_value_1, read_step_1],
+        [read_addr_2, read_value_2, read_step_2],
+        read_selector,
+    );
 
     address_in_sections(stack, &read_addr, uninitialized_sections);
     stack.op_verify();
diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs
index 2149f49..ed2b666 100644
--- a/bitcoin-script-riscv/src/riscv/script_utils.rs
+++ b/bitcoin-script-riscv/src/riscv/script_utils.rs
@@ -1442,39 +1442,48 @@ pub fn verify_wrong_chunk_value(
     chunk_table.drop(stack);
 }
 
-pub fn get_chosen_read(stack: &mut StackTracker) {
-    stack.clear_definitions();
-
-    let read_1_addr = stack.define(8, "prover_read_1_addr");
-    let read_1_value = stack.define(8, "prover_read_1_value");
-    let read_1_step = stack.define(16, "prover_read_1_step");
+pub fn get_selected_vars<const N: usize>(
+    stack: &mut StackTracker,
+    vars_1: [StackVariable; N],
+    vars_2: [StackVariable; N],
+    var_selector: StackVariable,
+) -> [StackVariable; N] {
+    assert_eq!(vars_1.len(), vars_2.len());
+    let consumes = vars_1.len() as u32 * 2;
+
+    let output: Vec<_> = vars_1
+        .iter()
+        .enumerate()
+        .map(|(i, var)| (stack.get_size(*var), format!("var_{}", i)))
+        .collect();
 
-    let read_2_addr = stack.define(8, "prover_read_2_addr");
-    let read_2_value = stack.define(8, "prover_read_2_value");
-    let read_2_step = stack.define(16, "prover_read_2_step");
+    // we need the variables to be on top of the stack, or we will break variables that are higher when merging the branches
+    for (var_1, var_2) in vars_1.iter().zip(vars_2.iter()) {
+        assert_eq!(stack.get_size(*var_1), stack.get_size(*var_2));
+        stack.move_var(*var_1);
+        stack.move_var(*var_2);
+    }
 
-    let read_selector = stack.define(2, "read_selector");
     let one = stack.byte(1);
+    stack.equality(var_selector, true, one, true, true, false);
 
-    stack.equality(read_selector, true, one, true, true, false);
-
-    let (mut challenge_read_1, mut challenge_read_2) = stack.open_if();
-
-    challenge_read_1.drop(read_2_step);
-    challenge_read_1.drop(read_2_value);
-    challenge_read_1.drop(read_2_addr);
+    let (mut chose_var_1, mut chose_var_2) = stack.open_if();
 
-    challenge_read_2.move_var(read_1_addr);
-    challenge_read_2.drop(read_1_addr);
+    for (var_1, var_2) in vars_1.into_iter().zip(vars_2.into_iter()) {
+        chose_var_1.move_var(var_2);
+        chose_var_1.drop(var_2);
+        chose_var_1.move_var(var_1);
 
-    challenge_read_2.move_var(read_1_value);
-    challenge_read_2.drop(read_1_value);
-
-    challenge_read_2.move_var(read_1_step);
-    challenge_read_2.drop(read_1_step);
+        chose_var_2.move_var(var_1);
+        chose_var_2.drop(var_1);
+        chose_var_2.move_var(var_2);
+    }
 
-    stack.end_if(challenge_read_1, challenge_read_2, 3, vec![], 0);
-    stack.clear_definitions();
+    stack
+        .end_if(chose_var_1, chose_var_2, consumes, output, 0)
+        .try_into()
+        .ok()
+        .expect("Vec length does not match expected array size")
 }
 
 pub fn address_in_range(stack: &mut StackTracker, range: &(u32, u32), address: &StackVariable) {
@@ -1904,51 +1913,44 @@ mod tests {
         assert!(stack.run().success);
     }
 
-    fn test_get_chosen_read_aux(read_selector: u8) {
+    fn test_get_selected_vars_aux(var_selector: u8) {
         let mut stack = StackTracker::new();
 
-        stack.number_u32(0x1111_1111);
-        stack.number_u32(0x2222_2222);
-        stack.number_u64(0x3333_3333_3333_3333);
+        let previous_var = stack.number_u32(0x3333_3333);
 
-        stack.number_u32(0x4444_4444);
-        stack.number_u32(0x5555_5555);
-        stack.number_u64(0x6666_6666_6666_6666);
+        let var_1 = stack.number_u32(0x1111_1111);
+        let var_2 = stack.number_u32(0x2222_2222);
+        let selector = stack.byte(var_selector);
 
-        stack.byte(read_selector);
+        let next_var = stack.number_u32(0x4444_4444);
 
-        get_chosen_read(&mut stack);
+        let [chosen_var] = get_selected_vars(&mut stack, [var_1], [var_2], selector);
 
-        let address = stack.define(8, "address");
-        let value = stack.define(8, "value");
-        let step = stack.define(16, "step");
-
-        let expected_address;
-        let expected_value;
-        let expected_step;
-
-        if read_selector == 1 {
-            expected_address = stack.number_u32(0x1111_1111);
-            expected_value = stack.number_u32(0x2222_2222);
-            expected_step = stack.number_u64(0x3333_3333_3333_3333);
+        // we should get the selected variable
+        let expected_var = if var_selector == 1 {
+            0x1111_1111
         } else {
-            expected_address = stack.number_u32(0x4444_4444);
-            expected_value = stack.number_u32(0x5555_5555);
-            expected_step = stack.number_u64(0x6666_6666_6666_6666);
+            0x2222_2222
         };
+        let expected_var = stack.number_u32(expected_var);
+        stack.equality(chosen_var, true, expected_var, true, true, true);
+
+        // previous variable should remain unchanged
+        let expected_var = stack.number_u32(0x3333_3333);
+        stack.equality(previous_var, true, expected_var, true, true, true);
 
-        stack.equality(address, true, expected_address, true, true, true);
-        stack.equality(value, true, expected_value, true, true, true);
-        stack.equality(step, true, expected_step, true, true, true);
+        // next variable should also remain unchanged
+        let expected_var = stack.number_u32(0x4444_4444);
+        stack.equality(next_var, true, expected_var, true, true, true);
 
         stack.op_true();
         assert!(stack.run().success);
     }
 
     #[test]
-    fn test_get_chosen_read() {
-        test_get_chosen_read_aux(1);
-        test_get_chosen_read_aux(2);
+    fn test_get_selected_vars() {
+        test_get_selected_vars_aux(1);
+        test_get_selected_vars_aux(2);
     }
 
     fn test_verify_wrong_chunk_value_aux(address: u32, value: u32, chunk: &Chunk) -> bool {

From 39ea2956f868456ec01448f975258e7675ccad62 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 13:05:54 -0300
Subject: [PATCH 06/34] Add read value challenge script

---
 bitcoin-script-riscv/src/riscv/challenges.rs | 165 +++++++++++++++++--
 1 file changed, 150 insertions(+), 15 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index 53f436d..c4c8567 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -10,8 +10,8 @@ use bitvmx_cpu_definitions::{
 use crate::riscv::{
     memory_alignment::{is_aligned, load_lower_half_nibble_table, load_upper_half_nibble_table},
     script_utils::{
-        address_in_range, address_in_sections, address_not_in_sections, get_chosen_read,
-        verify_wrong_chunk_value, witness_equals, StackTables,
+        address_in_range, address_in_sections, address_not_in_sections, get_selected_vars,
+        is_lower_than, verify_wrong_chunk_value, witness_equals, StackTables,
     },
 };
 
@@ -458,6 +458,55 @@ pub fn uninitialized_challenge(
     stack.drop(read_addr);
 }
 
+pub fn read_value_challenge(stack: &mut StackTracker) {
+    stack.clear_definitions();
+
+    let read_addr_1 = stack.define(8, "prover_read_addr_1");
+    let read_value_1 = stack.define(8, "prover_read_value_1");
+    let read_step_1 = stack.define(16, "prover_read_step_1");
+
+    let read_addr_2 = stack.define(8, "prover_read_addr_2");
+    let read_value_2 = stack.define(8, "prover_read_value_2");
+    let read_step_2 = stack.define(16, "prover_read_step_2");
+
+    let read_selector = stack.define(2, "read_selector");
+
+    let write_addr = stack.define(8, "write_addr");
+    let write_value = stack.define(8, "write_value");
+    let write_step = stack.define(16, "write_step");
+
+    let [read_addr, read_value, read_step] = get_selected_vars(
+        stack,
+        [read_addr_1, read_value_1, read_step_1],
+        [read_addr_2, read_value_2, read_step_2],
+        read_selector,
+    );
+
+    stack.rename(read_step, "read_Step");
+
+    // if read_step == write_step -> write_addr != read_addr || write_value != read_value
+    stack.equality(read_step, false, write_step, false, true, false);
+
+    stack.equality(write_addr, false, read_addr, false, false, false);
+    stack.equality(write_value, true, read_value, true, false, false);
+    stack.op_boolor();
+    stack.op_booland();
+
+    let init = stack.number_u64(LAST_STEP_INIT);
+
+    // if read_step == INIT || read_step < write_step -> write_addr == read_addr
+    stack.equality(read_step, false, init, true, true, false);
+    is_lower_than(stack, read_step, write_step, true);
+    stack.op_boolor();
+    
+    stack.equality(write_addr, true, read_addr, true, true, false);
+    stack.op_booland();
+
+    stack.op_boolor();
+
+    stack.op_verify();
+}
+
 //TODO: memory section challenge
 //TODO: program crash challenge - this might be more about finding the right place to challenge that a challenge itself
 
@@ -569,6 +618,28 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
                 code_sections.as_ref().unwrap(),
             );
         }
+        ChallengeType::ReadValue {
+            read_1,
+            read_2,
+            read_selector,
+            trace,
+        } => {
+            stack.number_u32(read_1.address);
+            stack.number_u32(read_1.value);
+            stack.number_u64(read_1.last_step);
+
+            stack.number_u32(read_2.address);
+            stack.number_u32(read_2.value);
+            stack.number_u64(read_2.last_step);
+
+            stack.byte(*read_selector);
+
+            stack.number_u32(trace.trace_step.write_1.address);
+            stack.number_u32(trace.trace_step.write_1.value);
+            stack.number_u64(trace.step_number);
+
+            read_value_challenge(&mut stack);
+        }
         _ => {
             return false;
         }
@@ -580,7 +651,10 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
 #[cfg(test)]
 mod tests {
 
-    use bitvmx_cpu_definitions::{memory::MemoryWitness, trace::TraceRead};
+    use bitvmx_cpu_definitions::{
+        memory::MemoryWitness,
+        trace::{TraceRead, TraceWrite},
+    };
 
     use super::*;
 
@@ -1277,37 +1351,37 @@ mod tests {
             data: vec![0x1111_1111, 0x2222_2222, 0x3333_3333, 0x4444_4444],
         };
 
-        //can't challenge not init state
+        // can't challenge not init state
         let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, 1);
         let read_2 = TraceRead::new(0x1000_0004, 0x1234_5678, 2);
         assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
         assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
 
-        //can't challenge if value is right
+        // can't challenge if value is right
         let read_1 = TraceRead::new(0x1000_0000, 0x1111_1111, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0x1000_0004, 0x2222_2222, LAST_STEP_INIT);
         assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
         assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
 
-        //can't challenge if address is outside chunk
+        // can't challenge if address is outside chunk
         let read_1 = TraceRead::new(0x0000_0004, 0x1234_5678, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0x0000_0008, 0x1234_5678, LAST_STEP_INIT);
         assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
         assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
 
-        //challenge is valid if the address is the same but the value differs in both
+        // challenge is valid if the address is the same but the value differs in both
         let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0x1000_0004, 0x1234_5678, LAST_STEP_INIT);
         assert!(test_initialized_aux(&read_1, &read_2, 1, chunk));
         assert!(test_initialized_aux(&read_1, &read_2, 2, chunk));
 
-        //challenge is valid if the address is the same but the value differs in read_1 and uses correct selector
+        // challenge is valid if the address is the same but the value differs in read_1 and uses correct selector
         let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0x1000_0004, 0x2222_2222, LAST_STEP_INIT);
         assert!(test_initialized_aux(&read_1, &read_2, 1, chunk));
         assert!(!test_initialized_aux(&read_1, &read_2, 2, chunk));
 
-        //challenge is valid if the address is the same but the value differs in read_2 and uses correct selector
+        // challenge is valid if the address is the same but the value differs in read_2 and uses correct selector
         let read_1 = TraceRead::new(0x1000_0000, 0x1111_1111, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0x1000_0004, 0x1234_5678, LAST_STEP_INIT);
         assert!(!test_initialized_aux(&read_1, &read_2, 1, chunk));
@@ -1344,7 +1418,7 @@ mod tests {
             ranges: vec![(0x1000_0000, 0x2000_0000), (0xA000_0000, 0xB000_0000)],
         };
 
-        //can't challenge not init state
+        // can't challenge not init state
         let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, 1);
         let read_2 = TraceRead::new(0xA000_0000, 0x1234_5678, 2);
         assert!(!test_uninitialized_aux(
@@ -1360,7 +1434,7 @@ mod tests {
             uninitialized_sections
         ));
 
-        //can't challenge if value is right
+        // can't challenge if value is right
         let read_1 = TraceRead::new(0x1000_0000, 0, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0xA000_0000, 0, LAST_STEP_INIT);
         assert!(!test_uninitialized_aux(
@@ -1376,7 +1450,7 @@ mod tests {
             uninitialized_sections
         ));
 
-        //can't challenge if address is outside uninitialized sections
+        // can't challenge if address is outside uninitialized sections
         let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
         assert!(!test_uninitialized_aux(
@@ -1392,7 +1466,7 @@ mod tests {
             uninitialized_sections
         ));
 
-        //challenge is valid if the address is the same but the value differs in both
+        // challenge is valid if the address is the same but the value differs in both
         let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0xA000_0000, 0x1234_5678, LAST_STEP_INIT);
         assert!(test_uninitialized_aux(
@@ -1408,7 +1482,7 @@ mod tests {
             uninitialized_sections
         ));
 
-        //challenge is valid if the address is the same but the value differs in read_1 and uses correct selector
+        // challenge is valid if the address is the same but the value differs in read_1 and uses correct selector
         let read_1 = TraceRead::new(0x1000_0000, 0x1234_5678, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0xA000_0000, 0, LAST_STEP_INIT);
         assert!(test_uninitialized_aux(
@@ -1424,7 +1498,7 @@ mod tests {
             uninitialized_sections
         ));
 
-        //challenge is valid if the address is the same but the value differs in read_2 and uses correct selector
+        // challenge is valid if the address is the same but the value differs in read_2 and uses correct selector
         let read_1 = TraceRead::new(0x1000_0000, 0, LAST_STEP_INIT);
         let read_2 = TraceRead::new(0xA000_0000, 0x1234_5678, LAST_STEP_INIT);
         assert!(!test_uninitialized_aux(
@@ -1440,4 +1514,65 @@ mod tests {
             uninitialized_sections
         ));
     }
+
+    fn test_read_value_aux(read: TraceRead, write: TraceWrite, write_step: u64) -> bool {
+        let stack = &mut StackTracker::new();
+
+        stack.number_u32(read.address);
+        stack.number_u32(read.value);
+        stack.number_u64(read.last_step);
+
+        stack.number_u32(read.address);
+        stack.number_u32(read.value);
+        stack.number_u64(read.last_step);
+
+        stack.byte(1);
+
+        stack.number_u32(write.address);
+        stack.number_u32(write.value);
+        stack.number_u64(write_step);
+        
+        read_value_challenge(stack);
+
+        stack.op_true();
+        stack.run().success
+    }
+    #[test]
+    fn test_read_value() {
+        // can't challenge if read is correct
+        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let step = 100;
+        let write = TraceWrite::new(0x1000_0000, 0);
+        assert!(!test_read_value_aux(read, write, step));
+
+        // can't challenge if write is older
+        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let step = 50;
+        let write = TraceWrite::new(0x1000_0000, 100);
+        assert!(!test_read_value_aux(read, write, step));
+
+        // can't challenge if write is newer but for different address
+        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let step = 200;
+        let write = TraceWrite::new(0x2000_0000, 100);
+        assert!(!test_read_value_aux(read, write, step));
+
+        // challenge is valid if write is newer for the same address
+        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let write_step = 200;
+        let write = TraceWrite::new(0x1000_0000, 100);
+        assert!(test_read_value_aux(read, write, write_step));
+
+        // challenge is valid if write is at the same step but for different address
+        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let write_step = 100;
+        let write = TraceWrite::new(0x2000_0000, 100);
+        assert!(test_read_value_aux(read, write, write_step));
+
+        // challenge is valid if write is at the same step for different address but different value
+        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let write_step = 100;
+        let write = TraceWrite::new(0x1000_0000, 100);
+        assert!(test_read_value_aux(read, write, write_step));
+    }
 }

From 3bcd47af74dffaa9b074ad01b7a24788d5751b7a Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 13:07:21 -0300
Subject: [PATCH 07/34] make is_lower_than work with 64bit numbers

---
 .../src/riscv/script_utils.rs                 | 58 +++++++++++++++----
 1 file changed, 48 insertions(+), 10 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs
index ed2b666..328c730 100644
--- a/bitcoin-script-riscv/src/riscv/script_utils.rs
+++ b/bitcoin-script-riscv/src/riscv/script_utils.rs
@@ -636,6 +636,9 @@ pub fn is_lower_than(
     than: StackVariable,
     unsigned: bool,
 ) -> StackVariable {
+    assert_eq!(stack.get_size(value), stack.get_size(than));
+    let size = stack.get_size(value);
+
     if !unsigned {
         stack.copy_var_sub_n(value, 0);
         if_greater(stack, 7, 1, 0); //1 if negative
@@ -643,6 +646,7 @@ pub fn is_lower_than(
         if_greater(stack, 7, 1, 0); //1 if negative
         stack.op_2dup();
         stack.op_equal();
+        let n = 2_i32.pow(size + 1);
         stack
             .custom(
                 script! {
@@ -652,9 +656,9 @@ pub fn is_lower_than(
                     OP_ELSE
                         OP_GREATERTHAN
                         OP_IF
-                            512
+                            { n }
                         OP_ELSE
-                            { -512 }
+                            { -n }
                         OP_ENDIF
                     OP_ENDIF
                 },
@@ -666,8 +670,8 @@ pub fn is_lower_than(
             .unwrap();
     }
 
-    for i in 0..8 {
-        let n: i32 = 2_i32.pow(8 - i);
+    for i in 0..size {
+        let n: i32 = 2_i32.pow(size - i);
         stack.move_var_sub_n(value, 0);
         stack.move_var_sub_n(than, 0);
         stack.op_2dup();
@@ -677,7 +681,7 @@ pub fn is_lower_than(
                 script! {
                     OP_IF
                         OP_2DROP
-                        { n}
+                        { n }
                     OP_ELSE
                         OP_EQUAL
                         OP_IF
@@ -694,7 +698,7 @@ pub fn is_lower_than(
             )
             .unwrap();
     }
-    for _ in 0..7 {
+    for _ in 0..size - 1 {
         stack.op_add();
     }
     if !unsigned {
@@ -1736,6 +1740,24 @@ mod tests {
         test_lower_helper(0x0000_0000, 0xffff_f800, 0, false);
     }
 
+    fn test_lower_helper_64bits(value: u64, than: u64, expected: u32, unsigned: bool) {
+        let mut stack = StackTracker::new();
+        let value = stack.number_u64(value);
+        let than = stack.number_u64(than);
+        is_lower_than(&mut stack, value, than, unsigned);
+        stack.number(expected);
+        stack.op_equal();
+        assert!(stack.run().success);
+    }
+
+    #[test]
+    fn test_lower_64bits() {
+        test_lower_helper_64bits(0x0000_0000_0000_0000, 0xffff_ffff_ffff_ffff, 1, true);
+        test_lower_helper_64bits(0x0000_0000_0000_0000, 0xffff_ffff_ffff_ffff, 0, false);
+        test_lower_helper_64bits(0xf000_0000_0000_0000, 0xffff_ffff_ffff_ffff, 1, false);
+        test_lower_helper_64bits(0x0000_0000_0000_0000, 0xffff_f800_0000_0000, 0, false);
+    }
+
     #[test]
     fn test_shift_dynamic() {
         for y in 0..16 {
@@ -1973,9 +1995,25 @@ mod tests {
             data: vec![0x1111_1111, 0x2222_2222],
         };
 
-        assert!(test_verify_wrong_chunk_value_aux(0x1000_0000, 0x1234_5678, chunk));
-        assert!(test_verify_wrong_chunk_value_aux(0x1000_0004, 0x1234_5678, chunk));
-        assert!(!test_verify_wrong_chunk_value_aux(0x1000_0000, 0x1111_1111, chunk));
-        assert!(!test_verify_wrong_chunk_value_aux(0x1000_0004, 0x2222_2222, chunk));
+        assert!(test_verify_wrong_chunk_value_aux(
+            0x1000_0000,
+            0x1234_5678,
+            chunk
+        ));
+        assert!(test_verify_wrong_chunk_value_aux(
+            0x1000_0004,
+            0x1234_5678,
+            chunk
+        ));
+        assert!(!test_verify_wrong_chunk_value_aux(
+            0x1000_0000,
+            0x1111_1111,
+            chunk
+        ));
+        assert!(!test_verify_wrong_chunk_value_aux(
+            0x1000_0004,
+            0x2222_2222,
+            chunk
+        ));
     }
 }

From fced1e968dade796cec38a2668c84de8d68979f0 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 13:19:16 -0300
Subject: [PATCH 08/34] Separate NAryLogs

---
 emulator/src/decision/execution_log.rs | 55 +++++++++++++++++---------
 1 file changed, 36 insertions(+), 19 deletions(-)

diff --git a/emulator/src/decision/execution_log.rs b/emulator/src/decision/execution_log.rs
index 3b8c33c..02e8ecd 100644
--- a/emulator/src/decision/execution_log.rs
+++ b/emulator/src/decision/execution_log.rs
@@ -20,25 +20,29 @@ impl ExecutionLog {
     }
 }
 
-#[derive(Debug, Serialize, Deserialize)]
-pub struct ProverChallengeLog {
-    pub execution: ExecutionLog,
-    pub input: Vec<u8>,
+#[derive(Debug, Serialize, Deserialize, Default)]
+pub struct ProverNAryLog {
     pub base_step: u64,
     pub verifier_decisions: Vec<u32>,
     pub hash_rounds: Vec<Vec<String>>,
     pub final_trace: TraceRWStep,
 }
 
+#[derive(Debug, Serialize, Deserialize)]
+pub struct ProverChallengeLog {
+    pub execution: ExecutionLog,
+    pub input: Vec<u8>,
+    pub conflict_step_log: ProverNAryLog,
+    pub read_challenge_log: ProverNAryLog,
+}
+
 impl ProverChallengeLog {
     pub fn new(execution: ExecutionLog, input: Vec<u8>) -> Self {
         Self {
             execution,
             input,
-            base_step: 0,
-            verifier_decisions: Vec::new(),
-            hash_rounds: Vec::new(),
-            final_trace: TraceRWStep::default(),
+            conflict_step_log: ProverNAryLog::default(),
+            read_challenge_log: ProverNAryLog::default(),
         }
     }
 
@@ -51,19 +55,36 @@ impl ProverChallengeLog {
     }
 }
 
-#[derive(Debug, Serialize, Deserialize)]
-pub struct VerifierChallengeLog {
-    pub prover_claim_execution: ExecutionLog,
-    pub execution: ExecutionLog,
-    pub input: Vec<u8>,
+#[derive(Debug, Serialize, Deserialize, Default)]
+pub struct VerifierNAryLog {
     pub base_step: u64,
+    pub read_selector: u8,
     pub step_to_challenge: u64,
+    pub read_step: u64,
     pub verifier_decisions: Vec<u32>,
     pub prover_hash_rounds: Vec<Vec<String>>,
     pub verifier_hash_rounds: Vec<Vec<String>>,
     pub final_trace: TraceRWStep,
 }
 
+impl VerifierNAryLog {
+    pub fn new(step_to_challenge: u64) -> Self {
+        Self {
+            step_to_challenge,
+            ..Default::default()
+        }
+    }
+}
+
+#[derive(Debug, Serialize, Deserialize)]
+pub struct VerifierChallengeLog {
+    pub prover_claim_execution: ExecutionLog,
+    pub execution: ExecutionLog,
+    pub input: Vec<u8>,
+    pub conflict_step_log: VerifierNAryLog,
+    pub read_challenge_log: VerifierNAryLog,
+}
+
 impl VerifierChallengeLog {
     pub fn new(
         prover_execution: ExecutionLog,
@@ -75,12 +96,8 @@ impl VerifierChallengeLog {
             prover_claim_execution: prover_execution,
             execution,
             input,
-            base_step: 0,
-            step_to_challenge,
-            verifier_decisions: Vec::new(),
-            prover_hash_rounds: Vec::new(),
-            verifier_hash_rounds: Vec::new(),
-            final_trace: TraceRWStep::default(),
+            conflict_step_log: VerifierNAryLog::new(step_to_challenge),
+            read_challenge_log: VerifierNAryLog::default(),
         }
     }
 

From cb0412dd7076b15744e37299f19f455974974480 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 13:20:23 -0300
Subject: [PATCH 09/34] Fix fail_write step

unlike fil_read, we don't need to substract one for the step in its
creation since fail writes are done after the step execution,
so the step was already incremented
---
 emulator/src/executor/utils.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/emulator/src/executor/utils.rs b/emulator/src/executor/utils.rs
index 5cecf82..113557e 100644
--- a/emulator/src/executor/utils.rs
+++ b/emulator/src/executor/utils.rs
@@ -152,7 +152,7 @@ pub struct FailWrite {
 impl FailWrite {
     pub fn new(args: &Vec<String>) -> Self {
         Self {
-            step: parse_value::<u64>(&args[0]) - 1,
+            step: parse_value::<u64>(&args[0]),
             address_original: parse_value::<u32>(&args[1]),
             value: parse_value::<u32>(&args[2]),
             modified_address: parse_value::<u32>(&args[3]),
@@ -407,7 +407,7 @@ mod utils_tests {
             "4026531900".to_string(),
         ];
         let fail_write = FailWrite::new(&fail_write_args);
-        program.step = 9;
+        program.step = 10;
         fail_write.patch_mem(&mut program);
         let idx = program.registers.get_original_idx(4026531900);
 
@@ -435,7 +435,7 @@ mod utils_tests {
             "4096".to_string(),
         ];
         let fail_write = FailWrite::new(&fail_write_args);
-        program.step = 9;
+        program.step = 10;
         fail_write.patch_mem(&mut program);
 
         assert_eq!(program.read_mem(4096).unwrap(), 10);

From 99c51267e9cd08c199c8a0f5b640c6e8b7ec7fe2 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 14:00:27 -0300
Subject: [PATCH 10/34] Add read value challenge

---
 definitions/src/challenge.rs         |   7 ++
 emulator/src/decision/challenge.rs   | 171 ++++++++++++++++++++-------
 emulator/src/decision/nary_search.rs |  60 +++++++++-
 emulator/src/main.rs                 |  18 +++
 emulator/tests/challenge.rs          |   4 +-
 5 files changed, 211 insertions(+), 49 deletions(-)

diff --git a/definitions/src/challenge.rs b/definitions/src/challenge.rs
index b948c6c..f838e89 100644
--- a/definitions/src/challenge.rs
+++ b/definitions/src/challenge.rs
@@ -27,6 +27,13 @@ pub enum ChallengeType {
         Option<SectionDefinition>, // register sections
         Option<SectionDefinition>, // code sections
     ),
+    ReadValueNArySearch(u32),
+    ReadValue {
+        read_1: TraceRead,
+        read_2: TraceRead,
+        read_selector: u8,
+        trace: TraceRWStep,
+    },
     No,
 }
 
diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 0173d60..250596c 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -13,7 +13,7 @@ use tracing::{error, info, warn};
 use crate::{
     decision::{
         execution_log::VerifierChallengeLog,
-        nary_search::{choose_segment, ExecutionHashes},
+        nary_search::{choose_segment, ExecutionHashes, NArySearchType},
     },
     executor::utils::FailConfiguration,
     loader::program_definition::ProgramDefinition,
@@ -59,28 +59,26 @@ pub fn prover_get_hashes_for_round(
     round: u8,
     verifier_decision: u32,
     fail_config: Option<FailConfiguration>,
+    nary_type: NArySearchType,
 ) -> Result<Vec<String>, EmulatorError> {
     let mut challenge_log = ProverChallengeLog::load(checkpoint_path)?;
-    let base = challenge_log.base_step;
-
+    let nary_log = nary_type.get_prover_nary_log(&mut challenge_log);
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
 
     let new_base = match round {
-        1 => base,
-        _ => program_def
-            .nary_def()
-            .step_from_base_and_bits(round - 1, base, verifier_decision),
+        1 => nary_log.base_step,
+        _ => program_def.nary_def().step_from_base_and_bits(
+            round - 1,
+            nary_log.base_step,
+            verifier_decision,
+        ),
     };
 
-    challenge_log.base_step = new_base;
-    let hashes = program_def.get_round_hashes(
-        checkpoint_path,
-        round,
-        challenge_log.base_step,
-        fail_config,
-    )?;
-    challenge_log.hash_rounds.push(hashes.clone());
-    challenge_log.verifier_decisions.push(verifier_decision);
+    nary_log.base_step = new_base;
+    let hashes =
+        program_def.get_round_hashes(checkpoint_path, round, nary_log.base_step, fail_config)?;
+    nary_log.hash_rounds.push(hashes.clone());
+    nary_log.verifier_decisions.push(verifier_decision);
     challenge_log.save(checkpoint_path)?;
     Ok(hashes)
 }
@@ -155,30 +153,32 @@ pub fn verifier_choose_segment(
     round: u8,
     prover_last_hashes: Vec<String>,
     fail_config: Option<FailConfiguration>,
+    nary_type: NArySearchType,
 ) -> Result<u32, EmulatorError> {
     let mut challenge_log = VerifierChallengeLog::load(checkpoint_path)?;
-    let base = challenge_log.base_step;
-
+    let nary_log = nary_type.get_verifier_nary_log(&mut challenge_log);
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
 
-    let hashes = program_def.get_round_hashes(checkpoint_path, round, base, fail_config)?;
+    let hashes =
+        program_def.get_round_hashes(checkpoint_path, round, nary_log.base_step, fail_config)?;
 
     let claim_hashes = ExecutionHashes::from_hexstr(&prover_last_hashes);
     let my_hashes = ExecutionHashes::from_hexstr(&hashes);
 
     let (bits, base, new_selected) = choose_segment(
         &program_def.nary_def(),
-        base,
-        challenge_log.step_to_challenge,
+        nary_log.base_step,
+        nary_log.step_to_challenge,
         round,
         &claim_hashes,
         &my_hashes,
+        nary_type,
     );
-    challenge_log.base_step = base;
-    challenge_log.step_to_challenge = new_selected;
-    challenge_log.verifier_decisions.push(bits);
-    challenge_log.prover_hash_rounds.push(prover_last_hashes);
-    challenge_log.verifier_hash_rounds.push(hashes);
+    nary_log.base_step = base;
+    nary_log.step_to_challenge = new_selected;
+    nary_log.verifier_decisions.push(bits);
+    nary_log.prover_hash_rounds.push(prover_last_hashes);
+    nary_log.verifier_hash_rounds.push(hashes);
     challenge_log.save(checkpoint_path)?;
 
     info!("Verifier selects bits: {bits} base: {base} selection: {new_selected}");
@@ -191,24 +191,25 @@ pub fn prover_final_trace(
     checkpoint_path: &str,
     final_bits: u32,
     fail_config: Option<FailConfiguration>,
+    nary_type: NArySearchType,
 ) -> Result<TraceRWStep, EmulatorError> {
     let mut challenge_log = ProverChallengeLog::load(checkpoint_path)?;
-    let base = challenge_log.base_step;
+    let nary_log = nary_type.get_prover_nary_log(&mut challenge_log);
 
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
     let nary_def = program_def.nary_def();
 
     let total_rounds = nary_def.total_rounds();
-    let final_step = nary_def.step_from_base_and_bits(total_rounds, base, final_bits);
+    let final_step = nary_def.step_from_base_and_bits(total_rounds, nary_log.base_step, final_bits);
 
-    challenge_log.base_step = final_step;
-    challenge_log.verifier_decisions.push(final_bits);
+    nary_log.base_step = final_step;
+    nary_log.verifier_decisions.push(final_bits);
 
     info!("The prover needs to provide the full trace for the selected step {final_step}");
-    challenge_log.final_trace =
-        program_def.get_trace_step(checkpoint_path, final_step, fail_config)?;
+    let final_trace = program_def.get_trace_step(checkpoint_path, final_step, fail_config)?;
+    nary_log.final_trace = final_trace.clone();
     challenge_log.save(checkpoint_path)?;
-    Ok(challenge_log.final_trace)
+    Ok(final_trace)
 }
 
 pub fn get_hashes(
@@ -247,6 +248,8 @@ pub enum ForceChallenge {
     InitializedData,
     UninitializedData,
     AddressesSections,
+    ReadValueNArySearch,
+    ReadValue,
     No,
 }
 
@@ -277,12 +280,15 @@ pub fn verifier_choose_challenge(
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
     let program = program_def.load_program_from_checkpoint(checkpoint_path, 0)?;
     let nary_def = program_def.nary_def();
-    let verifier_log = VerifierChallengeLog::load(checkpoint_path)?;
 
+    let mut verifier_log = VerifierChallengeLog::load(checkpoint_path)?;
+    let conflict_step_log = &mut verifier_log.conflict_step_log;
+    conflict_step_log.final_trace = trace.clone();
+    
     let (step_hash, next_hash) = get_hashes(
-        &nary_def.step_mapping(&verifier_log.verifier_decisions),
-        &verifier_log.prover_hash_rounds,
-        verifier_log.step_to_challenge,
+        &nary_def.step_mapping(&conflict_step_log.verifier_decisions),
+        &conflict_step_log.prover_hash_rounds,
+        conflict_step_log.step_to_challenge,
     );
 
     // check trace_hash
@@ -304,7 +310,7 @@ pub fn verifier_choose_challenge(
         ));
     }
 
-    let step = verifier_log.step_to_challenge;
+    let step = conflict_step_log.step_to_challenge;
     let mut steps = vec![step, step + 1];
     let mut my_trace_idx = 1;
     if step > 0 {
@@ -409,6 +415,7 @@ pub fn verifier_choose_challenge(
         || force == ForceChallenge::InputData
         || force == ForceChallenge::InitializedData
         || force == ForceChallenge::UninitializedData
+        || force == ForceChallenge::ReadValueNArySearch
     {
         let (conflict_read, my_conflict_read, read_selector) = if is_read_1_conflict {
             (trace.read_1.clone(), my_trace.read_1.clone(), 1)
@@ -478,12 +485,86 @@ pub fn verifier_choose_challenge(
                     }),
                 ));
             }
+        } else {
+            let step_to_challenge = if conflict_last_step == LAST_STEP_INIT {
+                my_conflict_last_step
+            } else if my_conflict_last_step == LAST_STEP_INIT {
+                conflict_last_step
+            } else {
+                conflict_last_step.max(my_conflict_last_step)
+            };
+
+            let bits = nary_def.step_bits_for_round(1, step_to_challenge - 1);
+
+            let read_challenge_log = &mut verifier_log.read_challenge_log;
+            read_challenge_log.step_to_challenge = step_to_challenge - 1;
+            read_challenge_log.read_step = step_to_challenge - 1;
+            read_challenge_log.read_selector = read_selector;
+            read_challenge_log.base_step = 0;
+            read_challenge_log.verifier_decisions.push(bits);
+            read_challenge_log
+                .prover_hash_rounds
+                .push(conflict_step_log.prover_hash_rounds[0].clone());
+            verifier_log.save(checkpoint_path)?;
+
+            return Ok(ChallengeType::ReadValueNArySearch(bits));
         }
     }
-
+    verifier_log.save(checkpoint_path)?;
     Ok(ChallengeType::No)
 }
 
+pub fn verifier_choose_challenge_read_challenge(
+    program_definition_file: &str,
+    checkpoint_path: &str,
+    trace: TraceRWStep,
+    force: ForceChallenge,
+) -> Result<ChallengeType, EmulatorError> {
+    let program_def = ProgramDefinition::from_config(program_definition_file)?;
+    let nary_def = program_def.nary_def();
+    let verifier_log = VerifierChallengeLog::load(checkpoint_path)?;
+
+    let read_challenge_log = verifier_log.read_challenge_log;
+    let challenge_step = read_challenge_log.step_to_challenge;
+
+    let (step_hash, next_hash) = get_hashes(
+        &nary_def.step_mapping(&read_challenge_log.verifier_decisions),
+        &read_challenge_log.prover_hash_rounds,
+        challenge_step,
+    );
+
+    // check trace_hash
+    if (!validate_step_hash(&step_hash, &trace.trace_step, &next_hash)
+        && force == ForceChallenge::No)
+        || force == ForceChallenge::TraceHash
+    {
+        info!("Verifier choose to challenge TRACE_HASH");
+        return Ok(ChallengeType::TraceHash(
+            step_hash,
+            trace.trace_step,
+            next_hash,
+        ));
+    };
+
+    let read_step = read_challenge_log.read_step;
+    if (read_step == challenge_step && force == ForceChallenge::No)
+        || force == ForceChallenge::ReadValue
+    {
+        let conflict_step_trace = verifier_log.conflict_step_log.final_trace;
+        let read_1 = conflict_step_trace.read_1;
+        let read_2 = conflict_step_trace.read_2;
+        let read_selector = read_challenge_log.read_selector;
+
+        return Ok(ChallengeType::ReadValue {
+            read_1,
+            read_2,
+            read_selector,
+            trace,
+        });
+    }
+
+    Ok(ChallengeType::No)
+}
 /*
   TEST CASES
   ----------
@@ -636,6 +717,7 @@ mod tests {
                 round,
                 v_decision,
                 fail_config_prover.clone(),
+                NArySearchType::ConflictStep,
             )
             .unwrap();
             info!("{:?}", &hashes);
@@ -646,6 +728,7 @@ mod tests {
                 round,
                 hashes,
                 fail_config_verifier.clone(),
+                NArySearchType::ConflictStep,
             )
             .unwrap();
             info!("{:?}", v_decision);
@@ -655,8 +738,14 @@ mod tests {
 
         //PROVER PROVIDES EXECUTE STEP (and reveals full_trace)
         //Use v_desision + 1 as v_decision defines the last agreed step
-        let final_trace =
-            prover_final_trace(pdf, chk_prover_path, v_decision + 1, fail_config_prover).unwrap();
+        let final_trace = prover_final_trace(
+            pdf,
+            chk_prover_path,
+            v_decision + 1,
+            fail_config_prover,
+            NArySearchType::ConflictStep,
+        )
+        .unwrap();
         info!("Prover final trace: {:?}", final_trace.to_csv());
 
         let result = verify_script(&final_trace, REGISTERS_BASE_ADDRESS, &None);
diff --git a/emulator/src/decision/nary_search.rs b/emulator/src/decision/nary_search.rs
index 472c38c..a7b6af8 100644
--- a/emulator/src/decision/nary_search.rs
+++ b/emulator/src/decision/nary_search.rs
@@ -1,8 +1,41 @@
 use std::collections::HashMap;
 
+use clap::ValueEnum;
 use serde::Serialize;
 use tracing::{error, info};
 
+use crate::decision::execution_log::{
+    ProverChallengeLog, ProverNAryLog, VerifierChallengeLog, VerifierNAryLog,
+};
+
+#[derive(Clone, Copy, PartialEq, ValueEnum)]
+pub enum NArySearchType {
+    ConflictStep,
+    ReadValueChallenge,
+}
+
+impl NArySearchType {
+    pub fn get_prover_nary_log<'a>(
+        &'a self,
+        challenge_log: &'a mut ProverChallengeLog,
+    ) -> &'a mut ProverNAryLog {
+        match self {
+            Self::ConflictStep => &mut challenge_log.conflict_step_log,
+            Self::ReadValueChallenge => &mut challenge_log.read_challenge_log,
+        }
+    }
+
+    pub fn get_verifier_nary_log<'a>(
+        &'a self,
+        challenge_log: &'a mut VerifierChallengeLog,
+    ) -> &'a mut VerifierNAryLog {
+        match self {
+            Self::ConflictStep => &mut challenge_log.conflict_step_log,
+            Self::ReadValueChallenge => &mut challenge_log.read_challenge_log,
+        }
+    }
+}
+
 #[derive(Debug, Clone, Serialize)]
 pub struct NArySearchDefinition {
     pub max_steps: u64,
@@ -157,19 +190,26 @@ pub fn choose_segment(
     round: u8,
     prover_hashes: &ExecutionHashes,
     my_hashes: &ExecutionHashes,
+    nary_type: NArySearchType,
 ) -> (u32, u64, u64) {
     if prover_hashes.hashes.len() != my_hashes.hashes.len() {
         error!("Prover and my hashes should have the same length");
     }
 
     // finds if there is any difference in the hashes
-    let mut selection = prover_hashes.hashes.len() + 1;
+    let mut selection = if nary_type == NArySearchType::ConflictStep {
+        prover_hashes.hashes.len() + 1
+    } else {
+        1
+    };
     for i in 0..prover_hashes.hashes.len() {
         let prover_hash = &prover_hashes.hashes[i];
         let my_hash = &my_hashes.hashes[i];
         if prover_hash != my_hash {
             selection = i + 1;
-            break;
+            if nary_type == NArySearchType::ConflictStep {
+                break;
+            };
         }
     }
 
@@ -177,12 +217,19 @@ pub fn choose_segment(
     //println!("Selection: {}", selection);
     let mismatch_step = nary_defs.step_from_base_and_bits(round, base_step, selection as u32) - 1;
     //println!("Mismatch step: {}", mismatch_step);
-    let lower_limit_bits = if selected_step < mismatch_step {
-        nary_defs.step_bits_for_round(round, selected_step)
+    let (lower_limit_bits, choice) = if selected_step < mismatch_step {
+        if nary_type == NArySearchType::ConflictStep {
+            (nary_defs.step_bits_for_round(round, selected_step), selected_step)
+        } else {
+            (selection as u32, mismatch_step + 1)
+        }
     } else {
-        selection as u32 - 1
+        if nary_type == NArySearchType::ConflictStep {
+            (selection as u32 - 1, mismatch_step)
+        } else {
+            (nary_defs.step_bits_for_round(round, selected_step), selected_step)
+        }
     };
-    let choice = mismatch_step.min(selected_step);
 
     //println!("Lower limit bits: {}", lower_limit_bits);
     let base_step = nary_defs.step_from_base_and_bits(round, base_step, lower_limit_bits);
@@ -331,6 +378,7 @@ mod tests {
             round,
             &prover_hashes.into(),
             &my_hashes.into(),
+            NArySearchType::ConflictStep,
         );
         assert_eq!(bits, exp_bits);
         assert_eq!(base, exp_step);
diff --git a/emulator/src/main.rs b/emulator/src/main.rs
index dd1e8de..249a8c9 100644
--- a/emulator/src/main.rs
+++ b/emulator/src/main.rs
@@ -112,6 +112,10 @@ enum Commands {
         /// Command File to write the result
         #[arg(short, long, value_name = "COMMAND_PATH")]
         command_file: String,
+
+        /// Nary Search type
+        #[arg(short, long, value_name = "NARY_TYPE")]
+        nary_type: NArySearchType,
     },
 
     VerifierChooseSegment {
@@ -138,6 +142,10 @@ enum Commands {
         /// Command File to write the result
         #[arg(short, long, value_name = "COMMAND_PATH")]
         command_file: String,
+
+        /// Nary Search type
+        #[arg(short, long, value_name = "NARY_TYPE")]
+        nary_type: NArySearchType,
     },
 
     ProverFinalTrace {
@@ -160,6 +168,10 @@ enum Commands {
         /// Command File to write the result
         #[arg(short, long, value_name = "COMMAND_PATH")]
         command_file: String,
+
+        /// Nary Search type
+        #[arg(short, long, value_name = "NARY_TYPE")]
+        nary_type: NArySearchType,
     },
 
     VerifierChooseChallenge {
@@ -504,6 +516,7 @@ fn main() -> Result<(), EmulatorError> {
             v_decision,
             fail_config_prover,
             command_file,
+            nary_type,
         }) => {
             let result = prover_get_hashes_for_round(
                 pdf,
@@ -511,6 +524,7 @@ fn main() -> Result<(), EmulatorError> {
                 *round_number,
                 *v_decision,
                 fail_config_prover.clone(),
+                *nary_type,
             )?;
             info!("Prover get hashes for round: {:?}", result);
 
@@ -530,6 +544,7 @@ fn main() -> Result<(), EmulatorError> {
             hashes,
             fail_config_verifier,
             command_file,
+            nary_type,
         }) => {
             let result = verifier_choose_segment(
                 pdf,
@@ -537,6 +552,7 @@ fn main() -> Result<(), EmulatorError> {
                 *round_number,
                 hashes.clone(),
                 fail_config_verifier.clone(),
+                *nary_type,
             )?;
             info!("Verifier choose segment: {:?}", result);
 
@@ -555,12 +571,14 @@ fn main() -> Result<(), EmulatorError> {
             v_decision,
             fail_config_prover,
             command_file,
+            nary_type,
         }) => {
             let result: TraceRWStep = prover_final_trace(
                 pdf,
                 checkpoint_prover_path,
                 *v_decision,
                 fail_config_prover.clone(),
+                *nary_type,
             )?;
             info!("Prover final trace: {:?}", result);
 
diff --git a/emulator/tests/challenge.rs b/emulator/tests/challenge.rs
index e4cdbb3..03b1230 100644
--- a/emulator/tests/challenge.rs
+++ b/emulator/tests/challenge.rs
@@ -1,6 +1,6 @@
 use emulator::{
     constants::REGISTERS_BASE_ADDRESS,
-    decision::nary_search::{choose_segment, ExecutionHashes},
+    decision::nary_search::{choose_segment, ExecutionHashes, NArySearchType},
     executor::verifier::verify_script,
     loader::program_definition::ProgramDefinition,
 };
@@ -42,7 +42,7 @@ fn test_nary_search_trace_aux(input: u8, expect_err: bool, checkpoint_path: &str
         let my_hashes = ExecutionHashes::from_hexstr(&reply_hashes);
 
         let (bits, new_base, new_selected) =
-            choose_segment(&defs, base, selected, round, &claim_hashes, &my_hashes);
+            choose_segment(&defs, base, selected, round, &claim_hashes, &my_hashes, NArySearchType::ConflictStep);
         base = new_base;
         selected = new_selected;
 

From 6484cea21e76cdd207d0361ab1df31f07e8edab8 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 14:17:45 -0300
Subject: [PATCH 11/34] Add read challenge tests

---
 emulator/src/decision/challenge.rs        | 347 +++++++++++++++++++++-
 emulator/src/executor/fetcher.rs          |   8 +
 emulator/src/executor/utils.rs            |  34 ++-
 emulator/src/loader/program_definition.rs |  22 +-
 emulator/src/main.rs                      |  27 +-
 5 files changed, 427 insertions(+), 11 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 250596c..925bade 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -640,7 +640,7 @@ mod tests {
         constants::REGISTERS_BASE_ADDRESS,
         decision::challenge::*,
         executor::{
-            utils::{FailExecute, FailOpcode, FailReads, FailWrite},
+            utils::{FailExecute, FailOpcode, FailReads, FailTraceWrite, FailWrite},
             verifier::verify_script,
         },
         loader::program_definition::ProgramDefinition,
@@ -670,10 +670,13 @@ mod tests {
         input: u8,
         execute_err: bool,
         fail_config_prover: Option<FailConfiguration>,
+        fail_config_prover_read_challenge: Option<FailConfiguration>,
         fail_config_verifier: Option<FailConfiguration>,
+        fail_config_verifier_read_challenge: Option<FailConfiguration>,
         challenge_ok: bool,
         force_condition: ForceCondition,
         force: ForceChallenge,
+        force_read_challenge: ForceChallenge,
     ) {
         let pdf = &format!("../docker-riscv32/riscv32/build/{}", pdf);
         let input = vec![17, 17, 17, input];
@@ -768,10 +771,58 @@ mod tests {
             true,
         )
         .unwrap();
-        let result = execute_challenge(&challenge);
-        assert_eq!(result, challenge_ok);
 
+        let challenge = match &challenge {
+            ChallengeType::ReadValueNArySearch(bits) => {
+                let mut v_decision = *bits;
+                for round in 2..nary_def.total_rounds() + 1 {
+                    let hashes = prover_get_hashes_for_round(
+                        pdf,
+                        chk_prover_path,
+                        round,
+                        v_decision,
+                        fail_config_prover_read_challenge.clone(),
+                        NArySearchType::ReadValueChallenge,
+                    )
+                    .unwrap();
+                    info!("{:?}", &hashes);
+
+                    v_decision = verifier_choose_segment(
+                        pdf,
+                        chk_verifier_path,
+                        round,
+                        hashes,
+                        fail_config_verifier_read_challenge.clone(),
+                        NArySearchType::ReadValueChallenge,
+                    )
+                    .unwrap();
+                    info!("{:?}", v_decision);
+                }
+
+                let final_trace = prover_final_trace(
+                    pdf,
+                    chk_prover_path,
+                    v_decision + 1,
+                    fail_config_prover_read_challenge,
+                    NArySearchType::ReadValueChallenge,
+                )
+                .unwrap();
+                info!("Prover final trace: {:?}", final_trace.to_csv());
+
+                verifier_choose_challenge_read_challenge(
+                    pdf,
+                    chk_verifier_path,
+                    final_trace,
+                    force_read_challenge,
+                )
+                .unwrap()
+            }
+            _ => challenge,
+        };
+
+        let result = execute_challenge(&challenge);
         info!("Challenge: {:?} result: {}", challenge, result);
+        assert_eq!(result, challenge_ok);
     }
 
     #[test]
@@ -785,9 +836,12 @@ mod tests {
             true,
             None,
             None,
+            None,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
         //good input: expect execute step to succeed
         test_challenge_aux(
@@ -797,9 +851,12 @@ mod tests {
             false,
             None,
             None,
+            None,
+            None,
             false,
             ForceCondition::ValidInputStepAndHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
     }
 
@@ -815,9 +872,12 @@ mod tests {
             false,
             fail_hash.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
         test_challenge_aux(
             "4",
@@ -825,10 +885,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_hash,
+            None,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::TraceHash,
+            ForceChallenge::No,
         );
     }
 
@@ -844,9 +907,12 @@ mod tests {
             false,
             fail_hash.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
         test_challenge_aux(
             "6",
@@ -854,10 +920,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_hash,
+            None,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::TraceHashZero,
+            ForceChallenge::No,
         );
     }
 
@@ -872,9 +941,12 @@ mod tests {
             false,
             fail_entrypoint.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
         test_challenge_aux(
             "8",
@@ -882,10 +954,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_entrypoint,
+            None,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::EntryPoint,
+            ForceChallenge::No,
         );
     }
 
@@ -900,9 +975,12 @@ mod tests {
             false,
             fail_pc.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
         test_challenge_aux(
             "10",
@@ -910,10 +988,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_pc,
+            None,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::ProgramCounter,
+            ForceChallenge::No,
         );
     }
 
@@ -941,9 +1022,12 @@ mod tests {
             false,
             fail_read_2.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         test_challenge_aux(
@@ -952,10 +1036,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_read_2,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::InputData,
+            ForceChallenge::No,
         );
     }
 
@@ -993,9 +1080,12 @@ mod tests {
             false,
             fail_execute,
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         let fail_args = vec![
@@ -1019,10 +1109,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_read_2,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::AddressesSections,
+            ForceChallenge::No,
         );
     }
 
@@ -1060,9 +1153,12 @@ mod tests {
             false,
             fail_execute,
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         let fail_args = vec![
@@ -1086,10 +1182,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_read_2,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::AddressesSections,
+            ForceChallenge::No,
         );
     }
 
@@ -1124,9 +1223,12 @@ mod tests {
             false,
             fail_execute,
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         let fail_args = vec!["1106", "0xaa000000", "0x11111100", "0x00000000"]
@@ -1143,10 +1245,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_write,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::AddressesSections,
+            ForceChallenge::No,
         );
     }
 
@@ -1184,9 +1289,12 @@ mod tests {
             false,
             fail_execute,
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
         let fail_args = vec!["1106", "0xaa000000", "0x11111100", "0xf0000004"]
             .iter()
@@ -1202,10 +1310,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_write,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::AddressesSections,
+            ForceChallenge::No,
         );
     }
 
@@ -1243,9 +1354,12 @@ mod tests {
             false,
             fail_execute,
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         let fail_args = vec!["1106", "0xaa000000", "0x11111100", "0x80000000"]
@@ -1262,10 +1376,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_write,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::AddressesSections,
+            ForceChallenge::No,
         );
     }
 
@@ -1300,9 +1417,12 @@ mod tests {
             false,
             fail_execute.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         test_challenge_aux(
@@ -1311,10 +1431,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_execute,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::AddressesSections,
+            ForceChallenge::No,
         );
     }
 
@@ -1349,9 +1472,12 @@ mod tests {
             false,
             fail_execute.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         test_challenge_aux(
@@ -1360,10 +1486,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_execute,
+            None,
             false,
             ForceCondition::No,
             ForceChallenge::AddressesSections,
+            ForceChallenge::No,
         );
     }
 
@@ -1386,9 +1515,12 @@ mod tests {
             false,
             fail_opcode.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         test_challenge_aux(
@@ -1397,10 +1529,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_opcode,
+            None,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::Opcode,
+            ForceChallenge::No,
         );
     }
 
@@ -1436,9 +1571,12 @@ mod tests {
             false,
             fail_execute.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         test_challenge_aux(
@@ -1447,10 +1585,13 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_execute,
+            None,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::InitializedData,
+            ForceChallenge::No,
         );
     }
 
@@ -1480,9 +1621,12 @@ mod tests {
             false,
             fail_read_2.clone(),
             None,
+            None,
+            None,
             true,
             ForceCondition::No,
             ForceChallenge::No,
+            ForceChallenge::No,
         );
 
         test_challenge_aux(
@@ -1491,10 +1635,207 @@ mod tests {
             17,
             false,
             None,
+            None,
             fail_read_2,
+            None,
             false,
             ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::UninitializedData,
+            ForceChallenge::No,
+        );
+    }
+
+    #[test]
+    fn test_challenge_modified_value_lies_write_step_trace() {
+        init_trace();
+        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
+            .iter()
+            .map(|x| x.to_string())
+            .collect::<Vec<String>>();
+
+        let fail_read_2 = Some(FailConfiguration::new_fail_reads(FailReads::new(
+            None,
+            Some(&fail_read_args),
+        )));
+
+        let fail_trace_write_args = vec!["200", "0xaa000000", "0x11111100"]
+            .iter()
+            .map(|x| x.to_string())
+            .collect::<Vec<String>>();
+
+        let fail_trace_write = Some(FailConfiguration::new_fail_trace_write(
+            FailTraceWrite::new(&fail_trace_write_args),
+        ));
+
+        test_challenge_aux(
+            "33",
+            "hello-world.yaml",
+            17,
+            false,
+            fail_read_2.clone(),
+            fail_trace_write.clone(),
+            None,
+            None,
+            true,
+            ForceCondition::No,
+            ForceChallenge::No,
+            ForceChallenge::No,
+        );
+
+        test_challenge_aux(
+            "34",
+            "hello-world.yaml",
+            17,
+            false,
+            None,
+            None,
+            fail_read_2,
+            fail_trace_write,
+            false,
+            ForceCondition::ValidInputWrongStepOrHash,
+            ForceChallenge::ReadValueNArySearch,
+            ForceChallenge::TraceHash,
+        );
+    }
+
+    #[test]
+    fn test_challenge_modified_value_lies_all_hashes_from_write_step() {
+        init_trace();
+        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
+            .iter()
+            .map(|x| x.to_string())
+            .collect::<Vec<String>>();
+
+        let fail_read_2 = Some(FailConfiguration::new_fail_reads(FailReads::new(
+            None,
+            Some(&fail_read_args),
+        )));
+
+        let fail_write_args = vec!["200", "0xaa000000", "0x11111100", "0xaa000000"]
+            .iter()
+            .map(|x| x.to_string())
+            .collect::<Vec<String>>();
+        let fail_write = Some(FailConfiguration::new_fail_write(FailWrite::new(
+            &fail_write_args,
+        )));
+
+        test_challenge_aux(
+            "35",
+            "hello-world.yaml",
+            17,
+            false,
+            fail_read_2.clone(),
+            fail_write.clone(),
+            None,
+            None,
+            true,
+            ForceCondition::No,
+            ForceChallenge::No,
+            ForceChallenge::No,
+        );
+
+        test_challenge_aux(
+            "36",
+            "hello-world.yaml",
+            17,
+            false,
+            None,
+            None,
+            fail_read_2,
+            fail_write,
+            false,
+            ForceCondition::ValidInputWrongStepOrHash,
+            ForceChallenge::ReadValueNArySearch,
+            ForceChallenge::TraceHash,
+        );
+    }
+    #[test]
+    fn test_challenge_modified_value_lies_hashes_until_step() {
+        init_trace();
+        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
+            .iter()
+            .map(|x| x.to_string())
+            .collect::<Vec<String>>();
+
+        let fail_read_2 = Some(FailConfiguration::new_fail_reads(FailReads::new(
+            None,
+            Some(&fail_read_args),
+        )));
+
+        let fail_hash_until = Some(FailConfiguration::new_fail_hash_until(233));
+
+        test_challenge_aux(
+            "37",
+            "hello-world.yaml",
+            17,
+            false,
+            fail_read_2.clone(),
+            fail_hash_until.clone(),
+            None,
+            None,
+            true,
+            ForceCondition::No,
+            ForceChallenge::No,
+            ForceChallenge::No,
+        );
+
+        test_challenge_aux(
+            "38",
+            "hello-world.yaml",
+            17,
+            false,
+            None,
+            None,
+            fail_read_2,
+            fail_hash_until,
+            false,
+            ForceCondition::ValidInputWrongStepOrHash,
+            ForceChallenge::ReadValueNArySearch,
+            ForceChallenge::TraceHash,
+        );
+    }
+
+    #[test]
+    fn test_challenge_modified_value_doesnt_lie() {
+        init_trace();
+        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
+            .iter()
+            .map(|x| x.to_string())
+            .collect::<Vec<String>>();
+
+        let fail_read_2 = Some(FailConfiguration::new_fail_reads(FailReads::new(
+            None,
+            Some(&fail_read_args),
+        )));
+
+        test_challenge_aux(
+            "39",
+            "hello-world.yaml",
+            17,
+            false,
+            fail_read_2.clone(),
+            None,
+            None,
+            None,
+            true,
+            ForceCondition::No,
+            ForceChallenge::No,
+            ForceChallenge::No,
+        );
+
+        test_challenge_aux(
+            "40",
+            "hello-world.yaml",
+            17,
+            false,
+            None,
+            None,
+            fail_read_2,
+            None,
+            false,
+            ForceCondition::ValidInputWrongStepOrHash,
+            ForceChallenge::ReadValueNArySearch,
+            ForceChallenge::ReadValue,
         );
     }
 }
diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs
index 2484a8f..f701e4f 100644
--- a/emulator/src/executor/fetcher.rs
+++ b/emulator/src/executor/fetcher.rs
@@ -153,6 +153,14 @@ pub fn execute_program(
             }
         }
 
+        if let Some(fail_trace_write) = &fail_config.fail_trace_write {
+            if fail_trace_write.step == program.step {
+                if let Ok(trace) = trace.as_mut() {
+                    trace.trace_step.write_1 = fail_trace_write.trace_write.clone()
+                }
+            }
+        }
+
         if let Some(step) = mem_dump {
             if program.step == step {
                 info!("\n========== Dumping memory at step: {} ==========", step);
diff --git a/emulator/src/executor/utils.rs b/emulator/src/executor/utils.rs
index 113557e..633c843 100644
--- a/emulator/src/executor/utils.rs
+++ b/emulator/src/executor/utils.rs
@@ -1,6 +1,6 @@
 use std::str::FromStr;
 
-use bitvmx_cpu_definitions::trace::{TraceRWStep, TraceRead};
+use bitvmx_cpu_definitions::trace::{TraceRWStep, TraceRead, TraceWrite};
 use num_traits;
 
 use crate::loader::program::Program;
@@ -216,12 +216,32 @@ impl FailOpcode {
     }
 }
 
+#[derive(Clone, Debug, Serialize, Deserialize)]
+pub struct FailTraceWrite {
+    pub step: u64,
+    pub trace_write: TraceWrite,
+}
+
+impl FailTraceWrite {
+    pub fn new(args: &Vec<String>) -> Self {
+        Self {
+            step: parse_value::<u64>(&args[0]),
+            trace_write: TraceWrite {
+                address: parse_value::<u32>(&args[1]),
+                value: parse_value::<u32>(&args[2]),
+            },
+        }
+    }
+}
+
 #[derive(Clone, Debug, Default, Serialize, Deserialize)]
 pub struct FailConfiguration {
     pub fail_hash: Option<u64>,
+    pub fail_hash_until: Option<u64>,
     pub fail_execute: Option<FailExecute>,
     pub fail_reads: Option<FailReads>,
     pub fail_write: Option<FailWrite>,
+    pub fail_trace_write: Option<FailTraceWrite>,
     pub fail_pc: Option<u64>,
     pub fail_opcode: Option<FailOpcode>,
 }
@@ -233,6 +253,18 @@ impl FailConfiguration {
             ..Default::default()
         }
     }
+    pub fn new_fail_trace_write(fail_trace_write: FailTraceWrite) -> Self {
+        Self {
+            fail_trace_write: Some(fail_trace_write),
+            ..Default::default()
+        }
+    }
+    pub fn new_fail_hash_until(step: u64) -> Self {
+        Self {
+            fail_hash_until: Some(step),
+            ..Default::default()
+        }
+    }
     pub fn new_fail_execute(fail_execute: FailExecute) -> Self {
         Self {
             fail_execute: Some(fail_execute),
diff --git a/emulator/src/loader/program_definition.rs b/emulator/src/loader/program_definition.rs
index 74d0c70..31e8a2e 100644
--- a/emulator/src/loader/program_definition.rs
+++ b/emulator/src/loader/program_definition.rs
@@ -1,4 +1,4 @@
-use bitvmx_cpu_definitions::trace::TraceRWStep;
+use bitvmx_cpu_definitions::trace::{hash_to_string, TraceRWStep};
 use config::Config;
 use serde::Deserialize;
 
@@ -158,7 +158,7 @@ impl ProgramDefinition {
         steps.insert(0, base); //asks base step as it should be always obtainable
 
         let (_result, trace) =
-            self.execute_helper(checkpoint_path, vec![], Some(steps), fail_config)?;
+            self.execute_helper(checkpoint_path, vec![], Some(steps), fail_config.clone())?;
         // at least the base step should be present
         if trace.len() == 0 {
             return Err(EmulatorError::CantObtainTrace);
@@ -167,7 +167,23 @@ impl ProgramDefinition {
         // if there are actual steps skip the first one
         let skip = if trace.len() > 1 { 1 } else { 0 };
 
-        let mut ret: Vec<String> = trace.iter().skip(skip).map(|t| t.1.clone()).collect();
+        let fail_config = &fail_config.unwrap_or_default();
+
+        let mut ret: Vec<String> = trace.iter().skip(skip).map(|t| {
+            let mut hash = t.1.clone();
+
+            if let Some(step) = fail_config.fail_hash_until {
+                if t.0.step_number < step {
+                    let mut decoded = hex::decode(hash).unwrap();
+                    decoded[0] = decoded[0].wrapping_add(1);
+
+                    let new_hash: [u8; 20] = decoded.try_into().unwrap();
+                    hash = hash_to_string(&new_hash);
+                }
+            }
+
+            hash
+        }).collect();
         let obtained_hashes = ret.len();
 
         assert!(obtained_hashes <= required_hashes);
diff --git a/emulator/src/main.rs b/emulator/src/main.rs
index 249a8c9..bc8096b 100644
--- a/emulator/src/main.rs
+++ b/emulator/src/main.rs
@@ -3,13 +3,17 @@ use bitvmx_cpu_definitions::{challenge::EmulatorResultType, trace::TraceRWStep};
 use clap::{Parser, Subcommand};
 use emulator::{
     constants::REGISTERS_BASE_ADDRESS,
-    decision::challenge::{
-        prover_execute, prover_final_trace, prover_get_hashes_for_round, verifier_check_execution,
-        verifier_choose_challenge, verifier_choose_segment, ForceChallenge, ForceCondition,
+    decision::{
+        challenge::{
+            prover_execute, prover_final_trace, prover_get_hashes_for_round,
+            verifier_check_execution, verifier_choose_challenge, verifier_choose_segment,
+            ForceChallenge, ForceCondition,
+        },
+        nary_search::NArySearchType,
     },
     executor::{
         fetcher::execute_program,
-        utils::{FailConfiguration, FailExecute, FailOpcode, FailReads, FailWrite},
+        utils::{FailConfiguration, FailExecute, FailOpcode, FailReads, FailTraceWrite, FailWrite},
     },
     loader::program::{generate_rom_commitment, load_elf, Program},
     EmulatorError, ExecutionResult,
@@ -277,6 +281,12 @@ enum Commands {
         #[arg(long)]
         fail_hash: Option<u64>,
 
+        /// Fail producing hash but only for steps until a specific one.
+        /// fail_hash will propagate the error to the next steps due to the hash of a step depending on the previous hash.
+        /// this one doesn't since we modify the hash after all the hashes have been calculated in get_round_hashes
+        #[arg(long)]
+        fail_hash_until: Option<u64>,
+
         /// Fail producing the write value for a specific step
         #[arg(long, value_names = &["step", "fake_trace"], num_args = 2)]
         fail_execute: Option<Vec<String>>,
@@ -297,6 +307,10 @@ enum Commands {
         #[arg(long, value_names = &["step", "address_original", "value", "modified_address"], num_args = 4)]
         fail_write: Option<Vec<String>>,
 
+        /// Fail trace write **after** calculating the step hash
+        #[arg(long, value_names = &["step", "address", "value"])]
+        fail_trace_write: Option<Vec<String>>,
+
         /// Fail while reading the pc at the given step
         #[arg(long)]
         fail_pc: Option<u64>,
@@ -352,11 +366,13 @@ fn main() -> Result<(), EmulatorError> {
             sections,
             checkpoint_path,
             fail_hash,
+            fail_hash_until,
             fail_execute: fail_execute_args,
             list,
             fail_read_1: fail_read_1_args,
             fail_read_2: fail_read_2_args,
             fail_write: fail_write_args,
+            fail_trace_write: fail_trace_write_args,
             fail_opcode: fail_opcode_args,
             dump_mem,
             fail_pc,
@@ -416,11 +432,14 @@ fn main() -> Result<(), EmulatorError> {
             };
 
             let fail_write = fail_write_args.as_ref().map(FailWrite::new);
+            let fail_trace_write = fail_trace_write_args.as_ref().map(FailTraceWrite::new);
             let fail_opcode = fail_opcode_args.as_ref().map(FailOpcode::new);
 
             let debugvar = *debug;
             let fail_config = FailConfiguration {
                 fail_hash: *fail_hash,
+                fail_hash_until: *fail_hash_until,
+                fail_trace_write,
                 fail_execute,
                 fail_reads,
                 fail_write,

From 7a9d6cc9cdec568a25b2b3c06f6d6ffc22d5d7df Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 14:21:10 -0300
Subject: [PATCH 12/34] make find_section_idx public

---
 emulator/src/loader/program.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/emulator/src/loader/program.rs b/emulator/src/loader/program.rs
index 901fe24..54dc789 100644
--- a/emulator/src/loader/program.rs
+++ b/emulator/src/loader/program.rs
@@ -297,7 +297,7 @@ impl Program {
         self.sections.insert(pos, section);
     }
 
-    fn find_section_idx(&self, address: u32) -> Result<usize, ExecutionResult> {
+    pub fn find_section_idx(&self, address: u32) -> Result<usize, ExecutionResult> {
         // Binary search to find the appropriate section
         self.sections
             .binary_search_by(|section| {

From aec65665f7988b12fdf816c231028e00a3a216de Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 14:34:18 -0300
Subject: [PATCH 13/34] move variables out of nary log

---
 emulator/src/decision/challenge.rs     | 12 ++++++------
 emulator/src/decision/execution_log.rs |  6 ++++--
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 925bade..160de09 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -498,13 +498,13 @@ pub fn verifier_choose_challenge(
 
             let read_challenge_log = &mut verifier_log.read_challenge_log;
             read_challenge_log.step_to_challenge = step_to_challenge - 1;
-            read_challenge_log.read_step = step_to_challenge - 1;
-            read_challenge_log.read_selector = read_selector;
             read_challenge_log.base_step = 0;
             read_challenge_log.verifier_decisions.push(bits);
             read_challenge_log
-                .prover_hash_rounds
-                .push(conflict_step_log.prover_hash_rounds[0].clone());
+            .prover_hash_rounds
+            .push(conflict_step_log.prover_hash_rounds[0].clone());
+            verifier_log.read_step = step_to_challenge - 1;
+            verifier_log.read_selector = read_selector;
             verifier_log.save(checkpoint_path)?;
 
             return Ok(ChallengeType::ReadValueNArySearch(bits));
@@ -546,14 +546,14 @@ pub fn verifier_choose_challenge_read_challenge(
         ));
     };
 
-    let read_step = read_challenge_log.read_step;
+    let read_step = verifier_log.read_step;
     if (read_step == challenge_step && force == ForceChallenge::No)
         || force == ForceChallenge::ReadValue
     {
         let conflict_step_trace = verifier_log.conflict_step_log.final_trace;
         let read_1 = conflict_step_trace.read_1;
         let read_2 = conflict_step_trace.read_2;
-        let read_selector = read_challenge_log.read_selector;
+        let read_selector = verifier_log.read_selector;
 
         return Ok(ChallengeType::ReadValue {
             read_1,
diff --git a/emulator/src/decision/execution_log.rs b/emulator/src/decision/execution_log.rs
index 02e8ecd..3b580b1 100644
--- a/emulator/src/decision/execution_log.rs
+++ b/emulator/src/decision/execution_log.rs
@@ -58,9 +58,7 @@ impl ProverChallengeLog {
 #[derive(Debug, Serialize, Deserialize, Default)]
 pub struct VerifierNAryLog {
     pub base_step: u64,
-    pub read_selector: u8,
     pub step_to_challenge: u64,
-    pub read_step: u64,
     pub verifier_decisions: Vec<u32>,
     pub prover_hash_rounds: Vec<Vec<String>>,
     pub verifier_hash_rounds: Vec<Vec<String>>,
@@ -83,6 +81,8 @@ pub struct VerifierChallengeLog {
     pub input: Vec<u8>,
     pub conflict_step_log: VerifierNAryLog,
     pub read_challenge_log: VerifierNAryLog,
+    pub read_selector: u8,
+    pub read_step: u64,
 }
 
 impl VerifierChallengeLog {
@@ -98,6 +98,8 @@ impl VerifierChallengeLog {
             input,
             conflict_step_log: VerifierNAryLog::new(step_to_challenge),
             read_challenge_log: VerifierNAryLog::default(),
+            read_selector: 0,
+            read_step: 0,
         }
     }
 

From 558574c773d96cf9e506936c6c5519e7b8fbcb94 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 24 Jul 2025 17:33:20 -0300
Subject: [PATCH 14/34] cargo fmt

---
 bitcoin-script-riscv/src/riscv/challenges.rs |  4 +--
 emulator/src/decision/nary_search.rs         | 10 +++++--
 emulator/src/loader/program_definition.rs    | 30 +++++++++++---------
 emulator/tests/challenge.rs                  | 11 +++++--
 4 files changed, 36 insertions(+), 19 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index c4c8567..7eef5df 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -498,7 +498,7 @@ pub fn read_value_challenge(stack: &mut StackTracker) {
     stack.equality(read_step, false, init, true, true, false);
     is_lower_than(stack, read_step, write_step, true);
     stack.op_boolor();
-    
+
     stack.equality(write_addr, true, read_addr, true, true, false);
     stack.op_booland();
 
@@ -1531,7 +1531,7 @@ mod tests {
         stack.number_u32(write.address);
         stack.number_u32(write.value);
         stack.number_u64(write_step);
-        
+
         read_value_challenge(stack);
 
         stack.op_true();
diff --git a/emulator/src/decision/nary_search.rs b/emulator/src/decision/nary_search.rs
index a7b6af8..44bac67 100644
--- a/emulator/src/decision/nary_search.rs
+++ b/emulator/src/decision/nary_search.rs
@@ -219,7 +219,10 @@ pub fn choose_segment(
     //println!("Mismatch step: {}", mismatch_step);
     let (lower_limit_bits, choice) = if selected_step < mismatch_step {
         if nary_type == NArySearchType::ConflictStep {
-            (nary_defs.step_bits_for_round(round, selected_step), selected_step)
+            (
+                nary_defs.step_bits_for_round(round, selected_step),
+                selected_step,
+            )
         } else {
             (selection as u32, mismatch_step + 1)
         }
@@ -227,7 +230,10 @@ pub fn choose_segment(
         if nary_type == NArySearchType::ConflictStep {
             (selection as u32 - 1, mismatch_step)
         } else {
-            (nary_defs.step_bits_for_round(round, selected_step), selected_step)
+            (
+                nary_defs.step_bits_for_round(round, selected_step),
+                selected_step,
+            )
         }
     };
 
diff --git a/emulator/src/loader/program_definition.rs b/emulator/src/loader/program_definition.rs
index 31e8a2e..8d326e7 100644
--- a/emulator/src/loader/program_definition.rs
+++ b/emulator/src/loader/program_definition.rs
@@ -169,21 +169,25 @@ impl ProgramDefinition {
 
         let fail_config = &fail_config.unwrap_or_default();
 
-        let mut ret: Vec<String> = trace.iter().skip(skip).map(|t| {
-            let mut hash = t.1.clone();
-
-            if let Some(step) = fail_config.fail_hash_until {
-                if t.0.step_number < step {
-                    let mut decoded = hex::decode(hash).unwrap();
-                    decoded[0] = decoded[0].wrapping_add(1);
-
-                    let new_hash: [u8; 20] = decoded.try_into().unwrap();
-                    hash = hash_to_string(&new_hash);
+        let mut ret: Vec<String> = trace
+            .iter()
+            .skip(skip)
+            .map(|t| {
+                let mut hash = t.1.clone();
+
+                if let Some(step) = fail_config.fail_hash_until {
+                    if t.0.step_number < step {
+                        let mut decoded = hex::decode(hash).unwrap();
+                        decoded[0] = decoded[0].wrapping_add(1);
+
+                        let new_hash: [u8; 20] = decoded.try_into().unwrap();
+                        hash = hash_to_string(&new_hash);
+                    }
                 }
-            }
 
-            hash
-        }).collect();
+                hash
+            })
+            .collect();
         let obtained_hashes = ret.len();
 
         assert!(obtained_hashes <= required_hashes);
diff --git a/emulator/tests/challenge.rs b/emulator/tests/challenge.rs
index 03b1230..cd3be6f 100644
--- a/emulator/tests/challenge.rs
+++ b/emulator/tests/challenge.rs
@@ -41,8 +41,15 @@ fn test_nary_search_trace_aux(input: u8, expect_err: bool, checkpoint_path: &str
         let claim_hashes = ExecutionHashes::from_hexstr(&reply_hashes);
         let my_hashes = ExecutionHashes::from_hexstr(&reply_hashes);
 
-        let (bits, new_base, new_selected) =
-            choose_segment(&defs, base, selected, round, &claim_hashes, &my_hashes, NArySearchType::ConflictStep);
+        let (bits, new_base, new_selected) = choose_segment(
+            &defs,
+            base,
+            selected,
+            round,
+            &claim_hashes,
+            &my_hashes,
+            NArySearchType::ConflictStep,
+        );
         base = new_base;
         selected = new_selected;
 

From cd66611fba4a5844753a17ef1931206495ae7811 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 31 Jul 2025 12:06:19 -0300
Subject: [PATCH 15/34] Add verifier_choose_challenge_for_read_challenge to
 main commands

---
 emulator/src/decision/challenge.rs |  4 +--
 emulator/src/main.rs               | 45 ++++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+), 2 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 4e99466..73bb0cd 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -514,7 +514,7 @@ pub fn verifier_choose_challenge(
     Ok(ChallengeType::No)
 }
 
-pub fn verifier_choose_challenge_read_challenge(
+pub fn verifier_choose_challenge_for_read_challenge(
     program_definition_file: &str,
     checkpoint_path: &str,
     trace: TraceRWStep,
@@ -809,7 +809,7 @@ mod tests {
                 .unwrap();
                 info!("Prover final trace: {:?}", final_trace.to_csv());
 
-                verifier_choose_challenge_read_challenge(
+                verifier_choose_challenge_for_read_challenge(
                     pdf,
                     chk_verifier_path,
                     final_trace,
diff --git a/emulator/src/main.rs b/emulator/src/main.rs
index a38e6fd..df2e944 100644
--- a/emulator/src/main.rs
+++ b/emulator/src/main.rs
@@ -204,6 +204,28 @@ enum Commands {
         command_file: String,
     },
 
+    VerifierChooseChallengeForReadChallenge {
+        /// Yaml file to load
+        #[arg(short, long, value_name = "FILE")]
+        pdf: String,
+
+        /// Checkpoint verifier path
+        #[arg(short, long, value_name = "CHECKPOINT_VERIFIER_PATH")]
+        checkpoint_verifier_path: String,
+
+        /// Prover final trace
+        #[arg(short, long, value_name = "PROVER_FINAL_TRACE")]
+        prover_final_trace: TraceRWStep,
+
+        /// Force
+        #[arg(short, long, default_value = "no")]
+        force: ForceChallenge,
+
+        /// Command File to write the result
+        #[arg(short, long, value_name = "COMMAND_PATH")]
+        command_file: String,
+    },
+
     ///Generate the instruction mapping
     InstructionMapping,
 
@@ -636,6 +658,29 @@ fn main() -> Result<(), EmulatorError> {
             file.write_all(result.to_string().as_bytes())
                 .expect("Failed to write JSON to file");
         }
+        Some(Commands::VerifierChooseChallengeForReadChallenge {
+            pdf,
+            checkpoint_verifier_path,
+            prover_final_trace,
+            force,
+            command_file,
+        }) => {
+            let result = verifier_choose_challenge_for_read_challenge(
+                pdf,
+                checkpoint_verifier_path,
+                prover_final_trace.clone(),
+                force.clone(),
+            )?;
+            info!("Verifier choose challenge: {:?}", result);
+
+            let result = EmulatorResultType::VerifierChooseChallengeResult {
+                challenge: result.clone(),
+            }
+            .to_value()?;
+            let mut file = create_or_open_file(command_file);
+            file.write_all(result.to_string().as_bytes())
+                .expect("Failed to write JSON to file");
+        }
         None => {
             error!("No command specified");
         }

From 555e487a50740552a69b5f7bd222baddf6b4b2bb Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 31 Jul 2025 12:08:25 -0300
Subject: [PATCH 16/34] Fix verifier_check_execution fixed info messages and
 don't store logs if there is no disagreement

---
 emulator/src/decision/challenge.rs | 32 ++++++++++++------------------
 1 file changed, 13 insertions(+), 19 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 73bb0cd..6c0c947 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -99,25 +99,24 @@ pub fn verifier_check_execution(
     let mut should_challenge = true;
 
     if result == ExecutionResult::Halt(0, last_step) {
-        info!("The program executed successfully with the prover input");
-        info!("Do not challenge.");
-
         if claim_last_step != last_step || claim_last_hash != last_hash {
-            warn!("The prover provided a valid input, but the last step or hash differs");
-            warn!("Do not challenge (as the challenge is not waranteed to be successful)");
-            warn!("Report this case to be evaluated by the security team");
-            should_challenge = force_condition == ForceCondition::ValidInputWrongStepOrHash
-                || force_condition == ForceCondition::Always;
+            if force_condition == ForceCondition::ValidInputWrongStepOrHash {
+                should_challenge = true;
+            } else {
+                warn!("The prover provided a valid input, but the last step or hash differs");
+                warn!("Do not challenge (as the challenge is not waranteed to be successful)");
+                warn!("Report this case to be evaluated by the security team");
+            }
         } else {
-            should_challenge = force_condition == ForceCondition::ValidInputStepAndHash
-                || force_condition == ForceCondition::Always;
+            should_challenge = force_condition == ForceCondition::ValidInputStepAndHash;
         }
     }
 
-    // if !should_challenge {
-    //     // TODO: Should be removed after here, not creating challenge_log.
-    //     return Ok(None);
-    // }
+    if !should_challenge && force_condition != ForceCondition::Always {
+        info!("The program executed successfully with the prover input");
+        info!("Do not challenge.");
+        return Ok(None);
+    }
 
     warn!("There is a discrepancy between the prover and verifier execution");
     warn!("This execution will be challenged");
@@ -139,11 +138,6 @@ pub fn verifier_check_execution(
     );
     challenge_log.save(checkpoint_path)?;
 
-    if !should_challenge {
-        // TODO: Remove
-        return Ok(None);
-    }
-
     Ok(Some(step_to_challenge))
 }
 

From fd6292a3de673adf2aaa58e336e109c4f44564cd Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 31 Jul 2025 12:20:36 -0300
Subject: [PATCH 17/34] Make load traces compliant with RISC-V specification

---
 emulator/src/executor/fetcher.rs | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs
index e351cc9..d6f3234 100644
--- a/emulator/src/executor/fetcher.rs
+++ b/emulator/src/executor/fetcher.rs
@@ -988,16 +988,6 @@ pub fn op_load(
     x: &IType,
     program: &mut Program,
 ) -> Result<(TraceRead, TraceRead, TraceWrite, MemoryWitness), ExecutionResult> {
-    if x.rd() == REGISTER_ZERO as u32 {
-        program.pc.next_address();
-        return Ok((
-            TraceRead::default(),
-            TraceRead::default(),
-            TraceWrite::default(),
-            MemoryWitness::default(),
-        ));
-    }
-
     let micro = program.pc.get_micro();
 
     let (read_1, mut src_mem, alignment) = get_src_mem(&program.registers, x);
@@ -1083,8 +1073,22 @@ pub fn op_load(
             let value = program.registers.get(AUX_REGISTER_1);
             let read_1 = program.registers.to_trace_read(AUX_REGISTER_1);
 
-            program.registers.set(x.rd(), value, program.step);
             program.pc.next_address();
+
+            if x.rd() == REGISTER_ZERO as u32 {
+                return Ok((
+                    read_1,
+                    TraceRead::default(),
+                    TraceWrite::default(),
+                    MemoryWitness::new(
+                        MemoryAccessType::Register,
+                        MemoryAccessType::Unused,
+                        MemoryAccessType::Unused,
+                    ),
+                ));
+            }
+
+            program.registers.set(x.rd(), value, program.step);
             let write_1 = program.registers.to_trace_write(x.rd());
 
             (read_1, TraceRead::default(), write_1, MemoryWitness::rur())

From 2e52a40d78ab05def67c757c20b433c10f3f39db Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 31 Jul 2025 12:25:37 -0300
Subject: [PATCH 18/34] Don't allow sections with addresses lower than 0x1000

---
 emulator/src/loader/program.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/emulator/src/loader/program.rs b/emulator/src/loader/program.rs
index 5b1a67f..0a51627 100644
--- a/emulator/src/loader/program.rs
+++ b/emulator/src/loader/program.rs
@@ -286,6 +286,16 @@ impl Program {
                 }
             }
         }
+
+        let low_section = self.sections.iter().find(|section| section.start < 0x1000);
+
+        if let Some(low_section) = low_section {
+            return Err(EmulatorError::CantLoadPorgram(format!(
+                "Cannot load program: section '{}' starts at a low memory address (0x{:X}), which is below the allowed threshold of 0x1000.",
+                low_section.name,
+                low_section.start,
+            )));
+        }
         Ok(())
     }
 

From ca135964f359ec56e63af0168de7823212a0eb12 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Thu, 31 Jul 2025 12:26:26 -0300
Subject: [PATCH 19/34] Add flag to disable saving non-checkpoint steps

---
 emulator/src/decision/challenge.rs        | 61 +++++++++++++++++++----
 emulator/src/executor/fetcher.rs          | 25 ++++------
 emulator/src/loader/program.rs            | 24 +++++++++
 emulator/src/loader/program_definition.rs | 39 ++++++++++-----
 emulator/src/main.rs                      | 22 ++++++--
 emulator/tests/challenge.rs               |  8 +--
 emulator/tests/compliance.rs              |  1 +
 emulator/tests/exceptions.rs              |  1 +
 8 files changed, 136 insertions(+), 45 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 6c0c947..75506b2 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -28,10 +28,15 @@ pub fn prover_execute(
     checkpoint_path: &str,
     force: bool,
     fail_config: Option<FailConfiguration>,
+    save_non_checkpoint_steps: bool,
 ) -> Result<(ExecutionResult, u64, String), EmulatorError> {
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
-    let (result, last_step, last_hash) =
-        program_def.get_execution_result(input.clone(), checkpoint_path, fail_config)?;
+    let (result, last_step, last_hash) = program_def.get_execution_result(
+        input.clone(),
+        checkpoint_path,
+        fail_config,
+        save_non_checkpoint_steps,
+    )?;
     if result != ExecutionResult::Halt(0, last_step) {
         error!(
             "The execution of the program {} failed with error: {:?}. The claim should not be commited on-chain.",
@@ -62,6 +67,7 @@ pub fn prover_get_hashes_for_round(
     nary_type: NArySearchType,
 ) -> Result<Vec<String>, EmulatorError> {
     let mut challenge_log = ProverChallengeLog::load(checkpoint_path)?;
+    let input = challenge_log.input.clone();
     let nary_log = nary_type.get_prover_nary_log(&mut challenge_log);
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
 
@@ -75,8 +81,13 @@ pub fn prover_get_hashes_for_round(
     };
 
     nary_log.base_step = new_base;
-    let hashes =
-        program_def.get_round_hashes(checkpoint_path, round, nary_log.base_step, fail_config)?;
+    let hashes = program_def.get_round_hashes(
+        checkpoint_path,
+        input,
+        round,
+        nary_log.base_step,
+        fail_config,
+    )?;
     nary_log.hash_rounds.push(hashes.clone());
     nary_log.verifier_decisions.push(verifier_decision);
     challenge_log.save(checkpoint_path)?;
@@ -91,10 +102,15 @@ pub fn verifier_check_execution(
     claim_last_hash: &str,
     force_condition: ForceCondition,
     fail_config: Option<FailConfiguration>,
+    save_non_checkpoint_steps: bool,
 ) -> Result<Option<u64>, EmulatorError> {
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
-    let (result, last_step, last_hash) =
-        program_def.get_execution_result(input.clone(), checkpoint_path, fail_config)?;
+    let (result, last_step, last_hash) = program_def.get_execution_result(
+        input.clone(),
+        checkpoint_path,
+        fail_config,
+        save_non_checkpoint_steps,
+    )?;
 
     let mut should_challenge = true;
 
@@ -150,11 +166,18 @@ pub fn verifier_choose_segment(
     nary_type: NArySearchType,
 ) -> Result<u32, EmulatorError> {
     let mut challenge_log = VerifierChallengeLog::load(checkpoint_path)?;
+    let input = challenge_log.input.clone();
+
     let nary_log = nary_type.get_verifier_nary_log(&mut challenge_log);
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
 
-    let hashes =
-        program_def.get_round_hashes(checkpoint_path, round, nary_log.base_step, fail_config)?;
+    let hashes = program_def.get_round_hashes(
+        checkpoint_path,
+        input,
+        round,
+        nary_log.base_step,
+        fail_config,
+    )?;
 
     let claim_hashes = ExecutionHashes::from_hexstr(&prover_last_hashes);
     let my_hashes = ExecutionHashes::from_hexstr(&hashes);
@@ -188,6 +211,7 @@ pub fn prover_final_trace(
     nary_type: NArySearchType,
 ) -> Result<TraceRWStep, EmulatorError> {
     let mut challenge_log = ProverChallengeLog::load(checkpoint_path)?;
+    let input = challenge_log.input.clone();
     let nary_log = nary_type.get_prover_nary_log(&mut challenge_log);
 
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
@@ -200,7 +224,8 @@ pub fn prover_final_trace(
     nary_log.verifier_decisions.push(final_bits);
 
     info!("The prover needs to provide the full trace for the selected step {final_step}");
-    let final_trace = program_def.get_trace_step(checkpoint_path, final_step, fail_config)?;
+    let final_trace =
+        program_def.get_trace_step(checkpoint_path, input, final_step, fail_config)?;
     nary_log.final_trace = final_trace.clone();
     challenge_log.save(checkpoint_path)?;
     Ok(final_trace)
@@ -272,13 +297,19 @@ pub fn verifier_choose_challenge(
     return_script_parameters: bool,
 ) -> Result<ChallengeType, EmulatorError> {
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
-    let program = program_def.load_program_from_checkpoint(checkpoint_path, 0)?;
+    let mut program = program_def.load_program()?;
     let nary_def = program_def.nary_def();
 
     let mut verifier_log = VerifierChallengeLog::load(checkpoint_path)?;
     let conflict_step_log = &mut verifier_log.conflict_step_log;
     conflict_step_log.final_trace = trace.clone();
 
+    program.load_input(
+        verifier_log.input.clone(),
+        &program_def.input_section_name,
+        false,
+    )?;
+
     let (step_hash, next_hash) = get_hashes(
         &nary_def.step_mapping(&conflict_step_log.verifier_decisions),
         &conflict_step_log.prover_hash_rounds,
@@ -314,7 +345,13 @@ pub fn verifier_choose_challenge(
 
     //obtain all the steps needed
     let my_execution = program_def
-        .execute_helper(checkpoint_path, vec![], Some(steps), fail_config)?
+        .execute_helper(
+            checkpoint_path,
+            verifier_log.input.clone(),
+            Some(steps),
+            fail_config,
+            false,
+        )?
         .1;
     info!("execution: {:?}", my_execution);
     let my_trace = my_execution[my_trace_idx].0.clone();
@@ -687,6 +724,7 @@ mod tests {
             chk_prover_path,
             true,
             fail_config_prover.clone(),
+            false,
         )
         .unwrap();
         info!("{:?}", result_1);
@@ -700,6 +738,7 @@ mod tests {
             &result_1.2,
             force_condition,
             fail_config_verifier.clone(),
+            false,
         )
         .unwrap();
         info!("{:?}", result);
diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs
index d6f3234..45c7bfa 100644
--- a/emulator/src/executor/fetcher.rs
+++ b/emulator/src/executor/fetcher.rs
@@ -32,24 +32,17 @@ pub fn execute_program(
     trace_list: Option<Vec<u64>>,
     mem_dump: Option<u64>,
     fail_config: FailConfiguration,
+    save_non_checkpoint_steps: bool,
 ) -> (ExecutionResult, FullTrace) {
     let trace_set: Option<HashSet<u64>> = trace_list.map(|vec| vec.into_iter().collect());
 
     let mut traces = Vec::new();
 
-    if !input.is_empty() {
-        if let Some(section) = program.find_section_by_name_mut(input_section_name) {
-            let input_as_u32 = vec_u8_to_vec_u32(&input, little_endian);
-            for (i, byte) in input_as_u32.iter().enumerate() {
-                section.data[i] = *byte;
-            }
-        } else {
-            return (
-                ExecutionResult::SectionNotFound(input_section_name.to_string()),
-                traces,
-            );
-        }
+    let load_input_result = program.load_input(input.clone(), input_section_name, little_endian);
+    if load_input_result.is_err() {
+        return (load_input_result.err().unwrap(), traces);
     }
+
     let instruction_mapping = match verify_on_chain && use_instruction_mapping {
         true => Some(create_verification_script_mapping(
             program.registers.get_base_address(),
@@ -64,7 +57,9 @@ pub fn execute_program(
     if let Some(path) = &checkpoint_path {
         //create path if it does not exist
         std::fs::create_dir_all(path).unwrap();
-        program.serialize_to_file(path);
+        if save_non_checkpoint_steps {
+            program.serialize_to_file(path);
+        }
     }
 
     if print_trace && (trace_set.is_none() || trace_set.as_ref().unwrap().contains(&program.step)) {
@@ -189,7 +184,9 @@ pub fn execute_program(
         }
 
         if let Some(path) = &checkpoint_path {
-            if program.step % CHECKPOINT_SIZE == 0 || trace.is_err() || program.halt {
+            if program.step % CHECKPOINT_SIZE == 0
+                || ((trace.is_err() || program.halt) && save_non_checkpoint_steps)
+            {
                 program.serialize_to_file(path);
             }
         }
diff --git a/emulator/src/loader/program.rs b/emulator/src/loader/program.rs
index 0a51627..32c76ac 100644
--- a/emulator/src/loader/program.rs
+++ b/emulator/src/loader/program.rs
@@ -200,6 +200,30 @@ pub struct Program {
 }
 
 impl Program {
+    pub fn load_input(
+        &mut self,
+        input: Vec<u8>,
+        input_section_name: &str,
+        little_endian: bool,
+    ) -> Result<(), ExecutionResult> {
+        // if the step is non-zero then we are running the program from a checkpoint
+        // so we shouldn't rewrite the input. First, because it's already included in the checkpoint
+        // and second, because the input section is writable and the value could've been changed
+        if !input.is_empty() && self.step == 0 {
+            if let Some(section) = self.find_section_by_name_mut(input_section_name) {
+                let input_as_u32 = vec_u8_to_vec_u32(&input, little_endian);
+                for (i, byte) in input_as_u32.iter().enumerate() {
+                    section.data[i] = *byte;
+                }
+            } else {
+                return Err(ExecutionResult::SectionNotFound(
+                    input_section_name.to_string(),
+                ));
+            }
+        }
+
+        Ok(())
+    }
     pub fn serialize_to_file(&self, fpath: &str) {
         let fname = format!("{}/checkpoint.{}.json", fpath, self.step);
         let serialized = serde_json::to_string(self).unwrap();
diff --git a/emulator/src/loader/program_definition.rs b/emulator/src/loader/program_definition.rs
index 8d326e7..eaa79ff 100644
--- a/emulator/src/loader/program_definition.rs
+++ b/emulator/src/loader/program_definition.rs
@@ -72,15 +72,13 @@ impl ProgramDefinition {
             )));
         }
 
-        let mut checkpoint_step = 0;
-        loop {
-            if step < checkpoint_step + CHECKPOINT_SIZE {
-                break;
-            }
-            checkpoint_step += CHECKPOINT_SIZE;
-        }
+        let checkpoint_step = (step / CHECKPOINT_SIZE) * CHECKPOINT_SIZE;
 
-        Program::deserialize_from_file(checkpoint_path, checkpoint_step)
+        if checkpoint_step == 0 {
+            self.load_program()
+        } else {
+            Program::deserialize_from_file(checkpoint_path, checkpoint_step)
+        }
     }
 
     pub fn execute_helper(
@@ -89,6 +87,7 @@ impl ProgramDefinition {
         input_data: Vec<u8>,
         steps: Option<Vec<u64>>,
         fail_config: Option<FailConfiguration>,
+        save_non_checkpoint_steps: bool,
     ) -> Result<(ExecutionResult, FullTrace), EmulatorError> {
         let checkpoint_path_str = checkpoint_path.to_string();
         let (mut program, checkpoint_path, output_trace) = match &steps {
@@ -117,6 +116,7 @@ impl ProgramDefinition {
             steps,
             None,
             fail_config.unwrap_or_default(),
+            save_non_checkpoint_steps,
         ))
     }
 
@@ -125,9 +125,15 @@ impl ProgramDefinition {
         input_data: Vec<u8>,
         checkpoint_path: &str,
         fail_config: Option<FailConfiguration>,
+        save_non_checkpoint_steps: bool,
     ) -> Result<(ExecutionResult, u64, String), EmulatorError> {
-        let (result, trace) =
-            self.execute_helper(checkpoint_path, input_data, None, fail_config)?;
+        let (result, trace) = self.execute_helper(
+            checkpoint_path,
+            input_data,
+            None,
+            fail_config,
+            save_non_checkpoint_steps,
+        )?;
 
         if trace.len() == 0 {
             return Err(EmulatorError::CantObtainTrace);
@@ -145,6 +151,7 @@ impl ProgramDefinition {
     pub fn get_round_hashes(
         &self,
         checkpoint_path: &str,
+        input: Vec<u8>,
         round: u8,
         base: u64,
         fail_config: Option<FailConfiguration>,
@@ -157,8 +164,13 @@ impl ProgramDefinition {
         let required_hashes = steps.len();
         steps.insert(0, base); //asks base step as it should be always obtainable
 
-        let (_result, trace) =
-            self.execute_helper(checkpoint_path, vec![], Some(steps), fail_config.clone())?;
+        let (_result, trace) = self.execute_helper(
+            checkpoint_path,
+            input,
+            Some(steps),
+            fail_config.clone(),
+            false,
+        )?;
         // at least the base step should be present
         if trace.len() == 0 {
             return Err(EmulatorError::CantObtainTrace);
@@ -201,12 +213,13 @@ impl ProgramDefinition {
     pub fn get_trace_step(
         &self,
         checkpoint_path: &str,
+        input: Vec<u8>,
         step: u64,
         fail_config: Option<FailConfiguration>,
     ) -> Result<TraceRWStep, EmulatorError> {
         let steps = vec![step];
         let (_result, trace) =
-            self.execute_helper(checkpoint_path, vec![], Some(steps), fail_config)?;
+            self.execute_helper(checkpoint_path, input, Some(steps), fail_config, false)?;
         // at least the base step should be present
         if trace.len() == 0 {
             return Err(EmulatorError::CantObtainTrace);
diff --git a/emulator/src/main.rs b/emulator/src/main.rs
index df2e944..7522f50 100644
--- a/emulator/src/main.rs
+++ b/emulator/src/main.rs
@@ -5,9 +5,7 @@ use emulator::{
     constants::REGISTERS_BASE_ADDRESS,
     decision::{
         challenge::{
-            prover_execute, prover_final_trace, prover_get_hashes_for_round,
-            verifier_check_execution, verifier_choose_challenge, verifier_choose_segment,
-            ForceChallenge, ForceCondition,
+            prover_execute, prover_final_trace, prover_get_hashes_for_round, verifier_check_execution, verifier_choose_challenge, verifier_choose_challenge_for_read_challenge, verifier_choose_segment, ForceChallenge, ForceCondition
         },
         nary_search::NArySearchType,
     },
@@ -56,6 +54,10 @@ enum Commands {
         /// Command File to write the result
         #[arg(short, long, value_name = "COMMAND_PATH")]
         command_file: String,
+
+        /// Should we save steps that are not checkpoints (like first, error and halt steps)
+        #[arg(short, long, default_value = "true")]
+        save_non_checkpoint_steps: bool,
     },
 
     VerifierCheckExecution {
@@ -90,6 +92,10 @@ enum Commands {
         /// Command File to write the result
         #[arg(short, long, value_name = "COMMAND_PATH")]
         command_file: String,
+
+        /// Should we save steps that are not checkpoints (like first, error and halt steps)
+        #[arg(short, long, default_value = "true")]
+        save_non_checkpoint_steps: bool,
     },
 
     ProverGetHashesForRound {
@@ -344,6 +350,10 @@ enum Commands {
         /// Memory dump at given step
         #[arg(short, long)]
         dump_mem: Option<u64>,
+
+        /// Should we save steps that are not checkpoints (like first, error and halt steps)
+        #[arg(short, long, default_value = "true")]
+        save_non_checkpoint_steps: bool,
     },
 }
 
@@ -398,6 +408,7 @@ fn main() -> Result<(), EmulatorError> {
             fail_opcode: fail_opcode_args,
             dump_mem,
             fail_pc,
+            save_non_checkpoint_steps,
         }) => {
             if elf.is_none() && step.is_none() {
                 error!("To execute an elf file or a checkpoint step is required");
@@ -485,6 +496,7 @@ fn main() -> Result<(), EmulatorError> {
                 numbers,
                 *dump_mem,
                 fail_config,
+                *save_non_checkpoint_steps,
             )
             .0;
             info!("Execution result: {:?}", result);
@@ -496,6 +508,7 @@ fn main() -> Result<(), EmulatorError> {
             force,
             fail_config_prover,
             command_file,
+            save_non_checkpoint_steps,
         }) => {
             let input_bytes = hex::decode(input).expect("Invalid hex string");
             let result = prover_execute(
@@ -504,6 +517,7 @@ fn main() -> Result<(), EmulatorError> {
                 checkpoint_prover_path,
                 *force,
                 fail_config_prover.clone(),
+                *save_non_checkpoint_steps,
             )?;
             info!("Prover execute: {:?}", result);
 
@@ -532,6 +546,7 @@ fn main() -> Result<(), EmulatorError> {
             force,
             fail_config_verifier,
             command_file,
+            save_non_checkpoint_steps,
         }) => {
             let input_bytes = hex::decode(input).expect("Invalid hex string");
             let result = verifier_check_execution(
@@ -542,6 +557,7 @@ fn main() -> Result<(), EmulatorError> {
                 claim_last_hash,
                 force.clone(),
                 fail_config_verifier.clone(),
+                *save_non_checkpoint_steps,
             )?;
             info!("Verifier checks execution: {:?}", result);
 
diff --git a/emulator/tests/challenge.rs b/emulator/tests/challenge.rs
index cd3be6f..388590c 100644
--- a/emulator/tests/challenge.rs
+++ b/emulator/tests/challenge.rs
@@ -19,9 +19,9 @@ fn test_nary_search_trace_aux(input: u8, expect_err: bool, checkpoint_path: &str
     let program_def = ProgramDefinition::from_config(program_definition_file).unwrap();
 
     let defs = program_def.nary_def();
-
+    let input = vec![17, 17, 17, input];
     let (_bad_result, last_step, _last_hash) = program_def
-        .get_execution_result(vec![17, 17, 17, input], checkpoint_path, None)
+        .get_execution_result(input.clone(), checkpoint_path, None, true)
         .unwrap();
 
     let challenge_selected_step = last_step.min(1500);
@@ -34,7 +34,7 @@ fn test_nary_search_trace_aux(input: u8, expect_err: bool, checkpoint_path: &str
     for round in 1..defs.total_rounds() + 1 {
         info!("Prover gets the steps required by the n-ary search round: {round}");
         let reply_hashes = program_def
-            .get_round_hashes(checkpoint_path, round, base, None)
+            .get_round_hashes(checkpoint_path, input.clone(), round, base, None)
             .unwrap(); //get_hashes(&bad_trace, &steps);
         info!("Hashes: {:?}", reply_hashes);
 
@@ -58,7 +58,7 @@ fn test_nary_search_trace_aux(input: u8, expect_err: bool, checkpoint_path: &str
 
     info!("The prover needs to provide the full trace for the selected step {selected}");
     let trace = program_def
-        .get_trace_step(checkpoint_path, selected, None)
+        .get_trace_step(checkpoint_path, input, selected, None)
         .unwrap();
 
     info!("{:?}", trace.to_csv());
diff --git a/emulator/tests/compliance.rs b/emulator/tests/compliance.rs
index 08d1dfa..eadacff 100644
--- a/emulator/tests/compliance.rs
+++ b/emulator/tests/compliance.rs
@@ -31,6 +31,7 @@ fn verify_file(
         None,
         None,
         FailConfiguration::default(),
+        false,
     ))
 }
 
diff --git a/emulator/tests/exceptions.rs b/emulator/tests/exceptions.rs
index 0f17009..f74b527 100644
--- a/emulator/tests/exceptions.rs
+++ b/emulator/tests/exceptions.rs
@@ -32,6 +32,7 @@ fn verify_file(
         None,
         None,
         FailConfiguration::default(),
+        false,
     ))
 }
 

From d7302b0142078b855663d4add9cd8d1d00139158 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Fri, 1 Aug 2025 11:05:24 -0300
Subject: [PATCH 20/34] Fixed verifier_check_execution info messages again

---
 emulator/src/decision/challenge.rs | 32 ++++++++++++++----------------
 1 file changed, 15 insertions(+), 17 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 75506b2..4f2a2ea 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -112,25 +112,23 @@ pub fn verifier_check_execution(
         save_non_checkpoint_steps,
     )?;
 
-    let mut should_challenge = true;
-
-    if result == ExecutionResult::Halt(0, last_step) {
-        if claim_last_step != last_step || claim_last_hash != last_hash {
-            if force_condition == ForceCondition::ValidInputWrongStepOrHash {
-                should_challenge = true;
-            } else {
-                warn!("The prover provided a valid input, but the last step or hash differs");
-                warn!("Do not challenge (as the challenge is not waranteed to be successful)");
-                warn!("Report this case to be evaluated by the security team");
-            }
+    let input_is_valid = result == ExecutionResult::Halt(0, last_step);
+    let same_step_and_hash = last_step == claim_last_step && last_hash == claim_last_hash;
+
+    let should_challenge = force_condition == ForceCondition::Always
+        || !input_is_valid
+        || (force_condition == ForceCondition::ValidInputWrongStepOrHash && !same_step_and_hash)
+        || (force_condition == ForceCondition::ValidInputStepAndHash && same_step_and_hash);
+
+    if !should_challenge {
+        if same_step_and_hash {
+            info!("The program executed successfully with the prover input");
+            info!("Do not challenge.");
         } else {
-            should_challenge = force_condition == ForceCondition::ValidInputStepAndHash;
+            warn!("The prover provided a valid input, but the last step or hash differs");
+            warn!("Do not challenge (as the challenge is not guaranteed to be successful)");
+            warn!("Report this case to be evaluated by the security team");
         }
-    }
-
-    if !should_challenge && force_condition != ForceCondition::Always {
-        info!("The program executed successfully with the prover input");
-        info!("Do not challenge.");
         return Ok(None);
     }
 

From 3679a01f94ff1918a7f738af48bf0baa5c958c1a Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Fri, 1 Aug 2025 11:29:28 -0300
Subject: [PATCH 21/34] Fix incorrect force_condition in some tests

---
 emulator/src/decision/challenge.rs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 4f2a2ea..c4ac3eb 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -1280,7 +1280,7 @@ mod tests {
             fail_write,
             None,
             false,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::AddressesSections,
             ForceChallenge::No,
         );
@@ -1345,7 +1345,7 @@ mod tests {
             fail_write,
             None,
             false,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::AddressesSections,
             ForceChallenge::No,
         );
@@ -1411,7 +1411,7 @@ mod tests {
             fail_write,
             None,
             false,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::AddressesSections,
             ForceChallenge::No,
         );
@@ -1708,7 +1708,7 @@ mod tests {
             None,
             None,
             true,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
             ForceChallenge::No,
         );
@@ -1760,7 +1760,7 @@ mod tests {
             None,
             None,
             true,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
             ForceChallenge::No,
         );
@@ -1805,7 +1805,7 @@ mod tests {
             None,
             None,
             true,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
             ForceChallenge::No,
         );
@@ -1849,7 +1849,7 @@ mod tests {
             None,
             None,
             true,
-            ForceCondition::No,
+            ForceCondition::ValidInputWrongStepOrHash,
             ForceChallenge::No,
             ForceChallenge::No,
         );

From b1bff7cd7e0f28b219b61868dbed6dd521728911 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Mon, 4 Aug 2025 15:01:55 -0300
Subject: [PATCH 22/34] Don't allow sections next to the stack sections If
 there is a stack overflow, the stack pointer will point to an address outside
 of the stack section. If there are no sections next to the stack section then
 it will cause a segmentation fault for accessing an invalid address

---
 emulator/src/loader/program.rs | 36 ++++++++++++++++++++++++++++++----
 1 file changed, 32 insertions(+), 4 deletions(-)

diff --git a/emulator/src/loader/program.rs b/emulator/src/loader/program.rs
index 32c76ac..4dc4658 100644
--- a/emulator/src/loader/program.rs
+++ b/emulator/src/loader/program.rs
@@ -294,7 +294,7 @@ impl Program {
         }
     }
 
-    pub fn sanity_check(&self) -> Result<(), EmulatorError> {
+    pub fn sanity_check(&self, sp_base_address: Option<u32>) -> Result<(), EmulatorError> {
         //check overlapping sections
         for i in 0..self.sections.len() {
             for j in i + 1..self.sections.len() {
@@ -312,7 +312,6 @@ impl Program {
         }
 
         let low_section = self.sections.iter().find(|section| section.start < 0x1000);
-
         if let Some(low_section) = low_section {
             return Err(EmulatorError::CantLoadPorgram(format!(
                 "Cannot load program: section '{}' starts at a low memory address (0x{:X}), which is below the allowed threshold of 0x1000.",
@@ -320,6 +319,35 @@ impl Program {
                 low_section.start,
             )));
         }
+
+        if sp_base_address.is_none() {
+            return Ok(());
+        }
+
+        let stack_section = self.find_section(sp_base_address.unwrap());
+
+        if stack_section.is_err() {
+            return Ok(());
+        }
+
+        let stack_section = stack_section.unwrap();
+
+        let section_next_to_stack = self.sections.iter().find(|&other_section| {
+            let stack_section_end = stack_section.start + stack_section.size;
+            let other_section_end = other_section.start + other_section.size;
+
+            (other_section != stack_section)
+                && (stack_section_end == other_section.start
+                    || other_section_end == stack_section.start)
+        });
+
+        if let Some(section_next_to_stack) = section_next_to_stack {
+            return Err(EmulatorError::CantLoadPorgram(format!(
+                "Cannot load program: section '{}' is next to the stack section and a stack overflow could corrupt its content",
+                section_next_to_stack.name
+            )));
+        }
+
         Ok(())
     }
 
@@ -683,9 +711,9 @@ pub fn load_elf(fname: &str, show_sections: bool) -> Result<Program, EmulatorErr
         program.add_section(Section::new_with_data(&name, data, start, size, is_code, is_write, initialized));
     });
 
+    program.sanity_check(Some(STACK_BASE_ADDRESS))?;
     program.merge_sections();
     program.generate_sections_definitions();
-    program.sanity_check()?;
 
     Ok(program)
 }
@@ -777,7 +805,7 @@ mod tests {
         let mut program = Program::new(0, 0, 0);
         program.add_section(Section::new("test_1", 0, 10, false, true, false));
         program.add_section(Section::new("test_2", 9, 5, false, true, false));
-        assert!(program.sanity_check().is_err());
+        assert!(program.sanity_check(None).is_err());
     }
 
     #[test]

From e4167ffb964e5e0c9d8e3d280a568e42aaea1ef5 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 6 Aug 2025 11:59:39 -0300
Subject: [PATCH 23/34] fix first base step in nary search for read_value
 challenge

---
 emulator/src/decision/challenge.rs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index c4ac3eb..31587e2 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -527,7 +527,7 @@ pub fn verifier_choose_challenge(
 
             let read_challenge_log = &mut verifier_log.read_challenge_log;
             read_challenge_log.step_to_challenge = step_to_challenge - 1;
-            read_challenge_log.base_step = 0;
+            read_challenge_log.base_step = nary_def.step_from_base_and_bits(1, 0, bits);
             read_challenge_log.verifier_decisions.push(bits);
             read_challenge_log
                 .prover_hash_rounds
@@ -1732,7 +1732,7 @@ mod tests {
     #[test]
     fn test_challenge_modified_value_lies_all_hashes_from_write_step() {
         init_trace();
-        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
+        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "600"]
             .iter()
             .map(|x| x.to_string())
             .collect::<Vec<String>>();
@@ -1742,7 +1742,7 @@ mod tests {
             Some(&fail_read_args),
         )));
 
-        let fail_write_args = vec!["200", "0xaa000000", "0x11111100", "0xaa000000"]
+        let fail_write_args = vec!["600", "0xaa000000", "0x11111100", "0xaa000000"]
             .iter()
             .map(|x| x.to_string())
             .collect::<Vec<String>>();
@@ -1783,7 +1783,7 @@ mod tests {
     #[test]
     fn test_challenge_modified_value_lies_hashes_until_step() {
         init_trace();
-        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
+        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "600"]
             .iter()
             .map(|x| x.to_string())
             .collect::<Vec<String>>();
@@ -1793,7 +1793,7 @@ mod tests {
             Some(&fail_read_args),
         )));
 
-        let fail_hash_until = Some(FailConfiguration::new_fail_hash_until(233));
+        let fail_hash_until = Some(FailConfiguration::new_fail_hash_until(700));
 
         test_challenge_aux(
             "37",
@@ -1829,7 +1829,7 @@ mod tests {
     #[test]
     fn test_challenge_modified_value_doesnt_lie() {
         init_trace();
-        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
+        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "600"]
             .iter()
             .map(|x| x.to_string())
             .collect::<Vec<String>>();

From 0e14a127579155adff9cf75b2431083c938ade95 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 6 Aug 2025 12:00:46 -0300
Subject: [PATCH 24/34] Optimize read value challenge We don't need the final
 trace of the prover, the verifier can already challenge using his trace and
 the hashes given by the prover

---
 bitcoin-script-riscv/src/riscv/challenges.rs | 226 ++++++++++++++++---
 definitions/src/challenge.rs                 |  11 +-
 emulator/src/decision/challenge.rs           | 109 ++++-----
 emulator/src/main.rs                         |  15 +-
 4 files changed, 256 insertions(+), 105 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index 7eef5df..6e79f11 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -471,8 +471,15 @@ pub fn read_value_challenge(stack: &mut StackTracker) {
 
     let read_selector = stack.define(2, "read_selector");
 
+    let step_hash = stack.define(40, "step_hash");
+
     let write_addr = stack.define(8, "write_addr");
     let write_value = stack.define(8, "write_value");
+    let write_pc = stack.define(8, "write_pc");
+    let write_micro = stack.define(2, "write_micro");
+
+    let next_hash = stack.define(40, "next_hash");
+
     let write_step = stack.define(16, "write_step");
 
     let [read_addr, read_value, read_step] = get_selected_vars(
@@ -482,13 +489,11 @@ pub fn read_value_challenge(stack: &mut StackTracker) {
         read_selector,
     );
 
-    stack.rename(read_step, "read_Step");
-
     // if read_step == write_step -> write_addr != read_addr || write_value != read_value
     stack.equality(read_step, false, write_step, false, true, false);
 
     stack.equality(write_addr, false, read_addr, false, false, false);
-    stack.equality(write_value, true, read_value, true, false, false);
+    stack.equality(write_value, false, read_value, true, false, false);
     stack.op_boolor();
     stack.op_booland();
 
@@ -499,12 +504,54 @@ pub fn read_value_challenge(stack: &mut StackTracker) {
     is_lower_than(stack, read_step, write_step, true);
     stack.op_boolor();
 
-    stack.equality(write_addr, true, read_addr, true, true, false);
+    stack.equality(write_addr, false, read_addr, true, true, false);
     stack.op_booland();
 
     stack.op_boolor();
 
     stack.op_verify();
+
+    //save the hash to compare
+    stack.to_altstack();
+
+    stack.explode(step_hash);
+    stack.explode(write_addr);
+    stack.explode(write_value);
+    stack.explode(write_pc);
+    stack.explode(write_micro);
+
+    let result = blake3::blake3(stack, (40 + 8 + 8 + 8 + 2) / 2, 5);
+    stack.from_altstack();
+    stack.equals(result, true, next_hash, true);
+}
+
+pub fn correct_hash_challenge(stack: &mut StackTracker) {
+    stack.clear_definitions();
+
+    let prover_hash = stack.define(40, "prover_hash");
+    let verifier_hash = stack.define(40, "verifier_hash");
+
+    let write_addr = stack.define(8, "write_addr");
+    let write_value = stack.define(8, "write_value");
+    let write_pc = stack.define(8, "write_pc");
+    let write_micro = stack.define(2, "write_micro");
+
+    let next_hash = stack.define(40, "next_hash");
+
+    stack.not_equal(prover_hash, true, verifier_hash, false);
+
+    //save the hash to compare
+    stack.to_altstack();
+
+    stack.explode(verifier_hash);
+    stack.explode(write_addr);
+    stack.explode(write_value);
+    stack.explode(write_pc);
+    stack.explode(write_micro);
+
+    let result = blake3::blake3(stack, (40 + 8 + 8 + 8 + 2) / 2, 5);
+    stack.from_altstack();
+    stack.equals(result, true, next_hash, true);
 }
 
 //TODO: memory section challenge
@@ -622,7 +669,10 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
             read_1,
             read_2,
             read_selector,
+            step_hash,
             trace,
+            next_hash,
+            step,
         } => {
             stack.number_u32(read_1.address);
             stack.number_u32(read_1.value);
@@ -634,12 +684,37 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
 
             stack.byte(*read_selector);
 
-            stack.number_u32(trace.trace_step.write_1.address);
-            stack.number_u32(trace.trace_step.write_1.value);
-            stack.number_u64(trace.step_number);
+            stack.hexstr_as_nibbles(step_hash);
+
+            stack.number_u32(trace.get_write().address);
+            stack.number_u32(trace.get_write().value);
+            stack.number_u32(trace.get_pc().get_address());
+            stack.byte(trace.get_pc().get_micro());
+
+            stack.hexstr_as_nibbles(next_hash);
+
+            stack.number_u64(*step);
 
             read_value_challenge(&mut stack);
         }
+        ChallengeType::CorrectHash {
+            prover_hash,
+            verifier_hash,
+            trace,
+            next_hash,
+        } => {
+            stack.hexstr_as_nibbles(prover_hash);
+            stack.hexstr_as_nibbles(verifier_hash);
+
+            stack.number_u32(trace.get_write().address);
+            stack.number_u32(trace.get_write().value);
+            stack.number_u32(trace.get_pc().get_address());
+            stack.byte(trace.get_pc().get_micro());
+
+            stack.hexstr_as_nibbles(next_hash);
+
+            correct_hash_challenge(&mut stack);
+        }
         _ => {
             return false;
         }
@@ -653,7 +728,7 @@ mod tests {
 
     use bitvmx_cpu_definitions::{
         memory::MemoryWitness,
-        trace::{TraceRead, TraceWrite},
+        trace::{ProgramCounter, TraceRead, TraceStep, TraceWrite},
     };
 
     use super::*;
@@ -862,6 +937,72 @@ mod tests {
         ));
     }
 
+    fn test_correct_hash_aux(
+        prover_hash: &str,
+        verifier_hash: &str,
+        write_add: u32,
+        write_value: u32,
+        pc: u32,
+        micro: u8,
+        next_hash: &str,
+    ) -> bool {
+        let mut stack = StackTracker::new();
+
+        stack.hexstr_as_nibbles(prover_hash);
+        stack.hexstr_as_nibbles(verifier_hash);
+
+        stack.number_u32(write_add);
+        stack.number_u32(write_value);
+        stack.number_u32(pc);
+        stack.byte(micro);
+
+        stack.hexstr_as_nibbles(next_hash);
+
+        correct_hash_challenge(&mut stack);
+
+        stack.op_true();
+        stack.run().success
+    }
+
+    #[test]
+    fn test_correct_hash() {
+        let wrong_hash = "006942ae363a1a52823aa28eebe597d32b9d92e9";
+        let correct_hash = "e2f115006467b4b1b2b27612bbfd40ed3bc8299b";
+        let next_hash = "345721506e79c53d2549fc63d02ba8fc3b17efa4";
+
+        // can't challenge if prover has same hash
+        assert!(!test_correct_hash_aux(
+            correct_hash,
+            correct_hash,
+            0xf0000028,
+            0x00000001,
+            0x8000010c,
+            0x00,
+            next_hash
+        ));
+
+        // can't challenge if verifier has wrong hash
+        assert!(!test_correct_hash_aux(
+            correct_hash,
+            wrong_hash,
+            0xf0000028,
+            0x00000001,
+            0x8000010c,
+            0x00,
+            next_hash
+        ));
+
+        // challenge is valid if prover has wrong hash and verifier correct hash
+        assert!(test_correct_hash_aux(
+            wrong_hash,
+            correct_hash,
+            0xf0000028,
+            0x00000001,
+            0x8000010c,
+            0x00,
+            next_hash
+        ));
+    }
     #[test]
     fn test_padding_hash() {
         let pre_hash = "006942ae363a1a52823aa28eebe597d32b9d92e9";
@@ -1515,7 +1656,13 @@ mod tests {
         ));
     }
 
-    fn test_read_value_aux(read: TraceRead, write: TraceWrite, write_step: u64) -> bool {
+    fn test_read_value_aux(
+        read: TraceRead,
+        trace: &TraceStep,
+        step_hash: &str,
+        next_hash: &str,
+        write_step: u64,
+    ) -> bool {
         let stack = &mut StackTracker::new();
 
         stack.number_u32(read.address);
@@ -1528,8 +1675,15 @@ mod tests {
 
         stack.byte(1);
 
-        stack.number_u32(write.address);
-        stack.number_u32(write.value);
+        stack.hexstr_as_nibbles(&step_hash);
+
+        stack.number_u32(trace.get_write().address);
+        stack.number_u32(trace.get_write().value);
+        stack.number_u32(trace.get_pc().get_address());
+        stack.byte(trace.get_pc().get_micro());
+
+        stack.hexstr_as_nibbles(&next_hash);
+
         stack.number_u64(write_step);
 
         read_value_challenge(stack);
@@ -1539,40 +1693,50 @@ mod tests {
     }
     #[test]
     fn test_read_value() {
+        let hash = "e2f115006467b4b1b2b27612bbfd40ed3bc8299b";
+        let next_hash = "345721506e79c53d2549fc63d02ba8fc3b17efa4";
+        let wrong_hash = "006942ae363a1a52823aa28eebe597d32b9d92e9";
+
+        let write_pc = ProgramCounter::new(0x8000010c, 0x00);
+        let write = TraceWrite::new(0xf0000028, 1);
+        let trace = &TraceStep::new(write, write_pc);
+
         // can't challenge if read is correct
-        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let read = TraceRead::new(0xf0000028, 1, 100);
         let step = 100;
-        let write = TraceWrite::new(0x1000_0000, 0);
-        assert!(!test_read_value_aux(read, write, step));
+        assert!(!test_read_value_aux(read, trace, hash, next_hash, step));
 
         // can't challenge if write is older
-        let read = TraceRead::new(0x1000_0000, 0, 100);
+        let read = TraceRead::new(0xf0000028, 0, 100);
         let step = 50;
-        let write = TraceWrite::new(0x1000_0000, 100);
-        assert!(!test_read_value_aux(read, write, step));
+        assert!(!test_read_value_aux(read, trace, hash, next_hash, step));
 
         // can't challenge if write is newer but for different address
         let read = TraceRead::new(0x1000_0000, 0, 100);
         let step = 200;
-        let write = TraceWrite::new(0x2000_0000, 100);
-        assert!(!test_read_value_aux(read, write, step));
+        assert!(!test_read_value_aux(read, trace, hash, next_hash, step));
 
-        // challenge is valid if write is newer for the same address
-        let read = TraceRead::new(0x1000_0000, 0, 100);
-        let write_step = 200;
-        let write = TraceWrite::new(0x1000_0000, 100);
-        assert!(test_read_value_aux(read, write, write_step));
+        // challenge is valid if write is newer for the same address and has correct hash
+        let read = TraceRead::new(0xf0000028, 0, 100);
+        let step = 200;
+        assert!(test_read_value_aux(
+            read.clone(),
+            trace,
+            hash,
+            next_hash,
+            step
+        ));
+        // can't challenge if hash is wrong
+        assert!(!test_read_value_aux(read, trace, hash, wrong_hash, step));
 
         // challenge is valid if write is at the same step but for different address
         let read = TraceRead::new(0x1000_0000, 0, 100);
-        let write_step = 100;
-        let write = TraceWrite::new(0x2000_0000, 100);
-        assert!(test_read_value_aux(read, write, write_step));
+        let step = 100;
+        assert!(test_read_value_aux(read, trace, hash, next_hash, step));
 
         // challenge is valid if write is at the same step for different address but different value
-        let read = TraceRead::new(0x1000_0000, 0, 100);
-        let write_step = 100;
-        let write = TraceWrite::new(0x1000_0000, 100);
-        assert!(test_read_value_aux(read, write, write_step));
+        let read = TraceRead::new(0xf0000028, 0, 100);
+        let step = 100;
+        assert!(test_read_value_aux(read, trace, hash, next_hash, step));
     }
 }
diff --git a/definitions/src/challenge.rs b/definitions/src/challenge.rs
index f838e89..06afe01 100644
--- a/definitions/src/challenge.rs
+++ b/definitions/src/challenge.rs
@@ -32,7 +32,16 @@ pub enum ChallengeType {
         read_1: TraceRead,
         read_2: TraceRead,
         read_selector: u8,
-        trace: TraceRWStep,
+        step_hash: String,
+        trace: TraceStep,
+        next_hash: String,
+        step: u64,
+    },
+    CorrectHash {
+        prover_hash: String,
+        verifier_hash: String,
+        trace: TraceStep,
+        next_hash: String,
     },
     No,
 }
diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 31587e2..48611c3 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -256,6 +256,7 @@ pub fn get_hashes(
 #[derive(Debug, Clone, Serialize, Deserialize, PartialEq, EnumString, Display, EnumIter)]
 #[strum(serialize_all = "snake_case")]
 pub enum ForceChallenge {
+    CorrectHash,
     TraceHash,
     TraceHashZero,
     EntryPoint,
@@ -529,9 +530,15 @@ pub fn verifier_choose_challenge(
             read_challenge_log.step_to_challenge = step_to_challenge - 1;
             read_challenge_log.base_step = nary_def.step_from_base_and_bits(1, 0, bits);
             read_challenge_log.verifier_decisions.push(bits);
+
             read_challenge_log
                 .prover_hash_rounds
                 .push(conflict_step_log.prover_hash_rounds[0].clone());
+
+            read_challenge_log
+                .verifier_hash_rounds
+                .push(conflict_step_log.verifier_hash_rounds[0].clone());
+
             verifier_log.read_step = step_to_challenge - 1;
             verifier_log.read_selector = read_selector;
             verifier_log.save(checkpoint_path)?;
@@ -546,7 +553,7 @@ pub fn verifier_choose_challenge(
 pub fn verifier_choose_challenge_for_read_challenge(
     program_definition_file: &str,
     checkpoint_path: &str,
-    trace: TraceRWStep,
+    fail_config: Option<FailConfiguration>,
     force: ForceChallenge,
 ) -> Result<ChallengeType, EmulatorError> {
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
@@ -562,18 +569,36 @@ pub fn verifier_choose_challenge_for_read_challenge(
         challenge_step,
     );
 
-    // check trace_hash
-    if (!validate_step_hash(&step_hash, &trace.trace_step, &next_hash)
-        && force == ForceChallenge::No)
-        || force == ForceChallenge::TraceHash
+    let (my_step_hash, my_next_hash) = get_hashes(
+        &nary_def.step_mapping(&read_challenge_log.verifier_decisions),
+        &read_challenge_log.verifier_hash_rounds,
+        challenge_step,
+    );
+
+    assert_eq!(next_hash, my_next_hash);
+
+    let my_execution = program_def
+        .execute_helper(
+            checkpoint_path,
+            verifier_log.input.clone(),
+            Some(vec![challenge_step + 1]),
+            fail_config,
+            false,
+        )?
+        .1;
+    info!("execution: {:?}", my_execution);
+    let my_trace = my_execution[0].0.clone();
+
+    if (step_hash != my_step_hash && force == ForceChallenge::No)
+        || force == ForceChallenge::CorrectHash
     {
-        info!("Verifier choose to challenge TRACE_HASH");
-        return Ok(ChallengeType::TraceHash(
-            step_hash,
-            trace.trace_step,
+        return Ok(ChallengeType::CorrectHash {
+            prover_hash: step_hash,
+            verifier_hash: my_step_hash,
+            trace: my_trace.trace_step,
             next_hash,
-        ));
-    };
+        });
+    }
 
     let read_step = verifier_log.read_step;
     if (read_step == challenge_step && force == ForceChallenge::No)
@@ -588,7 +613,10 @@ pub fn verifier_choose_challenge_for_read_challenge(
             read_1,
             read_2,
             read_selector,
-            trace,
+            step_hash,
+            trace: my_trace.trace_step,
+            next_hash,
+            step: challenge_step + 1,
         });
     }
 
@@ -669,7 +697,7 @@ mod tests {
         constants::REGISTERS_BASE_ADDRESS,
         decision::challenge::*,
         executor::{
-            utils::{FailExecute, FailOpcode, FailReads, FailTraceWrite, FailWrite},
+            utils::{FailExecute, FailOpcode, FailReads, FailWrite},
             verifier::verify_script,
         },
         loader::program_definition::ProgramDefinition,
@@ -843,7 +871,7 @@ mod tests {
                 verifier_choose_challenge_for_read_challenge(
                     pdf,
                     chk_verifier_path,
-                    final_trace,
+                    fail_config_verifier_read_challenge,
                     force_read_challenge,
                 )
                 .unwrap()
@@ -1676,59 +1704,6 @@ mod tests {
         );
     }
 
-    #[test]
-    fn test_challenge_modified_value_lies_write_step_trace() {
-        init_trace();
-        let fail_read_args = vec!["1106", "0xaa000000", "0x11111100", "0xaa000000", "200"]
-            .iter()
-            .map(|x| x.to_string())
-            .collect::<Vec<String>>();
-
-        let fail_read_2 = Some(FailConfiguration::new_fail_reads(FailReads::new(
-            None,
-            Some(&fail_read_args),
-        )));
-
-        let fail_trace_write_args = vec!["200", "0xaa000000", "0x11111100"]
-            .iter()
-            .map(|x| x.to_string())
-            .collect::<Vec<String>>();
-
-        let fail_trace_write = Some(FailConfiguration::new_fail_trace_write(
-            FailTraceWrite::new(&fail_trace_write_args),
-        ));
-
-        test_challenge_aux(
-            "33",
-            "hello-world.yaml",
-            17,
-            false,
-            fail_read_2.clone(),
-            fail_trace_write.clone(),
-            None,
-            None,
-            true,
-            ForceCondition::ValidInputWrongStepOrHash,
-            ForceChallenge::No,
-            ForceChallenge::No,
-        );
-
-        test_challenge_aux(
-            "34",
-            "hello-world.yaml",
-            17,
-            false,
-            None,
-            None,
-            fail_read_2,
-            fail_trace_write,
-            false,
-            ForceCondition::ValidInputWrongStepOrHash,
-            ForceChallenge::ReadValueNArySearch,
-            ForceChallenge::TraceHash,
-        );
-    }
-
     #[test]
     fn test_challenge_modified_value_lies_all_hashes_from_write_step() {
         init_trace();
diff --git a/emulator/src/main.rs b/emulator/src/main.rs
index 7522f50..4c7e446 100644
--- a/emulator/src/main.rs
+++ b/emulator/src/main.rs
@@ -5,7 +5,10 @@ use emulator::{
     constants::REGISTERS_BASE_ADDRESS,
     decision::{
         challenge::{
-            prover_execute, prover_final_trace, prover_get_hashes_for_round, verifier_check_execution, verifier_choose_challenge, verifier_choose_challenge_for_read_challenge, verifier_choose_segment, ForceChallenge, ForceCondition
+            prover_execute, prover_final_trace, prover_get_hashes_for_round,
+            verifier_check_execution, verifier_choose_challenge,
+            verifier_choose_challenge_for_read_challenge, verifier_choose_segment, ForceChallenge,
+            ForceCondition,
         },
         nary_search::NArySearchType,
     },
@@ -219,9 +222,9 @@ enum Commands {
         #[arg(short, long, value_name = "CHECKPOINT_VERIFIER_PATH")]
         checkpoint_verifier_path: String,
 
-        /// Prover final trace
-        #[arg(short, long, value_name = "PROVER_FINAL_TRACE")]
-        prover_final_trace: TraceRWStep,
+        /// Fail Configuration
+        #[arg(short, long, value_name = "FailConfigVerifier")]
+        fail_config_verifier: Option<FailConfiguration>,
 
         /// Force
         #[arg(short, long, default_value = "no")]
@@ -677,14 +680,14 @@ fn main() -> Result<(), EmulatorError> {
         Some(Commands::VerifierChooseChallengeForReadChallenge {
             pdf,
             checkpoint_verifier_path,
-            prover_final_trace,
+            fail_config_verifier,
             force,
             command_file,
         }) => {
             let result = verifier_choose_challenge_for_read_challenge(
                 pdf,
                 checkpoint_verifier_path,
-                prover_final_trace.clone(),
+                fail_config_verifier.clone(),
                 force.clone(),
             )?;
             info!("Verifier choose challenge: {:?}", result);

From ef41e49ef315efbae3333417f1581e4a6e1a88c9 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Mon, 25 Aug 2025 11:29:50 -0300
Subject: [PATCH 25/34] Revert "Make load traces compliant with RISC-V
 specification"

This reverts commit fd6292a3de673adf2aaa58e336e109c4f44564cd.
This change is being worked on a different branch
---
 emulator/src/executor/fetcher.rs | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs
index 45c7bfa..44dc5ed 100644
--- a/emulator/src/executor/fetcher.rs
+++ b/emulator/src/executor/fetcher.rs
@@ -985,6 +985,16 @@ pub fn op_load(
     x: &IType,
     program: &mut Program,
 ) -> Result<(TraceRead, TraceRead, TraceWrite, MemoryWitness), ExecutionResult> {
+    if x.rd() == REGISTER_ZERO as u32 {
+        program.pc.next_address();
+        return Ok((
+            TraceRead::default(),
+            TraceRead::default(),
+            TraceWrite::default(),
+            MemoryWitness::default(),
+        ));
+    }
+
     let micro = program.pc.get_micro();
 
     let (read_1, mut src_mem, alignment) = get_src_mem(&program.registers, x);
@@ -1070,22 +1080,8 @@ pub fn op_load(
             let value = program.registers.get(AUX_REGISTER_1);
             let read_1 = program.registers.to_trace_read(AUX_REGISTER_1);
 
-            program.pc.next_address();
-
-            if x.rd() == REGISTER_ZERO as u32 {
-                return Ok((
-                    read_1,
-                    TraceRead::default(),
-                    TraceWrite::default(),
-                    MemoryWitness::new(
-                        MemoryAccessType::Register,
-                        MemoryAccessType::Unused,
-                        MemoryAccessType::Unused,
-                    ),
-                ));
-            }
-
             program.registers.set(x.rd(), value, program.step);
+            program.pc.next_address();
             let write_1 = program.registers.to_trace_write(x.rd());
 
             (read_1, TraceRead::default(), write_1, MemoryWitness::rur())

From 75697231f24c399bf631a040ac2b0154e5a48f1c Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Mon, 8 Sep 2025 12:10:43 -0300
Subject: [PATCH 26/34] restore RomData Challenge

---
 bitcoin-script-riscv/src/riscv/challenges.rs | 98 ++++++++++++++++++++
 definitions/src/challenge.rs                 |  1 +
 2 files changed, 99 insertions(+)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index 6e79f11..9b06fcc 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -65,6 +65,46 @@ pub fn input_challenge(stack: &mut StackTracker, address: u32) {
     stack.op_verify();
 }
 
+// One rom value equivocation challenge
+// [WOTS_PROVER_READ_ADD_1|WOTS_PROVER_READ_VALUE_1|WOTS_PROVER_LAST_STEP_1|WOTS_PROVER_READ_ADD_2|WOTS_PROVER_READ_VALUE_2|WOTS_PROVER_LAST_STEP_2]
+// If STEP_1 == INIT && ADD_1 == const_address && VALUE_1 != const_value || STEP_2 == INIT && ADD_2 == const_address && VALUE_2 != const_value  => verifier wins
+pub fn rom_challenge(stack: &mut StackTracker, address: u32, value: u32) {
+    assert_ne!(address, 0x0000_0000);
+    stack.clear_definitions();
+    let add_1 = stack.define(8, "prover_read_add_1");
+    let read_1 = stack.define(8, "prover_read_value_1");
+    let prover_step_1 = stack.define(16, "prover_last_step_1");
+
+    let add_2 = stack.define(8, "prover_read_add_2");
+    let read_2 = stack.define(8, "prover_read_value_2");
+    let prover_step_2 = stack.define(16, "prover_last_step_2");
+
+    //compares agaisnt read_2
+    let init = stack.number_u64(LAST_STEP_INIT);
+    stack.equality(prover_step_2, true, init, true, true, false);
+    let const_value = stack.number_u32(value);
+    stack.equality(read_2, true, const_value, true, false, false);
+    let const_address = stack.number_u32(address);
+    stack.equality(add_2, true, const_address, true, true, false);
+    stack.op_booland();
+    stack.op_booland();
+
+    //compares agaisnt read_1
+    let init = stack.number_u64(LAST_STEP_INIT);
+    stack.equality(prover_step_1, true, init, true, true, false);
+    let const_value = stack.number_u32(value);
+    stack.equality(read_1, true, const_value, true, false, false);
+    let const_address = stack.number_u32(address);
+    stack.equality(add_1, true, const_address, true, true, false);
+
+    stack.op_booland();
+    stack.op_booland();
+
+    //one of the two needs to be right
+    stack.op_boolor();
+    stack.op_verify();
+}
+
 // If the prover executes step = 1 and entry_point != valid entry point
 // the verifier can execute this equivocation and win the challenge
 // [WOTS_PROVER_TRACE_PC:8 | WOTS_PROVER_TRACE_MICRO:2 | WOTS_PROVER_TRACE_STEP:16]
@@ -640,6 +680,15 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
 
             uninitialized_challenge(&mut stack, uninitialized_sections.as_ref().unwrap());
         }
+        ChallengeType::RomData(read_1, read_2 ,address, input_for_address ) => {
+            stack.number_u32(read_1.address);
+            stack.number_u32(read_1.value);
+            stack.number_u64(read_1.last_step);
+            stack.number_u32(read_2.address);
+            stack.number_u32(read_2.value);
+            stack.number_u64(read_2.last_step);
+            rom_challenge(&mut stack, *address, *input_for_address);
+        }
         ChallengeType::AddressesSections(
             read_1,
             read_2,
@@ -1020,6 +1069,55 @@ mod tests {
         ));
     }
 
+    fn test_rom_aux(read_1: &TraceRead, read_2: &TraceRead, rom_add: u32, rom_value: u32) -> bool {
+        let mut stack = StackTracker::new();
+
+        stack.number_u32(read_1.address);
+        stack.number_u32(read_1.value);
+        stack.number_u64(read_1.last_step);
+        stack.number_u32(read_2.address);
+        stack.number_u32(read_2.value);
+        stack.number_u64(read_2.last_step);
+
+        rom_challenge(&mut stack, rom_add, rom_value);
+
+        stack.op_true();
+        stack.run().success
+    }
+
+    #[test]
+    fn test_rom() {
+        //can't challenge not init state
+        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, 1);
+        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, 2);
+        assert!(!test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x0000_0000));
+
+        //can't challenge if value is right
+        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        assert!(!test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_5678));
+
+        //can't challenge if address is different
+        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        assert!(!test_rom_aux(&read_1, &read_2, 0x0000_0003, 0x1234_0000));
+
+        //challenge is valid if the address is the same but the value differs in both
+        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        assert!(test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_0000));
+
+        //challenge is valid if the address is the same but the value differs in read_1
+        let read_1 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x0000_0005, 0x1234_0000, LAST_STEP_INIT);
+        assert!(test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_0000));
+
+        //challenge is valid if the address is the same but the value differs in read_2
+        let read_1 = TraceRead::new(0x0000_0005, 0x1234_0000, LAST_STEP_INIT);
+        let read_2 = TraceRead::new(0x0000_0002, 0x1234_5678, LAST_STEP_INIT);
+        assert!(test_rom_aux(&read_1, &read_2, 0x0000_0002, 0x1234_0000));
+    }
+
     fn test_input_aux(
         read_1: &TraceRead,
         read_2: &TraceRead,
diff --git a/definitions/src/challenge.rs b/definitions/src/challenge.rs
index 06afe01..dca9477 100644
--- a/definitions/src/challenge.rs
+++ b/definitions/src/challenge.rs
@@ -16,6 +16,7 @@ pub enum ChallengeType {
     InputData(TraceRead, TraceRead, u32, u32),
     InitializedData(TraceRead, TraceRead, u8, u32, Option<Chunk>),
     UninitializedData(TraceRead, TraceRead, u8, Option<SectionDefinition>),
+    RomData(TraceRead, TraceRead, u32, u32),
     AddressesSections(
         TraceRead,
         TraceRead,

From 43b1cc351cc8b1715778e1c6a8f5912dcc2a88f1 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 10 Sep 2025 11:37:21 -0300
Subject: [PATCH 27/34] change var_selector type to number

---
 bitcoin-script-riscv/src/riscv/challenges.rs  | 22 +++++++++----------
 .../src/riscv/script_utils.rs                 | 10 ++++-----
 definitions/src/challenge.rs                  |  6 ++---
 emulator/src/decision/execution_log.rs        |  2 +-
 4 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index 9b06fcc..9fc25c6 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -442,7 +442,7 @@ pub fn initialized_challenge(stack: &mut StackTracker, chunk: &Chunk) {
     let read_value_2 = stack.define(8, "prover_read_value_2");
     let read_step_2 = stack.define(16, "prover_read_step_2");
 
-    let read_selector = stack.define(2, "read_selector");
+    let read_selector = stack.define(1, "read_selector");
 
     let [read_addr, read_value, read_step] = get_selected_vars(
         stack,
@@ -477,7 +477,7 @@ pub fn uninitialized_challenge(
     let read_value_2 = stack.define(8, "prover_read_value_2");
     let read_step_2 = stack.define(16, "prover_read_step_2");
 
-    let read_selector = stack.define(2, "read_selector");
+    let read_selector = stack.define(1, "read_selector");
 
     let [read_addr, read_value, read_step] = get_selected_vars(
         stack,
@@ -509,7 +509,7 @@ pub fn read_value_challenge(stack: &mut StackTracker) {
     let read_value_2 = stack.define(8, "prover_read_value_2");
     let read_step_2 = stack.define(16, "prover_read_step_2");
 
-    let read_selector = stack.define(2, "read_selector");
+    let read_selector = stack.define(1, "read_selector");
 
     let step_hash = stack.define(40, "step_hash");
 
@@ -663,7 +663,7 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
             stack.number_u32(read_2.value);
             stack.number_u64(read_2.last_step);
 
-            stack.byte(*read_selector);
+            stack.number(*read_selector);
 
             initialized_challenge(&mut stack, chunk.as_ref().unwrap());
         }
@@ -676,7 +676,7 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
             stack.number_u32(read_2.value);
             stack.number_u64(read_2.last_step);
 
-            stack.byte(*read_selector);
+            stack.number(*read_selector);
 
             uninitialized_challenge(&mut stack, uninitialized_sections.as_ref().unwrap());
         }
@@ -731,7 +731,7 @@ pub fn execute_challenge(challege_type: &ChallengeType) -> bool {
             stack.number_u32(read_2.value);
             stack.number_u64(read_2.last_step);
 
-            stack.byte(*read_selector);
+            stack.number(*read_selector);
 
             stack.hexstr_as_nibbles(step_hash);
 
@@ -1562,7 +1562,7 @@ mod tests {
     fn test_initialized_aux(
         read_1: &TraceRead,
         read_2: &TraceRead,
-        read_selector: u8,
+        read_selector: u32,
         chunk: &Chunk,
     ) -> bool {
         let mut stack = StackTracker::new();
@@ -1575,7 +1575,7 @@ mod tests {
         stack.number_u32(read_2.value);
         stack.number_u64(read_2.last_step);
 
-        stack.byte(read_selector);
+        stack.number(read_selector);
 
         initialized_challenge(&mut stack, chunk);
 
@@ -1630,7 +1630,7 @@ mod tests {
     fn test_uninitialized_aux(
         read_1: &TraceRead,
         read_2: &TraceRead,
-        read_selector: u8,
+        read_selector: u32,
         sections: &SectionDefinition,
     ) -> bool {
         let mut stack = StackTracker::new();
@@ -1643,7 +1643,7 @@ mod tests {
         stack.number_u32(read_2.value);
         stack.number_u64(read_2.last_step);
 
-        stack.byte(read_selector);
+        stack.number(read_selector);
 
         uninitialized_challenge(&mut stack, sections);
 
@@ -1771,7 +1771,7 @@ mod tests {
         stack.number_u32(read.value);
         stack.number_u64(read.last_step);
 
-        stack.byte(1);
+        stack.number(1);
 
         stack.hexstr_as_nibbles(&step_hash);
 
diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs
index 328c730..dc0564b 100644
--- a/bitcoin-script-riscv/src/riscv/script_utils.rs
+++ b/bitcoin-script-riscv/src/riscv/script_utils.rs
@@ -1468,9 +1468,9 @@ pub fn get_selected_vars<const N: usize>(
         stack.move_var(*var_2);
     }
 
-    let one = stack.byte(1);
-    stack.equality(var_selector, true, one, true, true, false);
-
+    stack.move_var(var_selector);
+    stack.number(1);
+    stack.op_equal();
     let (mut chose_var_1, mut chose_var_2) = stack.open_if();
 
     for (var_1, var_2) in vars_1.into_iter().zip(vars_2.into_iter()) {
@@ -1935,14 +1935,14 @@ mod tests {
         assert!(stack.run().success);
     }
 
-    fn test_get_selected_vars_aux(var_selector: u8) {
+    fn test_get_selected_vars_aux(var_selector: u32) {
         let mut stack = StackTracker::new();
 
         let previous_var = stack.number_u32(0x3333_3333);
 
         let var_1 = stack.number_u32(0x1111_1111);
         let var_2 = stack.number_u32(0x2222_2222);
-        let selector = stack.byte(var_selector);
+        let selector = stack.number(var_selector);
 
         let next_var = stack.number_u32(0x4444_4444);
 
diff --git a/definitions/src/challenge.rs b/definitions/src/challenge.rs
index dca9477..af9d3c5 100644
--- a/definitions/src/challenge.rs
+++ b/definitions/src/challenge.rs
@@ -14,8 +14,8 @@ pub enum ChallengeType {
     ProgramCounter(String, TraceStep, String, TraceReadPC),
     Opcode(TraceReadPC, u32, Option<Chunk>), // (PROVER_PC, PROVER_OPCODE), CHUNK_INDEX, CHUNK_BASE_ADDRESS, OPCODES_CHUNK
     InputData(TraceRead, TraceRead, u32, u32),
-    InitializedData(TraceRead, TraceRead, u8, u32, Option<Chunk>),
-    UninitializedData(TraceRead, TraceRead, u8, Option<SectionDefinition>),
+    InitializedData(TraceRead, TraceRead, u32, u32, Option<Chunk>),
+    UninitializedData(TraceRead, TraceRead, u32, Option<SectionDefinition>),
     RomData(TraceRead, TraceRead, u32, u32),
     AddressesSections(
         TraceRead,
@@ -32,7 +32,7 @@ pub enum ChallengeType {
     ReadValue {
         read_1: TraceRead,
         read_2: TraceRead,
-        read_selector: u8,
+        read_selector: u32,
         step_hash: String,
         trace: TraceStep,
         next_hash: String,
diff --git a/emulator/src/decision/execution_log.rs b/emulator/src/decision/execution_log.rs
index 3b580b1..a709e53 100644
--- a/emulator/src/decision/execution_log.rs
+++ b/emulator/src/decision/execution_log.rs
@@ -81,7 +81,7 @@ pub struct VerifierChallengeLog {
     pub input: Vec<u8>,
     pub conflict_step_log: VerifierNAryLog,
     pub read_challenge_log: VerifierNAryLog,
-    pub read_selector: u8,
+    pub read_selector: u32,
     pub read_step: u64,
 }
 

From 330568396d195dd529e32c5bdb9cdacac1ba98c0 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 10 Sep 2025 11:44:50 -0300
Subject: [PATCH 28/34] use optimized static shift

---
 bitcoin-script-riscv/src/riscv/challenges.rs  |  4 +-
 .../src/riscv/script_utils.rs                 | 55 ++++++++++++++++++-
 2 files changed, 54 insertions(+), 5 deletions(-)

diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index 9fc25c6..c37bfa0 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -422,7 +422,7 @@ pub fn opcode_challenge(stack: &mut StackTracker, chunk: &Chunk) {
 
     let pc = stack.define(8, "prover_pc");
     let opcode = stack.define(8, "prover_opcode");
-    let tables = StackTables::new(stack, true, false, 0, 0, 0);
+    let tables = StackTables::new(stack, true, false, 2, 2, 0);
 
     address_in_range(stack, &chunk.range(), &pc);
     stack.op_verify();
@@ -457,7 +457,7 @@ pub fn initialized_challenge(stack: &mut StackTracker, chunk: &Chunk) {
     let init = stack.number_u64(LAST_STEP_INIT);
     stack.equality(read_step, true, init, true, true, true);
 
-    let tables = &StackTables::new(stack, true, false, 0, 0, 0);
+    let tables = &StackTables::new(stack, true, false, 2, 2, 0);
     verify_wrong_chunk_value(stack, tables, chunk, read_addr, read_value);
 
     tables.drop(stack);
diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs
index dc0564b..98684ad 100644
--- a/bitcoin-script-riscv/src/riscv/script_utils.rs
+++ b/bitcoin-script-riscv/src/riscv/script_utils.rs
@@ -67,6 +67,34 @@ pub fn nib_to_bin(stack: &mut StackTracker) {
     }
 }
 
+pub fn static_right_shift_2(
+    stack: &mut StackTracker,
+    tables: &StackTables,
+    number: StackVariable,
+) -> StackVariable {
+    let size = stack.get_size(number);
+    for n in 0..size {
+        stack.move_var_sub_n(number, 0);
+        if n < size - 1 {
+            stack.op_dup();
+            stack.get_value_from_table(tables.lshift.shift_2, None);
+            stack.to_altstack();
+        }
+
+        stack.get_value_from_table(tables.rshift.shift_2, None);
+
+        if n > 0 {
+            stack.op_add();
+        }
+
+        if n < size - 1 {
+            stack.from_altstack();
+        }
+    }
+
+    stack.join_in_stack(size, None, Some("right_shift_2"))
+}
+
 //expects the shift ammount and the number to be shifted on the stack
 pub fn shift_number(
     stack: &mut StackTracker,
@@ -1434,8 +1462,7 @@ pub fn verify_wrong_chunk_value(
     let base_addr = stack.number_u32(chunk.base_addr);
     let offset = sub(stack, &tables, address, base_addr);
 
-    let to_shift = stack.number(2);
-    let index = shift_number(stack, to_shift, offset, true, false);
+    let index = static_right_shift_2(stack, tables, offset);
 
     let index_nibbles = stack.explode(index);
     nibbles_to_number(stack, index_nibbles);
@@ -1495,10 +1522,12 @@ pub fn address_in_range(stack: &mut StackTracker, range: &(u32, u32), address: &
     let end = stack.number_u32(range.1);
     let address_copy = stack.copy_var(*address);
 
+    // start <= address
     is_equal_to(stack, &start, &address_copy);
     is_lower_than(stack, start, address_copy, true);
     stack.op_boolor();
 
+    // address <= end
     let address_copy = stack.copy_var(*address);
     is_equal_to(stack, &end, &address_copy);
     is_lower_than(stack, address_copy, end, true);
@@ -1712,6 +1741,26 @@ mod tests {
         test_shift_case(0xF100_0013, 13, false, false, 0x0002_6000);
     }
 
+    fn test_static_right_shift_2_case(value: u32, expected: u32) {
+        let mut stack = StackTracker::new();
+        let tables = &StackTables::new(&mut stack, false, false, 2, 2, 0);
+        let number = stack.number_u32(value);
+        let shifted = static_right_shift_2(&mut stack, tables, number);
+        println!("Size:  {} ", stack.get_script().len());
+        let expected = stack.number_u32(expected);
+        stack.equals(shifted, true, expected, true);
+        tables.drop(&mut stack);
+        stack.op_true();
+        assert!(stack.run().success);
+    }
+
+    #[test]
+    fn test_static_right_shift_2() {
+        test_static_right_shift_2_case(0b1101_1011, 0b0011_0110);
+        test_static_right_shift_2_case(0xF100_0013, 0x3C40_0004);
+        test_static_right_shift_2_case(3, 0);
+    }
+
     #[test]
     fn test_nib_to_bin() {
         for i in 0..16 {
@@ -1980,7 +2029,7 @@ mod tests {
 
         let address = stack.number_u32(address);
         let value = stack.number_u32(value);
-        let tables = &StackTables::new(&mut stack, true, false, 0, 0, 0);
+        let tables = &StackTables::new(&mut stack, true, false, 2, 2, 0);
 
         verify_wrong_chunk_value(&mut stack, tables, chunk, address, value);
         tables.drop(&mut stack);

From 2704aba8d6833fc9cfafe8e7c64068d371eb56a2 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 10 Sep 2025 11:48:33 -0300
Subject: [PATCH 29/34] refactor nary_log retrieval logic

---
 emulator/src/decision/challenge.rs     | 27 +++++---------------------
 emulator/src/decision/execution_log.rs | 16 ++++++++++++++-
 emulator/src/decision/nary_search.rs   | 26 -------------------------
 3 files changed, 20 insertions(+), 49 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 48611c3..ef1cb28 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -68,7 +68,7 @@ pub fn prover_get_hashes_for_round(
 ) -> Result<Vec<String>, EmulatorError> {
     let mut challenge_log = ProverChallengeLog::load(checkpoint_path)?;
     let input = challenge_log.input.clone();
-    let nary_log = nary_type.get_prover_nary_log(&mut challenge_log);
+    let nary_log = challenge_log.get_nary_log(nary_type);
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
 
     let new_base = match round {
@@ -166,7 +166,7 @@ pub fn verifier_choose_segment(
     let mut challenge_log = VerifierChallengeLog::load(checkpoint_path)?;
     let input = challenge_log.input.clone();
 
-    let nary_log = nary_type.get_verifier_nary_log(&mut challenge_log);
+    let nary_log = challenge_log.get_nary_log(nary_type);
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
 
     let hashes = program_def.get_round_hashes(
@@ -206,11 +206,10 @@ pub fn prover_final_trace(
     checkpoint_path: &str,
     final_bits: u32,
     fail_config: Option<FailConfiguration>,
-    nary_type: NArySearchType,
 ) -> Result<TraceRWStep, EmulatorError> {
     let mut challenge_log = ProverChallengeLog::load(checkpoint_path)?;
     let input = challenge_log.input.clone();
-    let nary_log = nary_type.get_prover_nary_log(&mut challenge_log);
+    let nary_log = challenge_log.get_nary_log(NArySearchType::ConflictStep);
 
     let program_def = ProgramDefinition::from_config(program_definition_file)?;
     let nary_def = program_def.nary_def();
@@ -800,14 +799,8 @@ mod tests {
 
         //PROVER PROVIDES EXECUTE STEP (and reveals full_trace)
         //Use v_desision + 1 as v_decision defines the last agreed step
-        let final_trace = prover_final_trace(
-            pdf,
-            chk_prover_path,
-            v_decision + 1,
-            fail_config_prover,
-            NArySearchType::ConflictStep,
-        )
-        .unwrap();
+        let final_trace =
+            prover_final_trace(pdf, chk_prover_path, v_decision + 1, fail_config_prover).unwrap();
         info!("Prover final trace: {:?}", final_trace.to_csv());
 
         let result = verify_script(&final_trace, REGISTERS_BASE_ADDRESS, &None);
@@ -858,16 +851,6 @@ mod tests {
                     info!("{:?}", v_decision);
                 }
 
-                let final_trace = prover_final_trace(
-                    pdf,
-                    chk_prover_path,
-                    v_decision + 1,
-                    fail_config_prover_read_challenge,
-                    NArySearchType::ReadValueChallenge,
-                )
-                .unwrap();
-                info!("Prover final trace: {:?}", final_trace.to_csv());
-
                 verifier_choose_challenge_for_read_challenge(
                     pdf,
                     chk_verifier_path,
diff --git a/emulator/src/decision/execution_log.rs b/emulator/src/decision/execution_log.rs
index a709e53..d93cd8a 100644
--- a/emulator/src/decision/execution_log.rs
+++ b/emulator/src/decision/execution_log.rs
@@ -1,7 +1,7 @@
 use bitvmx_cpu_definitions::trace::TraceRWStep;
 use serde::{Deserialize, Serialize};
 
-use crate::{EmulatorError, ExecutionResult};
+use crate::{decision::nary_search::NArySearchType, EmulatorError, ExecutionResult};
 
 #[derive(Debug, Serialize, Deserialize)]
 pub struct ExecutionLog {
@@ -53,6 +53,13 @@ impl ProverChallengeLog {
     pub fn load(path: &str) -> Result<Self, EmulatorError> {
         deserialize_challenge_log(path)
     }
+
+    pub fn get_nary_log(&mut self, nary_search: NArySearchType) -> &mut ProverNAryLog {
+        match nary_search {
+            NArySearchType::ConflictStep => &mut self.conflict_step_log,
+            NArySearchType::ReadValueChallenge => &mut self.read_challenge_log,
+        }
+    }
 }
 
 #[derive(Debug, Serialize, Deserialize, Default)]
@@ -110,6 +117,13 @@ impl VerifierChallengeLog {
     pub fn load(path: &str) -> Result<Self, EmulatorError> {
         deserialize_challenge_log(path)
     }
+
+    pub fn get_nary_log(&mut self, nary_search: NArySearchType) -> &mut VerifierNAryLog {
+        match nary_search {
+            NArySearchType::ConflictStep => &mut self.conflict_step_log,
+            NArySearchType::ReadValueChallenge => &mut self.read_challenge_log,
+        }
+    }
 }
 
 pub fn serialize_challenge_log<T: Serialize>(path: &str, data: &T) -> Result<(), EmulatorError> {
diff --git a/emulator/src/decision/nary_search.rs b/emulator/src/decision/nary_search.rs
index 44bac67..bd329b3 100644
--- a/emulator/src/decision/nary_search.rs
+++ b/emulator/src/decision/nary_search.rs
@@ -4,38 +4,12 @@ use clap::ValueEnum;
 use serde::Serialize;
 use tracing::{error, info};
 
-use crate::decision::execution_log::{
-    ProverChallengeLog, ProverNAryLog, VerifierChallengeLog, VerifierNAryLog,
-};
-
 #[derive(Clone, Copy, PartialEq, ValueEnum)]
 pub enum NArySearchType {
     ConflictStep,
     ReadValueChallenge,
 }
 
-impl NArySearchType {
-    pub fn get_prover_nary_log<'a>(
-        &'a self,
-        challenge_log: &'a mut ProverChallengeLog,
-    ) -> &'a mut ProverNAryLog {
-        match self {
-            Self::ConflictStep => &mut challenge_log.conflict_step_log,
-            Self::ReadValueChallenge => &mut challenge_log.read_challenge_log,
-        }
-    }
-
-    pub fn get_verifier_nary_log<'a>(
-        &'a self,
-        challenge_log: &'a mut VerifierChallengeLog,
-    ) -> &'a mut VerifierNAryLog {
-        match self {
-            Self::ConflictStep => &mut challenge_log.conflict_step_log,
-            Self::ReadValueChallenge => &mut challenge_log.read_challenge_log,
-        }
-    }
-}
-
 #[derive(Debug, Clone, Serialize)]
 pub struct NArySearchDefinition {
     pub max_steps: u64,

From 7718fdf47447673fc7886dfe227a0364842106d7 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 10 Sep 2025 11:50:47 -0300
Subject: [PATCH 30/34] remove unused fail-config

---
 emulator/src/executor/fetcher.rs |  8 --------
 emulator/src/executor/utils.rs   | 27 +--------------------------
 emulator/src/main.rs             | 15 +--------------
 3 files changed, 2 insertions(+), 48 deletions(-)

diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs
index 44dc5ed..ea4974e 100644
--- a/emulator/src/executor/fetcher.rs
+++ b/emulator/src/executor/fetcher.rs
@@ -148,14 +148,6 @@ pub fn execute_program(
             }
         }
 
-        if let Some(fail_trace_write) = &fail_config.fail_trace_write {
-            if fail_trace_write.step == program.step {
-                if let Ok(trace) = trace.as_mut() {
-                    trace.trace_step.write_1 = fail_trace_write.trace_write.clone()
-                }
-            }
-        }
-
         if let Some(step) = mem_dump {
             if program.step == step {
                 info!("\n========== Dumping memory at step: {} ==========", step);
diff --git a/emulator/src/executor/utils.rs b/emulator/src/executor/utils.rs
index 0776504..b4d5138 100644
--- a/emulator/src/executor/utils.rs
+++ b/emulator/src/executor/utils.rs
@@ -1,6 +1,6 @@
 use std::str::FromStr;
 
-use bitvmx_cpu_definitions::trace::{TraceRWStep, TraceRead, TraceWrite};
+use bitvmx_cpu_definitions::trace::{TraceRWStep, TraceRead};
 use num_traits;
 
 use crate::loader::program::Program;
@@ -216,24 +216,6 @@ impl FailOpcode {
     }
 }
 
-#[derive(Clone, Debug, Serialize, Deserialize)]
-pub struct FailTraceWrite {
-    pub step: u64,
-    pub trace_write: TraceWrite,
-}
-
-impl FailTraceWrite {
-    pub fn new(args: &Vec<String>) -> Self {
-        Self {
-            step: parse_value::<u64>(&args[0]),
-            trace_write: TraceWrite {
-                address: parse_value::<u32>(&args[1]),
-                value: parse_value::<u32>(&args[2]),
-            },
-        }
-    }
-}
-
 #[derive(Clone, Debug, Default, Serialize, Deserialize)]
 pub struct FailConfiguration {
     pub fail_hash: Option<u64>,
@@ -241,7 +223,6 @@ pub struct FailConfiguration {
     pub fail_execute: Option<FailExecute>,
     pub fail_reads: Option<FailReads>,
     pub fail_write: Option<FailWrite>,
-    pub fail_trace_write: Option<FailTraceWrite>,
     pub fail_pc: Option<u64>,
     pub fail_opcode: Option<FailOpcode>,
     pub fail_memory_protection: bool,
@@ -254,12 +235,6 @@ impl FailConfiguration {
             ..Default::default()
         }
     }
-    pub fn new_fail_trace_write(fail_trace_write: FailTraceWrite) -> Self {
-        Self {
-            fail_trace_write: Some(fail_trace_write),
-            ..Default::default()
-        }
-    }
     pub fn new_fail_hash_until(step: u64) -> Self {
         Self {
             fail_hash_until: Some(step),
diff --git a/emulator/src/main.rs b/emulator/src/main.rs
index 4c7e446..5643cab 100644
--- a/emulator/src/main.rs
+++ b/emulator/src/main.rs
@@ -14,7 +14,7 @@ use emulator::{
     },
     executor::{
         fetcher::execute_program,
-        utils::{FailConfiguration, FailExecute, FailOpcode, FailReads, FailTraceWrite, FailWrite},
+        utils::{FailConfiguration, FailExecute, FailOpcode, FailReads, FailWrite},
     },
     loader::program::{generate_rom_commitment, load_elf, Program},
     EmulatorError, ExecutionResult,
@@ -181,10 +181,6 @@ enum Commands {
         /// Command File to write the result
         #[arg(short, long, value_name = "COMMAND_PATH")]
         command_file: String,
-
-        /// Nary Search type
-        #[arg(short, long, value_name = "NARY_TYPE")]
-        nary_type: NArySearchType,
     },
 
     VerifierChooseChallenge {
@@ -338,10 +334,6 @@ enum Commands {
         #[arg(long, value_names = &["step", "address_original", "value", "modified_address"], num_args = 4)]
         fail_write: Option<Vec<String>>,
 
-        /// Fail trace write **after** calculating the step hash
-        #[arg(long, value_names = &["step", "address", "value"])]
-        fail_trace_write: Option<Vec<String>>,
-
         /// Fail while reading the pc at the given step
         #[arg(long)]
         fail_pc: Option<u64>,
@@ -407,7 +399,6 @@ fn main() -> Result<(), EmulatorError> {
             fail_read_1: fail_read_1_args,
             fail_read_2: fail_read_2_args,
             fail_write: fail_write_args,
-            fail_trace_write: fail_trace_write_args,
             fail_opcode: fail_opcode_args,
             dump_mem,
             fail_pc,
@@ -468,14 +459,12 @@ fn main() -> Result<(), EmulatorError> {
             };
 
             let fail_write = fail_write_args.as_ref().map(FailWrite::new);
-            let fail_trace_write = fail_trace_write_args.as_ref().map(FailTraceWrite::new);
             let fail_opcode = fail_opcode_args.as_ref().map(FailOpcode::new);
 
             let debugvar = *debug;
             let fail_config = FailConfiguration {
                 fail_hash: *fail_hash,
                 fail_hash_until: *fail_hash_until,
-                fail_trace_write,
                 fail_execute,
                 fail_reads,
                 fail_write,
@@ -632,14 +621,12 @@ fn main() -> Result<(), EmulatorError> {
             v_decision,
             fail_config_prover,
             command_file,
-            nary_type,
         }) => {
             let result: TraceRWStep = prover_final_trace(
                 pdf,
                 checkpoint_prover_path,
                 *v_decision,
                 fail_config_prover.clone(),
-                *nary_type,
             )?;
             info!("Prover final trace: {:?}", result);
 

From f6752fecf0877eacb67269e180cee1923d73f242 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Wed, 10 Sep 2025 11:51:18 -0300
Subject: [PATCH 31/34] decrease chunk size

---
 definitions/src/lib.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/definitions/src/lib.rs b/definitions/src/lib.rs
index a3a683b..56760c0 100644
--- a/definitions/src/lib.rs
+++ b/definitions/src/lib.rs
@@ -4,5 +4,5 @@ pub mod trace;
 
 pub mod constants {
     pub const LAST_STEP_INIT: u64 = 0xFFFF_FFFF_FFFF_FFFF;
-    pub const CHUNK_SIZE: u32 = 500;
+    pub const CHUNK_SIZE: u32 = 100;
 }

From 91034f1e2b2b21497f4e4bc74040ebbf9d3a58b1 Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Mon, 15 Sep 2025 12:16:27 -0300
Subject: [PATCH 32/34] tmp commit

---
 bitcoin-script-riscv/Cargo.toml              | 2 +-
 bitcoin-script-riscv/src/riscv/challenges.rs | 1 +
 emulator/src/decision/challenge.rs           | 3 +++
 3 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/bitcoin-script-riscv/Cargo.toml b/bitcoin-script-riscv/Cargo.toml
index a6e9a2c..4100636 100644
--- a/bitcoin-script-riscv/Cargo.toml
+++ b/bitcoin-script-riscv/Cargo.toml
@@ -10,7 +10,7 @@ bitcoin-script-stack = { git = "https://github.com/FairgateLabs/rust-bitcoin-scr
     "interactive",
 ], branch = "v2" }
 bitcoin-script-functions = { git = "https://github.com/FairgateLabs/rust-bitcoin-script-functions" }
-bitcoin = "=0.32.5"
+bitcoin = "=0.32.6"
 bitcoin-script = { git = "https://github.com/FairgateLabs/rust-bitcoin-script", branch = "bitvmx" }
 riscv-decode = "0.2.1"
 thiserror = "1.0.61"
diff --git a/bitcoin-script-riscv/src/riscv/challenges.rs b/bitcoin-script-riscv/src/riscv/challenges.rs
index c37bfa0..8bef550 100644
--- a/bitcoin-script-riscv/src/riscv/challenges.rs
+++ b/bitcoin-script-riscv/src/riscv/challenges.rs
@@ -486,6 +486,7 @@ pub fn uninitialized_challenge(
         read_selector,
     );
 
+    // TODO: ASSERT NOT TOO MANY SECTIONS
     address_in_sections(stack, &read_addr, uninitialized_sections);
     stack.op_verify();
 
diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index ef1cb28..10ee6e0 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -436,6 +436,8 @@ pub fn verifier_choose_challenge(
         ));
     }
 
+    // TODO: check read_step < current_step
+
     // check const read value
     let is_read_1_conflict = trace.read_1.value != my_trace.read_1.value;
     let is_read_2_conflict = trace.read_2.value != my_trace.read_2.value;
@@ -1784,6 +1786,7 @@ mod tests {
         );
     }
 
+    // TODO: add case for write to the same address and different value
     #[test]
     fn test_challenge_modified_value_doesnt_lie() {
         init_trace();

From 1aee5d259c2174e8083316814076fe6f9c23225c Mon Sep 17 00:00:00 2001
From: crivasr <camilorivasramunni@gmail.com>
Date: Mon, 15 Sep 2025 15:50:23 -0300
Subject: [PATCH 33/34] update docker submodule

---
 docker-riscv32 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docker-riscv32 b/docker-riscv32
index abe6769..34a6997 160000
--- a/docker-riscv32
+++ b/docker-riscv32
@@ -1 +1 @@
-Subproject commit abe67699a6d6a09cce15d1476ce2aec676de30a6
+Subproject commit 34a699736f50516d754441239cd8be2b26bc3a41

From 79ae57c6b93b8c76b3266c920a79a5d7d8d4a6a3 Mon Sep 17 00:00:00 2001
From: Kevin Wahle <62912263+KevinWahle@users.noreply.github.com>
Date: Mon, 15 Sep 2025 16:22:27 -0300
Subject: [PATCH 34/34] update uninitialized ranges handling and add string
 convertion to NArySearchType

---
 emulator/src/decision/challenge.rs   |  8 +++-----
 emulator/src/decision/nary_search.rs | 26 +++++++++++++++++++++++---
 emulator/src/loader/program.rs       |  8 +++++---
 3 files changed, 31 insertions(+), 11 deletions(-)

diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs
index 10ee6e0..547c2f1 100644
--- a/emulator/src/decision/challenge.rs
+++ b/emulator/src/decision/challenge.rs
@@ -1,7 +1,7 @@
 use bitvmx_cpu_definitions::{
     challenge::ChallengeType,
     constants::{CHUNK_SIZE, LAST_STEP_INIT},
-    memory::{Chunk, SectionDefinition},
+    memory::Chunk,
     trace::{generate_initial_step_hash, hashvec_to_string, validate_step_hash, TraceRWStep},
 };
 
@@ -505,15 +505,13 @@ pub fn verifier_choose_challenge(
                 || force == ForceChallenge::UninitializedData
             {
                 info!("Verifier choose to challenge invalid UNINITIALIZED DATA");
-                let uninitilized_ranges = program.get_uninitialized_ranges(program_def);
+                let uninitilized_ranges = program.get_uninitialized_ranges(&program_def);
 
                 return Ok(ChallengeType::UninitializedData(
                     trace.read_1,
                     trace.read_2,
                     read_selector,
-                    return_script_parameters.then_some(SectionDefinition {
-                        ranges: uninitilized_ranges,
-                    }),
+                    return_script_parameters.then_some(uninitilized_ranges),
                 ));
             }
         } else {
diff --git a/emulator/src/decision/nary_search.rs b/emulator/src/decision/nary_search.rs
index bd329b3..86a5d8a 100644
--- a/emulator/src/decision/nary_search.rs
+++ b/emulator/src/decision/nary_search.rs
@@ -1,14 +1,34 @@
-use std::collections::HashMap;
+use std::{collections::HashMap, str::FromStr};
 
 use clap::ValueEnum;
-use serde::Serialize;
+use serde::{Deserialize, Serialize};
 use tracing::{error, info};
 
-#[derive(Clone, Copy, PartialEq, ValueEnum)]
+#[derive(Clone, Copy, PartialEq, ValueEnum, Serialize, Deserialize, Debug)]
 pub enum NArySearchType {
     ConflictStep,
     ReadValueChallenge,
 }
+impl ToString for NArySearchType {
+    fn to_string(&self) -> String {
+        match self {
+            NArySearchType::ConflictStep => "conflict-step".to_string(),
+            NArySearchType::ReadValueChallenge => "read-value-challenge".to_string(),
+        }
+    }
+}
+
+impl FromStr for NArySearchType {
+    type Err = String;
+
+    fn from_str(s: &str) -> Result<Self, Self::Err> {
+        match s {
+            "conflict-step" => Ok(NArySearchType::ConflictStep),
+            "read-value-challenge" => Ok(NArySearchType::ReadValueChallenge),
+            _ => Err(format!("'{}' is not a valid NArySearchType", s)),
+        }
+    }
+}
 
 #[derive(Debug, Clone, Serialize)]
 pub struct NArySearchDefinition {
diff --git a/emulator/src/loader/program.rs b/emulator/src/loader/program.rs
index 4dc4658..e390a7d 100644
--- a/emulator/src/loader/program.rs
+++ b/emulator/src/loader/program.rs
@@ -562,8 +562,8 @@ impl Program {
 
     pub fn get_uninitialized_ranges(
         &self,
-        program_definition: ProgramDefinition,
-    ) -> Vec<(u32, u32)> {
+        program_definition: &ProgramDefinition,
+    ) -> SectionDefinition {
         let mut uninitialized: Vec<(u32, u32)> = self
             .sections
             .iter()
@@ -599,7 +599,9 @@ impl Program {
             uninitialized.push((uninit_start, end));
         }
 
-        uninitialized
+        SectionDefinition {
+            ranges: uninitialized,
+        }
     }
 }