Fix/modexp audit

main/modexp/array_lib/array_add_AGTB.zkasm

@@ -23,10 +23,10 @@
 ; code
 ; --------------------------
 ; first_iteration           <-- Compute a[0] + b[0]
-; while(inB_index_check) {  <-- While 0 < i < len(b)
+; while(inB_index_check) {  <-- While 1 <= i < len(b)
 ;     loop2inB              <-- Compute a[i] + b[i] + carry
 ; }
-; while (inA_index_check) { <-- While 0 < i < len(a)
+; while (inA_index_check) { <-- While len(b) <= i < len(a)
 ;     loop2inA              <-- Compute a[i] + carry
 ; }
 ; 1] check_carry            <-- If there is a carry, append it to the result
@@ -36,7 +36,7 @@
 
 VAR GLOBAL array_add_AGTB_inA[%ARRAY_MAX_LEN_DOUBLED]
 VAR GLOBAL array_add_AGTB_inB[%ARRAY_MAX_LEN]
-VAR GLOBAL array_add_AGTB_out[%ARRAY_MAX_LEN_DOUBLED] ; This cannot be bigger because we use it for division checking
+VAR GLOBAL array_add_AGTB_out[%ARRAY_MAX_LEN_DOUBLED] ; This cannot be higher because we use it for division checking
 VAR GLOBAL array_add_AGTB_len_inA
 VAR GLOBAL array_add_AGTB_len_inB
 VAR GLOBAL array_add_AGTB_len_out

main/modexp/array_lib/array_add_short.zkasm

@@ -19,7 +19,7 @@
 ; code
 ; --------------------------
 ; first_iteration           <-- Compute a[0] + b
-; while(loop_index_check) { <-- While 0 < i < len(a)
+; while(loop_index_check) { <-- While 1 <= i < len(a)
 ;     loop2inA              <-- Compute a[i] + carry
 ; }
 ; 1] check_carry            <-- If there is a carry, append it to the result
@@ -29,7 +29,7 @@
 
 VAR GLOBAL array_add_short_inA[%ARRAY_MAX_LEN]
 VAR GLOBAL array_add_short_inB
-VAR GLOBAL array_add_short_out[%ARRAY_MAX_LEN] ; This cannot be bigger because we use it for division checking
+VAR GLOBAL array_add_short_out[%ARRAY_MAX_LEN] ; This cannot be higher because we use it for division checking
 VAR GLOBAL array_add_short_len_inA
 VAR GLOBAL array_add_short_len_out
 

main/modexp/array_lib/array_div_long.zkasm

@@ -1,5 +1,5 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  PRE: The input arrays have been trimmed, len(inB) >= 2 and therefore inB != 0
+;;  PRE: The input arrays have been trimmed, len(inB) >= 2 and therefore inB != 0,1.
 ;; POST: The quotient and remainder are trimmed.
 ;;
 ;; array_div_long:
@@ -58,7 +58,7 @@
 
 VAR GLOBAL array_div_long_inA[%ARRAY_MAX_LEN_DOUBLED]
 VAR GLOBAL array_div_long_inB[%ARRAY_MAX_LEN]
-VAR GLOBAL array_div_long_quo[%ARRAY_MAX_LEN_DOUBLED_MINUS_ONE]
+VAR GLOBAL array_div_long_quo[%ARRAY_MAX_LEN_DOUBLED_MINUS_ONE] ; Note: This cannot be higher because len(inB) >= 2
 VAR GLOBAL array_div_long_rem[%ARRAY_MAX_LEN]
 
 VAR GLOBAL array_div_long_len_inA
@@ -131,6 +131,7 @@ array_div_long_inA_not_zero_two_chunks:
         ; where i is the first different chunk from 0 to len(inA)
 
         RR          :JMPN(array_div_long_check_inALTinB)
+        ; inA > inB
 
         C - RR      :JMPN(failAssert) ; if C < RR ERROR
 
@@ -231,7 +232,6 @@ array_div_long_inAGTinB:
 
         C               :MSTORE(array_div_long_len_quo)
         $ => D          :MLOAD(array_div_long_len_inB)
-        C - 1 => RR
         D - 1 => E
 
         ; save the first non-zero chunk of quo

main/modexp/array_lib/array_div_short.zkasm

@@ -1,5 +1,5 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;  PRE: The input arrays have been trimmed and inB != 0.
+;;  PRE: The input arrays have been trimmed and inB != 0,1.
 ;; POST: The quotient is trimmed.
 ;;
 ;; array_div_short:
@@ -55,14 +55,16 @@ array_div_short:
         C               :MSTORE(array_div_short_len_quo)
 
         ; Let's cover the edge cases
-        ; Is C == 1 and inA == 0?
+        ; 1] Is C == 1 and inA == 0?
         C - 1           :JMPNZ(array_div_short_inAGTinB) ; If len(inA) > 1, then we already know that inA > inB
