Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Modexp Durian #408

Merged
merged 13 commits into from
Oct 10, 2024
Merged

Modexp Durian #408

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
8021659
Modexp new version
hecmas Oct 3, 2024
768e2b1
Updating tests
hecmas Oct 3, 2024
675e3ae
update constant forkId = 13
laisolizq Oct 2, 2024
b7904d4
last fixes pre-modexp
laisolizq Mar 22, 2024
c592be1
update selector modexp & fix comment
laisolizq Oct 2, 2024
436105a
update test-vectors forkid 13
laisolizq Oct 3, 2024
8164ea7
Fixing package
hecmas Oct 4, 2024
8aabaf7
Merge branch 'develop-durian' into feature/modexp-durian
hecmas Oct 4, 2024
ee45fd2
update pre-modexp includes
laisolizq Oct 4, 2024
127a08d
Moving the return correctly
hecmas Oct 7, 2024
ce1d2b1
Library counters done
hecmas Oct 9, 2024
08edf32
First version of modexp counters done
hecmas Oct 9, 2024
e2d7b11
Modexp counters done
hecmas Oct 9, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
149 changes: 83 additions & 66 deletions main/modexp/array_lib/array_add_AGTB.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; PRE: len(inA) >= len(inB)
;;
;; PRE: len(inA) >= len(inB)
;; POST: out is trimmed
;;
;; array_add_AGTB:
;; in:
;; · C ∈ [1, 32], the len of inA
;; · C ∈ [1, 64], the len of inA
;; · D ∈ [1, 32], the len of inB
;; · inA ∈ [0, 2²⁵⁶ - 1]^C, the first input array
;; · inB ∈ [0, 2²⁵⁶ - 1]^D, the second input array
Expand All @@ -13,34 +13,30 @@
;; · out = inA + inB, with len(out) <= C + 1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; function array_add_AGTB(a: bigint[], b: bigint[], base: bigint): bigint[] {
; const alen = a.length;
; const blen = b.length;
; let result = new Array<bigint>(alen);
; let sum = 0n;
; let carry = 0n;
; for (let i = 0; i < blen; i++) {
; sum = a[i] + b[i] + carry;
; carry = sum >= base ? 1n : 0n;
; out[i] = sum - carry * base;
; }
; for (let i = blen; i < alen; i++) {
; sum = a[i] + carry;
; carry = sum == base ? 1n : 0n; // the past carry is at most 1n
; out[i] = sum - carry * base;
; }

; if (carry === 1n) {
; result.push(carry);
; }
; return result;
; }
;; WARNING: This function is tailored for checking that a = q·b + r in the array_div_long function.
;; In can be used for other purposes except for the worst case, i.e. when len(inA) == %ARRAY_MAX_LEN_DOUBLED.
;; Specifically, there is an implicit assumption that the output len of this function cannot be
;; greater than %ARRAY_MAX_LEN_DOUBLED, and do not allow to generate the proof in such case.

; NOTE: It's unoptimized for the case where len(inB) = 1. Use array_add_short instead.

VAR GLOBAL array_add_AGTB_inA[%ARRAY_MAX_LEN]
; code
; --------------------------
; first_iteration <-- Compute a[0] + b[0]
; while(inB_index_check) { <-- While 0 < i < len(b)
; loop2inB <-- Compute a[i] + b[i] + carry
; }
; while (inA_index_check) { <-- While 0 < i < len(a)
; loop2inA <-- Compute a[i] + carry
; }
; 1] check_carry <-- If there is a carry, append it to the result
; 2] trim <-- Otherwise, trim the result
; end
; --------------------------

VAR GLOBAL array_add_AGTB_inA[%ARRAY_MAX_LEN_DOUBLED]
VAR GLOBAL array_add_AGTB_inB[%ARRAY_MAX_LEN]
VAR GLOBAL array_add_AGTB_out[%ARRAY_MAX_LEN_PLUS_ONE]
VAR GLOBAL array_add_AGTB_out[%ARRAY_MAX_LEN_DOUBLED] ; This cannot be bigger because we use it for division checking
VAR GLOBAL array_add_AGTB_len_inA
VAR GLOBAL array_add_AGTB_len_inB
VAR GLOBAL array_add_AGTB_len_out
Expand All @@ -49,73 +45,94 @@ VAR GLOBAL array_add_AGTB_carry

