diff --git a/main/modexp/array_lib/array_add_AGTB.zkasm b/main/modexp/array_lib/array_add_AGTB.zkasm
index 3982aa5f..7bcbccf8 100644
--- a/main/modexp/array_lib/array_add_AGTB.zkasm
+++ b/main/modexp/array_lib/array_add_AGTB.zkasm
@@ -13,7 +13,7 @@
 ;;                  · out = inA + inB, with len(out) <= C + 1
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_add_AGTB(a: bigint[], b: bigint[], B: bigint): bigint[] {
+; 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);
@@ -21,13 +21,13 @@
 ;     let carry = 0n;
 ;     for (let i = 0; i < blen; i++) {
 ;         sum = a[i] + b[i] + carry;
-;         carry = sum >= B ? 1n : 0n;
-;         result[i] = sum - carry * B;
+;         carry = sum >= base ? 1n : 0n;
+;         out[i] = sum - carry * base;
 ;     }
 ;     for (let i = blen; i < alen; i++) {
 ;         sum = a[i] + carry;
-;         carry = sum == B ? 1n : 0n; // the past carry is at most 1n
-;         result[i] = sum - carry * B;
+;         carry = sum == base ? 1n : 0n; // the past carry is at most 1n
+;         out[i] = sum - carry * base;
 ;     }
 
 ;     if (carry === 1n) {
@@ -36,7 +36,7 @@
 ;     return result;
 ; }
 
-; NOTE: It's unoptimized for the case where len(inB) = 1. Use array_add_short instead if possible.
+; 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]
 VAR GLOBAL array_add_AGTB_inB[%ARRAY_MAX_LEN]
@@ -50,8 +50,8 @@ VAR GLOBAL array_add_AGTB_carry
 VAR GLOBAL array_add_AGTB_RR
 
 array_add_AGTB:
-        %MAX_CNT_BINARY - CNT_BINARY     - 3*D  - 1 -    C+   D - 1      :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 6 - 17*D - 4 - 11*C+11*D - 8      :JMPN(outOfCountersStep)
+        %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)
 
         RR              :MSTORE(array_add_AGTB_RR)
 
@@ -60,71 +60,61 @@ array_add_AGTB:
 
         0 => E ; index in loops
         0               :MSTORE(array_add_AGTB_carry)
-                        :JMP(array_add_AGTB_loopZero2inB)
-
-; Begin of branching
-array_add_AGTB_add_carry1:
-        D + 1 => D     :JMP(return_array_add_AGTB_add_carry1)
-
-array_add_AGTB_add_carry2:
-        D + 1 => D     :JMP(return_array_add_AGTB_add_carry2)
-
-array_add_AGTB_add_carry3:
-        D + 1 => D     :JMP(return_array_add_AGTB_add_carry3)
-; End of branching
 
 array_add_AGTB_loopZero2inB:
-        0 => D  ; for the carry
+        ; The result will be stored as D·base + C
+
+        0 => D  ; reset the carry chunk
 
-        ; a[i] + b[i]
+        ; 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, JMPC(array_add_AGTB_add_carry1)
-                        return_array_add_AGTB_add_carry1:
+        $ => C          :ADD, JMPNC(__array_add_AGTB_continue_1)
+        1 => D
+                        __array_add_AGTB_continue_1:
 
-        ; sum = (a[i] + b[i]) + carry
+        ; sum = (a[i] + b[i]) + carry: This number cannot be GT base + (base - 1), two chunks
         $ => A          :MLOAD(array_add_AGTB_carry)
         C => B
-        $ => C          :ADD, JMPC(array_add_AGTB_add_carry2)
-                        return_array_add_AGTB_add_carry2:
+        $ => C          :ADD, JMPNC(__array_add_AGTB_continue_2)
+        1 => D
+                        __array_add_AGTB_continue_2:
 
         C               :MSTORE(array_add_AGTB_out + E)
         D               :MSTORE(array_add_AGTB_carry)
 
-        E + 1 => E
-        E => A
+        E + 1 => E,A
         $ => B          :MLOAD(array_add_AGTB_len_inB)
-        $               :EQ, JMPC(array_add_AGTB_loop_index_check1, array_add_AGTB_loopZero2inB)
+        B - A           :JMPZ(array_add_AGTB_loop_index_check, array_add_AGTB_loopZero2inB)
 
-array_add_AGTB_loop_index_check1:
-        E => A
+array_add_AGTB_loop_index_check:
         $ => B          :MLOAD(array_add_AGTB_len_inA)
-        $               :EQ, JMPC(array_add_AGTB_check_carry)
+        B - A           :JMPZ(array_add_AGTB_check_carry)
+
         0 => D
 array_add_AGTB_loopInB2InA:
-        ; sum = a[i] + carry
+        ; 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, JMPC(array_add_AGTB_add_carry3)
-                        return_array_add_AGTB_add_carry3:
+        $ => C          :ADD, JMPNC(__array_add_AGTB_continue_3)
+        1 => D
+                        __array_add_AGTB_continue_3:
 
         C               :MSTORE(array_add_AGTB_out + E)
         D               :MSTORE(array_add_AGTB_carry)
 
-        E + 1 => E
-        E => A
+        E + 1 => E,A
         $ => B          :MLOAD(array_add_AGTB_len_inA)
-        $               :EQ, JMPC(array_add_AGTB_check_carry, array_add_AGTB_loopInB2InA)
+        B - A           :JMPZ(array_add_AGTB_check_carry, array_add_AGTB_loopInB2InA)
 
 array_add_AGTB_check_carry:
-        $ => A          :MLOAD(array_add_AGTB_carry)
-        1 => B
-        $               :EQ, JMPNC(array_add_AGTB_len_out)
+        D => A
+        A               :JMPZ(__array_add_AGTB_continue_4)
+        ; 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_len_out:
+                        __array_add_AGTB_continue_4:
         E               :MSTORE(array_add_AGTB_len_out)
 
 array_add_AGTB_end:
diff --git a/main/modexp/array_lib/array_add_short.zkasm b/main/modexp/array_lib/array_add_short.zkasm
index 04d2bd42..6fe10b0b 100644
--- a/main/modexp/array_lib/array_add_short.zkasm
+++ b/main/modexp/array_lib/array_add_short.zkasm
@@ -10,15 +10,15 @@
 ;;                  · out = inA + inB, with len(out) <= C + 1
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_add_short(a: bigint[], b: bigint, B: bigint): bigint[] {
+; 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 >= B ? 1n : 0n;
-;         result[i] = sum - carry * B;
+;         carry = sum >= base ? 1n : 0n;
+;         out[i] = sum - carry * base;
 ;     }
 
 ;     if (carry === 1n) {
@@ -38,8 +38,8 @@ VAR GLOBAL array_add_short_carry
 VAR GLOBAL array_add_short_RR
 
 array_add_short:
-        %MAX_CNT_BINARY - CNT_BINARY     - 2*C  - 1       :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 6 - 12*C - 8       :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY     -    C           :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 5 - 10*C - 8       :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_add_short_RR)
 
@@ -48,40 +48,37 @@ array_add_short:
         0 => E ; index in loops
         $ => A          :MLOAD(array_add_short_inB)
         A               :MSTORE(array_add_short_carry)
-                        :JMP(array_add_short_loopZero2inA)
-
-; Begin of branching
-array_add_short_add_carry:
-        D + 1 => D     :JMP(return_array_add_short_add_carry)
-; End of branching
 
 array_add_short_loopZero2inA:
-        0 => D  ; for the carry
+        ; The result will be stored as D·base + C
+
+        0 => D  ; reset the carry chunk
 
-        ; a[i] + carry. If i = 0, then carry = inB.
+        ; 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
         $ => A          :MLOAD(array_add_short_inA + E)
         $ => B          :MLOAD(array_add_short_carry)
-        $ => C          :ADD, JMPC(array_add_short_add_carry)
-                        return_array_add_short_add_carry:
+        $ => C          :ADD, JMPNC(__array_add_short_continue_1)
+        1 => D
+                        __array_add_short_continue_1:
 
         C               :MSTORE(array_add_short_out + E)
         D               :MSTORE(array_add_short_carry)
 
-        E + 1 => E
-        E => A
+        E + 1 => E,A
         $ => B          :MLOAD(array_add_short_len_inA)
-        $               :EQ, JMPC(array_add_short_check_carry, array_add_short_loopZero2inA)
+        B - A           :JMPZ(array_add_short_check_carry, array_add_short_loopZero2inA)
 
 array_add_short_check_carry:
         D => A
-        1 => B
-        $               :EQ, JMPNC(array_add_short_len_out)
+        A               :JMPZ(__array_add_short_continue_2)
+        ; 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_len_out:
-        E               :MSTORE(array_add_short_len_out)
+                        __array_add_short_continue_2:
+         E              :MSTORE(array_add_short_len_out)
 
 array_add_short_end:
         $ => RR         :MLOAD(array_add_short_RR)
diff --git a/main/modexp/array_lib/array_div.zkasm b/main/modexp/array_lib/array_div.zkasm
index 2bada0d5..9a1e4e5e 100644
--- a/main/modexp/array_lib/array_div.zkasm
+++ b/main/modexp/array_lib/array_div.zkasm
@@ -13,7 +13,7 @@
 ;;                  · [quo,rem] = [inA / inB, inA % inB], with len(quo) <= C - D + 1, len(rem) <= D
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_div(a: bigint[], b: bigint[], B: bigint): bigint[] {
+; function array_div(a: bigint[], b: bigint[], base: bigint): bigint[] {
 ;     if (a === [0n]) {
 ;         if (b === [0n]) {
 ;             throw new Error("Division by zero");
@@ -30,9 +30,9 @@
 ;     }
 ;
 ;     if (b.length === 1) {
-;         return array_div_short(a, b, B);
+;         return array_div_short(a, b, base);
 ;     }
-;     return array_div_long(a, b, B);
+;     return array_div_long(a, b, base);
 ; }
 
 VAR GLOBAL array_div_inA[%ARRAY_MAX_LEN]
@@ -52,73 +52,61 @@ VAR GLOBAL array_div_RR
 ; 1 - inB is zero
 
 array_div:
-        %MAX_CNT_BINARY - CNT_BINARY - 4                    :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 19 - 4*C - 4*D - 1   :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY - 2                    :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 12 - 3*C - 3*D - 1   :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_div_RR)
+
         C               :MSTORE(array_div_len_inA)
         D               :MSTORE(array_div_len_inB)
 
         ; Let's cover the edge cases
-        ; 1] Is C == 1 and inA == 0?
-        C => A
         1 => B
