From 3ed7c54772609e45ea8fc42de2afd3a453465551 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 15:24:51 +0100 Subject: [PATCH 01/11] o1vm/riscv32im: add runtime assertion for input invariants --- o1vm/src/interpreters/riscv32im/witness.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index c02b240bb4..011185339b 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -214,6 +214,14 @@ impl InterpreterEnv for Env { lowest_bit: u32, position: Self::Position, ) -> Self::Variable { + assert!( + lowest_bit < highest_bit, + "The lowest bit must be strictly lower than the highest bit" + ); + assert!( + highest_bit <= 32, + "The interpreter is for a 32bits architecture" + ); let x: u32 = (*x).try_into().unwrap(); let res = (x >> lowest_bit) & ((1 << (highest_bit - lowest_bit)) - 1); let res = res as u64; From e2b64e30fb06e4c7d8df5b2543a6922007d6aa6d Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 15:25:27 +0100 Subject: [PATCH 02/11] o1vm/riscv32: sign_extend - add runtime assert for input invariants --- o1vm/src/interpreters/riscv32im/interpreter.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index f27d89ec4e..6338616219 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1388,6 +1388,7 @@ pub trait InterpreterEnv { /// Given a variable `x`, this function extends it to a signed integer of /// `bitlength` bits. fn sign_extend(&mut self, x: &Self::Variable, bitlength: u32) -> Self::Variable { + assert!(bitlength <= 32); // FIXME: Constrain `high_bit` let high_bit = { let pos = self.alloc_scratch(); From 921811bd41c0ce1b786712ebe307ce1198bfb017 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 15:25:58 +0100 Subject: [PATCH 03/11] o1vm/riscv32im: sign_extend - make it friendly with overflow checks When bitlength = 0 and when compiling with `-Coverflow-checks=y`, the runtime alerts us that there is an overflow while shifting. Lifting the type to u64 and cast the value as u32 when the computation is done. --- o1vm/src/interpreters/riscv32im/interpreter.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index 6338616219..e960a93fb4 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -1394,7 +1394,13 @@ pub trait InterpreterEnv { let pos = self.alloc_scratch(); unsafe { self.bitmask(x, bitlength, bitlength - 1, pos) } }; - high_bit * Self::constant(((1 << (32 - bitlength)) - 1) << bitlength) + x.clone() + // Casting in u64 for special case of bitlength = 0 to avoid overflow. + // No condition for constant time execution. + // Decomposing the steps for readability. + let v: u64 = (1u64 << (32 - bitlength)) - 1; + let v: u64 = v << bitlength; + let v: u32 = v as u32; + high_bit * Self::constant(v) + x.clone() } fn report_exit(&mut self, exit_code: &Self::Variable); From 177a9d5d245d1e438d2be6b279e343b575c39d00 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 14:00:22 +0100 Subject: [PATCH 04/11] o1vm/riscv: sll tests - inline exit_success --- o1vm/resources/programs/riscv32im/src/sll.S | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/o1vm/resources/programs/riscv32im/src/sll.S b/o1vm/resources/programs/riscv32im/src/sll.S index 0f8cedd065..daf76f7fb8 100644 --- a/o1vm/resources/programs/riscv32im/src/sll.S +++ b/o1vm/resources/programs/riscv32im/src/sll.S @@ -1,6 +1,8 @@ .global _start -exit_success: +_start: + lui t0, 0x42 + sll t0, t0, 2 li a0, 0 li a1, 0 li a2, 0 @@ -10,8 +12,3 @@ exit_success: li a6, 0 li a7, 42 ecall - -_start: - lui t0, 0x42 - sll t0, t0, 2 - jal exit_success From d2d8d97309c6b9bd3843afaef6c6c0e3d57ecd4b Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 14:00:46 +0100 Subject: [PATCH 05/11] o1vm/riscv32: run build-riscv32-programs --- o1vm/resources/programs/riscv32im/bin/sll | Bin 456 -> 452 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/o1vm/resources/programs/riscv32im/bin/sll b/o1vm/resources/programs/riscv32im/bin/sll index f5a7fc75b1f62ac9d2aebd97981d7a0843554b68..a6fbe52b56bbec3057643a92f1fd6c6ed9c74f29 100755 GIT binary patch delta 91 zcmX@Xe1v&|1ZN2YBZCP81B1#$MRCRj6D_sH7XW!6%nHN|0t^h>l~@=iPg0s#tU7VY d0Y;t4sf@~u3nq6ms!RL_Do_Tgf&xY;4FGX*5QhK& delta 86 zcmX@Ye1ds`1m_F}Mg|iG1_q6ZisFn*CR%FqF9GsEm=%Z_1Q;e(tMY7DVqus(Nr~b8 lhxoq}7aU+Tn4HL{%nDKzKY1gg@Z>p+0!++|lh-kd0RVou72E&- From 763521614321f795e5e1a5d44db4f684c493fa20 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 14:01:19 +0100 Subject: [PATCH 06/11] o1vm/riscv32: stop ignoring sll.S test --- o1vm/tests/test_riscv_elf.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index 8aba68fd3f..343cbfb73c 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -88,10 +88,7 @@ fn test_fibonacci_7() { } } -// FIXME: stop ignore when all the instructions necessary for running this -// program are implemented. #[test] -#[ignore] fn test_sll() { let curr_dir = std::env::current_dir().unwrap(); let path = curr_dir.join(std::path::PathBuf::from( From ae5870f163a5da2bc398674ae280f6d1883cd91e Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 14:01:52 +0100 Subject: [PATCH 07/11] Ignore object files from o1vm programs --- .gitignore | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 67a6dff458..c6f644327e 100644 --- a/.gitignore +++ b/.gitignore @@ -41,4 +41,5 @@ meta.json state.json # Directory for the RISC-V 32bits toolchain -_riscv32-gnu-toolchain \ No newline at end of file +_riscv32-gnu-toolchain +o1vm/resources/programs/riscv32im/bin/*.o \ No newline at end of file From 5dc6d5759b45ead66c2d033793bf738387ae97dc Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 14:14:07 +0100 Subject: [PATCH 08/11] o1vm/riscv32: update sll program to get a more predictable input --- o1vm/resources/programs/riscv32im/src/sll.S | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/o1vm/resources/programs/riscv32im/src/sll.S b/o1vm/resources/programs/riscv32im/src/sll.S index daf76f7fb8..e343543e81 100644 --- a/o1vm/resources/programs/riscv32im/src/sll.S +++ b/o1vm/resources/programs/riscv32im/src/sll.S @@ -1,7 +1,9 @@ .global _start _start: - lui t0, 0x42 + # Load 2^12 in the register t0 + lui t0, 0b1 + # Multiply by 4 sll t0, t0, 2 li a0, 0 li a1, 0 From e267608fc3df2db7602b9eb2c0a91c01b7561826 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 14:14:32 +0100 Subject: [PATCH 09/11] o1vm/riscv32: run make build-riscv32im-programs --- o1vm/resources/programs/riscv32im/bin/sll | Bin 452 -> 452 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/o1vm/resources/programs/riscv32im/bin/sll b/o1vm/resources/programs/riscv32im/bin/sll index a6fbe52b56bbec3057643a92f1fd6c6ed9c74f29..14d0b82f86ad9a542d07cfc83ab024dc1483e35a 100755 GIT binary patch delta 13 UcmX@Ye1v&IDU%Sx#&Taq03f9V9smFU delta 13 UcmX@Ye1v&IDU%Y*#&Taq03jI!G5`Po From 1c0c81ec13214b69c3027852a7ba45b021de5843 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Sun, 22 Dec 2024 14:14:47 +0100 Subject: [PATCH 10/11] o1vm/riscv32: update with expected output --- o1vm/tests/test_riscv_elf.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index 343cbfb73c..287e91d9b2 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -101,5 +101,6 @@ fn test_sll() { witness.step(); } - // FIXME: check the state of the registers after the program has run. + // Expected output of the program + assert_eq!(witness.registers.general_purpose[5], 1 << 14) } From 826c154c1b3a36a95c86439b71ca549109a23162 Mon Sep 17 00:00:00 2001 From: Danny Willems Date: Mon, 23 Dec 2024 15:18:53 +0100 Subject: [PATCH 11/11] o1vm/riscv32im: update IP for sll As the program changed, the initial IP also changed. --- o1vm/tests/test_riscv_elf.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index 287e91d9b2..c2925b7b10 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -15,8 +15,8 @@ fn test_registers_indexed_by_alias() { let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); let witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); - assert_eq!(witness.registers[Ip], 65688); - assert_eq!(witness.registers[NextIp], 65692); + assert_eq!(witness.registers[Ip], 65652); + assert_eq!(witness.registers[NextIp], 65656); } #[test]