certora linting

Certora · Mar 28, 2023 · 032a7c5 · 032a7c5
1 parent 8571c88
commit 032a7c5
Show file tree

Hide file tree

Showing 4 changed files with 93 additions and 94 deletions.
diff --git a/certora/harness/AaveTokenV3Harness.sol b/certora/harness/AaveTokenV3Harness.sol
@@ -8,48 +8,50 @@
 
 pragma solidity ^0.8.0;
 
-import {AaveTokenV3} from "../../src/AaveTokenV3.sol";
+import {AaveTokenV3} from '../../src/AaveTokenV3.sol';
 
 contract AaveTokenV3Harness is AaveTokenV3 {
-
-    // returns user's token balance, used in some community rules
-    function getBalance(address user) view public returns (uint104) {
+  // returns user's token balance, used in some community rules
+  function getBalance(address user) public view returns (uint104) {
     return _balances[user].balance;
-   }
-   // returns user's delegated proposition balance
-   function getDelegatedPropositionBalance(address user) view public returns (uint72) {
+  }
+
+  // returns user's delegated proposition balance
+  function getDelegatedPropositionBalance(address user) public view returns (uint72) {
     return _balances[user].delegatedPropositionBalance;
-   }
+  }
 
-   // returns user's delegated voting balance
-   function getDelegatedVotingBalance(address user) view public returns (uint72) {
+  // returns user's delegated voting balance
+  function getDelegatedVotingBalance(address user) public view returns (uint72) {
     return _balances[user].delegatedVotingBalance;
-   }
-
-   //returns user's delegating proposition status
-   function getDelegatingProposition(address user) view public returns (bool) {
-    return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
-        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
-   }
-
-   // returns user's delegating voting status
-   function getDelegatingVoting(address user) view public returns (bool) {
-     return _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
-        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
-   }
-
-   // returns user's voting delegate
-   function getVotingDelegate(address user) view public returns (address) {
+  }
+
+  //returns user's delegating proposition status
+  function getDelegatingProposition(address user) public view returns (bool) {
+    return
+      _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
+      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+  }
+
+  // returns user's delegating voting status
+  function getDelegatingVoting(address user) public view returns (bool) {
+    return
+      _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
+      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+  }
+
+  // returns user's voting delegate
+  function getVotingDelegate(address user) public view returns (address) {
     return _votingDelegateeV2[user];
-   }
+  }
 
-   // returns user's proposition delegate
-   function getPropositionDelegate(address user) view public returns (address) {
+  // returns user's proposition delegate
+  function getPropositionDelegate(address user) public view returns (address) {
     return _propositionDelegateeV2[user];
-   }
+  }
 
-   // returns user's delegation state
-   function getDelegationState(address user) view public returns (DelegationState) {
+  // returns user's delegation state
+  function getDelegationState(address user) public view returns (DelegationState) {
     return _balances[user].delegationState;
-   }
-}
+  }
+}
diff --git a/certora/harness/AaveTokenV3HarnessCommunity.sol b/certora/harness/AaveTokenV3HarnessCommunity.sol
@@ -2,57 +2,56 @@
 
 /**
 
-  This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for 
+  This is an extension of the AaveTokenV3 with added getters and view function wrappers needed for
   community-written rules
  */
 
 pragma solidity ^0.8.0;
 
