Skip to content

Commit

Permalink
Updating counters
Browse files Browse the repository at this point in the history
  • Loading branch information
@hecmas
hecmas committed Apr 2, 2024
1 parent a72c10a commit 031f254
Show file tree
Hide file tree
Showing 3 changed files with 53 additions and 67 deletions.
4 changes: 2 additions & 2 deletions main/ecrecover/FPSECP256K1/sqrtFpSecp256k1.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; RESOURCES:
; with sqrt: 1 arith + 1 binary + 9 steps
; with sqrt: 1 arith + 1 binary + 7 steps
; without sqrt: 1 binary + 4 steps
; TOTAL (worst case): 1 arith + 1 binary + 9 steps
; TOTAL (worst case): 1 arith + 1 binary + 7 steps

sqrtFpSecp256k1:
; start by free-inputing the square root of the input C
Expand Down
70 changes: 29 additions & 41 deletions main/ecrecover/dblScalarMulSecp256k1.zkasm
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; PRE: p1 = (p1_x, p1_y), p2 = (p2_x, p2_y) are in E(Fp)\{𝒪} and p1_x,p1_y,p2_x,p2_y,k1,k2 are alias-free
;; Moreover, k1 and k2 cannot be zero at the same time
;; POST: The resulting coordinates p3_x,p3_y are alias-free and variable p3_is_zero ∈ {0,1}
;;
;; dblScalarMulSecp256k1:
Expand Down Expand Up @@ -42,15 +43,15 @@ VAR GLOBAL dblScalarMulSecp256k1_RR
VAR GLOBAL dblScalarMulSecp256k1_RCX

; RESOURCES (k1,k2):
; 1 arith + 19 steps // setup, calculation p12
; + number_of_bits_1(k1|k2) * arith // additions
; + max_bin_len(k1,k2) * arith // doubles
; + max_bin_len(k1,k2)/32 * 29 steps // additions + doubles (steps, worst case)
; + (256 - max_bin_len(k1,k2)/32) * 24 steps // additions + doubles (steps, worst case)
; + 8 steps + 2 bin // last part
; 1 arith + 19 steps // setup, calculation p12
; + number_of_bits_1(k1|k2) * arith // additions
; + max_bin_len(k1,k2) * arith // doubles
; + max_bin_len(k1,k2)/32 * 27 steps // additions + doubles (steps, worst case)
; + (256 - max_bin_len(k1,k2)/32) * 22 steps // additions + doubles (steps, worst case)
; + 6 steps // last part
;
;
; RESOURCES (worst case): 513 arith + 2 binaries + 6239 steps // 20 + 256/32 * 29 + (256 - 256/32) * 24 + 8 = 6212
; RESOURCES (worst case): 513 arith + 5697 steps // 19 + 256/32 * 27 + (256 - 256/32) * 22 + 6 = 5697

dblScalarMulSecp256k1:
RR :MSTORE(dblScalarMulSecp256k1_RR)
Expand Down Expand Up @@ -93,8 +94,11 @@ dblScalarMulSecp256k1:
; y must be distinct from 0, because the cubic root of -7 doesn't exist (y² = x³ + 7)

; check p1_y + p2_y = SECP256K1_P
D => A ; A = p2_y, B = p1_y
%SECP256K1_P :ADD
B => A ; A = p1_y
1 => B
D => C ; C = p2_y
0 => D
%SECP256K1_P :ARITH
; We have p2 == -p1

; p12 = p1 - p1 = 𝒪, therefore is the point at infinity
Expand Down Expand Up @@ -139,13 +143,13 @@ dblScalarMulSecp256k1DiffInitialPoints:
; Goes forward in different branches of code depending on the values of the
; most significant bits of k1 and k2.

; [steps.byloop (worst case & nosave): 8 + 16 = 24]
; [steps.byloop (worst case & save): 13 + 16 = 29]
; [steps.byloop (worst case & nosave): 7 + 15 = 22]
; [steps.byloop (worst case & save): 12 + 15 = 27]

; [steps.byloop ((bit.k1 || bit.k2) == 1) & nosave: 6 + 16 = 22]
; [steps.byloop ((bit.k1 && bit.k2) == 1) & nosave: 8 + 16 = 24]
; [steps.byloop ((bit.k1 || bit.k2) == 1) & save: 11 + 16 = 27]
; [steps.byloop ((bit.k1 && bit.k2) == 1) & save: 13 + 16 = 29]
; [steps.byloop ((bit.k1 || bit.k2) == 1) & nosave: 5 + 15 = 20]
; [steps.byloop ((bit.k1 && bit.k2) == 1) & nosave: 7 + 15 = 22]
; [steps.byloop ((bit.k1 || bit.k2) == 1) & save: 10 + 15 = 25]
; [steps.byloop ((bit.k1 && bit.k2) == 1) & save: 12 + 15 = 27]