VAR GLOBAL array_add_AGTB_RR

/*
* RESOURCES:
* -----------------------------
* (worst case) [steps: 9, bin: 1] + (lenB-1)*[steps: 10, bin: 2] + [steps: 3] + (lenA - lenB)*[steps: 6, bin: 1] + [steps: 6]
* total: [steps: 8 + 6*lenA + 4*lenB, bin: lenA + lenB - 2]
* -----------------------------
*/

array_add_AGTB:
%MAX_CNT_BINARY - CNT_BINARY - 2*D - C+ D :JMPN(outOfCountersBinary)
%MAX_CNT_STEPS - STEP - 5 - 14*D - 3 - 9*C+9*D - 8 :JMPN(outOfCountersStep)
%MAX_CNT_BINARY - CNT_BINARY + 2 - %ARRAY_MAX_LEN_DOUBLED - %ARRAY_MAX_LEN :JMPN(outOfCountersBinary)
%MAX_CNT_STEPS - STEP - 8 - 6*%ARRAY_MAX_LEN_DOUBLED - 4*%ARRAY_MAX_LEN :JMPN(outOfCountersStep)

RR :MSTORE(array_add_AGTB_RR)

C :MSTORE(array_add_AGTB_len_inA)
D :MSTORE(array_add_AGTB_len_inB)

0 => E ; index in loops
0 :MSTORE(array_add_AGTB_carry)
array_add_AGTB_first_iteration:
; a[0] + b[0], where a[0],b[0] ∈ [0,base-1]: This number cannot be GT base + (base - 2), two chunks
$ => A :MLOAD(array_add_AGTB_inA)
$ => B :MLOAD(array_add_AGTB_inB)
$ :ADD, MSTORE(array_add_AGTB_out), JMPNC(__array_add_AGTB_continue_1)
;-----------------
1 => D :MSTORE(array_add_AGTB_carry), JMP(__array_add_AGTB_continue_2)
__array_add_AGTB_continue_1:
0 => D :MSTORE(array_add_AGTB_carry)
__array_add_AGTB_continue_2:
;-----------------

array_add_AGTB_loopZero2inB:
; The result will be stored as D·base + C
1 => E

0 => D ; reset the carry chunk
array_add_AGTB_inB_index_check:
$ - E :F_MLOAD(array_add_AGTB_len_inB), JMPZ(array_add_AGTB_inA_index_check)

array_add_AGTB_loop2inB:
; a[i] + b[i], where a[i],b[i] ∈ [0,base-1]: This number cannot be GT base + (base - 2), two chunks
$ => A :MLOAD(array_add_AGTB_inA + E)
$ => B :MLOAD(array_add_AGTB_inB + E)
$ => C :ADD, JMPNC(__array_add_AGTB_continue_1)
1 => D
__array_add_AGTB_continue_1:
$ => B :ADD, JMPNC(__array_add_AGTB_continue_3)
;-----------------
1 => D :JMP(__array_add_AGTB_continue_4)
__array_add_AGTB_continue_3:
0 => D
__array_add_AGTB_continue_4:
;-----------------

; sum = (a[i] + b[i]) + carry: This number cannot be GT base + (base - 1), two chunks
; sum = (a[i] + b[i]) + carry, where carry ∈ [0,1]: This number cannot be GT base + (base - 1), two chunks
$ => A :MLOAD(array_add_AGTB_carry)
C => B
$ => C :ADD, JMPNC(__array_add_AGTB_continue_2)
$ :ADD, MSTORE(array_add_AGTB_out + E), JMPNC(__array_add_AGTB_continue_5)
;-----------------
1 => D
__array_add_AGTB_continue_2:
__array_add_AGTB_continue_5:
;-----------------

C :MSTORE(array_add_AGTB_out + E)
D :MSTORE(array_add_AGTB_carry)
; NOTE: It cannot happen that a[i] + b[i] produces carry and (a[i] + b[i]) + carry as well at the same time

