Merge pull request #310 from 0xPolygonHermez/feature/incaberry

Feature/incaberry
0xPolygonHermez · Nov 21, 2023 · de55837 · de55837
2 parents a4e9c3a + f3b6d78
commit de55837
Show file tree

Hide file tree

Showing 13 changed files with 396 additions and 106 deletions.
diff --git a/main/constants.zkasm b/main/constants.zkasm
@@ -9,7 +9,7 @@ CONST %LOCAL_EXIT_ROOT_STORAGE_POS = 1
 CONST %LAST_TX_STORAGE_POS = 0
 CONST %STATE_ROOT_STORAGE_POS = 1
 CONST %MAX_MEM_EXPANSION_BYTES = 0x3fffe0
-CONST %FORK_ID = 5
+CONST %FORK_ID = 6
 CONST %CALLDATA_RESERVED_CTX = 1
 
 ; RLP

diff --git a/main/ecrecover/addFpEc.zkasm b/main/ecrecover/addFpEc.zkasm
@@ -1,8 +1,13 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; addFpEc C = (A + C) % FpEc
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A,C no alias-free
+;; POST: C no alias-free (on MAP)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   2 ariths + 7 steps
 
 addFpEc:
         1 => B

diff --git a/main/ecrecover/checkSqrtFpEc.zkasm b/main/ecrecover/checkSqrtFpEc.zkasm
@@ -8,13 +8,21 @@
 ;;         BLOCK:  1         2  3        4      5       6      7
 ;;             (*) 222 + initial initialization
 ;;
-;; return 1 => no sqrts  0 => has solutions
+;; PRE: C no alias-free
+;; POST: A in [0,1]
+;; return A: A = 1 ==> C = -1 ==> hasn't root
+;;           A = 0 ==> C != -1 ==> has root or MAP, proof fails.
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 VAR GLOBAL checkSqrtFpEc_base
 VAR GLOBAL checkSqrtFpEc_RR
 
 checkSqrtFpEc:
+        ; RESOURCES:
+        ;   248 x (3 steps + 2 arith + 8 steps + 2 arith + 7 steps) = 992 ariths + 4464 steps
+        ;   6 x (1 step + 2 arith + 8 steps) = 12 ariths + 54 steps
+        ;   6 steps + 1 binary
+        ; TOTAL = 1004 ariths + 1 binary + 4524 steps
 
         RR          :MSTORE(checkSqrtFpEc_RR)
         C           :MSTORE(checkSqrtFpEc_base)
@@ -1539,7 +1547,12 @@ checkSqrtFpEc:
         C => B	:CALL(mulFpEc)
 
 
+        ; FPEC_MINUS_ONE hasn't alias of 256 bits
         C => B
         %FPEC_MINUS_ONE => A
         $ => RR     :MLOAD(checkSqrtFpEc_RR)
+
+        ; A = 1 ==> C = -1 ==> hasn't root
+        ; A = 0 ==> C != -1 ==> has root or MAP, proof fails.
+
         $ => A      :EQ,RETURN
diff --git a/main/ecrecover/ecrecover.zkasm b/main/ecrecover/ecrecover.zkasm
@@ -30,6 +30,13 @@ INCLUDE "constEc.zkasm"
 ; 6 - not exists sqrt of y
 ; 100 - fail sqrt, but has solution (!!!)
 
+; MAP: MAlicious Prover
+;
+; RESOURCES:
+;   PATH without root:      1014 arith + 10 binaries + 4527 steps
+;   PATH with root:         528 arith + 523 binaries + 6294 steps - 1 keccak
+;   PATH fail checks:       2 arith + 8 binaries + 45 steps
+
 ecrecover_precompiled:
         %FNEC_MINUS_ONE :MSTORE(ecrecover_s_upperlimit),JMP(ecrecover_store_args)
 
@@ -45,9 +52,9 @@ ecrecover_store_args:
         C           :MSTORE(ecrecover_s)
         D           :MSTORE(ecrecover_v)
 
-        ; check counters
 
-        %MAX_CNT_BINARY - CNT_BINARY - 1600   :JMPN(outOfCountersBinary)
+
+        %MAX_CNT_BINARY - CNT_BINARY - 550   :JMPN(outOfCountersBinary)
         %MAX_CNT_ARITH - CNT_ARITH - 1100     :JMPN(outOfCountersArith)
         %MAX_CNT_STEPS - STEP - 6400     :JMPN(outOfCountersStep)
 
@@ -73,9 +80,11 @@ ecrecover_store_args:
         $           :EQ,JMPC(ecrecover_s_is_zero)
 
         ; compute r inverse
+        ; [steps: 23, bin: 4]
         $ => A      :MLOAD(ecrecover_r),CALL(invFnEc)
         B           :MSTORE(ecrecover_r_inv)
 
+        ; [steps: 37, bin: 6, arith: 2]
         0x1Bn => B
         $ => A      :MLOAD(ecrecover_v)
         $ => E      :EQ,JMPNC(ecrecover_v_not_eq_1b)
@@ -85,6 +94,7 @@ ecrecover_store_args:
 
 ecrecover_v_not_eq_1b:
         0x1Cn => B
