Skip to content

Commit

Permalink
Adding counters to p256verify
Browse files Browse the repository at this point in the history
  • Loading branch information
@hecmas
hecmas committed Oct 8, 2024
1 parent adb5bac commit 77acf25
Show file tree
Hide file tree
Showing 8 changed files with 133 additions and 66 deletions.
5 changes: 5 additions & 0 deletions main/p256verify/addFpSecp256r1.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,11 @@
;; POST: The result is in Fp
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; RESOURCES:
; -----------------------------
; [steps: 10, bin: 1, arith: 2]
; -----------------------------

addFpSecp256r1:
; 1] Compute and check the sum over Z
; A·[1] + C = [D]·2²⁵⁶ + [E]
Expand Down
100 changes: 53 additions & 47 deletions main/p256verify/dblScalarMulSecp256r1.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,16 +41,17 @@ VAR GLOBAL dblScalarMulSecp256r1_acum_k2
VAR GLOBAL dblScalarMulSecp256r1_RR
VAR GLOBAL dblScalarMulSecp256r1_RCX

; RESOURCES (k1,k2):
; 1 arith + 19 steps // setup, calculation p12
; RESOURCES:
; 1 bin + 1 arith + 21 steps // setup, calculation p12 (w.c., p1 = -p2)
; + 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)
; + max_bin_len(k1,k2)/32 * 29 steps // additions + doubles (worst case on save)
; + (256 - max_bin_len(k1,k2)/32) * 24 steps // additions + doubles (worst case no save)
; + 6 steps // last part
;
;
; RESOURCES (worst case): 513 arith + 5697 steps // 19 + 256/32 * 27 + (256 - 256/32) * 22 + 6 = 5697
; RESOURCES (worst case): 6459 steps + 1 bin + 513 arith // steps: 21 + 256/32 * 29 + (256 - 256/32) * 25 + 6 = 6459
; // arith: 1 + 256 + 256 = 513

dblScalarMulSecp256r1:
RR :MSTORE(dblScalarMulSecp256r1_RR)
Expand All @@ -77,14 +78,14 @@ dblScalarMulSecp256r1:

; check whether p1_x == p2_x
${A == C} :JMPZ(dblScalarMulSecp256r1DiffInitialPoints)
; [steps: 11]
; [steps: 13, bin: 1, arith: 0]

; verify path p1_x == p2_x
C :ASSERT

; check whether p1_y == p2_y
${B == D} :JMPNZ(dblScalarMulSecp256r1SameInitialPoints)
; [steps: 13]
; [steps: 15, bin: 1, arith: 0]

; verify path p1_y != p2_y <==> p1_y = -p2_y <==> p1_y + p2_y = 0
; Note: In this path we could use a binary, but we use an arith
Expand All @@ -102,10 +103,10 @@ dblScalarMulSecp256r1:

; p12 = 𝒪, therefore is the point at infinity
1 :MSTORE(dblScalarMulSecp256r1_p12_zero), JMP(dblScalarMulSecp256r1_loop_fi)
; [steps: 19, arith: 1]
; [steps: 21, bin: 1, arith: 1]

dblScalarMulSecp256r1SameInitialPoints:
; [steps.before: 13]
; before: [steps: 15, bin: 1, arith: 0]
; verify path p1_y (B) == p2_y (D)
B :MLOAD(dblScalarMulSecp256r1_p2_y)

Expand All @@ -116,38 +117,42 @@ dblScalarMulSecp256r1SameInitialPoints:
; A == p1_x
; B == p1_y
; 2·(A, B) = (E, op)
${xDblPointEc_secp256r1(A,B)} => E :MSTORE(dblScalarMulSecp256r1_p12_x)
${xDblPointEc_secp256r1(A,B)} => E :MSTORE(dblScalarMulSecp256r1_p12_x)
${yDblPointEc_secp256r1(A,B)} :ARITH_SECP256R1_ECADD_SAME, MSTORE(dblScalarMulSecp256r1_p12_y), JMP(dblScalarMulSecp256r1_loop_fi)
; [steps: 17, arith: 1]
; [steps: 19, bin: 1, arith: 1]

