From 39029c74b53aaa38dee6bf7baba75dc9068b8fdc Mon Sep 17 00:00:00 2001 From: crivasr Date: Wed, 6 Aug 2025 15:50:24 -0300 Subject: [PATCH 01/10] Fix division instructions to comply with RISC-V spec --- emulator/src/executor/fetcher.rs | 50 ++++++++++++++++---------------- 1 file changed, 25 insertions(+), 25 deletions(-) diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs index ea4974e..0bc6a23 100644 --- a/emulator/src/executor/fetcher.rs +++ b/emulator/src/executor/fetcher.rs @@ -523,30 +523,30 @@ pub fn op_arithmetic( let value_2 = program.registers.get(x.rs2()); let witness = match instruction { - Rem(_) => match value_2 { - 0 => Some(0xFFFF_FFFF), - 0xFFFF_FFFF => Some(value_1), - _ => Some((value_1 as i32 / value_2 as i32) as u32), - }, - Div(_) => match value_2 { - 0 => Some(value_1), - 0xFFFF_FFFF => Some(0), - _ => Some((value_1 as i32 % value_2 as i32) as u32), - }, - Remu(_) => { + Rem(_) => Some(match (value_1 as i32, value_2 as i32) { + (_, 0) => (-1 as i32) as u32, + (std::i32::MIN, -1) => std::i32::MIN as u32, + _ => (value_1 as i32 / value_2 as i32) as u32, + }), + Div(_) => Some(match (value_1 as i32, value_2 as i32) { + (_, 0) => value_1, + (std::i32::MIN, -1) => 0, + _ => (value_1 as i32 % value_2 as i32) as u32, + }), + Remu(_) => Some({ if value_2 == 0 { - Some(0xFFFFFFFF) + std::i32::MAX as u32 } else { - Some(value_1 / value_2) + value_1 / value_2 } - } - Divu(_) => { + }), + Divu(_) => Some({ if value_2 == 0 { - Some(value_1) + value_1 } else { - Some(value_1 % value_2) + value_1 % value_2 } - } + }), _ => None, }; @@ -567,21 +567,21 @@ pub fn op_arithmetic( let result: u64 = (value_1 as u64) * (value_2 as u64); (result >> 32) as u32 // High 32 bits } - Div(_) => match value_2 { - 0 => 0xFFFF_FFFF, - 0xFFFF_FFFF => value_1, + Div(_) => match (value_1 as i32, value_2 as i32) { + (_, 0) => (-1 as i32) as u32, + (std::i32::MIN, -1) => std::i32::MIN as u32, _ => (value_1 as i32 / value_2 as i32) as u32, }, Divu(_) => { if value_2 == 0 { - 0xFFFFFFFF + std::u32::MAX as u32 } else { value_1 / value_2 } } - Rem(_) => match value_2 { - 0 => value_1, - 0xFFFF_FFFF => 0, + Rem(_) => match (value_1 as i32, value_2 as i32) { + (_, 0) => value_1, + (std::i32::MIN, -1) => 0, _ => (value_1 as i32 % value_2 as i32) as u32, }, Remu(_) => { From e95eb278483885e9935c8d34d8df6595cbcc5315 Mon Sep 17 00:00:00 2001 From: crivasr Date: Wed, 6 Aug 2025 15:54:46 -0300 Subject: [PATCH 02/10] Small fix --- emulator/src/executor/fetcher.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/emulator/src/executor/fetcher.rs b/emulator/src/executor/fetcher.rs index 0bc6a23..706ef3f 100644 --- a/emulator/src/executor/fetcher.rs +++ b/emulator/src/executor/fetcher.rs @@ -535,7 +535,7 @@ pub fn op_arithmetic( }), Remu(_) => Some({ if value_2 == 0 { - std::i32::MAX as u32 + std::u32::MAX } else { value_1 / value_2 } @@ -574,7 +574,7 @@ pub fn op_arithmetic( }, Divu(_) => { if value_2 == 0 { - std::u32::MAX as u32 + std::u32::MAX } else { value_1 / value_2 } From ce4cbc1c5a96c1afd9d33262c13b8e5222c1533d Mon Sep 17 00:00:00 2001 From: crivasr Date: Thu, 14 Aug 2025 15:02:56 -0300 Subject: [PATCH 03/10] Fix bitcoin script division --- .../src/riscv/script_utils.rs | 86 +++++++++++++------ 1 file changed, 58 insertions(+), 28 deletions(-) diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs index 98684ad..762d931 100644 --- a/bitcoin-script-riscv/src/riscv/script_utils.rs +++ b/bitcoin-script-riscv/src/riscv/script_utils.rs @@ -1176,7 +1176,7 @@ pub fn sign_check( stack_false.op_equalverify(); stack.end_if(stack_true, stack_false, 2, vec![], 0); - //then assert sign of divisor and dividen are the same the quotient sign is positive and negative otherwise + //then assert that if the sign of divisor and dividen are the same then the quotient sign is positive and negative otherwise is_negative(stack, divisor); // divisor_sign | dividend_sign dividend_sign rem_sign stack.op_dup(); // divisor_sign divisor_sign | dividend_sign dividend_sign rem_sign stack.from_altstack(); // divisor_sign divisor_sign dividend_sign | dividend_sign rem_sign @@ -1210,19 +1210,48 @@ pub fn sign_check( (divisor, quotient, dividend, remainder) } -pub fn edge_case( +pub fn div_by_zero_case( stack: &mut StackTracker, dividend: StackVariable, divisor: StackVariable, quotient: StackVariable, remainder: StackVariable, - compare: u32, result: Option, ) -> (StackTracker, StackTracker) { - let value = stack.number_u32(compare); - is_equal_to(stack, &value, &divisor); + let zero = stack.number_u32(0); + is_equal_to(stack, &zero, &divisor); + stack.to_altstack(); + stack.drop(zero); + stack.from_altstack(); + let (mut stack_true, stack_false) = stack.open_if(); + + stack_true.drop(remainder); + stack_true.drop(quotient); + stack_true.drop(divisor); + if result.is_some() { + stack_true.drop(dividend); + stack_true.number_u32(result.unwrap()); + } + + (stack_true, stack_false) +} + +pub fn overflow_case( + stack: &mut StackTracker, + dividend: StackVariable, + divisor: StackVariable, + quotient: StackVariable, + remainder: StackVariable, + result: Option, +) -> (StackTracker, StackTracker) { + let minus_one = stack.number_u32(-1 as i32 as u32); + let min_i32 = stack.number_u32(std::i32::MIN as u32); + is_equal_to(stack, &minus_one, &divisor); + is_equal_to(stack, &min_i32, ÷nd); + stack.op_booland(); stack.to_altstack(); - stack.drop(value); + stack.drop(min_i32); + stack.drop(minus_one); stack.from_altstack(); let (mut stack_true, stack_false) = stack.open_if(); @@ -1244,8 +1273,7 @@ pub fn division_and_remainder( divisor: StackVariable, quotient: StackVariable, remainder: StackVariable, - compare: u32, - result: Option, + div_by_zero_result: Option, is_rem_check: bool, ) -> StackVariable { stack.move_var(dividend); @@ -1253,8 +1281,13 @@ pub fn division_and_remainder( stack.move_var(quotient); stack.move_var(remainder); - let (stack_true, mut stack_false) = edge_case( - stack, dividend, divisor, quotient, remainder, compare, result, + let (stack_true, mut stack_false) = div_by_zero_case( + stack, + dividend, + divisor, + quotient, + remainder, + div_by_zero_result, ); if is_rem_check { @@ -1298,8 +1331,7 @@ pub fn divu( divisor, quotient, remainder, - 0, - Some(0xFFFF_FFFF), + Some(std::u32::MAX), false, ) } @@ -1313,7 +1345,7 @@ pub fn remu( quotient: StackVariable, ) -> StackVariable { division_and_remainder( - stack, tables, dividend, divisor, quotient, remainder, 0, None, true, + stack, tables, dividend, divisor, quotient, remainder, None, true, ) } @@ -1324,10 +1356,8 @@ pub fn division_and_remainder_signed( divisor: StackVariable, quotient: StackVariable, remainder: StackVariable, - compare_1: u32, - result_1: Option, - compare_2: u32, - result_2: Option, + div_by_zero_result: Option, + overflow_result: Option, is_rem_check: bool, ) -> StackVariable { stack.move_var(dividend); @@ -1335,18 +1365,22 @@ pub fn division_and_remainder_signed( stack.move_var(quotient); stack.move_var(remainder); - let (stack_true, mut stack_false) = edge_case( - stack, dividend, divisor, quotient, remainder, compare_1, result_1, + let (stack_true, mut stack_false) = div_by_zero_case( + stack, + dividend, + divisor, + quotient, + remainder, + div_by_zero_result, ); - let (stack_true_2, mut stack_no_edge) = edge_case( + let (stack_true_2, mut stack_no_edge) = overflow_case( &mut stack_false, dividend, divisor, quotient, remainder, - compare_2, - result_2, + overflow_result, ); if is_rem_check { @@ -1405,10 +1439,8 @@ pub fn div( divisor, quotient, remainder, - 0, - Some(0xFFFF_FFFF), - 0xFFFF_FFFF, - None, + Some(-1 as i32 as u32), + Some(std::i32::MIN as u32), false, ) } @@ -1428,9 +1460,7 @@ pub fn rem( divisor, quotient, remainder, - 0, None, - 0xFFFF_FFFF, Some(0), true, ) From 267825f4ad4f77b07f14f4c7aa1a60957d6eaf3a Mon Sep 17 00:00:00 2001 From: crivasr Date: Thu, 14 Aug 2025 15:57:12 -0300 Subject: [PATCH 04/10] add division tests --- .../src/riscv/script_utils.rs | 61 +++++++++++++++++++ emulator/tests/test_r_type_instructions.rs | 40 ++++++++++++ 2 files changed, 101 insertions(+) diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs index 762d931..5e85ba1 100644 --- a/bitcoin-script-riscv/src/riscv/script_utils.rs +++ b/bitcoin-script-riscv/src/riscv/script_utils.rs @@ -1693,6 +1693,67 @@ mod tests { test_multiply_aux(0xFFFF_FFFF, 0x1, 0x0, 0xFFFF_FFFF); } + fn test_division_aux( + dividend: i32, + divisor: i32, + quotient: i32, + remainder: i32, + signed: bool, + ) { + let mut stack = StackTracker::new(); + let tables = StackTables::new(&mut stack, true, true, 0, 0, 0); + + let dividend = stack.number_u32(dividend as u32); + let dividend_copy = stack.copy_var(dividend); + + let divisor = stack.number_u32(divisor as u32); + let divisor_copy = stack.copy_var(divisor); + + let quotient = stack.number_u32(quotient as u32); + let quotient_copy = stack.copy_var(quotient); + + let remainder = stack.number_u32(remainder as u32); + let remainder_copy = stack.copy_var(remainder); + + let expected_div = stack.copy_var(quotient); + let expected_rem = stack.copy_var(remainder); + + let result_div; + let result_rem; + + if signed { + result_div = div(&mut stack, &tables, dividend, divisor, quotient, remainder); + result_rem = rem(&mut stack, &tables, dividend_copy, divisor_copy, remainder_copy, quotient_copy); + } else { + result_div = divu(&mut stack, &tables, dividend, divisor, quotient, remainder); + result_rem = remu(&mut stack, &tables, dividend_copy, divisor_copy, remainder_copy, quotient_copy); + } + + stack.equals(expected_div, true, result_div, true); + stack.equals(expected_rem, true, result_rem, true); + + tables.drop(&mut stack); + + stack.op_true(); + assert!(stack.run().success); + } + + #[test] + pub fn test_division() { + // signed division by 0 + test_division_aux(100, 0, -1, 100, true); + // unsigned division by 0 + test_division_aux(100, 0, std::u32::MAX as i32, 100, false); + // overflow + test_division_aux(std::i32::MIN, -1, std::i32::MIN, 0, true); + + test_division_aux(100, -6, -16, 4, true); + test_division_aux(-100, 6, -16, -4, true); + test_division_aux(-100, -6, 16, -4, true); + + test_division_aux(100, 6, 16, 4, false); + } + fn test_left_rotate_helper(value: u32, rotate: u32, expected: u32) { let mut stack = StackTracker::new(); let value = stack.number_u32(value); diff --git a/emulator/tests/test_r_type_instructions.rs b/emulator/tests/test_r_type_instructions.rs index 56e5cae..7f06464 100644 --- a/emulator/tests/test_r_type_instructions.rs +++ b/emulator/tests/test_r_type_instructions.rs @@ -198,3 +198,43 @@ fn test_sra() { assert_eq!(program.registers.get(1), 0x1); } + +fn test_division_aux(dividend: i32, divisor: i32, quotioent: i32, remainder: i32, signed: bool) { + let mut program = get_new_program(); + + program.registers.set(3, divisor as u32, 0); + program.registers.set(2, dividend as u32, 0); + + let x = create_rtype_from(3, 2, 1); + + let (div, rem) = if signed { + (Instruction::Div(x), Instruction::Rem(x)) + } else { + (Instruction::Divu(x), Instruction::Remu(x)) + }; + + let (_, witness) = op_arithmetic(&div, &x, &mut program); + assert_eq!(program.registers.get(1), quotioent as u32); + assert_eq!(witness.unwrap(), remainder as u32); + + + let (_, witness) = op_arithmetic(&rem, &x, &mut program); + assert_eq!(program.registers.get(1), remainder as u32); + assert_eq!(witness.unwrap(), quotioent as u32); +} + +#[test] +pub fn test_division() { + // signed division by 0 + test_division_aux(100, 0, -1, 100, true); + // unsigned division by 0 + test_division_aux(100, 0, std::u32::MAX as i32, 100, false); + // overflow + test_division_aux(std::i32::MIN, -1, std::i32::MIN, 0, true); + + test_division_aux(100, -6, -16, 4, true); + test_division_aux(-100, 6, -16, -4, true); + test_division_aux(-100, -6, 16, -4, true); + + test_division_aux(100, 6, 16, 4, false); +} From 8d8746185d114c5c54806bb8da64290eefceee29 Mon Sep 17 00:00:00 2001 From: crivasr Date: Thu, 14 Aug 2025 16:04:02 -0300 Subject: [PATCH 05/10] add div by -1 test case --- bitcoin-script-riscv/src/riscv/script_utils.rs | 1 + emulator/tests/test_r_type_instructions.rs | 1 + 2 files changed, 2 insertions(+) diff --git a/bitcoin-script-riscv/src/riscv/script_utils.rs b/bitcoin-script-riscv/src/riscv/script_utils.rs index 5e85ba1..f12f889 100644 --- a/bitcoin-script-riscv/src/riscv/script_utils.rs +++ b/bitcoin-script-riscv/src/riscv/script_utils.rs @@ -1752,6 +1752,7 @@ mod tests { test_division_aux(-100, -6, 16, -4, true); test_division_aux(100, 6, 16, 4, false); + test_division_aux(100, -1, -100, 0, true); } fn test_left_rotate_helper(value: u32, rotate: u32, expected: u32) { diff --git a/emulator/tests/test_r_type_instructions.rs b/emulator/tests/test_r_type_instructions.rs index 7f06464..490926d 100644 --- a/emulator/tests/test_r_type_instructions.rs +++ b/emulator/tests/test_r_type_instructions.rs @@ -237,4 +237,5 @@ pub fn test_division() { test_division_aux(-100, -6, 16, -4, true); test_division_aux(100, 6, 16, 4, false); + test_division_aux(100, -1, -100, 0, true); } From f47e5a8e432c3d684cea5e2cad8fb4281afc8bac Mon Sep 17 00:00:00 2001 From: crivasr Date: Thu, 14 Aug 2025 17:09:28 -0300 Subject: [PATCH 06/10] add audit test --- emulator/src/decision/challenge.rs | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs index 547c2f1..dae65ce 100644 --- a/emulator/src/decision/challenge.rs +++ b/emulator/src/decision/challenge.rs @@ -1850,4 +1850,29 @@ mod tests { ForceChallenge::No, ); } + + #[test] + fn test_challenge_wrong_division() { + init_trace(); + + let fail_args = vec!["13", "0xF000003C", "0x64", "0xF000003C"] + .iter() + .map(|x| x.to_string()) + .collect::>(); + let fail_write = Some(FailConfiguration::new_fail_write(FailWrite::new( + &fail_args, + ))); + + test_challenge_aux( + "audit_02", + "audit_02.yaml", + 0, + true, // final trace verification fails due to wrong div result + fail_write, + None, + true, + ForceCondition::No, + ForceChallenge::No, + ); + } } From 645762a8cdb7c0b61054b24b8b3173070617a046 Mon Sep 17 00:00:00 2001 From: crivasr Date: Wed, 20 Aug 2025 13:20:25 -0300 Subject: [PATCH 07/10] verify audit tests like compliance --- emulator/src/decision/challenge.rs | 25 -------------------- emulator/tests/audit.rs | 35 ++++++++++++++++++++++++++++ emulator/tests/compliance.rs | 37 +++--------------------------- emulator/tests/utils/common.rs | 29 ++++++++++++++++++++++- 4 files changed, 66 insertions(+), 60 deletions(-) create mode 100644 emulator/tests/audit.rs diff --git a/emulator/src/decision/challenge.rs b/emulator/src/decision/challenge.rs index dae65ce..547c2f1 100644 --- a/emulator/src/decision/challenge.rs +++ b/emulator/src/decision/challenge.rs @@ -1850,29 +1850,4 @@ mod tests { ForceChallenge::No, ); } - - #[test] - fn test_challenge_wrong_division() { - init_trace(); - - let fail_args = vec!["13", "0xF000003C", "0x64", "0xF000003C"] - .iter() - .map(|x| x.to_string()) - .collect::>(); - let fail_write = Some(FailConfiguration::new_fail_write(FailWrite::new( - &fail_args, - ))); - - test_challenge_aux( - "audit_02", - "audit_02.yaml", - 0, - true, // final trace verification fails due to wrong div result - fail_write, - None, - true, - ForceCondition::No, - ForceChallenge::No, - ); - } } diff --git a/emulator/tests/audit.rs b/emulator/tests/audit.rs new file mode 100644 index 0000000..c0a973f --- /dev/null +++ b/emulator/tests/audit.rs @@ -0,0 +1,35 @@ +use emulator::ExecutionResult; +use tracing::info; + +mod utils; +use utils::common::verify_file; + +#[test] +fn audit_tests() { + let path = "../docker-riscv32/riscv32/build/audit"; + let paths = std::fs::read_dir(path).unwrap(); + let mut count = 0; + for path in paths { + if let Ok(path) = path { + let fname = path.file_name(); + let fname = fname.to_string_lossy(); + if fname.ends_with(".elf") && !fname.contains("audit_01") { + let path = path.path(); + let path = path.to_string_lossy(); + + let (result, _) = verify_file(&format!("{}", path), true).unwrap(); + match result { + ExecutionResult::Halt(exit_code, _) => { + assert!(exit_code == 0, "Error executing file {}", path); + info!("File {} executed successfully", path); + count += 1; + } + _ => assert!(false, "Error executing file {}", path), + } + } + } + } + + info!("Total files executed: {}", count); + assert_eq!(count, 1); +} diff --git a/emulator/tests/compliance.rs b/emulator/tests/compliance.rs index eadacff..f373104 100644 --- a/emulator/tests/compliance.rs +++ b/emulator/tests/compliance.rs @@ -1,39 +1,8 @@ -use emulator::{ - executor::{ - fetcher::{execute_program, FullTrace}, - utils::FailConfiguration, - }, - loader::program::load_elf, - EmulatorError, ExecutionResult, -}; +use emulator::ExecutionResult; use tracing::info; -fn verify_file( - fname: &str, - verify_on_chain: bool, -) -> Result<(ExecutionResult, FullTrace), EmulatorError> { - let mut program = load_elf(&fname, false)?; - - info!("Execute program {}", fname); - Ok(execute_program( - &mut program, - Vec::new(), - ".bss", - false, - &None, - None, - false, - verify_on_chain, - false, - false, - false, - true, - None, - None, - FailConfiguration::default(), - false, - )) -} +mod utils; +use utils::common::verify_file; #[test] fn list_files() { diff --git a/emulator/tests/utils/common.rs b/emulator/tests/utils/common.rs index 727371b..ef82992 100644 --- a/emulator/tests/utils/common.rs +++ b/emulator/tests/utils/common.rs @@ -1,8 +1,9 @@ #![allow(dead_code)] use bitvmx_cpu_definitions::{memory::SectionDefinition, trace::ProgramCounter}; -use emulator::loader::program::{Program, Registers, Section}; +use emulator::{executor::{fetcher::{execute_program, FullTrace}, utils::FailConfiguration}, loader::program::{load_elf, Program, Registers, Section}, EmulatorError, ExecutionResult}; use rand::Rng; use riscv_decode::types::{BType, IType, JType, RType, SType, ShiftType, UType}; +use tracing::info; use std::ops::RangeInclusive; const PROGRAM_REG_RANGE: RangeInclusive = 0x1..=0x1F; @@ -79,3 +80,29 @@ pub fn rnd_range() -> u32 { let mut rng = rand::thread_rng(); rng.gen_range(PROGRAM_REG_RANGE) } + +pub fn verify_file( + fname: &str, + verify_on_chain: bool, +) -> Result<(ExecutionResult, FullTrace), EmulatorError> { + let mut program = load_elf(&fname, false)?; + + info!("Execute program {}", fname); + Ok(execute_program( + &mut program, + Vec::new(), + ".bss", + false, + &None, + None, + false, + verify_on_chain, + false, + false, + false, + true, + None, + None, + FailConfiguration::default(), + )) +} \ No newline at end of file From 8520ca866f84b37dac95ca1d7d65b9f4113e4f57 Mon Sep 17 00:00:00 2001 From: crivasr Date: Mon, 15 Sep 2025 14:08:20 -0300 Subject: [PATCH 08/10] rename test --- emulator/tests/audit.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/emulator/tests/audit.rs b/emulator/tests/audit.rs index c0a973f..1174998 100644 --- a/emulator/tests/audit.rs +++ b/emulator/tests/audit.rs @@ -13,7 +13,7 @@ fn audit_tests() { if let Ok(path) = path { let fname = path.file_name(); let fname = fname.to_string_lossy(); - if fname.ends_with(".elf") && !fname.contains("audit_01") { + if fname.ends_with("verify.elf") { let path = path.path(); let path = path.to_string_lossy(); From 19b8eec5e7cb402e435e9a4161521ec64fa3e3a5 Mon Sep 17 00:00:00 2001 From: crivasr Date: Mon, 15 Sep 2025 17:26:12 -0300 Subject: [PATCH 09/10] temporarily filter tests --- emulator/tests/audit.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/emulator/tests/audit.rs b/emulator/tests/audit.rs index 1174998..ceff2f6 100644 --- a/emulator/tests/audit.rs +++ b/emulator/tests/audit.rs @@ -13,7 +13,7 @@ fn audit_tests() { if let Ok(path) = path { let fname = path.file_name(); let fname = fname.to_string_lossy(); - if fname.ends_with("verify.elf") { + if fname.ends_with("verify.elf") && fname.contains("09") { let path = path.path(); let path = path.to_string_lossy(); From bf0c2cc6ab17b873586c4625551fd0c4f4f42b99 Mon Sep 17 00:00:00 2001 From: crivasr Date: Tue, 16 Sep 2025 12:36:00 -0300 Subject: [PATCH 10/10] add checkpoint argument to execute_program call --- emulator/tests/utils/common.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/emulator/tests/utils/common.rs b/emulator/tests/utils/common.rs index ef82992..6024a3a 100644 --- a/emulator/tests/utils/common.rs +++ b/emulator/tests/utils/common.rs @@ -104,5 +104,6 @@ pub fn verify_file( None, None, FailConfiguration::default(), + false, )) } \ No newline at end of file