Merge pull request #42 from 0xPolygonHermez/fix/ecrecover-point-at-in…

…finity fix/ecrecover point at infinity
0xPolygonHermez · Nov 20, 2023 · 994aa21 · 994aa21
2 parents 70fece7 + e78c976
commit 994aa21
Show file tree

Hide file tree

Showing 12 changed files with 134 additions and 36 deletions.
diff --git a/main/ecrecover/addFpEc.zkasm b/main/ecrecover/addFpEc.zkasm
@@ -1,8 +1,10 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; addFpEc C = (A + C) % FpEc
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A,C no alias-free
+;; POST: C no alias-free (on MAP)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ; RESOURCES:
 ;   2 ariths + 7 steps

diff --git a/main/ecrecover/checkSqrtFpEc.zkasm b/main/ecrecover/checkSqrtFpEc.zkasm
@@ -8,7 +8,10 @@
 ;;         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

diff --git a/main/ecrecover/ecrecover.zkasm b/main/ecrecover/ecrecover.zkasm
@@ -120,6 +120,7 @@ ecrecover_v_ok:
         C           :MSTORE(ecrecover_y2),CALL(sqrtFpEc)
 
         ; If has root B = 1 else B = 0
+        ; If B = 1 => C is alias-free (see sqrtFpEc)
 
         ; [steps: 85, bin: 9, arith: 10]
         B           :JMPNZ(ecrecover_has_sqrt)
@@ -152,28 +153,46 @@ ecrecover_has_sqrt:
 
         C           :MSTORE(ecrecover_y)
 
-        ;   C = (hash * inv_r) % n
-
+        ; calculate C as (hash * inv_r) % FNEC
         $ => A      :MLOAD(ecrecover_hash)
         ; [steps: 92, bin: 10, arith: 10]
         $ => B      :MLOAD(ecrecover_r_inv),CALL(mulFnEc)
 
-        ; C = n - (hash * inv_r) % n
+        ; 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)
 
         ; [steps: 100, bin: 9, arith: 12]
-        ${const.FNEC - C}  => A :MSTORE(mulPointEc_k1)
-        1 => B
-        0 => D
-        %FNEC       :ARITH
 
-        ; A, multipointEc_k1 is alias free, because A + C = FNEC exactly (D == 0)
+k1_c_is_zero:
+        ; k1 = 0 is alias-free
+        0   :MSTORE(mulPointEc_k1), JMP(k1_calculated)
+
+
+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)
+
+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 = (s * inv_r) % FNEC => k2
         ; [steps: 113, bin: 9, arith: 15]
         C => A      :MSTORE(mulPointEc_k2)
         %FNEC => B