dblScalarMulSecp256r1DiffInitialPoints:
; [steps.before: 11]
; before: [steps: 13, bin: 1, arith: 0]
; verify path p1_x != p2_x
; p2_x != p1_x ==> p2 != p1
; [MAP] if p1 == p2 => arith fails because p1 = p2

; p12 = p1 + p2, therefore isn't the point at infinity
0 :MSTORE(dblScalarMulSecp256r1_p12_zero)
0 :MSTORE(dblScalarMulSecp256r1_p12_zero)

; Compute and check the addition p1 + p2
; (A, B) + (C, D) = (E, op)
${xAddPointEc_secp256r1(A,B,C,D)} => E :MSTORE(dblScalarMulSecp256r1_p12_x)
${yAddPointEc_secp256r1(A,B,C,D)} :ARITH_SECP256R1_ECADD_DIFFERENT, MSTORE(dblScalarMulSecp256r1_p12_y)
; [steps: 14, arith: 1]
; [steps: 16, bin: 1, arith: 1]


; [steps.before (worst case): 19, arith.before: 1]
; before (w.c.): [steps: 21, bin: 1, arith: 1]

; 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): 7 + 15 = 22]
; [steps.byloop (worst case & save): 12 + 15 = 27]

; [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]
; [steps bit.k1 = 0 && bit.k2 = 0 && nosave: 3 + steps.doubleNoRR = 8, arith: arith.double = 1]
; [steps bit.k1 = 0 && bit.k2 = 0 && save: 3 + steps.save + steps.double = 13, arith: arith.double = 1]
; [steps bit.k1 = 1 && bit.k2 = 0 && nosave: 6 + steps.add = 21, arith: arith.add = 2]
; [steps bit.k1 = 1 && bit.k2 = 0 && save: 6 + steps.save + steps.add = 26, arith: arith.add = 2]
; [steps bit.k1 = 0 && bit.k2 = 1 && nosave: 6 + steps.add = 21, arith: arith.add = 2]
; [steps bit.k1 = 0 && bit.k2 = 1 && save: 6 + steps.save + steps.add = 26, arith: arith.add = 2]
; [steps bit.k1 = 1 && bit.k2 = 1 && nosave: 9 + steps.add = 24, arith: arith.add = 2] <- worst case
; [steps bit.k1 = 1 && bit.k2 = 1 && save: 9 + steps.save + steps.add = 29, arith: arith.add = 2] <- worst case
; ----------------------------------------------------------
; worst case & nosave: [steps.byloop: 24, arith.byloop: 2]
; worst case & save: [steps.byloop: 29, arith.byloop: 2]

; First iteration
; ------------------------------
Expand Down Expand Up @@ -200,12 +205,13 @@ dblScalarMulSecp256r1_k11_k21_add_prepare:

; at this point, C,D contain the point to be added
dblScalarMulSecp256r1_add:
; [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.p3empty.nolast: 5 + steps.double = 7, arith: arith.double = 1]
; [steps.p3empty.last: 5]
; [steps.xeq.yeq: 9 + steps.double = 15, arith: 1 + arith.double = 2] <- worst case
; [steps.xeq.yneq: 10 + steps.double = 11, arith: 1]
; [steps.xneq.nolast: 6 + steps.double = 12, arith: 1 + arith.double = 2]
; [steps.xneq.last: 6 + steps.double = 7, arith: 1]
; --------------------------------------------
; [steps.block: 15, arith.block: 2]

; if p3 is the point at infinity do not add, just assign, since 𝒪 + P = P
Expand All @@ -228,7 +234,7 @@ dblScalarMulSecp256r1_add:
${yAddPointEc_secp256r1(A,B,C,D)} :ARITH_SECP256R1_ECADD_DIFFERENT, MSTORE(dblScalarMulSecp256r1_p3_y), JMP(dblScalarMulSecp256r1_double)