-        $ => A          :MLOAD(array_div_short_inA); Here, len(inA) = len(inB) = 1
+
+        ; Here, len(inA) = len(inB) = 1
+        $ => A          :MLOAD(array_div_short_inA)
         0 => B
         $               :EQ, JMPC(array_div_short_inA_is_zero)
 
 array_div_short_equal_len:
-        ; Here, C = 1
+        ; 2] Check if inA = inB, inA < inB or inA > inB
 
         ; If the lengths are equal, then we must compare the only chunk
         $0{signedComparison(addr.array_div_short_inA,addr.array_div_short_inB)} => RR :JMPZ(array_div_short_check_same_input)
@@ -76,9 +78,7 @@ array_div_short_equal_len:
 
         RR          :JMPN(array_div_short_check_inALTinB)
 
-        1 - RR      :JMPN(failAssert) ; if 1 < RR ERROR
-
-        ; Ensure that the chunk is higher
+        ; Ensure inB < inA
         $ => A          :MLOAD(array_div_short_inB)
         $ => B          :MLOAD(array_div_short_inA)
         1               :LT, JMP(array_div_short_inAGTinB)
@@ -101,8 +101,7 @@ array_div_short_same_input:
         0               :MSTORE(array_div_short_rem), JMP(array_div_short_end)
 
 array_div_short_check_inALTinB:
-        RR + 1          :JMPN(failAssert) ; if RR < -1 ERROR
-
+        ; Ensure inA < inB
         $ => A          :MLOAD(array_div_short_inA)
         $ => B          :MLOAD(array_div_short_inB)
         1               :LT
@@ -138,7 +137,6 @@ array_div_short_inAGTinB:
         ; 3] Let's multiply the quotient by inB
 
         C               :MSTORE(array_div_short_len_quo)
-        C - 1 => RR
 
         ; save the first non-zero chunk of quo
         A               :MSTORE(array_div_short_quo + RR)
@@ -200,7 +198,6 @@ array_div_short_check_result_eq_inA1:
         A               :MLOAD(array_div_short_inA + RR)
         RR - 1 => RR    :JMPN(array_div_short_end, array_div_short_check_result_eq_inA1)
 
-
 ; Path with remainder equal to 0
 array_div_short_rem_is_zero:
         0               :ASSERT, MSTORE(array_div_short_rem)

main/modexp/array_lib/array_div_two.zkasm

@@ -51,14 +51,17 @@ array_div_two:
         C               :MSTORE(array_div_two_len_quo)
 
         ; Let's cover the edge cases
-        0 => B
         ; 1] Is C == 1 and in == 0?
         C - 1           :JMPNZ(array_div_two_inAGTinB) ; If len(in) > 1, then we already know that in > 2
-        $ => A          :MLOAD(array_div_two_in); Here, len(in) = 1
-        $               :EQ, JMPC(array_div_two_inALTinB)
+
         ; Here, len(in) = 1
+        $ => A          :MLOAD(array_div_two_in)
+        0 => B
+        $               :EQ, JMPC(array_div_two_inALTinB)
 
+array_div_two_equal_len:
         ; 2] Check if in = 2, in < 2 or in > 2
+
         ; If the lengths are equal, then we must compare the only chunk
         $0{signedComparisonWithConst(addr.array_div_two_in,2)} => RR :JMPZ(array_div_two_check_same_input)
 
@@ -71,9 +74,7 @@ array_div_two:
 
         RR          :JMPN(array_div_two_check_inALTtwo)
 
-        1 - RR      :JMPN(failAssert) ; if 1 < RR ERROR
-
-        ; Ensure that the chunk is higher
+        ; Ensure 2 < inA
         2 => A
         $ => B          :MLOAD(array_div_two_in)
         1               :LT, JMP(array_div_two_inAGTinB)
@@ -88,14 +89,11 @@ array_div_two_same_input:
         1               :MSTORE(array_div_two_len_quo), JMP(array_div_two_end)
 
 array_div_two_check_inALTtwo:
-        RR + 1          :JMPN(failAssert) ; if RR < -1 ERROR
-
-        $ => A          :MLOAD(array_div_two_in)
-        2 => B
-        1               :LT
+        ; Ensure in < 2 <-> in == 1
+        1               :MLOAD(array_div_two_in)
 
 array_div_two_inALTinB:
-        ; If in < 2, then the result is 0
+        ; If in == 1, then the result is 0
         0               :MSTORE(array_div_two_quo)
         1               :MSTORE(array_div_two_len_quo), JMP(array_div_two_end)
 ; End of edge cases
@@ -123,7 +121,6 @@ array_div_two_inAGTinB:
         ; 3] Let's multiply the quotient by 2
 
         C               :MSTORE(array_div_two_len_quo)
-        C - 1 => RR
 
         ; save the first non-zero chunk of quo
         A               :MSTORE(array_div_two_quo + RR)