E + 1 => E,A
$ => B :MLOAD(array_add_AGTB_len_inB)
B - A :JMPZ(array_add_AGTB_loop_index_check, array_add_AGTB_loopZero2inB)
D :MSTORE(array_add_AGTB_carry)

array_add_AGTB_loop_index_check:
$ => B :MLOAD(array_add_AGTB_len_inA)
B - A :JMPZ(array_add_AGTB_check_carry)
E + 1 => E :JMP(array_add_AGTB_inB_index_check)

array_add_AGTB_loopInB2InA:
0 => D ; reset the carry chunk
array_add_AGTB_inA_index_check:
$ - E :F_MLOAD(array_add_AGTB_len_inA), JMPZ(array_add_AGTB_check_carry)

array_add_AGTB_loop2inA:
; sum = a[i] + carry: This number cannot be GT base, two chunks
$ => A :MLOAD(array_add_AGTB_inA + E)
$ => B :MLOAD(array_add_AGTB_carry)
$ => C :ADD, JMPNC(__array_add_AGTB_continue_3)
1 => D
__array_add_AGTB_continue_3:
D => B
$ :ADD, MSTORE(array_add_AGTB_out + E), JMPNC(__array_add_AGTB_continue_6)
;-----------------
1 => D :JMP(__array_add_AGTB_continue_7)
__array_add_AGTB_continue_6:
0 => D
__array_add_AGTB_continue_7:
;-----------------

C :MSTORE(array_add_AGTB_out + E)
D :MSTORE(array_add_AGTB_carry)

E + 1 => E,A
$ => B :MLOAD(array_add_AGTB_len_inA)
B - A :JMPZ(array_add_AGTB_check_carry, array_add_AGTB_loopInB2InA)
E + 1 => E :JMP(array_add_AGTB_inA_index_check)

array_add_AGTB_check_carry:
D => A
A :JMPZ(__array_add_AGTB_continue_4)
D :JMPZ(array_add_AGTB_trim)

; Carry path
E - %ARRAY_MAX_LEN_DOUBLED :JMPZ(failAssert)

; In this case, the carry = 1 and we should append it to the result
1 :MSTORE(array_add_AGTB_out + E)
E + 1 :MSTORE(array_add_AGTB_len_out)
:JMP(array_add_AGTB_end)
__array_add_AGTB_continue_4:
E + 1 :MSTORE(array_add_AGTB_len_out), JMP(array_add_AGTB_end)

array_add_AGTB_trim:
E :MSTORE(array_add_AGTB_len_out)

array_add_AGTB_end:
Expand Down
105 changes: 61 additions & 44 deletions main/modexp/array_lib/array_add_short.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; POST: out is trimmed
;;
;; array_add_short:
;; in:
Expand All @@ -10,75 +11,91 @@
;; · out = inA + inB, with len(out) <= C + 1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; function array_add_short(a: bigint[], b: bigint, base: bigint): bigint[] {
; const alen = a.length;
; let result = new Array<bigint>(alen);
; let sum = 0n;
; let carry = b;
; for (let i = 0; i < alen; i++) {
; sum = a[i] + carry;
; carry = sum >= base ? 1n : 0n;
; out[i] = sum - carry * base;
; }

; if (carry === 1n) {
; result.push(carry);
; }
; return result;
;; WARNING: This function is tailored for checking that a = q·b + r in the array_div_short function.
;; In can be used for other purposes except for the worst case, i.e. when len(inA) == %ARRAY_MAX_LEN.
;; Specifically, there is an implicit assumption that the output len of this function cannot be
;; greater than %ARRAY_MAX_LEN, and do not allow to generate the proof in such case.

; code
; --------------------------
; first_iteration <-- Compute a[0] + b
; while(loop_index_check) { <-- While 0 < i < len(a)
; loop2inA <-- Compute a[i] + carry
; }
; 1] check_carry <-- If there is a carry, append it to the result
; 2] trim <-- Otherwise, trim the result
; end
; --------------------------

