Merge pull request #106 from morpho-org/test/abs-certora

Add Certora verification for `abs` and `safeAbs`
morpho-org · Jun 21, 2023 · d50e424 · d50e424
2 parents 540207b + 82669d7
commit d50e424
Show file tree

Hide file tree

Showing 8 changed files with 103 additions and 59 deletions.
diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh
@@ -2,6 +2,7 @@
 
 set -euxo pipefail
 
+certora/scripts/verifyBitvectorMath.sh $@
 certora/scripts/verifyCompoundMath.sh $@
 certora/scripts/verifyMath.sh $@
 certora/scripts/verifyPercentageMath.sh $@

diff --git a/certora/scripts/verifyBitvectorMath.sh b/certora/scripts/verifyBitvectorMath.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+certoraRun \
+    test/mocks/MathMock.sol \
+    --verify MathMock:certora/specs/bitvectorMath.spec \
+    --settings -useBitVectorTheory \
+    --msg "Math" \
+    $@
diff --git a/certora/scripts/verifyMath.sh b/certora/scripts/verifyMath.sh
@@ -3,8 +3,5 @@
 certoraRun \
     test/mocks/MathMock.sol \
     --verify MathMock:certora/specs/math.spec \
-    --settings -useBitVectorTheory \
     --msg "Math" \
     $@
-
-
diff --git a/certora/specs/bitvectorMath.spec b/certora/specs/bitvectorMath.spec
@@ -0,0 +1,34 @@
+methods {
+    function min(uint256, uint256) external returns (uint256) envfree;
+    function max(uint256, uint256) external returns (uint256) envfree;
+}
+
+/// min ///
+
+rule minSafety(uint256 a, uint256 b) {
+    uint res = min(a, b);
+
+    assert a <= b => res == a;
+    assert a > b => res == b;
+}
+
+rule minLiveness(uint256 a, uint256 b) {
+    min@withrevert(a, b);
+
+    assert lastReverted <=> false;
+}
+
+/// max ///
+
+rule maxSafety(uint256 a, uint256 b) {
+    uint res = max(a, b);
+
+    assert a >= b => res == a;
+    assert a < b => res == b;
+}
+
+rule maxLiveness(uint256 a, uint256 b) {
+    max@withrevert(a, b);
+
+    assert lastReverted <=> false;
+}
diff --git a/certora/specs/compoundMath.spec b/certora/specs/compoundMath.spec
@@ -1,9 +1,9 @@
 methods {
-    function mul(uint256, uint256)   external returns (uint256)   envfree;
-    function div(uint256, uint256)   external returns (uint256)   envfree;
+    function mul(uint256, uint256) external returns (uint256) envfree;
+    function div(uint256, uint256) external returns (uint256) envfree;
 }
 
-definition WAD()  returns uint = 10^18;
+definition WAD() returns uint = 10^18;
 definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
 
 /// mul ///

diff --git a/certora/specs/math.spec b/certora/specs/math.spec
@@ -1,41 +1,45 @@
-
 methods {
-    function min(uint256, uint256)           external returns (uint256)       envfree;
-    function max(uint256, uint256)           external returns (uint256)       envfree;
-    function zeroFloorSub(uint256, uint256)  external returns (uint256)       envfree;
-    function divUp(uint256, uint256)         external returns (uint256)       envfree;
+    function abs(int256) external returns (int256) envfree;
+    function safeAbs(int256) external returns (int256) envfree;
+    function zeroFloorSub(uint256, uint256) external returns (uint256) envfree;
+    function divUp(uint256, uint256) external returns (uint256) envfree;
 }
 
-/// min ///
+definition MIN_INT256() returns int256 = -2^255;
+definition MAX_INT256() returns int256 = 2^255 - 1;
+
+/// abs ///
 
