Skip to content

Commit

Permalink
o1vm/riscv32im: programs performing arithmetic on 2^31 - 1
Browse files Browse the repository at this point in the history
  • Loading branch information
dannywillems committed Dec 31, 2024
1 parent aa41e09 commit bf9f0c6
Show file tree
Hide file tree
Showing 4 changed files with 75 additions and 1 deletion.
Binary file added o1vm/resources/programs/riscv32im/bin/mersenne_31
Binary file not shown.
50 changes: 50 additions & 0 deletions o1vm/resources/programs/riscv32im/src/mersenne_31.S
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
.section .text
.global _start

exit_success:
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

# Reduce a0 into the field. It does suppose that a0
# is a 32-bit number.
# We only deal with positive values.
# The input is located in a0, and the output
# is located also in a0.
# FIXME: calling convention should be respected here...
# That's ugly.
# Use temprary registers like t0-t6, and copy into the stack.
reduce_in_field:
li t0, 0x7fffffff
remu a0, a0, t0
ret

mersenne_add:
add sp, sp, -4
sw ra, 0(sp)

add a0, a0, a1
jal ra, reduce_in_field

lw ra, 0(sp)
add sp, sp, 4
ret

_start:
# Loading arguments
li a0, 0
li a1, 0x04

jal ra, mersenne_add

# Result is located in a0.
# Saving on the stack
sw a0, 0(sp)

jal ra, exit_success
7 changes: 6 additions & 1 deletion o1vm/src/interpreters/riscv32im/witness.rs
Original file line number Diff line number Diff line change
Expand Up @@ -842,7 +842,12 @@ impl<Fp: Field> Env<Fp> {
/// Execute a single step in the RISCV32i program
pub fn step(&mut self) -> Instruction {
self.reset_scratch_state();
let (opcode, _instruction) = self.decode_instruction();
let (opcode, instruction) = self.decode_instruction();

println!(
"Executing {:#10x}: {:} {:#10x}",
self.registers.current_instruction_pointer, opcode, instruction
);

interpreter::interpret_instruction(self, opcode);

Expand Down
19 changes: 19 additions & 0 deletions o1vm/tests/test_riscv_elf.rs
Original file line number Diff line number Diff line change
Expand Up @@ -447,3 +447,22 @@ fn test_jal() {
assert_eq!(witness.registers[T0], 12);
assert_eq!(witness.registers[T1], 7);
}

#[test]
fn test_mersenne_prime() {
let curr_dir = std::env::current_dir().unwrap();
let path = curr_dir.join(std::path::PathBuf::from(
"resources/programs/riscv32im/bin/mersenne_31",
));

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();
}

let sp = witness.registers[Sp];
let v = witness.get_uint32(sp);
assert_eq!(v, 4);
}

0 comments on commit bf9f0c6

Please sign in to comment.