dblScalarMulSecp256r1_p3_assignment:
; p3 = (C,D)
; p3 = (C,D) is either p1, p2 or p12
0 :MSTORE(dblScalarMulSecp256r1_p3_zero)
C => A :MSTORE(dblScalarMulSecp256r1_p3_x)
D => B :MSTORE(dblScalarMulSecp256r1_p3_y)
Expand Down Expand Up @@ -318,37 +324,37 @@ dblScalarMulSecp256r1_save_k10_k20:
; $ => C :MLOAD(dblScalarMulSecp256r1_acum_k1)
ROTL_C + RCX :MSTORE(dblScalarMulSecp256r1_acum_k1)

$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)

0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_double)
0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_double)

dblScalarMulSecp256r1_save_k11_k20:
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k1)
ROTL_C + RCX :MSTORE(dblScalarMulSecp256r1_acum_k1)
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k1)
ROTL_C + RCX :MSTORE(dblScalarMulSecp256r1_acum_k1)

$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)

0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_k11_k20_add_prepare)
0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_k11_k20_add_prepare)

dblScalarMulSecp256r1_save_k11_k21:
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k1)
ROTL_C + RCX :MSTORE(dblScalarMulSecp256r1_acum_k1)
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k1)
ROTL_C + RCX :MSTORE(dblScalarMulSecp256r1_acum_k1)

$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)

0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_k11_k21_add_prepare)
0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_k11_k21_add_prepare)

dblScalarMulSecp256r1_save_k10_k21:
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k1)
ROTL_C + RCX :MSTORE(dblScalarMulSecp256r1_acum_k1)
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k1)
ROTL_C + RCX :MSTORE(dblScalarMulSecp256r1_acum_k1)

$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)
$ => C :MLOAD(dblScalarMulSecp256r1_acum_k2)
ROTL_C + HASHPOS :MSTORE(dblScalarMulSecp256r1_acum_k2)

0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_k10_k21_add_prepare)
0n => RCX,HASHPOS :JMP(dblScalarMulSecp256r1_k10_k21_add_prepare)

; Sage code
; ----------------------------------------
Expand Down
11 changes: 8 additions & 3 deletions main/p256verify/invFnSecp256r1.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,22 +8,27 @@
;; POST: The result is in Fn*
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; RESOURCES:
; -----------------------------
; [steps: 11, bin: 1, arith: 2]
; -----------------------------

VAR GLOBAL invFnSecp256r1_tmp

invFnSecp256r1:
; 1] Compute and check the inverse over Z
; A·A⁻¹ + [0] = [D]·2²⁵⁶ + [E]
${var _invFnSecp256r1_A = inverseFnEc_secp256r1(A)} => B :MSTORE(invFnSecp256r1_tmp)
0 => C
${var _invFnSecp256r1_A = inverseFnEc_secp256r1(A)} => B :MSTORE(invFnSecp256r1_tmp);
$${var _invFnSecp256r1_AAinv = A * _invFnSecp256r1_A}
${_invFnSecp256r1_AAinv >> 256} => D
${_invFnSecp256r1_AAinv} => E :ARITH

; 2] Check it over Fn, that is, it must be satisfied that:
; [SECP256R1_N]·[(A·A⁻¹) / SECP256R1_N] + [1] = D·2²⁵⁶ + E
%SECP256R1_N => A
${_invFnSecp256r1_AAinv / const.SECP256R1_N} => B ; quotient (256 bits)
1 => C ; remainder
${_invFnSecp256r1_AAinv / const.SECP256R1_N} => B ; quotient (256 bits)
1 => C ; remainder
E :ARITH

; 3] Check that the result is lower than SECP256R1_N
Expand Down
5 changes: 5 additions & 0 deletions main/p256verify/mulFnSecp256r1.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,11 @@
;; POST: The result is in Fn
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; RESOURCES:
; -----------------------------
; [steps: 10, bin: 1, arith: 2]
; -----------------------------