-rule minSafety(uint256 a, uint256 b) {
-    uint res = min(a, b);
+rule absSafety(int256 a) {
+    int256 res = abs(a);
 
-    assert a <= b => res == a;
-    assert a > b => res == b;
+    assert a >= 0 => res == a;
+    assert a < 0 && a > MIN_INT256() => to_mathint(res) == -a;
+    assert a == MIN_INT256() => res == MAX_INT256();
 }
 
-rule minLiveness(uint256 a, uint256 b) {
-    min@withrevert(a, b);
+rule absLiveness(int256 a) {
+    abs@withrevert(a);
 
     assert lastReverted <=> false;
 }
 
-/// max ///
+/// safeAbs ///
 
-rule maxSafety(uint256 a, uint256 b) {
-    uint res = max(a, b);
+rule safeAbsSafety(int256 a) {
+    int256 res = safeAbs(a);
 
-    assert a >= b => res == a;
-    assert a < b => res == b;
+    assert a >= 0 => res == a;
+    assert a < 0 => to_mathint(res) == -a;
 }
 
-rule maxLiveness(uint256 a, uint256 b) {
-    max@withrevert(a, b);
+rule safeAbsLiveness(int256 a) {
+    safeAbs@withrevert(a);
 
-    assert lastReverted <=> false;
+    assert lastReverted <=> a == MIN_INT256();
 }
 
+
 /// zeroFloorSub ///
 
 rule zeroFloorSubSafety(uint256 a, uint256 b) {

diff --git a/certora/specs/percentageMath.spec b/certora/specs/percentageMath.spec
@@ -1,16 +1,16 @@
 methods {
-    function percentAdd(uint256, uint256)            external returns (uint256)   envfree;
-    function percentSub(uint256, uint256)            external returns (uint256)   envfree;
-    function percentMul(uint256, uint256)            external returns (uint256)   envfree;
-    function percentMulDown(uint256, uint256)        external returns (uint256)   envfree;
-    function percentMulUp(uint256, uint256)          external returns (uint256)   envfree;
-    function percentDiv(uint256, uint256)            external returns (uint256)   envfree;
-    function percentDivDown(uint256, uint256)        external returns (uint256)   envfree;
-    function percentDivUp(uint256, uint256)          external returns (uint256)   envfree;
-    function weightedAvg(uint256, uint256, uint256)  external returns (uint256)   envfree;
-}
-
-definition PERCENTAGE_FACTOR()  returns uint = 10^4;
+    function percentAdd(uint256, uint256) external returns (uint256) envfree;
+    function percentSub(uint256, uint256) external returns (uint256) envfree;
+    function percentMul(uint256, uint256) external returns (uint256) envfree;
+    function percentMulDown(uint256, uint256) external returns (uint256) envfree;
+    function percentMulUp(uint256, uint256) external returns (uint256) envfree;
+    function percentDiv(uint256, uint256) external returns (uint256) envfree;
+    function percentDivDown(uint256, uint256) external returns (uint256) envfree;
+    function percentDivUp(uint256, uint256) external returns (uint256) envfree;
+    function weightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
+}
+
+definition PERCENTAGE_FACTOR() returns uint = 10^4;
 definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
 
 /// percentAdd ///

diff --git a/certora/specs/wadRayMath.spec b/certora/specs/wadRayMath.spec
@@ -1,25 +1,25 @@
 methods {
-    function wadMul(uint256, uint256)                   external returns (uint256)       envfree;
-    function wadMulDown(uint256, uint256)               external returns (uint256)       envfree;
-    function wadMulUp(uint256, uint256)                 external returns (uint256)       envfree;
-    function wadDiv(uint256, uint256)                   external returns (uint256)       envfree;
-    function wadDivDown(uint256, uint256)               external returns (uint256)       envfree;
-    function wadDivUp(uint256, uint256)                 external returns (uint256)       envfree;
-    function rayMul(uint256, uint256)                   external returns (uint256)       envfree;
-    function rayMulDown(uint256, uint256)               external returns (uint256)       envfree;
-    function rayMulUp(uint256, uint256)                 external returns (uint256)       envfree;
-    function rayDiv(uint256, uint256)                   external returns (uint256)       envfree;
-    function rayDivDown(uint256, uint256)               external returns (uint256)       envfree;
-    function rayDivUp(uint256, uint256)                 external returns (uint256)       envfree;
-    function rayToWad(uint256)                          external returns (uint256)       envfree;
-    function wadToRay(uint256)                          external returns (uint256)       envfree;
-    function wadWeightedAvg(uint256, uint256, uint256)  external returns (uint256)       envfree;
-    function rayWeightedAvg(uint256, uint256, uint256)  external returns (uint256)       envfree;
-}
-
-definition WAD()       returns uint = 10^18;
-definition RAY()       returns uint = 10^27;
-definition WADTORAY()  returns uint = 10^9;
+    function wadMul(uint256, uint256) external returns (uint256) envfree;
+    function wadMulDown(uint256, uint256) external returns (uint256) envfree;
+    function wadMulUp(uint256, uint256) external returns (uint256) envfree;
+    function wadDiv(uint256, uint256) external returns (uint256) envfree;
+    function wadDivDown(uint256, uint256) external returns (uint256) envfree;
+    function wadDivUp(uint256, uint256) external returns (uint256) envfree;
+    function rayMul(uint256, uint256) external returns (uint256) envfree;
+    function rayMulDown(uint256, uint256) external returns (uint256) envfree;
+    function rayMulUp(uint256, uint256) external returns (uint256) envfree;
+    function rayDiv(uint256, uint256) external returns (uint256) envfree;
+    function rayDivDown(uint256, uint256) external returns (uint256) envfree;
+    function rayDivUp(uint256, uint256) external returns (uint256) envfree;
+    function rayToWad(uint256) external returns (uint256) envfree;
+    function wadToRay(uint256) external returns (uint256) envfree;
+    function wadWeightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
+    function rayWeightedAvg(uint256, uint256, uint256) external returns (uint256) envfree;
+}
+
+definition WAD() returns uint = 10^18;
+definition RAY() returns uint = 10^27;
+definition WADTORAY() returns uint = 10^9;
 definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
 
 /// wadMul ///