-        $               :EQ, JMPNC(array_div_inA_continue)
-        0 => B
+        ; 1] Is C == 1 and inA == 0?
+        C - B           :JMPNZ(__array_div_inA_continue)
         $ => A          :MLOAD(array_div_inA)
-        $               :EQ, JMPC(array_div_inA_is_zero)
-                        array_div_inA_continue:
+        $               :LT, JMPC(array_div_inA_is_zero)
+                        __array_div_inA_continue:
 
         ; 2] Is D == 1 and inB == 0?
-        D => A
-        1 => B
-        $               :EQ, JMPNC(array_div_inB_continue1)
-        0 => B
+        D - B           :JMPNZ(__array_div_inB_continue_1)
         $ => A          :MLOAD(array_div_inB)
-        $               :EQ, JMPC(array_div_inB_is_zero)
-                        array_div_inB_continue1:
+        $               :LT, JMPC(array_div_inB_is_zero)
+                        __array_div_inB_continue_1:
 
         ; 3] Check if inA = inB or inA < inB
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 array_div_compare_inA:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_inA + RR)
         A               :MSTORE(array_compare_inA + RR)
-        RR              :JMPZ(array_div_compare_inB, array_div_compare_inA)
+        RR - 1 => RR    :JMPN(array_div_compare_inB, array_div_compare_inA)
 
 array_div_compare_inB:
-        E - 1 => E
         $ => A          :MLOAD(array_div_inB + E)
         A               :MSTORE(array_compare_inB + E)
-        E               :JMPZ(array_div_compare, array_div_compare_inB)
+        E - 1 => E      :JMPN(array_div_compare, array_div_compare_inB)
 
 array_div_compare:
                         :CALL(array_compare)
 
-        %MAX_CNT_BINARY - CNT_BINARY - 2                  :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 7 - 4*C - 4*D - 1  :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP        - 5 - 3*C - 3*D - 1  :JMPN(outOfCountersStep)
 
         $ => A          :MLOAD(array_compare_result), JMPZ(array_div_prep_inALTinB)
-        1 => B
-        $               :EQ, JMPC(array_div_same_input)
+        A - 1           :JMPZ(array_div_same_input)
         ; From here, inA > inB
 
-        C => RR
-        D => A,E
-        1 => B
-        $               :EQ, JMPC(array_div_inA_to_div_short, array_div_inA_to_div_long); worst case is div long
+        C - 1 => RR
+        D - 1 => E
+        D - 1           :JMPZ(array_div_inA_to_div_short, array_div_inA_to_div_long); worst case is div long
 
 ; Begin of edge cases
 array_div_inA_is_zero:
         ;Is D == 1 and inB == 0? 0/0 is undefined
-        D => A
-        1 => B
-        $               :EQ, JMPNC(array_div_inB_continue2)
-        0 => B
+        D - B           :JMPNZ(__array_div_inB_continue_2)
         $ => A          :MLOAD(array_div_inB)
-        $               :EQ, JMPC(array_div_inB_is_zero)
-                        array_div_inB_continue2:
+        $               :LT, JMPC(array_div_inB_is_zero)
+                        __array_div_inB_continue_2:
         ; From here, inB != 0
 
         ; Return [q,r] = [0,0] and len(q) = 1, len(r) = 1
@@ -145,13 +133,11 @@ array_div_prep_inALTinB:
 
         %MAX_CNT_STEPS - STEP  - 1 - 4*C - 2        :JMPN(outOfCountersStep)
 
-        0 => RR
-
+        C - 1 => RR
 array_div_inALTinB:
         $ => A          :MLOAD(array_div_inA + RR)
         A               :MSTORE(array_div_rem + RR)
-        RR + 1 => RR
-        C - 1 => C      :JMPNZ(array_div_inALTinB)
+        RR - 1 => RR    :JMPN(array_div_inALTinB_before_end, array_div_inALTinB)
 
 array_div_inALTinB_before_end:
         0               :MSTORE(array_div_quo)
@@ -160,49 +146,44 @@ array_div_inALTinB_before_end:
 
 ; Long
 array_div_inA_to_div_long:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_inA + RR)
         A               :MSTORE(array_div_long_inA + RR)
-        RR              :JMPZ(array_div_inB_to_div_long, array_div_inA_to_div_long)
+        RR - 1 => RR    :JMPN(array_div_inB_to_div_long, array_div_inA_to_div_long)
 
 array_div_inB_to_div_long:
-        E - 1 => E
         $ => A          :MLOAD(array_div_inB + E)
         A               :MSTORE(array_div_long_inB + E)
-        E               :JMPZ(array_div_compute_long, array_div_inB_to_div_long)
+        E - 1 => E      :JMPN(array_div_compute_long, array_div_inB_to_div_long)
 
 array_div_compute_long:
                         :CALL(array_div_long)
 
-        %MAX_CNT_STEPS - STEP - 6      :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 7      :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_div_long_len_quo)
         $ => D          :MLOAD(array_div_long_len_rem)
         C               :MSTORE(array_div_len_quo)
         D               :MSTORE(array_div_len_rem)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*D - 2  :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*D - 2  :JMPN(outOfCountersStep)
 
 array_div_assign_long_quo:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_long_quo + RR)
         A               :MSTORE(array_div_quo + RR)
-        RR              :JMPZ(array_div_assign_long_rem, array_div_assign_long_quo)
+        RR - 1 => RR    :JMPN(array_div_assign_long_rem, array_div_assign_long_quo)
 
 array_div_assign_long_rem:
-        E - 1 => E
         $ => A          :MLOAD(array_div_long_rem + E)
         A               :MSTORE(array_div_rem + E)
-        E               :JMPZ(array_div_end, array_div_assign_long_rem)
+        E - 1 => E      :JMPN(array_div_end, array_div_assign_long_rem)
 
 ; Short
 array_div_inA_to_div_short:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_inA + RR)
         A               :MSTORE(array_div_short_inA + RR)
-        RR              :JMPZ(array_div_inB_to_div_short, array_div_inA_to_div_short)
+        RR - 1 => RR    :JMPN(array_div_inB_to_div_short, array_div_inA_to_div_short)
 
 array_div_inB_to_div_short:
         $ => A          :MLOAD(array_div_inB)
@@ -216,15 +197,14 @@ array_div_compute_short:
         $ => C          :MLOAD(array_div_short_len_quo)
         C               :MSTORE(array_div_len_quo)
         1               :MSTORE(array_div_len_rem)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4  :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 4  :JMPN(outOfCountersStep)
 
 array_div_assign_short_quo:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_short_quo + RR)
         A               :MSTORE(array_div_quo + RR)
-        RR              :JMPZ(array_div_assign_short_rem, array_div_assign_short_quo)
+        RR - 1 => RR    :JMPN(array_div_assign_short_rem, array_div_assign_short_quo)
 
 array_div_assign_short_rem:
         $ => A          :MLOAD(array_div_short_rem)
diff --git a/main/modexp/array_lib/array_div_long.zkasm b/main/modexp/array_lib/array_div_long.zkasm
index c9792a7d..51201964 100644
--- a/main/modexp/array_lib/array_div_long.zkasm
+++ b/main/modexp/array_lib/array_div_long.zkasm
@@ -13,7 +13,7 @@
 ;;                  · [quo,rem] = [inA / inB, inA % inB], with len(quo) <= C - D + 1, len(rem) <= D
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_div_long(a: bigint[], b: bigint[], B: bigint): bigint[] {
+; function array_div_long(a: bigint[], b: bigint[], base: bigint): bigint[] {
 ;     if (a === [0n]) {
 ;         if (b === [0n]) {
 ;             throw new Error("Division by zero");
@@ -50,58 +50,52 @@ VAR GLOBAL array_div_long_RR
 ; 1 - inB is zero
 
 array_div_long:
-        %MAX_CNT_BINARY - CNT_BINARY - 4                  :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 19 - 4*C - 4*D - 1 :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY - 2                  :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 12 - 3*C - 3*D - 1 :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_div_long_RR)
+
         C               :MSTORE(array_div_long_len_inA)
         D               :MSTORE(array_div_long_len_inB)
 
         ; Let's cover the edge cases
-        ; 1] Is C == 1 and inA == 0?
-        C => A
         1 => B
-        $               :EQ, JMPNC(array_div_long_inA_continue)
-        0 => B
+        ; 1] Is C == 1 and inA == 0?
+        C - B           :JMPNZ(__array_div_long_inA_continue)
         $ => A          :MLOAD(array_div_long_inA)
-        $               :EQ, JMPC(array_div_long_inA_is_zero)
-                        array_div_long_inA_continue:
+        $               :LT, JMPC(array_div_long_inA_is_zero)
+                        __array_div_long_inA_continue:
 
         ; 2] Is D == 1 and inB == 0?
-        D => A
-        1 => B
-        $               :EQ, JMPNC(array_div_long_inB_continue1)
-        0 => B
+        D - B           :JMPNZ(__array_div_long_inB_continue_1)
         $ => A          :MLOAD(array_div_long_inB)
-        $               :EQ, JMPC(array_div_long_inB_is_zero)
-                        array_div_long_inB_continue1:
+        $               :LT, JMPC(array_div_long_inB_is_zero)
+                        __array_div_long_inB_continue_1:
 
         ; 3] Check if inA = inB or inA < inB
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 array_div_long_compare_inA1:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_long_inA + RR)
         A               :MSTORE(array_compare_inA + RR)
