refactor: address review comments

makerdao · Oct 22, 2024 · e6aa067 · e6aa067
1 parent a8db00d
commit e6aa067
Show file tree

Hide file tree

Showing 13 changed files with 76 additions and 118 deletions.
diff --git a/certora/DssVestMintable.conf b/certora/DssVestMintable.conf
@@ -1,36 +1,25 @@
 {
+  "verify": "DssVestMintable:certora/DssVestMintable.spec",
+  "parametric_contracts": [
+    "DssVestMintable"
+  ],
   "files": [
     "src/DssVest.sol:DssVestMintable",
-    "certora/mocks/DSToken.sol",
-    "certora/mocks/MockAuthority.sol",
+    "certora/harness/DSToken.sol",
+    "certora/harness/MockAuthority.sol"
   ],
-  "link": [
-    "DssVestMintable:gem=DSToken",
-    "DSToken:authority=MockAuthority"
-    ],
-  "rule_sanity": "basic",
-  "multi_assert_check": true,
-  "wait_for_results": "all",
-  "solc_map": {
-    "DssVestMintable": "solc-0.6.12",
-    "DSToken": "solc-0.6.12",
-    "MockAuthority": "solc-0.6.12"
-  },
+  "solc": "solc-0.6.12",
   "solc_optimize_map": {
     "DssVestMintable": "200",
     "DSToken": "0",
     "MockAuthority": "0"
   },
-  "verify": "DssVestMintable:certora/DssVestMintable.spec",
-  "prover_args": [
-    "-smt_hashingScheme plainInjectivity",
-    "-s [yices,z3]",
-    "-splitParallel true",
-    "-mediumTimeout 3600",
-    "-depth 30",
-    "-enableSolidityBasedInlining true"
+  "link": [
+    "DssVestMintable:gem=DSToken",
+    "DSToken:authority=MockAuthority"
   ],
-  "parametric_contracts": [
-    "DssVestMintable"
-  ]
+  "build_cache": true,
+  "rule_sanity": "basic",
+  "multi_assert_check": true,
+  "wait_for_results": "all"
 }
diff --git a/certora/DssVestMintable.spec b/certora/DssVestMintable.spec
@@ -1,7 +1,5 @@
 // DssVestMintable.spec
 
-// certoraRun src/DssVest.sol:DssVestMintable certora/DSToken.sol certora/MockAuthority.sol --link DssVestMintable:gem=DSToken DSToken:authority=MockAuthority --verify DssVestMintable:certora/DssVestMintable.spec --rule_sanity
-
 using DSToken as token;
 using MockAuthority as authority;
 
@@ -38,14 +36,13 @@ hook Sload uint256 value locked {
     require lockedGhost() == value;
 }
 
-invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0
-filtered { f -> !f.isFallback }
-invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0
-filtered { f -> !f.isFallback }
-invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id)
-filtered { f -> !f.isFallback }
-invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id)
-filtered { f -> !f.isFallback }
+invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0;
+
+invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0;
+
+invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id);
+
+invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id);
 
 // The following invariant is replaced with a rule as it was kind of difficult to be finished this way.
 // Leaving this commented for possible future option to be finished.
@@ -286,8 +283,8 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2
 
     create@withrevert(e, _usr, _tot, _bgn, _tau, _eta, _mgr);
 
-    mathint clf = to_mathint(_bgn) + to_mathint(_eta);
-    mathint fin = to_mathint(_bgn) + to_mathint(_tau);
+    mathint clf = _bgn + _eta;
+    mathint fin = _bgn + _tau;
 
     bool revert1  = e.msg.value > 0;
     bool revert2  = ward != 1;

