|
| 1 | +%builtins range_check |
| 2 | + |
| 3 | +// Source: https://github.com/myBraavos/efficient-secp256r1/blob/main/src/secp256r1/ec.cairo#L188 |
| 4 | + |
| 5 | +from starkware.cairo.common.cairo_secp.bigint import BigInt3, nondet_bigint3, BASE, bigint_mul, UnreducedBigInt3 |
| 6 | +from starkware.cairo.common.cairo_secp.ec import EcPoint |
| 7 | + |
| 8 | +// N = 0xffffffff00000000ffffffffffffffffbce6faada7179e84f3b9cac2fc632551 |
| 9 | +const N0 = 0x179e84f3b9cac2fc632551; |
| 10 | +const N1 = 0x3ffffffffffef39beab69c; |
| 11 | +const N2 = 0xffffffff00000000fffff; |
| 12 | + |
| 13 | +// Constants for unreduced_mul/sqr |
| 14 | +const s2 = -2**76 - 2**12; |
| 15 | +const s1 = -2**66 + 4; |
| 16 | +const s0 = 2**56; |
| 17 | + |
| 18 | +const r2 = 2**54 - 2**22; |
| 19 | +const r1 = -2**12; |
| 20 | +const r0 = 4; |
| 21 | + |
| 22 | +// SECP_REM = 2**224 - 2**192 - 2**96 + 1 |
| 23 | +const SECP_REM0 = 1; |
| 24 | +const SECP_REM1 = -2**10; |
| 25 | +const SECP_REM2 = 0xffffffff00000; |
| 26 | + |
| 27 | +func assert_165_bit{range_check_ptr}(value) { |
| 28 | + const UPPER_BOUND = 2 ** 165; |
| 29 | + const SHIFT = 2 ** 128; |
| 30 | + const HIGH_BOUND = SHIFT - UPPER_BOUND / SHIFT; |
| 31 | + |
| 32 | + let low = [range_check_ptr]; |
| 33 | + let high = [range_check_ptr + 1]; |
| 34 | + |
| 35 | + %{ |
| 36 | + from starkware.cairo.common.math_utils import as_int |
| 37 | +
|
| 38 | + # Correctness check. |
| 39 | + value = as_int(ids.value, PRIME) % PRIME |
| 40 | + assert value < ids.UPPER_BOUND, f'{value} is outside of the range [0, 2**250).' |
| 41 | +
|
| 42 | + # Calculation for the assertion. |
| 43 | + ids.high, ids.low = divmod(ids.value, ids.SHIFT) |
| 44 | + %} |
| 45 | + |
| 46 | + assert [range_check_ptr + 2] = high + HIGH_BOUND; |
| 47 | + |
| 48 | + assert value = high * SHIFT + low; |
| 49 | + |
| 50 | + let range_check_ptr = range_check_ptr + 3; |
| 51 | + return (); |
| 52 | +} |
| 53 | + |
| 54 | +func unreduced_mul(a: BigInt3, b: BigInt3) -> (res_low: UnreducedBigInt3) { |
| 55 | + tempvar twice_d2 = a.d2*b.d2; |
| 56 | + tempvar d1d2 = a.d2*b.d1 + a.d1*b.d2; |
| 57 | + return ( |
| 58 | + UnreducedBigInt3( |
| 59 | + d0=a.d0*b.d0 + s0*twice_d2 + r0*d1d2, |
| 60 | + d1=a.d1*b.d0 + a.d0*b.d1 + s1*twice_d2 + r1*d1d2, |
| 61 | + d2=a.d2*b.d0 + a.d1*b.d1 + a.d0*b.d2 + s2*twice_d2 + r2*d1d2, |
| 62 | + ), |
| 63 | + ); |
| 64 | +} |
| 65 | + |
| 66 | +func unreduced_sqr(a: BigInt3) -> (res_low: UnreducedBigInt3) { |
| 67 | + tempvar twice_d2 = a.d2*a.d2; |
| 68 | + tempvar twice_d1d2 = a.d2*a.d1 + a.d1*a.d2; |
| 69 | + tempvar d1d0 = a.d1*a.d0; |
| 70 | + return ( |
| 71 | + UnreducedBigInt3( |
| 72 | + d0=a.d0*a.d0 + s0*twice_d2 + r0*twice_d1d2, |
| 73 | + d1=d1d0 + d1d0 + s1*twice_d2 + r1*twice_d1d2, |
| 74 | + d2=a.d2*a.d0 + a.d1*a.d1 + a.d0*a.d2 + s2*twice_d2 + r2*twice_d1d2, |
| 75 | + ), |
| 76 | + ); |
| 77 | +} |
| 78 | + |
| 79 | +func verify_zero{range_check_ptr}(val: UnreducedBigInt3) { |
| 80 | + alloc_locals; |
| 81 | + local q; |
| 82 | + %{ from starkware.cairo.common.cairo_secp.secp256r1_utils import SECP256R1_P as SECP_P %} |
| 83 | + %{ |
| 84 | + from starkware.cairo.common.cairo_secp.secp_utils import pack |
| 85 | +
|
| 86 | + q, r = divmod(pack(ids.val, PRIME), SECP_P) |
| 87 | + assert r == 0, f"verify_zero: Invalid input {ids.val.d0, ids.val.d1, ids.val.d2}." |
| 88 | + ids.q = q % PRIME |
| 89 | + %} |
| 90 | +
|
| 91 | + assert_165_bit(q + 2**164); |
| 92 | + // q in [-2**164, 2**164) |
| 93 | +
|
| 94 | + tempvar r1 = (val.d0 + q * SECP_REM0) / BASE; |
| 95 | + assert_165_bit(r1 + 2**164); |
| 96 | + // r1 in [-2**164, 2**164) also meaning |
| 97 | + // numerator divides BASE which is the case when val divides secp256r1 |
| 98 | + // so r1 * BASE = val.d0 + q*SECP_REM0 in the integers |
| 99 | +
|
| 100 | + tempvar r2 = (val.d1 + q * SECP_REM1 + r1) / BASE; |
| 101 | + assert_165_bit(r2 + 2**164); |
| 102 | + // r2 in [-2**164, 2**164) following the same reasoning |
| 103 | + // so r2 * BASE = val.d1 + q*SECP_REM1 + r1 in the integers |
| 104 | + // so r2 * BASE ** 2 = val.d1 * BASE + q*SECP_REM1 * BASE + r1 * BASE |
| 105 | +
|
| 106 | + assert val.d2 + q * SECP_REM2 = q * (BASE / 4) - r2; |
| 107 | + // both lhs and rhs are in (-2**250, 2**250) so assertion valid in the integers |
| 108 | + // multiply both sides by BASE**2 |
| 109 | + // val.d2*BASE**2 + q * SECP_REM2*BASE**2 |
| 110 | + // = q * (2**256) - val.d1 * BASE + q*SECP_REM1 * BASE + val.d0 + q*SECP_REM0 |
| 111 | + // collect val on one side and all the rest on the other => |
| 112 | + // val = q*(2**256 - SECP_REM) = q * secp256r1 = 0 mod secp256r1 |
| 113 | +
|
| 114 | + return (); |
| 115 | +} |
| 116 | +
|
| 117 | +func compute_slope{range_check_ptr}(point0: EcPoint, point1: EcPoint) -> (slope: BigInt3) { |
| 118 | + %{ from starkware.cairo.common.cairo_secp.secp256r1_utils import SECP256R1_P as SECP_P %} |
| 119 | + %{ |
| 120 | + from starkware.cairo.common.cairo_secp.secp_utils import pack |
| 121 | + from starkware.python.math_utils import line_slope |
| 122 | +
|
| 123 | + # Compute the slope. |
| 124 | + x0 = pack(ids.point0.x, PRIME) |
| 125 | + y0 = pack(ids.point0.y, PRIME) |
| 126 | + x1 = pack(ids.point1.x, PRIME) |
| 127 | + y1 = pack(ids.point1.y, PRIME) |
| 128 | + value = slope = line_slope(point1=(x0, y0), point2=(x1, y1), p=SECP_P) |
| 129 | + %} |
| 130 | + let (slope) = nondet_bigint3(); |
| 131 | +
|
| 132 | + let x_diff = BigInt3( |
| 133 | + d0=point0.x.d0 - point1.x.d0, d1=point0.x.d1 - point1.x.d1, d2=point0.x.d2 - point1.x.d2 |
| 134 | + ); |
| 135 | + let (x_diff_slope: UnreducedBigInt3) = unreduced_mul(x_diff, slope); |
| 136 | + verify_zero( |
| 137 | + UnreducedBigInt3( |
| 138 | + d0=x_diff_slope.d0 - point0.y.d0 + point1.y.d0, |
| 139 | + d1=x_diff_slope.d1 - point0.y.d1 + point1.y.d1, |
| 140 | + d2=x_diff_slope.d2 - point0.y.d2 + point1.y.d2, |
| 141 | + ), |
| 142 | + ); |
| 143 | +
|
| 144 | + return (slope=slope); |
| 145 | +} |
| 146 | +
|
| 147 | +func fast_ec_add{range_check_ptr}(point0: EcPoint, point1: EcPoint) -> (res: EcPoint) { |
| 148 | + // Check whether point0 is the zero point. |
| 149 | + if (point0.x.d0 == 0) { |
| 150 | + if (point0.x.d1 == 0) { |
| 151 | + if (point0.x.d2 == 0) { |
| 152 | + return (res=point1); |
| 153 | + } |
| 154 | + } |
| 155 | + } |
| 156 | +
|
| 157 | + // Check whether point1 is the zero point. |
| 158 | + if (point1.x.d0 == 0) { |
| 159 | + if (point1.x.d1 == 0) { |
| 160 | + if (point1.x.d2 == 0) { |
| 161 | + return (res=point0); |
| 162 | + } |
| 163 | + } |
| 164 | + } |
| 165 | +
|
| 166 | + let (slope: BigInt3) = compute_slope(point0, point1); |
| 167 | + let (slope_sqr: UnreducedBigInt3) = unreduced_sqr(slope); |
| 168 | + %{ from starkware.cairo.common.cairo_secp.secp256r1_utils import SECP256R1_P as SECP_P %} |
| 169 | + // Hint #21 |
| 170 | + %{ |
| 171 | + from starkware.cairo.common.cairo_secp.secp_utils import pack |
| 172 | +
|
| 173 | + slope = pack(ids.slope, PRIME) |
| 174 | + x0 = pack(ids.point0.x, PRIME) |
| 175 | + x1 = pack(ids.point1.x, PRIME) |
| 176 | + y0 = pack(ids.point0.y, PRIME) |
| 177 | +
|
| 178 | + value = new_x = (pow(slope, 2, SECP_P) - x0 - x1) % SECP_P |
| 179 | + %} |
| 180 | + let (new_x: BigInt3) = nondet_bigint3(); |
| 181 | +
|
| 182 | + %{ value = new_y = (slope * (x0 - new_x) - y0) % SECP_P %} |
| 183 | + let (new_y: BigInt3) = nondet_bigint3(); |
| 184 | + verify_zero( |
| 185 | + UnreducedBigInt3( |
| 186 | + d0=slope_sqr.d0 - new_x.d0 - point0.x.d0 - point1.x.d0, |
| 187 | + d1=slope_sqr.d1 - new_x.d1 - point0.x.d1 - point1.x.d1, |
| 188 | + d2=slope_sqr.d2 - new_x.d2 - point0.x.d2 - point1.x.d2, |
| 189 | + ), |
| 190 | + ); |
| 191 | +
|
| 192 | + let (x_diff_slope: UnreducedBigInt3) = unreduced_mul( |
| 193 | + BigInt3(d0=point0.x.d0 - new_x.d0, d1=point0.x.d1 - new_x.d1, d2=point0.x.d2 - new_x.d2), |
| 194 | + slope, |
| 195 | + ); |
| 196 | + verify_zero( |
| 197 | + UnreducedBigInt3( |
| 198 | + d0=x_diff_slope.d0 - point0.y.d0 - new_y.d0, |
| 199 | + d1=x_diff_slope.d1 - point0.y.d1 - new_y.d1, |
| 200 | + d2=x_diff_slope.d2 - point0.y.d2 - new_y.d2, |
| 201 | + ), |
| 202 | + ); |
| 203 | +
|
| 204 | + return (res=EcPoint(new_x, new_y)); |
| 205 | +} |
| 206 | +
|
| 207 | +func main{range_check_ptr}(){ |
| 208 | + let x = BigInt3(1, 5, 10); |
| 209 | + let y = BigInt3(2, 4, 20); |
| 210 | +
|
| 211 | + let point_a = EcPoint(x, y); |
| 212 | + let point_e = EcPoint( |
| 213 | + BigInt3(55117564152931927789817182, 33048130247267262167865975, 14533608608654363688616034), |
| 214 | + BigInt3(54056253314096377704781816, 68158355584365770862343034, 3052322168655618600739346), |
| 215 | + ); |
| 216 | +
|
| 217 | + // fast_ec_add |
| 218 | + let (point_f) = fast_ec_add(point_a, point_e); |
| 219 | + assert point_f = EcPoint( |
| 220 | + BigInt3(49699015624329293412442365, 46510866771824701261167999, 1989434117861440887085793), |
| 221 | + BigInt3(214124551187530669800637, 1052132420873960207582277, 4516480956028272815500807), |
| 222 | + ); |
| 223 | +
|
| 224 | + return (); |
| 225 | +} |
0 commit comments