Merge pull request #2893 from o1-labs/dw/test-add-overflow

o1vm/riscv32im: add tests for add with overflows

o1vm/resources/programs/riscv32im/src/add_overflow.S

@@ -0,0 +1,31 @@
+# The addition performed by `add` is simply a bit-wise addition
+# The lowest 32 bits are kept, and no overflow bit is kept.
+.section .text
+.globl _start
+
+_start:
+    # Large positive values
+    # It is equal to
+    # 0b01111111111111111111111111111111 +
+    # 0b00000000000000000000000000000001 =
+    # 0b10000000000000000000000000000000 =
+    li t0, 2147483647    # t0 = 2147483647 (Max 32-bit signed int)
+    li t1, 1             # t1 = 1
+    add t2, t0, t1       # t2 = t0 + t1
+
+    # 0b11111111111111111111111111111111 +
+    # 0b00000000000000000000000000000001 =
+    # 0b00000000000000000000000000000000 =
+    li t3, 0b11111111111111111111111111111111
+    add t4, t3, t1       # t4 = t3 + t1 (Expected: overflow, wrap around)
+
+    # Custom exit syscall
+    li a0, 0
+    li a1, 0
+    li a2, 0
+    li a3, 0
+    li a4, 0
+    li a5, 0
+    li a6, 0
+    li a7, 42
+    ecall

o1vm/tests/test_riscv_elf.rs

@@ -158,3 +158,23 @@ fn test_add_2() {
     assert_eq!(witness.registers[T5], 912); // t5 = t0 + t2
     assert_eq!(witness.registers[T6], 1368); // t6 = t4 + x0 (Copy t4 to t6)
 }
+
+#[test]
+fn test_add_overflow() {
+    let curr_dir = std::env::current_dir().unwrap();
+    let path = curr_dir.join(std::path::PathBuf::from(
+        "resources/programs/riscv32im/bin/add_overflow",
+    ));
+    let state = o1vm::elf_loader::parse_riscv32(&path).unwrap();
+    let mut witness = Env::<Fp>::create(PAGE_SIZE.try_into().unwrap(), state);
+
+    while !witness.halt {
+        witness.step();
+    }
+
+    assert_eq!(witness.registers[T0], 0b01111111111111111111111111111111);
+    assert_eq!(witness.registers[T1], 0b00000000000000000000000000000001);
+    assert_eq!(witness.registers[T2], 0b10000000000000000000000000000000);
+    assert_eq!(witness.registers[T3], 0b11111111111111111111111111111111);
+    assert_eq!(witness.registers[T4], 0b00000000000000000000000000000000);
+}