|
| 1 | +// SPDX-License-Identifier: MIT |
| 2 | +pragma solidity ^0.8.30; |
| 3 | + |
| 4 | +import {EllipticCurve} from "@elliptic-curve-solidity/contracts/EllipticCurve.sol"; |
| 5 | +import {Test} from "forge-std/Test.sol"; |
| 6 | + |
| 7 | +import {Delta} from "../../src/libs/proving/Delta.sol"; |
| 8 | + |
| 9 | +/** |
| 10 | + * @title EllipticCurvePropertiesTest |
| 11 | + * @dev Property-based tests for EllipticCurve.ecAdd using Foundry fuzzing. |
| 12 | + * |
| 13 | + * These tests verify GROUP PROPERTIES with points VERIFIED to be on the curve. |
| 14 | + * Points are generated via scalar multiplication: P = k × G |
| 15 | + * This guarantees all test points satisfy the curve equation y² = x³ + ax + b |
| 16 | + * |
| 17 | + * Run with: forge test -vv |
| 18 | + * Run with more fuzz runs: forge test --fuzz-runs 10000 -vv |
| 19 | + */ |
| 20 | +contract EllipticCurvePropertiesTest is Test { |
| 21 | + using EllipticCurve for *; |
| 22 | + |
| 23 | + /* GROUP PROPERTY TESTS (Points Verified On Curve) */ |
| 24 | + |
| 25 | + /// @notice GROUP PROPERTY: Commutativity - P + Q = Q + P |
| 26 | + /// @dev Uses secp256k1 with points VERIFIED to be on the curve |
| 27 | + function testGroupProperty_Commutativity_Secp256k1(uint256 scalar1, uint256 scalar2) public pure { |
| 28 | + // Generate two points on secp256k1 by scalar multiplication of G |
| 29 | + scalar1 = bound(scalar1, 1, 20); // Keep small for performance |
| 30 | + scalar2 = bound(scalar2, 1, 20); |
| 31 | + |
| 32 | + // P1 = scalar1 * G |
| 33 | + (uint256 x1, uint256 y1) = |
| 34 | + EllipticCurve.ecMul({_k: scalar1, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 35 | + |
| 36 | + // P2 = scalar2 * G |
| 37 | + (uint256 x2, uint256 y2) = |
| 38 | + EllipticCurve.ecMul({_k: scalar2, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 39 | + |
| 40 | + // Verify both points are on curve |
| 41 | + assertTrue( |
| 42 | + EllipticCurve.isOnCurve({_x: x1, _y: y1, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP}), |
| 43 | + "P1 must be on curve" |
| 44 | + ); |
| 45 | + assertTrue( |
| 46 | + EllipticCurve.isOnCurve({_x: x2, _y: y2, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP}), |
| 47 | + "P2 must be on curve" |
| 48 | + ); |
| 49 | + |
| 50 | + // Test commutativity: P1 + P2 = P2 + P1 |
| 51 | + (uint256 resultX1, uint256 resultY1) = |
| 52 | + EllipticCurve.ecAdd({_x1: x1, _y1: y1, _x2: x2, _y2: y2, _aa: Delta._AA, _pp: Delta._PP}); |
| 53 | + (uint256 resultX2, uint256 resultY2) = |
| 54 | + EllipticCurve.ecAdd({_x1: x2, _y1: y2, _x2: x1, _y2: y1, _aa: Delta._AA, _pp: Delta._PP}); |
| 55 | + |
| 56 | + assertEq(resultX1, resultX2, "GROUP PROPERTY: P + Q must equal Q + P"); |
| 57 | + assertEq(resultY1, resultY2, "GROUP PROPERTY: P + Q must equal Q + P"); |
| 58 | + } |
| 59 | + |
| 60 | + /// @notice GROUP PROPERTY: Identity - P + O = P |
| 61 | + function testGroupProperty_Identity_Secp256k1(uint256 scalar) public pure { |
| 62 | + scalar = bound(scalar, 1, 20); |
| 63 | + |
| 64 | + // P = scalar * G (guaranteed on curve) |
| 65 | + (uint256 x, uint256 y) = |
| 66 | + EllipticCurve.ecMul({_k: scalar, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 67 | + |
| 68 | + // Verify P is on curve |
| 69 | + assertTrue( |
| 70 | + EllipticCurve.isOnCurve({_x: x, _y: y, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP}), |
| 71 | + "P must be on curve" |
| 72 | + ); |
| 73 | + |
| 74 | + // P + O should equal P |
| 75 | + (uint256 resultX, uint256 resultY) = |
| 76 | + EllipticCurve.ecAdd({_x1: x, _y1: y, _x2: 0, _y2: 0, _aa: Delta._AA, _pp: Delta._PP}); |
| 77 | + |
| 78 | + assertEq(resultX, x, "GROUP PROPERTY: P + O must equal P"); |
| 79 | + assertEq(resultY, y, "GROUP PROPERTY: P + O must equal P"); |
| 80 | + } |
| 81 | + |
| 82 | + /// @notice GROUP PROPERTY: Inverse - P + (-P) = O |
| 83 | + function testGroupProperty_Inverse_Secp256k1(uint256 scalar) public pure { |
| 84 | + scalar = bound(scalar, 1, 20); |
| 85 | + |
| 86 | + // P = scalar * G (guaranteed on curve) |
| 87 | + (uint256 x, uint256 y) = |
| 88 | + EllipticCurve.ecMul({_k: scalar, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 89 | + |
| 90 | + // Verify P is on curve |
| 91 | + assertTrue( |
| 92 | + EllipticCurve.isOnCurve({_x: x, _y: y, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP}), |
| 93 | + "P must be on curve" |
| 94 | + ); |
| 95 | + |
| 96 | + // Get -P |
| 97 | + (uint256 invX, uint256 invY) = EllipticCurve.ecInv({_x: x, _y: y, _pp: Delta._PP}); |
| 98 | + |
| 99 | + // Verify -P is on curve |
| 100 | + assertTrue( |
| 101 | + EllipticCurve.isOnCurve({_x: invX, _y: invY, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP}), |
| 102 | + "-P must be on curve" |
| 103 | + ); |
| 104 | + |
| 105 | + // P + (-P) should equal O |
| 106 | + (uint256 resultX, uint256 resultY) = |
| 107 | + EllipticCurve.ecAdd({_x1: x, _y1: y, _x2: invX, _y2: invY, _aa: Delta._AA, _pp: Delta._PP}); |
| 108 | + |
| 109 | + assertTrue(_isPointAtInfinity(resultX, resultY), "GROUP PROPERTY: P + (-P) must equal point at infinity"); |
| 110 | + } |
| 111 | + |
| 112 | + /// @notice GROUP PROPERTY: Associativity - (P + Q) + R = P + (Q + R) |
| 113 | + function testGroupProperty_Associativity_Secp256k1(uint256 scalar1, uint256 scalar2, uint256 scalar3) public pure { |
| 114 | + scalar1 = bound(scalar1, 1, 10); // Keep small for performance |
| 115 | + scalar2 = bound(scalar2, 1, 10); |
| 116 | + scalar3 = bound(scalar3, 1, 10); |
| 117 | + |
| 118 | + // Generate three points on curve |
| 119 | + (uint256 x1, uint256 y1) = |
| 120 | + EllipticCurve.ecMul({_k: scalar1, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 121 | + (uint256 x2, uint256 y2) = |
| 122 | + EllipticCurve.ecMul({_k: scalar2, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 123 | + (uint256 x3, uint256 y3) = |
| 124 | + EllipticCurve.ecMul({_k: scalar3, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 125 | + |
| 126 | + // Verify all points are on curve |
| 127 | + assertTrue(EllipticCurve.isOnCurve({_x: x1, _y: y1, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP})); |
| 128 | + assertTrue(EllipticCurve.isOnCurve({_x: x2, _y: y2, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP})); |
| 129 | + assertTrue(EllipticCurve.isOnCurve({_x: x3, _y: y3, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP})); |
| 130 | + |
| 131 | + // Compute (P + Q) + R |
| 132 | + (uint256 pqX, uint256 pqY) = |
| 133 | + EllipticCurve.ecAdd({_x1: x1, _y1: y1, _x2: x2, _y2: y2, _aa: Delta._AA, _pp: Delta._PP}); |
| 134 | + (uint256 resultX1, uint256 resultY1) = |
| 135 | + EllipticCurve.ecAdd({_x1: pqX, _y1: pqY, _x2: x3, _y2: y3, _aa: Delta._AA, _pp: Delta._PP}); |
| 136 | + |
| 137 | + // Compute P + (Q + R) |
| 138 | + (uint256 qrX, uint256 qrY) = |
| 139 | + EllipticCurve.ecAdd({_x1: x2, _y1: y2, _x2: x3, _y2: y3, _aa: Delta._AA, _pp: Delta._PP}); |
| 140 | + |
| 141 | + (uint256 resultX2, uint256 resultY2) = |
| 142 | + EllipticCurve.ecAdd({_x1: x1, _y1: y1, _x2: qrX, _y2: qrY, _aa: Delta._AA, _pp: Delta._PP}); |
| 143 | + |
| 144 | + assertEq(resultX1, resultX2, "GROUP PROPERTY: Associativity must hold"); |
| 145 | + assertEq(resultY1, resultY2, "GROUP PROPERTY: Associativity must hold"); |
| 146 | + } |
| 147 | + |
| 148 | + /// @notice GROUP PROPERTY: Closure - If P, Q on curve, then P+Q on curve or at infinity |
| 149 | + function testGroupProperty_Closure_Secp256k1(uint256 scalar1, uint256 scalar2) public pure { |
| 150 | + scalar1 = bound(scalar1, 1, 20); |
| 151 | + scalar2 = bound(scalar2, 1, 20); |
| 152 | + |
| 153 | + // Generate two points on curve |
| 154 | + (uint256 x1, uint256 y1) = |
| 155 | + EllipticCurve.ecMul({_k: scalar1, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 156 | + (uint256 x2, uint256 y2) = |
| 157 | + EllipticCurve.ecMul({_k: scalar2, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 158 | + |
| 159 | + // Verify inputs are on curve |
| 160 | + assertTrue(EllipticCurve.isOnCurve({_x: x1, _y: y1, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP})); |
| 161 | + assertTrue(EllipticCurve.isOnCurve({_x: x2, _y: y2, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP})); |
| 162 | + |
| 163 | + // Add points |
| 164 | + (uint256 resultX, uint256 resultY) = |
| 165 | + EllipticCurve.ecAdd({_x1: x1, _y1: y1, _x2: x2, _y2: y2, _aa: Delta._AA, _pp: Delta._PP}); |
| 166 | + |
| 167 | + // Result must be on curve or at infinity |
| 168 | + bool atInfinity = _isPointAtInfinity(resultX, resultY); |
| 169 | + bool onCurve = |
| 170 | + EllipticCurve.isOnCurve({_x: resultX, _y: resultY, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP}); |
| 171 | + |
| 172 | + assertTrue(atInfinity || onCurve, "GROUP PROPERTY: Closure - result must be on curve or at infinity"); |
| 173 | + } |
| 174 | + |
| 175 | + /* PRECONDITION TESTS (UNREDUCED COORDINATES) */ |
| 176 | + |
| 177 | + /// @notice PRECONDITION TEST: Demonstrates correct behavior with reduced coordinates |
| 178 | + function test_Precondition_ReducedCoordinates() public pure { |
| 179 | + // Use a small prime: p = 7, curve parameter a = 2 |
| 180 | + uint256 pp = 7; |
| 181 | + uint256 aa = 2; |
| 182 | + |
| 183 | + // Point P: (3, 5), Point Q: (3, 2) where Q is inverse of P since 2 + 5 = 7 ≡ 0 (mod 7) |
| 184 | + (uint256 rx, uint256 ry) = EllipticCurve.ecAdd({_x1: 3, _y1: 5, _x2: 3, _y2: 2, _aa: aa, _pp: pp}); |
| 185 | + |
| 186 | + // P + (-P) should equal point at infinity |
| 187 | + assertTrue( |
| 188 | + _isPointAtInfinity(rx, ry), "With REDUCED coordinates: (3,5) + (3,2) correctly gives point at infinity" |
| 189 | + ); |
| 190 | + } |
| 191 | + |
| 192 | + /* CONCRETE TESTS (SECP256K1) */ |
| 193 | + |
| 194 | + /// @notice Concrete: G + G = 2G |
| 195 | + function test_Concrete_Doubling_Secp256k1() public pure { |
| 196 | + (uint256 rx, uint256 ry) = EllipticCurve.ecAdd({ |
| 197 | + _x1: Delta._GX, _y1: Delta._GY, _x2: Delta._GX, _y2: Delta._GY, _aa: Delta._AA, _pp: Delta._PP |
| 198 | + }); |
| 199 | + |
| 200 | + // Expected 2G |
| 201 | + assertEq(rx, 0xc6047f9441ed7d6d3045406e95c07cd85c778e4b8cef3ca7abac09b95c709ee5); |
| 202 | + assertEq(ry, 0x1ae168fea63dc339a3c58419466ceaeef7f632653266d0e1236431a950cfe52a); |
| 203 | + |
| 204 | + // Verify result is on curve |
| 205 | + assertTrue(EllipticCurve.isOnCurve({_x: rx, _y: ry, _aa: Delta._AA, _bb: Delta._BB, _pp: Delta._PP})); |
| 206 | + } |
| 207 | + |
| 208 | + /// @notice Concrete: G + O = G |
| 209 | + function test_Concrete_Identity_Secp256k1() public pure { |
| 210 | + (uint256 rx, uint256 ry) = |
| 211 | + EllipticCurve.ecAdd({_x1: Delta._GX, _y1: Delta._GY, _x2: 0, _y2: 0, _aa: Delta._AA, _pp: Delta._PP}); |
| 212 | + |
| 213 | + assertEq(rx, Delta._GX); |
| 214 | + assertEq(ry, Delta._GY); |
| 215 | + } |
| 216 | + |
| 217 | + /// @notice Concrete: G + (-G) = O |
| 218 | + function test_Concrete_Inverse_Secp256k1() public pure { |
| 219 | + (uint256 invX, uint256 invY) = EllipticCurve.ecInv({_x: Delta._GX, _y: Delta._GY, _pp: Delta._PP}); |
| 220 | + |
| 221 | + (uint256 rx, uint256 ry) = |
| 222 | + EllipticCurve.ecAdd({_x1: Delta._GX, _y1: Delta._GY, _x2: invX, _y2: invY, _aa: Delta._AA, _pp: Delta._PP}); |
| 223 | + |
| 224 | + assertTrue(_isPointAtInfinity(rx, ry), "G + (-G) should be point at infinity"); |
| 225 | + } |
| 226 | + |
| 227 | + /// @notice Concrete: (G + 2G) + 3G = G + (2G + 3G) = 6G |
| 228 | + function test_Concrete_Associativity_Secp256k1() public pure { |
| 229 | + // Compute 2G, 3G |
| 230 | + |
| 231 | + (uint256 p2GX, uint256 p2GY) = |
| 232 | + EllipticCurve.ecMul({_k: 2, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 233 | + (uint256 p3GX, uint256 p3GY) = |
| 234 | + EllipticCurve.ecMul({_k: 3, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 235 | + |
| 236 | + // Compute (G + 2G) + 3G |
| 237 | + (uint256 pG2GX, uint256 pG2GY) = |
| 238 | + EllipticCurve.ecAdd({_x1: Delta._GX, _y1: Delta._GY, _x2: p2GX, _y2: p2GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 239 | + (uint256 result1X, uint256 result1Y) = |
| 240 | + EllipticCurve.ecAdd({_x1: pG2GX, _y1: pG2GY, _x2: p3GX, _y2: p3GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 241 | + |
| 242 | + // Compute G + (2G + 3G) |
| 243 | + (uint256 p2G3GX, uint256 p2G3GY) = |
| 244 | + EllipticCurve.ecAdd({_x1: p2GX, _y1: p2GY, _x2: p3GX, _y2: p3GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 245 | + (uint256 result2X, uint256 result2Y) = EllipticCurve.ecAdd({ |
| 246 | + _x1: Delta._GX, _y1: Delta._GY, _x2: p2G3GX, _y2: p2G3GY, _aa: Delta._AA, _pp: Delta._PP |
| 247 | + }); |
| 248 | + |
| 249 | + // Both should equal 6G |
| 250 | + (uint256 g6x, uint256 g6y) = |
| 251 | + EllipticCurve.ecMul({_k: 6, _x: Delta._GX, _y: Delta._GY, _aa: Delta._AA, _pp: Delta._PP}); |
| 252 | + |
| 253 | + assertEq(result1X, result2X, "Associativity: (G+2G)+3G = G+(2G+3G)"); |
| 254 | + |
| 255 | + assertEq(result1Y, result2Y, "Associativity: (G+2G)+3G = G+(2G+3G)"); |
| 256 | + assertEq(result1X, g6x, "Result should be 6G"); |
| 257 | + assertEq(result1Y, g6y, "Result should be 6G"); |
| 258 | + } |
| 259 | + |
| 260 | + /// @notice Returns whether a point is at infinity or not. |
| 261 | + function _isPointAtInfinity(uint256 x, uint256 y) internal pure returns (bool isAtInfinity) { |
| 262 | + isAtInfinity = x == 0 && y == 0; |
| 263 | + } |
| 264 | +} |
0 commit comments