VAR GLOBAL array_add_short_inA[%ARRAY_MAX_LEN]
VAR GLOBAL array_add_short_inB
VAR GLOBAL array_add_short_out[%ARRAY_MAX_LEN_PLUS_ONE]
VAR GLOBAL array_add_short_out[%ARRAY_MAX_LEN] ; This cannot be bigger because we use it for division checking
VAR GLOBAL array_add_short_len_inA
VAR GLOBAL array_add_short_len_out

VAR GLOBAL array_add_short_carry

VAR GLOBAL array_add_short_RR


/*
* RESOURCES:
* -----------------------------
* (worst case) [steps: 8] + (lenA-1)*[steps: 6, bin: 1] + [steps: 6]
* total: [steps: 8 + 6*lenA, bin: lenA - 1]
* -----------------------------
*/

array_add_short:
%MAX_CNT_BINARY - CNT_BINARY - C :JMPN(outOfCountersBinary)
%MAX_CNT_STEPS - STEP - 5 - 10*C - 8 :JMPN(outOfCountersStep)
%MAX_CNT_BINARY - CNT_BINARY + 1 - %ARRAY_MAX_LEN :JMPN(outOfCountersBinary)
%MAX_CNT_STEPS - STEP - 8 - 6*%ARRAY_MAX_LEN :JMPN(outOfCountersStep)

RR :MSTORE(array_add_short_RR)

C :MSTORE(array_add_short_len_inA)

0 => E ; index in loops
$ => A :MLOAD(array_add_short_inB)
A :MSTORE(array_add_short_carry)
array_add_short_first_iteration:
; a[0] + b, where a[0] ∈ [0,base-1]: the number cannot be GT base + (base - 2), two chunks
$ => A :MLOAD(array_add_short_inA)
$ => B :MLOAD(array_add_short_inB)
$ :ADD, MSTORE(array_add_short_out), JMPC(__array_add_short_continue_1)
; ---------------------
0 => D :JMP(__array_add_short_continue_2)
__array_add_short_continue_1:
1 => D
__array_add_short_continue_2:
; ---------------------

array_add_short_loopZero2inA:
; The result will be stored as D·base + C
1 => E

0 => D ; reset the carry chunk
array_add_short_loop_index_check:
; C = len_inA
C - E :JMPZ(array_add_short_check_carry)

; a[i] + carry, where a[i] ∈ [0,base-1]:
; · If i = 0, then carry = inB and then the number cannot be GT base + (base - 2), two chunks
; · Otherwise, the number cannot be GT base, two chunks
array_add_short_loop2inA:
; a[i] + carry, where a[i] ∈ [0,base-1]: the number cannot be GT base, two chunks
$ => A :MLOAD(array_add_short_inA + E)
$ => B :MLOAD(array_add_short_carry)
$ => C :ADD, JMPNC(__array_add_short_continue_1)
D => B
$ :ADD, MSTORE(array_add_short_out + E), JMPC(__array_add_short_continue_3)
; ---------------------
0 => D :JMP(__array_add_short_continue_4)
__array_add_short_continue_3:
1 => D
__array_add_short_continue_1:

C :MSTORE(array_add_short_out + E)
D :MSTORE(array_add_short_carry)
__array_add_short_continue_4:
; ---------------------

E + 1 => E,A
$ => B :MLOAD(array_add_short_len_inA)
B - A :JMPZ(array_add_short_check_carry, array_add_short_loopZero2inA)
E + 1 => E :JMP(array_add_short_loop_index_check)

array_add_short_check_carry:
D => A
A :JMPZ(__array_add_short_continue_2)
D :JMPZ(array_add_short_trim)

; Carry path
E - %ARRAY_MAX_LEN :JMPZ(failAssert)

; In this case, the carry = 1 and we should append it to the result
1 :MSTORE(array_add_short_out + E)
E + 1 :MSTORE(array_add_short_len_out)
:JMP(array_add_short_end)
__array_add_short_continue_2:
E :MSTORE(array_add_short_len_out)
E + 1 :MSTORE(array_add_short_len_out), JMP(array_add_short_end)

array_add_short_trim:
E :MSTORE(array_add_short_len_out)

array_add_short_end:
$ => RR :MLOAD(array_add_short_RR)
Expand Down
Loading
Loading