Update specs to newer version

makerdao · Sep 9, 2024 · dca0561 · dca0561
1 parent 7b2e485
commit dca0561
Show file tree

Hide file tree

Showing 11 changed files with 508 additions and 374 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -0,0 +1,49 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        lockstake:
+          - urn
+          - lsmkr
+          - engine
+          - engine-wipe-revert
+          - 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: Install Certora
+        run: pip3 install certora-cli-beta
+
+      - name: Verify ${{ matrix.lockstake }}
+        run: make certora-${{ matrix.lockstake }} --wait_for_results all
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
diff --git a/certora/LockstakeClipper.conf b/certora/LockstakeClipper.conf
@@ -83,5 +83,6 @@
     "contract_recursion_limit": "2",
     "multi_assert_check": true,
     "parametric_contracts": ["LockstakeClipper"],
+    "build_cache": true,
     "msg": "LockstakeClipper"
 }
diff --git a/certora/LockstakeClipper.spec b/certora/LockstakeClipper.spec
@@ -989,29 +989,46 @@ rule yank_revert(uint256 id) {
     mathint locked = lockedGhost();
     bytes32 ilk = ilk();
 
-    mathint a; mathint salesIdTab; mathint salesIdLot; address salesIdUsr;
-    a, salesIdTab, salesIdLot, a, salesIdUsr, a, a = sales(id);
+    mathint count = count();
+    mathint activeLast;
+    if (count > 0) {
+        activeLast = active(assert_uint256(count - 1));
+    } else {
+        activeLast = 0;
+    }
+
+    mathint salesIdPos; mathint salesIdTab; mathint salesIdLot; address salesIdUsr; mathint a;
+    salesIdPos, salesIdTab, salesIdLot, a, salesIdUsr, a, a = sales(id);
 
+    mathint engineWardsClipper = lockstakeEngine.wards(currentContract);
+
+    mathint dogWardsClipper = dog.wards(currentContract);
     mathint dogDirt = dog.Dirt();
     address b; mathint dogIlkDirt;
     b, a, a, dogIlkDirt = dog.ilks(ilk);
 
     mathint vatGemIlkClipper = vat.gem(ilk, currentContract);
+    mathint vatGemIlkSender  = vat.gem(ilk, e.msg.sender);
 
     // LockstakeEngine assumptions
+    require engineWardsClipper == 1;
     require lockstakeEngine.urnAuctions(salesIdUsr) > 0;
     // Dog assumptions
+    require dogWardsClipper == 1;
     require dogDirt >= salesIdTab;
     require dogIlkDirt >= salesIdTab;
+    // Vat assumption
+    require vatGemIlkSender + salesIdLot <= max_uint256;
 
-    yank(e, id);
+    yank@withrevert(e, id);
 
     bool revert1 = e.msg.value > 0;
     bool revert2 = wardsSender != 1;
     bool revert3 = locked != 0;
     bool revert4 = salesIdUsr == addrZero();
     bool revert5 = vatGemIlkClipper < salesIdLot;
+    bool revert6 = count == 0 || to_mathint(id) != activeLast && salesIdPos > count - 1;
 
     assert lastReverted <=> revert1 || revert2 || revert3 ||
-                            revert4 || revert5, "Revert rules failed";
+                            revert4 || revert5 || revert6, "Revert rules failed";
 }
diff --git a/certora/LockstakeEngine.conf b/certora/LockstakeEngine.conf
@@ -8,11 +8,11 @@
         "test/mocks/VoteDelegateMock.sol",
         "certora/harness/VoteDelegate2Mock.sol",
         "test/mocks/VoteDelegateMock.sol:VoteDelegateFactoryMock",
-        "test/mocks/NstJoinMock.sol",
-        "test/mocks/NstMock.sol",
+        "test/mocks/UsdsJoinMock.sol",
+        "test/mocks/UsdsMock.sol",
         "certora/harness/tokens/MkrMock.sol",