; First iteration
; ------------------------------
Expand Down Expand Up @@ -176,26 +180,16 @@ dblScalarMulSecp256k1_k11:

; high_bit(k1) == 0 high_bit(k2) == 1
dblScalarMulSecp256k1_k10_k21_add_prepare:
; [steps.before.nosave: 4]
; [steps.before.save: 9]
; [steps.before (w.c.): 9]
$ => C :MLOAD(dblScalarMulSecp256k1_p2_x)
$ => D :MLOAD(dblScalarMulSecp256k1_p2_y), JMP(dblScalarMulSecp256k1_add)

; high_bit(k1) == 1 high_bit(k2) == 0
dblScalarMulSecp256k1_k11_k20_add_prepare:
; [steps.before.nosave: 3]
; [steps.before.save: 9]
; [steps.before (w.c.): 9]
$ => C :MLOAD(dblScalarMulSecp256k1_p1_x)
$ => D :MLOAD(dblScalarMulSecp256k1_p1_y), JMP(dblScalarMulSecp256k1_add)

; high_bit(k1) == 1 high_bit(k2) == 1
dblScalarMulSecp256k1_k11_k21_add_prepare:
; [steps.before.nosave: 5]
; [steps.before.save: 10]
; [steps.before (w.c.): 10]

; if (dblScalarMulSecp256k1_p12_zero) k11_k21 is the same as k10_k20
; because adding the point at infinity to a point is the point itself
$ :MLOAD(dblScalarMulSecp256k1_p12_zero), JMPNZ(dblScalarMulSecp256k1_double)
Expand All @@ -205,13 +199,13 @@ dblScalarMulSecp256k1_k11_k21_add_prepare:

; at this point, C,D contain the point to be added
dblScalarMulSecp256k1_add:
; [steps.p3empty.nolast: 4 + steps.double = 10]
; [steps.p3empty.last: 4 + steps.double = 5]
; [steps.xeq.yeq: 9 + steps.double = 15]
; [steps.xeq.yneq: 10 + steps.double = 16]
; [steps.xneq.nolast: 7 + steps.double = 13]
; [steps.xneq.last: 7 + steps.double = 8]
; [steps.block: 16]
; [steps.p3empty.nolast: 5 + steps.double = 7]
; [steps.p3empty.last: 5 + steps.double = 6]
; [steps.xeq.yeq: 8 + steps.double = 14, arith: 1 + steps.double = 2]
; [steps.xeq.yneq: 9 + steps.double = 15, arith: 1 + steps.double = 1]
; [steps.xneq.nolast: 6 + steps.double = 12, arith: 1 + steps.double = 2]
; [steps.xneq.last: 6 + steps.double = 7, arith: 1 + steps.double = 1]
; [steps.block: 15, arith.block: 2]

; if p3 is the point at infinity do not add, just assign, since 𝒪 + P = P
$ :MLOAD(dblScalarMulSecp256k1_p3_zero), JMPNZ(dblScalarMulSecp256k1_p3_assignment)
Expand Down Expand Up @@ -242,8 +236,8 @@ dblScalarMulSecp256k1_p3_assignment:
dblScalarMulSecp256k1_double:
; [steps.last: 1]
; [steps.nolast.p3empty: 2]
; [steps.nolast.p3: 6]
; [steps.block: 6]
; [steps.nolast: 6, arith: 1]
; [steps.block: 6, arith: 1]

; E,A = p3_x B = p3_y
RR - 1 => RR :JMPN(dblScalarMulSecp256k1_end_loop)
Expand All @@ -261,10 +255,6 @@ dblScalarMulSecp256k1_double_compute:
${yDblPointEc(A,B)} :ARITH_ECADD_SAME, MSTORE(dblScalarMulSecp256k1_p3_y), JMP(dblScalarMulSecp256k1_loop)

dblScalarMulSecp256k1_x_equals_before_add:
; [steps.same.point: 7]
; [steps.opposite.point: 8]
; [steps.block: 8]

; [MAP] if C != mem.dblScalarMulSecp256k1_p3_x ==> fails, MLOAD fails because read something different
; for memory. It verifies C and dblScalarMulSecp256k1_p3_x are same value, as an ASSERT.
C :MLOAD(dblScalarMulSecp256k1_p3_x)
Expand All @@ -285,6 +275,7 @@ dblScalarMulSecp256k1_x_equals_before_add:
; instead of binary to use similar resources on different paths.

; if p2_y == -p3_y, and them are alias free ==> p2_y + p3_y === SECP256K1_P
; Note: The Secp256k1 curve does not have points with y = 0

1 => B
D => A
Expand All @@ -300,7 +291,6 @@ dblScalarMulSecp256k1_x_equals_before_add:
1n :MSTORE(dblScalarMulSecp256k1_p3_zero), JMP(dblScalarMulSecp256k1_double)

dblScalarMulSecp256k1_same_point_to_add:
; [steps.block: 5]
; must check really are equals, use MLOAD as ASSERT
; ASSERT(D == dblScalarMulSecp256k1_p3_y)

Expand All @@ -313,8 +303,6 @@ dblScalarMulSecp256k1_same_point_to_add:
${yDblPointEc(A,B)} :ARITH_ECADD_SAME, MSTORE(dblScalarMulSecp256k1_p3_y), JMP(dblScalarMulSecp256k1_double)

dblScalarMulSecp256k1_end_loop:
; [steps.block: 8]

; Check that the accumulated scalars coincide with the original ones
$ => A :MLOAD(dblScalarMulSecp256k1_k1)
A :MLOAD(dblScalarMulSecp256k1_acum_k1)
Expand Down
46 changes: 22 additions & 24 deletions main/ecrecover/ecrecover.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,11 +34,11 @@ INCLUDE "constSecp256k1.zkasm"
; MAP: MAlicious Prover

; RESOURCES:
; PATH without root: [steps: 1816, bin: 8, arith: 505]
; PATH with root: [steps: 6343, bin: 13, arith: 520, keccak: 1]
; PATH with result of dbl is infinity: [steps: 6332, bin: 12, arith: 520]
; PATH without root: [steps: 1800, bin: 8, arith: 505]
; PATH with root: [steps: 5775, bin: 11, arith: 520, keccak: 1]
; PATH with result of dbl is infinity: [steps: 5763, bin: 10, arith: 520]
; --------------------------------------------------------------------------------------
; worst case: [steps: 6343, bin: 13, arith: 520, keccak: 1]
; worst case: [steps: 5775, bin: 11, arith: 520, keccak: 1]

ecrecover_precompiled:
%SECP256K1_N_MINUS_ONE :MSTORE(ecrecover_s_upperlimit), JMP(ecrecover_store_args)
Expand Down Expand Up @@ -76,24 +76,24 @@ ecrecover_store_args:
$ :EQ, JMPC(ecrecover_s_is_zero)
$ => A :MLOAD(ecrecover_s_upperlimit)
$ :LT, JMPC(ecrecover_s_is_too_big)
; [steps: 23, bin: 4]
; [steps: 21, bin: 4]

0x1Bn => B ; 27
$ => A :MLOAD(ecrecover_v)
$ => E :EQ, JMPNC(ecrecover_v_not_eq_1b)

; ecrecover_v_eq_1b:
0n :MSTORE(ecrecover_v_parity), JMP(ecrecover_v_ok)
; 1] [steps: 27, bin: 5]
; 1] [steps: 25, bin: 5]

ecrecover_v_not_eq_1b:
0x1Cn => B ; 28
; ecrecover_v_eq_1c:
$ => E :EQ, MSTORE(ecrecover_v_parity), JMPNC(ecrecover_v_not_eq_1b1c)
; 2] [steps: 29, bin: 6]
; 2] [steps: 27, bin: 6]

ecrecover_v_ok:
; before (w.c.) -> [steps: 29, bin: 6]
; before (w.c.) -> [steps: 27, bin: 6]
;
; y² = x³ + 7
;
Expand All @@ -119,25 +119,25 @@ ecrecover_v_ok:
; A = 7, B = 1, C = r³ + 7

; load on A parity expected
; [steps: 42, bin: 6, arith: 3]
$ => A :MLOAD(ecrecover_v_parity), CALL(sqrtFpSecp256k1) ; with sqrt: [steps: 9, bin: 1, arith: 1]
; [steps: 35, bin: 6, arith: 3]
$ => A :MLOAD(ecrecover_v_parity), CALL(sqrtFpSecp256k1) ; with sqrt: [steps: 7, bin: 1, arith: 1]
;without sqrt: [steps: 4, bin: 1, arith: 0]

