Merge branch 'master' into cli-beta

CLIFlags/README.md

@@ -0,0 +1,33 @@
+# Examples of CLI Flags for certoraRun
+
+This is an index of some of the CLI flags available in the certoraRun command along with some examples of runs. Each flag links to its corresponding documentation over at Certora Docs. In this folder you can also see some confs called `<flag>.conf` with examples of these flags on some of the other examples available in this repository.
+
+For more information about available CLI options go to: https://docs.certora.com/en/latest/docs/prover/cli/options.html
+
+| Flag | Examples |
+| ---- | -------- |
+| [--verify](https://docs.certora.com/en/latest/docs/prover/cli/options.html#verify) | Every run uses verify ([e.g.](https://prover.certora.com/output/15800/83116717cc7a48f5b53172666a83817e?anonymousKey=0a5ee559275dcb173b18a69caeda4f33a2b8f014)). |
+| [--msg](https://docs.certora.com/en/latest/docs/prover/cli/options.html#msg-description) | [Run with a message.](https://prover.certora.com/output/15800/1aa5389f01604c33817e4f9ccf2f70fc?anonymousKey=e6f6fbe19097097df6851846847f5139b930b394) |
+| [--rule](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#rule-rule-name) | [An ERC20 run.](https://prover.certora.com/output/15800/21e87636bbdc4f1783c467c70bffbd32?anonymousKey=23b497245d7c1614db30315093f2cd34900f99f9) /  [Selecting only 1 rule.](https://prover.certora.com/output/15800/c554c7baf7534fe0940c98c60883bc6f?anonymousKey=1cef55a4c343c50c82b40d7c400ae185ede867d8) |
+| [--method](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#method-method-signature) | [An ERC20 run.](https://prover.certora.com/output/15800/21e87636bbdc4f1783c467c70bffbd32?anonymousKey=23b497245d7c1614db30315093f2cd34900f99f9) / [Only 1 method used.](https://prover.certora.com/output/15800/3cf9410d78014c2f91835a5f8aa60767?anonymousKey=8392f2471d7507a21fd990a19ad0611592261f1e) |
+| [--parametric_contracts](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#parametric-contracts-contract-name) | [A LiquidityPool run without specifying.](https://prover.certora.com/output/15800/7ba2e8562afd4a5782f282059a0c1f00?anonymousKey=e12b94385957f1ebb14c0c1d8a77ec6f8765da7a) / [With specifying a contract.](https://prover.certora.com/output/15800/309c9ba5749e41b6b5a8b151ab3dd616?anonymousKey=44524f6189d23054e528c2a3ba97cc21112194fd) |
+| [--multi_assert_check](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#multi-assert-check) | [false](https://prover.certora.com/output/15800/e11354b5e03441cc9ac1d210fe686347?anonymousKey=911ba098228465f7c6fc0ba1d4d40cbde83bef94) / [true](https://prover.certora.com/output/15800/23c97944b0074bebb7e79ad4cd852984?anonymousKey=6e4c43f376883162646e5c61101abdcf36131c4e) |
+| [--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_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) | |
+| [--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) | |
+| [--hashing_length_bound](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#hashing-length-bound) | |
+| [--link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#link) | [Liquidity Pool without linking](https://prover.certora.com/output/15800/e80f04180604458597fecc47c2b64e74?anonymousKey=b893bb90a8858acf903ba4aff1006af89a96d188) / [With linking](https://prover.certora.com/output/15800/f8f4b7a9180b49c1acdff4111a3c8e7a?anonymousKey=4a5b9ea156448922f7a1b4a25311d2b1e5c676ad) |
+| [--address](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#address) | |
+| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | |

CLIFlags/link.conf

@@ -0,0 +1,15 @@
+{
+    "files": [
+        "../DEFI/LiquidityPool/contracts/Pool.sol",
+        "../DEFI/LiquidityPool/contracts/Asset.sol",
+        "../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol"
+    ],
+    "verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec",
+    // Link a field in the contract to another contract.
+    "link": [
+        "Pool:asset=Asset"
+    ],
+
+    "parametric_contracts": ["Pool"],
+    "solc_allow_path": "../"
+}

CLIFlags/loop_iter.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../CVLByExample/NativeBalances/contracts/Auction.sol",
+    ],
+    "verify": "Auction:../CVLByExample/NativeBalances/certora/specs/Auction.spec",
+    // Set number of loop unrolling for loops.
+    "loop_iter": "3",
+
+    "optimistic_loop": true,
+    "solc_allow_path": "../"
+}

CLIFlags/method.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Use only specific method for parametric rules and invariants.
+    "method": "transfer(address,uint256)",
+
+    "solc_allow_path": "../"
+}

CLIFlags/msg.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame"
+    ],
+    "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec",
+    // Add a message.
+    "msg": "This run will have a message :)",
+
+    "solc_allow_path": "../"
+}

CLIFlags/multi_assert_check.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../CVLByExample/Optional/contracts/Base.sol",
+        "../CVLByExample/Optional/contracts/Base.sol:Partial",
+    ],
+    "verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec",
+    // Enable multi asserts.
+    "multi_assert_check": true,
+
+    "solc_allow_path": "../"
+}

CLIFlags/optimistic_loop.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Consider only paths in which the loop unwind condition holds.
+    "optimistic_loop": true,
+
+    "solc_allow_path": "../"
+}

CLIFlags/parametric_contract.conf

@@ -0,0 +1,15 @@
+{
+    "files": [
+        "../DEFI/LiquidityPool/contracts/Pool.sol",
+        "../DEFI/LiquidityPool/contracts/Asset.sol",
+        "../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol"
+    ],
+    "verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec",
+    // Specify on which contracts to run parametric rules.
+    "parametric_contracts": ["Pool"],
+
+    "link": [
+        "Pool:asset=Asset"
+    ],
+    "solc_allow_path": "../"
+}

CLIFlags/rule.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Select only a specific rule.
+    "rule": [
+        "mintIntegrity"
+    ],
+
+    "solc_allow_path": "../"
+}