-        RR              :JMPZ(array_div_long_compare_inB1, array_div_long_compare_inA1)
+        RR - 1 => RR    :JMPN(array_div_long_compare_inB1, array_div_long_compare_inA1)
 
 array_div_long_compare_inB1:
-        E - 1 => E
         $ => A          :MLOAD(array_div_long_inB + E)
         A               :MSTORE(array_compare_inB + E)
-        E               :JMPZ(array_div_long_compare1, array_div_long_compare_inB1)
+        E - 1 => E      :JMPN(array_div_long_compare1, array_div_long_compare_inB1)
 
 array_div_long_compare1:
                         :CALL(array_compare)
 
-        %MAX_CNT_BINARY - CNT_BINARY - 4         :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 20        :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY - 1         :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 15        :JMPN(outOfCountersStep)
 
         $ => A          :MLOAD(array_compare_result), JMPZ(array_div_long_prep_inALTinB)
-        1 => B
-        $               :EQ, JMPC(array_div_long_same_input)
+        A - 1           :JMPZ(array_div_long_same_input)
         ; From here, inA > inB
 
+        ; Strategy: Divide outside and check the result inside
         $${MPdiv(addr.array_div_long_inA,mem.array_div_long_len_inA,addr.array_div_long_inB,mem.array_div_long_len_inB)}
 
                         :JMP(array_div_long_prepare_mul_quo_inB)
@@ -109,14 +103,11 @@ array_div_long_compare1:
 ; Begin of edge cases
 array_div_long_inA_is_zero:
         ; Is D == 1 and inB == 0? 0/0 is undefined
-        D => A
-        1 => B
-        $               :EQ, JMPNC(array_div_long_inB_continue2)
-        0 => B
+        D - B           :JMPNZ(__array_div_long_inB_continue_2)
         $ => A          :MLOAD(array_div_long_inB)
-        $               :EQ, JMPC(array_div_long_inB_is_zero)
-                        array_div_long_inB_continue2:
-        ; From here, inB != 0
+        $               :LT, JMPC(array_div_long_inB_is_zero)
+                        __array_div_long_inB_continue_2:
+        ; From here, inA == 0 and inB != 0
 
         ; Return [q,r] = [0,0] and len(q) = 1, len(r) = 1
         0               :MSTORE(array_div_long_quo)
@@ -130,6 +121,7 @@ array_div_long_inB_is_zero:
         1 => B          :JMP(array_div_long_end)
 
 array_div_long_same_input:
+        ; if inA = inB, then return [1, 0] and len(q) = 1, len(r) = 1
         1               :MSTORE(array_div_long_quo)
         0               :MSTORE(array_div_long_rem)
         1               :MSTORE(array_div_long_len_quo)
@@ -137,18 +129,17 @@ array_div_long_same_input:
         0 => B          :JMP(array_div_long_end)
 
 array_div_long_prep_inALTinB:
-        C               :MSTORE(array_div_long_len_rem)
+        ; if inA < inB, then return [0, inA] and len(q) = 1, len(r) = C
         1               :MSTORE(array_div_long_len_quo)
+        C               :MSTORE(array_div_long_len_rem)
 
         %MAX_CNT_STEPS - STEP  - 1 - 4*C - 2        :JMPN(outOfCountersStep)
 
-        0 => RR
-
+        C - 1 => RR
 array_div_long_inALTinB:
         $ => A          :MLOAD(array_div_long_inA + RR)
         A               :MSTORE(array_div_long_rem + RR)
-        RR + 1 => RR
-        C - 1 => C      :JMPNZ(array_div_long_inALTinB)
+        RR - 1 => RR    :JMPN(array_div_long_inALTinB_before_end, array_div_long_inALTinB)
 
 array_div_long_inALTinB_before_end:
         0               :MSTORE(array_div_long_quo)
@@ -171,36 +162,35 @@ array_div_long_prepare_mul_quo_inB:
         ; From here, the quotient is trimmed
 
         C               :MSTORE(array_div_long_len_quo)
+
         $ => D          :MLOAD(array_div_long_len_inB)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 5*%ARRAY_MAX_LEN - 4*D - 1      :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 4*%ARRAY_MAX_LEN - 3*D - 1      :JMPN(outOfCountersStep)
 
 array_div_long_quo_to_mul:
-        RR - 1 => RR
         ${receiveQuotientChunk(RR)} => A
         A               :MSTORE(array_div_long_quo + RR)
         A               :MSTORE(array_mul_inA + RR)
-        RR              :JMPZ(array_div_long_inB_to_mul, array_div_long_quo_to_mul)
+        RR - 1 => RR    :JMPN(array_div_long_inB_to_mul, array_div_long_quo_to_mul)
 
 array_div_long_inB_to_mul:
-        E - 1 => E
         $ => A          :MLOAD(array_div_long_inB + E)
         A               :MSTORE(array_mul_inB + E)
-        E               :JMPZ(array_div_long_mul_quo_inB, array_div_long_inB_to_mul)
+        E - 1 => E      :JMPN(array_div_long_mul_quo_inB, array_div_long_inB_to_mul)
 
 array_div_long_mul_quo_inB:
                         :CALL(array_mul)
 
-        %MAX_CNT_BINARY - CNT_BINARY - 3        :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 14       :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY - 1        :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 10       :JMPN(outOfCountersStep)
 
         ; Check the remainder
         $0{receiveLenRemainder()} => D
 
         ; 1] The received length must be between 1 and %ARRAY_MAX_LEN
-        D - 1 => E             :JMPN(failAssert) ; If D = 0, then fail
+        D - 1 => E              :JMPN(failAssert) ; If D = 0, then fail
         %ARRAY_MAX_LEN - D      :JMPN(failAssert) ; If D > %ARRAY_MAX_LEN, then fail
         ; From here, 1 <= D <= %ARRAY_MAX_LEN
 
@@ -213,22 +203,20 @@ array_div_long_mul_quo_inB:
 
         ; 3] Finally, we must ensure that the remainder is lower than inB
         $ => C           :MLOAD(array_div_long_len_inB)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*%ARRAY_MAX_LEN - 1    :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*%ARRAY_MAX_LEN - 1    :JMPN(outOfCountersStep)
 
 array_div_long_compare_inB2:
-        RR - 1 => RR
-        $ => A          :MLOAD(array_div_inB + RR)
+        $ => A          :MLOAD(array_div_long_inB + RR)
         A               :MSTORE(array_compare_inA + RR)
-        RR              :JMPZ(array_div_long_compare_rem, array_div_long_compare_inB2)
+        RR - 1 => RR    :JMPN(array_div_long_compare_rem, array_div_long_compare_inB2)
 
 array_div_long_compare_rem:
-        E - 1 => E
         ${receiveRemainderChunk(E)} => A
         A               :MSTORE(array_compare_inB + E)
-        E               :JMPZ(array_div_long_compare2, array_div_long_compare_rem)
+        E - 1 => E      :JMPN(array_div_long_compare2, array_div_long_compare_rem)
 
 array_div_long_compare2:
                         :CALL(array_compare)
@@ -241,23 +229,21 @@ array_div_long_compare2:
 
         ; prepare output and remainder to be added
         $ => C          :MLOAD(array_mul_len_out)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 5*D - 1    :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 4*D - 1    :JMPN(outOfCountersStep)
 
 array_div_long_res_to_add:
-        RR - 1 => RR
         $ => A          :MLOAD(array_mul_out + RR)
         A               :MSTORE(array_add_AGTB_inA + RR)
-        RR              :JMPZ(array_div_long_rem_to_add, array_div_long_res_to_add)
+        RR - 1 => RR    :JMPN(array_div_long_rem_to_add, array_div_long_res_to_add)
 
 array_div_long_rem_to_add:
-        E - 1 => E
         ${receiveRemainderChunk(E)} => A
         A               :MSTORE(array_div_long_rem + E)
         A               :MSTORE(array_add_AGTB_inB + E)
-        E               :JMPZ(array_div_long_add_res_rem, array_div_long_rem_to_add)
+        E - 1 => E      :JMPN(array_div_long_add_res_rem, array_div_long_rem_to_add)
 
 array_div_long_add_res_rem:
                         :CALL(array_add_AGTB)
@@ -267,22 +253,20 @@ array_div_long_add_res_rem:
         ; prepare next
         $ => C           :MLOAD(array_add_AGTB_len_out)
         $ => D           :MLOAD(array_div_long_len_inA)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*D - 1    :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*D - 1    :JMPN(outOfCountersStep)
 
 array_div_long_compare_inA2:
-        RR - 1 => RR
         $ => A          :MLOAD(array_add_AGTB_out + RR)
         A               :MSTORE(array_compare_inA + RR)
-        RR              :JMPZ(array_div_long_compare_inB3, array_div_long_compare_inA2)
+        RR - 1 => RR    :JMPN(array_div_long_compare_inB3, array_div_long_compare_inA2)
 
 array_div_long_compare_inB3:
-        E - 1 => E
         $ => A          :MLOAD(array_div_long_inA + E)
         A               :MSTORE(array_compare_inB + E)
-        E               :JMPZ(array_div_long_compare3, array_div_long_compare_inB3)
+        E - 1 => E      :JMPN(array_div_long_compare3, array_div_long_compare_inB3)
 
 array_div_long_compare3:
                         :CALL(array_compare)
@@ -290,7 +274,7 @@ array_div_long_compare3:
         %MAX_CNT_STEPS - STEP - 4      :JMPN(outOfCountersStep)
 
         1               :MLOAD(array_compare_result)
-        0 => B ; everything worked fine
+        0 => B
 
 array_div_long_end:
         $ => RR         :MLOAD(array_div_long_RR)
