Merge pull request #49 from Certora/niv/Immutable-exmple+direct-strorage-access

Immutable example + direct storage access

Author: nivcertora

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),<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) |
@@ -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) |

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;

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,

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;
+    }
+}