@@ -146,13 +143,8 @@ array_div_two_mul_quo_inB:
 
         ${A == 0}       :JMPNZ(array_div_two_rem_is_zero)
 
-        ; Check that the remainder is not zero
-        0 => B
-        0               :EQ
-
-        ; We must ensure the the remaider is lower than 2
-        2 => B
-        1               :LT
+        ; Check that the remainder is 1 < 2
+        1               :ASSERT
 
         A               :MSTORE(array_add_short_inB)
 
@@ -178,16 +170,15 @@ array_div_two_check_result_eq_inA1:
         A               :MLOAD(array_div_two_in + RR)
         RR - 1 => RR    :JMPN(array_div_two_end, array_div_two_check_result_eq_inA1)
 
-
 ; Path with remainder equal to 0
 array_div_two_rem_is_zero:
         0               :ASSERT
 
-        ; The length of q·b must be the same as the input of a
+        ; The length of q·2 must be the same as the input of a
         $ => C          :MLOAD(array_div_two_len_in)
         C               :MLOAD(array_mul_two_len_out)
 
-        ; Check that input == 2·quo + 0
+        ; Check that input == q·2 + 0
         C - 1 => RR
 array_div_two_check_result_eq_inA2:
         $ => A          :MLOAD(array_mul_two_out + RR)

main/modexp/array_lib/array_mul_long.zkasm

@@ -37,7 +37,7 @@
 
 VAR GLOBAL array_mul_long_inA[%ARRAY_MAX_LEN_DOUBLED]
 VAR GLOBAL array_mul_long_inB[%ARRAY_MAX_LEN]
-VAR GLOBAL array_mul_long_out[%ARRAY_MAX_LEN_DOUBLED] ; This cannot be bigger because we use it for division checking
+VAR GLOBAL array_mul_long_out[%ARRAY_MAX_LEN_DOUBLED] ; This cannot be higher because it is used for division checking (in the w.c.)
 VAR GLOBAL array_mul_long_len_inA
 VAR GLOBAL array_mul_long_len_inB
 VAR GLOBAL array_mul_long_len_out
@@ -82,7 +82,7 @@ array_mul_long_first_iteration_first_row:
 
         ; out[1] = carry
         1 => RR
-        D => C          :MSTORE(array_mul_long_out + RR)
+        D => C          :MSTORE(array_mul_long_out + RR) ; The store is not needed, but it is included for clarity
 
 array_mul_long_finish_first_row:
         ; The result will be stored as D·base + C

main/modexp/array_lib/array_mul_short.zkasm

@@ -50,7 +50,7 @@ array_mul_short:
 array_mul_short_first_iteration:
         ; The result will be stored as D·base + C
 
-        ; 1] a[0] * b, where a[0],b ∈ [0,base-1]: This number cannot be GT (base - 1)·base, two chunks
+        ; 1] a[0]·b, where a[0],b ∈ [0,base-1]: This number cannot be GT (base - 1)·base, two chunks
         $ => A          :MLOAD(array_mul_short_inA)
         $ => B          :MLOAD(array_mul_short_inB)
         0 => C
@@ -69,7 +69,7 @@ array_mul_short_loop_index_check:
 array_mul_short_loop2inA:
         ; The result will be stored as D·base + C
 
-        ; 1] a[i] * b + carry, where a[i],b,carry ∈ [0,base-1]: This number cannot be GT (base - 1)·base, two chunks
+        ; 1] a[i]·b + carry, where a[i],b,carry ∈ [0,base-1]: This number cannot be GT (base - 1)·base, two chunks
         $ => A          :MLOAD(array_mul_short_inA + E)
         D => C
         $${var _arrayShortMul_AB = A*B + C}
@@ -83,6 +83,7 @@ array_mul_short_loop2inA:
 
 ; If the last carry > 0, we need to insert it to the output
 array_mul_short_check_carry:
+        ; D = carry, E = last_index_out
         D => A
         0 => B
         $               :EQ, JMPC(array_mul_short_trim)

main/modexp/array_lib/array_mul_two.zkasm

@@ -18,7 +18,7 @@
 ; code
 ; --------------------------
 ; first_iteration           <-- a[0] + a[0]
-; while(loop_index_check) { <-- While 0 < i < len(a)
+; while(loop_index_check) { <-- While 1 <= i < len(a)
 ;     loop2in               <-- Compute a[i] + a[i] + carry
 ; }
 ; 1] check_carry            <-- If there is a carry, append it to the result
@@ -27,7 +27,7 @@
 ; --------------------------
 
 VAR GLOBAL array_mul_two_in[%ARRAY_MAX_LEN]
-VAR GLOBAL array_mul_two_out[%ARRAY_MAX_LEN]  ; This cannot be bigger because we use it for division checking
+VAR GLOBAL array_mul_two_out[%ARRAY_MAX_LEN]  ; This cannot be higher because we use it for division checking
 
 VAR GLOBAL array_mul_two_len_in
 VAR GLOBAL array_mul_two_len_out