-        "test/mocks/MkrNgtMock.sol",
-        "certora/harness/tokens/NgtMock.sol",
+        "test/mocks/MkrSkyMock.sol",
+        "certora/harness/tokens/SkyMock.sol",
         "certora/harness/tokens/RewardsMock.sol",
         "test/mocks/StakingRewardsMock.sol",
         "certora/harness/StakingRewards2Mock.sol"
@@ -26,11 +26,11 @@
         "VoteDelegateMock": "solc-0.8.21",
         "VoteDelegate2Mock": "solc-0.8.21",
         "VoteDelegateFactoryMock": "solc-0.8.21",
-        "NstJoinMock": "solc-0.8.21",
-        "NstMock": "solc-0.8.21",
+        "UsdsJoinMock": "solc-0.8.21",
+        "UsdsMock": "solc-0.8.21",
         "MkrMock": "solc-0.8.21",
-        "MkrNgtMock": "solc-0.8.21",
-        "NgtMock": "solc-0.8.21",
+        "MkrSkyMock": "solc-0.8.21",
+        "SkyMock": "solc-0.8.21",
         "StakingRewardsMock": "solc-0.8.21",
         "StakingRewards2Mock": "solc-0.8.21",
         "RewardsMock": "solc-0.8.21"
@@ -41,11 +41,11 @@
         "LockstakeMkr": "200",
         "Jug": "0",
         "Vat": "0",
-        "NstJoinMock": "0",
-        "NstMock": "0",
+        "UsdsJoinMock": "0",
+        "UsdsMock": "0",
         "MkrMock": "0",
-        "MkrNgtMock": "0",
-        "NgtMock": "0",
+        "MkrSkyMock": "0",
+        "SkyMock": "0",
         "VoteDelegateMock": "0",
         "VoteDelegate2Mock": "0",
         "VoteDelegateFactoryMock": "0",
@@ -57,21 +57,21 @@
         "LockstakeEngine:jug=Jug",
         "LockstakeEngine:voteDelegateFactory=VoteDelegateFactoryMock",
         "LockstakeEngine:vat=Vat",
-        "LockstakeEngine:nstJoin=NstJoinMock",
-        "LockstakeEngine:nst=NstMock",
+        "LockstakeEngine:usdsJoin=UsdsJoinMock",
+        "LockstakeEngine:usds=UsdsMock",
         "LockstakeEngine:mkr=MkrMock",
         "LockstakeEngine:lsmkr=LockstakeMkr",
-        "LockstakeEngine:mkrNgt=MkrNgtMock",
-        "LockstakeEngine:ngt=NgtMock",
+        "LockstakeEngine:mkrSky=MkrSkyMock",
+        "LockstakeEngine:sky=SkyMock",
         "LockstakeEngine:urnImplementation=LockstakeUrn",
         "LockstakeUrn:engine=LockstakeEngine",
         "LockstakeUrn:lsmkr=LockstakeMkr",
         "LockstakeUrn:vat=Vat",
         "Jug:vat=Vat",
-        "NstJoinMock:vat=Vat",
-        "NstJoinMock:nst=NstMock",
-        "MkrNgtMock:mkr=MkrMock",
-        "MkrNgtMock:ngt=NgtMock",
+        "UsdsJoinMock:vat=Vat",
+        "UsdsJoinMock:usds=UsdsMock",
+        "MkrSkyMock:mkr=MkrMock",
+        "MkrSkyMock:sky=SkyMock",
         "VoteDelegateMock:gov=MkrMock",
         "VoteDelegate2Mock:gov=MkrMock",
         "VoteDelegateFactoryMock:gov=MkrMock",
@@ -90,5 +90,10 @@
     "optimistic_loop": true,
     "multi_assert_check": true,
     "parametric_contracts": ["LockstakeEngine"],
+    "build_cache": true,
+    "dynamic_bound": "1",
+    "prototype": [
+        "3d602d80600a3d3981f3363d3d373d3d3d363d73=LockstakeUrn"
+    ],
     "msg": "LockstakeEngine"
 }