Skip to content

Immutable example + direct storage access #49

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
nivcertora merged 7 commits into from
Jan 17, 2024
Merged

Immutable example + direct storage access #49

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
4d66645
Imutable example + direct storage access
nivcertora Jan 15, 2024
0d964ce
fix index
nivcertora Jan 15, 2024
9ba9994
Trigger CI
nivcertora Jan 15, 2024
352dd2a
Trigger CI
nivcertora Jan 15, 2024
5216ab3
Trigger CI
nivcertora Jan 15, 2024
938dabd
Create Readme
nivcertora Jan 16, 2024
59ffba7
.
nivcertora Jan 16, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions CVLByExample/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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),<br> [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) |
Expand All @@ -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),<br> [`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),<br> [`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),<br> [`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),<br> [`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),<br> 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),<br> 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),<br> [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),<br> [`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),<br> 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),<br> 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),<br> [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),<br> [`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),<br> [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),<br> `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),<br> [returning a struct as a tuple](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L21),<br> `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),<br> [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),<br> [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),<br> [`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) |
Expand Down
25 changes: 11 additions & 14 deletions DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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();
}
Expand Down Expand Up @@ -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)) ;
}
Expand All @@ -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);
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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;
}

Expand Down Expand Up @@ -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;
Expand Down
8 changes: 0 additions & 8 deletions DEFI/ConstantProductPool/contracts/correct/ConstantProductPoolFixed.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
17 changes: 17 additions & 0 deletions DEFI/Immutable/Immutable.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
}
}
Loading