Skip to content

Commit 345eef2

Browse files
liav-certoraliav-certora
committed
Merge branch 'master' into cli-beta
2 parents 3923259 + 53af1ec commit 345eef2

22 files changed

+755
-0
lines changed

‎CLIFlags/README.md‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
# Examples of CLI Flags for certoraRun
2+
3+
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.
4+
5+
For more information about available CLI options go to: https://docs.certora.com/en/latest/docs/prover/cli/options.html
6+
7+
| Flag | Examples |
8+
| ---- | -------- |
9+
| [--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)). |
10+
| [--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) |
11+
| [--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) |
12+
| [--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) |
13+
| [--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) |
14+
| [--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) |
15+
| [--independent_satisfy](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#independent-satisfy) | |
16+
| [--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) |
17+
| [--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) |
18+
| [--solc_map](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-map) | |
19+
| [--solc_optimize](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-optimize) | |
20+
| [--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) |
21+
| [--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) |
22+
| [--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. |
23+
| [--packages_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages-path) | |
24+
| [--packages](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages) | |
25+
| [--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) |
26+
| [--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) |
27+
| [--optimistic_summary_recursion](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-summary-recursion) | |
28+
| [--summary_recursion_limit](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#summary-recursion-limit) | |
29+
| [--optimistic_hashing](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-hashing) | |
30+
| [--hashing_length_bound](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#hashing-length-bound) | |
31+
| [--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) |
32+
| [--address](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#address) | |
33+
| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | |

‎CLIFlags/link.conf‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
"files": [
3+
"../DEFI/LiquidityPool/contracts/Pool.sol",
4+
"../DEFI/LiquidityPool/contracts/Asset.sol",
5+
"../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol"
6+
],
7+
"verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec",
8+
// Link a field in the contract to another contract.
9+
"link": [
10+
"Pool:asset=Asset"
11+
],
12+
13+
"parametric_contracts": ["Pool"],
14+
"solc_allow_path": "../"
15+
}

‎CLIFlags/loop_iter.conf‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{
2+
"files": [
3+
"../CVLByExample/NativeBalances/contracts/Auction.sol",
4+
],
5+
"verify": "Auction:../CVLByExample/NativeBalances/certora/specs/Auction.spec",
6+
// Set number of loop unrolling for loops.
7+
"loop_iter": "3",
8+
9+
"optimistic_loop": true,
10+
"solc_allow_path": "../"
11+
}

‎CLIFlags/method.conf‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
{
2+
"files": [
3+
"../DEFI/ERC20/contracts/ERC20.sol"
4+
],
5+
"verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
6+
// Use only specific method for parametric rules and invariants.
7+
"method": "transfer(address,uint256)",
8+
9+
"solc_allow_path": "../"
10+
}

‎CLIFlags/msg.conf‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
{
2+
"files": [
3+
"../CVLByExample/Invariant/contracts/BallGame.sol:BallGame"
4+
],
5+
"verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec",
6+
// Add a message.
7+
"msg": "This run will have a message :)",
8+
9+
"solc_allow_path": "../"
10+
}

‎CLIFlags/multi_assert_check.conf‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{
2+
"files": [
3+
"../CVLByExample/Optional/contracts/Base.sol",
4+
"../CVLByExample/Optional/contracts/Base.sol:Partial",
5+
],
6+
"verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec",
7+
// Enable multi asserts.
8+
"multi_assert_check": true,
9+
10+
"solc_allow_path": "../"
11+
}

‎CLIFlags/optimistic_loop.conf‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
{
2+
"files": [
3+
"../DEFI/ERC20/contracts/ERC20.sol"
4+
],
5+
"verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
6+
// Consider only paths in which the loop unwind condition holds.
7+
"optimistic_loop": true,
8+
9+
"solc_allow_path": "../"
10+
}

‎CLIFlags/parametric_contract.conf‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{
2+
"files": [
3+
"../DEFI/LiquidityPool/contracts/Pool.sol",
4+
"../DEFI/LiquidityPool/contracts/Asset.sol",
5+
"../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol"
6+
],
7+
"verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec",
8+
// Specify on which contracts to run parametric rules.
9+
"parametric_contracts": ["Pool"],
10+
11+
"link": [
12+
"Pool:asset=Asset"
13+
],
14+
"solc_allow_path": "../"
15+
}

‎CLIFlags/rule.conf‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{
2+
"files": [
3+
"../DEFI/ERC20/contracts/ERC20.sol"
4+
],
5+
"verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec",
6+
// Select only a specific rule.
7+
"rule": [
8+
"mintIntegrity"
9+
],
10+
11+
"solc_allow_path": "../"
12+
}

‎CLIFlags/rule_sanity.conf‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{
2+
"files": [
3+
"../CVLByExample/Optional/contracts/Base.sol",
4+
"../CVLByExample/Optional/contracts/Base.sol:Partial",
5+
],
6+
"verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec",
7+
// Perform sanity check, set to none/basic/advanced.
8+
"rule_sanity": "advanced",
9+
10+
"solc_allow_path": "../"
11+
}

0 commit comments

Comments
 (0)