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 fbd1bf01..edb7b5e3 100644 --- a/CLIFlags/README.md +++ b/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) | | 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 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/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/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 d7171b3b..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); @@ -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], 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; } 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/contracts/SqrRoot.sol similarity index 100% rename from CVLByExample/Summarization/GhostSummary/SqrRoot/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/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec b/CVLByExample/Summarization/GhostSummary/SqrRoot/specs/UnsummarizedSqrRoot.spec new file mode 100644 index 00000000..0ec58611 --- /dev/null +++ b/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"); +} diff --git a/CVLByExample/Summarization/WildcardVsExact/README.md b/CVLByExample/Summarization/WildcardVsExact/README.md new file mode 100644 index 00000000..a44a3ac1 --- /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 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. 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