diff --git a/main/modexp/array_lib/array_div_short.zkasm b/main/modexp/array_lib/array_div_short.zkasm
index 27fe5e63..22b2ddf7 100644
--- a/main/modexp/array_lib/array_div_short.zkasm
+++ b/main/modexp/array_lib/array_div_short.zkasm
@@ -12,7 +12,7 @@
 ;;                  · [quo,rem] = [inA / inB[0], inA % inB[0]], with len(quo) <= C, len(rem) = 1
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_div_short(a: bigint[], b: bigint, B: bigint): bigint[] {
+; function array_div_short(a: bigint[], b: bigint, base: bigint): bigint[] {
 ;     if (a === [0n]) {
 ;         if (b === 0n) {
 ;             throw new Error("Division by zero");
@@ -47,37 +47,33 @@ VAR GLOBAL array_div_short_RR
 ; 1 - inB is zero
 
 array_div_short:
-
-        %MAX_CNT_BINARY - CNT_BINARY - 3             :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 15 - 4*C - 3  :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY - 2             :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 11 - 3*C - 3  :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_div_short_RR)
+
         C               :MSTORE(array_div_short_len_inA)
         C               :MSTORE(array_div_short_len_quo)
 
         ; Let's cover the edge cases
-        ; 1] Is inA == 0?
-        C => A
         1 => B
-        $               :EQ, JMPNC(array_div_short_inA_continue)
-        0 => B
+        ; 1] Is C == 1 and inA == 0?
+        C - B           :JMPNZ(__array_div_short_inA_continue)
         $ => A          :MLOAD(array_div_short_inA)
-        $               :EQ, JMPC(array_div_short_inA_is_zero)
-                        array_div_short_inA_continue:
+        $               :LT, JMPC(array_div_short_inA_is_zero)
+                        __array_div_short_inA_continue:
 
         ; 2] Is inB == 0?
-        0 => B
         $ => A          :MLOAD(array_div_short_inB)
-        $               :EQ, JMPC(array_div_short_inB_is_zero)
+        $               :LT, JMPC(array_div_short_inB_is_zero)
 
         ; Check whether inA = inB or inA < inB
-        C => RR
+        C - 1 => RR
         1 => D
 array_div_short_inA_to_compare1:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_short_inA + RR)
         A               :MSTORE(array_compare_inA + RR)
-        RR              :JMPZ(array_div_short_inB_to_compare, array_div_short_inA_to_compare1)
+        RR - 1 => RR    :JMPN(array_div_short_inB_to_compare, array_div_short_inA_to_compare1)
 
 array_div_short_inB_to_compare:
         $ => A          :MLOAD(array_div_short_inB)
@@ -86,14 +82,12 @@ array_div_short_inB_to_compare:
 array_div_short_compare_inA_inB:
                         :CALL(array_compare)
 
-        %MAX_CNT_BINARY - CNT_BINARY - 4     :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 18    :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY - 1     :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 13    :JMPN(outOfCountersStep)
 
         $ => A          :MLOAD(array_compare_result), JMPZ(array_div_short_inALTinB)
-        1 => B
-        $               :EQ, JMPC(array_div_short_same_input)
-
-        ; From here, it is known that inA > inB
+        A - 1           :JMPZ(array_div_short_same_input)
+        ; From here, inA > inB
 
         ; Strategy: Divide outside and check the result inside
         $${MPdiv_short(addr.array_div_short_inA,mem.array_div_short_len_inA,mem.array_div_short_inB)}
@@ -104,7 +98,7 @@ array_div_short_compare_inA_inB:
 array_div_short_inA_is_zero:
         ; Is inB == 0? 0/0 is undefined
         $ => A          :MLOAD(array_div_short_inB)
-        $               :EQ, JMPC(array_div_short_inB_is_zero)
+        $               :LT, JMPC(array_div_short_inB_is_zero)
         ; From here, inB != 0
 
         ; Return [q,r] = [0,0] and len(q) = 1, len(r) = 1
@@ -149,16 +143,16 @@ array_div_short_prepare_mul_quo_inB:
         ; From here, the quotient is trimmed
 
         C               :MSTORE(array_div_short_len_quo)
-        C => RR
 
-        %MAX_CNT_STEPS - STEP - 5*%ARRAY_MAX_LEN - 4      :JMPN(outOfCountersStep)
+        C - 1 => RR
+
+        %MAX_CNT_STEPS - STEP - 4*%ARRAY_MAX_LEN - 3      :JMPN(outOfCountersStep)
 
 array_div_short_quo_to_mul:
-        RR - 1 => RR
         ${receiveQuotientChunk_short(RR)} => A
         A               :MSTORE(array_div_short_quo + RR)
         A               :MSTORE(array_mul_short_inA + RR)
-        RR              :JMPZ(array_div_short_inB_to_mul, array_div_short_quo_to_mul)
+        RR - 1 => RR    :JMPN(array_div_short_inB_to_mul, array_div_short_quo_to_mul)
 
 array_div_short_inB_to_mul:
         $ => A          :MLOAD(array_div_short_inB)
@@ -171,16 +165,15 @@ array_div_short_mul_quo_inB:
 
         ; prepare next
         $ => C          :MLOAD(array_mul_short_len_out)
-        C => RR
+        C - 1 => RR
 
         %MAX_CNT_BINARY - CNT_BINARY - 1     :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP - 4*C - 6      :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 6      :JMPN(outOfCountersStep)
 
 array_div_short_result_to_add:
-        RR - 1 => RR
         $ => A          :MLOAD(array_mul_short_out + RR)
         A               :MSTORE(array_add_short_inA + RR)
-        RR              :JMPZ(array_div_short_rem_to_add, array_div_short_result_to_add)
+        RR - 1 => RR    :JMPN(array_div_short_rem_to_add, array_div_short_result_to_add)
 
 array_div_short_rem_to_add:
         ${receiveRemainderChunk_short()} => A
@@ -200,22 +193,20 @@ array_div_short_add_result_rem:
         ; prepare next
         $ => C          :MLOAD(array_add_short_len_out)
         $ => D          :MLOAD(array_div_short_len_inA)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*D - 1    :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*D - 1    :JMPN(outOfCountersStep)
 
 array_div_short_result_to_compare:
-        RR - 1 => RR
         $ => A          :MLOAD(array_add_short_out + RR)
         A               :MSTORE(array_compare_inA + RR)
-        RR              :JMPZ(array_div_short_inA_to_compare2, array_div_short_result_to_compare)
+        RR - 1 => RR    :JMPN(array_div_short_inA_to_compare2, array_div_short_result_to_compare)
 
 array_div_short_inA_to_compare2:
-        E - 1 => E
         $ => A          :MLOAD(array_div_short_inA + E)
         A               :MSTORE(array_compare_inB + E)
-        E               :JMPZ(array_div_short_compare_result_inA, array_div_short_inA_to_compare2)
+        E - 1 => E      :JMPN(array_div_short_compare_result_inA, array_div_short_inA_to_compare2)
 
 array_div_short_compare_result_inA:
                         :CALL(array_compare)
@@ -223,7 +214,8 @@ array_div_short_compare_result_inA:
         %MAX_CNT_STEPS - STEP - 4      :JMPN(outOfCountersStep)
 
         1               :MLOAD(array_compare_result)
-        0 => B
+
+        0 => B ; error code
 
 array_div_short_end:
         $ => RR         :MLOAD(array_div_short_RR)
diff --git a/main/modexp/array_lib/array_mul.zkasm b/main/modexp/array_lib/array_mul.zkasm
index df12797a..e4551c1b 100644
--- a/main/modexp/array_lib/array_mul.zkasm
+++ b/main/modexp/array_lib/array_mul.zkasm
@@ -12,11 +12,11 @@
 ;;                  · out = inA·inB, with len(out) <= C + D
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_mul(a: bigint[], b: bigint[], B: bigint): bigint[] {
+; function array_mul(a: bigint[], b: bigint[], base: bigint): bigint[] {
 ;     if (b.length === 1) {
-;         return array_mul_short(a, b, B);
+;         return array_mul_short(a, b, base);
 ;     }
-;     return array_mul_long(a, b, B);
+;     return array_mul_long(a, b, base);
 ; }
 
 VAR GLOBAL array_mul_inA[%ARRAY_MAX_LEN]
@@ -29,53 +29,48 @@ VAR GLOBAL array_mul_len_out
 VAR GLOBAL array_mul_RR
 
 array_mul:
-        %MAX_CNT_BINARY - CNT_BINARY - 1                  :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 7 - 4*C - 4*D - 1  :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP        - 6 - 3*C - 3*D - 1  :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_mul_RR)
+
         C               :MSTORE(array_mul_len_inA)
         D               :MSTORE(array_mul_len_inB)
 
-        C => RR
-        D => A,E
-        1 => B
-        $               :EQ, JMPC(array_mul_inA_to_mul_short) ; worst case is mul long
+        C - 1 => RR
+        D - 1 => E
+        D - 1           :JMPZ(array_mul_inA_to_mul_short) ; worst case is mul long
 ; Long
 array_mul_inA_to_mul_long:
-        RR - 1 => RR
         $ => A          :MLOAD(array_mul_inA + RR)
         A               :MSTORE(array_mul_long_inA + RR)
-        RR              :JMPZ(array_mul_inB_to_mul_long, array_mul_inA_to_mul_long)
+        RR - 1 => RR    :JMPN(array_mul_inB_to_mul_long, array_mul_inA_to_mul_long)
 
 array_mul_inB_to_mul_long:
-        E - 1 => E
         $ => A          :MLOAD(array_mul_inB + E)
         A               :MSTORE(array_mul_long_inB + E)
-        E               :JMPZ(array_mul_compute_long, array_mul_inB_to_mul_long)
+        E - 1 => E      :JMPN(array_mul_compute_long, array_mul_inB_to_mul_long)
 
 array_mul_compute_long:
                         :CALL(array_mul_long)
 
-        %MAX_CNT_STEPS - STEP - 3   :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 4   :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_mul_long_len_out)
         C               :MSTORE(array_mul_len_out)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 2 :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 2 :JMPN(outOfCountersStep)
 
 array_mul_assign_long:
-        RR - 1 => RR
         $ => A          :MLOAD(array_mul_long_out + RR)
         A               :MSTORE(array_mul_out + RR)
