From ff2bb0cf0b27ed834f7f39a365814f37d7aa8d61 Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Mon, 11 Mar 2024 15:52:49 +0200
Subject: [PATCH 01/10] Update storage.spec

---
 .../Storage/certora/specs/storage.spec        | 27 ++++++++++++++++---
 1 file changed, 23 insertions(+), 4 deletions(-)

diff --git a/CVLByExample/Storage/certora/specs/storage.spec b/CVLByExample/Storage/certora/specs/storage.spec
index d7171b3b..961232c6 100644
--- a/CVLByExample/Storage/certora/specs/storage.spec
+++ b/CVLByExample/Storage/certora/specs/storage.spec
@@ -94,23 +94,42 @@ rule integrityOfStoragePerCustomerShouldPass(BankAccountRecord.Customer c1, Bank
 
 /// This rule demonstrates how to call `deposit` (can be any transaction) twice from the same state by restoring the storage to
 /// its initial state before the second call.
+rule storageAfterTwoDepositFromInitDoesNotChange() {
+    uint256 bankAccount;
+    env e;
+    require e.msg.sender < max_address;
+    // uint256 initBalance = nativeBalances[bank];
+    storage initStorage = lastStorage;
+    deposit(e, bankAccount);
+    // Only full storage can be assigned to a variable.
+    storage afterCallStorage = lastStorage;
+    // nativeBalances is mapping(address => uint256. mapping is not yet supported as a CVL local variable type, so a variable
+    // corresponds to a single entry is used instead.
+    uint256 afterCallBalance = nativeBalances[bank];
+    deposit(e, bankAccount) at initStorage;
+    assert (nativeBalances[bank] == afterCallBalance, "Different native balances from same initial storage");
+    assert(lastStorage[bank] == afterCallStorage[bank], "Different native storage from same initial storage");
+    assert(lastStorage[nativeBalances] == afterCallStorage[nativeBalances], 
+        "Different storage of native balances after call from same initial storage");
+}
+
 /// Two withdrawals are sequentially called where both start from the initial state. Therefore, the storage after each of the
 /// withdrawals are the same.
 /// This fails in the default configuration because of the call to an unresolved function in withdraw. 
-/// It passes with -optimistic_fallback.
-rule storageAfterTwoDepositFromInitDoesNotChangeShouldPass() {
+/// It passes with --optimistic_fallback.
+rule storageAfterTwoWithdrawalsFromInitDoesNotChange() {
     uint256 bankAccount;
     env e;
     require e.msg.sender < max_address;
     // uint256 initBalance = nativeBalances[bank];
     storage initStorage = lastStorage;
-    deposit(e, bankAccount);
+    withdraw(e, bankAccount);
     // Only full storage can be assigned to a variable.
     storage afterCallStorage = lastStorage;
     // nativeBalances is mapping(address => uint256. mapping is not yet supported as a CVL local variable type, so a variable
     // corresponds to a single entry is used instead.
     uint256 afterCallBalance = nativeBalances[bank];
-    deposit(e, bankAccount) at initStorage;
+    withdraw(e, bankAccount) at initStorage;
     assert (nativeBalances[bank] == afterCallBalance, "Different native balances from same initial storage");
     assert(lastStorage[bank] == afterCallStorage[bank], "Different native storage from same initial storage");
     assert(lastStorage[nativeBalances] == afterCallStorage[nativeBalances], 

From df4364c084a1db66d34a3b44de2a31211b124943 Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Mon, 11 Mar 2024 16:37:40 +0200
Subject: [PATCH 02/10] optimistic_fallback

---
 CLIFlags/README.md                              |  1 +
 CLIFlags/optimistic_fallback.conf               | 14 ++++++++++++++
 CVLByExample/Storage/README.md                  |  2 +-
 CVLByExample/Storage/certora/specs/storage.spec |  4 ++--
 4 files changed, 18 insertions(+), 3 deletions(-)
 create mode 100644 CLIFlags/optimistic_fallback.conf

diff --git a/CLIFlags/README.md b/CLIFlags/README.md
index fbd1bf01..99135d6d 100644
--- a/CLIFlags/README.md
+++ b/CLIFlags/README.md
@@ -22,6 +22,7 @@ For more information about available CLI options go to: https://docs.certora.com
 | [--solc_allow_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-allow-path) | Every conf example in this folder has it. |
 | [--packages_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages-path) | |
 | [--packages](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages) | |
+| --optimistic_fallback | [false](https://prover.certora.com/output/15800/5f15bade773a4d5c9494408d3751156c?anonymousKey=c28bae503fe3444c21adc2971bda5a2f74e685cc) / [true](https://prover.certora.com/output/15800/a23a21a8ef9642ba83d97547fc361b70?anonymousKey=596e02bc0b6976504873489348d118bdbb2abb7f) |
 | [--optimistic_loop](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-loop) | [false](https://prover.certora.com/output/15800/8db8b5eaeb244ba490394e05edac0fe1?anonymousKey=5067d0c0908cc2f1cb348e8b163bfec327884cee) / [true](https://prover.certora.com/output/15800/89e59b62f44f439c9502363cef4e7b49?anonymousKey=bac549ca44168b6e0b282a980240c247b34d77ee) |
 | [--loop_iter](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#loop-iter) | [A run with 1 loop unrolling](https://prover.certora.com/output/15800/9b085d85bcc345d5bd2612f8bea5da98?anonymousKey=a6c544d73525dcb582eba2b971d85d97c16b35db) / [Same run with 3 loop unrolling](https://prover.certora.com/output/15800/0b152fe8cfcc41168429a287fa2ba7f8?anonymousKey=38fd94f0ac9bd36f3cecb23d8275b23b864e2d77) |
 | [--optimistic_summary_recursion](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-summary-recursion) | |
diff --git a/CLIFlags/optimistic_fallback.conf b/CLIFlags/optimistic_fallback.conf
new file mode 100644
index 00000000..65aff557
--- /dev/null
+++ b/CLIFlags/optimistic_fallback.conf
@@ -0,0 +1,14 @@
+{
+  "files": [
+    "../CVLByExample/Structs/BankAccounts/Bank.sol"
+  ],
+  "verify": "Bank:../CVLByExample/Storage/certora/specs/storage.spec",
+  //Allow going to contract fallback function on unresolved.
+  "optimistic_fallback": true,
+  
+  "optimistic_loop": true,
+  "loop_iter": "3",
+  "multi_assert_check": true,
+  "rule_sanity": "basic",
+  "solc_allow_path": "../"
+}
\ No newline at end of file
diff --git a/CVLByExample/Storage/README.md b/CVLByExample/Storage/README.md
index 8b2afa20..1ab8641c 100644
--- a/CVLByExample/Storage/README.md
+++ b/CVLByExample/Storage/README.md
@@ -18,5 +18,5 @@ Run this configuration via:
 
 ```certoraRun runStorage.conf```
 
-[Report of this run](https://prover.certora.com/output/15800/99b53a463b524e35ae8f0d31534785cd?anonymousKey=11428309d8ae62ecb8ae41811146878f1207e4ce)
+[Report of this run](https://prover.certora.com/output/15800/915c17159838441a9ecf6fd5672b033d?anonymousKey=176943c3b4df8b5b92bc346545be02f072516013)
 
diff --git a/CVLByExample/Storage/certora/specs/storage.spec b/CVLByExample/Storage/certora/specs/storage.spec
index 961232c6..ff2fabac 100644
--- a/CVLByExample/Storage/certora/specs/storage.spec
+++ b/CVLByExample/Storage/certora/specs/storage.spec
@@ -49,7 +49,7 @@ rule storageDoesNotChangeByWithdrawWhenRevert() {
 /// This rule demonstrates how to verify changes in the full storage when changing data structures of the current contract.
 /// The storage changes after each customer addition.
 /// The rule Should pass.
-rule addingCustomersChangesStorageShouldPass(BankAccountRecord.Customer c1, BankAccountRecord.Customer c2) {
+rule addingCustomersChangesStorage(BankAccountRecord.Customer c1, BankAccountRecord.Customer c2) {
     require c1.id != c2.id;
     addCustomer(c1);
     storage afterC1 = lastStorage;
@@ -72,7 +72,7 @@ rule witnessForStorageChangeAfterEachCustomerAddition(BankAccountRecord.Customer
 /// This rule demonstrates how to compare the storage of a specific contract and nativeBalances in several
 /// points of the run using several variables and indices.
 /// Different storage after each customer addition.
-rule integrityOfStoragePerCustomerShouldPass(BankAccountRecord.Customer c1, BankAccountRecord.Customer c2) {
+rule integrityOfStoragePerCustomer(BankAccountRecord.Customer c1, BankAccountRecord.Customer c2) {
     require c1.id != c2.id;
     require !isCustomer(c1.id);
     require !isCustomer(c2.id);

From 35f4a7810f37996728471d25a86705c4a000290b Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Mon, 11 Mar 2024 23:41:21 +0200
Subject: [PATCH 03/10] recursion flags

---
 CLIFlags/Helpers/Fibonacci.sol              | 13 +++++++++++++
 CLIFlags/Helpers/Fibonacci.spec             | 14 ++++++++++++++
 CLIFlags/README.md                          |  2 ++
 CLIFlags/contract_recursion_limit.conf      | 10 ++++++++++
 CLIFlags/optimistic_contract_recursion.conf | 11 +++++++++++
 5 files changed, 50 insertions(+)
 create mode 100644 CLIFlags/Helpers/Fibonacci.sol
 create mode 100644 CLIFlags/Helpers/Fibonacci.spec
 create mode 100644 CLIFlags/contract_recursion_limit.conf
 create mode 100644 CLIFlags/optimistic_contract_recursion.conf

diff --git a/CLIFlags/Helpers/Fibonacci.sol b/CLIFlags/Helpers/Fibonacci.sol
new file mode 100644
index 00000000..6aa7ba8a
--- /dev/null
+++ b/CLIFlags/Helpers/Fibonacci.sol
@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+
+pragma solidity >=0.8.0;
+
+
+contract Fibonacci {
+    function fibonacci(uint32 i) external returns (uint32) {
+        if(i == 1 || i == 2) {
+            return 1;
+        }
+        return this.fibonacci(i- 1) + this.fibonacci(i - 2);
+    }
+}
\ No newline at end of file
diff --git a/CLIFlags/Helpers/Fibonacci.spec b/CLIFlags/Helpers/Fibonacci.spec
new file mode 100644
index 00000000..7a536745
--- /dev/null
+++ b/CLIFlags/Helpers/Fibonacci.spec
@@ -0,0 +1,14 @@
+methods {
+    function fibonacci(uint32) external returns (uint32) envfree;
+}
+
+rule fibonacciMonotonicallyIncreasing {
+    uint32 i1;
+    uint32 i2;
+
+    assert i2 > i1 => fibonacci(i2) >= fibonacci(i1);
+}
+
+rule fifthFibonacciElementIsFive {
+    assert fibonacci(5) == 5;
+}
diff --git a/CLIFlags/README.md b/CLIFlags/README.md
index 99135d6d..3f665375 100644
--- a/CLIFlags/README.md
+++ b/CLIFlags/README.md
@@ -25,6 +25,8 @@ For more information about available CLI options go to: https://docs.certora.com
 | --optimistic_fallback | [false](https://prover.certora.com/output/15800/5f15bade773a4d5c9494408d3751156c?anonymousKey=c28bae503fe3444c21adc2971bda5a2f74e685cc) / [true](https://prover.certora.com/output/15800/a23a21a8ef9642ba83d97547fc361b70?anonymousKey=596e02bc0b6976504873489348d118bdbb2abb7f) |
 | [--optimistic_loop](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-loop) | [false](https://prover.certora.com/output/15800/8db8b5eaeb244ba490394e05edac0fe1?anonymousKey=5067d0c0908cc2f1cb348e8b163bfec327884cee) / [true](https://prover.certora.com/output/15800/89e59b62f44f439c9502363cef4e7b49?anonymousKey=bac549ca44168b6e0b282a980240c247b34d77ee) |
 | [--loop_iter](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#loop-iter) | [A run with 1 loop unrolling](https://prover.certora.com/output/15800/9b085d85bcc345d5bd2612f8bea5da98?anonymousKey=a6c544d73525dcb582eba2b971d85d97c16b35db) / [Same run with 3 loop unrolling](https://prover.certora.com/output/15800/0b152fe8cfcc41168429a287fa2ba7f8?anonymousKey=38fd94f0ac9bd36f3cecb23d8275b23b864e2d77) |
+| --optimistic_contract_recursion | [false](https://prover.certora.com/output/15800/908365f5dfb04e2b9a6d0dfef3a7c006?anonymousKey=2db3842d23c9fb7a6065551ed56fc9bdfa815595) / [true](https://prover.certora.com/output/15800/65a836c4a9f542f79ad7e2fd563a8a18?anonymousKey=2bb9bcbad7f489038331183b3e6573fec4235c73) |
+| --contract_recursion_limit | [A run with limit of 1 recursion calls](https://prover.certora.com/output/15800/e2b6169b29af4a1a984a12cfb7192754?anonymousKey=8377c4f7bc0388ede45cef5aac6bfe6746471bec) / [Same run but with limit of 5](https://prover.certora.com/output/15800/e30361434d7d4f90835977a131226ea3?anonymousKey=6a06425fa5a78281927156369530d28fca0578a6) |
 | [--optimistic_summary_recursion](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-summary-recursion) | |
 | [--summary_recursion_limit](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#summary-recursion-limit) | |
 | [--optimistic_hashing](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-hashing) | |
diff --git a/CLIFlags/contract_recursion_limit.conf b/CLIFlags/contract_recursion_limit.conf
new file mode 100644
index 00000000..2ab08892
--- /dev/null
+++ b/CLIFlags/contract_recursion_limit.conf
@@ -0,0 +1,10 @@
+{
+    "files": [
+        "Helpers/Fibonacci.sol"
+    ],
+    "verify": "Fibonacci:Helpers/Fibonacci.spec",
+    // Specify the allowed number of recursion calls.
+    "contract_recursion_limit": "5",
+
+    "rule": ["fifthFibonacciElementIsFive"]
+}
\ No newline at end of file
diff --git a/CLIFlags/optimistic_contract_recursion.conf b/CLIFlags/optimistic_contract_recursion.conf
new file mode 100644
index 00000000..7acf9350
--- /dev/null
+++ b/CLIFlags/optimistic_contract_recursion.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "Helpers/Fibonacci.sol"
+    ],
+    "verify": "Fibonacci:Helpers/Fibonacci.spec",
+    // Turn on optimistic contract recursion.
+    "optimistic_contract_recursion": true,
+
+    "contract_recursion_limit": "1",
+    "rule": ["fibonacciMonotonicallyIncreasing"]
+}
\ No newline at end of file

From 8355972cc5e1ab47a38af62490e9c64b51240c3a Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Tue, 12 Mar 2024 19:45:14 +0200
Subject: [PATCH 04/10] wildcard vs exact

---
 .../Summarization/AutoSummary/README.md       |   9 +
 .../Summarization/AutoSummary/SqrRoot.sol     | 246 ++++++++++++++++++
 .../Summarization/AutoSummary/SqrRoot.spec    |  15 ++
 .../Summarization/AutoSummary/runSqrRoot.conf |   9 +
 .../Summarization/WildcardVsExact/README.md   |  22 ++
 .../WildcardVsExact/contracts/A.sol           |  13 +
 .../WildcardVsExact/contracts/B.sol           |   8 +
 .../WildcardVsExact/runWilcardVsExact.conf    |  11 +
 .../specs/WildcardVsExact.spec                |  15 ++
 9 files changed, 348 insertions(+)
 create mode 100644 CVLByExample/Summarization/AutoSummary/README.md
 create mode 100644 CVLByExample/Summarization/AutoSummary/SqrRoot.sol
 create mode 100644 CVLByExample/Summarization/AutoSummary/SqrRoot.spec
 create mode 100644 CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
 create mode 100644 CVLByExample/Summarization/WildcardVsExact/README.md
 create mode 100644 CVLByExample/Summarization/WildcardVsExact/contracts/A.sol
 create mode 100644 CVLByExample/Summarization/WildcardVsExact/contracts/B.sol
 create mode 100644 CVLByExample/Summarization/WildcardVsExact/runWilcardVsExact.conf
 create mode 100644 CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec

diff --git a/CVLByExample/Summarization/AutoSummary/README.md b/CVLByExample/Summarization/AutoSummary/README.md
new file mode 100644
index 00000000..f3ff07eb
--- /dev/null
+++ b/CVLByExample/Summarization/AutoSummary/README.md
@@ -0,0 +1,9 @@
+
+
+To run this spec:
+
+```certoraRun.py runSqrRoot.conf```
+
+[A report of this run](https://prover.certora.com/output/15800/cff390126cf44336be35c571165952d9?anonymousKey=c3faa490ac0613f3dd1e77f761ab0ddad8a9a3d7)
+
+
diff --git a/CVLByExample/Summarization/AutoSummary/SqrRoot.sol b/CVLByExample/Summarization/AutoSummary/SqrRoot.sol
new file mode 100644
index 00000000..8134957f
--- /dev/null
+++ b/CVLByExample/Summarization/AutoSummary/SqrRoot.sol
@@ -0,0 +1,246 @@
+// SPDX-License-Identifier: MIT
+
+contract SqrRoot{
+    IERC20 public immutable token0;
+    IERC20 public immutable token1;
+
+    uint256 public reserve0;
+    uint256 public reserve1;
+
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+
+    constructor(address _token0, address _token1) {
+        token0 = IERC20(_token0);
+        token1 = IERC20(_token1);
+    }
+
+    function _mint(address _to, uint256 _amount) private {
+        balanceOf[_to] += _amount;
+        totalSupply += _amount;
+    }
+
+    function _burn(address _from, uint256 _amount) private {
+        balanceOf[_from] -= _amount;
+        totalSupply -= _amount;
+    }
+
+    function _update(uint256 _reserve0, uint256 _reserve1) private {
+        reserve0 = _reserve0;
+        reserve1 = _reserve1;
+    }
+
+    function swap(address _tokenIn, uint256 _amountIn) external returns (uint256 amountOut) {
+        require(
+            _tokenIn == address(token0) || _tokenIn == address(token1),
+            "invalid token"
+        );
+        require(_amountIn > 0, "amount in = 0");
+
+        bool isToken0 = _tokenIn == address(token0);
+        (IERC20 tokenIn, IERC20 tokenOut, uint256 reserveIn, uint256 reserveOut) = isToken0
+            ? (token0, token1, reserve0, reserve1)
+            : (token1, token0, reserve1, reserve0);
+
+        tokenIn.transferFrom(msg.sender, address(this), _amountIn);
+
+        /*
+        How much dy for dx?
+
+        xy = k
+        (x + dx)(y - dy) = k
+        y - dy = k / (x + dx)
+        y - k / (x + dx) = dy
+        y - xy / (x + dx) = dy
+        (yx + ydx - xy) / (x + dx) = dy
+        ydx / (x + dx) = dy
+        */
+        // 0.3% fee
+        uint256 amountInWithFee = (_amountIn * 997) / 1000;
+        amountOut = (reserveOut * amountInWithFee) / (reserveIn + amountInWithFee);
+
+        tokenOut.transfer(msg.sender, amountOut);
+
+        _update(token0.balanceOf(address(this)), token1.balanceOf(address(this)));
+    }
+
+    function addLiquidity(uint256 _amount0, uint256 _amount1) external returns (uint256 shares) {
+        token0.transferFrom(msg.sender, address(this), _amount0);
+        token1.transferFrom(msg.sender, address(this), _amount1);
+
+        /*
+        How much dx, dy to add?
+
+        xy = k
+        (x + dx)(y + dy) = k'
+
+        No price change, before and after adding liquidity
+        x / y = (x + dx) / (y + dy)
+
+        x(y + dy) = y(x + dx)
+        x * dy = y * dx
+
+        x / y = dx / dy
+        dy = y / x * dx
+        */
+        require (reserve0 > 0 && reserve1 > 0);
+        if (reserve0 > 0 || reserve1 > 0) {
+            require(reserve0 * _amount1 == reserve1 * _amount0, "x / y != dx / dy");
+        }
+
+        /*
+        How much shares to mint?
+
+        f(x, y) = value of liquidity
+        We will define f(x, y) = sqrt(xy)
+
+        L0 = f(x, y)
+        L1 = f(x + dx, y + dy)
+        T = total shares
+        s = shares to mint
+
+        Total shares should increase proportional to increase in liquidity
+        L1 / L0 = (T + s) / T
+
+        L1 * T = L0 * (T + s)
+
+        (L1 - L0) * T / L0 = s 
+        */
+
+        /*
+        Claim
+        (L1 - L0) / L0 = dx / x = dy / y
+
+        Proof
+        --- Equation 1 ---
+        (L1 - L0) / L0 = (sqrt((x + dx)(y + dy)) - sqrt(xy)) / sqrt(xy)
+        
+        dx / dy = x / y so replace dy = dx * y / x
+
+        --- Equation 2 ---
+        Equation 1 = (sqrt(xy + 2ydx + dx^2 * y / x) - sqrt(xy)) / sqrt(xy)
+
+        Multiply by sqrt(x) / sqrt(x)
+        Equation 2 = (sqrt(x^2y + 2xydx + dx^2 * y) - sqrt(x^2y)) / sqrt(x^2y)
+                   = (sqrt(y)(sqrt(x^2 + 2xdx + dx^2) - sqrt(x^2)) / (sqrt(y)sqrt(x^2))
+        
+        sqrt(y) on top and bottom cancels out
+
+        --- Equation 3 ---
+        Equation 2 = (sqrt(x^2 + 2xdx + dx^2) - sqrt(x^2)) / (sqrt(x^2)
+        = (sqrt((x + dx)^2) - sqrt(x^2)) / sqrt(x^2)  
+        = ((x + dx) - x) / x
+        = dx / x
+
+        Since dx / dy = x / y,
+        dx / x = dy / y
+
+        Finally
+        (L1 - L0) / L0 = dx / x = dy / y
+        */
+
+        if (totalSupply == 0) {
+            shares = sqrt(_amount0 * _amount1);
+        } else {
+            shares = _min(
+                (_amount0 * totalSupply) / reserve0,
+                (_amount1 * totalSupply) / reserve1
+            );
+        }
+        require(shares > 0, "shares = 0");
+        _mint(msg.sender, shares);
+
+        _update(token0.balanceOf(address(this)), token1.balanceOf(address(this)));
+    }
+
+    function removeLiquidity(
+        uint256 _shares
+    ) external returns (uint256 amount0, uint256 amount1) {
+        /*
+        Claim
+        dx, dy = amount of liquidity to remove
+        dx = s / T * x
+        dy = s / T * y
+
+        Proof
+        Let's find dx, dy such that
+        v / L = s / T
+        
+        where
+        v = f(dx, dy) = sqrt(dxdy)
+        L = total liquidity = sqrt(xy)
+        s = shares
+        T = total supply
+
+        --- Equation 1 ---
+        v = s / T * L
+        sqrt(dxdy) = s / T * sqrt(xy)
+
+        Amount of liquidity to remove must not change price so 
+        dx / dy = x / y
+
+        replace dy = dx * y / x
+        sqrt(dxdy) = sqrt(dx * dx * y / x) = dx * sqrt(y / x)
+
+        Divide both sides of Equation 1 with sqrt(y / x)
+        dx = s / T * sqrt(xy) / sqrt(y / x)
+           = s / T * sqrt(x^2) = s / T * x
+
+        Likewise
+        dy = s / T * y
+        */
+
+        // bal0 >= reserve0
+        // bal1 >= reserve1
+        uint256 bal0 = token0.balanceOf(address(this));
+        uint256 bal1 = token1.balanceOf(address(this));
+
+        amount0 = (_shares * bal0) / totalSupply;
+        amount1 = (_shares * bal1) / totalSupply;
+        require(amount0 > 0 && amount1 > 0, "amount0 or amount1 = 0");
+
+        _burn(msg.sender, _shares);
+        _update(bal0 - amount0, bal1 - amount1);
+
+        token0.transfer(msg.sender, amount0);
+        token1.transfer(msg.sender, amount1);
+    }
+
+    function sqrt(uint256 y) public pure returns (uint256 z) {
+        if (y > 3) {
+            z = y;
+            uint256 x = y / 2 + 1;
+            while (x < z) {
+                z = x;
+                x = (y / x + x) / 2;
+            }
+        } else if (y != 0) {
+            z = 1;
+        }
+    }
+
+    function _min(uint256 x, uint256 y) private pure returns (uint256) {
+        return x <= y ? x : y;
+    }
+}
+
+interface IERC20 {
+    function totalSupply() external view returns (uint256);
+
+    function balanceOf(address account) external view returns (uint256);
+
+    function transfer(address recipient, uint256 amount) external returns (bool);
+
+    function allowance(address owner, address spender) external view returns (uint256);
+
+    function approve(address spender, uint256 amount) external returns (bool);
+
+    function transferFrom(
+        address sender,
+        address recipient,
+        uint256 amount
+    ) external returns (bool);
+
+    event Transfer(address indexed from, address indexed to, uint256 amount);
+    event Approval(address indexed owner, address indexed spender, uint256 amount);
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/AutoSummary/SqrRoot.spec b/CVLByExample/Summarization/AutoSummary/SqrRoot.spec
new file mode 100644
index 00000000..7d98b265
--- /dev/null
+++ b/CVLByExample/Summarization/AutoSummary/SqrRoot.spec
@@ -0,0 +1,15 @@
+/*
+methods {
+    function sqrt(uint256 y) internal returns (uint256);
+}
+*/
+
+rule addLiquidityMonotonicity(uint256 amount0, uint256 amount1, uint256 amount2, uint256 amount3) {
+    env e;
+    storage initStorage = lastStorage;
+    uint256 firstAdd = addLiquidity(e, amount0, amount1);
+    uint256 secondAdd = addLiquidity(e, amount2, amount3) at initStorage;
+    assert ((amount0 <= amount2 || amount1 <= amount3) => 
+            (firstAdd <= secondAdd), 
+            "addLiquidity is not monotonic");
+}
diff --git a/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf b/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
new file mode 100644
index 00000000..e5f98e09
--- /dev/null
+++ b/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
@@ -0,0 +1,9 @@
+{
+  "files": [
+    "SqrRoot.sol",
+  ],
+  "verify": "SqrRoot:SqrRoot.spec",
+  "optimistic_loop": true,
+  "loop_iter": "4",
+  "rule_sanity": "basic"
+}
diff --git a/CVLByExample/Summarization/WildcardVsExact/README.md b/CVLByExample/Summarization/WildcardVsExact/README.md
new file mode 100644
index 00000000..53e6ad00
--- /dev/null
+++ b/CVLByExample/Summarization/WildcardVsExact/README.md
@@ -0,0 +1,22 @@
+# What happens when a function has both exact and wildcard summarizations?
+
+When a function matches a wildcard summarization but also has an exact summarization, the exact summarization will be used to summarize
+this function. We will demonstrate such case using a simple example.
+
+We have 2 very simple contracts: `A` (in `A.sol`) and `B` (in `B.sol`).
+`A` holds a reference to `B` and has a simple function `callAFunc` that call the function `toBeSummarized` from B and returns it.
+The function toBeSummarized just returns 0.
+
+The spec `WildcardVsExact.spec` defines 2 different summarizations:
+* A wildcard summarization that will match a `toBeSummarized()` signature from any contract in the scene. This summarization returns 5.
+* An exact summarization to `B.toBeSummarized()` that returns 7.
+
+The spec also include 2 simple rules: `isFive` and `isSeven` that asserts that `callAFunc` returns 5 and 7 respectively.
+
+Run this spec via
+```certoraRun runWildcardVsExact.conf```
+
+[The report of this run](https://prover.certora.com/output/15800/cbdf895a0130407e9997def721834bc3?anonymousKey=ae82616d3ac4a4b608bd41d5c6d1a6b0e1bbe836)
+
+As you can see `isFive` fails because the wildcard summarization was not used. But `isSeven` passes because the exact summarization was used
+instead of calling the actual function that would have returned 0.
diff --git a/CVLByExample/Summarization/WildcardVsExact/contracts/A.sol b/CVLByExample/Summarization/WildcardVsExact/contracts/A.sol
new file mode 100644
index 00000000..4e7ba3c2
--- /dev/null
+++ b/CVLByExample/Summarization/WildcardVsExact/contracts/A.sol
@@ -0,0 +1,13 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+pragma solidity >=0.8.0;
+
+import "./B.sol";
+
+contract A {
+
+    B public other;
+
+    function callAFunc() external returns (uint256) {
+        return other.toBeSummarized();
+    }
+}
diff --git a/CVLByExample/Summarization/WildcardVsExact/contracts/B.sol b/CVLByExample/Summarization/WildcardVsExact/contracts/B.sol
new file mode 100644
index 00000000..b5a884bd
--- /dev/null
+++ b/CVLByExample/Summarization/WildcardVsExact/contracts/B.sol
@@ -0,0 +1,8 @@
+// SPDX-License-Identifier: AGPL-3.0-only
+pragma solidity >=0.8.0;
+
+contract B {
+    function toBeSummarized() external returns (uint256) {
+        return 0;
+    }
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/WildcardVsExact/runWilcardVsExact.conf b/CVLByExample/Summarization/WildcardVsExact/runWilcardVsExact.conf
new file mode 100644
index 00000000..84ea252e
--- /dev/null
+++ b/CVLByExample/Summarization/WildcardVsExact/runWilcardVsExact.conf
@@ -0,0 +1,11 @@
+{
+    "files": [
+        "contracts/A.sol",
+        "contracts/B.sol"
+    ],
+    "link": [
+        "A:other=B"
+    ],
+    "verify": "A:specs/WildcardVsExact.spec",
+    "msg": "Wildcard summary vs exact summary"
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec b/CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec
new file mode 100644
index 00000000..cdff934d
--- /dev/null
+++ b/CVLByExample/Summarization/WildcardVsExact/specs/WildcardVsExact.spec
@@ -0,0 +1,15 @@
+using B as B;
+
+methods {
+    function callAFunc() external returns (uint256) envfree;
+    function _.toBeSummarized() external => ALWAYS(5) ALL;
+    function B.toBeSummarized() external returns(uint256) => ALWAYS(7) ALL;
+}
+
+rule isFive {
+    assert callAFunc() == 5;
+}
+
+rule isSeven {
+    assert callAFunc() == 7;
+}
\ No newline at end of file

From 00e28a38ac74c44402daaa57338fcfbdcefd63c6 Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Wed, 13 Mar 2024 00:06:11 +0200
Subject: [PATCH 05/10] autosummary does nothing :(

---
 CVLByExample/Summarization/AutoSummary/README.md       | 6 +++---
 CVLByExample/Summarization/AutoSummary/runSqrRoot.conf | 3 ++-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/CVLByExample/Summarization/AutoSummary/README.md b/CVLByExample/Summarization/AutoSummary/README.md
index f3ff07eb..218c2b4a 100644
--- a/CVLByExample/Summarization/AutoSummary/README.md
+++ b/CVLByExample/Summarization/AutoSummary/README.md
@@ -1,9 +1,9 @@
-
+**NEED TO CHECK THIS EXAMPLE**
 
 To run this spec:
 
 ```certoraRun.py runSqrRoot.conf```
 
-[A report of this run](https://prover.certora.com/output/15800/cff390126cf44336be35c571165952d9?anonymousKey=c3faa490ac0613f3dd1e77f761ab0ddad8a9a3d7)
-
+[A report of this run without autosummary](https://prover.certora.com/output/15800/0219068978f14c2a8c78ba5ebbb60feb?anonymousKey=5df460072f757b068c0683b04a32eb6de5d49c47)
 
+[A report of this run with autosummary](https://prover.certora.com/output/15800/53388c908d75493caf9fd93c6bb2ed0f?anonymousKey=33e05fe8eaf39f2aee1eab7f44c17d380b02ed0b)
diff --git a/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf b/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
index e5f98e09..d9262cc4 100644
--- a/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
+++ b/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
@@ -4,6 +4,7 @@
   ],
   "verify": "SqrRoot:SqrRoot.spec",
   "optimistic_loop": true,
-  "loop_iter": "4",
+  "auto_nondet_difficult_internal_funcs": true,
+  "loop_iter": "6",
   "rule_sanity": "basic"
 }

From ec84089c2472d6cff68f18e083d5dc6826731992 Mon Sep 17 00:00:00 2001
From: Nurit Dor <57101353+nd-certora@users.noreply.github.com>
Date: Wed, 13 Mar 2024 19:25:01 +0200
Subject: [PATCH 06/10] hook on length

---
 .../EnumerableSet/certora/spec/set.spec                   | 8 +++-----
 .../Structs/BankAccounts/certora/specs/structs.spec       | 6 ++----
 2 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec b/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec
index 25bff479..554a8d8b 100644
--- a/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec
+++ b/CVLByExample/QuantifierExamples/EnumerableSet/certora/spec/set.spec
@@ -23,13 +23,12 @@ ghost mapping(bytes32 => uint256) ghostIndexes {
 // ghost field for the length of the values array (stored in offset 0)
 ghost uint256 ghostLength {
     // assumption: it's infeasible to grow the list to these many elements.
-    axiom ghostLength < 0xffffffffffffffffffffffffffffffff;
+    axiom ghostLength < max_uint256;
 }
 
 // HOOKS
 // Store hook to synchronize ghostLength with the length of the set._inner._values array. 
-// We need to use (offset 0) here, as there is no keyword yet to access the length.
-hook Sstore currentContract.set.(offset 0) uint256 newLength {
+hook Sstore currentContract.set._inner._values.length uint256 newLength {
     ghostLength = newLength;
 }
 // Store hook to synchronize ghostValues array with set._inner._values.
@@ -50,8 +49,7 @@ hook Sstore currentContract.set._inner._indexes[KEY bytes32 value] uint256 newIn
 // and that the solver can use this knowledge in the proofs.
 
 // Load hook to synchronize ghostLength with the length of the set._inner._values array. 
-// Again we use (offset 0) here, as there is no keyword yet to access the length.
-hook Sload uint256 length currentContract.set.(offset 0) {
+hook Sload uint256 length currentContract.set._inner._values.length {
     require ghostLength == length;
 }
 hook Sload bytes32 value currentContract.set._inner._values[INDEX uint256 index] {
diff --git a/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec b/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec
index 08da5501..8a5f591e 100644
--- a/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec
+++ b/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec
@@ -122,8 +122,7 @@ ghost mapping(address => uint256) numOfAccounts {
 }
 
 /// Store hook to synchronize numOfAccounts with the length of the customers[KEY address a].accounts array.
-/// We need to use (offset 32) here, as there is no keyword yet to access the length.
-hook Sstore _customers[KEY address user].(offset 32) uint256 newLength {
+hook Sstore _customers[KEY address user].accounts.length uint256 newLength {
     if (newLength > numOfAccounts[user])
         require accountBalanceMirror[user][require_uint256(newLength-1)] == 0 ;   
     numOfAccounts[user] = newLength;
@@ -137,8 +136,7 @@ invariant checkNumOfAccounts(address user)
     numOfAccounts[user] == bank.getNumberOfAccounts(user);
 
 /// This Sload is required in order to eliminate adding unintializaed account balance to sumBalances.
-/// (offset 32) is the location of the size of the mapping. It is used because the field `size` is not yet supported in cvl.  
-hook Sload uint256 length _customers[KEY address user].(offset 32) {
+hook Sload uint256 length _customers[KEY address user].accounts.length {
     require numOfAccounts[user] == length; 
 }
 

From ba32e8d8003921b430f5d02690ea4b377b66e77b Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Wed, 13 Mar 2024 21:20:17 +0200
Subject: [PATCH 07/10] auto nondet

---
 .../Summarization/AutoSummary/README.md       |   9 -
 .../Summarization/AutoSummary/runSqrRoot.conf |  10 -
 .../GhostSummary/SqrRoot/README.md            |  32 ++-
 .../GhostSummary/SqrRoot/SqrRoot.sol          | 246 ------------------
 .../SqrRoot/contracts}/SqrRoot.sol            |   0
 .../SqrRoot/runAutoSummarizedSqrRoot.conf     |  12 +
 .../GhostSummary/SqrRoot/runSqrRoot.conf      |   8 -
 .../SqrRoot/runSummarizedSqrRoot.conf         |  10 +
 .../SqrRoot/runUnsummarizedSqrRoot.conf       |  10 +
 .../SummarizedSqrRoot.spec}                   |   3 +-
 .../SqrRoot/specs/UnsummarizedSqrRoot.spec}   |   6 -
 11 files changed, 62 insertions(+), 284 deletions(-)
 delete mode 100644 CVLByExample/Summarization/AutoSummary/README.md
 delete mode 100644 CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
 delete mode 100644 CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.sol
 rename CVLByExample/Summarization/{AutoSummary => GhostSummary/SqrRoot/contracts}/SqrRoot.sol (100%)
 create mode 100644 CVLByExample/Summarization/GhostSummary/SqrRoot/runAutoSummarizedSqrRoot.conf
 delete mode 100644 CVLByExample/Summarization/GhostSummary/SqrRoot/runSqrRoot.conf
 create mode 100644 CVLByExample/Summarization/GhostSummary/SqrRoot/runSummarizedSqrRoot.conf
 create mode 100644 CVLByExample/Summarization/GhostSummary/SqrRoot/runUnsummarizedSqrRoot.conf
 rename CVLByExample/Summarization/GhostSummary/SqrRoot/{SqrRoot.spec => specs/SummarizedSqrRoot.spec} (90%)
 rename CVLByExample/Summarization/{AutoSummary/SqrRoot.spec => GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec} (84%)

diff --git a/CVLByExample/Summarization/AutoSummary/README.md b/CVLByExample/Summarization/AutoSummary/README.md
deleted file mode 100644
index 218c2b4a..00000000
--- a/CVLByExample/Summarization/AutoSummary/README.md
+++ /dev/null
@@ -1,9 +0,0 @@
-**NEED TO CHECK THIS EXAMPLE**
-
-To run this spec:
-
-```certoraRun.py runSqrRoot.conf```
-
-[A report of this run without autosummary](https://prover.certora.com/output/15800/0219068978f14c2a8c78ba5ebbb60feb?anonymousKey=5df460072f757b068c0683b04a32eb6de5d49c47)
-
-[A report of this run with autosummary](https://prover.certora.com/output/15800/53388c908d75493caf9fd93c6bb2ed0f?anonymousKey=33e05fe8eaf39f2aee1eab7f44c17d380b02ed0b)
diff --git a/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf b/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
deleted file mode 100644
index d9262cc4..00000000
--- a/CVLByExample/Summarization/AutoSummary/runSqrRoot.conf
+++ /dev/null
@@ -1,10 +0,0 @@
-{
-  "files": [
-    "SqrRoot.sol",
-  ],
-  "verify": "SqrRoot:SqrRoot.spec",
-  "optimistic_loop": true,
-  "auto_nondet_difficult_internal_funcs": true,
-  "loop_iter": "6",
-  "rule_sanity": "basic"
-}
diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md b/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md
index 2628d904..c8c6e416 100644
--- a/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md
+++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md
@@ -1,9 +1,33 @@
-This directory provides a precise ghost summary for the function `sqrRoot`. Certora team has proven the code obeys the property.
+# Summarizing a Square Root Function
 
-To run this spec:
+In this example we'll try to prove that adding liquidity to a certain protocol is monotonic. But there is a problem,
+the protocol computes some square roots as part of it's calculations.
 
-```certoraRun.py runSqrRoot.conf```
+Run the following spec:
+```certoraRun runUnsummarizedSqrRoot.conf```
+[A report of this run](https://prover.certora.com/output/15800/305a18aa989940d0857e3c928d26dd46?anonymousKey=1f2dd488f9d710622ae9757f27c84642f7d43e45)
 
-[A report of this run](https://prover.certora.com/output/15800/2846cde0b56a45c3ab044868e95cc7fd?anonymousKey=e509c40a5d1ee37bf7a3b95f5a672f40ee4abd41)
+As you can see, the prover timed out trying to prove the rule. This is due to the nature of the complex math square root operation.
+In order to solve this timeout, we can try using a feature of the prover that will automatically use NONDET summarizations for
+difficult* internal functions.
+To enable this option you can add the flag `--auto_nondet_difficult_internal_funcs`, it is already included in the following conf.
+
+Run it using:
+```certoraRun runAutoSummarizedSqrRoot.conf```
+[A report of this run](https://prover.certora.com/output/15800/2c57a7956db04b09b309fa6220dfa2d9?anonymousKey=719eaa90c86e6c73c6f2af637b5921a5b063d47a)
+
+(*The prover calculates a difficulty score using various attributes of the functions.)
+
+The timeout was solved and we got a counter example to the rule. If you'll look closely at the counter example you'll notice that
+it seems wrong. This is because as we mentioned above, we used a NONDET summarization for the `sqrRoot` function, which is an integral part of the liquidity calculation, instead of actually calculating the square root.
+
+What we can do, is use a smarter hand-crafted summarization. The spec `SummarizedSqrRoot.conf` contains a precise ghost summary for the function `sqrRoot`. The Certora team has proven the summarization is indeed equal to a square root operation.
+
+To run this spec use:
+
+```certoraRun.py runSummarizedSqrRoot.conf```
+[A report of this run](https://prover.certora.com/output/15800/b91e56bd9fab47e69ab023e94b168ed3?anonymousKey=136f48b482a96179742e755d4c644e69abb1595e)
+
+Now the rule is passing and we successfully proven the monotonicity property.
 
 
diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.sol b/CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.sol
deleted file mode 100644
index 8134957f..00000000
--- a/CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.sol
+++ /dev/null
@@ -1,246 +0,0 @@
-// SPDX-License-Identifier: MIT
-
-contract SqrRoot{
-    IERC20 public immutable token0;
-    IERC20 public immutable token1;
-
-    uint256 public reserve0;
-    uint256 public reserve1;
-
-    uint256 public totalSupply;
-    mapping(address => uint256) public balanceOf;
-
-    constructor(address _token0, address _token1) {
-        token0 = IERC20(_token0);
-        token1 = IERC20(_token1);
-    }
-
-    function _mint(address _to, uint256 _amount) private {
-        balanceOf[_to] += _amount;
-        totalSupply += _amount;
-    }
-
-    function _burn(address _from, uint256 _amount) private {
-        balanceOf[_from] -= _amount;
-        totalSupply -= _amount;
-    }
-
-    function _update(uint256 _reserve0, uint256 _reserve1) private {
-        reserve0 = _reserve0;
-        reserve1 = _reserve1;
-    }
-
-    function swap(address _tokenIn, uint256 _amountIn) external returns (uint256 amountOut) {
-        require(
-            _tokenIn == address(token0) || _tokenIn == address(token1),
-            "invalid token"
-        );
-        require(_amountIn > 0, "amount in = 0");
-
-        bool isToken0 = _tokenIn == address(token0);
-        (IERC20 tokenIn, IERC20 tokenOut, uint256 reserveIn, uint256 reserveOut) = isToken0
-            ? (token0, token1, reserve0, reserve1)
-            : (token1, token0, reserve1, reserve0);
-
-        tokenIn.transferFrom(msg.sender, address(this), _amountIn);
-
-        /*
-        How much dy for dx?
-
-        xy = k
-        (x + dx)(y - dy) = k
-        y - dy = k / (x + dx)
-        y - k / (x + dx) = dy
-        y - xy / (x + dx) = dy
-        (yx + ydx - xy) / (x + dx) = dy
-        ydx / (x + dx) = dy
-        */
-        // 0.3% fee
-        uint256 amountInWithFee = (_amountIn * 997) / 1000;
-        amountOut = (reserveOut * amountInWithFee) / (reserveIn + amountInWithFee);
-
-        tokenOut.transfer(msg.sender, amountOut);
-
-        _update(token0.balanceOf(address(this)), token1.balanceOf(address(this)));
-    }
-
-    function addLiquidity(uint256 _amount0, uint256 _amount1) external returns (uint256 shares) {
-        token0.transferFrom(msg.sender, address(this), _amount0);
-        token1.transferFrom(msg.sender, address(this), _amount1);
-
-        /*
-        How much dx, dy to add?
-
-        xy = k
-        (x + dx)(y + dy) = k'
-
-        No price change, before and after adding liquidity
-        x / y = (x + dx) / (y + dy)
-
-        x(y + dy) = y(x + dx)
-        x * dy = y * dx
-
-        x / y = dx / dy
-        dy = y / x * dx
-        */
-        require (reserve0 > 0 && reserve1 > 0);
-        if (reserve0 > 0 || reserve1 > 0) {
-            require(reserve0 * _amount1 == reserve1 * _amount0, "x / y != dx / dy");
-        }
-
-        /*
-        How much shares to mint?
-
-        f(x, y) = value of liquidity
-        We will define f(x, y) = sqrt(xy)
-
-        L0 = f(x, y)
-        L1 = f(x + dx, y + dy)
-        T = total shares
-        s = shares to mint
-
-        Total shares should increase proportional to increase in liquidity
-        L1 / L0 = (T + s) / T
-
-        L1 * T = L0 * (T + s)
-
-        (L1 - L0) * T / L0 = s 
-        */
-
-        /*
-        Claim
-        (L1 - L0) / L0 = dx / x = dy / y
-
-        Proof
-        --- Equation 1 ---
-        (L1 - L0) / L0 = (sqrt((x + dx)(y + dy)) - sqrt(xy)) / sqrt(xy)
-        
-        dx / dy = x / y so replace dy = dx * y / x
-
-        --- Equation 2 ---
-        Equation 1 = (sqrt(xy + 2ydx + dx^2 * y / x) - sqrt(xy)) / sqrt(xy)
-
-        Multiply by sqrt(x) / sqrt(x)
-        Equation 2 = (sqrt(x^2y + 2xydx + dx^2 * y) - sqrt(x^2y)) / sqrt(x^2y)
-                   = (sqrt(y)(sqrt(x^2 + 2xdx + dx^2) - sqrt(x^2)) / (sqrt(y)sqrt(x^2))
-        
-        sqrt(y) on top and bottom cancels out
-
-        --- Equation 3 ---
-        Equation 2 = (sqrt(x^2 + 2xdx + dx^2) - sqrt(x^2)) / (sqrt(x^2)
-        = (sqrt((x + dx)^2) - sqrt(x^2)) / sqrt(x^2)  
-        = ((x + dx) - x) / x
-        = dx / x
-
-        Since dx / dy = x / y,
-        dx / x = dy / y
-
-        Finally
-        (L1 - L0) / L0 = dx / x = dy / y
-        */
-
-        if (totalSupply == 0) {
-            shares = sqrt(_amount0 * _amount1);
-        } else {
-            shares = _min(
-                (_amount0 * totalSupply) / reserve0,
-                (_amount1 * totalSupply) / reserve1
-            );
-        }
-        require(shares > 0, "shares = 0");
-        _mint(msg.sender, shares);
-
-        _update(token0.balanceOf(address(this)), token1.balanceOf(address(this)));
-    }
-
-    function removeLiquidity(
-        uint256 _shares
-    ) external returns (uint256 amount0, uint256 amount1) {
-        /*
-        Claim
-        dx, dy = amount of liquidity to remove
-        dx = s / T * x
-        dy = s / T * y
-
-        Proof
-        Let's find dx, dy such that
-        v / L = s / T
-        
-        where
-        v = f(dx, dy) = sqrt(dxdy)
-        L = total liquidity = sqrt(xy)
-        s = shares
-        T = total supply
-
-        --- Equation 1 ---
-        v = s / T * L
-        sqrt(dxdy) = s / T * sqrt(xy)
-
-        Amount of liquidity to remove must not change price so 
-        dx / dy = x / y
-
-        replace dy = dx * y / x
-        sqrt(dxdy) = sqrt(dx * dx * y / x) = dx * sqrt(y / x)
-
-        Divide both sides of Equation 1 with sqrt(y / x)
-        dx = s / T * sqrt(xy) / sqrt(y / x)
-           = s / T * sqrt(x^2) = s / T * x
-
-        Likewise
-        dy = s / T * y
-        */
-
-        // bal0 >= reserve0
-        // bal1 >= reserve1
-        uint256 bal0 = token0.balanceOf(address(this));
-        uint256 bal1 = token1.balanceOf(address(this));
-
-        amount0 = (_shares * bal0) / totalSupply;
-        amount1 = (_shares * bal1) / totalSupply;
-        require(amount0 > 0 && amount1 > 0, "amount0 or amount1 = 0");
-
-        _burn(msg.sender, _shares);
-        _update(bal0 - amount0, bal1 - amount1);
-
-        token0.transfer(msg.sender, amount0);
-        token1.transfer(msg.sender, amount1);
-    }
-
-    function sqrt(uint256 y) public pure returns (uint256 z) {
-        if (y > 3) {
-            z = y;
-            uint256 x = y / 2 + 1;
-            while (x < z) {
-                z = x;
-                x = (y / x + x) / 2;
-            }
-        } else if (y != 0) {
-            z = 1;
-        }
-    }
-
-    function _min(uint256 x, uint256 y) private pure returns (uint256) {
-        return x <= y ? x : y;
-    }
-}
-
-interface IERC20 {
-    function totalSupply() external view returns (uint256);
-
-    function balanceOf(address account) external view returns (uint256);
-
-    function transfer(address recipient, uint256 amount) external returns (bool);
-
-    function allowance(address owner, address spender) external view returns (uint256);
-
-    function approve(address spender, uint256 amount) external returns (bool);
-
-    function transferFrom(
-        address sender,
-        address recipient,
-        uint256 amount
-    ) external returns (bool);
-
-    event Transfer(address indexed from, address indexed to, uint256 amount);
-    event Approval(address indexed owner, address indexed spender, uint256 amount);
-}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/AutoSummary/SqrRoot.sol b/CVLByExample/Summarization/GhostSummary/SqrRoot/contracts/SqrRoot.sol
similarity index 100%
rename from CVLByExample/Summarization/AutoSummary/SqrRoot.sol
rename to CVLByExample/Summarization/GhostSummary/SqrRoot/contracts/SqrRoot.sol
diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/runAutoSummarizedSqrRoot.conf b/CVLByExample/Summarization/GhostSummary/SqrRoot/runAutoSummarizedSqrRoot.conf
new file mode 100644
index 00000000..af6747ad
--- /dev/null
+++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/runAutoSummarizedSqrRoot.conf
@@ -0,0 +1,12 @@
+{
+  "files": [
+    "contracts/SqrRoot.sol",
+  ],
+  "verify": "SqrRoot:specs/UnsummarizedSqrRoot.spec",
+  "msg": "Unsummarized sqrt proof",
+  "rule_sanity": "basic",
+  "optimistic_loop": true,
+  "loop_iter": "7",
+  "auto_nondet_difficult_internal_funcs": true,
+  "auto_nondet_minimal_difficulty": "8"
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/runSqrRoot.conf b/CVLByExample/Summarization/GhostSummary/SqrRoot/runSqrRoot.conf
deleted file mode 100644
index 25643dcf..00000000
--- a/CVLByExample/Summarization/GhostSummary/SqrRoot/runSqrRoot.conf
+++ /dev/null
@@ -1,8 +0,0 @@
-{
-  "files": [
-    "SqrRoot.sol",
-  ],
-  "verify": "SqrRoot:SqrRoot.spec",
-  "msg": "ghost function summary for sqrt",
-  "rule_sanity": "basic"
-}
diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/runSummarizedSqrRoot.conf b/CVLByExample/Summarization/GhostSummary/SqrRoot/runSummarizedSqrRoot.conf
new file mode 100644
index 00000000..7e76d169
--- /dev/null
+++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/runSummarizedSqrRoot.conf
@@ -0,0 +1,10 @@
+{
+  "files": [
+    "contracts/SqrRoot.sol",
+  ],
+  "verify": "SqrRoot:specs/SummarizedSqrRoot.spec",
+  "msg": "Unsummarized sqrt proof",
+  "rule_sanity": "basic",
+  "optimistic_loop": true,
+  "loop_iter": "7"
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/runUnsummarizedSqrRoot.conf b/CVLByExample/Summarization/GhostSummary/SqrRoot/runUnsummarizedSqrRoot.conf
new file mode 100644
index 00000000..293f8e32
--- /dev/null
+++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/runUnsummarizedSqrRoot.conf
@@ -0,0 +1,10 @@
+{
+  "files": [
+    "contracts/SqrRoot.sol",
+  ],
+  "verify": "SqrRoot:specs/UnsummarizedSqrRoot.spec",
+  "msg": "Unsummarized sqrt proof",
+  "rule_sanity": "basic",
+  "optimistic_loop": true,
+  "loop_iter": "7"
+}
\ No newline at end of file
diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.spec b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/SummarizedSqrRoot.spec
similarity index 90%
rename from CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.spec
rename to CVLByExample/Summarization/GhostSummary/SqrRoot/specs/SummarizedSqrRoot.spec
index 4f01c782..048d3d1c 100644
--- a/CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.spec
+++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/SummarizedSqrRoot.spec
@@ -1,6 +1,7 @@
 methods {
-    function sqrt(uint256 y) internal  returns (uint256) => floorSqrt(y);
+    function sqrt(uint256 y) internal returns (uint256) => floorSqrt(y);
 }
+
 // A precise summarization of sqrt
 ghost floorSqrt(uint256) returns uint256 {    
                 // sqrt(x)^2 <= x
diff --git a/CVLByExample/Summarization/AutoSummary/SqrRoot.spec b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec
similarity index 84%
rename from CVLByExample/Summarization/AutoSummary/SqrRoot.spec
rename to CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec
index 7d98b265..0ec58611 100644
--- a/CVLByExample/Summarization/AutoSummary/SqrRoot.spec
+++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec
@@ -1,9 +1,3 @@
-/*
-methods {
-    function sqrt(uint256 y) internal returns (uint256);
-}
-*/
-
 rule addLiquidityMonotonicity(uint256 amount0, uint256 amount1, uint256 amount2, uint256 amount3) {
     env e;
     storage initStorage = lastStorage;

From 579653bdf009e65d9c7fe81a9c198866ae075f1b Mon Sep 17 00:00:00 2001
From: liav-certora <liav@certora.com>
Date: Wed, 13 Mar 2024 21:22:20 +0200
Subject: [PATCH 08/10] remove flags

---
 CLIFlags/README.md | 2 --
 1 file changed, 2 deletions(-)

diff --git a/CLIFlags/README.md b/CLIFlags/README.md
index 3f665375..7bb23f01 100644
--- a/CLIFlags/README.md
+++ b/CLIFlags/README.md
@@ -15,8 +15,6 @@ For more information about available CLI options go to: https://docs.certora.com
 | [--independent_satisfy](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#independent-satisfy) | |
 | [--rule_sanity](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#rule-sanity) | [none](https://prover.certora.com/output/15800/16fdf7aa282243e591889d9ec27a71ef?anonymousKey=6bdd16c5780e0127246ddc3eea3ee8a22c9729b8) / [basic](https://prover.certora.com/output/15800/2c5aa93c4bc54a939dea395202c0e47c?anonymousKey=bf07b5bdc3a7c7b28fda762942b02456731d2371) / [advanced](https://prover.certora.com/output/15800/e44ef408e1794a8fa32178f63fbe83da?anonymousKey=4afd4e7f98fc3d11d03b0a8522d417a2671f70fe) |
 | [--solc](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc) | [ERC20 compiled with solc8.0](https://prover.certora.com/output/15800/aa8e3c59b7434058a1f0927f6cd1da77?anonymousKey=099deb423f4cb86913f8a536309ea8a64511ca46) / [compiled with solc8.10](https://prover.certora.com/output/15800/c67c4072730d40f7b081556ddf78334e?anonymousKey=e9d7ffddc9f338e3a865505fbbe18f095823ae43) |
-| [--solc_map](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-map) | |
-| [--solc_optimize](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-optimize) | |
 | [--solc_via_ir](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-via-ir) | [false](https://prover.certora.com/output/15800/83116717cc7a48f5b53172666a83817e?anonymousKey=0a5ee559275dcb173b18a69caeda4f33a2b8f014) / [true](https://prover.certora.com/output/15800/4a29b3f21b884b8d8fc5550f61fa45b7?anonymousKey=f1909b5b181ae4534377501a3c06c896bfff2d67) |
 | [--solc_evm_version](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-evm-version) | [ERC20 with Berlin](https://prover.certora.com/output/15800/1d55dc0613b444f2a690fce8f645d9d1?anonymousKey=9efa9f0b59bfc8c37aa7c9d0d8573c9d99f1c2cf) / [ERC20 with London](https://prover.certora.com/output/15800/115e1f215f344fefb7dd389cb4db9d9f?anonymousKey=75c515fd97ff0ae21b887b5915db180d807dc9d2) |
 | [--solc_allow_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-allow-path) | Every conf example in this folder has it. |

From a05e29ce8bb98b86c0b6a99b3f53643ac8cb4b98 Mon Sep 17 00:00:00 2001
From: liav-certora <114004726+liav-certora@users.noreply.github.com>
Date: Wed, 13 Mar 2024 21:23:09 +0200
Subject: [PATCH 09/10] Update CLIFlags/README.md

Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com>
---
 CLIFlags/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CLIFlags/README.md b/CLIFlags/README.md
index 7bb23f01..edb7b5e3 100644
--- a/CLIFlags/README.md
+++ b/CLIFlags/README.md
@@ -20,7 +20,7 @@ For more information about available CLI options go to: https://docs.certora.com
 | [--solc_allow_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-allow-path) | Every conf example in this folder has it. |
 | [--packages_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages-path) | |
 | [--packages](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages) | |
-| --optimistic_fallback | [false](https://prover.certora.com/output/15800/5f15bade773a4d5c9494408d3751156c?anonymousKey=c28bae503fe3444c21adc2971bda5a2f74e685cc) / [true](https://prover.certora.com/output/15800/a23a21a8ef9642ba83d97547fc361b70?anonymousKey=596e02bc0b6976504873489348d118bdbb2abb7f) |
+| --optimistic_fallback | [false](https://prover.certora.com/output/15800/5f15bade773a4d5c9494408d3751156c?anonymousKey=c28bae503fe3444c21adc2971bda5a2f74e685cc) / [true](https://prover.certora.com/output/15800/a23a21a8ef9642ba83d97547fc361b70?anonymousKey=596e02bc0b6976504873489348d118bdbb2abb7f)  notice rule storageAfterTwoWithdrawalsFromInitDoesNotChange |
 | [--optimistic_loop](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-loop) | [false](https://prover.certora.com/output/15800/8db8b5eaeb244ba490394e05edac0fe1?anonymousKey=5067d0c0908cc2f1cb348e8b163bfec327884cee) / [true](https://prover.certora.com/output/15800/89e59b62f44f439c9502363cef4e7b49?anonymousKey=bac549ca44168b6e0b282a980240c247b34d77ee) |
 | [--loop_iter](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#loop-iter) | [A run with 1 loop unrolling](https://prover.certora.com/output/15800/9b085d85bcc345d5bd2612f8bea5da98?anonymousKey=a6c544d73525dcb582eba2b971d85d97c16b35db) / [Same run with 3 loop unrolling](https://prover.certora.com/output/15800/0b152fe8cfcc41168429a287fa2ba7f8?anonymousKey=38fd94f0ac9bd36f3cecb23d8275b23b864e2d77) |
 | --optimistic_contract_recursion | [false](https://prover.certora.com/output/15800/908365f5dfb04e2b9a6d0dfef3a7c006?anonymousKey=2db3842d23c9fb7a6065551ed56fc9bdfa815595) / [true](https://prover.certora.com/output/15800/65a836c4a9f542f79ad7e2fd563a8a18?anonymousKey=2bb9bcbad7f489038331183b3e6573fec4235c73) |

From 4a6a3491628310ae171d5f5d0dbddde2dcf6f7d5 Mon Sep 17 00:00:00 2001
From: liav-certora <114004726+liav-certora@users.noreply.github.com>
Date: Wed, 13 Mar 2024 21:23:25 +0200
Subject: [PATCH 10/10] Update
 CVLByExample/Summarization/WildcardVsExact/README.md

Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com>
---
 CVLByExample/Summarization/WildcardVsExact/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CVLByExample/Summarization/WildcardVsExact/README.md b/CVLByExample/Summarization/WildcardVsExact/README.md
index 53e6ad00..a44a3ac1 100644
--- a/CVLByExample/Summarization/WildcardVsExact/README.md
+++ b/CVLByExample/Summarization/WildcardVsExact/README.md
@@ -1,6 +1,6 @@
 # What happens when a function has both exact and wildcard summarizations?
 
-When a function matches a wildcard summarization but also has an exact summarization, the exact summarization will be used to summarize
+When a function matches a wildcard summarization but also has an exact summarization, the exact summarization is used to summarize
 this function. We will demonstrate such case using a simple example.
 
 We have 2 very simple contracts: `A` (in `A.sol`) and `B` (in `B.sol`).