Add Certora specs (#48)

* Certora setup (#37)

* builtin sanity, pre_condition rule

* folders

* more rules with advanced CVL properties

* document examples

* more options for ClipperCallee concrete implementations

* fix also fr Clipper

* where am I taken from

* fix

* remove kick summarization

* remove kick

* update links

* added rule sanity to configs

* added basic multicall spec

* adds a test solidity contract for multicall

* final setup touches and multicall

* added certora files and vim to gitignore

---------

Co-authored-by: EyalHochCertora <eyal@certora.com>
Co-authored-by: EyalHCertora <91595356+EyalHochCertora@users.noreply.github.com>

* LockstakeUrn

* Fix file header

* Use real Vat code and some changes to urn conf

* Use double quotes

* Add LockstakeMkr spec

* Fix

* Revert removal of end line

* LockstakeEngine (WIP) + Minor change for LockstakeUrn

* Remove space

* Remove factory from voteDelegate file

* Add missing check for selectVoteDelegate + add selectFarm and selectFarm_revert specs

* Add lock spec + minor changes to others

* lock_revert spec

* Improve comments

* lockNgt and lockNgt_revert specs

* Add free and feeeNgt specs

* Add free_revert and freeNgt_revert specs

* Add some new invariant rules + tidy up

* Add freeNoFee and freeNoFee_revert specs

* Simplify messages for non revert rules

* Add draw and draw_revert specs

* Add wipe, wipeAll and getReward specs

* Add wipe_revert and onKick specs

* Add wipeAll_revert spec

* Add getReward_revert spec

* farm renaming + minor changes

* Add onKick_revert spec + minor comments fix

* Fixes for inkMatchesLsmkrFarm

* Add onTake and onTake_revert specs

* Add onRemove and onRemove_revert specs

* Separate Multicall rules to different file + fix wipe_revert

* Minor changes

* Comment change

* First batch of LocstakeClipper specs

* Add redo and redo_specs + fix in storageAffected

* Clean up

* Fix specs timeouts for LockstakeEngine

* Add take spec + changes to storageAffected

* stopped revert conditions better matching with code

* Add take_revert spec

* Clipper: some variables renaming

* Add upchost upchost_revert specs

* Fix for take spec + add yank and yank_revert specs

* Engine: Rename several variables

* Update specs to newer version

* Remove unused function

* Fix CI

* Fix missing solc versions CI

* Fix timeouts

* Fix

* Change

* Some cleaning in multicall specs

* Add more invariants to LockstakeEngine

* Improve invariants for staking

* Fix

* Changes in invariants

* Include view functions invariants as well

* Fix

---------

Co-authored-by: Shoham Shamir <123297287+shoham-certora@users.noreply.github.com>
Co-authored-by: EyalHochCertora <eyal@certora.com>
Co-authored-by: EyalHCertora <91595356+EyalHochCertora@users.noreply.github.com>

.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 }}

.gitignore

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

Makefile

@@ -0,0 +1,6 @@
+PATH := ~/.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"
+}