Add initial LockstakeEngine/Urn/Clipper logic + tests

.github/workflows/certora.yml

@@ -0,0 +1,54 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        lockstake:
+          - urn
+          - lsmkr
+          - engine
+          - engine-multicall
+          - clipper
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - 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.8.21
+        run: solc-select install 0.8.21
+
+      - name: Solc Select 0.6.12
+        run: solc-select install 0.6.12
+
+      - name: Solc Select 0.5.12
+        run: solc-select install 0.5.12
+
+      - name: Install Certora
+        run: pip3 install certora-cli-beta
+
+      - name: Verify ${{ matrix.lockstake }}
+        run: make certora-${{ matrix.lockstake }} results=1
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.github/workflows/test.yml

@@ -1,6 +1,6 @@
 name: test
 
-on: workflow_dispatch
+on: [push, pull_request]
 
 env:
   FOUNDRY_PROFILE: ci
@@ -32,3 +32,5 @@ jobs:
         run: |
           forge test -vvv
         id: test
+        env:
+          ETH_RPC_URL: ${{ secrets.ETH_RPC_URL }}

.gitignore

@@ -12,3 +12,9 @@ docs/
 
 # Dotenv file
 .env
+
+# Certora
+.certora_internal
+
+# Vim
+.*.swp

.gitmodules

@@ -1,3 +1,3 @@
-[submodule "lib/dss-test"]
-	path = lib/dss-test
-	url = https://github.com/makerdao/dss-test
+[submodule "lib/token-tests"]
+	path = lib/token-tests
+	url = https://github.com/makerdao/token-tests/

Makefile

@@ -0,0 +1,6 @@
+PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts/solc-0.6.12:~/.solc-select/artifacts/solc-0.8.21:$(PATH)
+certora-urn                :; PATH=${PATH} certoraRun certora/LockstakeUrn.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-lsmkr              :; PATH=${PATH} certoraRun certora/LockstakeMkr.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-engine             :; PATH=${PATH} certoraRun certora/LockstakeEngine.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-engine-multicall   :; PATH=${PATH} certoraRun certora/LockstakeEngineMulticall.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)
+certora-clipper            :; PATH=${PATH} certoraRun certora/LockstakeClipper.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)

certora/LockstakeClipper.conf

@@ -0,0 +1,88 @@
+{
+    "files": [
+        "src/LockstakeClipper.sol",
+        "src/LockstakeEngine.sol",
+        "src/LockstakeUrn.sol",
+        "src/LockstakeMkr.sol",
+        "certora/harness/dss/Vat.sol",
+        "certora/harness/dss/Spotter.sol",
+        "certora/harness/dss/Dog.sol",
+        "certora/harness/dss/ClipperCallee.sol:BadGuy",
+        "certora/harness/dss/ClipperCallee.sol:RedoGuy",
+        "certora/harness/dss/ClipperCallee.sol:KickGuy",
+        "certora/harness/dss/ClipperCallee.sol:FileUintGuy",
+        "certora/harness/dss/ClipperCallee.sol:FileAddrGuy",
+        "certora/harness/dss/ClipperCallee.sol:YankGuy",
+        "test/mocks/VoteDelegateMock.sol",
+        "certora/harness/tokens/MkrMock.sol",
+        "test/mocks/StakingRewardsMock.sol"
+    ],
+    "solc_map": {
+        "LockstakeClipper": "solc-0.8.21",
+        "LockstakeEngine": "solc-0.8.21",
+        "LockstakeUrn": "solc-0.8.21",
+        "LockstakeMkr": "solc-0.8.21",
+        "Vat": "solc-0.5.12",
+        "Spotter": "solc-0.5.12",
+        "Dog": "solc-0.6.12",
+        "BadGuy": "solc-0.8.21",
+        "RedoGuy": "solc-0.8.21",
+        "KickGuy": "solc-0.8.21",
+        "FileUintGuy": "solc-0.8.21",
+        "FileAddrGuy": "solc-0.8.21",
+        "YankGuy": "solc-0.8.21",
+        "VoteDelegateMock": "solc-0.8.21",
+        "MkrMock": "solc-0.8.21",
+        "StakingRewardsMock": "solc-0.8.21"
+    },
+    "solc_optimize_map": {
+        "LockstakeClipper": "200",
+        "LockstakeEngine": "200",
+        "LockstakeUrn": "200",
+        "LockstakeMkr": "200",
+        "Vat": "0",
+        "Spotter": "0",
+        "Dog": "0",
+        "BadGuy": "0",
+        "RedoGuy": "0",
+        "KickGuy": "0",
+        "FileUintGuy": "0",
+        "FileAddrGuy": "0",
+        "YankGuy": "0",
+        "VoteDelegateMock": "0",
+        "MkrMock": "0",
+        "StakingRewardsMock": "0",
+    },
+    "link": [
+        "LockstakeClipper:vat=Vat",
+        "LockstakeClipper:engine=LockstakeEngine",
+        "LockstakeClipper:dog=Dog",
+        "LockstakeClipper:spotter=Spotter",
+        "LockstakeEngine:vat=Vat",
+        "LockstakeEngine:mkr=MkrMock",
+        "LockstakeEngine:lsmkr=LockstakeMkr",
+        "LockstakeUrn:engine=LockstakeEngine",
+        "VoteDelegateMock:gov=MkrMock",
+        "StakingRewardsMock:stakingToken=LockstakeMkr",
+        "Dog:vat=Vat",
+        "BadGuy:clip=LockstakeClipper",
+        "RedoGuy:clip=LockstakeClipper",
+        "KickGuy:clip=LockstakeClipper",
+        "FileUintGuy:clip=LockstakeClipper",
+        "FileAddrGuy:clip=LockstakeClipper",
+        "YankGuy:clip=LockstakeClipper"
+    ],
+    "verify": "LockstakeClipper:certora/LockstakeClipper.spec",
+    "prover_args": [
+        "-rewriteMSizeAllocations true"
+    ],
+    "smt_timeout": "7000",
+    "rule_sanity": "basic",
+    "optimistic_loop": true,
+    "optimistic_contract_recursion": true,
+    "contract_recursion_limit": "2",
+    "multi_assert_check": true,
+    "parametric_contracts": ["LockstakeClipper"],
+    "build_cache": true,
+    "msg": "LockstakeClipper"
+}