mulFnSecp256r1:
; 1] Compute and check the sum over Z
; A·B + [0] = [D]·2²⁵⁶ + [E]
Expand Down
5 changes: 5 additions & 0 deletions main/p256verify/mulFpSecp256r1.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,11 @@
;; POST: The result is in Fp
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; RESOURCES:
; -----------------------------
; [steps: 10, bin: 1, arith: 2]
; -----------------------------

mulFpSecp256r1:
; 1] Compute and check the sum over Z
; A·B + [0] = [D]·2²⁵⁶ + [E]
Expand Down
44 changes: 29 additions & 15 deletions main/p256verify/p256verify.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,16 @@ INCLUDE "constants.zkasm"
; 9 - result is the point at infinity

; RESOURCES:
; TODO
; · r is zero: [steps: 13, bin: 1, arith: 0]
; · r is too big: [steps: 15, bin: 2, arith: 0]
; · s is zero: [steps: 17, bin: 3, arith: 0]
; · s is too big: [steps: 19, bin: 4, arith: 0]
; · x is too big: [steps: 22, bin: 5, arith: 0]
; · y is too big: [steps: 24, bin: 6, arith: 0]
; · PK is zero: [steps: 29, bin: 8, arith: 0]
; · PK not in E: [steps: 104, bin: 15, arith: 12]
; · result is zero: [steps: 7708, bin: 19, arith: 531]
; · no error: [steps: 7718, bin: 22, arith: 531]

p256verify:
; save RR to call return at end of routine
Expand All @@ -59,9 +68,9 @@ p256verify:
D :MSTORE(p256verify_x)
E :MSTORE(p256verify_y)

; %MAX_CNT_BINARY - CNT_BINARY - 550 :JMPN(outOfCountersBinary)
; %MAX_CNT_ARITH - CNT_ARITH - 1100 :JMPN(outOfCountersArith)
; %MAX_CNT_STEPS - STEP - 6400 :JMPN(outOfCountersStep)
%MAX_CNT_BINARY - CNT_BINARY - 25 :JMPN(outOfCountersBinary)
%MAX_CNT_ARITH - CNT_ARITH - 550 :JMPN(outOfCountersArith)
%MAX_CNT_STEPS - STEP - 8000 :JMPN(outOfCountersStep)

p256verify_correctness_checks:
; 1] Check that r in [1,N-1]
Expand Down Expand Up @@ -92,52 +101,55 @@ p256verify_correctness_checks:
$ :EQ, JMPNC(p256verify_pk_not_point_at_infinity)
$ => A :MLOAD(p256verify_y)
$ :EQ, JMPC(p256verify_pk_point_at_infinity)
; [steps: 29, bin: 8, arith: 0]

p256verify_pk_not_point_at_infinity:
; 6] Check whether PK = (x,y) is a point on the curve
; PK in E(Fp) iff y² == x³ + a·x + b (mod p)
; 1.1] Compute LHS and RHS
$ => A :MLOAD(p256verify_x), CALL(squareFpSecp256r1)
$ => A :MLOAD(p256verify_x), CALL(squareFpSecp256r1) ; [in: A, out: A] [steps: 11, bin: 1, arith: 2]
; A = x²

$ => B :MLOAD(p256verify_x), CALL(mulFpSecp256r1)
$ => B :MLOAD(p256verify_x), CALL(mulFpSecp256r1) ; [in: A,B, out: C] [steps: 10, bin: 1, arith: 2]
; C = x³
C :MSTORE(p256verify_x3)

%SECP256R1_A => A
$ => B :MLOAD(p256verify_x), CALL(mulFpSecp256r1)
$ => B :MLOAD(p256verify_x), CALL(mulFpSecp256r1) ; [in: A,B, out: C]
; C = a·x

%SECP256R1_B => A :CALL(addFpSecp256r1)
%SECP256R1_B => A :CALL(addFpSecp256r1) ; [in: A,C, out: C] [steps: 10, bin: 1, arith: 2]
; C = a·x + b