-        RR              :JMPZ(array_mul_end, array_mul_assign_long)
+        RR - 1 => RR    :JMPN(array_mul_end, array_mul_assign_long)
 
 ; Short
 array_mul_inA_to_mul_short:
-        RR - 1 => RR
         $ => A          :MLOAD(array_mul_inA + RR)
         A               :MSTORE(array_mul_short_inA + RR)
-        RR              :JMPZ(array_mul_inB_to_mul_short, array_mul_inA_to_mul_short)
+        RR - 1 => RR    :JMPN(array_mul_inB_to_mul_short, array_mul_inA_to_mul_short)
 
 array_mul_inB_to_mul_short:
         $ => A          :MLOAD(array_mul_inB)
@@ -84,19 +79,18 @@ array_mul_inB_to_mul_short:
 array_mul_compute_short:
                         :CALL(array_mul_short)
 
-        %MAX_CNT_STEPS - STEP - 3   :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 4   :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_mul_short_len_out)
         C               :MSTORE(array_mul_len_out)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 2 :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 2 :JMPN(outOfCountersStep)
 
 array_mul_assign_short:
-        RR - 1 => RR
         $ => A          :MLOAD(array_mul_short_out + RR)
         A               :MSTORE(array_mul_out + RR)
-        RR              :JMPZ(array_mul_end, array_mul_assign_short)
+        RR - 1 => RR    :JMPN(array_mul_end, array_mul_assign_short)
 
 array_mul_end:
         $ => RR         :MLOAD(array_mul_RR)
diff --git a/main/modexp/array_lib/array_mul_long.zkasm b/main/modexp/array_lib/array_mul_long.zkasm
index bb5f6c30..3f63c3a9 100644
--- a/main/modexp/array_lib/array_mul_long.zkasm
+++ b/main/modexp/array_lib/array_mul_long.zkasm
@@ -13,23 +13,19 @@
 ;;                  · out = inA·inB, with len(out) <= C + D
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_mul_long(a: bigint[], b: bigint[], B: bigint): bigint[] {
+; function array_mul_long(a: bigint[], b: bigint[], base: bigint): bigint[] {
 ;     const alen = a.length;
 ;     const blen = b.length;
 ;     const len = alen + blen;
 ;     const result = new Array<bigint>(len).fill(0n);
 ;     let product: bigint;
 ;     let carry: bigint;
-;     let ai: bigint;
-;     let bj: bigint;
 ;     for (let i = 0; i < alen; i++) {
-;         ai = a[i];
 ;         for (let j = 0; j < blen; j++) {
-;             bj = b[j];
-;             product = ai * bj + result[i + j];
-;             carry = product / B;
-;             result[i + j] = product - carry * B;
-;             result[i + j + 1] += carry;
+;             product = a[i] * b[j] + out[i+j];
+;             carry = product / base;
+;             out[i+j] = product - carry * base;
+;             out[i + j + 1] += carry;
 ;         }
 ;     }
 ;     trim(result);
@@ -43,13 +39,13 @@ VAR GLOBAL array_mul_long_len_inA
 VAR GLOBAL array_mul_long_len_inB
 VAR GLOBAL array_mul_long_len_out
 
-VAR GLOBAL array_mul_long_result_carry
+VAR GLOBAL array_mul_long_out_chunk_2
 
 VAR GLOBAL array_mul_long_RR
 
 array_mul_long:
         %MAX_CNT_ARITH - CNT_ARITH - 1        :JMPN(outOfCountersArith)
-        %MAX_CNT_STEPS - STEP      - 6        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP      - 9        :JMPN(outOfCountersStep)
 
         C => A
         D => B
@@ -59,45 +55,38 @@ array_mul_long:
         B => D
         ; E holds C*D
 
-        %MAX_CNT_BINARY - CNT_BINARY                 - 5*E                :JMPN(outOfCountersBinary)
+        %MAX_CNT_BINARY - CNT_BINARY                 - 4*E                :JMPN(outOfCountersBinary)
         %MAX_CNT_ARITH - CNT_ARITH                   - E                  :JMPN(outOfCountersArith)
-        %MAX_CNT_STEPS - STEP        - 7 - 3*C - 3*D - 35*E - 2 - 4*C - 1 :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP        - 7 - 2*C - 2*D - 33*E - 2 - 3*C - 1 :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_mul_long_RR)
+
         C               :MSTORE(array_mul_long_len_inA)
         D               :MSTORE(array_mul_long_len_inB)
         C + D           :MSTORE(array_mul_long_len_out)
 
-        C + D => E ; auxiliar index
+        C + D - 1 => E ; auxiliar index
         0 => RCX   ; first index in loops
         0 => RR    ; second index in loops
 
 array_mul_long_clean_out:
-        E - 1 => E
         0               :MSTORE(array_mul_long_out + E)
-        E               :JMPZ(array_mul_long_loopZero2inB, array_mul_long_clean_out)
+        E - 1 => E      :JMPN(array_mul_long_loopZero2inB, array_mul_long_clean_out)
 
 ; Begin of branching
-array_mul_long_add_carry:
-        D + 1 => D      :JMP(return_array_mul_long_add_carry)
-
-array_mul_long_add_result_carry:
-        1               :MSTORE(array_mul_long_result_carry)
-                        :JMP(return_array_mul_long_add_result_carry)
-
 array_mul_long_loop_index_check:
         RCX + 1 => RCX
-        RCX => A
         $ => B          :MLOAD(array_mul_long_len_inA)
-        $               :EQ, JMPC(array_mul_long_prep_trim_in)
+        B - RCX         :JMPZ(array_mul_long_prep_trim_in)
 
-        0 => RR
-                        :JMP(return_array_mul_long_loop_index_check)
+        0 => RR ; reset the second index
 ; End of branching
 
 array_mul_long_loopZero2inB:
+        ; The result will be stored as D·base + C
+
         RCX => E
-        ; product = a_i * b_j + out[i + j]
+        ; 1] a[i]·b[j], where a[i],a[j] ∈ [0,base-1]: This number cannot be GT (base - 2)·base + 1, two chunks
         $ => A          :MLOAD(array_mul_long_inA + E)
         $ => B          :MLOAD(array_mul_long_inB + RR)
         0 => C
@@ -105,46 +94,52 @@ array_mul_long_loopZero2inB:
         ${_arrayLongMul_AB >> 256} => D
         ${_arrayLongMul_AB} => E :ARITH
 
-        ; sum lower part
+        ; 2] proudct = a[i]·b[j] + out[i+j], where out[i+j] ∈ [0,base-1]: This number cannot be GT (base - 1)·base, two chunks
         E => A
         RCX + RR => E
         $ => B          :MLOAD(array_mul_long_out + E)
-        $ => C          :ADD, JMPC(array_mul_long_add_carry)
-                        return_array_mul_long_add_carry:
-
-        ; sum higher part
+        $ => C          :ADD, JMPNC(__array_mul_long_no_carry_continue_1)
+        ;-----------------
+        ; Since here D ∈ [0, base - 2], there cannot be carry in the following addition
         D => A
-        $ => B          :MLOAD(array_mul_long_result_carry)
+        1 => B
         $ => D          :ADD
+        ;-----------------
+                        __array_mul_long_no_carry_continue_1:
+        $ => A          :MLOAD(array_mul_long_out_chunk_2)
+        D => B
+        $ => D          :ADD ; the number is of two chunks, no carry can be generated here
 
-        ; out[i + j] = product - carry·B
+        ; out[i+j] = product - carry·B
         C               :MSTORE(array_mul_long_out + E)
 
-        ; out[i + j + 1] += carry
+        ; out[i+j+1] += carry, where carry ∈ [0,base-1]: This number cannot be GT base + (base-3), two chunks
         E + 1 => E
         $ => A          :MLOAD(array_mul_long_out + E)
         D => B
-        $ => C          :ADD, JMPC(array_mul_long_add_result_carry)
-        0               :MSTORE(array_mul_long_result_carry)
-                        return_array_mul_long_add_result_carry:
+        $ => C          :ADD, JMPNC(__array_mul_long_no_carry_continue_2)
+        ;-----------------
+        1               :MSTORE(array_mul_long_out_chunk_2)
+                        :JMP(__array_mul_long_carry_continue)
+                        __array_mul_long_no_carry_continue_2:
+        0               :MSTORE(array_mul_long_out_chunk_2)
+                        __array_mul_long_carry_continue:
+        ;-----------------
+
         C               :MSTORE(array_mul_long_out + E)
 
         RR + 1 => RR
-        RR => A
         $ => B          :MLOAD(array_mul_long_len_inB)
-        $               :EQ, JMPC(array_mul_long_loop_index_check)
-                        return_array_mul_long_loop_index_check:
-                        :JMP(array_mul_long_loopZero2inB)
+        B - RR          :JMPZ(array_mul_long_loop_index_check, array_mul_long_loopZero2inB)
 
 array_mul_long_prep_trim_in:
         $ => C          :MLOAD(array_mul_long_len_out)
-        C => E
+        C - 1 => E
 
 array_mul_long_trim_in:
-        E - 1 => E
         $ => A          :MLOAD(array_mul_long_out + E)
         A               :MSTORE(array_trim_in + E)
-        E               :JMPZ(array_mul_long_trim, array_mul_long_trim_in)
+        E - 1 => E      :JMPN(array_mul_long_trim, array_mul_long_trim_in)
 
 array_mul_long_trim:
                         :CALL(array_trim)
