Skip to content

Commit

Permalink
for PR
Browse files Browse the repository at this point in the history
  • Loading branch information
nisnislevi committed May 27, 2024
1 parent 2e59bf9 commit 239a3b8
Show file tree
Hide file tree
Showing 7 changed files with 235 additions and 23 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/certora-gho.yml
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ jobs:
max-parallel: 16
matrix:
rule:
- verifyGhoToken.conf --rule length_leq_max_uint160 inv_balanceOf_leq_totalSupply total_supply_eq_sumAllLevel sumAllBalance_eq_totalSupply sumAllLevel_eq_sumAllBalance inv_valid_capacity inv_valid_level address_in_set_values_iff_in_set_indexes addr_in_set_iff_in_map addr_in_set_list_iff_in_map level_leq_capacity mint_after_burn burn_after_mint level_unchanged_after_mint_followed_by_burn level_after_mint level_after_burn facilitator_in_list_after_setFacilitatorBucketCapacity getFacilitatorBucketCapacity_after_setFacilitatorBucketCapacity facilitator_in_list_after_addFacilitator facilitator_in_list_after_mint_and_burn address_not_in_list_after_removeFacilitator balance_after_mint balance_after_burn mintLimitedByFacilitatorRemainingCapacity burnLimitedByFacilitatorLevel ARRAY_IS_INVERSE_OF_MAP_Invariant addressSetInvariant address_not_in_list_after_removeFacilitator_CASE_SPLIT_zero_address
- verifyGhoToken.conf
- verifyGhoAToken.conf --rule noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment
- verifyGhoDiscountRateStrategy.conf --rule equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate
- verifyFlashMinter.conf --rule balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee
Expand Down
55 changes: 55 additions & 0 deletions .github/workflows/certora-upgradeable-gho-token.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
name: certora-upgradeable-gho-token

on:
push:
branches:
- main
pull_request:
branches:
- main

workflow_dispatch:

jobs:
verify:
runs-on: ubuntu-latest

steps:
- uses: actions/checkout@v2
with:
submodules: recursive

- name: Install python
uses: actions/setup-python@v2
with: { python-version: 3.9 }

- name: Install java
uses: actions/setup-java@v1
with: { java-version: '11', java-package: jre }

- name: Install certora cli
run: pip install certora-cli==4.13.1

- name: Install solc
run: |
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
chmod +x solc-static-linux
sudo mv solc-static-linux /usr/local/bin/solc8.10
- name: Verify rule ${{ matrix.rule }}
run: |
cd certora/gho
touch applyHarness.patch
make munged
cd ../..
echo "key length" ${#CERTORAKEY}
certoraRun certora/gho/conf/${{ matrix.rule }}
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}

strategy:
fail-fast: false
max-parallel: 16
matrix:
rule:
- verifyUpgradeableGhoToken.conf
95 changes: 76 additions & 19 deletions certora/gho/applyHarness.patch
Original file line number Diff line number Diff line change
@@ -1,13 +1,7 @@
diff -ruN ../src/.gitignore .gitignore
--- ../src/.gitignore 1970-01-01 02:00:00.000000000 +0200
+++ .gitignore 2023-02-26 11:58:05.000000000 +0200
@@ -0,0 +1,2 @@
+*
+!.gitignore
diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
--- ../src/contracts/gho/GhoToken.sol 2023-02-26 10:23:14.000000000 +0200
+++ contracts/gho/GhoToken.sol 2023-02-26 13:26:13.000000000 +0200
@@ -74,11 +74,16 @@
diff -ruN ../../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
--- ../../src/contracts/gho/GhoToken.sol 2024-05-21 10:57:52.000000000 +0300
+++ contracts/gho/GhoToken.sol 2024-05-27 12:55:24.588859419 +0300
@@ -66,11 +66,16 @@
uint128 bucketCapacity
) external onlyRole(FACILITATOR_MANAGER_ROLE) {
Facilitator storage facilitator = _facilitators[facilitatorAddress];
Expand All @@ -24,9 +18,9 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol

_facilitatorsList.add(facilitatorAddress);

@@ -92,6 +97,10 @@
/// @inheritdoc IGhoToken
function removeFacilitator(address facilitatorAddress) external onlyRole(FACILITATOR_MANAGER_ROLE) {
@@ -86,6 +91,10 @@
address facilitatorAddress
) external onlyRole(FACILITATOR_MANAGER_ROLE) {
require(
+ _facilitators[facilitatorAddress].isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
+ 'FACILITATOR_DOES_NOT_EXIST'
Expand All @@ -35,7 +29,7 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
bytes(_facilitators[facilitatorAddress].label).length > 0,
'FACILITATOR_DOES_NOT_EXIST'
);
@@ -111,6 +120,10 @@
@@ -105,6 +114,10 @@
address facilitator,
uint128 newCapacity
) external onlyRole(BUCKET_MANAGER_ROLE) {
Expand All @@ -46,7 +40,7 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
require(bytes(_facilitators[facilitator].label).length > 0, 'FACILITATOR_DOES_NOT_EXIST');

uint256 oldCapacity = _facilitators[facilitator].bucketCapacity;
@@ -125,12 +138,12 @@
@@ -119,12 +132,12 @@
}

/// @inheritdoc IGhoToken
Expand All @@ -61,14 +55,77 @@ diff -ruN ../src/contracts/gho/GhoToken.sol contracts/gho/GhoToken.sol
return _facilitatorsList.values();
}
}
diff -ruN ../src/contracts/gho/interfaces/IGhoToken.sol contracts/gho/interfaces/IGhoToken.sol
--- ../src/contracts/gho/interfaces/IGhoToken.sol 2023-02-26 10:23:14.000000000 +0200
+++ contracts/gho/interfaces/IGhoToken.sol 2023-02-26 11:58:05.000000000 +0200
@@ -14,6 +14,7 @@
diff -ruN ../../src/contracts/gho/interfaces/IGhoToken.sol contracts/gho/interfaces/IGhoToken.sol
--- ../../src/contracts/gho/interfaces/IGhoToken.sol 2024-05-21 10:57:52.000000000 +0300
+++ contracts/gho/interfaces/IGhoToken.sol 2024-05-27 12:55:24.588859419 +0300
@@ -13,6 +13,7 @@
uint128 bucketCapacity;
uint128 bucketLevel;
string label;
+ bool isLabelNonempty; //TODO: remove workaroun when https://certora.atlassian.net/browse/CERT-977 is resolved
}