+        ; [steps: 42, bin: 8, arith: 2]
         $ => E      :EQ,JMPNC(ecrecover_v_not_eq_1b1c)
 
         ; ecrecover_v_eq_1c:
@@ -95,81 +105,100 @@ ecrecover_v_ok:
         ; y^2 = x^3 + 7
         ;
         ; A*B*A + 7 = calculate y from x
+        ;
+        ; [steps: 44, bin: 8, arith: 2]
         $ => A,B    :MLOAD(ecrecover_r),CALL(mulFpEc)
 
         C => A
         $ => B      :MLOAD(ecrecover_r),CALL(mulFpEc)
 
         7 => A      :CALL(addFpEc)
 
-
+        ; load on A parity expected
+        ; [steps: 69, bin: 8, arith: 8]
+        $ => A      :MLOAD(ecrecover_v_parity)
         C           :MSTORE(ecrecover_y2),CALL(sqrtFpEc)
 
-        ;; If has root y ** (p-1)/2 = 1, if -1 => no root, not valid signature
+        ; If has root B = 1 else B = 0
+        ; If B = 1 => C is alias-free (see sqrtFpEc)
 
-        %FPEC_NON_SQRT => A
-        C => B
-        $ => E      :EQ,JMPNC(ecrecover_has_sqrt)
+        ; [steps: 85, bin: 9, arith: 10]
+        B           :JMPNZ(ecrecover_has_sqrt)
 
         ; hasn't sqrt, now verify
 
         $ => C      :MLOAD(ecrecover_y2),CALL(checkSqrtFpEc)
         ; check must return on A register 1, because the root has no solution
+
+        ; [steps: 4524, bin: 10, arith: 1014]
         1           :ASSERT,JMP(ecrecover_not_exists_sqrt_of_y)
 
 ecrecover_has_sqrt:
         ; (v == 1b) ecrecover_y_parity = 0x00
         ; (v == 1c) ecrecover_y_parity = 0x01
 