diff --git a/main/modexp/array_lib/array_mul_short.zkasm b/main/modexp/array_lib/array_mul_short.zkasm
index c06a7a8f..506b9b6f 100644
--- a/main/modexp/array_lib/array_mul_short.zkasm
+++ b/main/modexp/array_lib/array_mul_short.zkasm
@@ -11,7 +11,7 @@
 ;;                  · out = inA·inB, with len(out) <= C + 1
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; function array_mul_short(a: bigint[], b: bigint, B: bigint): bigint[] {
+; function array_mul_short(a: bigint[], b: bigint, base: bigint): bigint[] {
 ;     const alen = a.length;
 ;     const len = alen;
 ;     const result = new Array<bigint>(len).fill(0n);
@@ -20,8 +20,8 @@
 ;     let i;
 ;     for (i = 0; i < alen; i++) {
 ;         product = a[i] * b + carry;
-;         carry = product / B;
-;         result[i] = product - carry * B;
+;         carry = product / base;
+;         out[i] = product - carry * base;
 ;     }
 
 ;     if (carry > 0n) {
@@ -43,31 +43,28 @@ VAR GLOBAL array_mul_short_carry
 VAR GLOBAL array_mul_short_RR
 
 array_mul_short:
-        %MAX_CNT_BINARY - CNT_BINARY               - 2*C  - 1   :JMPN(outOfCountersBinary)
+        %MAX_CNT_BINARY - CNT_BINARY               - 2*C        :JMPN(outOfCountersBinary)
         %MAX_CNT_ARITH - CNT_ARITH                 - C          :JMPN(outOfCountersArith)
-        %MAX_CNT_STEPS - STEP        - 6 - 3*C-3   - 18*C - 7   :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP        - 6 - 2*C-2   - 18*C - 6   :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_mul_short_RR)
+
         C               :MSTORE(array_mul_short_len_inA)
         C + 1           :MSTORE(array_mul_short_len_out)
 
-        C + 1 => E      ; auxiliar index
+        C => E          ; auxiliar index
         0 => RCX        ; index in loops
         0               :MSTORE(array_mul_short_carry)
 
 array_mul_short_clean_out:
-        E - 1 => E
         0               :MSTORE(array_mul_short_out + E)
-        E               :JMPZ(array_mul_short_loopZero2inA, array_mul_short_clean_out)
-
-; Begin of branching
-array_mul_short_add_carry:
-        D + 1 => D      :JMP(return_array_mul_short_add_carry)
-; End of branching
+        E - 1 => E      :JMPN(array_mul_short_loopZero2inA, array_mul_short_clean_out)
 
 array_mul_short_loopZero2inA:
+        ; The result will be stored as D·base + C
+
         RCX => E
-        ; product = a_i * b + carry
+        ; 1] a[i] * b, where a[i],b ∈ [0,base-1]: This number cannot be GT (base - 2)·base + 1, two chunks
         $ => A          :MLOAD(array_mul_short_inA + E)
         $ => B          :MLOAD(array_mul_short_inB)
         0 => C
@@ -75,41 +72,46 @@ array_mul_short_loopZero2inA:
         ${_arrayShortMul_AB >> 256} => D
         ${_arrayShortMul_AB} => E :ARITH
 
+        ; 2] product = a[i] * b + carry, where carry ∈ [0,base-1]: This number cannot be GT (base - 1)·base, two chunks
         E => A
         $ => B          :MLOAD(array_mul_short_carry)
-        $ => C          :ADD, JMPC(array_mul_short_add_carry)
-                        return_array_mul_short_add_carry:
+        $ => C          :ADD, JMPNC(__array_mul_short_no_carry_continue)
+        ;-----------------
+        ; Since here D ∈ [0, base - 2], there cannot be carry in the following addition
+        D => A
+        1 => B
+        $ => D          :ADD
+        ;-----------------
+                        __array_mul_short_no_carry_continue:
+
+        ; carry = product / base
         D               :MSTORE(array_mul_short_carry)
 
-        ; out[i] = product - carry·2²⁵⁶
+        ; out[i] = product - carry·base
         RCX => E
         C               :MSTORE(array_mul_short_out + E)
 
         RCX + 1 => RCX
-        RCX => A
         $ => B          :MLOAD(array_mul_short_len_inA)
-        $               :EQ, JMPC(array_mul_short_carry_check, array_mul_short_loopZero2inA)
+        B - RCX         :JMPZ(array_mul_short_carry_check, array_mul_short_loopZero2inA)
 
-; If carry > 0, we need to add it to the output
+; If the last carry > 0, we need to insert it to the output
 array_mul_short_carry_check:
-        $ => A          :MLOAD(array_mul_short_carry)
-        0 => B
-        $               :EQ, JMPC(array_mul_short_prep_trim_in)
+        $ => A          :MLOAD(array_mul_short_carry), JMPZ(array_mul_short_prep_trim_in)
 
         RCX => E
         A              :MSTORE(array_mul_short_out + E)
 
 array_mul_short_prep_trim_in:
         $ => C          :MLOAD(array_mul_short_len_out)
-        C => E
+        C - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 1   :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 1   :JMPN(outOfCountersStep)
 
 array_mul_short_trim_in:
-        E - 1 => E
         $ => A          :MLOAD(array_mul_short_out + E)
         A               :MSTORE(array_trim_in + E)
-        E               :JMPZ(array_mul_short_trim, array_mul_short_trim_in)
+        E - 1 => E      :JMPZ(array_mul_short_trim, array_mul_short_trim_in)
 
 array_mul_short_trim:
                         :CALL(array_trim)
diff --git a/main/modexp/array_lib/array_square.zkasm b/main/modexp/array_lib/array_square.zkasm
index 897d85e4..25e9a9a8 100644
--- a/main/modexp/array_lib/array_square.zkasm
+++ b/main/modexp/array_lib/array_square.zkasm
@@ -15,17 +15,13 @@
 ;     let out = new Array<bigint>(2*len).fill(0n);
 ;     let product: bigint;
 ;     let carry: bigint;
-;     let a_i: bigint;
-;     let a_j: bigint;
 ;     for (let i = 0; i < len; i++) {
-;         a_i = a[i];
-;         carry = 0n - a_i * a_i;
+;         carry = 0n - a[i] * a[i];
 ;         for (var j = i; j < len; j++) {
-;             a_j = a[j];
-;             product = 2n * (a_i * a_j) + out[i + j] + carry;
+;             product = 2n * (a[i] * a[j]) + out[i+j] + carry;
 ;             carry = product / base;
 
-;             out[i + j] = product - carry * base;
+;             out[i+j] = product - carry * base;
 ;         }
 ;         out[i + len] = carry;
 ;     }
@@ -51,7 +47,7 @@ VAR GLOBAL array_square_RR
 
 array_square:
         %MAX_CNT_ARITH - CNT_ARITH - 1        :JMPN(outOfCountersArith)
-        %MAX_CNT_STEPS - STEP      - 4        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP      - 7        :JMPN(outOfCountersStep)
 
         C => A,B
         0 => C,D
@@ -59,20 +55,20 @@ array_square:
         A => C
         ; E holds C*C
 
-        %MAX_CNT_BINARY - CNT_BINARY            - 10*E       :JMPN(outOfCountersBinary)
-        %MAX_CNT_ARITH - CNT_ARITH   - 1        - 2*E        :JMPN(outOfCountersArith)
-        %MAX_CNT_STEPS - STEP        - 14 - 3*C - 83*E - 2   :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY            -  9*E          :JMPN(outOfCountersBinary)
+        %MAX_CNT_ARITH - CNT_ARITH   - 1        -  2*E          :JMPN(outOfCountersArith)
+        %MAX_CNT_STEPS - STEP        - 5 - 2*C  - 68*E - 2      :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_square_RR)
+
         C               :MSTORE(array_square_len_in)
         C + C           :MSTORE(array_square_len_out)
 
-        0 => RCX       ; first index in loops
-        C + C => RR    ; second index in loops
+        0 => RCX,RR     ; first and second indexes in loops
+        C + C - 1 => E
 array_square_clean_out:
-        RR - 1 => RR
-        0               :MSTORE(array_square_out + RR)
-        RR              :JMPZ(array_square_ai_times_ai, array_square_clean_out)
+        0               :MSTORE(array_square_out + E)
+        E - 1 => E      :JMPN(array_square_ai_times_ai, array_square_clean_out)
 
 ; Begin of branching
 ; We perform subtraction of a value with three chunks
@@ -111,8 +107,8 @@ array_square_loop_index_check:
 ; End of branching
 
 array_square_ai_times_ai:
-        ; carry = 0 - a_i·a_i
-        ; a_i·a_i, where a_i ∈ [0,base-1]: This number cannot be GT (base - 2)·base + 1, two chunks
+        ; carry = 0 - a[i]·a[i]
+        ; a[i]·a[i], where a[i] ∈ [0,base-1]: This number cannot be GT (base - 2)·base + 1, two chunks
         $ => A,B       :MLOAD(array_square_in + RR)
         0 => C
         $${var _arraySquare_aiai = A*B}
@@ -123,10 +119,10 @@ array_square_ai_times_ai:
         0               :MSTORE(array_square_carry_sign)
 
 array_square_loopRR2len:
-        ; product = 2·(a_i·a_j) + out[i + j] + carry (in the worst case, this is a 3-chunk number)
+        ; product = 2·(a[i]·a[j]) + out[i+j] + carry (in the worst case, this is a 3-chunk number)
         ; The result will be stored as array_square_chunk_3·base² + D·base + C
 
-        ; 1] a_i·a_j, where a_i,a_j ∈ [0,base-1]: This number cannot be GT (base - 2)·base + 1, two chunks
+        ; 1] a[i]·a[j], where a[i],a[j] ∈ [0,base-1]: This number cannot be GT (base - 2)·base + 1, two chunks
         RCX => E
         $ => A          :MLOAD(array_square_in + E)
         $ => B          :MLOAD(array_square_in + RR)
@@ -136,7 +132,7 @@ array_square_loopRR2len:
         ${_arraySquare_aiaj} => E :ARITH
         D              :MSTORE(array_square_aiaj_chunk_2)
 
-        ; 2] 2·a_i·a_j: This number cannot be GT base² + (base - 4)·base + 2, three chunks
+        ; 2] 2·a[i]·a[j]: This number cannot be GT base² + (base - 4)·base + 2, three chunks
         E => A,B
         $ => C          :ADD, JMPNC(__array_square_no_carry_continue_1)
         ;-----------------
@@ -154,8 +150,8 @@ array_square_loopRR2len:
         ;-----------------
                         __array_square_no_carry_continue_2:
 