@@ -194,6 +213,8 @@ ecrecover_has_sqrt:
         ; [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
@@ -238,6 +259,9 @@ 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,10 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; 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

diff --git a/main/ecrecover/invFpEc.zkasm b/main/ecrecover/invFpEc.zkasm
@@ -1,8 +1,10 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; 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

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

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

diff --git a/main/ecrecover/mulPointEc.zkasm b/main/ecrecover/mulPointEc.zkasm
@@ -1,22 +1,35 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; mulPointEc
+;; mulPointEc (p1_x,p1_y,p2_x,p2_y,k1,k2) = (p3_x, p3_y, HASPOS)
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: p1_x, p1_y, p2_x, p2_y, k1, k2 are alias-free
+;; POST: p3_x, p3_y is alias-free  HASHPOS = [0,1]
+;;
+;; HASHPOS = 0 ==> p3 is the point at infinity
+;; HASHPOS = 1 ==> p3 is not the point at infinity
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 VAR GLOBAL mulPointEc_p1_x
 VAR GLOBAL mulPointEc_p1_y
 VAR GLOBAL mulPointEc_p2_x
 VAR GLOBAL mulPointEc_p2_y
 VAR GLOBAL mulPointEc_k1
 VAR GLOBAL mulPointEc_k2
+
+; p3 output point
 VAR GLOBAL mulPointEc_p3_x
 VAR GLOBAL mulPointEc_p3_y
-VAR GLOBAL mulPointEc_RR
+
+; point p12 = p1 + p2
 VAR GLOBAL mulPointEc_p12_x
 VAR GLOBAL mulPointEc_p12_y
-VAR GLOBAL mulPointEc_HASHPOS
+
+; mulPointEc_p12_empty = 1 ==> p12 is the point at infinity
+; mulPointEc_p12_empty = 0 ==> p12 isn't the point at infinity
 VAR GLOBAL mulPointEc_p12_empty
+
+; backups
+VAR GLOBAL mulPointEc_RR
 VAR GLOBAL mulPointEc_RCX
 
 ; PRECONDITION: p1,p2 are points of curve
@@ -38,12 +51,14 @@ VAR GLOBAL mulPointEc_RCX
 
 mulPointEc:
         RR      :MSTORE(mulPointEc_RR)
-        HASHPOS :MSTORE(mulPointEc_HASHPOS)
         RCX     :MSTORE(mulPointEc_RCX)
 
         256 => RCX
 
         ; HASHPOS used to mulPointEc_p3_no_infinity
+        ; HASHPOS = 0 ==> p3 is the point at infinity
+        ; HASHPOS = 1 ==> p3 is not the point at infinity
+
         0n => HASHPOS :MSTORE(mulPointEc_p3_x)
 
         0n      :MSTORE(mulPointEc_p3_y)
@@ -69,6 +84,7 @@ mulPointEc:
         ; because when add p12 do nothing.
 
         ; y + (-y) = y + P - y = P
+        ; y != 0, because cubic root of -7 not exists (y^2 = x^3 + 7)
 
         B => A        ; A = p1_y
         D => C        ; C = p2_y
@@ -283,6 +299,7 @@ mulPointEc_same_point_to_add:
         D       :MLOAD(mulPointEc_p3_y)
         C => A
         D => B
+
         ; (A,B) * 2 = (E, op)
         ${xDblPointEc(A,B)} => E  :MSTORE(mulPointEc_p3_x)
         ${yDblPointEc(A,B)} => B  :ARITH_ECADD_SAME, MSTORE(mulPointEc_p3_y), JMP(mulPointEc_after_add)
@@ -291,5 +308,4 @@ mulPointEc_end_loop:
         ; [steps.block: 3]
 
         $ => RR         :MLOAD(mulPointEc_RR)
-        $ => RCX        :MLOAD(mulPointEc_RCX)
-        $ => HASHPOS    :MLOAD(mulPointEc_HASHPOS), RETURN
+        $ => RCX        :MLOAD(mulPointEc_RCX), RETURN
diff --git a/main/ecrecover/sqFpEc.zkasm b/main/ecrecover/sqFpEc.zkasm
@@ -1,8 +1,11 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; sqFpEc (C = C * C)
 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: C no alias-free
+;; POST: C no alias-free (on MAP)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
 
 ; RESOURCES:
 ;   2 arith + 8 steps

diff --git a/main/ecrecover/sqrtFpEc.zkasm b/main/ecrecover/sqrtFpEc.zkasm
@@ -1,8 +1,11 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; sqrtFpEc (C = sqrt(C,A))
+;;
+;; PRE: A = [0,1], C no alias-free
+;; POST: C is alias-free
 ;; NOTE: if C has sqrt B = 1 if not B = 0
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ; RESOURCES:
 ;   with root: 2 arith + 1 binary + 14 steps
@@ -32,6 +35,8 @@ sqrtFpEc:
         ; A and C has same value
 
         %FPEC => B
+
+        ; A
         $ => B                                           :LT,JMPNC(sqrtFpEc_End)
 
         ; A,C < FPEC (alias free)

diff --git a/package.json b/package.json
@@ -1,6 +1,6 @@
 {
   "name": "@0xpolygonhermez/zkevm-rom",
-  "version": "2.0.0",
+  "version": "3.0.0",
   "description": "zkROM source code",
   "main": "index.js",
   "scripts": {
@@ -42,8 +42,8 @@
   },
   "devDependencies": {
     "@0xpolygonhermez/zkevm-proverjs": "github:0xPolygonHermez/zkevm-proverjs-internal#fix/ecrecover-alias-diffequals-sqrt",
-    "@0xpolygonhermez/zkevm-testvectors": "github:0xPolygonHermez/zkevm-testvectors#feature/update-fork",
-    "@0xpolygonhermez/zkevm-commonjs": "github:0xPolygonHermez/zkevm-commonjs#v2.0.0-fork.5",
+    "@0xpolygonhermez/zkevm-testvectors": "github:0xPolygonHermez/zkevm-testvectors#v3.0.0-rc.1-fork.6",
+    "@0xpolygonhermez/zkevm-commonjs": "github:0xPolygonHermez/zkevm-commonjs#v3.0.0-fork.6",
     "mocha": "^9.1.3",
     "chai": "^4.3.6",
     "chalk": "^3.0.0",

diff --git a/test/ecrecover.zkasm b/test/ecrecover.zkasm
@@ -12,7 +12,8 @@ start:
 
         CTX     :MSTORE(originalCTX)
         -1      :MSTORE(lastHashKIdUsed)
-                :JMP(repeat_ecrecover_test)
+                ; :JMP(repeat_ecrecover_test)
+                :JMP(edge_cases)
 
 INCLUDE "../main/ecrecover/ecrecover.zkasm"
 
@@ -437,6 +438,8 @@ repeat_ecrecover_test:
         :CALL(ecrecover_tx)
         0x0000000000000000000000000000000000000000n :ASSERT
 
+edge_cases:
+
         ; #40 EGX
 
         0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eeben => A
@@ -479,6 +482,40 @@ repeat_ecrecover_test:
         :CALL(ecrecover_tx)
         0x1772bf1cfa310fdca361ee65825a74013eeaa17en :ASSERT
 
+        ; p3 = point at infinity
+
+        0x0000000000000000000000000000000000000000000000000000000000000001n => A ; hash
+        0xc6047f9441ed7d6d3045406e95c07cd85c778e4b8cef3ca7abac09b95c709ee5n => B ; r
+        0x7fffffffffffffffffffffffffffffff5d576e7357a4501ddfe92f46681b20a1n => C ; s
+        0x1bn => D
+        :CALL(ecrecover_precompiled)
+        0x0000000000000000000000000000000000000000n :ASSERT
+        B => A
+        7 :ASSERT
+
+CONSTL %P2_C0_EGX = %ECGX & 0xFFFF
+
+        ; # p2 & 0xFFFF == EGX & 0xFFFF
+
+        0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eeben => A
+        %P2_C0_EGX => B
+        0x2bcf13b5e4f34a04a77344d5943e0228ba2e787583036325450c889d597a16c4n => C
+        0x1bn => D
+        :CALL(ecrecover_tx)
+        0x9446d37b3aaedc97b2a8a9437998ba5787a2d5cbn :ASSERT
+
+
+
+        ; # p2 & 0x001FFFF....FFFF == EGX & 0x001FFFF....FFFF
+
+CONSTL %P2_CH_EGX = %ECGX & 0x001FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFn
+
+        0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eeben => A
+        %P2_CH_EGX => B
+        0x2bcf13b5e4f34a04a77344d5943e0228ba2e787583036325450c889d597a16c4n => C
+        0x1bn => D
+        :CALL(ecrecover_tx)
+        0x4c90563674ab8de6f7731475a01a2bd09fd7b4b1n :ASSERT
         $${dump(STEP)}
 
         :JMP(end)