$ => A :MLOAD(p256verify_x3), CALL(addFpSecp256r1)
$ => A :MLOAD(p256verify_x3), CALL(addFpSecp256r1) ; [in: A,C, out: C] [steps: 10, bin: 1, arith: 2]
; C = x³ + a·x + b
C :MSTORE(p256verify_x3)

$ => A :MLOAD(p256verify_y), CALL(squareFpSecp256r1)
$ => A :MLOAD(p256verify_y), CALL(squareFpSecp256r1) ; [in: A, out: A] [steps: 11, bin: 1, arith: 2]
; A = y²

; 1.2] Check if LHS == RHS
$ => B :MLOAD(p256verify_x3)
$ :EQ, JMPNC(p256verify_pk_not_in_curve)
; [steps: 100, bin: 15, arith: 12]

p256verify_scalars:
; compute s⁻¹ (mod n)
$ => A :MLOAD(p256verify_s), CALL(invFnSecp256r1)
$ => A :MLOAD(p256verify_s), CALL(invFnSecp256r1) ; [in: A, out: A] [steps: 11, bin: 1, arith: 2]
; A = s⁻¹
A :MSTORE(p256verify_s_inv)

; compute u1 = hash·s⁻¹ (mod n)
$ => B :MLOAD(p256verify_hash), CALL(mulFnSecp256r1)
$ => B :MLOAD(p256verify_hash), CALL(mulFnSecp256r1) ; [in: A,B, out: C] [steps: 10, bin: 1, arith: 2]
; C = hash·s⁻¹
C :MSTORE(p256verify_u1)

; compute u2 = r·s⁻¹ (mod n)
$ => A :MLOAD(p256verify_r)
$ => B :MLOAD(p256verify_s_inv), CALL(mulFnSecp256r1)
$ => B :MLOAD(p256verify_s_inv), CALL(mulFnSecp256r1) ; [in: A,B, out: C] [steps: 10, bin: 1, arith: 2]
; C = r·s⁻¹
C :MSTORE(p256verify_u2)
; [steps: 138, bin: 18, arith: 18]

p256verify_ecp:
; Compute u1·G + u2·PK
Expand All @@ -151,7 +163,8 @@ p256verify_ecp:
$ => A :MLOAD(p256verify_x)
A :MSTORE(dblScalarMulSecp256r1_p2_x)
$ => A :MLOAD(p256verify_y)
A :MSTORE(dblScalarMulSecp256r1_p2_y), CALL(dblScalarMulSecp256r1)
A :MSTORE(dblScalarMulSecp256r1_p2_y), CALL(dblScalarMulSecp256r1) ; [steps: 6459, bin: 1, arith: 513]
; [steps: 7707, bin: 19, arith: 531]

p256verify_verification:
; check if result of dblScalarMulSecp256k1 is point at infinity
Expand Down Expand Up @@ -179,6 +192,7 @@ p256verify_final_check:

; program ended with no errors
0 => B :JMP(p256verify_end)
; till the end -> [steps: 7718, bin: 22, arith: 531]

; ERRORS
p256verify_r_is_zero:
Expand Down Expand Up @@ -219,5 +233,5 @@ INCLUDE "addFpSecp256r1.zkasm"
INCLUDE "invFnSecp256r1.zkasm"
INCLUDE "mulFnSecp256r1.zkasm"
INCLUDE "mulFpSecp256r1.zkasm"
INCLUDE "squareSecp256r1.zkasm"
INCLUDE "squareFpSecp256r1.zkasm"
INCLUDE "dblScalarMulSecp256r1.zkasm"
5 changes: 5 additions & 0 deletions main/p256verify/squareSecp256r1.zkasm → main/p256verify/squareFpSecp256r1.zkasm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,11 @@
;; POST: The result is in Fp
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; RESOURCES:
; -----------------------------
; [steps: 11, bin: 1, arith: 2]
; -----------------------------

squareFpSecp256r1:
; 1] Compute and check the inverse over Z
; A·A + [0] = [D]·2²⁵⁶ + [E]
Expand Down
Loading

0 comments on commit 77acf25

Please sign in to comment.