-        ; 3] 2·a_i·a_j + out[i + j]:
-        ;       a) j < len-1:  This number cannot be GT base² + (base - 3)·base + 1, as out[i + j] < base
+        ; 3] 2·a[i]·a[j] + out[i+j]:
+        ;       a) j < len-1:  This number cannot be GT base² + (base - 3)·base + 1, as out[i+j] < base
         ;       b) j == len-1: This number cannot be GT base² + (base - 3)·base + base - 1, as  out[i + len] <= base + (base - 3)
         ; In both cases, three chunks
         RCX + RR => E
@@ -184,7 +180,7 @@ array_square_loopRR2len:
         ;-----------------
                         __array_square_no_carry_continue_4:
 
-        ; 4] product = 2·a_i·a_j + out[i + j] + carry: This number cannot be GT base² + (base - 2)·base, three chunks
+        ; 4] product = 2·a[i]·a[j] + out[i+j] + carry: This number cannot be GT base² + (base - 2)·base, three chunks
         C => A
         $ => B          :MLOAD(array_square_carry_chunk_1)
         $               :MLOAD(array_square_carry_sign), JMPZ(array_square_is_negative_1)
@@ -215,26 +211,25 @@ array_square_loopRR2len:
         A               :MSTORE(array_square_carry_chunk_2)
         1               :MSTORE(array_square_carry_sign)
 
-        ; out[i + j] = product - carry·base;
+        ; out[i+j] = product - carry·base;
         RCX + RR => E
         C               :MSTORE(array_square_out + E)
         0               :MSTORE(array_square_chunk_3) ; reset the third chunk
 
-        RR + 1 => RR,A
+        RR + 1 => RR
         $ => B          :MLOAD(array_square_len_in)
-        B - A           :JMPZ(array_square_loop_index_check, array_square_loopRR2len) ; This subtraction is safe
+        B - RR          :JMPZ(array_square_loop_index_check, array_square_loopRR2len) ; This subtraction is safe
 
 array_square_prep_trim_in:
         $ => C          :MLOAD(array_square_len_out)
-        C => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 1   :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 1 - 3*C - 1   :JMPN(outOfCountersStep)
 
+        C - 1 => E
 array_square_trim_in:
-        E - 1 => E
         $ => A          :MLOAD(array_square_out + E)
         A               :MSTORE(array_trim_in + E)
-        E               :JMPZ(array_square_trim, array_square_trim_in)
+        E - 1 => E      :JMPN(array_square_trim, array_square_trim_in)
 
 array_square_trim:
                         :CALL(array_trim)
diff --git a/main/modexp/array_lib/unused/array_is_one.zkasm b/main/modexp/array_lib/unused/array_is_one.zkasm
index 81f96e99..90f86d8d 100644
--- a/main/modexp/array_lib/unused/array_is_one.zkasm
+++ b/main/modexp/array_lib/unused/array_is_one.zkasm
@@ -18,10 +18,10 @@ array_is_one:
         ; Is C == 1 and in == 1?
         C => A
         1 => B
-        $               :EQ, JMPNC(array_is_one_continue)
+        $               :EQ, JMPNC(__array_is_one_continue)
         $ => A          :MLOAD(array_is_one_in)
         $               :EQ, JMPC(array_is_one_sure)
-        array_is_one_continue:
+        __array_is_one_continue:
 
         0               :MSTORE(array_is_one_result)
                         :JMP(array_is_one_end)
diff --git a/main/modexp/array_lib/unused/array_is_zero.zkasm b/main/modexp/array_lib/unused/array_is_zero.zkasm
index fca7224d..022f310f 100644
--- a/main/modexp/array_lib/unused/array_is_zero.zkasm
+++ b/main/modexp/array_lib/unused/array_is_zero.zkasm
@@ -18,11 +18,11 @@ array_is_zero:
         ; Is C == 1 and in == 0?
         C => A
         1 => B
-        $               :EQ, JMPNC(array_is_zero_continue)
+        $               :EQ, JMPNC(__array_is_zero_continue)
         0 => B
         $ => A          :MLOAD(array_is_zero_in)
         $               :EQ, JMPC(array_is_zero_sure)
-        array_is_zero_continue:
+        __array_is_zero_continue:
 
         0               :MSTORE(array_is_zero_result)
                         :JMP(array_is_zero_end)
diff --git a/main/modexp/array_lib/utils/array_compare.zkasm b/main/modexp/array_lib/utils/array_compare.zkasm
index 292626d0..39388f56 100644
--- a/main/modexp/array_lib/utils/array_compare.zkasm
+++ b/main/modexp/array_lib/utils/array_compare.zkasm
@@ -45,22 +45,17 @@ VAR GLOBAL array_compare_result
 VAR GLOBAL array_compare_RR
 
 array_compare:
-        %MAX_CNT_BINARY - CNT_BINARY - 2 - 2*C          :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 8 - 8*C - 4      :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY     - 2*C          :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 4 - 7*C - 4      :JMPN(outOfCountersStep)
 
         RR              :MSTORE(array_compare_RR)
 
         ; Start by comparing the lengths of the arrays
-        C => A
-        D => B
-        $               :LT, JMPC(array_compare_ALTB)
-        C => B
-        D => A
-        $               :LT, JMPC(array_compare_AGTB)
+        C - D           :JMPN(array_compare_ALTB)
+        D - C           :JMPN(array_compare_AGTB)
 
-        C => E
+        C - 1 => E
 array_compare_same_len:
-        E - 1 => E
         $ => A          :MLOAD(array_compare_inA + E)
         $ => B          :MLOAD(array_compare_inB + E)
         $               :LT, JMPC(array_compare_ALTB)
@@ -69,7 +64,7 @@ array_compare_same_len:
         $ => B          :MLOAD(array_compare_inA + E)
         $               :LT, JMPC(array_compare_AGTB)
 
-        E      :JMPZ(array_compare_AEQB, array_compare_same_len)
+        E - 1 => E      :JMPN(array_compare_AEQB, array_compare_same_len)
 
 array_compare_AGTB:
         2               :MSTORE(array_compare_result)
@@ -81,7 +76,6 @@ array_compare_AEQB:
 
 array_compare_ALTB:
         0               :MSTORE(array_compare_result)
-                        :JMP(array_compare_end)
 
 array_compare_end:
         $ => RR         :MLOAD(array_compare_RR)
diff --git a/main/modexp/array_lib/utils/array_trim.zkasm b/main/modexp/array_lib/utils/array_trim.zkasm
index e0d5341f..efb9b750 100644
--- a/main/modexp/array_lib/utils/array_trim.zkasm
+++ b/main/modexp/array_lib/utils/array_trim.zkasm
@@ -23,20 +23,22 @@ VAR GLOBAL array_trim_in[%ARRAY_MAX_LEN_DOUBLED]
 VAR GLOBAL array_trim_RR
 
 array_trim:
-        %MAX_CNT_STEPS - STEP - 4       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 5       :JMPN(outOfCountersStep)
 
         RR             	:MSTORE(array_trim_RR)
 
+        0 => B ; used for comparison in the whole loop
+
         C => E
         ; scan from the last chunk to the first chunks until we find a non-zero chunk
         ; in case of zero input array, we return 1
 array_trim_loop:
         %MAX_CNT_BINARY - CNT_BINARY - 1        :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP - 6               :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3               :JMPN(outOfCountersStep)
 
         E - 1 => E      :JMPZ(array_trim_end)
+
         $ => A          :MLOAD(array_trim_in + E)
-        0 => B
         $               :EQ, JMPZ(array_trim_end, array_trim_loop)
 
 array_trim_end:
diff --git a/main/modexp/modexp.zkasm b/main/modexp/modexp.zkasm
index 77b50cc1..6491c42a 100644
--- a/main/modexp/modexp.zkasm
+++ b/main/modexp/modexp.zkasm
@@ -17,21 +17,21 @@
 ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; function modexp(b: bigint[], exp: bigint[], mod: bigint[], B: bigint): bigint[] {
+;; function modexp(b: bigint[], exp: bigint[], mod: bigint[], base: bigint): bigint[] {
 ;;     if (array_is_zero(mod) || array_is_one(mod)) return [0n];
 ;;     if (array_is_zero(b)) return [0n];
 ;;     if (array_is_one(b)) return [1n];
 ;;     if (array_is_zero(e)) return [1n];
 ;;
 ;;     let r = [1n];
-;;     let base = array_div(b, mod, B)[1];
+;;     let base = array_div(b, mod, base)[1];
 ;;     while (!array_is_zero(exp)) {
 ;;         if (array_is_zero(base)) return [0n];
 ;;         if (isOdd(exp)) {
-;;             r = array_div(array_mul(r, base, B),mod,B)[1];
+;;             r = array_div(array_mul(r, base, base),mod,base)[1];
 ;;         }
-;;         exp = array_div_short(exp, 2n, B)[0];
-;;         base = array_div(array_square(base, B),mod,B)[1];
+;;         exp = array_div_short(exp, 2n, base)[0];
+;;         base = array_div(array_square(base, base),mod,base)[1];
 ;;     }
 ;;     return r;
 ;; };
@@ -75,41 +75,38 @@ modexp:
         ; prepare for computing B % M
         $ => C          :MLOAD(modexp_Blen)
         $ => D          :MLOAD(modexp_Mlen)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*D  - 1    :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*D  - 1    :JMPN(outOfCountersStep)
 
 ; Compute B = B % M
 ; -------------------
 modexp_B_to_div:
-        RR - 1 => RR
         $ => A          :MLOAD(modexp_B + RR)
         A               :MSTORE(array_div_inA + RR)
-        RR              :JMPZ(modexp_M_to_div1, modexp_B_to_div)
+        RR - 1 => RR    :JMPN(modexp_M_to_div1, modexp_B_to_div)
 
 modexp_M_to_div1:
-        E - 1 => E
         $ => A          :MLOAD(modexp_M + E)
         A               :MSTORE(array_div_inB + E)
-        E               :JMPZ(modexp_div_B_and_M, modexp_M_to_div1)
+        E - 1 => E      :JMPN(modexp_div_B_and_M, modexp_M_to_div1)
 
 modexp_div_B_and_M:
                         :CALL(array_div)
 
-        %MAX_CNT_STEPS - STEP - 3         :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 4         :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_div_len_rem)
         C               :MSTORE(modexp_Blen)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C        :JMPN(outOfCountersStep)
 
 modexp_rem_from_div1:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_rem + RR)
         A               :MSTORE(modexp_B + RR)
