From d2903a38678dcd985c04e7eca3be60292c346ac6 Mon Sep 17 00:00:00 2001 From: svv232 Date: Sun, 1 Dec 2024 16:40:48 -0500 Subject: [PATCH 1/4] fixing the parsing and constraint generation for sbtype instructions --- .../src/interpreters/riscv32im/interpreter.rs | 65 ++++++++++++++----- 1 file changed, 50 insertions(+), 15 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 3ae830de49..04d50853f2 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2066,9 +2066,11 @@ pub fn interpret_stype(env: &mut Env, instr: SInstruction) /// Following the documentation found /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction) { + /* fetch instruction pointer from the program state */ let instruction_pointer = env.get_instruction_pointer(); + /* compute the next instruction ptr and add one, as well record raml lookup */ let _next_instruction_pointer = env.get_next_instruction_pointer(); - + /* read instruction from ip address */ let instruction = { let v0 = env.read_memory(&instruction_pointer); let v1 = env.read_memory(&(instruction_pointer.clone() + Env::constant(1))); @@ -2079,20 +2081,15 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction + (v1 * Env::constant(1 << 8)) + v0 }; + /* fetch opcode from instruction bit 0 - 6 for a total len of 7 */ let opcode = { let pos = env.alloc_scratch(); unsafe { env.bitmask(&instruction, 7, 0, pos) } }; + /* verify opcode is 7 bits */ env.range_check8(&opcode, 7); - // FIXME: trickier - let imm1 = { - let pos = env.alloc_scratch(); - unsafe { env.bitmask(&instruction, 12, 7, pos) } - }; - env.range_check8(&imm1, 5); - let funct3 = { let pos = env.alloc_scratch(); unsafe { env.bitmask(&instruction, 15, 12, pos) } @@ -2111,14 +2108,52 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction }; env.range_check8(&rs2, 5); - // FIXME: trickier - let imm2 = { - let pos = env.alloc_scratch(); - unsafe { env.bitmask(&instruction, 32, 25, pos) } - }; - env.range_check16(&imm2, 12); + let imm0_12 = { + let imm11 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 8, 7, pos) } + }; - // FIXME: check correctness of decomposition + env.range_check8(&imm11, 1); + + let imm1_4 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 12, 8, pos) } + }; + env.range_check8(&imm1_4, 4); + + let imm5_10 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 31, 25, pos) } + }; + env.range_check8(&imm5_10, 6); + + let imm12 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 32, 31, pos) } + }; + env.range_check8(&imm12, 1); + + // check correctness of decomposition of SB type function + env.add_constraint( + instruction.clone() + - (opcode * Env::constant(1 << 0)) // opcode at bits 0-7 + - (imm11.clone() * Env::constant(1 << 7)) // imm11 at bits 8 + - (imm1_4.clone() * Env::constant(1 << 8)) // imm1_4 at bits 9-11 + - (funct3 * Env::constant(1 << 11)) // funct3 at bits 11-14 + - (rs1 * Env::constant(1 << 14)) // rs1 at bits 15-20 + - (rs2 * Env::constant(1 << 19)) // rs2 at bits 20-24 + - (imm5_10.clone() * Env::constant(1 << 24)) // imm5_10 at bits 25-30 + - (imm12.clone() * Env::constant(1 << 31)), // imm12 at bits 31 + ); + + (imm12 * Env::constant(1 << 12)) + + (imm11 * Env::constant(1 << 11)) + + (imm5_10 * Env::constant(1 << 5)) + + (imm1_4 * Env::constant(1 << 1)) + }; + // extra bit is because the 0th bit in the immediate is always 0 i.e you cannot jump to an odd address + let _imm0_12 = env.sign_extend(&imm0_12, 13); match instr { SBInstruction::BranchEq => { From 767719a0ce0afb214ab8a8b065f80278dbe7bfa5 Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 23 Dec 2024 15:04:17 -0500 Subject: [PATCH 2/4] removing comments for instruction parsing, as these are now clarified by the tests --- o1vm/src/interpreters/riscv32im/interpreter.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 04d50853f2..5da6951177 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2066,9 +2066,7 @@ pub fn interpret_stype(env: &mut Env, instr: SInstruction) /// Following the documentation found /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction) { - /* fetch instruction pointer from the program state */ let instruction_pointer = env.get_instruction_pointer(); - /* compute the next instruction ptr and add one, as well record raml lookup */ let _next_instruction_pointer = env.get_next_instruction_pointer(); /* read instruction from ip address */ let instruction = { @@ -2081,13 +2079,11 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction + (v1 * Env::constant(1 << 8)) + v0 }; - /* fetch opcode from instruction bit 0 - 6 for a total len of 7 */ - let opcode = { let pos = env.alloc_scratch(); unsafe { env.bitmask(&instruction, 7, 0, pos) } }; - /* verify opcode is 7 bits */ + env.range_check8(&opcode, 7); let funct3 = { From 758fb1ef50ef62c673d34afe08b1938bc0af49be Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 23 Dec 2024 15:16:13 -0500 Subject: [PATCH 3/4] replace range check 8 for size one with assert_boolean --- o1vm/src/interpreters/riscv32im/interpreter.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 5da6951177..2d8c51ebd2 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -2110,7 +2110,7 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction unsafe { env.bitmask(&instruction, 8, 7, pos) } }; - env.range_check8(&imm11, 1); + env.assert_boolean(&imm11); let imm1_4 = { let pos = env.alloc_scratch(); @@ -2128,7 +2128,7 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction let pos = env.alloc_scratch(); unsafe { env.bitmask(&instruction, 32, 31, pos) } }; - env.range_check8(&imm12, 1); + env.assert_boolean(&imm12); // check correctness of decomposition of SB type function env.add_constraint( From 037f60ade8101ba5d72324cd982b843f802eed5a Mon Sep 17 00:00:00 2001 From: svv232 Date: Mon, 23 Dec 2024 15:33:41 -0500 Subject: [PATCH 4/4] passing in reference to assert_boolean --- o1vm/src/interpreters/riscv32im/interpreter.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 2d8c51ebd2..702e7ba2ab 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -594,9 +594,9 @@ pub trait InterpreterEnv { fn check_boolean(x: &Self::Variable); /// Assert that the value `x` is boolean, and add a constraint in the proof system. - fn assert_boolean(&mut self, x: Self::Variable) { - Self::check_boolean(&x); - self.add_constraint(x.clone() * x.clone() - x); + fn assert_boolean(&mut self, x: &Self::Variable) { + Self::check_boolean(x); + self.add_constraint(x.clone() * x.clone() - x.clone()); } fn add_lookup(&mut self, lookup: Lookup);