CLIFlags/rule_sanity.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../CVLByExample/Optional/contracts/Base.sol",
+        "../CVLByExample/Optional/contracts/Base.sol:Partial",
+    ],
+    "verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec",
+    // Perform sanity check, set to none/basic/advanced.
+    "rule_sanity": "advanced",
+
+    "solc_allow_path": "../"
+}

CLIFlags/solc.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Set the Solidity compiler version used.
+    "solc": "solc8.10",
+
+    "optimistic_loop": true,
+    "solc_allow_path": "../"
+}

CLIFlags/solc_evm_version.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "../DEFI/ERC20/contracts/ERC20.sol"
+    ],
+    "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
+    // Set the EVM version used.
+    "solc_evm_version": "london",
+
+    "optimistic_loop": true,
+    "solc_allow_path": "../"
+}

CLIFlags/solc_via_ir.conf

@@ -0,0 +1,10 @@
+{
+    "files": [
+        "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame"
+    ],
+    "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec",
+    // Enable IR based code generator.
+    "solc_via_ir": true,
+
+    "solc_allow_path": "../"
+}

CLIFlags/verify.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame"
+    ],
+    // Verify BallGame contract against the specified spec.
+    "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec",
+
+    "solc_allow_path": "../"
+}

CVLByExample/Ecrecover/Fullecrecover.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "Verify.sol"
+    ],
+    "optimistic_hashing": true,
+    "rule_sanity": "advanced", 
+    "verify": "Verify:ecrecover.spec"
+}

CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol

@@ -0,0 +1,70 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// game developer depoloys contract
+contract Verify {
+
+    function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external  returns (bool) {
+        return ecrecover(msgHash, v, r, s) == _addr;
+    }
+
+
+mapping (address => uint256) private nonces; 
+
+function executeMyFunctionFromSignature(
+    uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) external {
+
+    bytes32 hash = getHash(owner, myParam, deadline);
+
+
+    address signer = ecrecover(hash, v, r, s);
+    require(signer == owner, "MyFunction: invalid signature");
+    require(signer != address(0), "ECDSA: invalid signature");
+
+    require(block.timestamp < deadline, "MyFunction: signed transaction expired");
+    // nonces[owner]++; // forgeting to update the nonces will result in possible multiple execution 
+
+    _myFunction(owner, myParam);
+}
+
+function _myFunction(address owner, uint256 myParam) internal {
+
+}
+
+function getHash(
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) public returns(bytes32) {
+    bytes32 eip712DomainHash = keccak256(
+        abi.encode(
+            keccak256(
+                "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"
+            ),
+            keccak256(bytes("MyContractName")),
+            keccak256(bytes("1")),
+            address(this)
+        )
+    );
+
+    bytes32 hashStruct = keccak256(
+        abi.encode(
+            keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"),
+            owner,
+            myParam,
+            nonces[owner],
+            deadline
+        )
+    );
+
+    return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct));
+}
+
+
+}

CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol

@@ -0,0 +1,68 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.0;
+
+// game developer depoloys contract
+contract Verify {
+
+    function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external  returns (bool) {
+        return ecrecover(msgHash, v, r, s) == _addr;
+    }
+
+
+mapping (address => uint256) private nonces; 
+
+function executeMyFunctionFromSignature(
+    uint8 v,
+    bytes32 r,
+    bytes32 s,
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) external {
+
+    bytes32 hash = getHash(/*owner*/ msg.sender, myParam, deadline); // computing the has on the wrong address
+
+
+    address signer = ecrecover(hash, v, r, s);
+    require(signer == owner, "MyFunction: invalid signature");
+    require(signer != address(0), "ECDSA: invalid signature");
+
+    require(block.timestamp < deadline, "MyFunction: signed transaction expired");
+    nonces[owner]++; 
+
+    _myFunction(owner, myParam);
+}
+
+function _myFunction(address owner, uint256 myParam) internal {
+
+}
+
+function getHash(
+    address owner,
+    uint256 myParam,
+    uint256 deadline
+) public returns(bytes32) {
+    bytes32 eip712DomainHash = keccak256(
+        abi.encode(
+            keccak256(
+                "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"
+            ),
+            keccak256(bytes("MyContractName")),
+            keccak256(bytes("1")),
+            address(this)
+        )
+    );
+
+    bytes32 hashStruct = keccak256(
+        abi.encode(
+            keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"),
+            owner,
+            myParam,
+            nonces[owner],
+            deadline
+        )
+    );
+
+    return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct));
+}
+}