diff --git a/CVLByExample/README.md b/CVLByExample/README.md index 9e8e12eb..edbcf4e1 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -3,7 +3,7 @@ | Category | Links | | ----------------- | ----- | | **array** | [In a statement](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L88), [In SStore parameter](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L146), [by function call](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L77),
[Function declaration in method block](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L21) | -| **assert** | [assert](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L75) | +| **assert** | [assert](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L72) | | **assert_uint256** | [assert_uint256](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L180) | | **at** | [at](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L113) | | **builtin rule** | [builtin rule](https://github.com/Certora/Examples/blob/master/CVLByExample/Reentrancy/certora/spec/ReadOnlyReentrancy.spec#L1) | @@ -15,24 +15,24 @@ | **filtered** | [`filtered`](https://github.com/Certora/Examples/blob/master/CVLByExample/Reentrancy/certora/spec/Reentrancy.spec#L29) | | **forall** | [`forall`](https://github.com/Certora/Examples/blob/master/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec#L13) | | **Function call** | [Function call](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L123) | -| **ghost** | [simple variable example](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Full.spec#L72), [ghost mapping](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L118), [ghost function](https://github.com/Certora/Examples/blob/master/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec#L24),
[`init_state`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L219), [`axiom`](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L120), [ghost summary](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/WithGhostSummary.spec#L4) | +| **ghost** | [simple variable example](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Full.spec#L72), [ghost mapping](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L118), [ghost function](https://github.com/Certora/Examples/blob/master/CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec#L24),
[`init_state`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L216), [`axiom`](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L120), [ghost summary](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/GhostSummary/GhostMapping/certora/specs/WithGhostSummary.spec#L4) | | **hook** | [`Sstore`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Full.spec#L88), [`Sload`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Full.spec#L84) | | **import** | [`import`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L1) | -| **invariant** | [Simple Invariant](https://github.com/Certora/Examples/blob/master/CVLByExample/Invariant/certora/specs/BallGame.spec#L7), [strengthening](https://github.com/Certora/Examples/blob/master/CVLByExample/Invariant/certora/specs/BallGameCorrect.spec#L7), [`preserved with (env e)`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Broken.spec#L128),
[`requireInvariant`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L190) | +| **invariant** | [Simple Invariant](https://github.com/Certora/Examples/blob/master/CVLByExample/Invariant/certora/specs/BallGame.spec#L7), [strengthening](https://github.com/Certora/Examples/blob/master/CVLByExample/Invariant/certora/specs/BallGameCorrect.spec#L7), [`preserved with (env e)`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Broken.spec#L128),
[`requireInvariant`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L187) | | **lastreverted** | [`lastreverted`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Broken.spec#L49) | | **laststorage** | [`laststorage`](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L27) | -| **methods block** | [Calls to external contracts](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L29), [envfree](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L19),
Summary [`ALWAYS`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/AlwaysSummary.spec#L4), [`CONSTANT`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/ConstantVSNondet.spec#L5), [DISPATCHER](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L36), [`NONDET`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec#L2), [`HAVOC_ALL`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec#L3),
Summary Application [ALL](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/MultiContract/certora/specs/InternalExternalSummary.spec#L14), [UNRESOLVED](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec#L12), [direct summarization](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec#L9),
[wildcard summarization](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec#L12), [CVL Function Summary](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/WithEnv/WithEnvCVLFunctionSummary/withEnvSummary.spec#L7), [Ghost Summary](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/WithEnv/WithEnvGhostSummary/WithEnv.spec#L10),
[`optional`](https://github.com/Certora/Examples/blob/master/CVLByExample/Optional/certora/specs/Base.spec#L5), ['expect'](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec#L11) | +| **methods block** | [Calls to external contracts](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L26), [envfree](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L19),
Summary [`ALWAYS`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/AlwaysSummary.spec#L4), [`CONSTANT`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/ConstantVSNondet.spec#L5), [DISPATCHER](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L33), [`NONDET`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec#L2), [`HAVOC_ALL`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Keywords/certora/specs/NondetVsHavoc.spec#L3),
Summary Application [ALL](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/MultiContract/certora/specs/InternalExternalSummary.spec#L14), [UNRESOLVED](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec#L12), [direct summarization](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec#L9),
[wildcard summarization](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/Library/DirectSummary/certora/specs/AllDirect.spec#L12), [CVL Function Summary](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/WithEnv/WithEnvCVLFunctionSummary/withEnvSummary.spec#L7), [Ghost Summary](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/WithEnv/WithEnvGhostSummary/WithEnv.spec#L10),
[`optional`](https://github.com/Certora/Examples/blob/master/CVLByExample/Optional/certora/specs/Base.spec#L5), ['expect'](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec#L11) | | **nativeBalances**| [`nativeBalances`](https://github.com/Certora/Examples/blob/master/CVLByExample/NativeBalances/certora/specs/Auction.spec#L24) | | **override** | [`override`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L1), [`definition`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L8), [`function`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L38) | -| **require** | [`require`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L44) | +| **require** | [`require`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L41) | | **require_uint256**| [`require_uint256`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Broken.spec#L156) | | **rule** | [Simple Rule](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/pool_havoc.spec#L27), parameterized [Simple Parameters](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/Full.spec#L78), [Method Parameter](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L95) | -| **satisfy** | [`satisfy`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L255) | +| **satisfy** | [`satisfy`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L252) | | **selector** | [`selector`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L92) | | **sig** | [`sig`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L92) | | **storage** | [of a contract](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L86), [of a ghost](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L149), [of nativeBalances](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L116),
[full storage](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L106), [`laststorage`](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L106), [direct storage access](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L48) | | **struct** | [struct return type](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L47),
`struct` in `methods` block: [struct parameter](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L23), [struct return type](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L19),
[returning a struct as a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L21),
`struct` in a `CVL` function: [struct parameter to a CVL function](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L36),
[struct return type of a CVL function](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L47), [returning struct as a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L53),
[assignment to struct](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L98), [Assigning struct to a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L77) | -| **to_mathint** | [`to_mathint`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L45) | +| **to_mathint** | [`to_mathint`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L42) | | **use** | `rule`: [with filters](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L32), [overriding imported filters](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L32),
[`invariant`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L10): [overriding imported `preserved`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L12), [builtin rule](https://github.com/Certora/Examples/blob/master/CVLByExample/Reentrancy/certora/spec/ReadOnlyReentrancy.spec#L1) | | **using** | [`using`](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/pool_link.spec#L14) | | **withrevert** | [`withrevert`](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L44) | diff --git a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec index 4acb49a0..cd24e23f 100644 --- a/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec +++ b/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec @@ -19,10 +19,7 @@ methods{ function token0() external returns (address) envfree; function token1() external returns (address) envfree; function allowance(address,address) external returns (uint256) envfree; - function balanceOf(address) external returns (uint256) envfree; function totalSupply() external returns (uint256) envfree; - function getReserve0() external returns (uint256) envfree; - function getReserve1() external returns (uint256) envfree; function swap(address tokenIn, address recipient) external returns (uint256) envfree; //calls to external contracts @@ -41,8 +38,8 @@ methods{ function setup(env e){ address zero_address = 0; uint256 MINIMUM_LIQUIDITY = 1000; - require totalSupply() == 0 || balanceOf(zero_address) == MINIMUM_LIQUIDITY; - require balanceOf(zero_address) + balanceOf(e.msg.sender) <= to_mathint(totalSupply()); + require totalSupply() == 0 || currentContract._balances[zero_address] == MINIMUM_LIQUIDITY; + require currentContract._balances[zero_address] + currentContract._balances[e.msg.sender] <= to_mathint(totalSupply()); require _token0 == token0(); require _token1 == token1(); } @@ -96,10 +93,10 @@ rule noDecreaseByOther(method f, address account) { require account != currentContract; uint256 allowance = allowance(account, e.msg.sender); - uint256 before = balanceOf(account); + uint256 before = currentContract._balances[account]; calldataarg args; f(e,args); /* check on all possible arguments */ - uint256 after = balanceOf(account); + uint256 after = currentContract._balances[account]; /* logic implication : true when: (a) the left hand side is false or (b) right hand side is true */ assert after < before => (e.msg.sender == account || to_mathint(allowance) >= (before-after)) ; } @@ -121,8 +118,8 @@ Formula: */ invariant balanceGreaterThanReserve() - (getReserve0() <= _token0.balanceOf(currentContract))&& - (getReserve1() <= _token1.balanceOf(currentContract)) + (currentContract.reserve0 <= _token0.balanceOf(currentContract))&& + (currentContract.reserve1 <= _token1.balanceOf(currentContract)) { preserved with (env e){ setup(e); @@ -157,8 +154,8 @@ Formula: invariant integrityOfTotalSupply() - (totalSupply() == 0 <=> getReserve0() == 0) && - (totalSupply() == 0 <=> getReserve1() == 0) + (totalSupply() == 0 <=> currentContract.reserve0 == 0) && + (totalSupply() == 0 <=> currentContract.reserve1 == 0) { preserved with (env e){ requireInvariant balanceGreaterThanReserve(); @@ -193,11 +190,11 @@ rule monotonicityOfMint(uint256 x, uint256 y, address recipient) { require x > y ; _token0.transfer(eT0, currentContract, x); uint256 amountOut0 = mint(eM,recipient); - uint256 balanceAfter1 = balanceOf(recipient); + uint256 balanceAfter1 = currentContract._balances[recipient]; _token0.transfer(eT0, currentContract, y) at init; uint256 amountOut2 = mint(eM,recipient); - uint256 balanceAfter2 = balanceOf(recipient); + uint256 balanceAfter2 = currentContract._balances[recipient]; assert balanceAfter1 >= balanceAfter2; } @@ -270,7 +267,7 @@ rule zeroWithdrawNoEffect(address to) { env e; setup(e); // The assumption is no skimming - require getReserve0() == _token0.balanceOf(currentContract) && getReserve1() == _token1.balanceOf(currentContract); + require currentContract.reserve1 == _token0.balanceOf(currentContract) && currentContract.reserve1 == _token1.balanceOf(currentContract); storage before = lastStorage; burnSingle(e, _token0, 0, to); storage after = lastStorage; diff --git a/DEFI/ConstantProductPool/contracts/correct/ConstantProductPoolFixed.sol b/DEFI/ConstantProductPool/contracts/correct/ConstantProductPoolFixed.sol index 8456c030..3af02af9 100644 --- a/DEFI/ConstantProductPool/contracts/correct/ConstantProductPoolFixed.sol +++ b/DEFI/ConstantProductPool/contracts/correct/ConstantProductPoolFixed.sol @@ -173,14 +173,6 @@ contract ConstantProductPool is ERC20 { reserve1 = balance1; } - function getReserve0() public view returns (uint256) { - return reserve0; - } - - function getReserve1() public view returns (uint256) { - return reserve1; - } - function _getAmountOut( uint256 amountIn, uint256 reserveAmountIn, diff --git a/DEFI/Immutable/Immutable.sol b/DEFI/Immutable/Immutable.sol new file mode 100644 index 00000000..0342152a --- /dev/null +++ b/DEFI/Immutable/Immutable.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: MIT +import {Owner} from './Owner.sol'; +pragma solidity >=0.8.0; +contract Immutable { + // coding convention to uppercase constant variables + Owner public immutable OWNER; + uint public immutable MY_UINT; + + constructor() { + OWNER = Owner(msg.sender); + MY_UINT = 2; + } + + function getMyUint() public view returns (uint) { + return MY_UINT + 1; + } +} \ No newline at end of file diff --git a/DEFI/Immutable/Immutable.spec b/DEFI/Immutable/Immutable.spec new file mode 100644 index 00000000..8737c8ca --- /dev/null +++ b/DEFI/Immutable/Immutable.spec @@ -0,0 +1,49 @@ + +using Owner as owner; + +methods{ + function getMyUint() external returns uint envfree; + } + +rule OwnerNeverChangedUsingLinking(env e, method f, calldataarg arg){ + address currentOwner; + require currentOwner == owner; + f(e, arg); + assert currentOwner == owner; +} + +rule OwnerNeverChangedUsingCalls(env e, method f, calldataarg arg){ + address currentOwner; + require currentOwner == OWNER(e); + f(e, arg); + assert currentOwner == OWNER(e); +} + +//proved but not related to reality +rule HavocProoved(env e){ + require MY_UINT(e) == 5; + assert getMyUint() == 6; +} + + +// CRITICAL: [main] ERROR ALWAYS - Error in spec file (Immutable.spec:10:1): named pattern root 'MY_UINT' is not defined: did you spell something wrong? Note, named slots are only supported from solc 0.5.13 onward. +// CRITICAL: Encountered an error running Certora Prover: +// CVL specification syntax and type check failed + +// ghost uint ghostUint256; + +// hook Sload uint256 _MY_UINT currentContract.MY_UINT STORAGE { +// require ghostUint256 == _MY_UINT; +// } + +// rule UintNeverChengedUsingGhost(env e, method f, calldataarg args){ +// uint256 currentGhost = ghostUint256; +// f(e, args); +// assert currentGhost == ghostUint256; +// } + + +// Immutable cant be accessed through the direct storage access +// rule DirectStorageAccess(env e){ +// assert currentContract.MY_UINT ==2; +// } \ No newline at end of file diff --git a/DEFI/Immutable/Owner.sol b/DEFI/Immutable/Owner.sol new file mode 100644 index 00000000..7a464874 --- /dev/null +++ b/DEFI/Immutable/Owner.sol @@ -0,0 +1,3 @@ +pragma solidity >=0.8.0; +contract Owner{ +} diff --git a/DEFI/Immutable/PrivateImmutable.sol b/DEFI/Immutable/PrivateImmutable.sol new file mode 100644 index 00000000..552e0422 --- /dev/null +++ b/DEFI/Immutable/PrivateImmutable.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: MIT +import {Owner} from './Owner.sol'; +pragma solidity >=0.8.0; +contract PrivateImmutable { + // coding convention to uppercase constant variables + Owner private immutable OWNER; + uint public immutable MY_UINT; + + constructor() { + OWNER = Owner(msg.sender); + MY_UINT = 2; + } + + function getMyUint() public view returns (uint) { + return MY_UINT + 1; + } +} \ No newline at end of file diff --git a/DEFI/Immutable/Readme.md b/DEFI/Immutable/Readme.md new file mode 100644 index 00000000..fb9e6a18 --- /dev/null +++ b/DEFI/Immutable/Readme.md @@ -0,0 +1,94 @@ +# Immutable Example README + +The Immutable example showcases how to handle Immutable variables in CVL. + +## First Linking to immutable variable works only if the variable is declared public. + +### Public Linking Execution (Immutable.sol): + +To execute on public linking (Immutable.sol), follow these steps: + +```bash +certoraRun runImmutable.conf --server production --prover_version master +``` + +The process involves compiling Immutable.sol and exposing internal function information. The job is then submitted to the server. Track the progress and view results at [Certora Prover](https://prover.certora.com). Once completed, the detailed results will be available at [this link](https://prover.certora.com/output/1512/4fcdf5f50e6a4746a0fa72e6b7f35f51?anonymousKey=ac111a02702ff2ac73842ae71208ad0ec8f3378c). + +### Private Linking Execution (PrivateImmutable.sol - same spec): + +For private linking execution (PrivateImmutable.sol), use the following command: + +```bash +certoraRun runPrivateImmutable.conf --server production --prover_version master +``` + +During this process, Owner.sol and PrivateImmutable.sol are compiled, and internal function information is exposed. However, if an error occurs, such as linking to a variable OWNER that doesn't exist in PrivateImmutable, the Certora Prover will report the issue. + +```bash +CRITICAL: Encountered an error running Certora Prover: +Link to a variable OWNER that doesn't exist in the contract PrivateImmutable, neither as a state variable nor as an immutable. +``` + +## Second: Immutable Variable Hooks + +The hook on the Immutable variable may encounter issues. When attempting to add the specified hook and ghost, execution results in a critical error. The error indicates a problem with the specification file, particularly with the named pattern root 'MY_UINT.' Ensure compatibility with solc version 0.5.13 or later. + +```bash +ghost uint ghostUint256; + +hook Sload uint256 _MY_UINT currentContract.MY_UINT STORAGE { + require ghostUint256 == _MY_UINT; +} + +rule UintNeverChengedUsingGhost(env e, method f, calldataarg args){ + uint256 currentGhost = ghostUint256; + f(e, args); + assert currentGhost == ghostUint256; +} + +CRITICAL: [main] ERROR ALWAYS - Error in spec file (Immutable.spec:10:1): named pattern root 'MY_UINT' is not defined: did you spell something wrong? Note, named slots are only supported from solc 0.5.13 onward. +CRITICAL: Encountered an error running Certora Prover: +CVL specification syntax and type check failed +``` + + +## Third: Proving Assumptions on Immutable Variables + +Proving assumptions on Immutable variables is demonstrated with the following spec and contract: + +#### Specification (spec): + +```solidity +// verified +rule HavocProoved(env e){ + require MY_UINT(e) == 5; + assert getMyUint() == 6; +} +``` + +#### Contract: + +```solidity +uint public immutable MY_UINT; + +constructor() { + OWNER = Owner(msg.sender); + MY_UINT = 2; +} + +function getMyUint() public view returns (uint) { + return MY_UINT + 1; +} +``` + +## Fourth: Direct Storage access doesn't support (without throwing explained error) + +```bash +rule DirectStorageAccess(env e){ + assert currentContract.MY_UINT ==2; +} + +CRITICAL: Found errors +CRITICAL: Encountered an error running Certora Prover: +CVL specification syntax and type check failed +``` \ No newline at end of file diff --git a/DEFI/Immutable/runImmutable.conf b/DEFI/Immutable/runImmutable.conf new file mode 100644 index 00000000..6e32332e --- /dev/null +++ b/DEFI/Immutable/runImmutable.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "Immutable.sol", + "Owner.sol" + ], + "verify": "Immutable:Immutable.spec", + "link": [ + "Immutable:OWNER=Owner" + ], + "rule_sanity": "basic" +} diff --git a/DEFI/Immutable/runPrivateImmutable.conf b/DEFI/Immutable/runPrivateImmutable.conf new file mode 100644 index 00000000..5bb6145f --- /dev/null +++ b/DEFI/Immutable/runPrivateImmutable.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "PrivateImmutable.sol", + "Owner.sol" + ], + "verify": "PrivateImmutable:Immutable.spec", + "link": [ + "PrivateImmutable:OWNER=Owner" + ], + "rule_sanity": "basic" +} diff --git a/DEFI/LiquidityPool/contracts/ERC20.sol b/DEFI/LiquidityPool/contracts/ERC20.sol index fe8d6e4d..af7bd2ee 100644 --- a/DEFI/LiquidityPool/contracts/ERC20.sol +++ b/DEFI/LiquidityPool/contracts/ERC20.sol @@ -1,7 +1,7 @@ pragma solidity >=0.8.0; import "./IERC20.sol"; -abstract contract ERC20 is IERC20{ +abstract contract ERC20 is IERC20{ uint256 private _totalSupply; mapping(address => uint256) private _balanceOf;