diff --git a/main/constants.zkasm b/main/constants.zkasm index 61692fd1..4b2e41ec 100644 --- 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 index 9fd42436..96986f10 100644 --- 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 index 224eeb69..6f2440c1 100644 --- 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 index e77e0b60..29294bbc 100644 --- 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,6 +105,8 @@ 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 @@ -102,74 +114,91 @@ ecrecover_v_ok: 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 index 7288bba4..245b99a7 100644 --- 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 index 57883107..581bc211 100644 --- 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 index 4e289548..74c7a792 100644 --- 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 index 11d8ed4a..8b7cba7a 100644 --- 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 diff --git a/main/ecrecover/mulPointEc.zkasm b/main/ecrecover/mulPointEc.zkasm index b7178d11..648382e5 100644 --- a/main/ecrecover/mulPointEc.zkasm +++ b/main/ecrecover/mulPointEc.zkasm @@ -1,8 +1,13 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;; 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 @@ -10,24 +15,50 @@ 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 ; PRECONDITION: p1,p2 are alias-free +; RESOURCES (k1,k2): +; 1 arith + 18 steps // setup, calculation p12 +; + 2 binaries * 256 // get bits of k1,k2 (steps evaluated inside loop) +; + number_of_bits_1(k1|k2) * arith // additions +; + (256 - left_bits_zero(k1|k2) * arith // squares +; + 24 * 256 steps // get bits k1,k2 + additions + squares (steps, regular) +; - (24 - 8) * left_bits_zero(k1|k2) * steps // get bits k1,k2 + additions + squares (steps firts bits = 0) +; - (24 - 12) * number_of_bits_1(k1|k2) * steps // get bits k1,k2 + additions + squares (k1,k2 bits = 0) +; + (3 - 5) steps // last part - last part square no done +; - 1 arith // first asignation +; +; +; RESOURCES (worst case): 512 arith + 512 binaries + 6160 steps // 18 + 256 * 24 - 2 = 6160 + 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) @@ -38,28 +69,61 @@ mulPointEc: $ => D :MLOAD(mulPointEc_p2_y) ; check p1.x == p2.x - ${A == C} :JMPZ(mulPointDiffInitalPoints) + ; [steps: 11] + ${A == C} :JMPZ(mulPointDiffInitialPoints) + + ; verify path p1.x == p2.x C :ASSERT - ; check p1.y == p2.y - D => A - $ :EQ,JMPC(mulPointSameInitalPoints) + ; check p1.y (B) == p2.y (D) + ; [steps: 13] + ${B == D} :JMPNZ(mulPointSameInitialPoints) + + ; verify path p1.y != p2.y ==> p1.y = -p2.y + ; use arith because in this path save a lot of arith, + ; 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 + 1 => B + 0 => D ; check p1_y * 1 + p2_y = 0 * 2^256 * 0 + FPEC + %FPEC :ARITH ; p2 == -p1 ; mulPointEc_p12_empty = 1: no add p12 because it was origin point p = O + p = p + ; [steps: 18] 1n :MSTORE(mulPointEc_p12_empty),JMP(mulPointEc_loop) -mulPointSameInitalPoints: + +mulPointSameInitialPoints: + ; [steps.before: 13] + ; verify path p1.y (B) == p2.y (D) + ; as an ASSERT(B == mulPointEc_p2_y) + B :MLOAD(mulPointEc_p2_y) + ; p2 == p1 0n :MSTORE(mulPointEc_p12_empty) - $ => A :MLOAD(mulPointEc_p1_x) + ; A == p1_x + ; B == p1_y + ; (A,B) * 2 = (E, op) ${xDblPointEc(A,B)} => E :MSTORE(mulPointEc_p12_x) + + ; [steps: 17] ${yDblPointEc(A,B)} :ARITH_ECADD_SAME, MSTORE(mulPointEc_p12_y),JMP(mulPointEc_loop) -mulPointDiffInitalPoints: +mulPointDiffInitialPoints: + ; [steps.before: 11] + ; verify path p1.x != p2.x ; p2.x != p1.x ==> p2 != p1 + ; [MAP] if p1 == p2 => arith fails because p1 = p2 + 0n :MSTORE(mulPointEc_p12_empty) + ; (A, B) + (C, D) = (E, op) ${xAddPointEc(A,B,C,D)} => E :MSTORE(mulPointEc_p12_x) + ; [steps: 14] ${yAddPointEc(A,B,C,D)} :ARITH_ECADD_DIFFERENT, MSTORE(mulPointEc_p12_y) @@ -82,6 +146,11 @@ mulPointDiffInitalPoints: ; ; store E to be used in next round ; +; [steps.before (worst case): 18] +; +; [steps.byloop (p3initialempty.nolast): 8] +; [steps.byloop (bit.k1|bit.k2 == 0): 12] +; [steps.byloop (worst case): 7 + 17 = 24] mulPointEc_loop: $ => A,B :MLOAD(mulPointEc_k1) @@ -123,22 +192,36 @@ mulPointEc_k10_k21: $ => C :MLOAD(mulPointEc_p2_x) $ => D :MLOAD(mulPointEc_p2_y), JMP(mulPointEc_p2_loaded) +; [steps.loadp2 (worst case): 7 (regular case 6) + ; in this point C,D have point to be add mulPointEc_p2_loaded: + ; [steps.p3empty.nolast: 10] + ; [steps.p3empty.last: 5] + ; [steps.xeq.yeq: 10 + steps.square = 16] + ; [steps.xeq.yneq: 11 + steps.square = 17] + ; [steps.xneq.nolast: 7 + steps.square = 13] + ; [steps.xneq.last: 7 + steps.square = 13] + ; [steps.block: 17] ; check if p3 has a value, isn't point at infinity (Origin point) HASHPOS :JMPZ(mulPointEc_p3_assignment) + ; check C == p3.x - C => A ; point_x - $ => B :MLOAD(mulPointEc_p3_x) - $ :EQ,JMPC(mulPointEc_x_equals_before_add) + ${ C == mem.mulPointEc_p3_x } :JMPNZ(mulPointEc_x_equals_before_add) + + ; [MAP] if C == mem.mulPointEc_p3_x ==> fails arithmetic because check + ; points are different ; p3 = (A,B) $ => A :MLOAD(mulPointEc_p3_x) $ => B :MLOAD(mulPointEc_p3_y) ; p3 = p3 + (C,D) + ; (C, D) is point to add (p1 or p2 or p12) + ; (A, B) + (C, D) = (E, op) + ${xAddPointEc(A,B,C,D)} => E :MSTORE(mulPointEc_p3_x) ${yAddPointEc(A,B,C,D)} => B :ARITH_ECADD_DIFFERENT, MSTORE(mulPointEc_p3_y) @@ -154,6 +237,10 @@ mulPointEc_p3_assignment: D => B :MSTORE(mulPointEc_p3_y) mulPointEc_square: + ; [steps.last: 1] + ; [steps.nolast.p3empty: 2] + ; [steps.nolast.p3: 6] + ; [steps.block: 6] ; E,A = p3_x B = p3_y RCX - 1 => RCX :JMPZ(mulPointEc_end_loop) @@ -164,50 +251,61 @@ mulPointEc_square: $ => A :MLOAD(mulPointEc_p3_x) $ => B :MLOAD(mulPointEc_p3_y) + ; (A, B) * 2 = (E, op) ${xDblPointEc(A,B)} => E :MSTORE(mulPointEc_p3_x) ${yDblPointEc(A,B)} :ARITH_ECADD_SAME, MSTORE(mulPointEc_p3_y), JMP(mulPointEc_loop) mulPointEc_x_equals_before_add: + ; [MAP] if C != mem.mulPointEc_p3_x ==> fails, MLOAD fails because read something different + ; for memory. It verifies C and mulPointEc_p3_x are same value, as an ASSERT. + C :MLOAD(mulPointEc_p3_x) + ; points to add: point1 (p3) + point2 (C,D) - ; A,C: point2.x - ; B: point1.x (p3.x) + ; C: point2.x ; D: point2.y ; p3_x == C, check if points are same or a point was oposite point - D => A ; D contains y of point to add (depends of bits k1,k2) - $ => B :MLOAD(mulPointEc_p3_y) ; point1.y - $ :EQ,JMPC(mulPointEc_same_point_to_add) + ${ D == mem.mulPointEc_p3_y } :JMPNZ(mulPointEc_same_point_to_add) - ; C: point2.x - ; B: point1.y (p3.y) - ; A,D: point2.y + ; In this path must be verified that D != mulPointEc_p3_y to + ; how p2_y and p3_y are different for same x, it implies that + ; p2_y == -p3_y. In this case next operation with p3 doesn't + ; spend arithmetics, for this reason is used an arithmetic + ; instead of binary to use similar resources on different paths. - ; x1 = x2 and y1 != y2 - ; ASSUME y1 = -y2 - ; same instruction put HASHPOS and mulPointEc_p3_x to 0. + ; if p2_y == -p3_y, and them are alias free ==> p2_y + p3_y === FPEC - ; check [A (FPEC_MINUS_ONE) >= B point1.y (mulPointEc_p3_y)] => LT == 0 - %FPEC_MINUS_ONE => A - 0 :LT + 1 => B + D => A + 0 => D + $ => C :MLOAD(mulPointEc_p3_y) - ; check [A (FPEC_MINUS_ONE) >= B point2.y (D)] => LT == 0 - D => B - 0 :LT + ; p2_y * 1 + p3_y = 2^256 * 0 + FPEC + %FPEC :ARITH + + ; NOTE: all points are free of alias because arithmetic guaranties it ; HASHPOS flag = 0, mulPointEc_p3 was empty, need addition must be an assignation 0n => HASHPOS :MSTORE(mulPointEc_p3_x) 0n :MSTORE(mulPointEc_p3_y), JMP(mulPointEc_square) mulPointEc_same_point_to_add: + ; [steps.block: 5] + ; must check really are equals, use MLOAD as ASSERT + ; ASSERT(D == mulPointEc_p3_y) + + 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) mulPointEc_end_loop: + ; [steps.block: 3] $ => RR :MLOAD(mulPointEc_RR) - $ => HASHPOS :MLOAD(mulPointEc_HASHPOS), RETURN + $ => RCX :MLOAD(mulPointEc_RCX), RETURN diff --git a/main/ecrecover/sqFpEc.zkasm b/main/ecrecover/sqFpEc.zkasm index 21299558..9c542c8b 100644 --- a/main/ecrecover/sqFpEc.zkasm +++ b/main/ecrecover/sqFpEc.zkasm @@ -1,8 +1,14 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; sqFpEc (C = C * C) ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PRE: C no alias-free +;; POST: C no alias-free (on MAP) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +; RESOURCES: +; 2 arith + 8 steps sqFpEc: C => A,B diff --git a/main/ecrecover/sqrtFpEc.zkasm b/main/ecrecover/sqrtFpEc.zkasm index ca03cc0b..c739251d 100644 --- a/main/ecrecover/sqrtFpEc.zkasm +++ b/main/ecrecover/sqrtFpEc.zkasm @@ -1,26 +1,50 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; -;; sqrtFpEc (C = sqrt(C)) +;; 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 +; without root: 1 binary + 5 steps +; TOTAL (worst case): 2 arith + 1 binary + 14 steps VAR GLOBAL sqrtFpC_tmp VAR GLOBAL sqrtFpC_res sqrtFpEc: + ; PATH: hasn't sqrt => 1 binary + ; PATH: has sqrt => 1 binary + 2 arith + ; TOTAL resources: 1 binary + 2 arith + C :MSTORE(sqrtFpC_tmp) ; [A] * [A] + 0 = [D] * 2 ** 256 + [E] ; set C because if jmp to sqrtFpEc C must have return value (FPEC_NON_SQRT) - ${var _sqrtFpEc_sqrt = sqrtFpEc(C) } => A,C :MSTORE(sqrtFpC_res) - %FPEC_NON_SQRT => B - $ :EQ,JMPC(sqrtFpEc_End) + ${var _sqrtFpEc_sqrt = sqrtFpEcParity(C,A) } => A,C :MSTORE(sqrtFpC_res) + + ; In this point we check if C is LT than FPEC because if not: + ; a) A = FPEC_NON_SQRT, check hasn't sqrt. + ; b) A is an alias, it's a MAP, we check hasn't sqrt, but has => no proof generated + + ; A and C has same value + %FPEC => B + + ; A + $ => B :LT,JMPNC(sqrtFpEc_End) + + ; A,C < FPEC (alias free) A => B 0 => C + ; A = B => A * A + 0 =? + $${var _sqrtFpEc_sq = _sqrtFpEc_sqrt * _sqrtFpEc_sqrt } ${_sqrtFpEc_sq >> 256} => D @@ -36,7 +60,11 @@ sqrtFpEc: %FPEC => A E :ARITH + ; sqrtFpC_res hasn't alias because in this path sqrtFpC_res < FPEC + + 1 => B $ => C :MLOAD(sqrtFpC_res),RETURN sqrtFpEc_End: + ; B is 0, because C >= FPEC :RETURN \ No newline at end of file diff --git a/package.json b/package.json index e3f9aff6..c93499be 100644 --- 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": { @@ -22,7 +22,7 @@ "eslint": "npx eslint tools/**.js && npx eslint counters/counters-executor.js", "eslint:fix": "npx eslint tools/**.js --fix && npx eslint counters/counters-executor.js --fix", "test:gen": "node tools/gen-parallel-tests.js", - "test:start": "npx mocha --jobs $NUM_CPUS --timeout 0 --max-old-space-size=8192 --parallel tools/parallel-tests/*.test.js" + "test:start": "npx mocha --jobs $NUM_CPUS --timeout 0 --max-old-space-size=8192 --parallel \"tools/parallel-tests/*.test.js\"" }, "keywords": [ "zkrom", @@ -41,9 +41,9 @@ "yargs": "^17.5.1" }, "devDependencies": { - "@0xpolygonhermez/zkevm-proverjs": "github:0xPolygonHermez/zkevm-proverjs#5f0d122fdfb5e3e5b17f45976e08fd26c9f248ba", - "@0xpolygonhermez/zkevm-testvectors": "github:0xPolygonHermez/zkevm-testvectors#v2.0.0-fork.5", - "@0xpolygonhermez/zkevm-commonjs": "github:0xPolygonHermez/zkevm-commonjs#v2.0.0-fork.5", + "@0xpolygonhermez/zkevm-proverjs": "github:0xPolygonHermez/zkevm-proverjs#5ff55a11b376ee76d489b3b4305c5d5af783a76d", + "@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 index 40e98085..1999e51d 100644 --- a/test/ecrecover.zkasm +++ b/test/ecrecover.zkasm @@ -12,9 +12,12 @@ start: CTX :MSTORE(originalCTX) -1 :MSTORE(lastHashKIdUsed) + ; :JMP(repeat_ecrecover_test) + :JMP(edge_cases) -repeat_ecrecover_test: +INCLUDE "../main/ecrecover/ecrecover.zkasm" +repeat_ecrecover_test: ; A:ecrecover_hash B:ecrecover_r C:ecrecover_s D:ecrecover_v 0xd9eba16ed0ecae432b71fe008c98cc872bb4cc214d3220a36f365326cf807d68n => A @@ -435,9 +438,88 @@ repeat_ecrecover_test: :CALL(ecrecover_tx) 0x0000000000000000000000000000000000000000n :ASSERT +edge_cases: + + ; #40 EGX + + 0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eeben => A + %ECGX => B + 0x2bcf13b5e4f34a04a77344d5943e0228ba2e787583036325450c889d597a16c4n => C + 0x1bn => D + :CALL(ecrecover_tx) + 0x3c8b5f2426549658f425fad7e061c500626b39a3n :ASSERT + + ; #41 -EGX + + 0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eeben => A + %ECGX => B + 0x2bcf13b5e4f34a04a77344d5943e0228ba2e787583036325450c889d597a16c4n => C + 0x1cn => D + :CALL(ecrecover_tx) + 0x687526ad233c19b0a9b2eb8c96d1a45603f3919en :ASSERT + + 0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eec0n => A ; hash + 0xc6047f9441ed7d6d3045406e95c07cd85c778e4b8cef3ca7abac09b95c709ee5n => B ; r + 0x2bcf13b5e4f34a04a77344d5943e0228ba2e787583036325450c889d597a16c8n => C ; s + 0x1b => D ; v + :CALL(ecrecover_tx) + 0x89fea198bd4a0efb63f36b5a04c993cca3a1891dn :ASSERT + + + 0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eec0n => A ; hash + 0xc6047f9441ed7d6d3045406e95c07cd85c778e4b8cef3ca7abac09b95c709ee5n => B ; r + 0x2bcf13b5e4f34a04a77344d5943e0228ba2e787583036325450c889d597a16c8n => C ; s + 0x1c => D ; v + :CALL(ecrecover_tx) + 0xc613182e8da092201765f852e3d6fbec4d281432n :ASSERT + + ; p: (0xc6047f9441ed7d6d3045406e95c07cd85c778e4b8cef3ca7abac09b95c709ee5,0x1ae168fea63dc339a3c58419466ceaeef7f632653266d0e1236431a950cfe52a) + + 0x3cc4cb050478c49877188e4fbd022f35ccb41cee02d9d4417194cbf7ebc1eec1n => A ; hash + 0xc6047f9441ed7d6d3045406e95c07cd85c778e4b8cef3ca7abac09b95c709ee5n => B ; r + 0x2bcf13b5e4f34a04a77344d5943e0228ba2e787583036325450c889d597a16c8n => C ; s + 0x1b => D ; v + :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) -INCLUDE "../main/ecrecover/ecrecover.zkasm" outOfCountersBinary: outOfCountersArith: outOfCountersKeccak: