update harness and matrix

.github/workflows/formal-verifiation.yml

@@ -47,9 +47,18 @@ jobs:
           echo 'file:' ${{ matrix.params.file }}
           echo 'name:' ${{ matrix.params.name }}
           echo 'spec:' ${{ matrix.params.spec }}
+          echo 'args:' ${{ matrix.params.args || '' }}
+
           touch certora/applyHarness.patch
           make -C certora munged
-          certoraRun ${{ matrix.params.file }} --verify ${{ matrix.params.name }}:${{ matrix.params.spec }} --solc solc --optimistic_loop --loop_iter 3 --rule_sanity advanced --cloud
+
+          certoraRun ${{ matrix.params.file }} \
+            --verify ${{ matrix.params.name }}:${{ matrix.params.spec }} \
+            --solc solc \
+            --optimistic_loop
+            --loop_iter 3 \
+            --cloud \
+            ${{ matrix.params.args || '' }}
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
     strategy:

certora/applyHarness.patch

@@ -1016,85 +1016,3 @@ diff -ruN utils/Address.sol utils/Address.sol
          require(address(this).balance >= value, "Address: insufficient balance for call");
          (bool success, bytes memory returndata) = target.call{value: value}(data);
          return verifyCallResultFromTarget(target, success, returndata, errorMessage);
-diff -ruN utils/math/Math.sol utils/math/Math.sol
---- utils/math/Math.sol	2022-09-20 14:24:58.016740934 +0200
-+++ utils/math/Math.sol	2022-09-20 14:34:29.036665098 +0200
-@@ -342,4 +342,78 @@
-             return result + (rounding == Rounding.Up && 1 << (result * 8) < value ? 1 : 0);
-         }
-     }
-+
-+    /**
-+     * @dev Returns the square root of a number. It the number is not a perfect square, the value is rounded down.
-+     *
-+     * Inspired by Henry S. Warren, Jr.'s "Hacker's Delight" (Chapter 11).
-+     */
-+    function sqrt(uint256 a) internal pure returns (uint256) {
-+        if (a == 0) {
-+            return 0;
-+        }
-+
-+        // For our first guess, we get the biggest power of 2 which is smaller than the square root of the target.
-+        // We know that the "msb" (most significant bit) of our target number `a` is a power of 2 such that we have
-+        // `msb(a) <= a < 2*msb(a)`.
-+        // We also know that `k`, the position of the most significant bit, is such that `msb(a) = 2**k`.
-+        // This gives `2**k < a <= 2**(k+1)` → `2**(k/2) <= sqrt(a) < 2 ** (k/2+1)`.
-+        // Using an algorithm similar to the msb conmputation, we are able to compute `result = 2**(k/2)` which is a
-+        // good first aproximation of `sqrt(a)` with at least 1 correct bit.
-+        uint256 result = 1;
-+        uint256 x = a;
-+        if (x >> 128 > 0) {
-+            x >>= 128;
-+            result <<= 64;
-+        }
-+        if (x >> 64 > 0) {
-+            x >>= 64;
-+            result <<= 32;
-+        }
-+        if (x >> 32 > 0) {
-+            x >>= 32;
-+            result <<= 16;
-+        }
-+        if (x >> 16 > 0) {
-+            x >>= 16;
-+            result <<= 8;
-+        }
-+        if (x >> 8 > 0) {
-+            x >>= 8;
-+            result <<= 4;
-+        }
-+        if (x >> 4 > 0) {
-+            x >>= 4;
-+            result <<= 2;
-+        }
-+        if (x >> 2 > 0) {
-+            result <<= 1;
-+        }
-+
-+        // At this point `result` is an estimation with one bit of precision. We know the true value is a uint128,
-+        // since it is the square root of a uint256. Newton's method converges quadratically (precision doubles at
-+        // every iteration). We thus need at most 7 iteration to turn our partial result with one bit of precision
-+        // into the expected uint128 result.
-+        unchecked {
-+            result = (result + a / result) >> 1;
-+            result = (result + a / result) >> 1;
-+            result = (result + a / result) >> 1;
-+            result = (result + a / result) >> 1;
-+            result = (result + a / result) >> 1;
-+            result = (result + a / result) >> 1;
-+            result = (result + a / result) >> 1;
-+            return min(result, a / result);
-+        }
-+    }
-+
-+    /**
-+     * @notice Calculates sqrt(a), following the selected rounding direction.
-+     */
-+    function sqrt(uint256 a, Rounding rounding) internal pure returns (uint256) {
-+        uint256 result = sqrt(a);
-+        if (rounding == Rounding.Up && result * result < a) {
-+            result += 1;
-+        }
-+        return result;
-+    }
- }

certora/matrix.json

@@ -6,10 +6,6 @@
     "file": "certora/harnesses/ERC1155/ERC1155BurnableHarness.sol",
     "name": "ERC1155BurnableHarness",
     "spec": "certora/specs/ERC1155Burnable.spec"
-},{
-    "file": "certora/harnesses/ERC1155/ERC1155BurnableHarness.sol",
-    "name": "ERC1155BurnableHarness",
-    "spec": "certora/specs/ERC1155Burnable.spec"
 },{
     "file": "certora/harnesses/ERC1155/ERC1155PausableHarness.sol",
     "name": "ERC1155PausableHarness",
@@ -19,12 +15,15 @@
     "name": "ERC1155SupplyHarness",
     "spec": "certora/specs/ERC1155Supply.spec"
 },{
+    "disabled": true,
     "file": "certora/harnesses/ERC721VotesHarness.sol certora/munged/governance/TimelockController.sol certora/harnesses/GovernorPreventLateQuorumHarness.sol",
     "name": "GovernorPreventLateQuorumHarness",
-    "spec": "certora/specs/GovernorPreventLateQuorum.spec"
+    "spec": "certora/specs/GovernorPreventLateQuorum.spec",
+    "args": "--rule_sanity advanced"
 },{
     "disabled": true,
     "file": "certora/harnesses/InitializableComplexHarness.sol",
     "name": "InitializableComplexHarness",
-    "spec": "certora/specs/Initializable.spec"
+    "spec": "certora/specs/Initializable.spec",
+    "args": "--rule_sanity advanced"
 }]

certora/run.sh

@@ -0,0 +1,26 @@
+#!/bin/bash
+
+for receipt in $(cat certora/matrix.json | jq -r ".[$1] | @base64")
+do
+    FILE=$(echo $receipt | base64 --decode | jq -r '.file')
+    NAME=$(echo $receipt | base64 --decode | jq -r '.name')
+    SPEC=$(echo $receipt | base64 --decode | jq -r '.spec')
+    ARGS=$(echo $receipt | base64 --decode | jq -r '.args//""')
+    DISABLED=$(echo $receipt | base64 --decode | jq -r '.disabled//false')
+
+
+    echo "Running $SPEC on $FILE:$NAME ..."
+    if [[ $DISABLED == 'true' ]];
+    then
+        echo "disabled"
+    else
+        certoraRun $FILE --verify $NAME:$SPEC --solc solc --optimistic_loop --loop_iter 3 $ARGS --cloud
+    fi
+done
+
+# [00] ERC1155.spec                   -- pass
+# [01] ERC1155Burnable.spec           -- pass
+# [02] ERC1155Pausable.spec           -- pass
+# [03] ERC1155Supply.spec             -- pass
+# [04] GovernorPreventLateQuorum.spec -- nope
+# [05] Initializable.spec             -- nope