-        RR              :JMPZ(modexp_pre_loop, modexp_rem_from_div1)
+        RR - 1 => RR    :JMPN(modexp_pre_loop, modexp_rem_from_div1)
 ; -------------------
 
 ; Begin of edge cases
@@ -123,92 +120,84 @@ modexp_B_is_zero:
 modexp_loop_multiply:
         $ => C          :MLOAD(modexp_outlen)
         $ => D          :MLOAD(modexp_Blen)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*D - 1        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*D - 1        :JMPN(outOfCountersStep)
 
 ; Compute out * B
 ; -------------------
 modexp_out_to_mul_long:
-        RR - 1 => RR
         $ => A          :MLOAD(modexp_out + RR)
         A               :MSTORE(array_mul_inA + RR)
-        RR              :JMPZ(modexp_B_to_mul_long, modexp_out_to_mul_long)
+        RR - 1 => RR    :JMPN(modexp_B_to_mul_long, modexp_out_to_mul_long)
 
 modexp_B_to_mul_long:
-        E - 1 => E
         $ => A          :MLOAD(modexp_B + E)
         A               :MSTORE(array_mul_inB + E)
-        E               :JMPZ(modexp_mul_long_out_and_B, modexp_B_to_mul_long)
+        E - 1 => E      :JMPN(modexp_mul_long_out_and_B, modexp_B_to_mul_long)
 
 modexp_mul_long_out_and_B:
                         :CALL(array_mul)
 
-        %MAX_CNT_STEPS - STEP - 4         :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 5         :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_mul_len_out)
         $ => D          :MLOAD(modexp_Mlen)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*D - 1        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*D - 1        :JMPN(outOfCountersStep)
 
 ; Compute out = (out * B) % M
 modexp_out_to_div1:
-        RR - 1 => RR
         $ => A          :MLOAD(array_mul_out + RR)
         A               :MSTORE(array_div_inA + RR)
-        RR              :JMPZ(modexp_M_to_div, modexp_out_to_div1)
+        RR - 1 => RR    :JMPN(modexp_M_to_div, modexp_out_to_div1)
 
 modexp_M_to_div:
-        E - 1 => E
         $ => A          :MLOAD(modexp_M + E)
         A               :MSTORE(array_div_inB + E)
-        E               :JMPZ(modexp_div_out_and_M2, modexp_M_to_div)
+        E - 1 => E      :JMPN(modexp_div_out_and_M2, modexp_M_to_div)
 
 modexp_div_out_and_M2:
                         :CALL(array_div)
 
-        %MAX_CNT_STEPS - STEP - 3        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 4        :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_div_len_rem)
         C               :MSTORE(modexp_outlen)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 1        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 1        :JMPN(outOfCountersStep)
 
 modexp_rem_from_div2:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_rem + RR)
         A               :MSTORE(modexp_out + RR)
-        RR              :JMPZ(return_modexp_loop_multiply, modexp_rem_from_div2)
+        RR - 1 => RR    :JMPN(return_modexp_loop_multiply, modexp_rem_from_div2)
 ; -------------------
 ; End of branching
 
 modexp_pre_loop:
 ;       In the worst case, the exponent is odd in each iteration
-        %MAX_CNT_BINARY - CNT_BINARY - 5          :JMPN(outOfCountersBinary)
-        %MAX_CNT_STEPS - STEP        - 21         :JMPN(outOfCountersStep)
+        %MAX_CNT_BINARY - CNT_BINARY - 3          :JMPN(outOfCountersBinary)
+        %MAX_CNT_STEPS - STEP        - 13         :JMPN(outOfCountersStep)
 
-        ; Is E = 0?
-        $ => A          :MLOAD(modexp_Elen)
+        ; Is Elen = 1 and E = 0?
         1 => B
-        $               :EQ, JMPNC(modexp_E_continue2)
+        $ => A          :MLOAD(modexp_Elen)
+        A - B           :JMPNZ(__modexp_E_continue)
         $ => A          :MLOAD(modexp_E)
-        0 => B
-        $               :EQ, JMPC(modexp_end)
-                        modexp_E_continue2:
+        $               :LT, JMPC(modexp_end) ; we are done
+                        __modexp_E_continue:
 
 modexp_loop:
-        ; Is B = 0?
+        ; Is Blen = 1 and B = 0?
         $ => A          :MLOAD(modexp_Blen)
-        1 => B
-        $               :EQ, JMPNC(modexp_B_continue3)
+        A - B           :JMPNZ(__modexp_B_continue)
         $ => A          :MLOAD(modexp_B)
-        0 => B
-        $               :EQ, JMPC(modexp_B_is_zero)
-                        modexp_B_continue3:
+        $               :LT, JMPC(modexp_B_is_zero)
+                        __modexp_B_continue:
 
         ; Is E is odd?
         ; The base is 2^256, so I only need to check if the first chunk is odd to conclude that the whole number is odd.
@@ -220,92 +209,86 @@ modexp_loop:
         %MAX_CNT_STEPS - STEP - 3        :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(modexp_Elen)
-        2               :MSTORE(array_div_short_inB)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 1        :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 2        :JMPN(outOfCountersStep)
 
 ; Compute E = E // 2
 ; -------------------
 modexp_E_to_div_short:
-        RR - 1 => RR
         $ => A          :MLOAD(modexp_E + RR)
         A               :MSTORE(array_div_short_inA + RR)
-        RR              :JMPZ(modexp_div_E_and_2, modexp_E_to_div_short)
+        RR - 1 => RR    :JMPN(modexp_div_E_and_2, modexp_E_to_div_short)
 
 modexp_div_E_and_2:
+        2               :MSTORE(array_div_short_inB)
                         :CALL(array_div_short)
 
-        %MAX_CNT_STEPS - STEP - 3       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 4       :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_div_short_len_quo)
         C               :MSTORE(modexp_Elen)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 2       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3       :JMPN(outOfCountersStep)
 
 modexp_quo_from_div_short:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_short_quo + RR)
         A               :MSTORE(modexp_E + RR)
-        RR              :JMPZ(modexp_pre_B_square, modexp_quo_from_div_short)
+        RR - 1 => RR    :JMPN(modexp_pre_B_square, modexp_quo_from_div_short)
 ; -------------------
 
 ; Compute B^2
 ; -------------------
 modexp_pre_B_square:
         $ => C          :MLOAD(modexp_Blen)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 1       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 1       :JMPN(outOfCountersStep)
 
 modexp_B_to_square1:
-        RR - 1 => RR
         $ => A          :MLOAD(modexp_B + RR)
         A               :MSTORE(array_square_in + RR)
-        RR              :JMPZ(modexp_square_B, modexp_B_to_square1)
+        RR - 1 => RR    :JMPN(modexp_square_B, modexp_B_to_square1)
 
 modexp_square_B:
                         :CALL(array_square)
 
-        %MAX_CNT_STEPS - STEP - 4       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 5       :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_square_len_out)
         $ => D          :MLOAD(modexp_Mlen)
-        C => RR
-        D => E
+        C - 1 => RR
+        D - 1 => E
 
-        %MAX_CNT_STEPS - STEP - 4*C - 4*D - 1       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 3*D - 1       :JMPN(outOfCountersStep)
 
 ; Compute B = (B^2) % M
 modexp_out_to_div2:
-        RR - 1 => RR
         $ => A          :MLOAD(array_square_out + RR)
         A               :MSTORE(array_div_inA + RR)
-        RR              :JMPZ(modexp_M_to_div2, modexp_out_to_div2)
+        RR - 1 => RR    :JMPN(modexp_M_to_div2, modexp_out_to_div2)
 
 modexp_M_to_div2:
-        E - 1 => E
         $ => A          :MLOAD(modexp_M + E)
         A               :MSTORE(array_div_inB + E)
-        E               :JMPZ(modexp_div_out_and_M1, modexp_M_to_div2)
+        E - 1 => E      :JMPN(modexp_div_out_and_M1, modexp_M_to_div2)
 
 modexp_div_out_and_M1:
                         :CALL(array_div)
 
-        %MAX_CNT_STEPS - STEP - 3       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 4       :JMPN(outOfCountersStep)
 
         $ => C          :MLOAD(array_div_len_rem)
         C               :MSTORE(modexp_Blen)
-        C => RR
+        C - 1 => RR
 
-        %MAX_CNT_STEPS - STEP - 4*C - 1       :JMPN(outOfCountersStep)
+        %MAX_CNT_STEPS - STEP - 3*C - 2       :JMPN(outOfCountersStep)
 
 modexp_rem_from_div3:
-        RR - 1 => RR
         $ => A          :MLOAD(array_div_rem + RR)
         A               :MSTORE(modexp_B + RR)
-        RR              :JMPZ(modexp_pre_loop, modexp_rem_from_div3)
+        RR - 1 => RR    :JMPN(modexp_pre_loop, modexp_rem_from_div3)
 ; -------------------
 
 modexp_end:
diff --git a/main/precompiled/pre-ecPairing.zkasm b/main/precompiled/pre-ecPairing.zkasm
index e8e47693..6bc4039f 100644
--- a/main/precompiled/pre-ecPairing.zkasm
+++ b/main/precompiled/pre-ecPairing.zkasm
@@ -7,6 +7,7 @@
  * @process-precompiled
  *  - stack input: [x1, y1, x2, y2, ..., xk, yk]
  *  - stack output: [success]
+ * @note For implementation details, see: https://hackmd.io/kcEJAWISQ56eE6YpBnurgw?view
  */
 
 funcEcPairing: