Merge branch 'blake2s-hints-3' into blake2s-hints-4

Makefile

@@ -3,9 +3,8 @@
 
 CAIRO_VM_CLI:=cairo-vm/target/release/cairo-vm-cli
 
-# TODO: clone from last release
 $(CAIRO_VM_CLI):
-	git clone --depth 1 -b main https://github.com/lambdaclass/cairo-vm
+	git clone --depth 1 -b v0.9.0 https://github.com/lambdaclass/cairo-vm
 	cd cairo-vm; cargo b --release --bin cairo-vm-cli
 
 # Create proof mode programs. 

cairo_programs/div_mod_n.cairo

@@ -0,0 +1,129 @@
+%builtins range_check
+
+from starkware.cairo.common.cairo_secp.bigint import BigInt3, nondet_bigint3, BASE, bigint_mul
+from starkware.cairo.common.cairo_secp.constants import BETA, N0, N1, N2
+
+// Source: https://github.com/myBraavos/efficient-secp256r1/blob/73cca4d53730cb8b2dcf34e36c7b8f34b96b3230/src/secp256r1/signature.cairo
+
+// Computes a * b^(-1) modulo the size of the elliptic curve (N).
+//
+// Prover assumptions:
+// * All the limbs of a are in the range (-2 ** 210.99, 2 ** 210.99).
+// * All the limbs of b are in the range (-2 ** 124.99, 2 ** 124.99).
+// * b is in the range [0, 2 ** 256).
+//
+// Soundness assumptions:
+// * The limbs of a are in the range (-2 ** 249, 2 ** 249).
+// * The limbs of b are in the range (-2 ** 159.83, 2 ** 159.83).
+func div_mod_n{range_check_ptr}(a: BigInt3, b: BigInt3) -> (res: BigInt3) {
+    %{
+        from starkware.cairo.common.cairo_secp.secp_utils import N, pack
+        from starkware.python.math_utils import div_mod, safe_div
+
+        a = pack(ids.a, PRIME)
+        b = pack(ids.b, PRIME)
+        value = res = div_mod(a, b, N)
+    %}
+    let (res) = nondet_bigint3();
+
+    %{ value = k_plus_one = safe_div(res * b - a, N) + 1 %}
+    let (k_plus_one) = nondet_bigint3();
+    let k = BigInt3(d0=k_plus_one.d0 - 1, d1=k_plus_one.d1, d2=k_plus_one.d2);
+
+    let (res_b) = bigint_mul(res, b);
+    let n = BigInt3(N0, N1, N2);
+    let (k_n) = bigint_mul(k, n);
+
+    // We should now have res_b = k_n + a. Since the numbers are in unreduced form,
+    // we should handle the carry.
+
+    tempvar carry1 = (res_b.d0 - k_n.d0 - a.d0) / BASE;
+    assert [range_check_ptr + 0] = carry1 + 2 ** 127;
+
+    tempvar carry2 = (res_b.d1 - k_n.d1 - a.d1 + carry1) / BASE;
+    assert [range_check_ptr + 1] = carry2 + 2 ** 127;
+
+    tempvar carry3 = (res_b.d2 - k_n.d2 - a.d2 + carry2) / BASE;
+    assert [range_check_ptr + 2] = carry3 + 2 ** 127;
+
+    tempvar carry4 = (res_b.d3 - k_n.d3 + carry3) / BASE;
+    assert [range_check_ptr + 3] = carry4 + 2 ** 127;
+
+    assert res_b.d4 - k_n.d4 + carry4 = 0;
+
+    let range_check_ptr = range_check_ptr + 4;
+
+    return (res=res);
+}
+
+func div_mod_n_alt{range_check_ptr}(a: BigInt3, b: BigInt3) -> (res: BigInt3) {
+    // just used to import N
+    %{
+        from starkware.cairo.common.cairo_secp.secp_utils import N, pack
+        from starkware.python.math_utils import div_mod, safe_div
+
+        a = pack(ids.a, PRIME)
+        b = pack(ids.b, PRIME)
+        value = res = div_mod(a, b, N)
+    %}
+
+    %{
+        from starkware.cairo.common.cairo_secp.secp_utils import pack
+        from starkware.python.math_utils import div_mod, safe_div
+
+        a = pack(ids.a, PRIME)
+        b = pack(ids.b, PRIME)
+        value = res = div_mod(a, b, N)
+    %}
+    let (res) = nondet_bigint3();
+
+    %{ value = k_plus_one = safe_div(res * b - a, N) + 1 %}
+    let (k_plus_one) = nondet_bigint3();
+    let k = BigInt3(d0=k_plus_one.d0 - 1, d1=k_plus_one.d1, d2=k_plus_one.d2);
+
+    let (res_b) = bigint_mul(res, b);
+    let n = BigInt3(N0, N1, N2);
+    let (k_n) = bigint_mul(k, n);
+
+    tempvar carry1 = (res_b.d0 - k_n.d0 - a.d0) / BASE;
+    assert [range_check_ptr + 0] = carry1 + 2 ** 127;
+
+    tempvar carry2 = (res_b.d1 - k_n.d1 - a.d1 + carry1) / BASE;
+    assert [range_check_ptr + 1] = carry2 + 2 ** 127;
+
+    tempvar carry3 = (res_b.d2 - k_n.d2 - a.d2 + carry2) / BASE;
+    assert [range_check_ptr + 2] = carry3 + 2 ** 127;
+
+    tempvar carry4 = (res_b.d3 - k_n.d3 + carry3) / BASE;
+    assert [range_check_ptr + 3] = carry4 + 2 ** 127;
+
+    assert res_b.d4 - k_n.d4 + carry4 = 0;
+
+    let range_check_ptr = range_check_ptr + 4;
+
+    return (res=res);
+}
+
+func test_div_mod_n{range_check_ptr: felt}() {
+    let a: BigInt3 = BigInt3(100, 99, 98);
+    let b: BigInt3 = BigInt3(10, 9, 8);
+
+    let (res) = div_mod_n(a, b);
+
+    assert res = BigInt3(
+        3413472211745629263979533, 17305268010345238170172332, 11991751872105858217578135
+    );
+
+    // test alternative hint
+    let (res_alt) = div_mod_n_alt(a, b);
+
+    assert res_alt = res;
+
+    return ();
+}
+
+func main{range_check_ptr: felt}() {
+    test_div_mod_n();
+
+    return ();
+}

cairo_programs/reduce.cairo

@@ -0,0 +1,127 @@
+%builtins range_check
+
+from starkware.cairo.common.cairo_secp.bigint import BigInt3, UnreducedBigInt3, nondet_bigint3
+
+const BASE = 2 ** 86;
+const SECP_REM = 19;
+
+func verify_zero{range_check_ptr}(val: UnreducedBigInt3) {
+    let q = [ap];
+    %{
+        from starkware.cairo.common.cairo_secp.secp_utils import pack
+        SECP_P = 2**255-19
+        to_assert = pack(ids.val, PRIME)
+        q, r = divmod(pack(ids.val, PRIME), SECP_P)
+        assert r == 0, f"verify_zero: Invalid input {ids.val.d0, ids.val.d1, ids.val.d2}."
+        ids.q = q % PRIME
+    %}
+    let q_biased = [ap + 1];
+    q_biased = q + 2 ** 127, ap++;
+    [range_check_ptr] = q_biased, ap++;
+    // This implies that q is in the range [-2**127, 2**127).
+
+    tempvar r1 = (val.d0 + q * SECP_REM) / BASE;
+    assert [range_check_ptr + 1] = r1 + 2 ** 127;
+    // This implies that r1 is in the range [-2**127, 2**127).
+    // Therefore, r1 * BASE is in the range [-2**213, 2**213).
+    // By the soundness assumption, val.d0 is in the range (-2**250, 2**250).
+    // This implies that r1 * BASE = val.d0 + q * SECP_REM (as integers).
+
+    tempvar r2 = (val.d1 + r1) / BASE;
+    assert [range_check_ptr + 2] = r2 + 2 ** 127;
+    // Similarly, this implies that r2 * BASE = val.d1 + r1 (as integers).
+    // Therefore, r2 * BASE**2 = val.d1 * BASE + r1 * BASE.
+
+    assert val.d2 = q * (BASE / 8) - r2;
+    // Similarly, this implies that q * BASE / 4 = val.d2 + r2 (as integers).
+    // Therefore,
+    //   q * BASE**3 / 4 = val.d2 * BASE**2 + r2 * BASE ** 2 =
+    //   val.d2 * BASE**2 + val.d1 * BASE + r1 * BASE =
+    //   val.d2 * BASE**2 + val.d1 * BASE + val.d0 + q * SECP_REM =
+    //   val + q * SECP_REM.
+    // Hence, val = q * (BASE**3 / 4 - SECP_REM) = q * (2**256 - SECP_REM) = q * secp256k1_prime.
+
+    let range_check_ptr = range_check_ptr + 3;
+    return ();
+}
+
+// Receives an unreduced number, and returns a number that is equal to the original number mod
+// Ed25519 prime and in reduced form (meaning every limb is in the range [0, BASE)).
+//
+// Completeness assumption: x's limbs are in the range (-2**210.99, 2**210.99).
+// Soundness assumption: x's limbs are in the range (-2**249.99, 2**249.99).
+func reduce_ed25519{range_check_ptr}(x: UnreducedBigInt3) -> (reduced_x: BigInt3) {
+    %{
+        from starkware.cairo.common.cairo_secp.secp_utils import pack
+        SECP_P=2**255-19
+
+        value = pack(ids.x, PRIME) % SECP_P
+    %}
+    let (reduced_x: BigInt3) = nondet_bigint3();
+
+    verify_zero(
+        UnreducedBigInt3(d0=x.d0 - reduced_x.d0, d1=x.d1 - reduced_x.d1, d2=x.d2 - reduced_x.d2)
+    );
+    return (reduced_x=reduced_x);
+}
+
+func test_reduce_ed25519{range_check_ptr}() {
+    let x = UnreducedBigInt3(0, 0, 0);
+    let (res) = reduce_ed25519(x);
+    assert res = BigInt3(0, 0, 0);
+
+    let x = UnreducedBigInt3(
+        1113660525233188137217661511617697775365785011829423399545361443,
+        1243997169368861650657124871657865626433458458266748922940703512,
+        1484456708474143440067316914074363277495967516029110959982060577,
+    );
+    let (res) = reduce_ed25519(x);
+    assert res = BigInt3(
+        42193159084937489098474581, 19864776835133205750023223, 916662843592479469328893
+    );
+
+    return ();
+}
+
+func reduce_v2{range_check_ptr}(x: UnreducedBigInt3) -> (reduced_x: BigInt3) {
+    let orig_x = x;
+    %{ from starkware.cairo.common.cairo_secp.secp256r1_utils import SECP256R1_P as SECP_P %}
+    %{
+        from starkware.cairo.common.cairo_secp.secp_utils import pack
+        value = pack(ids.x, PRIME) % SECP_P
+    %}
+    let (reduced_x: BigInt3) = nondet_bigint3();
+
+    verify_zero(
+        UnreducedBigInt3(
+            d0=orig_x.d0 - reduced_x.d0,
+            d1=orig_x.d1 - reduced_x.d1,
+            d2=orig_x.d2 - reduced_x.d2
+        )
+    );
+    return (reduced_x=reduced_x);
+}
+
+func main{range_check_ptr}() {
+    test_reduce_ed25519();
+
+    // reduce_v2 tests
+    let x = UnreducedBigInt3(0, 0, 0);
+    let (reduce_v2_a) = reduce_v2(x);
+    assert reduce_v2_a = BigInt3(
+        0, 0, 0
+    );
+
+    let y = UnreducedBigInt3(12354, 745634534, 81298789312879123);
+    let (reduce_v2_b) = reduce_v2(y);
+    assert reduce_v2_b = BigInt3(
+        12354, 745634534, 81298789312879123
+    );
+
+    let z = UnreducedBigInt3(12354812987893128791212331231233, 7453123123123123312634534, 8129224990312325879);
+    let (reduce_v2_c) = reduce_v2(z);
+    assert reduce_v2_c = BigInt3(
+        16653320122975184709085185, 7453123123123123312794216, 8129224990312325879
+    );
+    return ();
+}

cairo_programs/signature.cairo

@@ -0,0 +1,24 @@
+%builtins range_check
+
+from starkware.cairo.common.cairo_secp.signature import div_mod_n, get_point_from_x
+from starkware.cairo.common.cairo_secp.bigint import BigInt3
+
+func main{range_check_ptr: felt}() {
+    let a: BigInt3 = BigInt3(100, 99, 98);
+    let b: BigInt3 = BigInt3(10, 9, 8);
+    let (res) = div_mod_n(a, b);
+    assert res.d0 = 3413472211745629263979533;
+    assert res.d1 = 17305268010345238170172332;
+    assert res.d2 = 11991751872105858217578135;
+
+    let x: BigInt3 = BigInt3(100, 99, 98);
+    let v: felt = 10;
+    let (point) = get_point_from_x(x, v);
+    assert point.x.d0 = 100;
+    assert point.x.d1 = 99;
+    assert point.x.d2 = 98;
+    assert point.y.d0 = 50471654703173585387369794;
+    assert point.y.d1 = 68898944762041070370364387;
+    assert point.y.d2 = 16932612780945290933872774;
+    return ();
+}