Merge pull request #61 from Certora/liav/CERT-5336-V7-Examples

Liav/cert 5336 v7 examples

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

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

CLIFlags/README.md

@@ -15,15 +15,16 @@ 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. |
 | [--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)  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) |
+| --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) | |

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"]
+}

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"]
+}

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": "../"
+}

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] {

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)
 

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

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

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.
 
 

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

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

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

CVLByExample/Summarization/GhostSummary/SqrRoot/SqrRoot.spec → 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

CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec

@@ -0,0 +1,9 @@
+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");
+}

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 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`).
+`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.

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

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

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

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