Align cli-beta and master

CVLByExample/README.md

@@ -2,20 +2,20 @@
 
 | 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) |
+| **array**         | [In a statement](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L88), [In SStore parameter](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L146), [by function call](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L77),<br> [Function declaration in method block](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L21) |
 | **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/ViewReentrancy.spec#L1) |
 | **calldataarg**   | [calldataarg](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L83) |
-| **cvldoc** | [cvldoc @param](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L44), [cvldoc @title](https://github.com/Certora/Examples/blob/master/CVLByExample/NativeBalances/certora/specs/Auction.spec#L11) |
+| **cvldoc** | [cvldoc @param](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/Structs/BankAccounts/certora/specs/structs.spec#L44), [cvldoc @title](https://github.com/Certora/Examples/blob/master/CVLByExample/NativeBalances/certora/specs/Auction.spec#L11) |
 | **CVL function**  | [CVL function](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/base.spec#L25), [`override`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L38) |
 | **definition**    | [`definition`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/base.spec#L22) |
 | **expect**        | [`expect`](https://github.com/Certora/Examples/blob/master/CVLByExample/Summarization/MultiContract/certora/specs/FunctionSummary.spec#L11) |
 | **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#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) |
+| **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/Types/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/Types/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#L187),<br> [Teams example (`preserved`, `requireInvariant`](Teams/Teams.spec),<br> [Invariant fail without preserved](Teams/NoPreserved.spec) |
@@ -26,7 +26,7 @@
 | **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#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) |
+| **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/Types/Structs/BankAccounts/certora/specs/structs.spec#L95) |
 | **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) |

CVLByExample/TransientStorage/Hooks/runTransientStorage.conf

@@ -4,5 +4,6 @@
   ],
   "verify": "MockMutexer:./Mutexer.spec",
   "solc": "solc8.24", 
-  "solc_evm_version": "cancun"
+  "solc_evm_version": "cancun",
+  "prover_args": ["-enableStorageSplitting false"]
 }

CVLByExample/TransientStorage/PreservedonTransactionBoundary/Vault.sol

@@ -3,8 +3,8 @@ pragma solidity 0.8.24;
 import {CallBacker} from './CallBacker.sol';
 
 contract Vault {
-    bytes32 slot = keccak256("transient");
-    bytes32 lock = keccak256("lock");
+    bytes32 constant slot = keccak256("transient");
+    bytes32 constant lock = keccak256("lock");
     int256 storageValue;
 
     function tload(bytes32 key) internal returns (int) {

DEFI/ERC4626/certora/specs/ERC4626.spec

@@ -477,16 +477,16 @@ function callFunctionsWithReceiverAndOwner(env e, method f, uint256 assets, uint
     if (f.selector == sig:withdraw(uint256,address,address).selector) {
         withdraw(e, assets, receiver, owner);
     }
-    if (f.selector == sig:redeem(uint256,address,address).selector) {
+    else if (f.selector == sig:redeem(uint256,address,address).selector) {
         redeem(e, shares, receiver, owner);
     } 
-    if (f.selector == sig:deposit(uint256,address).selector) {
+    else if (f.selector == sig:deposit(uint256,address).selector) {
         deposit(e, assets, receiver);
     }
-    if (f.selector == sig:mint(uint256,address).selector) {
+    else if (f.selector == sig:mint(uint256,address).selector) {
         mint(e, shares, receiver);
     }
-     if (f.selector == sig:transferFrom(address,address,uint256).selector) {
+    else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
         transferFrom(e, owner, receiver, shares);
     }
     else {

DEFI/LiquidityPool/certora/specs/Full.spec

@@ -254,6 +254,24 @@ rule flashLoanRevertConditions(env e){
     assert isExpectedToRevert <=> lastReverted;
 }
 
+/// Validates that a flash loan generates yield by increase the value of each share (modulo rounding)
+rule flashLoansGenerateYield(address receiver, uint amount) {
+    env e;
+    require e.msg.sender != currentContract;
+
+    uint assetsBefore = depositedAmount();
+    uint sharesBefore = totalSupply();
+    flashLoan(e, receiver, amount);
+    uint assetsAfter = depositedAmount();
+    uint sharesAfter = totalSupply();
+
+    // The total assets held by the contract must increase, while the number of shares remains constant.
+    // The yield might not be reflected in sharesToAmount due to the rounding.
+
+    assert assetsAfter > assetsBefore;
+    assert sharesAfter == sharesBefore;
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Find and show a path for each method.                                                                               │

README.md

@@ -1,3 +1,9 @@
+<div align="center">
+
+[![GitMCP](https://img.shields.io/endpoint?url=https://gitmcp.io/badge/Certora/Examples)](https://gitmcp.io/Certora/Examples)
+[![Twitter Follow](https://img.shields.io/twitter/follow/certorainc?style=social)](https://x.com/certorainc)
+</div>
+
 # Certora Prover and CVL Examples
 This repository contains a collection of examples illustrating CVL usage.
 The specifications are compatible with CVL2.