Merge pull request #115 from morpho-org/certora/update-script

morpho-org · Aug 13, 2023 · 8ddb14e · 8ddb14e
2 parents d50e424 + 65cd0ca
commit 8ddb14e
Show file tree

Hide file tree

Showing 10 changed files with 41 additions and 40 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -2,6 +2,10 @@ name: Certora
 
 on:
   push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
 
 jobs:
   verify:

diff --git a/certora/scripts/verifyAll.sh b/certora/scripts/verifyAll.sh
@@ -2,8 +2,8 @@
 
 set -euxo pipefail
 
-certora/scripts/verifyBitvectorMath.sh $@
-certora/scripts/verifyCompoundMath.sh $@
-certora/scripts/verifyMath.sh $@
-certora/scripts/verifyPercentageMath.sh $@
-certora/scripts/verifyWadRayMath.sh $@
+certora/scripts/verifyBitvectorMath.sh "$@"
+certora/scripts/verifyCompoundMath.sh "$@"
+certora/scripts/verifyMath.sh "$@"
+certora/scripts/verifyPercentageMath.sh "$@"
+certora/scripts/verifyWadRayMath.sh "$@"
diff --git a/certora/scripts/verifyBitvectorMath.sh b/certora/scripts/verifyBitvectorMath.sh
@@ -3,6 +3,6 @@
 certoraRun \
     test/mocks/MathMock.sol \
     --verify MathMock:certora/specs/bitvectorMath.spec \
-    --settings -useBitVectorTheory \
+    --prover_args "-useBitVectorTheory" \
     --msg "Math" \
-    $@
+    "$@"
diff --git a/certora/scripts/verifyCompoundMath.sh b/certora/scripts/verifyCompoundMath.sh
@@ -4,4 +4,4 @@ certoraRun \
     test/mocks/CompoundMathMock.sol \
     --verify CompoundMathMock:certora/specs/compoundMath.spec \
     --msg "CompoundMath" \
-    $@
+    "$@"
diff --git a/certora/scripts/verifyMath.sh b/certora/scripts/verifyMath.sh
@@ -4,4 +4,4 @@ certoraRun \
     test/mocks/MathMock.sol \
     --verify MathMock:certora/specs/math.spec \
     --msg "Math" \
-    $@
+    "$@"
diff --git a/certora/scripts/verifyPercentageMath.sh b/certora/scripts/verifyPercentageMath.sh
@@ -4,4 +4,4 @@ certoraRun \
     test/mocks/PercentageMathMock.sol \
     --verify PercentageMathMock:certora/specs/percentageMath.spec \
     --msg "PercentageMath" \
-    $@
+    "$@"
diff --git a/certora/scripts/verifyWadRayMath.sh b/certora/scripts/verifyWadRayMath.sh
@@ -4,4 +4,4 @@ certoraRun \
     test/mocks/WadRayMathMock.sol \
     --verify WadRayMathMock:certora/specs/wadRayMath.spec \
     --msg "WadRayMath" \
-    $@
+    "$@"
diff --git a/certora/specs/compoundMath.spec b/certora/specs/compoundMath.spec
@@ -4,7 +4,6 @@ methods {
 }
 
 definition WAD() returns uint = 10^18;
-definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
 
 /// mul ///
 
@@ -17,7 +16,7 @@ rule mulSafety(uint256 x, uint256 y) {
 rule mulLiveness(uint256 x, uint256 y) {
     mul@withrevert(x, y);
 
-    assert lastReverted <=> x * y >= UINT_LIMIT();
+    assert lastReverted <=> x * y >= 2^256;
 }
 
 /// div ///
@@ -31,5 +30,5 @@ rule divSafety(uint256 x, uint256 y) {
 rule divLiveness(uint256 x, uint256 y) {
     div@withrevert(x, y);
 
-    assert lastReverted <=> x * WAD() >= UINT_LIMIT() || y == 0;
+    assert lastReverted <=> x * WAD() >= 2^256 || y == 0;
 }
diff --git a/certora/specs/percentageMath.spec b/certora/specs/percentageMath.spec
@@ -11,7 +11,6 @@ methods {
 }
 
 definition PERCENTAGE_FACTOR() returns uint = 10^4;
-definition UINT_LIMIT() returns mathint = 2 ^ 255 * 2;
 
 /// percentAdd ///
 
@@ -25,7 +24,7 @@ rule percentAddLiveness(uint256 x, uint256 p) {
     percentAdd@withrevert(x, p);
 
     // The first condition does not imply the second one because x can be zero.
-    assert lastReverted <=> PERCENTAGE_FACTOR() + p >= UINT_LIMIT() || x * (PERCENTAGE_FACTOR() + p) + PERCENTAGE_FACTOR() / 2 >= UINT_LIMIT();
+    assert lastReverted <=> PERCENTAGE_FACTOR() + p >= 2^256 || x * (PERCENTAGE_FACTOR() + p) + PERCENTAGE_FACTOR() / 2 >= 2^256;
 }
 
 /// percentSub ///
@@ -39,7 +38,7 @@ rule percentSubSafety(uint256 x, uint256 p) {
 rule percentSubLiveness(uint256 x, uint256 p) {
     percentSub@withrevert(x, p);
 
-    assert lastReverted <=> x * (PERCENTAGE_FACTOR() - p) + PERCENTAGE_FACTOR() / 2 >= UINT_LIMIT() || p > PERCENTAGE_FACTOR();
+    assert lastReverted <=> x * (PERCENTAGE_FACTOR() - p) + PERCENTAGE_FACTOR() / 2 >= 2^256 || p > PERCENTAGE_FACTOR();
 }
 
 /// percentMul ///
@@ -53,7 +52,7 @@ rule percentMulSafety(uint256 x, uint256 p) {
 rule percentMulLiveness(uint256 x, uint256 p) {
     percentMul@withrevert(x, p);
 
-    assert lastReverted <=> x * p + PERCENTAGE_FACTOR() / 2 >= UINT_LIMIT();
+    assert lastReverted <=> x * p + PERCENTAGE_FACTOR() / 2 >= 2^256;
 }
 
 /// percentMulDown ///
@@ -67,7 +66,7 @@ rule percentMulDownSafety(uint256 a, uint256 p) {
 rule percentMulDownLiveness(uint256 a, uint256 p) {
     percentMulDown@withrevert(a, p);
 
-    assert lastReverted <=> a * p >= UINT_LIMIT();
+    assert lastReverted <=> a * p >= 2^256;
 }
 
 /// percentMulUp ///
@@ -81,7 +80,7 @@ rule percentMulUpSafety(uint256 a, uint256 p) {
 rule percentMulUpLiveness(uint256 a, uint256 p) {
     percentMulUp@withrevert(a, p);
 
-    assert lastReverted <=> a * p + PERCENTAGE_FACTOR() - 1 >= UINT_LIMIT();
+    assert lastReverted <=> a * p + PERCENTAGE_FACTOR() - 1 >= 2^256;
 }
 
 /// percentDiv ///
@@ -95,7 +94,7 @@ rule percentDivSafety(uint256 x, uint256 p) {
 rule percentDivLiveness(uint256 x, uint256 p) {
     percentDiv@withrevert(x, p);
 
-    assert lastReverted <=> x * PERCENTAGE_FACTOR() + p / 2 >= UINT_LIMIT() || p == 0;
+    assert lastReverted <=> x * PERCENTAGE_FACTOR() + p / 2 >= 2^256 || p == 0;
 }
 
 /// percentDivDown ///
@@ -109,7 +108,7 @@ rule percentDivDownSafety(uint256 a, uint256 p) {
 rule percentDivDownLiveness(uint256 a, uint256 p) {
     percentDivDown@withrevert(a, p);
 
-    assert lastReverted <=> a * PERCENTAGE_FACTOR() >= UINT_LIMIT() || p == 0;
+    assert lastReverted <=> a * PERCENTAGE_FACTOR() >= 2^256 || p == 0;
 }
 
 /// percentDivUp ///
@@ -123,7 +122,7 @@ rule percentDivUpSafety(uint256 a, uint256 p) {
 rule percentDivUpLiveness(uint256 a, uint256 p) {
     percentDivUp@withrevert(a, p);
 
-    assert lastReverted <=> a * PERCENTAGE_FACTOR() + (p - 1) >= UINT_LIMIT() || p == 0;
+    assert lastReverted <=> a * PERCENTAGE_FACTOR() + (p - 1) >= 2^256 || p == 0;
 }
 
 /// weightedAvg ///
@@ -137,5 +136,5 @@ rule weightedAvgSafety(uint256 x, uint256 y, uint256 p) {
 rule weightedAvgLiveness(uint256 x, uint256 y, uint256 p) {
     weightedAvg@withrevert(x, y, p);
 
-    assert lastReverted <=> x * (PERCENTAGE_FACTOR() - p) + y * p + PERCENTAGE_FACTOR() / 2 >= UINT_LIMIT() || p > PERCENTAGE_FACTOR();
+    assert lastReverted <=> x * (PERCENTAGE_FACTOR() - p) + y * p + PERCENTAGE_FACTOR() / 2 >= 2^256 || p > PERCENTAGE_FACTOR();
 }
diff --git a/certora/specs/wadRayMath.spec b/certora/specs/wadRayMath.spec
@@ -20,7 +20,6 @@ methods {
 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 ///
 
@@ -33,7 +32,7 @@ rule wadMulSafety(uint256 a, uint256 b) {
 rule wadMulLiveness(uint256 a, uint256 b) {
     wadMul@withrevert(a, b);
 
-    assert lastReverted <=> a * b + WAD() / 2 >= UINT_LIMIT();
+    assert lastReverted <=> a * b + WAD() / 2 >= 2^256;
 }
 
 /// wadMulDown ///
@@ -47,7 +46,7 @@ rule wadMulDownSafety(uint256 a, uint256 b) {
 rule wadMulDownLiveness(uint256 a, uint256 b) {
     wadMulDown@withrevert(a, b);
 
-    assert lastReverted <=> a * b >= UINT_LIMIT();
+    assert lastReverted <=> a * b >= 2^256;
 }
 
 /// wadMulUp ///
@@ -61,7 +60,7 @@ rule wadMulUpSafety(uint256 a, uint256 b) {
 rule wadMulUpLiveness(uint256 a, uint256 b) {
     wadMulUp@withrevert(a, b);
 
-    assert lastReverted <=> a * b + WAD() - 1 >= UINT_LIMIT();
+    assert lastReverted <=> a * b + WAD() - 1 >= 2^256;
 }
 
 /// wadDiv ///
@@ -75,7 +74,7 @@ rule wadDivSafety(uint256 a, uint256 b) {
 rule wadDivLiveness(uint256 a, uint256 b) {
     wadDiv@withrevert(a, b);
 
-    assert lastReverted <=> a * WAD() + b / 2 >= UINT_LIMIT() || b == 0;
+    assert lastReverted <=> a * WAD() + b / 2 >= 2^256 || b == 0;
 }
 
 /// wadDivDown ///
@@ -89,7 +88,7 @@ rule wadDivDownSafety(uint256 a, uint256 b) {
 rule wadDivDownLiveness(uint256 a, uint256 b) {
     wadDivDown@withrevert(a, b);
 
-    assert lastReverted <=> a * WAD() >= UINT_LIMIT() || b == 0;
+    assert lastReverted <=> a * WAD() >= 2^256 || b == 0;
 }
 
 /// wadDivUp ///
@@ -103,7 +102,7 @@ rule wadDivUpSafety(uint256 a, uint256 b) {
 rule wadDivUpLiveness(uint256 a, uint256 b) {
     wadDivUp@withrevert(a, b);
 
-    assert lastReverted <=> a * WAD() + (b - 1) >= UINT_LIMIT() || b == 0;
+    assert lastReverted <=> a * WAD() + (b - 1) >= 2^256 || b == 0;
 }
 
 /// rayMul ///
@@ -117,7 +116,7 @@ rule rayMulSafety(uint256 a, uint256 b) {
 rule rayMulLiveness(uint256 a, uint256 b) {
     rayMul@withrevert(a, b);
 
-    assert lastReverted <=> a * b + RAY() / 2 >= UINT_LIMIT();
+    assert lastReverted <=> a * b + RAY() / 2 >= 2^256;
 }
 
 /// rayMulDown ///
@@ -131,7 +130,7 @@ rule rayMulDownSafety(uint256 a, uint256 b) {
 rule rayMulDownLiveness(uint256 a, uint256 b) {
     rayMulDown@withrevert(a, b);
 
-    assert lastReverted <=> a * b >= UINT_LIMIT();
+    assert lastReverted <=> a * b >= 2^256;
 }
 
 /// rayMulUp ///
@@ -145,7 +144,7 @@ rule rayMulUpSafety(uint256 a, uint256 b) {
 rule rayMulUpLiveness(uint256 a, uint256 b) {
     rayMulUp@withrevert(a, b);
 
-    assert lastReverted <=> a * b + RAY() - 1 >= UINT_LIMIT();
+    assert lastReverted <=> a * b + RAY() - 1 >= 2^256;
 }
 
 /// rayDiv ///
@@ -159,7 +158,7 @@ rule rayDivSafety(uint256 a, uint256 b) {
 rule rayDivLiveness(uint256 a, uint256 b) {
     rayDiv@withrevert(a, b);
 
-    assert lastReverted <=> a * RAY() + b / 2 >= UINT_LIMIT() || b == 0;
+    assert lastReverted <=> a * RAY() + b / 2 >= 2^256 || b == 0;
 }
 
 /// rayDivDown ///
@@ -173,7 +172,7 @@ rule rayDivDownSafety(uint256 a, uint256 b) {
 rule rayDivDownLiveness(uint256 a, uint256 b) {
     rayDivDown@withrevert(a, b);
 
-    assert lastReverted <=> a * RAY() >= UINT_LIMIT() || b == 0;
+    assert lastReverted <=> a * RAY() >= 2^256 || b == 0;
 }
 
 /// rayDivUp ///
@@ -187,7 +186,7 @@ rule rayDivUpSafety(uint256 a, uint256 b) {
 rule rayDivUpLiveness(uint256 a, uint256 b) {
     rayDivUp@withrevert(a, b);
 
-    assert lastReverted <=> a * RAY() + (b - 1) >= UINT_LIMIT() || b == 0;
+    assert lastReverted <=> a * RAY() + (b - 1) >= 2^256 || b == 0;
 }
 
 /// rayToWad ///
@@ -215,7 +214,7 @@ rule wadToRaySafety(uint256 a) {
 rule wadToRayLiveness(uint256 a) {
     wadToRay@withrevert(a);
 
-    assert lastReverted <=> a * WADTORAY() >= UINT_LIMIT();
+    assert lastReverted <=> a * WADTORAY() >= 2^256;
 }
 
 /// wadWeightedAvg ///
@@ -229,7 +228,7 @@ rule wadWeightedAvgSafety(uint256 x, uint256 y, uint256 w) {
 rule wadWeightedAvgLiveness(uint256 x, uint256 y, uint256 w) {
     wadWeightedAvg@withrevert(x, y, w);
 
-    assert lastReverted <=> x * (WAD() - w) + y * w + WAD() / 2 >= UINT_LIMIT() || w > WAD();
+    assert lastReverted <=> x * (WAD() - w) + y * w + WAD() / 2 >= 2^256 || w > WAD();
 }
 
 /// rayWeightedAvg ///
@@ -243,5 +242,5 @@ rule rayWeightedAvgSafety(uint256 x, uint256 y, uint256 w) {
 rule rayWeightedAvgLiveness(uint256 x, uint256 y, uint256 w) {
     rayWeightedAvg@withrevert(x, y, w);
 
-    assert lastReverted <=> x * (RAY() - w) + y * w + RAY() / 2 >= UINT_LIMIT() || w > RAY();
+    assert lastReverted <=> x * (RAY() - w) + y * w + RAY() / 2 >= 2^256 || w > RAY();
 }