Taking back the ecrecover refactor

main/ecrecover/FNSECP256K1/invFnSecp256k1.zkasm

@@ -0,0 +1,33 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A is not alias-free
+;; POST: The result B is not alias-free (on MAP)
+;;
+;; invFnSecp256k1:
+;;             in: A
+;;             out: B = A⁻¹ (mod n)
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   2 ariths + 9 steps
+
+VAR GLOBAL invFnSecp256k1_tmp
+
+invFnSecp256k1:
+
+        ; 1] Compute and check the inverse over Z
+        ; A·A⁻¹ + 0 = [D]·2²⁵⁶ + [E]
+        0 => C
+        ${var _invFnSecp256k1_A = inverseFnEc(A)} => B :MSTORE(invFnSecp256k1_tmp)
+        $${var _invFnSecp256k1_AB = A * _invFnSecp256k1_A}
+        ${_invFnSecp256k1_AB >> 256} => D
+        ${_invFnSecp256k1_AB} => E :ARITH
+
+        ; 2] Check it over Fn, that is, it must be satisfied that:
+        ; n·[(A·A⁻¹) / n] + 1 = D·2²⁵⁶ + E
+        %SECP256K1_N => A
+        ${_invFnSecp256k1_AB / const.SECP256K1_N} => B
+        1 => C
+        E :ARITH
+
+        $ => B   :MLOAD(invFnSecp256k1_tmp), RETURN

main/ecrecover/FNSECP256K1/mulFnSecp256k1.zkasm

@@ -0,0 +1,28 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A,B are not alias-free
+;; POST: The result C is not alias-free (on MAP)
+;;
+;; mulFnSecp256k1:
+;;             in: A,B
+;;             out: C = A·B (mod n)
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   2 arith + 7 steps
+
+mulFnSecp256k1:
+
+        ; 1] Compute and check the multiplication over Z
+        ; A·B + 0 = [D]·2²⁵⁶ + [E]
+        0 => C
+        $${var _mulFnSecp256k1_AB = A * B}
+        ${_mulFnSecp256k1_AB >> 256} => D
+        ${_mulFnSecp256k1_AB} => E :ARITH
+
+        ; 2] Check it over Fn, that is, it must be satisfied that:
+        ; n·[(A·B) / n] + [(A·B) % n] = D·2²⁵⁶ + E
+        %SECP256K1_N => A
+        ${_mulFnSecp256k1_AB / const.SECP256K1_N} => B        ; quotient (256 bits)
+        ${_mulFnSecp256k1_AB % const.SECP256K1_N} => C        ; residue  (256 bits)
+        E :ARITH, RETURN

main/ecrecover/FPSECP256K1/addFpSecp256k1.zkasm

@@ -0,0 +1,29 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PRE: A,C are not alias-free
+;; POST: The result C is not alias-free (on MAP)
+;;
+;; addFpSecp256k1:
+;;             in: A,C
+;;             out: C = A + C (mod p)
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+; RESOURCES:
+;   2 ariths + 7 steps
+
+addFpSecp256k1:
+
+        ; 1] Compute and check the sum over Z
+        ; A·[1] + C = [D]·2²⁵⁶ + [E]
+        1 => B
+        $${var _addFpSecp256k1_AC = A + C}
+        ${_addFpSecp256k1_AC >> 256} => D
+        ${_addFpSecp256k1_AC} => E :ARITH
+
+        ; 2] Check it over Fp, that is, it must be satisfied that:
+        ; p·[(A+C) / p] + [(A+C) % p] = D·2²⁵⁶ + E
+        %SECP256K1_P => A
+        ${_addFpSecp256k1_AC / const.SECP256K1_P} => B        ; quotient  (256 bits)
+        ${_addFpSecp256k1_AC % const.SECP256K1_P} => C        ; residue (256 bits)
+
+        E :ARITH, RETURN