Hadrien Croubois 2 years ago
parent
commit
a64bb8801c
3 changed files with 52 additions and 36 deletions
  1. 25 28
      certora/specs.js
  2. 2 2
      certora/specs/GovernorFunctions.spec
  3. 25 6
      certora/specs/GovernorInvariants.spec

+ 25 - 28
certora/specs.js

@@ -38,9 +38,9 @@ module.exports = [].concat(
   },
   // Security
   {
-    "spec": "Pausable",
-    "contract": "PausableHarness",
-    "files": ["certora/harnesses/PausableHarness.sol"]
+    spec: 'Pausable',
+    contract: 'PausableHarness',
+    files: ['certora/harnesses/PausableHarness.sol'],
   },
   // Proxy
   {
@@ -77,29 +77,26 @@ module.exports = [].concat(
       '--optimistic_hashing',
     ],
   })),
-  /// WIP part
-  process.env.CI
-    ? []
-    : product(
-        ['GovernorHarness'],
-        ['GovernorFunctions'],
-        ['ERC20VotesBlocknumberHarness'],
-        ['propose', 'castVote', 'queue', 'execute', 'cancel'],
-      ).map(([contract, spec, token, fn]) => ({
-        spec,
-        contract,
-        files: [
-          `certora/harnesses/${contract}.sol`,
-          `certora/harnesses/${token}.sol`,
-          `certora/harnesses/TimelockControllerHarness.sol`,
-        ],
-        options: [
-          `--link ${contract}:token=${token}`,
-          `--link ${contract}:_timelock=TimelockControllerHarness`,
-          '--optimistic_loop',
-          '--optimistic_hashing',
-          '--rules',
-          ['liveness', 'effect', 'sideeffect'].map(rule => `${fn}_${rule}`).join(' '),
-        ],
-      })),
+  product(
+    ['GovernorHarness'],
+    ['GovernorFunctions'],
+    ['ERC20VotesBlocknumberHarness'], // 'ERC20VotesTimestampHarness'
+    ['propose', 'castVote', 'queue', 'execute', 'cancel'],
+  ).map(([contract, spec, token, fn]) => ({
+    spec,
+    contract,
+    files: [
+      `certora/harnesses/${contract}.sol`,
+      `certora/harnesses/${token}.sol`,
+      `certora/harnesses/TimelockControllerHarness.sol`,
+    ],
+    options: [
+      `--link ${contract}:token=${token}`,
+      `--link ${contract}:_timelock=TimelockControllerHarness`,
+      '--optimistic_loop',
+      '--optimistic_hashing',
+      '--rules',
+      ...['liveness', 'effect', 'sideeffect'].map(kind => `${fn}_${kind}`),
+    ],
+  })),
 );

+ 2 - 2
certora/specs/GovernorFunctions.spec

@@ -3,7 +3,7 @@ import "Governor.helpers.spec"
 import "GovernorInvariants.spec"
 
 use invariant proposalStateConsistency
-use invariant queuedImplyVoteOver
+use invariant queuedImplyDeadlineOver
 
 /*
 โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”
@@ -235,7 +235,7 @@ rule execute_sideeffect(uint256 pId, env e, uint256 otherId) {
 rule cancel_liveness(uint256 pId, env e) {
     require nonpayable(e);
     require clockSanity(e);
-    requireInvariant queuedImplyVoteOver(e, pId);
+    requireInvariant queuedImplyDeadlineOver(e, pId);
 
     uint8 stateBefore = state(e, pId);
 

+ 25 - 6
certora/specs/GovernorInvariants.spec

@@ -36,18 +36,19 @@ invariant proposalStateConsistency(uint256 pId)
 
 /*
 โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”
-โ”‚ Invariant: votes recorded => proposal snapshot is in the past                                                       โ”‚
+โ”‚ Invariant: votes recorded => created                                                                                โ”‚
 โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜
 */
-invariant votesImplySnapshotPassed(env e, uint256 pId)
+invariant votesImplyCreated(uint256 pId)
     (
         getAgainstVotes(pId) > 0 ||
         getForVotes(pId)     > 0 ||
         getAbstainVotes(pId) > 0
-    ) => proposalSnapshot(pId) < clock(e)
+    ) => proposalCreated(pId)
     {
-        preserved with (env e2) {
-            require clock(e) == clock(e2);
+        preserved with (env e) {
+            require clockSanity(e);
+            requireInvariant proposalStateConsistency(pId);
         }
     }
 
@@ -93,7 +94,25 @@ invariant queuedImplyCreated(uint pId)
         }
     }
 
-invariant queuedImplyVoteOver(env e, uint pId)
+
+/*
+โ”Œโ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”
+โ”‚ Invariant: timmings                                                                                                 โ”‚
+โ””โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”€โ”˜
+*/
+invariant votesImplySnapshotPassed(env e, uint256 pId)
+    (
+        getAgainstVotes(pId) > 0 ||
+        getForVotes(pId)     > 0 ||
+        getAbstainVotes(pId) > 0
+    ) => proposalSnapshot(pId) < clock(e)
+    {
+        preserved with (env e2) {
+            require clock(e) == clock(e2);
+        }
+    }
+
+invariant queuedImplyDeadlineOver(env e, uint pId)
     isQueued(pId) => proposalDeadline(pId) < clock(e)
     {
         preserved {