/**
diff -ruN ../../src/contracts/gho/UpgradeableGhoToken.sol contracts/gho/UpgradeableGhoToken.sol
--- ../../src/contracts/gho/UpgradeableGhoToken.sol 2024-05-21 11:57:23.000000000 +0300
+++ contracts/gho/UpgradeableGhoToken.sol 2024-05-27 15:04:16.458997293 +0300
@@ -76,11 +76,16 @@
uint128 bucketCapacity
) external onlyRole(FACILITATOR_MANAGER_ROLE) {
Facilitator storage facilitator = _facilitators[facilitatorAddress];
+ require(
+ !facilitator.isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
+ 'FACILITATOR_ALREADY_EXISTS'
+ );
require(bytes(facilitator.label).length == 0, 'FACILITATOR_ALREADY_EXISTS');
require(bytes(facilitatorLabel).length > 0, 'INVALID_LABEL');

facilitator.label = facilitatorLabel;
facilitator.bucketCapacity = bucketCapacity;
+ facilitator.isLabelNonempty = true;

_facilitatorsList.add(facilitatorAddress);

@@ -96,6 +101,10 @@
address facilitatorAddress
) external onlyRole(FACILITATOR_MANAGER_ROLE) {
require(
+ _facilitators[facilitatorAddress].isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
+ 'FACILITATOR_DOES_NOT_EXIST'
+ );
+ require(
bytes(_facilitators[facilitatorAddress].label).length > 0,
'FACILITATOR_DOES_NOT_EXIST'
);
@@ -115,6 +124,10 @@
address facilitator,
uint128 newCapacity
) external onlyRole(BUCKET_MANAGER_ROLE) {
+ require(
+ _facilitators[facilitator].isLabelNonempty, //TODO: remove workaroun when CERT-977 is resolved
+ 'FACILITATOR_DOES_NOT_EXIST'
+ );
require(bytes(_facilitators[facilitator].label).length > 0, 'FACILITATOR_DOES_NOT_EXIST');

uint256 oldCapacity = _facilitators[facilitator].bucketCapacity;
@@ -129,12 +142,12 @@
}

/// @inheritdoc IGhoToken
- function getFacilitatorBucket(address facilitator) external view returns (uint256, uint256) {
+ function getFacilitatorBucket(address facilitator) public view returns (uint256, uint256) {
return (_facilitators[facilitator].bucketCapacity, _facilitators[facilitator].bucketLevel);
}

/// @inheritdoc IGhoToken
- function getFacilitatorsList() external view returns (address[] memory) {
+ function getFacilitatorsList() public view returns (address[] memory) {
return _facilitatorsList.values();
}

diff -ruN ../../src/.gitignore .gitignore
--- ../../src/.gitignore 1970-01-01 02:00:00.000000000 +0200
+++ .gitignore 2024-05-27 12:55:24.588859419 +0300
@@ -0,0 +1,2 @@
+*
+!.gitignore
2 changes: 1 addition & 1 deletion certora/gho/conf/verifyGhoToken.conf
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{
"files": [
"certora/gho/harness/GhoTokenHarness.sol:GhoTokenHarness",
"certora/gho/munged/contracts/gho/GhoToken.sol"
// "certora/gho/munged/contracts/gho/GhoToken.sol"
],
"packages": [
"@aave/core-v3/=lib/aave-v3-core",
Expand Down
18 changes: 18 additions & 0 deletions certora/gho/conf/verifyUpgradeableGhoToken.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
{
"files": [
"certora/gho/harness/UpgradeableGhoTokenHarness.sol:UpgradeableGhoTokenHarness",
// "certora/gho/munged/contracts/gho/GhoToken.sol"
],
"packages": [
"@aave/core-v3/=lib/aave-v3-core",
"@aave/periphery-v3/=lib/aave-v3-periphery",
"@aave/=lib/aave-token",
"@openzeppelin/=lib/openzeppelin-contracts",
],
"loop_iter": "3",
"msg": "GhoToken, all rules.",
"optimistic_loop": true,
"process": "emv",
"solc": "solc8.10",
"verify": "UpgradeableGhoTokenHarness:certora/gho/specs/ghoToken.spec"
}
84 changes: 84 additions & 0 deletions certora/gho/harness/UpgradeableGhoTokenHarness.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
pragma solidity ^0.8.0;

import {IGhoToken} from '../munged/contracts/gho/interfaces/IGhoToken.sol';
import '@openzeppelin/contracts/utils/structs/EnumerableSet.sol';
import {UpgradeableGhoToken} from '../munged/contracts/gho/UpgradeableGhoToken.sol';

contract UpgradeableGhoTokenHarness is UpgradeableGhoToken {
using EnumerableSet for EnumerableSet.AddressSet;

constructor() UpgradeableGhoToken() {}

/**
* @notice Returns the bucket capacity
* @param facilitator The address of the facilitator
* @return The facilitator bucket capacity
*/
function getFacilitatorBucketCapacity(address facilitator) public view returns (uint256) {
(uint256 bucketCapacity, ) = getFacilitatorBucket(facilitator);
return bucketCapacity;
}