-        ; C,B: y = sqrt(y^2)
-        ; check B isn't an alias (B must be in [0, FPEC-1])
-
-        %FPEC_MINUS_ONE => A
-        0           :LT         ; assert to validate that B (y) isn't n alias.
-
-        ; C,B: y = sqrtFpEc(y^2)
+        ; C: y = sqrt(y^2)  [it's alias free, verified in previous lines]
 
         0x01n => A
+        C => B
+
+        ; A = parity(y)
         $ => A      :AND
-        $ => B      :MLOAD(ecrecover_v_parity)
 
-        ; ecrevover_y xor ecrecover_y_parity => 0 same parity, 1 different parity
-        ; ecrecover_y2  v parity
-        ; parity (A)       (B)      A+B-1
-        ;      0            0        -1     same parity
-        ;      0            1         0     different parity
-        ;      1            0         0     different parity
-        ;      1            1         1     same parity
+        ; how solution y = 0 not exists because -7 not has a cubic root,
+        ; always parity of A must be equal to v_parity
 
-        A + B - 1   :JMPNZ(ecrecover_v_y2_same_parity)
+        ; ASSERT (A == ecrecover_v_parity), if it fails => MAP
+        A           :MLOAD(ecrecover_v_parity)
 
-        ; calculate neg(ecrecover_y) C = (A:FPEC) - (B:ecrecovery_y)
+        C           :MSTORE(ecrecover_y)
 
-        %FPEC => A
-        C => B
-        $ => C      :SUB
+        ; calculate C as (hash * inv_r) % FNEC
+        $ => A      :MLOAD(ecrecover_hash)
+        ; [steps: 92, bin: 10, arith: 10]
+        $ => B      :MLOAD(ecrecover_r_inv),CALL(mulFnEc)
 
-ecrecover_v_y2_same_parity:
+        ; calculate k1 as (FNEC - hash * inv_r) % FNEC
+        ; C = (hash * inv_r) % FNEC no alias free (MAP)
+        C => A
+        0 => B
+        ; C is zero, special case
+        $   :EQ,JMPNC(k1_c_is_not_zero)
 
-        C           :MSTORE(ecrecover_y)
+        ; [steps: 100, bin: 9, arith: 12]
 
-        ;   C = (hash * inv_r) % n
+k1_c_is_zero:
+        ; k1 = 0 is alias-free
+        0   :MSTORE(mulPointEc_k1), JMP(k1_calculated)
 
-        $ => A      :MLOAD(ecrecover_hash)
-        $ => B      :MLOAD(ecrecover_r_inv),CALL(mulFnEc)
 
-        ; C = n - (hash * inv_r) % n
+k1_c_is_not_zero:
+        ; A,C = (hash * inv_r) % FNEC
+        ; check A is alias-free, if not MAP ==> proof fails
+        %FNEC => B
+        1   :LT         ; ASSERT A < FNEC
+
+        ; FNEC - A = FNEC - (hash * inv_r) % FNEC
+        A => B
+        %FNEC => A
+        ; B != 0 ==> multPointEc_k1 = FNEC - B
+        ; k1 is alias-free
+        $   :SUB, MSTORE(mulPointEc_k1)
 
-        ${const.FNEC - C}  => A :MSTORE(mulPointEc_k1)
-        1 => B
-        0 => D
-        %FNEC       :ARITH
+k1_calculated:
 
         $ => A      :MLOAD(ecrecover_s)
+
+        ; [steps: 105, bin: 9, arith: 13]
         $ => B      :MLOAD(ecrecover_r_inv),CALL(mulFnEc)
 
-        ;   C = (s * inv_r) % n
-        C           :MSTORE(mulPointEc_k2)
+        ;   C = (s * inv_r) % FNEC => k2
+        ; [steps: 113, bin: 9, arith: 15]
+        C => A      :MSTORE(mulPointEc_k2)
+        %FNEC => B
+
+        ; ASSERT(k2 is alias free)
+        1           :LT
 
         %ECGX       :MSTORE(mulPointEc_p1_x)
         %ECGY       :MSTORE(mulPointEc_p1_y)
@@ -181,24 +210,23 @@ ecrecover_v_y2_same_parity:
         ; y isn't an alias because was checked before
         ; (r,y) is a point of curve because it satisfacts the curve equation
         $ => A      :MLOAD(ecrecover_y)
+        ; [steps: 120, bin: 10, arith: 15]
         A           :MSTORE(mulPointEc_p2_y),CALL(mulPointEc)
 
+        ; check if result of mulPointEc is point at infinity
+        HASHPOS     :JMPZ(ecrecover_p3_point_at_infinity)
 
+        ; [steps: 6280, bin: 522, arith: 527]
         ; generate keccak of public key to obtain ethereum address
         $ => E         :MLOAD(lastHashKIdUsed)
         E + 1 => E     :MSTORE(lastHashKIdUsed)
         0 => HASHPOS
         32 => D
 
-        %FPEC => B
+        ; p3_x, p3_y are alias free because arithmetic guarantees it
         $ => A         :MLOAD(mulPointEc_p3_x)
-        1              :LT                  ; alias assert, mulPointEc_p3_x must be in [0, FPEC - 1]
-
         A              :HASHK(E)
-
         $ => A         :MLOAD(mulPointEc_p3_y)
-        1              :LT                  ; alias assert, mulPointEc_p3_y must be in [0, FPEC - 1]
-
         A              :HASHK(E)
 
         64             :HASHKLEN(E)
@@ -207,6 +235,7 @@ ecrecover_v_y2_same_parity:
         ; for address take only last 20 bytes
         0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFn => B
         $ => A         :AND
+        ; AtEnd [steps: 6294, bin: 523, keccak: 1, arith: 528]
         0 => B         :JMP(ecrecover_end)
 
 ; ERRORS
@@ -223,11 +252,16 @@ ecrecover_s_is_too_big:
         4 => B      :JMP(ecrecover_error)
 
 ecrecover_v_not_eq_1b1c:
+        ; AtEnd [steps: 45, bin: 8, arith: 2]
         5 => B      :JMP(ecrecover_error)
 
 ecrecover_not_exists_sqrt_of_y:
+        ; AtEnd [steps: 4527, bin: 10, arith: 1014]
         6 => B      :JMP(ecrecover_error)
 
+ecrecover_p3_point_at_infinity:
+        7 => B      :JMP(ecrecover_error)
+
 ecrecover_error:
         0 => A
 

diff --git a/main/ecrecover/invFnEc.zkasm b/main/ecrecover/invFnEc.zkasm
@@ -1,8 +1,15 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; invFnEc B = inv(A)
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A no alias-free
+;; POST: B no alias-free (on MAP)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   non-normalized: 2 ariths + 2 binaries + 12 steps
+;   normalized: 2 ariths + 1 binaries + 11 steps
+;   TOTAL (worst case): 2 ariths + 2 binaries + 12 steps
 
 VAR GLOBAL invFnEc_tmp
 

diff --git a/main/ecrecover/invFpEc.zkasm b/main/ecrecover/invFpEc.zkasm
@@ -1,8 +1,15 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; invFpEc B = inv(A)
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A no alias-free
+;; POST: B no alias-free (on MAP)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   non-normalized: 2 ariths + 2 binaries + 12 steps
+;   normalized: 2 ariths + 1 binaries + 11 steps
+;   TOTAL (worst case): 2 ariths + 2 binaries + 12 steps
 
 VAR GLOBAL invFpEc_tmp
 

diff --git a/main/ecrecover/mulFnEc.zkasm b/main/ecrecover/mulFnEc.zkasm
@@ -1,8 +1,13 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; mulFnEc (C = A * B)
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A,B no alias-free
+;; POST: C no alias-free (on MAP)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   2 arith + 7 steps
 
 mulFnEc:
         0 => C

diff --git a/main/ecrecover/mulFpEc.zkasm b/main/ecrecover/mulFpEc.zkasm
@@ -1,8 +1,13 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; mulFpEc (C = A * B)
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A,B no alias-free
+;; POST: C no alias-free (on MAP)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   2 arith + 7 steps
 
 mulFpEc:
         0 => C