another

oxen-io · Dec 20, 2023 · fd2d409 · fd2d409
1 parent 94cbc53
commit fd2d409
Show file tree

Hide file tree

Showing 2 changed files with 54 additions and 8 deletions.
diff --git a/contracts/test/BN256G2EchidnaTest.sol b/contracts/test/BN256G2EchidnaTest.sol
@@ -30,16 +30,62 @@ contract BN256G2EchidnaTest {
         /*assert(BN256G2.IsOnCurve(mulXx, mulXy, mulYx, mulYy));*/
     /*}*/
 
-    bytes private message;
-    BN256G2.G2Point Hm;
+    bytes private message1;
+    BN256G2.G2Point Hm1;
+    bytes private message2;
+    BN256G2.G2Point Hm2;
+    uint256 scalar;
 
-    function setMessage(bytes calldata _message) public {
-        message = _message;
-		Hm = BN256G2.hashToG2(BN256G2.hashToField(string(message)));
+    constructor() {
+        message1 = bytes("1");
+        Hm1 = BN256G2.hashToG2(BN256G2.hashToField(string(message1)));
+        message2 = bytes("2");
+        Hm2 = BN256G2.hashToG2(BN256G2.hashToField(string(message2)));
+        scalar = 1;
     }
 
-    function echidna_always_hashable() public returns (bool) {
-        return BN256G2.IsOnCurve(Hm.X[1], Hm.X[0], Hm.Y[1], Hm.Y[0]);
+    function setMessage1(bytes calldata _message) public {
+        message1 = _message;
+        Hm1 = BN256G2.hashToG2(BN256G2.hashToField(string(message1)));
+    }
+
+    function setMessage2(bytes calldata _message) public {
+        message2 = _message;
+        Hm2 = BN256G2.hashToG2(BN256G2.hashToField(string(message2)));
+    }
+
+    function setScalar(uint256 _scalar) public {
+        scalar = _scalar;
+    }
+
+    function echidna_always_hashable1() public returns (bool) {
+        return BN256G2.IsOnCurve(Hm1.X[1], Hm1.X[0], Hm1.Y[1], Hm1.Y[0]);
+    }
+
+    function echidna_always_hashable2() public returns (bool) {
+        return BN256G2.IsOnCurve(Hm2.X[1], Hm2.X[0], Hm2.Y[1], Hm2.Y[0]);
+    }
+
+    function echidna_always_addable() public returns (bool) {
+        (uint256 sumXx, uint256 sumXy, uint256 sumYx, uint256 sumYy) = BN256G2.ECTwistAdd(
+            Hm1.X[1], Hm1.X[0], Hm1.Y[1], Hm1.Y[0],
+            Hm2.X[1], Hm2.X[0], Hm2.Y[1], Hm2.Y[0]
+        );
+        return BN256G2.IsOnCurve(sumXx, sumXy, sumYx, sumYy);
+    }
+
+    function echidna_always_multiplyable1() public returns (bool) {
+        (uint256 mulXx, uint256 mulXy, uint256 mulYx, uint256 mulYy) = BN256G2.ECTwistMul(
+            scalar, Hm1.X[1], Hm1.X[0], Hm1.Y[1], Hm1.Y[0]
+        );
+        return BN256G2.IsOnCurve(mulXx, mulXy, mulYx, mulYy);
+    }
+
+    function echidna_always_multiplyable2() public returns (bool) {
+        (uint256 mulXx, uint256 mulXy, uint256 mulYx, uint256 mulYy) = BN256G2.ECTwistMul(
+            scalar, Hm2.X[1], Hm2.X[0], Hm2.Y[1], Hm2.Y[0]
+        );
+        return BN256G2.IsOnCurve(mulXx, mulXy, mulYx, mulYy);
     }
 }
 
diff --git a/echidna.config.yml b/echidna.config.yml
@@ -14,7 +14,7 @@ testMaxGas: 8000030
 #maxGasprice is the maximum gas price
 maxGasprice: 0
 #testLimit is the number of test sequences to run
-testLimit: 50000
+testLimit: 10000
 #stopOnFail makes echidna terminate as soon as any property fails and has been shrunk
 stopOnFail: false
 #estimateGas makes echidna perform analysis of maximum gas costs for functions (experimental)