diff --git a/certora/DssVestSuckable.conf b/certora/DssVestSuckable.conf
@@ -1,51 +1,38 @@
 {
+  "verify": "DssVestSuckable:certora/DssVestSuckable.spec",
+  "parametric_contracts": [
+    "DssVestSuckable"
+  ],
   "files": [
     "src/DssVest.sol:DssVestSuckable",
-    "certora/mocks/ChainLog.sol",
-    "certora/mocks/Dai.sol",
-    "certora/mocks/DaiJoin.sol",
-    "certora/mocks/DSToken.sol",
-    "certora/mocks/MockAuthority.sol",
-    "certora/mocks/Vat.sol"
-  ],
-  "link": [
-    "DssVestSuckable:chainlog=ChainLog",
-    "DssVestSuckable:join=DaiJoin",
-    "DssVestSuckable:vat=Vat",
-    "DaiJoin:vat=Vat",
-    "DaiJoin:dai=Dai"
+    "certora/harness/ChainLog.sol",
+    "certora/harness/Dai.sol",
+    "certora/harness/DaiJoin.sol",
+    "certora/harness/Vat.sol"
   ],
-  "rule_sanity": "basic",
-  "multi_assert_check": true,
-  "wait_for_results": "all",
   "solc_map": {
     "DssVestSuckable": "solc-0.6.12",
     "ChainLog": "solc-0.6.12",
     "Dai": "solc-0.5.12",
     "DaiJoin": "solc-0.5.12",
-    "DSToken": "solc-0.6.12",
-    "MockAuthority": "solc-0.6.12",
     "Vat": "solc-0.5.12"
   },
   "solc_optimize_map": {
     "DssVestSuckable": "200",
     "ChainLog": "0",
     "Dai": "0",
     "DaiJoin": "0",
-    "DSToken": "0",
-    "MockAuthority": "0",
     "Vat": "0"
   },
-  "verify": "DssVestSuckable:certora/DssVestSuckable.spec",
-  "prover_args": [
-    "-smt_hashingScheme plainInjectivity",
-    "-s [yices,z3]",
-    "-splitParallel true",
-    "-mediumTimeout 3600",
-    "-depth 30",
-    "-enableSolidityBasedInlining true"
+  "link": [
+    "DssVestSuckable:chainlog=ChainLog",
+    "DssVestSuckable:join=DaiJoin",
+    "DssVestSuckable:vat=Vat",
+    "DaiJoin:vat=Vat",
+    "DaiJoin:dai=Dai"
   ],
-  "parametric_contracts": [
-    "DssVestSuckable"
-  ]
+  "build_cache": true,
+  "rule_sanity": "basic",
+  "multi_assert_check": true,
+  "wait_for_results": "all"
 }
diff --git a/certora/DssVestSuckable.spec b/certora/DssVestSuckable.spec
@@ -1,7 +1,5 @@
 // DssVestSuckable.spec
 
-// certoraRun src/DssVest.sol:DssVestSuckable certora/ChainLog.sol certora/Vat.sol certora/DaiJoin.sol certora/Dai.sol --link DssVestSuckable:chainlog=ChainLog DssVestSuckable:vat=Vat DssVestSuckable:join=DaiJoin DaiJoin:vat=Vat DaiJoin:dai=Dai --verify DssVestSuckable:certora/DssVestSuckable.spec --rule_sanity
-
 using ChainLog as chainlog;
 using DaiJoin as join;
 using Vat as vat;
@@ -38,7 +36,6 @@ methods {
     function dai.balanceOf(address) external returns (uint256) envfree;
 }
 
-/* definition max_uint48 returns uint256 = 2^48 - 1; */
 definition RAY() returns uint256 = 10^27;
 
 ghost lockedGhost() returns uint256;
@@ -51,14 +48,14 @@ hook Sload uint256 value locked {
     require lockedGhost() == value;
 }
 
-invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0
-filtered { f -> !f.isFallback }
-invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0
-filtered { f -> !f.isFallback }
-invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id)
-filtered { f -> !f.isFallback }
-invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id)
-filtered { f -> !f.isFallback }
+invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0;
+
+invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0;
+
+invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id);
+
+invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id);
+
 
 // The following invariant is replaced with a rule as it was kind of difficult to be finished this way.
 // Leaving this commented for possible future option to be finished.
@@ -75,7 +72,7 @@ filtered { f -> !f.isFallback }
 //     init_state axiom rxd(_id) == 0;
 // }
 
-rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } {
+rule rxdLessOrEqualTot(method f)  {
     env e;
     uint256 _id;
 
@@ -299,8 +296,8 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2
 
     create@withrevert(e, _usr, _tot, _bgn, _tau, _eta, _mgr);
 
-    mathint clf = to_mathint(_bgn) + to_mathint(_eta);
-    mathint fin = to_mathint(_bgn) + to_mathint(_tau);
+    mathint clf = _bgn + _eta;
+    mathint fin = _bgn + _tau;
 
     bool revert1  = e.msg.value > 0;
     bool revert2  = ward != 1;

diff --git a/certora/DssVestTransferrable.conf b/certora/DssVestTransferrable.conf
@@ -1,32 +1,22 @@
 {
+  "verify": "DssVestTransferrable:certora/DssVestTransferrable.spec",
+  "parametric_contracts": [
+    "DssVestTransferrable"
+  ],
   "files": [
     "src/DssVest.sol:DssVestTransferrable",
-    "certora/mocks/Dai.sol",
+    "certora/harness/Dai.sol"
   ],
-  "link": [
-    "DssVestTransferrable:gem=Dai"
-  ],
-  "rule_sanity": "basic",
-  "multi_assert_check": true,
-  "wait_for_results": "all",
-  "solc_map": {
-    "DssVestTransferrable": "solc-0.6.12",
-    "Dai": "solc-0.6.12"
-  },
+  "solc": "solc-0.6.12",
   "solc_optimize_map": {
     "DssVestTransferrable": "200",
     "Dai": "0"
   },
-  "verify": "DssVestTransferrable:certora/DssVestTransferrable.spec",
-  "prover_args": [
-    "-smt_hashingScheme plainInjectivity",
-    "-s [yices,z3]",
-    "-splitParallel true",
-    "-mediumTimeout 3600",
-    "-depth 30",
-    "-enableSolidityBasedInlining true"
+  "link": [
+    "DssVestTransferrable:gem=Dai"
   ],
-  "parametric_contracts": [
-    "DssVestTransferrable"
-  ]
+  "build_cache": true,
+  "rule_sanity": "basic",
+  "multi_assert_check": true,
+  "wait_for_results": "all"
 }
diff --git a/certora/DssVestTransferrable.spec b/certora/DssVestTransferrable.spec
@@ -1,7 +1,5 @@
 // DssVestTransferrable.spec
 
-// certoraRun src/DssVest.sol:DssVestTransferrable certora/Dai.sol --link DssVestTransferrable:gem=Dai --verify DssVestTransferrable:certora/DssVestTransferrable.spec --rule_sanity
-
 using Dai as dai;
 
 methods {
@@ -36,14 +34,14 @@ hook Sload uint256 value locked {
     require lockedGhost() == value;
 }
 
-invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0
-filtered { f -> !f.isFallback }
-invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0
-filtered { f -> !f.isFallback }
-invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id)
-filtered { f -> !f.isFallback }
-invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id)
-filtered { f -> !f.isFallback }
+invariant everythingNotSetIfUsrNotSet(uint256 _id) usr(_id) == 0 => bgn(_id) == 0 && clf(_id) == 0 && fin(_id) == 0 && mgr(_id) == 0 && res(_id) == 0 && tot(_id) == 0 && rxd(_id) == 0;
+
+invariant usrCantBeZeroIfCreate(uint256 _id) _id > 0 && _id <= ids() => usr(_id) != 0;
+
+invariant clfGreaterOrEqualBgn(uint256 _id) clf(_id) >= bgn(_id);
+
+invariant finGreaterOrEqualClf(uint256 _id) fin(_id) >= clf(_id);
+
 
 // The following invariant is replaced with a rule as it was kind of difficult to be finished this way.
 // Leaving this commented for possible future option to be finished.
@@ -60,7 +58,7 @@ filtered { f -> !f.isFallback }
 //     init_state axiom rxd(_id) == 0;
 // }
 
-rule rxdLessOrEqualTot(method f) filtered { f -> !f.isFallback } {
+rule rxdLessOrEqualTot(method f)  {
     env e;
     uint256 _id;
 
@@ -284,8 +282,8 @@ rule create_revert(address _usr, uint256 _tot, uint256 _bgn, uint256 _tau, uint2
 
     create@withrevert(e, _usr, _tot, _bgn, _tau, _eta, _mgr);
 
-    mathint clf = to_mathint(_bgn) + to_mathint(_eta);
-    mathint fin = to_mathint(_bgn) + to_mathint(_tau);
+    mathint clf = _bgn + _eta;
+    mathint fin = _bgn + _tau;
 
     bool revert1  = e.msg.value > 0;
     bool revert2  = ward != 1;

diff --git a/certora/mocks/ChainLog.sol → certora/harness/ChainLog.sol b/certora/mocks/ChainLog.sol → certora/harness/ChainLog.sol
diff --git a/certora/mocks/DSToken.sol → certora/harness/DSToken.sol b/certora/mocks/DSToken.sol → certora/harness/DSToken.sol
diff --git a/certora/mocks/Dai.sol → certora/harness/Dai.sol b/certora/mocks/Dai.sol → certora/harness/Dai.sol
diff --git a/certora/mocks/DaiJoin.sol → certora/harness/DaiJoin.sol b/certora/mocks/DaiJoin.sol → certora/harness/DaiJoin.sol
diff --git a/certora/mocks/MockAuthority.sol → certora/harness/MockAuthority.sol b/certora/mocks/MockAuthority.sol → certora/harness/MockAuthority.sol
diff --git a/certora/mocks/Vat.sol → certora/harness/Vat.sol b/certora/mocks/Vat.sol → certora/harness/Vat.sol
diff --git a/src/DssVest.t.sol b/src/DssVest.t.sol
@@ -310,7 +310,7 @@ contract DssVestTest is DSTest {
 
     function testAccrued() public {
         uint256 id = mVest.create(address(this), 100 * days_vest, block.timestamp + 10 days, 100 days, 0, address(0));
-        assertTrue(mVest.valid(id), "0");
+        assertTrue(mVest.valid(id));
 
         assertEq(mVest.accrued(id), 0, "1");
         hevm.warp(block.timestamp + 43200);