diff --git a/.github/workflows/run-confs.yml b/.github/workflows/run-confs.yml new file mode 100644 index 0000000..d377b5a --- /dev/null +++ b/.github/workflows/run-confs.yml @@ -0,0 +1,45 @@ +name: test + +on: pull_request + +env: + FOUNDRY_PROFILE: ci + CONFIGS: | + certora/confs/exp2-check-summary.conf + certora/confs/exp2-implementation.conf + certora/confs/KatToken-exp2.conf + certora/confs/KatToken-simple.conf + certora/confs/MerkleMinter-simple.conf + certora/confs/sanity-KatToken.conf + certora/confs/sanity-MerkleMinter.conf + +jobs: + check: + runs-on: ubuntu-latest + permissions: + contents: read + statuses: write + pull-requests: write + steps: + - name: checkout repository + uses: actions/checkout@v4 + with: + submodules: recursive + + - name: install foundry + uses: foundry-rs/foundry-toolchain@v1 + + - name: install dependencies + run: | + forge soldeer install + npm i + + - name: run configs + uses: Certora/certora-run-action@v1 + with: + configurations: ${{ env.CONFIGS }} + solc-versions: 0.8.28 + solc-remove-version-prefix: "0." + certora-key: ${{ secrets.CERTORAKEY }} + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} diff --git a/.gitignore b/.gitignore index 2e06fbc..76e8f8d 100644 --- a/.gitignore +++ b/.gitignore @@ -14,4 +14,12 @@ docs/ .env dependencies/ -node_modules/ \ No newline at end of file +node_modules/ + +# Certora files +.certora_internal/ +.venv/ +emv-*-certora-* +package-lock.json +remappings.txt +soldeer.lock diff --git a/certora/.gitattributes b/certora/.gitattributes new file mode 100644 index 0000000..4dccbf9 --- /dev/null +++ b/certora/.gitattributes @@ -0,0 +1,3 @@ +*.spec linguist-language=Solidity +*.conf linguist-detectable +*.conf linguist-language=JSON5 \ No newline at end of file diff --git a/certora/confs/KatToken.conf b/certora/confs/KatToken.conf new file mode 100644 index 0000000..b46987a --- /dev/null +++ b/certora/confs/KatToken.conf @@ -0,0 +1,20 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/KatTokenHarness.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "msg": "KatToken", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + "process": "emv", + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "KatTokenHarness:certora/specs/KatToken.spec" +} \ No newline at end of file diff --git a/certora/confs/MerkleMinter.conf b/certora/confs/MerkleMinter.conf new file mode 100644 index 0000000..855f984 --- /dev/null +++ b/certora/confs/MerkleMinter.conf @@ -0,0 +1,26 @@ +{ + "assert_autofinder_success": true, + "files": [ + "src/MerkleMinter.sol", + "src/KatToken.sol" + ], + "global_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "link": [ + "MerkleMinter:katToken=KatToken" + ], + //"parametric_contracts": [ "MerkleMinter" ], + "msg": "MerkleMinter", + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + + "process": "emv", + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "MerkleMinter:certora/specs/MerkleMinter.spec" +} \ No newline at end of file diff --git a/certora/confs/powUtil.conf b/certora/confs/powUtil.conf new file mode 100644 index 0000000..b9cf13d --- /dev/null +++ b/certora/confs/powUtil.conf @@ -0,0 +1,23 @@ +{ + "assert_autofinder_success": true, + "files": [ + "certora/harnesses/PowUtilHarness.sol", + "src/KatToken.sol", + ], + "global_timeout": "7200", + "smt_timeout": "7200", + "loop_iter": "2", + "optimistic_loop": true, + "packages": [ + "@openzeppelin/merkle-tree=node_modules/@openzeppelin/merkle-tree", + "@openzeppelin-contracts-5.1.0=dependencies/@openzeppelin-contracts-5.1.0", + "forge-std-1.9.4=dependencies/forge-std-1.9.4" + ], + + "process": "emv", + "server": "production", + "solc": "solc8.28", + "solc_via_ir": false, + "verify": "PowUtilHarness:certora/specs/powUtil.spec", + "msg": "Check exp2", +} \ No newline at end of file diff --git a/certora/harnesses/KatTokenHarness.sol b/certora/harnesses/KatTokenHarness.sol new file mode 100644 index 0000000..b210947 --- /dev/null +++ b/certora/harnesses/KatTokenHarness.sol @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: SEE LICENSE IN LICENSE +pragma solidity 0.8.28; +import {KatToken} from "src/KatToken.sol"; + +contract KatTokenHarness is KatToken { + constructor( + string memory _name, + string memory _symbol, + address _inflationAdmin, + address _inflationBeneficiary, + address _merkleMinter + ) KatToken(_name, _symbol, _inflationAdmin, _inflationBeneficiary, _merkleMinter) + { + } + + function get_lastMintCapacityIncrease() public view returns (uint256) { + return lastMintCapacityIncrease; + } + + function get_distributedSupplyCap() public view returns (uint256) { + return distributedSupplyCap; + } + +} diff --git a/certora/harnesses/PowUtilHarness.sol b/certora/harnesses/PowUtilHarness.sol new file mode 100644 index 0000000..c832943 --- /dev/null +++ b/certora/harnesses/PowUtilHarness.sol @@ -0,0 +1,11 @@ +//SPDX-License-Identifier: MIT +pragma solidity 0.8.28; + +import {PowUtil} from "../../src/Powutil.sol"; + +// Makes it easier to access `PowUtil.exp2`. +contract PowUtilHarness { + function exp2(uint256 x) public pure returns (uint256 result) { + return PowUtil.exp2(x); + } +} \ No newline at end of file diff --git a/certora/scripts/run.sh b/certora/scripts/run.sh new file mode 100755 index 0000000..167df78 --- /dev/null +++ b/certora/scripts/run.sh @@ -0,0 +1,7 @@ +certoraRun certora/confs/KatToken.conf +certoraRun certora/confs/KatToken.conf --verify KatTokenHarness:certora/specs/KatToken_changeInflation.spec --msg changeInflation_revertConditions + +# the rule indexIsClaimedValueChange requires using bitVector theory +certoraRun certora/confs/MerkleMinter.conf --rule indexIsClaimedValueChange --prover_args -smt_bitVectorTheory true --msg "MerkleMinter indexIsClaimedValueChange" +# all the other rules can be verified using the default integer theory +certoraRun certora/confs/MerkleMinter.conf --exclude_rule indexIsClaimedValueChange \ No newline at end of file diff --git a/certora/specs/KatToken.spec b/certora/specs/KatToken.spec new file mode 100644 index 0000000..c749d2e --- /dev/null +++ b/certora/specs/KatToken.spec @@ -0,0 +1,207 @@ +import "./exp2-summary.spec"; + +methods { + function inflationAdmin() external returns (address) envfree; + function pendingInflationAdmin() external returns (address) envfree; + function inflationBeneficiary() external returns (address) envfree; + function pendingInflationBeneficiary() external returns (address) envfree; + function inflationFactor() external returns (uint256) envfree; + function MAX_INFLATION() external returns (uint256) envfree; + function merkleMinter() external returns (address) envfree; + function mintCapacity(address) external returns (uint256) envfree; + + //harness methods declared envfree + function get_lastMintCapacityIncrease() external returns (uint256) envfree; + function get_distributedSupplyCap() external returns (uint256) envfree; + + function ERC20._mint(address to, uint256 amount) internal + => _mintCVL(to, amount); + + //MerkleProof + function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE; + + function _.eip712Domain() external => NONDET DELETE; +} + +rule integrityOfchangeInflationAdmin(env e) { + address oldOwner = inflationAdmin(); + address newOwner; + + changeInflationAdmin(e, newOwner); + + assert(e.msg.sender == oldOwner); + assert(pendingInflationAdmin() == newOwner); +} + +rule integrityOfchangeInflationBeneficiary(env e) { + address oldOwner = inflationBeneficiary(); + address newOwner; + + changeInflationBeneficiary(e, newOwner); + + assert(e.msg.sender == oldOwner); + assert(pendingInflationBeneficiary() == newOwner); +} + +rule lastMintCapacityIncreaseNeverDecreases(env e, method f) +{ + uint256 lastMintCapacityIncrease_pre = get_lastMintCapacityIncrease(); + + calldataarg args; + f(e, args); + uint256 lastMintCapacityIncrease_post = get_lastMintCapacityIncrease(); + assert lastMintCapacityIncrease_post >= lastMintCapacityIncrease_pre; +} + +rule distributedSupplyCapNeverDecreases(env e, method f) +{ + uint256 distributedSupplyCap_pre = get_distributedSupplyCap(); + + calldataarg args; + f(e, args); + uint256 distributedSupplyCap_post = get_distributedSupplyCap(); + assert distributedSupplyCap_post >= distributedSupplyCap_pre; +} + +rule integrityOfDistributeMintCapacity(env e) { + address to; + uint256 amount; + + uint256 ownCapacityBefore = mintCapacity(e.msg.sender); + uint256 toCapacityBefore = mintCapacity(to); + + distributeMintCapacity(e, to, amount); + + uint256 ownCapacityAfter = mintCapacity(e.msg.sender); + uint256 toCapacityAfter = mintCapacity(to); + + assert(ownCapacityBefore >= amount); + assert(ownCapacityBefore + toCapacityBefore == ownCapacityAfter + toCapacityAfter); +} + +ghost mapping(address => mathint) mintedTo; +ghost mathint totalMintCapacityChange; +ghost mathint totalMintedChange; + +function _mintCVL(address to, uint256 amount) +{ + mintedTo[to] = mintedTo[to] + amount; + totalMintedChange = totalMintedChange + amount; +} + +hook Sstore KatTokenHarness.mintCapacity[KEY address user] uint256 newCap (uint256 oldCap) { + totalMintCapacityChange = totalMintCapacityChange + newCap - oldCap; +} + +function initGhosts() +{ + totalMintCapacityChange = 0; + totalMintedChange = 0; +} + +rule mintCapacityPlusMintedNeverDecrease(env e, method f) +{ + initGhosts(); + calldataarg args; + f(e, args); + assert totalMintedChange + totalMintCapacityChange >= 0; +} + +rule mintCapacityPlusMintedEqualsDistributedSupplyCap(env e, method f) +{ + initGhosts(); + uint256 distributedSupplyCap_pre = get_distributedSupplyCap(); + calldataarg args; + f(e, args); + uint256 distributedSupplyCap_post = get_distributedSupplyCap(); + assert distributedSupplyCap_post - distributedSupplyCap_pre == + totalMintedChange + totalMintCapacityChange; +} + +/** + * The inflation factor is bounded by MAX_INFLATION. + */ +invariant inflationFactorIsBounded() + inflationFactor() <= MAX_INFLATION(); + +rule integrityOfRenounceInflationAdmin(env e, method f) +{ + address admin_pre = inflationAdmin(); + renounceInflationAdmin(e); + address admin_post = inflationAdmin(); + + assert admin_pre == e.msg.sender; + assert admin_post == 0; +} + +rule integrityOfRenounceInflationBeneficiary(env e, method f) +{ + address beneficiary_pre = inflationBeneficiary(); + renounceInflationBeneficiary(e); + address beneficiary_post = inflationBeneficiary(); + + assert beneficiary_pre == e.msg.sender; + assert beneficiary_post == 0; +} + +// once renounceInflationAdmin is performed, the inflationAdmin will always be zero +// we've proved that renounceInflationAdmin changes it to zero so here we just prove +// that it cannot change from 0 to non-zero +rule inflationAdminValueChange(env e, method f) +{ + requireInvariant zeroAdminThenZeroPendingAdmin(); + address admin_pre = inflationAdmin(); + require e.msg.sender != 0; + calldataarg args; + f(e, args); + address admin_post = inflationAdmin(); + assert admin_pre == 0 => admin_post == 0; +} + +// once renounceInflationBeneficiary is performed, the inflationBeneficiary will always be zero +// we've proved that renounceInflationBeneficiary changes it to zero so here we just prove +// that it cannot change from 0 to non-zero +rule inflationBeneficiaryValueChange(env e, method f) +{ + requireInvariant zeroBeneficiaryThenZeroPendingBeneficiary(); + address beneficiary_pre = inflationBeneficiary(); + require e.msg.sender != 0; + calldataarg args; + f(e, args); + address beneficiary_post = inflationBeneficiary(); + assert beneficiary_pre == 0 => beneficiary_post == 0; +} + +invariant mintCapacityOfZeroIsZero() + mintCapacity(0) == 0 + { preserved + with (env e) + { + requireInvariant noBeneficiaryThenNoInflation(); + require e.msg.sender != 0; + } + } + +invariant noBeneficiaryThenNoInflation() + inflationBeneficiary() == 0 => inflationFactor() == 0 + { preserved with (env e) + { + require e.msg.sender != 0; + } + } + +invariant zeroAdminThenZeroPendingAdmin() + inflationAdmin() == 0 => pendingInflationAdmin() == 0 + { preserved with (env e) + { + require e.msg.sender != 0; + } + } + +invariant zeroBeneficiaryThenZeroPendingBeneficiary() + inflationBeneficiary() == 0 => pendingInflationBeneficiary() == 0 + { preserved with (env e) + { + require e.msg.sender != 0; + } + } \ No newline at end of file diff --git a/certora/specs/KatToken_changeInflation.spec b/certora/specs/KatToken_changeInflation.spec new file mode 100644 index 0000000..bf65302 --- /dev/null +++ b/certora/specs/KatToken_changeInflation.spec @@ -0,0 +1,43 @@ +import "./exp2-summary_stronger.spec"; + +methods { + function inflationAdmin() external returns (address) envfree; + function pendingInflationAdmin() external returns (address) envfree; + function inflationBeneficiary() external returns (address) envfree; + function pendingInflationBeneficiary() external returns (address) envfree; + function inflationFactor() external returns (uint256) envfree; + function MAX_INFLATION() external returns (uint256) envfree; + function merkleMinter() external returns (address) envfree; + function mintCapacity(address) external returns (uint256) envfree; + + //harness methods declared envfree + function get_lastMintCapacityIncrease() external returns (uint256) envfree; + function get_distributedSupplyCap() external returns (uint256) envfree; + + //MerkleProof + function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE; + + function _.eip712Domain() external => NONDET DELETE; +} + +/** + * The inflation factor is bounded by MAX_INFLATION. + */ +invariant inflationFactorIsBounded() + inflationFactor() <= MAX_INFLATION(); + +rule changeInflation_revertConditions(env e) +{ + requireInvariant inflationFactorIsBounded(); + require mintCapacity(inflationBeneficiary()) <= get_distributedSupplyCap(); // implied by mintCapacityPlusMintedEqualsDistributedSupplyCap + uint256 value; + changeInflation@withrevert(e, value); + bool reverted = lastReverted; + assert reverted => + e.msg.sender != inflationAdmin() || + e.msg.value != 0 || + inflationBeneficiary() == 0 || + value > MAX_INFLATION() || + e.block.timestamp > get_lastMintCapacityIncrease() + 100 *365 *24 *60 *60 || // unreasonably high, more than 100 years between calls to distributeInflation + get_distributedSupplyCap() > 10^35; // unreasonably high, causing an overflow. With 3% p.y. the inflation factor can get up to 1.03^100 < 20 while the initial distribution is 1e28 +} diff --git a/certora/specs/MerkleMinter.spec b/certora/specs/MerkleMinter.spec new file mode 100644 index 0000000..29ffe11 --- /dev/null +++ b/certora/specs/MerkleMinter.spec @@ -0,0 +1,170 @@ +methods { + function root() external returns (bytes32) envfree; + function rootSetter() external returns (address) envfree; + function katToken() external returns (address) envfree; + function unlockTime() external returns (uint256) envfree; + function locked() external returns (bool) envfree; + function unlocker() external returns (address) envfree; + function indexIsClaimed(uint256 index) external returns (bool) envfree; + + //MerkleProof + function _.verify(bytes32[], bytes32, bytes32) external => NONDET DELETE; + + function _.eip712Domain() external => NONDET DELETE; +} + +// Once the claiming becomes possible, the contract will never go to a locked state again +rule onceActivatedItStaysActive(env e1, env e2, method f) +{ + require e1.block.timestamp <= e2.block.timestamp; + bool active_pre = (e1.block.timestamp > unlockTime()) || !locked(); + + calldataarg args; + f(e1, args); + bool active_post = (e2.block.timestamp > unlockTime()) || !locked(); + assert active_pre => active_post; +} + +rule integrityOfInit() { + env e; + bytes32 _root; + address _katToken; + + address rootSetterBefore = rootSetter(); + + init(e, _root, _katToken); + + assert(e.msg.sender == rootSetterBefore); + assert(root() == _root); + assert(katToken() == _katToken); +} + +rule integrityOfUnlockAndRenounceUnlocker(env e) { + address currentUnlocker = unlocker(); + unlockAndRenounceUnlocker(e); + + assert(e.msg.sender == currentUnlocker); + assert(locked() == false); + assert(unlocker() == 0); +} + +rule canOnlyClaimWhenNotLocked(env e) +{ + bytes32[] proof; uint256 index; uint256 amount; address receiver; + claimKatToken(e, proof, index, amount, receiver); + + assert(e.block.timestamp > unlockTime() || !locked()); +} + +rule katTokenCannotBeChangedOutsideInit(env e, method f) + filtered { f -> f.selector != sig:init(bytes32, address).selector } + // init is the only method that can set the katToken +{ + address token_pre = katToken(); + calldataarg args; + f(e, args); + address token_post = katToken(); + assert token_pre == token_post; +} + +rule rootCannotBeChangedOutsideInit(env e, method f) + filtered { f -> f.selector != sig:init(bytes32, address).selector } + // init is the only method that can set the root +{ + bytes32 root_pre = root(); + calldataarg args; + f(e, args); + bytes32 root_post = root(); + assert root_pre == root_post; +} + +//locked can only change from true -> false or stay the same +rule lockedValueChange(env e, method f) +{ + bool locked_pre = locked(); + calldataarg args; + f(e, args); + bool locked_post = locked(); + assert locked_post => locked_pre; // if true after then if was already true before, i.e. it cannot go from false to true +} + +//rootSetter can only change from x -> 0 or stay the same +rule rootSetterValueChange(env e, method f) +{ + address rootSetter_pre = rootSetter(); + calldataarg args; + f(e, args); + address rootSetter_post = rootSetter(); + assert rootSetter_post == rootSetter_pre || rootSetter_post == 0; +} + +// indexIsClaimed can only change false -> true or stay the same +rule indexIsClaimedValueChange(env e, method f) +{ + uint256 index; + bool claimed_pre = indexIsClaimed(index); + calldataarg args; + f(e, args); + bool claimed_post = indexIsClaimed(index); + assert claimed_pre => claimed_post; +} + +// indexIsClaimed == true => claimKatToken(..,index) will revert +rule cannotClaimTheIndexTwice(env e) +{ + uint256 index; + bool isClaimed = indexIsClaimed(index); + bytes32[] proof; uint256 amount; address receiver; + + claimKatToken@withrevert(e, proof, index, amount, receiver); + bool reverted = lastReverted; + + assert isClaimed => reverted; +} + +// init cannot be called after the minter is unlocked i.e., after ((block.timestamp > unlockTime) || !locked) +// otherwise some claims could already have happened with a different root +rule cannotInitAfterUnlocked(env e) +{ + bool active = (e.block.timestamp > unlockTime()) || !locked(); + + bytes32 _root; + address _katToken; + init(e, _root, _katToken); + assert !active; // if active, we shouldn't get here as the method shoud revert +} + +rule cannotChangeRootWhenRootSetterIsZero(env e, method f) +{ + bytes32 root_pre = root(); + address rootSetter_pre = rootSetter(); + require e.msg.sender != 0; + calldataarg args; + f(e, args); + bytes32 root_post = root(); + + assert rootSetter_pre == 0 => root_post == root_pre; +} + +rule rootCanBeChanged(env e) +{ + bytes32 root_pre = root(); + bytes32 _root; address _katToken; + init(e, _root, _katToken); + + bytes32 root_post = root(); + satisfy root_pre != root_post; +} + +// It should not be possible to permanently renounce the rootSetter role without actually setting the root first +// We showed that +// 1. root can be changed +// 2. root root cannot change when rootSetter == address(0) +// 3. rootSetter cannot change from address(0) to non-zero, +// so here we just prove that it's not possible to have rootSetter == 0 && root == 0 +// that would already indicate an unrecoverable state +invariant rootCanAlwaysBeSet() + !(rootSetter() == 0 && root() == to_bytes32(0)) + { preserved + with (env e) { require e.msg.sender != 0; } + } \ No newline at end of file diff --git a/certora/specs/exp2-summary.spec b/certora/specs/exp2-summary.spec new file mode 100644 index 0000000..b27d865 --- /dev/null +++ b/certora/specs/exp2-summary.spec @@ -0,0 +1,35 @@ +// Provides a summary for PowUtil.exp2. +// The summary refers to a ghost `ghostExp2` that is restricted by a number of +// simple axioms: +// - exp2(0) == 1 +// - exp2(1) == 2 +// - exp2(x) is monotonically increasing +// - for x>=1, exp2(x) >= 2 +// - for x<=1, exp2(x) <= 2 +// Furthermore, we add axioms based on 3rd-order taylor expansions. We spell out +// the expansion around zero for 0<=x<2 and shift it for higher values of x. +// Similarly, we implement an upper bound by moving the expansion around zero +// to start at x=0, y=4/3. + +methods { + function PowUtil.exp2(uint256 x) internal returns (uint256) => cvlExp2(x); +} + +definition ONE18() returns uint256 = 1000000000000000000; +definition Log2() returns uint256 = 693147180559945309; + +ghost ghostExp2(mathint) returns uint256 { + axiom ghostExp2(0) == ONE18(); + axiom ghostExp2(ONE18()) == 2*ONE18(); + + axiom forall uint256 x1. forall uint256 x2. + x1 > x2 => ghostExp2(x1) >= ghostExp2(x2); + axiom forall uint256 x. + x >= ONE18() => ghostExp2(x) >= 2*ONE18(); + axiom forall uint256 x. + x <= ONE18() => ghostExp2(x) <= 2*ONE18(); +} + +function cvlExp2(uint256 x) returns uint256 { + return ghostExp2(x); +} diff --git a/certora/specs/exp2-summary_stronger.spec b/certora/specs/exp2-summary_stronger.spec new file mode 100644 index 0000000..2ac15d6 --- /dev/null +++ b/certora/specs/exp2-summary_stronger.spec @@ -0,0 +1,62 @@ +// The same as exp2-summary.spec but it adds several additional axioms + +methods { + function PowUtil.exp2(uint256 x) internal returns (uint256) => cvlExp2(x); +} + +definition ONE18() returns uint256 = 1000000000000000000; +definition Log2() returns uint256 = 693147180559945309; + +ghost ghostExp2(mathint) returns uint256 { + axiom ghostExp2(0) == ONE18(); + axiom ghostExp2(ONE18()) == 2*ONE18(); + + axiom ghostExp2(2*ONE18()) == 4*ONE18(); + axiom ghostExp2(3*ONE18()) == 8*ONE18(); + axiom ghostExp2(4*ONE18()) == 16*ONE18(); + axiom ghostExp2(5*ONE18()) == 32*ONE18(); + axiom ghostExp2(6*ONE18()) == 64*ONE18(); + axiom ghostExp2(7*ONE18()) == 128*ONE18(); + axiom ghostExp2(8*ONE18()) == 256*ONE18(); + + axiom forall uint256 x1. forall uint256 x2. + x1 > x2 => ghostExp2(x1) >= ghostExp2(x2); + axiom forall uint256 x. + x >= ONE18() => ghostExp2(x) >= 2*ONE18(); + axiom forall uint256 x. + x <= ONE18() => ghostExp2(x) <= 2*ONE18(); + + // // lower bound + // axiom forall uint256 x. + // ((x >= 0 && x < 2*ONE18()) => ( + // ghostExp2(x) >= + // ONE18() + // + x * Log2() / ONE18() + // + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + // + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + // )) && + // ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 2*ONE18()) * 4)) && + // ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 4*ONE18()) * 16)) && + // ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 6*ONE18()) * 64)) && + // ((x >= 8*ONE18()) => (ghostExp2(x) >= ghostExp2(x - 8*ONE18()) * 256)) + // ; + + // upper bound + axiom forall uint256 x. + ((x >= 0 && x < 2*ONE18()) => ( + ghostExp2(x) <= + 4*ONE18()/3 // rough estimate: this approximation at 2 is about 0.21 to low + + x * Log2() / ONE18() + + x*x * Log2()*Log2() / ONE18()/ONE18()/ONE18() / 2 + + x*x*x * Log2()*Log2()*Log2() /ONE18()/ONE18()/ONE18()/ONE18()/ONE18() / 6 + )) && + ((x >= 2*ONE18() && x < 4*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 2*ONE18()) * 4)) && + ((x >= 4*ONE18() && x < 6*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 4*ONE18()) * 16)) && + ((x >= 6*ONE18() && x < 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 6*ONE18()) * 64)) && + ((x >= 8*ONE18()) => (ghostExp2(x) <= ghostExp2(x - 8*ONE18()) * 256)) + ; +} + +function cvlExp2(uint256 x) returns uint256 { + return ghostExp2(x); +} diff --git a/certora/specs/powUtil.spec b/certora/specs/powUtil.spec new file mode 100644 index 0000000..28220b0 --- /dev/null +++ b/certora/specs/powUtil.spec @@ -0,0 +1,101 @@ +/** + * Check properties on the actual implementation here. + */ + +using KatToken as KatToken; + +methods { + function exp2(uint256 x) external returns (uint256) envfree; + + function KatToken.inflationFactor() external returns (uint256) envfree; + function KatToken.MAX_INFLATION() external returns (uint256) envfree; + function _.eip712Domain() external => NONDET DELETE; +} + +definition ONE18() returns uint256 = 1000000000000000000; +definition daysToSeconds(uint256 days) returns uint256 = assert_uint256(days * 60 * 60 * 24); + +/** + * Show that exp2 is actually exact for some easy values. + */ +rule exp2_correctValues() { + assert(exp2(require_uint256(0 * ONE18())) == 1*ONE18()); + assert(exp2(require_uint256(1 * ONE18())) == 2*ONE18()); + assert(exp2(require_uint256(2 * ONE18())) == 4*ONE18()); + assert(exp2(require_uint256(3 * ONE18())) == 8*ONE18()); + assert(exp2(require_uint256(4 * ONE18())) == 16*ONE18()); +} + +rule exp2_additivity() { + uint256 x; uint256 y; uint256 total; + require total == x + y; + require total <= 5*ONE18(); + + assert exp2(total)*ONE18() == exp2(x) * exp2(y); +} + +rule exp2_additivity2() { + uint256 x; uint256 total; + require total == x + x; + require total <= 5*ONE18(); + + assert exp2(total)*ONE18() == exp2(x) * exp2(x); +} + +rule exp2_correctnes(uint8 n) { + mathint BOUND = 100; + uint256 x = require_uint256(n*ONE18()); + require n <= BOUND; + + assert exp2(x) == (1 << n) * ONE18(); +} + +rule exp2_monotonePlus01(env e) +{ + mathint lBOUND = 0 * ONE18(); + mathint uBOUND = 1 * 10^10; + uint256 x; + require x >= lBOUND; + require x < uBOUND; + + assert exp2(x) <= exp2(require_uint256(x+1)); +} + +rule exp2_monotone12(env e) +{ + mathint lBOUND = 1 * ONE18(); + mathint uBOUND = 2 * ONE18(); + uint256 x; uint256 y; + require x >= lBOUND && y >= lBOUND; + require x < uBOUND && y < uBOUND; + + assert x < y => exp2(x) <= exp2(y); +} + +rule exp2_monotonicityX(env e) +{ + uint256 MIN_INFLATION = 1441974173906322; // log2(1.001) + uint256 MAX_INFLATION = 42644337408493690; // log2(1.03) + uint secondsPerYear = (365 *24 *60 *60); + uint256 minDifference = require_uint256(MIN_INFLATION / secondsPerYear); + + uint256 inflFactor; uint256 timeElapsed; + require inflFactor >= MIN_INFLATION && inflFactor <= MAX_INFLATION; + require timeElapsed <= 7 *24 *60 *60; //one week + + uint256 input = require_uint256(inflFactor * timeElapsed / secondsPerYear); + assert exp2(input) <= exp2(require_uint256(input + minDifference)); +} + +function withinTenPercentTolerance(mathint a, mathint b) returns bool +{ + return 9*a <= 10*b && 9*b <= 10*a; +} + +rule exp2_additivity2X() { + uint256 x; uint256 total; + require total == x + x; + require total <= 5*ONE18(); + + assert withinTenPercentTolerance(exp2(total)*ONE18(), exp2(x) * exp2(x)); +}