-import {AaveTokenV3} from "../../src/AaveTokenV3.sol";
+import {AaveTokenV3} from '../../src/AaveTokenV3.sol';
 
 contract AaveTokenV3Harness is AaveTokenV3 {
-    function getBalance(address user) view public returns (uint104) {
+  function getBalance(address user) public view returns (uint104) {
     return _balances[user].balance;
-   }
+  }
 
-   function getDelegatedPropositionBalance(address user) view public returns (uint72) {
+  function getDelegatedPropositionBalance(address user) public view returns (uint72) {
     return _balances[user].delegatedPropositionBalance;
-   }
-
+  }
 
-   function getDelegatedVotingBalance(address user) view public returns (uint72) {
+  function getDelegatedVotingBalance(address user) public view returns (uint72) {
     return _balances[user].delegatedVotingBalance;
-   }
-
-
-   function getDelegatingProposition(address user) view public returns (bool) {
-    return _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
-        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
-   }
+  }
 
+  function getDelegatingProposition(address user) public view returns (bool) {
+    return
+      _balances[user].delegationState == DelegationState.PROPOSITION_DELEGATED ||
+      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+  }
 
-   function getDelegatingVoting(address user) view public returns (bool) {
-     return _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
-        _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
-   }
+  function getDelegatingVoting(address user) public view returns (bool) {
+    return
+      _balances[user].delegationState == DelegationState.VOTING_DELEGATED ||
+      _balances[user].delegationState == DelegationState.FULL_POWER_DELEGATED;
+  }
 
-   function getVotingDelegate(address user) view public returns (address) {
+  function getVotingDelegate(address user) public view returns (address) {
     return _votingDelegateeV2[user];
-   }
+  }
 
-   function getPropositionDelegate(address user) view public returns (address) {
+  function getPropositionDelegate(address user) public view returns (address) {
     return _propositionDelegateeV2[user];
-   }
+  }
 
-   function getDelegationState(address user) view public returns (DelegationState) {
+  function getDelegationState(address user) public view returns (DelegationState) {
     return _balances[user].delegationState;
-   }
+  }
 
-   function getNonce(address user) view public returns (uint256) {
+  function getNonce(address user) public view returns (uint256) {
     return _nonces[user];
-   }
+  }
 
-   function ecrecoverWrapper(
+  function ecrecoverWrapper(
     bytes32 hash,
     uint8 v,
     bytes32 r,
@@ -61,7 +60,7 @@ contract AaveTokenV3Harness is AaveTokenV3 {
     return ecrecover(hash, v, r, s);
   }
 
-   function computeMetaDelegateHash(
+  function computeMetaDelegateHash(
     address delegator,
     address delegatee,
     uint256 deadline,
@@ -77,7 +76,7 @@ contract AaveTokenV3Harness is AaveTokenV3 {
     return digest;
   }
 
-    function computeMetaDelegateByTypeHash(
+  function computeMetaDelegateByTypeHash(
     address delegator,
     address delegatee,
     GovernancePowerType delegationType,
@@ -102,5 +101,4 @@ contract AaveTokenV3Harness is AaveTokenV3 {
     );
     return digest;
   }
-
-}
+}
diff --git a/certora/harness/AaveTokenV3HarnessStorage.sol b/certora/harness/AaveTokenV3HarnessStorage.sol
@@ -4,53 +4,52 @@
 
   This is an extension of the harnessed AaveTokenV3 with added getters on the _balances fields.
   The imported harnessed AaveTokenV3 contract uses uint8 instead of an enum for delegation state.
-  
+
   This modification is introduced to bypass a current Certora Prover limitation on accessing
   enum fields inside CVL hooks
 
  */
 
 pragma solidity ^0.8.0;
 
-import {AaveTokenV3} from "../munged/AaveTokenV3.sol";
+import {AaveTokenV3} from '../munged/AaveTokenV3.sol';
 
 contract AaveTokenV3Harness is AaveTokenV3 {
-    function getBalance(address user) view public returns (uint104) {
+  function getBalance(address user) public view returns (uint104) {
     return _balances[user].balance;
-   }
+  }
 
-   function getDelegatedPropositionBalance(address user) view public returns (uint72) {
+  function getDelegatedPropositionBalance(address user) public view returns (uint72) {
     return _balances[user].delegatedPropositionBalance;
-   }
-
+  }
 
-   function getDelegatedVotingBalance(address user) view public returns (uint72) {
+  function getDelegatedVotingBalance(address user) public view returns (uint72) {
     return _balances[user].delegatedVotingBalance;
-   }
+  }
 
-
-   function getDelegatingProposition(address user) view public returns (bool) {
+  function getDelegatingProposition(address user) public view returns (bool) {
     uint8 state = _balances[user].delegationState;
-    return state == uint8(DelegationState.PROPOSITION_DELEGATED) ||
-        state == uint8(DelegationState.FULL_POWER_DELEGATED);
-   }
-
+    return
+      state == uint8(DelegationState.PROPOSITION_DELEGATED) ||
+      state == uint8(DelegationState.FULL_POWER_DELEGATED);
+  }
 
-   function getDelegatingVoting(address user) view public returns (bool) {
+  function getDelegatingVoting(address user) public view returns (bool) {
     uint8 state = _balances[user].delegationState;
-    return state == uint8(DelegationState.VOTING_DELEGATED) ||
-        state == uint8(DelegationState.FULL_POWER_DELEGATED);
-   }
+    return
+      state == uint8(DelegationState.VOTING_DELEGATED) ||
+      state == uint8(DelegationState.FULL_POWER_DELEGATED);
+  }
 
-   function getVotingDelegate(address user) view public returns (address) {
+  function getVotingDelegate(address user) public view returns (address) {
     return _votingDelegateeV2[user];
-   }
+  }
 
-   function getPropositionDelegate(address user) view public returns (address) {
+  function getPropositionDelegate(address user) public view returns (address) {
     return _propositionDelegateeV2[user];
-   }
+  }
 
-   function getDelegationState(address user) view public returns (uint8) {
+  function getDelegationState(address user) public view returns (uint8) {
     return _balances[user].delegationState;
-   }
-}
+  }
+}
diff --git a/certora/harness/README.md b/certora/harness/README.md
@@ -3,5 +3,5 @@ We use two harnesses:
 - AaveTokenV3Harness adds a few simple getters to the original AaveTokenV3 code
 
 - AaveTokenV3HarnessStorage is used to verify general.spec. It changes delegationState field in _balances
-to be uint8 instead of DelegationState enum. The harness files are produced by running `make munged` which 
-patches the original code with `applyHarness.patch` patch.
+to be uint8 instead of DelegationState enum. The harness files are produced by running `make munged` which
+patches the original code with `applyHarness.patch` patch.