Add Certora specs for Vat and Dai contracts

.github/workflows/certora.yml

@@ -0,0 +1,43 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        l2dss:
+          - vat
+          - dai
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+
+      - uses: actions/setup-java@v2
+        with:
+          distribution: 'zulu'
+          java-version: '11'
+          java-package: jre
+
+      - name: Set up Python 3.8
+        uses: actions/setup-python@v3
+        with:
+          python-version: 3.8
+
+      - name: Install solc-select
+        run: pip3 install solc-select
+
+      - name: Solc Select 0.5.12
+        run: solc-select install 0.5.12
+
+      - name: Install Certora
+        run: pip3 install certora-cli-alpha-master
+
+      - name: Verify ${{ matrix.l2dss }}
+        run: make certora-${{ matrix.l2dss }} short=1 multi=1
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

@@ -1,2 +1,10 @@
 /out
 .DS_Store
+
+# certora
+.*certora*
+.last_confs/
+*.zip
+resource_errors.json
+.zip-output-url.txt
+certora_debug_log.txt

Makefile

@@ -1,7 +1,8 @@
 .PHONY: build clean test test-gas
 
-build    :; DAPP_BUILD_OPTIMIZE=0 DAPP_BUILD_OPTIMIZE_RUNS=0 dapp --use solc:0.5.12 build
-clean    :; dapp clean
-test     :; DAPP_BUILD_OPTIMIZE=0 DAPP_BUILD_OPTIMIZE_RUNS=0 DAPP_TEST_ADDRESS=0xAb5801a7D398351b8bE11C439e05C5B3259aeC9B dapp --use solc:0.5.12 test -v ${TEST_FLAGS}
-test-gas : build
-	LANG=C.UTF-8 hevm dapp-test --rpc="${ETH_RPC_URL}" --json-file=out/dapp.sol.json --dapp-root=. --verbose 2 --match "test_gas"
+build    	:; DAPP_BUILD_OPTIMIZE=0 DAPP_BUILD_OPTIMIZE_RUNS=0 dapp --use solc:0.5.12 build
+clean    	:; dapp clean
+test     	:; DAPP_BUILD_OPTIMIZE=0 DAPP_BUILD_OPTIMIZE_RUNS=0 DAPP_TEST_ADDRESS=0xAb5801a7D398351b8bE11C439e05C5B3259aeC9B dapp --use solc:0.5.12 test -v ${TEST_FLAGS}
+test-gas 	:; build && LANG=C.UTF-8 hevm dapp-test --rpc="${ETH_RPC_URL}" --json-file=out/dapp.sol.json --dapp-root=. --verbose 2 --match "test_gas"
+certora-vat :; PATH=~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts/:${PATH} certoraRun --solc_map Vat=solc-0.5.12 --optimize_map Vat=0 --rule_sanity basic src/vat.sol:Vat --verify Vat:certora/Vat.spec --staging jaroslav/partialLIAAxiomatisation --settings -mediumTimeout=180,-deleteSMTFile=false,-postProcessCounterExamples=none,-t=1200$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)
+certora-dai :; PATH=~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:${PATH} certoraRun --solc_map Dai=solc-0.5.12,Auxiliar=solc-0.5.12 --optimize_map Dai=0,Auxiliar=0 --rule_sanity basic src/dai.sol:Dai certora/Auxiliar.sol --verify Dai:certora/Dai.spec --settings -mediumTimeout=180 --optimistic_loop$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)$(if $(multi), --multi_assert_check,)

certora/Auxiliar.sol

@@ -0,0 +1,43 @@
+pragma solidity 0.5.12;
+
+interface IERC1271 {
+    function isValidSignature(
+        bytes32,
+        bytes calldata
+    ) external view returns (bytes4);
+}
+
+contract Auxiliar {    
+    function computeDigestForDai(
+        bytes32 domain_separator,
+        bytes32 permit_typehash,
+        address holder,
+        address spender,
+        uint256 nonce,
+        uint256 expiry,
+        bool allowed
+    ) public pure returns (bytes32 digest){
+        digest =
+        keccak256(abi.encodePacked(
+            "\x19\x01",
+            domain_separator,
+            keccak256(abi.encode(
+                permit_typehash,
+                holder,
+                spender,
+                nonce,
+                expiry,
+                allowed
+            ))
+        ));
+    }
+
+    function call_ecrecover(
+        bytes32 digest,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public pure returns (address signer) {
+        signer = ecrecover(digest, v, r, s);
+    }
+}