; If it has root C = 0, else B = 1
; If C = 0 => B is alias-free (see sqrtFpSecp256k1)

C :JMPZ(ecrecover_has_sqrt)
; [steps: 49, bin: 7, arith: 3]
; [steps: 39, bin: 7, arith: 3]

; hasn't sqrt, now verify

$ => C :MLOAD(ecrecover_y2), CALL(assertNQRFpSecp256k1) ; [steps: 1761, bin: 1, arith: 502]

:JMP(ecrecover_not_exists_sqrt_of_y)
; till the end -> [steps: 1816, bin: 8, arith: 505]
; till the end -> [steps: 1800, bin: 8, arith: 505]

ecrecover_has_sqrt:
; before -> [steps: 53, bin: 7, arith: 4]
; before -> [steps: 42, bin: 7, arith: 4]
; (v == 1b) ecrecover_y_parity = 0x00
; (v == 1c) ecrecover_y_parity = 0x01

Expand Down Expand Up @@ -166,15 +166,15 @@ ecrecover_has_sqrt:
0 => A
; B is zero, special case
$ :EQ, JMPNC(k1_c_is_not_zero)
; [steps: 72, bin: 9, arith: 6]
; [steps: 54, bin: 9, arith: 6]

k1_c_is_zero:
; k1 = 0 is alias-free
0 :MSTORE(dblScalarMulSecp256k1_k1), JMP(k1_calculated)


k1_c_is_not_zero:
; before (w.c.) -> [steps: 72, bin: 9, arith: 6]
; before (w.c.) -> [steps: 54, bin: 9, arith: 6]

; B = (hash * inv_r) % SECP256K1_N

Expand All @@ -183,6 +183,7 @@ k1_c_is_not_zero:
; B != 0 ==> dblScalarMulSecp256k1_k1 = SECP256K1_N - B
; k1 is alias-free
$ :SUB, MSTORE(dblScalarMulSecp256k1_k1)
; [steps: 56, bin: 10, arith: 6]

k1_calculated:
; Compute s * inv_r
Expand All @@ -193,7 +194,7 @@ k1_calculated:
${(A*B) % D} :ARITH_MOD, MSTORE(dblScalarMulSecp256k1_k2)

; C = (s * inv_r) % SECP256K1_N => k2
; [steps: 81, bin: 10, arith: 7]
; [steps: 59, bin: 10, arith: 7]

%SECP256K1_GX :MSTORE(dblScalarMulSecp256k1_p1_x)
%SECP256K1_GY :MSTORE(dblScalarMulSecp256k1_p1_y)
Expand All @@ -205,31 +206,28 @@ k1_calculated:
; y isn't an alias because was checked before
; (r,y) is a point of curve because it satisfies the curve equation
$ => A :MLOAD(ecrecover_y)
A :MSTORE(dblScalarMulSecp256k1_p2_y), CALL(dblScalarMulSecp256k1) ; 513 arith + 2 binaries + 6239 steps
A :MSTORE(dblScalarMulSecp256k1_p2_y), CALL(dblScalarMulSecp256k1) ; 513 arith + 5697 steps

; check if result of dblScalarMulSecp256k1 is point at infinity
$ :MLOAD(dblScalarMulSecp256k1_p3_zero), JMPNZ(ecrecover_p3_point_at_infinity)
; [steps: 6328, bin: 12, arith: 520]
; [steps: 5763, bin: 10, arith: 520]

; generate keccak of public key to obtain ethereum address
$ => E :MLOAD(nextHashKId)
E + 1 :MSTORE(nextHashKId)
0 => HASHPOS
32 => D

; p3_x, p3_y are alias free because arithmetic guarantees it
$ => A :MLOAD(dblScalarMulSecp256k1_p3_x)
A :HASHK(E)
$ => A :MLOAD(dblScalarMulSecp256k1_p3_y)
A :HASHK(E)
${mem.dblScalarMulSecp256k1_p3_x} :MLOAD(dblScalarMulSecp256k1_p3_x), HASHK32(E)
${mem.dblScalarMulSecp256k1_p3_y} :MLOAD(dblScalarMulSecp256k1_p3_y), HASHK32(E)

64 :HASHKLEN(E)
$ => A :HASHKDIGEST(E)

; for address take only last 20 bytes
0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFn => B
$ => A :AND
; till the end -> [steps: 6343, bin: 13, arith: 520]
; till the end -> [steps: 5775, bin: 11, arith: 520]
0 => B :JMP(ecrecover_end)

; ERRORS
Expand Down

0 comments on commit 031f254

Please sign in to comment.