diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index be318bb0a6..5c70bf9b8c 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -17,7 +17,7 @@ - [Commitments](./fundamentals/zkbook_commitment.md) - [Polynomial Commitments](./plonk/polynomial_commitments.md) - [Inner Product Argument](./plonk/inner_product.md) - - [Different Functionnalities](./plonk/inner_product_api.md) + - [Different Functionalities](./plonk/inner_product_api.md) - [Two Party Computation](./fundamentals/zkbook_2pc/overview.md) - [Garbled Circuits](./fundamentals/zkbook_2pc/gc.md) - [Basics](./fundamentals/zkbook_2pc/basics.md) diff --git a/book/src/plonk/zkpm.md b/book/src/plonk/zkpm.md index 4820a55095..e35dcff645 100644 --- a/book/src/plonk/zkpm.md +++ b/book/src/plonk/zkpm.md @@ -58,7 +58,7 @@ $$ = Z(\omega h)[(a(h) + \beta S_{\sigma1}(h) + \gamma)(b(h) + \beta S_{\sigma2}(h) + \gamma)(c(h) + \beta S_{\sigma3}(h) + \gamma)]$$ -The modified permuation checks that ensures that the check is performed only on all the values except the last $k$ elements in the witness polynomials are as follows. +The modified permutation checks that ensures that the check is performed only on all the values except the last $k$ elements in the witness polynomials are as follows. * For all $h \in H$, $L_1(h)(Z(h) - 1) = 0$ * For all $h \in \blue{H\setminus \{h_{n-k}, \ldots, h_n\}}$, $$\begin{aligned} & Z(h)[(a(h) + \beta h + \gamma)(b(h) + \beta k_1 h + \gamma)(c(h) + \beta k_2 h + \gamma)] \\ diff --git a/o1vm/README-optimism.md b/o1vm/README-optimism.md index 740d495a34..4ce5014df5 100644 --- a/o1vm/README-optimism.md +++ b/o1vm/README-optimism.md @@ -3,7 +3,7 @@ Install the first dependencies: ``` sudo apt update -# chrony will ensure the system clock is open to date +# chrony will ensure the system clock is up to date sudo apt install build-essential git vim chrony ufw -y ``` diff --git a/o1vm/resources/programs/riscv32im/bin/add_sub_swap b/o1vm/resources/programs/riscv32im/bin/add_sub_swap new file mode 100755 index 0000000000..292b82f40d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/add_sub_swap differ diff --git a/o1vm/resources/programs/riscv32im/bin/addi_boundary_immediate b/o1vm/resources/programs/riscv32im/bin/addi_boundary_immediate new file mode 100755 index 0000000000..65f5381c3c Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/addi_boundary_immediate differ diff --git a/o1vm/resources/programs/riscv32im/bin/addi_negative b/o1vm/resources/programs/riscv32im/bin/addi_negative index f610f7df86..5d3eca47c2 100755 Binary files a/o1vm/resources/programs/riscv32im/bin/addi_negative and b/o1vm/resources/programs/riscv32im/bin/addi_negative differ diff --git a/o1vm/resources/programs/riscv32im/bin/addi_overflow b/o1vm/resources/programs/riscv32im/bin/addi_overflow new file mode 100755 index 0000000000..d6df4b003c Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/addi_overflow differ diff --git a/o1vm/resources/programs/riscv32im/bin/and b/o1vm/resources/programs/riscv32im/bin/and new file mode 100755 index 0000000000..4b645914a8 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/and differ diff --git a/o1vm/resources/programs/riscv32im/bin/div_by_zero b/o1vm/resources/programs/riscv32im/bin/div_by_zero new file mode 100755 index 0000000000..57cd40f70d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/div_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/divu_by_zero b/o1vm/resources/programs/riscv32im/bin/divu_by_zero new file mode 100755 index 0000000000..494eedac4b Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/divu_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/jal b/o1vm/resources/programs/riscv32im/bin/jal new file mode 100755 index 0000000000..4b662e82bf Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/jal differ diff --git a/o1vm/resources/programs/riscv32im/bin/mul_overflow b/o1vm/resources/programs/riscv32im/bin/mul_overflow new file mode 100755 index 0000000000..3dd27cf465 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/mul_overflow differ diff --git a/o1vm/resources/programs/riscv32im/bin/rem_by_zero b/o1vm/resources/programs/riscv32im/bin/rem_by_zero new file mode 100755 index 0000000000..293f8dd5a2 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/rem_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/remu_by_zero b/o1vm/resources/programs/riscv32im/bin/remu_by_zero new file mode 100755 index 0000000000..b6dc591d1d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/remu_by_zero differ diff --git a/o1vm/resources/programs/riscv32im/bin/slt b/o1vm/resources/programs/riscv32im/bin/slt new file mode 100755 index 0000000000..4f8906dd86 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/slt differ diff --git a/o1vm/resources/programs/riscv32im/bin/sub b/o1vm/resources/programs/riscv32im/bin/sub new file mode 100755 index 0000000000..49411f110d Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/sub differ diff --git a/o1vm/resources/programs/riscv32im/bin/sub_2 b/o1vm/resources/programs/riscv32im/bin/sub_2 new file mode 100755 index 0000000000..964e9c737a Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/sub_2 differ diff --git a/o1vm/resources/programs/riscv32im/bin/sub_3 b/o1vm/resources/programs/riscv32im/bin/sub_3 new file mode 100755 index 0000000000..2bd2bff544 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/sub_3 differ diff --git a/o1vm/resources/programs/riscv32im/bin/xor b/o1vm/resources/programs/riscv32im/bin/xor new file mode 100755 index 0000000000..2a9f659899 Binary files /dev/null and b/o1vm/resources/programs/riscv32im/bin/xor differ diff --git a/o1vm/resources/programs/riscv32im/src/add_sub_swap.S b/o1vm/resources/programs/riscv32im/src/add_sub_swap.S new file mode 100644 index 0000000000..e09bf67b34 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/add_sub_swap.S @@ -0,0 +1,22 @@ +.section .text +.globl _start + +_start: + li t0, 5 # t0 = 5 + li t1, 10 # t1 = 10 + + # Swap t0 and t1 using add + add t2, t0, t1 # t2 = t0 + t1 (t2 = 5 + 10 = 15) + sub t0, t2, t0 # t0 = t2 - t0 (t0 = 15 - 5 = 10) + sub t1, t2, t1 # t1 = t2 - t1 (t1 = 15 - 10 = 5) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/addi_boundary_immediate.S b/o1vm/resources/programs/riscv32im/src/addi_boundary_immediate.S new file mode 100644 index 0000000000..241af6ea48 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/addi_boundary_immediate.S @@ -0,0 +1,20 @@ +.section .text +.globl _start + +_start: + li t0, 100 # t0 = 100 + addi t1, t0, 2047 # t1 = t0 + 2047 (Expected: t1 = 2147) + + li t2, 1000 # t2 = 1000 + addi t3, t2, -2048 # t3 = t2 + (-2048) (Expected: t1 = -1048) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/addi_negative.S b/o1vm/resources/programs/riscv32im/src/addi_negative.S index 5ef1bfda36..1b94dfb420 100644 --- a/o1vm/resources/programs/riscv32im/src/addi_negative.S +++ b/o1vm/resources/programs/riscv32im/src/addi_negative.S @@ -10,6 +10,9 @@ _start: # Subtract 100 using addi (addi with negative immediate) addi t2, t1, -100 # t2 = t1 + (-100) (Expected: t2 = -50) + li t3, -1000 # t3 = -1000 + addi t4, t3, -500 # t4 = t0 + (-500) (Expected: t4 = -1500) + # Custom exit syscall li a0, 0 li a1, 0 diff --git a/o1vm/resources/programs/riscv32im/src/addi_overflow.S b/o1vm/resources/programs/riscv32im/src/addi_overflow.S new file mode 100644 index 0000000000..c1539b05a4 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/addi_overflow.S @@ -0,0 +1,23 @@ +.section .text +.globl _start + +_start: + li t0, 2147483647 # t0 = 2147483647 (Max 32-bit signed int) + addi t1, t0, 1 # t1 = t0 + 1 (Expected: overflow to -2147483648) + + li t2, -2147483648 # t2 = -2147483648 (Min 32-bit signed int) + addi t3, t2, -1 # t3 = t2 + (-1) (Expected: overflow to 2147483647) + + li t4, 123456789 # t4 = 123456789 + addi t5, t4, 0 # t5 = t4 + 0 (Expected: t4 = 123456789) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/and.S b/o1vm/resources/programs/riscv32im/src/and.S new file mode 100644 index 0000000000..4bab937b9b --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/and.S @@ -0,0 +1,30 @@ +.section .text +.globl _start + +_start: + + # Simple AND + li t0, 0b1100 # t0 = 0b1100 + li t1, 0b1010 # t1 = 0b1010 + and t2, t0, t1 # t2 = t0 & t1 (Expected: t2 = 0b1000) + + # AND with zero (result always zero) + li t3, 0b1111 # t3 = 0b1111 + li t4, 0 # t4 = 0 + and t5, t3, t4 # t5 = t3 & t4 (Expected: t5 = 0) + + # AND of identical values (result same value) + li t6, 0b1010 # t6 = 0b1010 + li t0, 0b1010 # t0 = 0b1010 + and t1, t6, t0 # t1 = t6 & t0 (Expected: t1 = 0b1010) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/div_by_zero.S b/o1vm/resources/programs/riscv32im/src/div_by_zero.S new file mode 100644 index 0000000000..5f8c490924 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/div_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Signed division by zero (div) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + div t2, t0, t1 # t2 = t0 / t1 (Expected: division by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/divu_by_zero.S b/o1vm/resources/programs/riscv32im/src/divu_by_zero.S new file mode 100644 index 0000000000..b44ff50479 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/divu_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Unsigned division by zero (div) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + divu t2, t0, t1 # t2 = t0 / t1 (Expected: division by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/jal.S b/o1vm/resources/programs/riscv32im/src/jal.S new file mode 100644 index 0000000000..191cdfbb3e --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/jal.S @@ -0,0 +1,25 @@ +.section .text +.global _start + +# t0 <- t0 + t1 +add_t0_t1: + add t0, t0, t1 + ret + +_start: + li t0, 5 + li t1, 7 + # Could be jalr + # jal without offset + jal ra, add_t0_t1 + + # exit + 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 diff --git a/o1vm/resources/programs/riscv32im/src/mul_overflow.S b/o1vm/resources/programs/riscv32im/src/mul_overflow.S new file mode 100644 index 0000000000..c7cced4253 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/mul_overflow.S @@ -0,0 +1,18 @@ +.section .text +.globl _start + +_start: + li t0, 10000000 # Large number + li t1, 10000000 # Another large number + mul t2, t0, t1 # Test large multiplication (Expected overflow) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/rem_by_zero.S b/o1vm/resources/programs/riscv32im/src/rem_by_zero.S new file mode 100644 index 0000000000..bc9c4fb2eb --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/rem_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Signed remainder by zero (rem) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + rem t2, t0, t1 # t2 = t0 % t1 (Expected: remainder by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/remu_by_zero.S b/o1vm/resources/programs/riscv32im/src/remu_by_zero.S new file mode 100644 index 0000000000..fe11257f26 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/remu_by_zero.S @@ -0,0 +1,19 @@ +.section .text +.globl _start + +_start: + # Unsigned remainder by zero (remu) + li t0, 42 # t0 = 42 + li t1, 0 # t1 = 0 + remu t2, t0, t1 # t2 = t0 % t1 (Expected: remainder by zero) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/slt.S b/o1vm/resources/programs/riscv32im/src/slt.S new file mode 100644 index 0000000000..42ff3e513e --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/slt.S @@ -0,0 +1,30 @@ +.section .text +.globl _start + +_start: + + # SLT with t0 < t1 (Expected: 1) + li t0, 100 # t0 = 100 + li t1, 200 # t1 = 200 + slt t2, t0, t1 # t2 = (t0 < t1) ? 1 : 0 (Expected: t2 = 1) + + # SLT with t3 > t4 (Expected: 0) + li t3, 300 # t3 = 300 + li t4, 200 # t4 = 200 + slt t5, t3, t4 # t5 = (t3 < t4) ? 1 : 0 (Expected: t5 = 0) + + # SLT with t0 == t1 (Expected: 0) + li t0, 150 # t6 = 150 + li t1, 150 # t7 = 150 + slt t6, t0, t1 # t6 = (t0 < t1) ? 1 : 0 (Expected: t6 = 0) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/sub.S b/o1vm/resources/programs/riscv32im/src/sub.S new file mode 100644 index 0000000000..53abe9bd17 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/sub.S @@ -0,0 +1,25 @@ +.section .text +.globl _start + +_start: + + # Test 1: Simple subtraction + li t0, 1000 # t0 = 1000 + li t1, 500 # t1 = 500 + sub t2, t0, t1 # t2 = t0 - t1 (Expected: t2 = 500) + + # Test 2: Subtracting from zero + li t3, 0 # t3 = 0 + li t4, 100 # t4 = 100 + sub t5, t3, t4 # t5 = t3 - t4 (Expected: t5 = -100) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/sub_2.S b/o1vm/resources/programs/riscv32im/src/sub_2.S new file mode 100644 index 0000000000..8ccadb14ba --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/sub_2.S @@ -0,0 +1,25 @@ +.section .text +.globl _start + +_start: + + # Test 3: Subtracting a larger value (result negative) + li t0, 300 # t0 = 300 + li t1, 500 # t1 = 500 + sub t2, t0, t1 # t2 = t0 - t1 (Expected: t2 = -200) + + # Test 4: Subtracting negative values (result positive) + li t3, 100 # t3 = 100 + li t4, -50 # t4 = -50 + sub t5, t3, t4 # t5 = t3 - t4 (Expected: t5 = 150) + + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/sub_3.S b/o1vm/resources/programs/riscv32im/src/sub_3.S new file mode 100644 index 0000000000..78e90cc011 --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/sub_3.S @@ -0,0 +1,22 @@ +.section .text +.globl _start + +_start: + # Test 5: Result of subtracting from a register (using same value) + li t0, 1234 # t0 = 1234 + sub t1, t0, t0 # t1 = t0 - t0 (Expected: t1 = 0) + + # Test 6: Handling overflow (large subtraction result) + li t2, 2147483647 # t2 = 2147483647 (max positive signed 32-bit) + li t3, -1 # t3 = -1 + sub t4, t2, t3 # t4 = t2 - t3 (Expected: t0 = 2147483648, wraparound to -2147483648) + # 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 diff --git a/o1vm/resources/programs/riscv32im/src/xor.S b/o1vm/resources/programs/riscv32im/src/xor.S new file mode 100644 index 0000000000..ea78a68cca --- /dev/null +++ b/o1vm/resources/programs/riscv32im/src/xor.S @@ -0,0 +1,30 @@ +.section .text +.globl _start + +_start: + + # Simple XOR + li t0, 0b1100 # t0 = 0b1100 + li t1, 0b1010 # t1 = 0b1010 + xor t2, t0, t1 # t2 = t0 ^ t1 (Expected: t2 = 0b0110) + + # XOR with zero (no change) + li t3, 0b1010 # t3 = 0b1010 + li t4, 0 # t4 = 0 + xor t5, t3, t4 # t5 = t3 ^ t4 (Expected: t5 = 0b1010) + + # XOR of identical values (result 0) + li t6, 0b1111 # t6 = 0b1111 + li t0, 0b1111 # t0 = 0b1111 + xor t1, t6, t0 # t1 = t6 ^ t0 (Expected: t1 = 0) + + # 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 diff --git a/o1vm/src/interpreters/mips/interpreter.rs b/o1vm/src/interpreters/mips/interpreter.rs index 0ea55c67ea..5ba96d9885 100644 --- a/o1vm/src/interpreters/mips/interpreter.rs +++ b/o1vm/src/interpreters/mips/interpreter.rs @@ -934,7 +934,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); diff --git a/o1vm/src/interpreters/riscv32im/constraints.rs b/o1vm/src/interpreters/riscv32im/constraints.rs index ba1633e1a7..e45099490e 100644 --- a/o1vm/src/interpreters/riscv32im/constraints.rs +++ b/o1vm/src/interpreters/riscv32im/constraints.rs @@ -77,8 +77,8 @@ impl InterpreterEnv for Env { // No-op, witness only } - fn check_boolean(_x: &Self::Variable) { - // No-op, witness only + fn assert_boolean(&mut self, x: &Self::Variable) { + self.add_constraint(x.clone() * x.clone() - x.clone()); } fn add_lookup(&mut self, lookup: Lookup) { diff --git a/o1vm/src/interpreters/riscv32im/interpreter.rs b/o1vm/src/interpreters/riscv32im/interpreter.rs index e960a93fb4..91f100e911 100644 --- a/o1vm/src/interpreters/riscv32im/interpreter.rs +++ b/o1vm/src/interpreters/riscv32im/interpreter.rs @@ -598,14 +598,8 @@ pub trait InterpreterEnv { self.add_constraint(x - y); } - /// Check that the witness value `x` is a boolean (`0` or `1`); otherwise abort. - 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); fn add_lookup(&mut self, lookup: Lookup); @@ -1286,6 +1280,10 @@ pub trait InterpreterEnv { /// There are no constraints on the returned values; callers must manually add constraints to /// ensure that the pair of returned values correspond to the given values `x` and `y`, and /// that they fall within the desired range. + /// + /// Division by zero will create a panic! exception. The RISC-V + /// specification leaves the case unspecified, and therefore we prefer to + /// forbid this case while building the witness. unsafe fn div_signed( &mut self, x: &Self::Variable, @@ -1314,6 +1312,10 @@ pub trait InterpreterEnv { /// There are no constraints on the returned values; callers must manually add constraints to /// ensure that the pair of returned values correspond to the given values `x` and `y`, and /// that they fall within the desired range. + /// + /// Division by zero will create a panic! exception. The RISC-V + /// specification leaves the case unspecified, and therefore we prefer to + /// forbid this case while building the witness. unsafe fn div( &mut self, x: &Self::Variable, @@ -1505,11 +1507,12 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) // add: x[rd] = x[rs1] + x[rs2] let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let overflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _overflow) = - env.add_witness(&local_rs1, &local_rs2, rd_scratch, overflow_scratch); + let local_rd = { + let overflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_rs2, rd_scratch, overflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1521,11 +1524,12 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sub: x[rd] = x[rs1] - x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let underflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _underflow) = - env.sub_witness(&local_rs1, &local_rs2, rd_scratch, underflow_scratch); + let local_rd = { + let underflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _underflow) = unsafe { + env.sub_witness(&local_rs1, &local_rs2, rd_scratch, underflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1537,9 +1541,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sll: x[rd] = x[rs1] << x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let rd_scratch = env.alloc_scratch(); - env.shift_left(&local_rs1, &local_rs2, rd_scratch) + unsafe { env.shift_left(&local_rs1, &local_rs2, rd_scratch) } }; env.write_register(&rd, local_rd); @@ -1550,9 +1554,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* slt: x[rd] = (x[rs1] < x[rs2]) ? 1 : 0 */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let rd_scratch = env.alloc_scratch(); - env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) + unsafe { env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) } }; env.write_register(&rd, local_rd); @@ -1563,9 +1567,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sltu: x[rd] = (x[rs1] < (u)x[rs2]) ? 1 : 0 */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.test_less_than(&local_rs1, &local_rs2, pos) + unsafe { env.test_less_than(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1576,9 +1580,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* xor: x[rd] = x[rs1] ^ x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.xor_witness(&local_rs1, &local_rs2, pos) + unsafe { env.xor_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1589,9 +1593,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* srl: x[rd] = x[rs1] >> x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.shift_right(&local_rs1, &local_rs2, pos) + unsafe { env.shift_right(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1602,9 +1606,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* sra: x[rd] = x[rs1] >> x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.shift_right_arithmetic(&local_rs1, &local_rs2, pos) + unsafe { env.shift_right_arithmetic(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1615,9 +1619,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* or: x[rd] = x[rs1] | x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.or_witness(&local_rs1, &local_rs2, pos) + unsafe { env.or_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1628,9 +1632,9 @@ pub fn interpret_rtype(env: &mut Env, instr: RInstruction) /* and: x[rd] = x[rs1] & x[rs2] */ let local_rs1 = env.read_register(&rs1); let local_rs2 = env.read_register(&rs2); - let local_rd = unsafe { + let local_rd = { let pos = env.alloc_scratch(); - env.and_witness(&local_rs1, &local_rs2, pos) + unsafe { env.and_witness(&local_rs1, &local_rs2, pos) } }; env.write_register(&rd, local_rd); @@ -1893,11 +1897,12 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // addi: x[rd] = x[rs1] + sext(immediate) let local_rs1 = env.read_register(&(rs1.clone())); let local_imm = env.sign_extend(&imm, 12); - let overflow_scratch = env.alloc_scratch(); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { - let (local_rd, _overflow) = - env.add_witness(&local_rs1, &local_imm, rd_scratch, overflow_scratch); + let local_rd = { + let overflow_scratch = env.alloc_scratch(); + let rd_scratch = env.alloc_scratch(); + let (local_rd, _overflow) = unsafe { + env.add_witness(&local_rs1, &local_imm, rd_scratch, overflow_scratch) + }; local_rd }; env.write_register(&rd, local_rd); @@ -1908,8 +1913,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // xori: x[rd] = x[rs1] ^ sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.xor_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.xor_witness(&local_rs1, &local_imm, rd_scratch) } + }; env.write_register(&rd, local_rd); env.set_instruction_pointer(next_instruction_pointer.clone()); env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); @@ -1918,8 +1925,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // ori: x[rd] = x[rs1] | sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.or_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.or_witness(&local_rs1, &local_imm, rd_scratch) } + }; env.write_register(&rd, local_rd); env.set_instruction_pointer(next_instruction_pointer.clone()); env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); @@ -1928,8 +1937,10 @@ pub fn interpret_itype(env: &mut Env, instr: IInstruction) // andi: x[rd] = x[rs1] & sext(immediate) let local_rs1 = env.read_register(&rs1); let local_imm = env.sign_extend(&imm, 12); - let rd_scratch = env.alloc_scratch(); - let local_rd = unsafe { env.and_witness(&local_rs1, &local_imm, rd_scratch) }; + let local_rd = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.and_witness(&local_rs1, &local_imm, rd_scratch) } + }; env.write_register(&rd, local_rd); env.set_instruction_pointer(next_instruction_pointer.clone()); env.set_next_instruction_pointer(next_instruction_pointer + Env::constant(4u32)); @@ -2139,8 +2150,7 @@ pub fn interpret_stype(env: &mut Env, instr: SInstruction) /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction) { let instruction_pointer = env.get_instruction_pointer(); - let _next_instruction_pointer = env.get_next_instruction_pointer(); - + let next_instruction_pointer = env.get_next_instruction_pointer(); let instruction = { let v0 = env.read_memory(&instruction_pointer); let v1 = env.read_memory(&(instruction_pointer.clone() + Env::constant(1))); @@ -2151,19 +2161,12 @@ pub fn interpret_sbtype(env: &mut Env, instr: SBInstruction + (v1 * Env::constant(1 << 8)) + v0 }; - let opcode = { let pos = env.alloc_scratch(); unsafe { env.bitmask(&instruction, 7, 0, pos) } }; - 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); + env.range_check8(&opcode, 7); let funct3 = { let pos = env.alloc_scratch(); @@ -2183,33 +2186,210 @@ 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.assert_boolean(&imm11); + + 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.assert_boolean(&imm12); + + // 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.clone() * Env::constant(1 << 14)) // rs1 at bits 15-20 + - (rs2.clone() * 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 => { - unimplemented!("BranchEq") + // beq: if (x[rs1] == x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let equals = env.equal(&local_rs1, &local_rs2); + let offset = (Env::constant(1) - equals.clone()) * Env::constant(4) + equals * imm0_12; + let offset = env.sign_extend(&offset, 12); + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchNeq => { - unimplemented!("BranchNeq") + // bne: if (x[rs1] != x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let equals = env.equal(&local_rs1, &local_rs2); + let offset = equals.clone() * Env::constant(4) + (Env::constant(1) - equals) * imm0_12; + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchLessThan => { - unimplemented!("BranchLessThan") + // blt: if (x[rs1] < x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let less_than = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) } + }; + let offset = (less_than.clone()) * imm0_12 + + (Env::constant(1) - less_than.clone()) * Env::constant(4); + + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchGreaterThanEqual => { - unimplemented!("BranchGreaterThanEqual") + // bge: if (x[rs1] >= x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let less_than = { + let rd_scratch = env.alloc_scratch(); + unsafe { env.test_less_than_signed(&local_rs1, &local_rs2, rd_scratch) } + }; + + let offset = + less_than.clone() * Env::constant(4) + (Env::constant(1) - less_than) * imm0_12; + // greater than equal is the negation of less than + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness( + &next_instruction_pointer, + &offset, + res_scratch, + overflow_scratch, + ) + }; + // FIXME: Requires a range check + res + }; + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } SBInstruction::BranchLessThanUnsigned => { - unimplemented!("BranchLessThanUnsigned") + // bltu: if (x[rs1] { - unimplemented!("BranchGreaterThanEqualUnsigned") + // bgeu: if (x[rs1] >=u x[rs2]) pc += sext(offset) + let local_rs1 = env.read_register(&rs1); + let local_rs2 = env.read_register(&rs2); + + let rd_scratch = env.alloc_scratch(); + let less_than = unsafe { env.test_less_than(&local_rs1, &local_rs2, rd_scratch) }; + let offset = + less_than.clone() * Env::constant(4) + (Env::constant(1) - less_than) * imm0_12; + + // greater than equal is the negation of less than + let addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness(&instruction_pointer, &offset, res_scratch, overflow_scratch) + }; + res + }; + + env.set_instruction_pointer(next_instruction_pointer); + env.set_next_instruction_pointer(addr); } }; } @@ -2267,8 +2447,10 @@ pub fn interpret_utype(env: &mut Env, instr: UInstruction) UInstruction::LoadUpperImmediate => { // lui: x[rd] = sext(immediate[31:12] << 12) let local_imm = { - let pos = env.alloc_scratch(); - let shifted_imm = unsafe { env.shift_left(&imm, &Env::constant(12), pos) }; + let shifted_imm = { + let pos = env.alloc_scratch(); + unsafe { env.shift_left(&imm, &Env::constant(12), pos) } + }; env.sign_extend(&shifted_imm, 32) }; env.write_register(&rd, local_imm); @@ -2300,14 +2482,30 @@ pub fn interpret_utype(env: &mut Env, instr: UInstruction) /// Interpret an UJ-type instruction. /// The encoding of an UJ-type instruction is as follows: /// ```text -/// | 31 12 | 11 7 | 6 0 | -/// | immediate | rd | opcode | +/// | 31 12 | 11 7 | 6 0 | +/// | imm[20|10:1|11|19:12] | rd | opcode | /// ``` /// Following the documentation found /// [here](https://www.cs.cornell.edu/courses/cs3410/2024fa/assignments/cpusim/riscv-instructions.pdf) +/// +/// The interpretation of the immediate is as follow: +/// ```text +/// imm_20 = instruction[31] +/// imm_10_1 = instruction[30..21] +/// imm_11 = instruction[20] +/// imm_19_12 = instruction[19..12] +/// +/// imm = imm_20 << 19 + +/// imm_19_12 << 11 + +/// imm_11 << 10 + +/// imm_10_1 +/// +/// # The immediate is then sign-extended. The sign-extension is in the bit imm20 +/// imm = imm << 1 +/// ``` pub fn interpret_ujtype(env: &mut Env, instr: UJInstruction) { let instruction_pointer = env.get_instruction_pointer(); - let _next_instruction_pointer = env.get_next_instruction_pointer(); + let next_instruction_pointer = env.get_next_instruction_pointer(); let instruction = { let v0 = env.read_memory(&instruction_pointer); @@ -2332,18 +2530,55 @@ pub fn interpret_ujtype(env: &mut Env, instr: UJInstruction }; env.range_check8(&rd, 5); - // FIXME: trickier - let _imm = { + let imm20 = { let pos = env.alloc_scratch(); - unsafe { env.bitmask(&instruction, 32, 12, pos) } + unsafe { env.bitmask(&instruction, 32, 31, pos) } + }; + env.assert_boolean(&imm20); + + let imm10_1 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 31, 21, pos) } + }; + env.range_check16(&imm10_1, 10); + + let imm11 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 21, 20, pos) } + }; + env.assert_boolean(&imm11); + + let imm19_12 = { + let pos = env.alloc_scratch(); + unsafe { env.bitmask(&instruction, 20, 12, pos) } + }; + env.range_check8(&imm19_12, 8); + + let offset = { + imm10_1.clone() * Env::constant(1 << 1) + + imm11.clone() * Env::constant(1 << 11) + + imm19_12.clone() * Env::constant(1 << 12) + + imm20.clone() * Env::constant(1 << 20) }; // FIXME: check correctness of decomposition + match instr { UJInstruction::JumpAndLink => { - unimplemented!("JumpAndLink") + let offset = env.sign_extend(&offset, 21); + let new_addr = { + let res_scratch = env.alloc_scratch(); + let overflow_scratch = env.alloc_scratch(); + let (res, _overflow) = unsafe { + env.add_witness(&instruction_pointer, &offset, res_scratch, overflow_scratch) + }; + res + }; + env.write_register(&rd, next_instruction_pointer.clone()); + env.set_instruction_pointer(new_addr.clone()); + env.set_next_instruction_pointer(new_addr + Env::constant(4u32)); } - }; + } } pub fn interpret_syscall(env: &mut Env, _instr: SyscallInstruction) { diff --git a/o1vm/src/interpreters/riscv32im/mod.rs b/o1vm/src/interpreters/riscv32im/mod.rs index 59c855694b..ed6dd1b38a 100644 --- a/o1vm/src/interpreters/riscv32im/mod.rs +++ b/o1vm/src/interpreters/riscv32im/mod.rs @@ -1,7 +1,5 @@ /// The minimal number of columns required for the VM -// FIXME: the value will be updated when the interpreter is fully -// implemented. Using a small value for now. -pub const SCRATCH_SIZE: usize = 80; +pub const SCRATCH_SIZE: usize = 39; /// Number of instructions in the ISA pub const INSTRUCTION_SET_SIZE: usize = 48; diff --git a/o1vm/src/interpreters/riscv32im/witness.rs b/o1vm/src/interpreters/riscv32im/witness.rs index 011185339b..256de81687 100644 --- a/o1vm/src/interpreters/riscv32im/witness.rs +++ b/o1vm/src/interpreters/riscv32im/witness.rs @@ -88,8 +88,8 @@ impl InterpreterEnv for Env { assert_eq!(*x, *y); } - fn check_boolean(x: &Self::Variable) { - if !(*x == 0 || *x == 1) { + fn assert_boolean(&mut self, x: &Self::Variable) { + if *x != 0 && *x != 1 { panic!("The value {} is not a boolean", *x); } } diff --git a/o1vm/src/lookups.rs b/o1vm/src/lookups.rs index eff69771f3..5085e0dae8 100644 --- a/o1vm/src/lookups.rs +++ b/o1vm/src/lookups.rs @@ -25,23 +25,29 @@ pub(crate) type LookupTable = LogupTable; /// All of the possible lookup table IDs used in the zkVM #[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)] pub enum LookupTableIDs { - // PadLookup ID is 0 because this is the only fixed table whose first entry is not 0. - // This way, it is guaranteed that the 0 value is not always in the tables after the - // randomization with the joint combiner is applied. - /// All [1..136] values of possible padding lengths, the value 2^len, and the 5 corresponding pad suffixes with the 10*1 rule + // PadLookup ID is 0 because this is the only fixed table whose first entry + // is not 0. This way, it is guaranteed that the 0 value is not always in + // the tables after the randomization with the joint combiner is applied. + /// All [1..136] values of possible padding lengths, the value 2^len, and + /// the 5 corresponding pad suffixes with the 10*1 rule PadLookup = 0, - /// 24-row table with all possible values for round and their round constant in expanded form (in big endian) [0..=23] + /// 24-row table with all possible values for round and their round constant + /// in expanded form (in big endian) [0..=23] RoundConstantsLookup = 1, /// Values from 0 to 4 to check the number of bytes read from syscalls AtMost4Lookup = 2, - /// All values that can be stored in a byte (amortized table, better than model as RangeCheck16 (x and scaled x) + /// All values that can be stored in a byte (amortized table, better than + /// model as RangeCheck16 (x and scaled x) ByteLookup = 3, - // Read tables come first to allow indexing with the table ID for the multiplicities + // Read tables come first to allow indexing with the table ID for the + // multiplicities /// Single-column table of all values in the range [0, 2^16) RangeCheck16Lookup = 4, - /// Single-column table of 2^16 entries with the sparse representation of all values + /// Single-column table of 2^16 entries with the sparse representation of + /// all values SparseLookup = 5, - /// Dual-column table of all values in the range [0, 2^16) and their sparse representation + /// Dual-column table of all values in the range [0, 2^16) and their sparse + /// representation ResetLookup = 6, // RAM Tables @@ -123,7 +129,8 @@ impl LookupTableID for LookupTableIDs { /// Trait that creates all the fixed lookup tables used in the VM pub(crate) trait FixedLookupTables { - /// Checks whether a value is in a table and returns the position if it is or None otherwise. + /// Checks whether a value is in a table and returns the position if it is + /// or None otherwise. fn is_in_table(table: &LookupTable, value: Vec) -> Option; /// Returns the pad table fn table_pad() -> LookupTable; @@ -144,7 +151,8 @@ pub(crate) trait FixedLookupTables { impl FixedLookupTables for LookupTable { fn is_in_table(table: &LookupTable, value: Vec) -> Option { let id = table.table_id; - // In these tables, the first value of the vector is related to the index within the table. + // In these tables, the first value of the vector is related to the + // index within the table. let idx = value[0] .to_bytes() .iter() diff --git a/o1vm/tests/test_riscv_elf.rs b/o1vm/tests/test_riscv_elf.rs index 120cf6ebd1..ad83a34821 100644 --- a/o1vm/tests/test_riscv_elf.rs +++ b/o1vm/tests/test_riscv_elf.rs @@ -67,9 +67,7 @@ fn test_no_action() { assert_eq!(witness.registers.general_purpose[17], 42); } -// FIXME: stop ignoring when all the instructions are implemented. #[test] -#[ignore] fn test_fibonacci_7() { let curr_dir = std::env::current_dir().unwrap(); let path = curr_dir.join(std::path::PathBuf::from( @@ -198,4 +196,257 @@ fn test_addi_negative() { assert_eq!(witness.registers[T0], 100); assert_eq!(witness.registers[T1], 50); assert_eq!(witness.registers[T2], (-50_i32) as u32); + assert_eq!(witness.registers[T3], (-1000_i32) as u32); + assert_eq!(witness.registers[T4], (-1500_i32) as u32); +} + +#[test] +fn test_add_sub_swap() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/add_sub_swap", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 10); + assert_eq!(witness.registers[T1], 5); + assert_eq!(witness.registers[T2], 15); +} + +#[test] +fn test_addi_overflow() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/addi_overflow", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T1], (-2147483648_i32) as u32); + assert_eq!(witness.registers[T3], 2147483647); + assert_eq!(witness.registers[T5], 123456789); +} + +#[test] +fn test_addi_boundary_immediate() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/addi_boundary_immediate", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T1], 2147); + assert_eq!(witness.registers[T3], (-1048_i32) as u32); +} + +#[test] +fn test_sub() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/sub", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 500); + assert_eq!(witness.registers[T5], (-100_i32) as u32); +} + +#[test] +fn test_sub_2() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/sub_2", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], -200_i32 as u32); + assert_eq!(witness.registers[T5], 150); +} + +#[test] +fn test_sub_3() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/sub_3", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T1], 0); + assert_eq!(witness.registers[T4], -2147483648_i32 as u32); +} + +#[test] +fn test_xor() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/xor", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 0b0110); // Result: t2 = 0b0110 + assert_eq!(witness.registers[T5], 0b1010); // Result: t5 = 0b1010 + assert_eq!(witness.registers[T1], 0); // Result: t1 = 0 +} + +#[test] +fn test_and() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/and", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 0b1000); + assert_eq!(witness.registers[T5], 0); + assert_eq!(witness.registers[T1], 0b1010); +} + +#[test] +fn test_slt() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/slt", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 1); + assert_eq!(witness.registers[T5], 0); + assert_eq!(witness.registers[T6], 0); +} + +#[test] +#[should_panic] +fn test_div_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/div_by_zero", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +#[should_panic] +fn test_divu_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/divu_by_zero", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +#[should_panic] +fn test_rem_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/rem_by_zero", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +#[should_panic] +fn test_remu_by_zero() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/remu_by_zero", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } +} + +#[test] +fn test_mul_overflow() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/mul_overflow", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T2], 276447232); +} + +#[test] +fn test_jal() { + let curr_dir = std::env::current_dir().unwrap(); + let path = curr_dir.join(std::path::PathBuf::from( + "resources/programs/riscv32im/bin/jal", + )); + let state = o1vm::elf_loader::parse_riscv32(&path).unwrap(); + let mut witness = Env::::create(PAGE_SIZE.try_into().unwrap(), state); + + while !witness.halt { + witness.step(); + } + + assert_eq!(witness.registers[T0], 12); + assert_eq!(witness.registers[T1], 7); }