/**
* @notice Returns the bucket level
* @param facilitator The address of the facilitator
* @return The facilitator bucket level
*/
function getFacilitatorBucketLevel(address facilitator) public view returns (uint256) {
(, uint256 bucketLevel) = getFacilitatorBucket(facilitator);
return bucketLevel;
}

/**
* @notice Returns the length of the facilitator list
* @return The length of the facilitator list
*/
function getFacilitatorsListLen() external view returns (uint256) {
address[] memory flist = getFacilitatorsList();
return flist.length;
}

/**
* @notice Indicator of GhoToken mapping
* @param addr An address of a facilitator
* @return True of facilitator is in GhoToken mapping
*/
function is_in_facilitator_mapping(address addr) external view returns (bool) {
Facilitator memory facilitator = _facilitators[addr];
return facilitator.isLabelNonempty; //TODO: remove workaround when CERT-977 is resolved
// return (bytes(facilitator.label).length > 0);
}

/**
* @notice Indicator of AddressSet mapping
* @param addr An address of a facilitator
* @return True of facilitator is in AddressSet mapping
*/
function is_in_facilitator_set_map(address addr) external view returns (bool) {
return _facilitatorsList.contains(addr);
}

/**
* @notice Indicator of AddressSet list
* @param addr An address of a facilitator
* @return True of facilitator is in AddressSet array
*/
function is_in_facilitator_set_array(address addr) external view returns (bool) {
address[] memory flist = getFacilitatorsList();
for (uint256 i = 0; i < flist.length; ++i) {
if (address(flist[i]) == addr) {
return true;
}
}
return false;
}

/**
* @notice Converts address to bytes32
* @param value Some address
* @return b the value as bytes32
*/
function to_bytes32(address value) external pure returns (bytes32 b) {
b = bytes32(uint256(uint160(value)));
}
}
2 changes: 0 additions & 2 deletions certora/gho/specs/ghoToken.spec
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
import "set.spec";

using GhoToken as GHOTOKEN;
methods{
function mint(address,uint256) external;
function burn(uint256) external;
Expand All @@ -15,7 +14,6 @@ methods{
function is_in_facilitator_mapping(address) external returns bool envfree;
function is_in_facilitator_set_map(address) external returns bool envfree;
function is_in_facilitator_set_array(address) external returns bool envfree;
//function to_bytes32(address) external returns (bytes32) envfree;
}

ghost sumAllBalance() returns mathint {
Expand Down

0 comments on commit 239a3b8

Please sign in to comment.