From 18b68ccd98883098c72a4886def2198e54923c6f Mon Sep 17 00:00:00 2001 From: rahav Date: Tue, 22 Aug 2023 14:32:50 +0300 Subject: [PATCH 01/61] conf file api --- docs/prover/cli/conf-file-api.md | 99 ++++++++++++++++++++++++++++++++ docs/prover/cli/index.md | 1 + 2 files changed, 100 insertions(+) create mode 100644 docs/prover/cli/conf-file-api.md diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md new file mode 100644 index 00000000..03390d75 --- /dev/null +++ b/docs/prover/cli/conf-file-api.md @@ -0,0 +1,99 @@ +Certora Prover Conf File API +============================ + +The **Conf File API** is an alternative API for  `certoraRun` . In terms of functionality +this API is identical to the [CLI Options](options.md). Instead of calling `certoraRun` +with a list of shell flags, some or all the flags can be stored in a [JSON](https://www.json.org/json-en.html) file: + +```bash +certoraRun my_params.conf +``` +
+To denote a text file as a conf file use the .conf suffix +
+ +Converting from CLI Options to JSON +----------------------------------- + +**JSON Keys** + +JSON keys in the conf file are the flag names without the leading dashes: +```{contents} Overview +The CLI flag --verify will be stored under the "verify" in the conf file +``` +The JSON key for the input files in the CLI API is **"files"** + +**String Value CLI Options** + +Flags in CLI API that accept a single string will be stored as **JSON Strings**. Example: +```{contents} +"solc": "solc4.25" +``` +**Number Value CLI Options** + +Flags in CLI API that accept numbers will be store as **JSON Strings** not as **JSON Numbers**. Example: + +```{contents} +"smt_timeout": "600" +``` + +**Boolean Value CLI Options** + +Since boolean flags in CLI API do not get a value they will be store as **JSON true**. Example: + +```{contents} +"send_only": true +``` +**List Value CLI Options** + +Flags in CLI API that accept multiple strings will be stored as **JSON Arrays**. Example: +```{contents} + "packages": [ + "@balancer-labs/v2-solidity-utils=pkg/solidity-utils", + "@balancer-labs/v2-vault=pkg/vault" + ] +``` + +**Map Value CLI Options** + +Flags in CLI API that are maps will be stored as **JSON Objects**. Example: +```{contents} + "solc_map": { + "A": "solc5.11", + "B": "solc5.9", + "C": "solc6.8" + } + +``` + +
+Whenever certoraRun completes execution successfully the equivalent +conf file is generated +and is stored as run.conf in the build directory under .certora_interal. +

Conf file of the latest run can be found in: +

+./.certora_internal/latest/run.conf +
+
+ +**Complete Example** + +```{contents} +certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol --verify A:SolcArgs/Trigger.spec --solc_map SolcArgs/A.sol=solc6.1,B=solc6.1,C=solc5.12 --multi_assert_check +``` +```{contents} +{ + "files": [ + "SolcArgs/A.sol", + "SolcArgs/A.sol:B", + "SolcArgs/C.sol" + ], + "multi_assert_check": true, + "solc_map": { + "B": "solc6.1", + "C": "solc5.12", + "SolcArgs/A.sol": "solc6.1" + }, + "verify": "A:SolcArgs/Trigger.spec" +} +``` diff --git a/docs/prover/cli/index.md b/docs/prover/cli/index.md index e7d0fa38..5e32c8fc 100644 --- a/docs/prover/cli/index.md +++ b/docs/prover/cli/index.md @@ -8,5 +8,6 @@ Certora Prover CLI verification.md linking.md options.md +conf-file-api.md ``` From 01f85282efb3882e3db5925b9020d16140d72e39 Mon Sep 17 00:00:00 2001 From: rahav Date: Tue, 22 Aug 2023 15:45:32 +0300 Subject: [PATCH 02/61] fix content --- docs/prover/cli/conf-file-api.md | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 03390d75..8074ee02 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -18,7 +18,7 @@ Converting from CLI Options to JSON **JSON Keys** JSON keys in the conf file are the flag names without the leading dashes: -```{contents} Overview +``` The CLI flag --verify will be stored under the "verify" in the conf file ``` The JSON key for the input files in the CLI API is **"files"** @@ -26,14 +26,14 @@ The JSON key for the input files in the CLI API is **"files"** **String Value CLI Options** Flags in CLI API that accept a single string will be stored as **JSON Strings**. Example: -```{contents} +``` "solc": "solc4.25" ``` **Number Value CLI Options** Flags in CLI API that accept numbers will be store as **JSON Strings** not as **JSON Numbers**. Example: -```{contents} +``` "smt_timeout": "600" ``` @@ -41,13 +41,13 @@ Flags in CLI API that accept numbers will be store as **JSON Strings** not as ** Since boolean flags in CLI API do not get a value they will be store as **JSON true**. Example: -```{contents} +``` "send_only": true ``` **List Value CLI Options** Flags in CLI API that accept multiple strings will be stored as **JSON Arrays**. Example: -```{contents} +``` "packages": [ "@balancer-labs/v2-solidity-utils=pkg/solidity-utils", "@balancer-labs/v2-vault=pkg/vault" @@ -57,7 +57,7 @@ Flags in CLI API that accept multiple strings will be stored as **JSON Arrays**. **Map Value CLI Options** Flags in CLI API that are maps will be stored as **JSON Objects**. Example: -```{contents} +``` "solc_map": { "A": "solc5.11", "B": "solc5.9", @@ -78,10 +78,10 @@ and is stored as run.conf in the build directory under **Complete Example** -```{contents} +``` certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol --verify A:SolcArgs/Trigger.spec --solc_map SolcArgs/A.sol=solc6.1,B=solc6.1,C=solc5.12 --multi_assert_check ``` -```{contents} +``` { "files": [ "SolcArgs/A.sol", From 0678a26f5e6b6ee2f3ed138aea3009d07e0d72a8 Mon Sep 17 00:00:00 2001 From: rahav Date: Tue, 22 Aug 2023 15:56:58 +0300 Subject: [PATCH 03/61] json5 refernce --- docs/prover/cli/conf-file-api.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 8074ee02..036fa4b0 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -3,7 +3,8 @@ Certora Prover Conf File API The **Conf File API** is an alternative API for  `certoraRun` . In terms of functionality this API is identical to the [CLI Options](options.md). Instead of calling `certoraRun` -with a list of shell flags, some or all the flags can be stored in a [JSON](https://www.json.org/json-en.html) file: +with a list of shell flags, some or all the flags can be stored in a [JSON](https://www.json.org/json-en.html) file +(to be more precise the format is [JSON5](https://json5.org/)): ```bash certoraRun my_params.conf From f125ae259e90671c694197bbac384bbde8541dc0 Mon Sep 17 00:00:00 2001 From: rahav Date: Tue, 22 Aug 2023 16:40:05 +0300 Subject: [PATCH 04/61] spelling --- docs/prover/cli/conf-file-api.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 036fa4b0..6eb61815 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -2,7 +2,7 @@ Certora Prover Conf File API ============================ The **Conf File API** is an alternative API for  `certoraRun` . In terms of functionality -this API is identical to the [CLI Options](options.md). Instead of calling `certoraRun` +this API is identical to the [CLI Options](options.md) API. Instead of calling `certoraRun` with a list of shell flags, some or all the flags can be stored in a [JSON](https://www.json.org/json-en.html) file (to be more precise the format is [JSON5](https://json5.org/)): @@ -18,7 +18,7 @@ Converting from CLI Options to JSON **JSON Keys** -JSON keys in the conf file are the flag names without the leading dashes: +JSON keys in the conf file are the CLI option flag names without the leading dashes: ``` The CLI flag --verify will be stored under the "verify" in the conf file ``` @@ -32,7 +32,7 @@ Flags in CLI API that accept a single string will be stored as **JSON Strings**. ``` **Number Value CLI Options** -Flags in CLI API that accept numbers will be store as **JSON Strings** not as **JSON Numbers**. Example: +Flags in CLI API that accept numbers will be stored as **JSON Strings** not as **JSON Numbers**. Example: ``` "smt_timeout": "600" @@ -40,7 +40,7 @@ Flags in CLI API that accept numbers will be store as **JSON Strings** not as ** **Boolean Value CLI Options** -Since boolean flags in CLI API do not get a value they will be store as **JSON true**. Example: +Since boolean flags in CLI API do not get a value they will be stored as **JSON true**. Example: ``` "send_only": true From 87400d12a78a78b7ec9bf51a6b6bd266b6203a11 Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 23 Aug 2023 13:11:21 +0300 Subject: [PATCH 05/61] Chandra's comments --- docs/prover/cli/conf-file-api.md | 38 ++++++++++++++++++-------------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 6eb61815..b0c26b5b 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -6,22 +6,22 @@ this API is identical to the [CLI Options](options.md) API. Instead of calling ` with a list of shell flags, some or all the flags can be stored in a [JSON](https://www.json.org/json-en.html) file (to be more precise the format is [JSON5](https://json5.org/)): -```bash +``` certoraRun my_params.conf ``` -
-To denote a text file as a conf file use the .conf suffix -
-Converting from CLI Options to JSON ------------------------------------ +Conf files must use the .conf suffix + + +How CLI Options are mapped to JSON +---------------------------------- **JSON Keys** -JSON keys in the conf file are the CLI option flag names without the leading dashes: -``` -The CLI flag --verify will be stored under the "verify" in the conf file -``` +JSON keys in the conf file are the CLI option flag names without the leading dashes. +For example, +the CLI flag **--verify** will be stored under the **"verify"** in the conf file + The JSON key for the input files in the CLI API is **"files"** **String Value CLI Options** @@ -40,7 +40,7 @@ Flags in CLI API that accept numbers will be stored as **JSON Strings** not as * **Boolean Value CLI Options** -Since boolean flags in CLI API do not get a value they will be stored as **JSON true**. Example: +Since boolean flags in the CLI API do not get a value they will be stored as **JSON true**. Example: ``` "send_only": true @@ -67,21 +67,25 @@ Flags in CLI API that are maps will be stored as **JSON Objects**. Example: ``` -
+ Whenever certoraRun completes execution successfully the equivalent conf file is generated -and is stored as run.conf in the build directory under .certora_interal. +and is stored as run.conf in the build directory under .certora_internal.

Conf file of the latest run can be found in: -

-./.certora_internal/latest/run.conf -
-
+ +``` +./.certora_internal/latest/run.conf +``` + **Complete Example** +The command line: ``` certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol --verify A:SolcArgs/Trigger.spec --solc_map SolcArgs/A.sol=solc6.1,B=solc6.1,C=solc5.12 --multi_assert_check ``` + +will generate the conf file below: ``` { "files": [ From fcf769f16d94fe7adf559a0b7446b06406e21123 Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 23 Aug 2023 13:40:51 +0300 Subject: [PATCH 06/61] Chandra's comments --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index b0c26b5b..90f6e6cf 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -70,7 +70,7 @@ Flags in CLI API that are maps will be stored as **JSON Objects**. Example: Whenever certoraRun completes execution successfully the equivalent conf file is generated -and is stored as run.conf in the build directory under .certora_internal. +and is stored as `**run.conf**` in the build directory under **`.certora_internal`**.

Conf file of the latest run can be found in: ``` From 6452ca49fc6bbaf5026f155543337a1829121f3c Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 23 Aug 2023 14:32:35 +0300 Subject: [PATCH 07/61] Chandra's comments --- docs/prover/cli/conf-file-api.md | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 90f6e6cf..4aa62788 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -67,10 +67,8 @@ Flags in CLI API that are maps will be stored as **JSON Objects**. Example: ``` - -Whenever certoraRun completes execution successfully the equivalent -conf file is generated -and is stored as `**run.conf**` in the build directory under **`.certora_internal`**. +A conf file is generated each time certoraRun completes execution successfully. +The conf file is stored as `**run.conf**` in the build directory under **`.certora_internal`**.

Conf file of the latest run can be found in: ``` From b5b14ee9a0c454d882602596c5c7aa7c90649c45 Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 23 Aug 2023 14:36:07 +0300 Subject: [PATCH 08/61] Chandra's comments --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 4aa62788..87210283 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -67,7 +67,7 @@ Flags in CLI API that are maps will be stored as **JSON Objects**. Example: ``` -A conf file is generated each time certoraRun completes execution successfully. +A conf file is generated each time `certoraRun` completes execution successfully. The conf file is stored as `**run.conf**` in the build directory under **`.certora_internal`**.

Conf file of the latest run can be found in: From 10fd1b778824da9923c168f69d09cbb0d22bbeb3 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Tue, 5 Sep 2023 12:20:51 +0300 Subject: [PATCH 09/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: shellygr --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 87210283..935c4f49 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -1,7 +1,7 @@ Certora Prover Conf File API ============================ -The **Conf File API** is an alternative API for  `certoraRun` . In terms of functionality +The **Conf File API** is an alternative API for `certoraRun`. In terms of functionality this API is identical to the [CLI Options](options.md) API. Instead of calling `certoraRun` with a list of shell flags, some or all the flags can be stored in a [JSON](https://www.json.org/json-en.html) file (to be more precise the format is [JSON5](https://json5.org/)): From e1de9f57cdc9c379b26c28ae4878e9a4b0a4faca Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Tue, 5 Sep 2023 15:48:21 +0300 Subject: [PATCH 10/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 935c4f49..8306459e 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -10,7 +10,7 @@ with a list of shell flags, some or all the flags can be stored in a [JSON](http certoraRun my_params.conf ``` -Conf files must use the .conf suffix +Conf files must use the `.conf` suffix How CLI Options are mapped to JSON From 4c962660219b8caf7e376632cb43353a361a74d4 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Thu, 7 Sep 2023 11:31:44 +0300 Subject: [PATCH 11/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: shellygr --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 8306459e..58e912df 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -40,7 +40,7 @@ Flags in CLI API that accept numbers will be stored as **JSON Strings** not as * **Boolean Value CLI Options** -Since boolean flags in the CLI API do not get a value they will be stored as **JSON true**. Example: +Since some boolean flags in the CLI API do not get a value they will be stored as **JSON true**. Example: ``` "send_only": true From 0d227af9a40befdf3de345084fa60ebbfa181d54 Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 7 Sep 2023 13:58:54 +0300 Subject: [PATCH 12/61] Mike's comments --- docs/prover/cli/conf-file-api.md | 120 +++++++++++++++++++++++++++---- docs/prover/cli/options.md | 2 +- 2 files changed, 106 insertions(+), 16 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 87210283..db113205 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -1,29 +1,108 @@ -Certora Prover Conf File API -============================ +Certora Prover Conf File Format +=============================== -The **Conf File API** is an alternative API for  `certoraRun` . In terms of functionality -this API is identical to the [CLI Options](options.md) API. Instead of calling `certoraRun` -with a list of shell flags, some or all the flags can be stored in a [JSON](https://www.json.org/json-en.html) file +Conf files are an alternative way for setting arguments for the + `certoraRun` tool. In terms of functionality +using conf files is identical to the use of the [CLI Options](options.md). Instead of calling `certoraRun` +with a list of shell flags, some or all the flags can be stored in a JSON file (to be more precise the format is [JSON5](https://json5.org/)): ``` certoraRun my_params.conf ``` -Conf files must use the .conf suffix +* Conf files must use the .conf suffix +* How CLI Options are mapped to JSON ---------------------------------- -**JSON Keys** +Command-line arguments are stored as key-value pairs in the conf file. +The keys are the names of the parameters (with the leading -- removed). +For example, +``` +certoraRun --verify Example:example.spec +``` +is equivalent to running with the following conf file: + +``` +{ "verify": "Example:example.spec" } +``` +The values in the map depend on the type of arguments: + +* for flags that take no additional arguments (such as[--send_only](options.md#--send_only)), +the value should be true. For example, +``` +certoraRun --send_only +``` -JSON keys in the conf file are the CLI option flag names without the leading dashes. -For example, -the CLI flag **--verify** will be stored under the **"verify"** in the conf file +would be encoded as: +``` +{ "send_only": true } +``` -The JSON key for the input files in the CLI API is **"files"** +* flags that take a single additional argument (such as[--solc](options.md#--solc) or as [--loop_iter](options.md#--loop_iter) + are encoded as a JSON string. For example, +``` +certoraRun --solc solc4.25 --loop_iter 2 +``` +would be encoded as: +``` +{ "solc": "solc4.25", "loop_iter": "2" } +``` + +Note that conf files do not use JSON numbers; numbers are encoded as strings. + +* flags that take multiple additional arguments (such as [--packages](options.md#--packages)) +are encoded as JSON lists. For example, +``` +certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils @balancer-labs/v2-vault=pkg/vault +``` +would be encoded as: +``` +{ +"packages": [ + "@balancer-labs/v2-solidity-utils=pkg/solidity-utils", + "@balancer-labs/v2-vault=pkg/vault" + ] +} +``` + + + + + + +Command-line arguments are stored as key-value pairs in the conf file. +* The keys are the names of the parameters +(with the leading -- removed). For example, the **--verify** flag +``` +certoraRun ... --verify Example:example.spec ... +``` +will appear in the conf file as: +``` +{ + ... + "verify": "Example:example.spec" + ... +} +``` + +* The input files in the CLI API will be stored under the key **files** + +``` +certoraRun example.sol ... +``` +will appear in the conf file as: +``` +{ + ... + "files": "Example:example.spec" + ... +} +``` **String Value CLI Options** Flags in CLI API that accept a single string will be stored as **JSON Strings**. Example: @@ -66,15 +145,26 @@ Flags in CLI API that are maps will be stored as **JSON Objects**. Example: } ``` +**Generating a Conf File** -A conf file is generated each time `certoraRun` completes execution successfully. -The conf file is stored as `**run.conf**` in the build directory under **`.certora_internal`**. -

Conf file of the latest run can be found in: +After each successful run of `certoraRun` a conf file is generated and is +stored in the file **run.conf** under the internal directory of that run. +The conf file of the latest run can be found in: ``` -./.certora_internal/latest/run.conf +.certora_internal/latest/run.conf ``` +Instead of generating a complete conf file from scratch, users can take +one of these generated conf files as a basis for their modifications. + +**Conf Files in the VS Code IDE Extension** + +VS Code users can generate conf files using the [Certora IDE Extension](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover). The extension +offers an intuitive UI for configuring Prover jobs. Each job +keeps a conf file that allows rerunning the job. All conf files +are stored in the VS code project under the folder  `certora/confs`. A link to the job's conf file +can also be found in the files section of the run report once the job is completed. **Complete Example** diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index 5efcd13d..5b0f301a 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -463,7 +463,7 @@ By default, we do not use a cache. If you want to use a cache to speed up the bu **Example** `certoraRun Bank.sol --verify Bank:Bank.spec --cache bank_regulation` -(--smt_timeout)= +_timeout)= ### `--smt_timeout ` **What does it do?** From 48179a2ffed01ab3d0a7068f905fa1728d6c0434 Mon Sep 17 00:00:00 2001 From: rahav Date: Tue, 14 Nov 2023 12:19:02 +0200 Subject: [PATCH 13/61] fix --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 3b86e993..5b1c0c78 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -42,7 +42,7 @@ would be encoded as: { "send_only": true } ``` -* flags that take a single additional argument (such as[--solc](options.md#--solc) or as [--loop_iter](options.md#--loop_iter) +* flags that take a single additional argument (such as[--solc](options.md#--solc)) or as [--loop_iter](options.md#--loop_iter) are encoded as a JSON string. For example, ``` certoraRun --solc solc4.25 --loop_iter 2 From 378125feb5084a80ca49d6aa38cf3dd4e9b6d5c6 Mon Sep 17 00:00:00 2001 From: rahav Date: Tue, 14 Nov 2023 12:29:11 +0200 Subject: [PATCH 14/61] fix --- docs/prover/cli/conf-file-api.md | 6 +++--- docs/prover/cli/options.md | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 5b1c0c78..e2d995e6 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -31,7 +31,7 @@ is equivalent to running with the following conf file: ``` The values in the map depend on the type of arguments: -* for flags that take no additional arguments (such as[--send_only](options.md#--send_only)), +* for flags that take no additional arguments (such as[--send_only](options.html?highlight=options#send-only)), the value should be true. For example, ``` certoraRun --send_only @@ -42,7 +42,7 @@ would be encoded as: { "send_only": true } ``` -* flags that take a single additional argument (such as[--solc](options.md#--solc)) or as [--loop_iter](options.md#--loop_iter) +* flags that take a single additional argument (such as[--solc](options.md#--solc)) or as [--loop_iter](options.html?highlight=options#loop-iter) are encoded as a JSON string. For example, ``` certoraRun --solc solc4.25 --loop_iter 2 @@ -55,7 +55,7 @@ would be encoded as: Note that conf files do not use JSON numbers; numbers are encoded as strings. -* flags that take multiple additional arguments (such as [--packages](options.md#--packages)) +* flags that take multiple additional arguments (such as [--packages](highlight=options#packages)) are encoded as JSON lists. For example, ``` certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils @balancer-labs/v2-vault=pkg/vault diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index 98f2214b..7b4ff474 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -454,7 +454,7 @@ By default, we do not use a cache. If you want to use a cache to speed up the bu **Example** `certoraRun Bank.sol --verify Bank:Bank.spec --cache bank_regulation` -_timeout)= +(--smt_timeout)= ### `--smt_timeout ` **What does it do?** From b2c2c5c482cdd844d897972c73162f2a1391d3fb Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 16 Nov 2023 16:28:44 +0200 Subject: [PATCH 15/61] fix ref --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index e2d995e6..c0a66e00 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -31,7 +31,7 @@ is equivalent to running with the following conf file: ``` The values in the map depend on the type of arguments: -* for flags that take no additional arguments (such as[--send_only](options.html?highlight=options#send-only)), +* for flags that take no additional arguments (such as {ref}`--send_only`), the value should be true. For example, ``` certoraRun --send_only From 8c698c26c143fd76f29b3a149fc7106bb116589f Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 16 Nov 2023 16:31:30 +0200 Subject: [PATCH 16/61] fix ref --- docs/prover/cli/conf-file-api.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index c0a66e00..5c43551f 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -42,7 +42,7 @@ would be encoded as: { "send_only": true } ``` -* flags that take a single additional argument (such as[--solc](options.md#--solc)) or as [--loop_iter](options.html?highlight=options#loop-iter) +* flags that take a single additional argument (such as {ref}`--solc`) or as {ref}`--loop_iter`) are encoded as a JSON string. For example, ``` certoraRun --solc solc4.25 --loop_iter 2 @@ -55,7 +55,7 @@ would be encoded as: Note that conf files do not use JSON numbers; numbers are encoded as strings. -* flags that take multiple additional arguments (such as [--packages](highlight=options#packages)) +* flags that take multiple additional arguments (such as {ref}`--packages`) are encoded as JSON lists. For example, ``` certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils @balancer-labs/v2-vault=pkg/vault From ebc0af8122affd275cab44f8dc390cff6c2fb59a Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 16 Nov 2023 16:44:28 +0200 Subject: [PATCH 17/61] fix ref --- docs/prover/cli/options.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index 7b4ff474..a8228c24 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -243,7 +243,7 @@ When we do not care much for the output. It is recommended when running the tool Options that control the Solidity compiler ------------------------------------------ - +(--solc)= ### `--solc` **What does it do?** @@ -336,6 +336,7 @@ By default, we look for the packages in `$NODE_PATH`. If the packages are in any **Example** `certoraRun Bank.sol --verify Bank:Bank.spec --packages_path Solidity/packages` +(--packages)= ### `--packages` **What does it do?** From 0a661f3522e84b692960bdd22cb3b3121689225c Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 16 Nov 2023 17:43:51 +0200 Subject: [PATCH 18/61] remove redundent text --- docs/prover/cli/conf-file-api.md | 63 ++++---------------------------- 1 file changed, 7 insertions(+), 56 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 5c43551f..26922beb 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -12,14 +12,14 @@ certoraRun my_params.conf ``` * Conf files must use the `.conf` suffix -* + How CLI Options are mapped to JSON ---------------------------------- Command-line arguments are stored as key-value pairs in the conf file. -The keys are the names of the parameters (with the leading -- removed). +The keys are the names of the parameters (with the leading `--` removed). For example, ``` certoraRun --verify Example:example.spec @@ -31,8 +31,8 @@ is equivalent to running with the following conf file: ``` The values in the map depend on the type of arguments: -* for flags that take no additional arguments (such as {ref}`--send_only`), -the value should be true. For example, +* boolean flags that take no arguments (such as {ref}`--send_only`), +the value should be `true`. For example, ``` certoraRun --send_only ``` @@ -42,7 +42,7 @@ would be encoded as: { "send_only": true } ``` -* flags that take a single additional argument (such as {ref}`--solc`) or as {ref}`--loop_iter`) +* flags that expect a single argument (such as {ref}`--solc`) or as {ref}`--loop_iter`) are encoded as a JSON string. For example, ``` certoraRun --solc solc4.25 --loop_iter 2 @@ -55,7 +55,7 @@ would be encoded as: Note that conf files do not use JSON numbers; numbers are encoded as strings. -* flags that take multiple additional arguments (such as {ref}`--packages`) +* flags that expect multiple arguments (such as {ref}`--packages`) are encoded as JSON lists. For example, ``` certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils @balancer-labs/v2-vault=pkg/vault @@ -71,25 +71,6 @@ would be encoded as: ``` - - - - -Command-line arguments are stored as key-value pairs in the conf file. -* The keys are the names of the parameters -(with the leading -- removed). For example, the **--verify** flag -``` -certoraRun ... --verify Example:example.spec ... -``` -will appear in the conf file as: -``` -{ - ... - "verify": "Example:example.spec" - ... -} -``` - * The input files in the CLI API will be stored under the key **files** ``` @@ -99,40 +80,10 @@ will appear in the conf file as: ``` { ... - "files": "Example:example.spec" + "files": "example.sol" ... } ``` -**String Value CLI Options** - -Flags in CLI API that accept a single string will be stored as **JSON Strings**. Example: -``` -"solc": "solc4.25" -``` -**Number Value CLI Options** - -Flags in CLI API that accept numbers will be stored as **JSON Strings** not as **JSON Numbers**. Example: - -``` -"smt_timeout": "600" -``` - -**Boolean Value CLI Options** - -Since some boolean flags in the CLI API do not get a value they will be stored as **JSON true**. Example: - -``` -"send_only": true -``` -**List Value CLI Options** - -Flags in CLI API that accept multiple strings will be stored as **JSON Arrays**. Example: -``` - "packages": [ - "@balancer-labs/v2-solidity-utils=pkg/solidity-utils", - "@balancer-labs/v2-vault=pkg/vault" - ] -``` **Map Value CLI Options** From 6703df49e84d3907539b5e52c267af2d28ef5f07 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 13 Dec 2023 14:58:35 +0200 Subject: [PATCH 19/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 26922beb..9de64cfd 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -33,7 +33,7 @@ The values in the map depend on the type of arguments: * boolean flags that take no arguments (such as {ref}`--send_only`), the value should be `true`. For example, -``` +```sh certoraRun --send_only ``` From 5deca4a735a759f8c8285825e3e5006773abae49 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 13 Dec 2023 14:59:13 +0200 Subject: [PATCH 20/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 9de64cfd..b7fd8d88 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -26,7 +26,7 @@ certoraRun --verify Example:example.spec ``` is equivalent to running with the following conf file: -``` +```json { "verify": "Example:example.spec" } ``` The values in the map depend on the type of arguments: From 5a6310f562b885a81a9840d952b92b90d0326f7a Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 13 Dec 2023 16:53:55 +0200 Subject: [PATCH 21/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index b7fd8d88..2092da58 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -71,7 +71,7 @@ would be encoded as: ``` -* The input files in the CLI API will be stored under the key **files** +* The input files in the CLI API will be stored under the key `files` ``` certoraRun example.sol ... From ce4fcd990130a9b6be2636b56764d142f9014db7 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 13 Dec 2023 17:20:39 +0200 Subject: [PATCH 22/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 2092da58..e84d8631 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -99,12 +99,7 @@ Flags in CLI API that are maps will be stored as **JSON Objects**. Example: **Generating a Conf File** After each successful run of `certoraRun` a conf file is generated and is -stored in the file **run.conf** under the internal directory of that run. -The conf file of the latest run can be found in: - -``` -.certora_internal/latest/run.conf -``` +stored in the file `.certora_internal/latest/run.conf`. Instead of generating a complete conf file from scratch, users can take one of these generated conf files as a basis for their modifications. From 9c9fe3eabcec4df7398f21e2ef49c5195cfd7516 Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 13 Dec 2023 17:22:06 +0200 Subject: [PATCH 23/61] Mike's comments --- docs/prover/cli/conf-file-api.md | 145 ++++++++++++++++++------------- docs/prover/cli/options.md | 26 ++++-- 2 files changed, 103 insertions(+), 68 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 26922beb..1c496a3b 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -1,5 +1,5 @@ -Certora Prover Conf File Format -=============================== +Conf Files +========== Conf files are an alternative way for setting arguments for the  `certoraRun` tool. In terms of functionality @@ -31,75 +31,96 @@ is equivalent to running with the following conf file: ``` The values in the map depend on the type of arguments: -* boolean flags that take no arguments (such as {ref}`--send_only`), -the value should be `true`. For example, -``` -certoraRun --send_only -``` +* Boolean flags take no arguments (such as {ref}`--send_only`), in +the conf file the value should be `true`, since the default value of boolean attributes. For example, +is `false` there is no need to set a boolean attribute to values other than `true` + ``` + certoraRun --send_only + ``` -would be encoded as: -``` -{ "send_only": true } -``` + would be encoded as: + ``` + { "send_only": true } + ``` -* flags that expect a single argument (such as {ref}`--solc`) or as {ref}`--loop_iter`) +* Flags that expect a single argument (such as {ref}`--solc`) or as {ref}`--loop_iter`) are encoded as a JSON string. For example, -``` -certoraRun --solc solc4.25 --loop_iter 2 -``` + ``` + certoraRun --solc solc4.25 --loop_iter 2 + ``` + would be encoded as: + ``` + { "solc": "solc4.25", "loop_iter": "2" } + ``` + Note that conf files do not use JSON numbers; numbers are encoded as strings. -would be encoded as: -``` -{ "solc": "solc4.25", "loop_iter": "2" } -``` -Note that conf files do not use JSON numbers; numbers are encoded as strings. - -* flags that expect multiple arguments (such as {ref}`--packages`) +* Flags that expect multiple arguments (such as {ref}`--packages`) are encoded as JSON lists. For example, -``` -certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils @balancer-labs/v2-vault=pkg/vault -``` -would be encoded as: -``` -{ -"packages": [ - "@balancer-labs/v2-solidity-utils=pkg/solidity-utils", - "@balancer-labs/v2-vault=pkg/vault" - ] -} -``` + ``` + certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils \ + @balancer-labs/v2-vault=pkg/vault + ``` + would be encoded as: + ``` + { + "packages": [ + "@balancer-labs/v2-solidity-utils=pkg/solidity-utils", + "@balancer-labs/v2-vault=pkg/vault" + ] + } + ``` * The input files in the CLI API will be stored under the key **files** -``` -certoraRun example.sol ... -``` -will appear in the conf file as: -``` -{ - ... - "files": "example.sol" - ... -} -``` + ``` + certoraRun example.sol ... + ``` + will appear in the conf file as: + ``` + { + ... + "files": [ "example.sol" ], + ... + } + ``` -**Map Value CLI Options** -Flags in CLI API that are maps will be stored as **JSON Objects**. Example: -``` +* Flags in CLI API that are maps ({ref}`--solc_map` and {ref}`--solc_optimize_map`) will be stored as JSON objects. + For example, + ``` + certoraRun --solc_map A=solc5.11,B=solc5.9,C=solc6.8 + ``` + would be encoded as: + ``` + "solc_map": { "A": "solc5.11", "B": "solc5.9", "C": "solc6.8" } -``` -**Generating a Conf File** + ``` + and + + ``` + certoraRun --solc_optimize_map A=200,B=200,C=300 + ``` + + would be encoded as: + ``` + "solc_optimize_map": { + "A": "200", + "B": "200", + "C": "300" + } + + ``` +## Generating a Conf File After each successful run of `certoraRun` a conf file is generated and is -stored in the file **run.conf** under the internal directory of that run. +stored in the file `run.conf` under the internal directory of that run. The conf file of the latest run can be found in: ``` @@ -109,19 +130,23 @@ The conf file of the latest run can be found in: Instead of generating a complete conf file from scratch, users can take one of these generated conf files as a basis for their modifications. -**Conf Files in the VS Code IDE Extension** +## Conf Files in the VS Code IDE Extension +The [Certora IDE Extension](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover) +automatically generates conf files for each configured job; these conf files +are stored in the VS code project under the folder  `certora/confs`. +Once the job is completed, a link to the job's conf file can also be found in the files section of the +run report. -VS Code users can generate conf files using the [Certora IDE Extension](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover). The extension -offers an intuitive UI for configuring Prover jobs. Each job -keeps a conf file that allows rerunning the job. All conf files -are stored in the VS code project under the folder  `certora/confs`. A link to the job's conf file -can also be found in the files section of the run report once the job is completed. - -**Complete Example** +### Complete Example The command line: ``` -certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol --verify A:SolcArgs/Trigger.spec --solc_map SolcArgs/A.sol=solc6.1,B=solc6.1,C=solc5.12 --multi_assert_check +certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol \ + --verify A:SolcArgs/Trigger.spec \ + --solc_map SolcArgs/A.sol=solc6.1,B=solc6.1,C=solc5.12 \ + --multi_assert_check + + ``` will generate the conf file below: diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index 1fec7234..ec6b0e8b 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -1,5 +1,5 @@ -Certora Prover CLI Options -========================== +CLI Options +=========== The `certoraRun` utility invokes the Solidity compiler and afterwards sends the job to Certora's servers.  @@ -267,28 +267,32 @@ When different contracts have to be compiled for different Solidity versions. **Example** `certoraRun Bank.sol Exchange.sol --verify Bank:Bank.spec --solc_map Bank=solc4.25,Exchange=solc6.7` + ### `--solc_optimize` **What does it do?** -Passes the value of this option to the solidity compiler's option `--solc_optimize`. +Passes the value of this option as is to the solidity compiler's option `--optimize` and `--optimize-runs`. **When to use it?** -When we want to select the Solidity compiler EVM version +When we want to activate in the solidity compiler the opcode-based optimizer for the generated bytecode and control the +number of times the optimizer will be activated (if no value is set, the compiler's default is 200 runs) **Example** -`certoraRun Bank.sol --verify Bank:Bank.spec --solc_evm_version Istanbul` +`certoraRun Bank.sol --verify Bank:Bank.spec --solc_optimize 300` -### `--solc_optimize` + +### `--solc_optimize_map` **What does it do?** +Set optimize values when different files run with different number of runs Passes the value of this option as is to the solidity compiler's option `--optimize` and `--optimize-runs`. **When to use it?** -When we want to activate in the solidity compiler the opcode-based optimizer for the generated bytecode and control the +When we want to activate in the solidity compiler the opcode-based optimizer for the generated bytecode and control the number of times the optimizer will be activated (if no value is set, the compiler's default is 200 runs) **Example** -`certoraRun Bank.sol --verify Bank:Bank.spec --solc_optimize 300` +`certoraRun Bank.sol --verify Bank:Bank.spec --solc_optimize_map Bank=200,Exchange=300` ### `--solc_via_ir` @@ -820,3 +824,9 @@ splits generated here is equal to `2^n` where `n` is the initial splitting depth (unless the program has less than `n` branchings, which will be rare in practice). +Using Conf Files +---------------- +For larger projects, the command line for running the Certora Prover can become large +and cumbersome. It is therefore recommended to use configuration files instead. +These are [JSON5](https://json5.org/) files (with .conf extension) that hold the parameters and options for the Prover. +See more on conf file [here3](./conf-file-api.md) \ No newline at end of file From 64c8cb24d89ebbc1a93e12d07ba2eb6975c73adc Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 13 Dec 2023 17:33:15 +0200 Subject: [PATCH 24/61] Mike's comments --- docs/prover/cli/options.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index ec6b0e8b..4482c778 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -267,7 +267,7 @@ When different contracts have to be compiled for different Solidity versions. **Example** `certoraRun Bank.sol Exchange.sol --verify Bank:Bank.spec --solc_map Bank=solc4.25,Exchange=solc6.7` - +(--solc_optimize)= ### `--solc_optimize` **What does it do?** @@ -280,7 +280,7 @@ number of times the optimizer will be activated (if no value is set, the compile **Example** `certoraRun Bank.sol --verify Bank:Bank.spec --solc_optimize 300` - +(--solc_optimize_map)= ### `--solc_optimize_map` **What does it do?** From 35090a6775095c681906aa8eaa29f294b87fea97 Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 13 Dec 2023 17:44:52 +0200 Subject: [PATCH 25/61] ref --- docs/prover/cli/options.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index 4482c778..1916a673 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -255,7 +255,7 @@ Whenever you want to use a Solidity compiler executable with a non-default name. **Example** `certoraRun Bank.sol --verify Bank:Bank.spec --solc solc8.1` - +(--solc_map)= ### `--solc_map` **What does it do?** From b8721a5028e0f0f10e14d6fff753da9a6c36833c Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 13 Dec 2023 17:47:27 +0200 Subject: [PATCH 26/61] test_ref --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 708ed7c1..efac4c6a 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -87,7 +87,7 @@ are encoded as JSON lists. For example, ``` -* Flags in CLI API that are maps ({ref}`--solc_map` and {ref}`--solc_optimize_map`) will be stored as JSON objects. +* Flags in CLI API that are maps ({ref}`--packages` and {ref}`--packages`) will be stored as JSON objects. For example, ``` certoraRun --solc_map A=solc5.11,B=solc5.9,C=solc6.8 From a4d1e99f2be57664a2de7458ae433383f0155dd0 Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 13 Dec 2023 17:53:26 +0200 Subject: [PATCH 27/61] ref --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index efac4c6a..708ed7c1 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -87,7 +87,7 @@ are encoded as JSON lists. For example, ``` -* Flags in CLI API that are maps ({ref}`--packages` and {ref}`--packages`) will be stored as JSON objects. +* Flags in CLI API that are maps ({ref}`--solc_map` and {ref}`--solc_optimize_map`) will be stored as JSON objects. For example, ``` certoraRun --solc_map A=solc5.11,B=solc5.9,C=solc6.8 From 86624af7dba50f11d3402a2f25b6191b16d9df5d Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 14 Dec 2023 12:15:57 +0200 Subject: [PATCH 28/61] clean --- docs/prover/cli/conf-file-api.md | 48 +++++++++++++++----------------- 1 file changed, 23 insertions(+), 25 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 708ed7c1..7d17a1eb 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -19,7 +19,7 @@ How CLI Options are mapped to JSON ---------------------------------- Command-line arguments are stored as key-value pairs in the conf file. -The keys are the names of the parameters (with the leading `--` removed). +The keys are the names of the CLI options (with the leading `--` removed). For example, ``` certoraRun --verify Example:example.spec @@ -31,9 +31,23 @@ is equivalent to running with the following conf file: ``` The values in the map depend on the type of arguments: -* Boolean flags take no arguments (such as {ref}`--send_only`), in -the conf file the value should be `true`, since the default value of boolean attributes. For example, -is `false` there is no need to set a boolean attribute to values other than `true` +* The input files in the CLI API will be stored as list under the key `files` + + ``` + certoraRun example.sol ... + ``` + will appear in the conf file as: + ``` + { + ... + "files": [ "example.sol" ], + ... + } + ``` + +* Boolean options are options that take no arguments (for example {ref}`--send_only`). In +the conf file all keys must come with a value, the value for boolean options is `true`. +Since the default value of boolean options is `false` there is no need to set a boolean attribute to values other than `true` ```sh certoraRun --send_only ``` @@ -43,7 +57,7 @@ is `false` there is no need to set a boolean attribute to values other than `tru { "send_only": true } ``` -* Flags that expect a single argument (such as {ref}`--solc`) or as {ref}`--loop_iter`) +* Options that expect a single argument (for example {ref}`--solc`) or {ref}`--loop_iter`) are encoded as a JSON string. For example, ``` certoraRun --solc solc4.25 --loop_iter 2 @@ -52,10 +66,10 @@ is `false` there is no need to set a boolean attribute to values other than `tru ``` { "solc": "solc4.25", "loop_iter": "2" } ``` - Note that conf files do not use JSON numbers; numbers are encoded as strings. + Note that in conf files numbers are also encoded as strings. -* Flags that expect multiple arguments (such as {ref}`--packages`) +* Options that expect multiple arguments (for example {ref}`--packages`) are encoded as JSON lists. For example, ``` certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils \ @@ -71,23 +85,7 @@ are encoded as JSON lists. For example, } ``` - -* The input files in the CLI API will be stored under the key `files` - - ``` - certoraRun example.sol ... - ``` - will appear in the conf file as: - ``` - { - ... - "files": [ "example.sol" ], - ... - } - ``` - - -* Flags in CLI API that are maps ({ref}`--solc_map` and {ref}`--solc_optimize_map`) will be stored as JSON objects. +* Options that are maps ({ref}`--solc_map` and {ref}`--solc_optimize_map`) will be stored as JSON objects. For example, ``` certoraRun --solc_map A=solc5.11,B=solc5.9,C=solc6.8 @@ -128,7 +126,7 @@ The conf file of the latest run can be found in: ``` Instead of generating a complete conf file from scratch, users can take -one of these generated conf files as a basis for their modifications. +one of these generated conf files as a basis for their modifications. ## Conf Files in the VS Code IDE Extension The [Certora IDE Extension](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover) From eabbcec633e391fe5e9d6379a86c477e3a716b5a Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:14:31 +0200 Subject: [PATCH 29/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 7d17a1eb..05a3ead8 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -7,7 +7,7 @@ using conf files is identical to the use of the [CLI Options](options.md). Inste with a list of shell flags, some or all the flags can be stored in a JSON file (to be more precise the format is [JSON5](https://json5.org/)): -``` +```sh certoraRun my_params.conf ``` From 7a170f3befd8dec23a2637c9374c1e216544af0e Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:14:43 +0200 Subject: [PATCH 30/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 05a3ead8..a001c649 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -11,7 +11,7 @@ with a list of shell flags, some or all the flags can be stored in a JSON file certoraRun my_params.conf ``` -* Conf files must use the `.conf` suffix +Conf files must use the `.conf` suffix. From 8acdd86c86b4490ca6b3743454440830674b6f2d Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:14:55 +0200 Subject: [PATCH 31/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index a001c649..6710beb4 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -15,7 +15,7 @@ Conf files must use the `.conf` suffix. -How CLI Options are mapped to JSON +How CLI options are mapped to JSON ---------------------------------- Command-line arguments are stored as key-value pairs in the conf file. From 8b38c0973d70ad6d565fe98fe094dfde77266b6c Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:15:07 +0200 Subject: [PATCH 32/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 6710beb4..8830dff9 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -21,7 +21,7 @@ How CLI options are mapped to JSON Command-line arguments are stored as key-value pairs in the conf file. The keys are the names of the CLI options (with the leading `--` removed). For example, -``` +```sh certoraRun --verify Example:example.spec ``` is equivalent to running with the following conf file: From 055b3dc155844ef0091ccfa946efb3d19dda4aa5 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:15:20 +0200 Subject: [PATCH 33/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 8830dff9..41a258a2 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -31,7 +31,7 @@ is equivalent to running with the following conf file: ``` The values in the map depend on the type of arguments: -* The input files in the CLI API will be stored as list under the key `files` +* The input files in the CLI API will be stored as a list under the key `files`. For example, ``` certoraRun example.sol ... From 45bcdf3feccc3225a1cf35a939c3839569a67a37 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:15:30 +0200 Subject: [PATCH 34/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 41a258a2..68e03917 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -33,7 +33,7 @@ The values in the map depend on the type of arguments: * The input files in the CLI API will be stored as a list under the key `files`. For example, - ``` + ```sh certoraRun example.sol ... ``` will appear in the conf file as: From 64fedaa417fac0f56e74f0db312f9ccf4aec0993 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:15:55 +0200 Subject: [PATCH 35/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 68e03917..520c6ff7 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -47,7 +47,7 @@ The values in the map depend on the type of arguments: * Boolean options are options that take no arguments (for example {ref}`--send_only`). In the conf file all keys must come with a value, the value for boolean options is `true`. -Since the default value of boolean options is `false` there is no need to set a boolean attribute to values other than `true` +Since the default value of boolean options is `false` there is no need to set a boolean attribute to values other than `true`. For example, ```sh certoraRun --send_only ``` From 3d91b32bac79aab92c5666d4b45a304438f81826 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:16:03 +0200 Subject: [PATCH 36/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 520c6ff7..068764e2 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -57,7 +57,7 @@ Since the default value of boolean options is `false` there is no need to set a { "send_only": true } ``` -* Options that expect a single argument (for example {ref}`--solc`) or {ref}`--loop_iter`) +* Options that expect a single argument (for example {ref}`--solc` or {ref}`--loop_iter`) are encoded as a JSON string. For example, ``` certoraRun --solc solc4.25 --loop_iter 2 From eb99063dadd64e2ffc9c1a8ef8737fdc2e8cb94d Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:16:13 +0200 Subject: [PATCH 37/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 068764e2..e838e967 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -71,7 +71,7 @@ Since the default value of boolean options is `false` there is no need to set a * Options that expect multiple arguments (for example {ref}`--packages`) are encoded as JSON lists. For example, - ``` + ```sh certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils \ @balancer-labs/v2-vault=pkg/vault ``` From 8c7e90d5f12b7108bf65be7aa209350852eef5c5 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:16:22 +0200 Subject: [PATCH 38/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index e838e967..a300b403 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -74,7 +74,7 @@ are encoded as JSON lists. For example, ```sh certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils \ @balancer-labs/v2-vault=pkg/vault - ``` + ```json would be encoded as: ``` { From ca6e80c67c0a8dcd6eb141d8165a15448fc7156f Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:16:32 +0200 Subject: [PATCH 39/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index a300b403..7b23cb89 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -87,7 +87,7 @@ are encoded as JSON lists. For example, * Options that are maps ({ref}`--solc_map` and {ref}`--solc_optimize_map`) will be stored as JSON objects. For example, - ``` + ```sh certoraRun --solc_map A=solc5.11,B=solc5.9,C=solc6.8 ``` would be encoded as: From d810aeb01612020567cab8c26c52dd9d56c36b04 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:16:40 +0200 Subject: [PATCH 40/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 7b23cb89..95a54003 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -91,7 +91,7 @@ are encoded as JSON lists. For example, certoraRun --solc_map A=solc5.11,B=solc5.9,C=solc6.8 ``` would be encoded as: - ``` + ```json "solc_map": { "A": "solc5.11", From e944fda026a5e1e8a67aca62b87d13060f409927 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:17:01 +0200 Subject: [PATCH 41/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 95a54003..db929f38 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -93,11 +93,13 @@ are encoded as JSON lists. For example, would be encoded as: ```json - "solc_map": { - "A": "solc5.11", - "B": "solc5.9", - "C": "solc6.8" - } +{ + "solc_map": { + "A": "solc5.11", + "B": "solc5.9", + "C": "solc6.8" + } +} ``` and From 82b0b58d95ee0427d9d07942ab8d5d25c1c6ebf4 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:17:11 +0200 Subject: [PATCH 42/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index db929f38..b8ef18b9 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -104,7 +104,7 @@ are encoded as JSON lists. For example, ``` and - ``` + ```sh certoraRun --solc_optimize_map A=200,B=200,C=300 ``` From ff2bbe9be88eb05ed2b9183ca70f4aa2b9eedd7d Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:17:19 +0200 Subject: [PATCH 43/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index b8ef18b9..9ff4880d 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -109,7 +109,7 @@ are encoded as JSON lists. For example, ``` would be encoded as: - ``` + ```json "solc_optimize_map": { "A": "200", "B": "200", From 177cf9e1d3080a8bb2279e7f99d1be4e45fa0038 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:17:28 +0200 Subject: [PATCH 44/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 9ff4880d..17f0e8d6 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -110,11 +110,13 @@ are encoded as JSON lists. For example, would be encoded as: ```json - "solc_optimize_map": { - "A": "200", - "B": "200", - "C": "300" - } +{ + "solc_optimize_map": { + "A": "200", + "B": "200", + "C": "300" + } +} ``` ## Generating a Conf File From 21bceeefd7745ce711424beef02ca437fae92526 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:17:39 +0200 Subject: [PATCH 45/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 17f0e8d6..b5d5ae7a 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -119,7 +119,7 @@ are encoded as JSON lists. For example, } ``` -## Generating a Conf File +## Generating a conf file After each successful run of `certoraRun` a conf file is generated and is stored in the file `run.conf` under the internal directory of that run. From 05678f3c9118682465d6baa2c742d76026f8c54d Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:17:47 +0200 Subject: [PATCH 46/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index b5d5ae7a..2312a55e 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -125,7 +125,7 @@ After each successful run of `certoraRun` a conf file is generated and is stored in the file `run.conf` under the internal directory of that run. The conf file of the latest run can be found in: -``` +```sh .certora_internal/latest/run.conf ``` From eacc988355ce2500e96c5a8115d9c7e547756546 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:17:59 +0200 Subject: [PATCH 47/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 2312a55e..290b845b 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -132,7 +132,7 @@ The conf file of the latest run can be found in: Instead of generating a complete conf file from scratch, users can take one of these generated conf files as a basis for their modifications. -## Conf Files in the VS Code IDE Extension +## Conf files in the VS Code IDE extension The [Certora IDE Extension](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover) automatically generates conf files for each configured job; these conf files are stored in the VS code project under the folder  `certora/confs`. From f7ac815d9d5af7b8e22d7261fef9deb9a14910c5 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:18:08 +0200 Subject: [PATCH 48/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 290b845b..48e9bc66 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -135,7 +135,7 @@ one of these generated conf files as a basis for their modifications. ## Conf files in the VS Code IDE extension The [Certora IDE Extension](https://marketplace.visualstudio.com/items?itemName=Certora.vscode-certora-prover) automatically generates conf files for each configured job; these conf files -are stored in the VS code project under the folder  `certora/confs`. +are stored in the VS Code project under the folder  `certora/confs`. Once the job is completed, a link to the job's conf file can also be found in the files section of the run report. From 4fce2cae9a1861cd1769273037cd792d533161ba Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:18:16 +0200 Subject: [PATCH 49/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 48e9bc66..f3bdb0a3 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -139,7 +139,7 @@ are stored in the VS Code project under the folder  `certora/confs`. Once the job is completed, a link to the job's conf file can also be found in the files section of the run report. -### Complete Example +### Complete example The command line: ``` From b326d354fac5b64ebfb51d434fd454a7f51fa455 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:18:24 +0200 Subject: [PATCH 50/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index f3bdb0a3..b84522c9 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -141,7 +141,7 @@ run report. ### Complete example -The command line: +The command line ``` certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol \ --verify A:SolcArgs/Trigger.spec \ From 8797697da4cb85b95ab367d68cdfce026449bbd2 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:18:32 +0200 Subject: [PATCH 51/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index b84522c9..b309eb00 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -142,7 +142,7 @@ run report. ### Complete example The command line -``` +```sh certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol \ --verify A:SolcArgs/Trigger.spec \ --solc_map SolcArgs/A.sol=solc6.1,B=solc6.1,C=solc5.12 \ From 37b8ebe7c20a8267806809cba03ec65badebcac7 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:18:40 +0200 Subject: [PATCH 52/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index b309eb00..7582a387 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -152,7 +152,7 @@ certoraRun SolcArgs/A.sol SolcArgs/A.sol:B SolcArgs/C.sol \ ``` will generate the conf file below: -``` +```json { "files": [ "SolcArgs/A.sol", From 06eac96df700d7369ea629eb3f8473f21b3a9e67 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:18:59 +0200 Subject: [PATCH 53/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 7582a387..87248b36 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -53,7 +53,7 @@ Since the default value of boolean options is `false` there is no need to set a ``` would be encoded as: - ``` + ```json { "send_only": true } ``` From 286a0b1afa2074316cd26a59fd940c626adda00c Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:19:06 +0200 Subject: [PATCH 54/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 87248b36..baa49751 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -59,7 +59,7 @@ Since the default value of boolean options is `false` there is no need to set a * Options that expect a single argument (for example {ref}`--solc` or {ref}`--loop_iter`) are encoded as a JSON string. For example, - ``` + ```sh certoraRun --solc solc4.25 --loop_iter 2 ``` would be encoded as: From 45c3d9ea0ceb5663917bf334add9a45ae8824899 Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:19:13 +0200 Subject: [PATCH 55/61] Update docs/prover/cli/conf-file-api.md Co-authored-by: Michael D. George --- docs/prover/cli/conf-file-api.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index baa49751..044e0253 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -63,7 +63,7 @@ Since the default value of boolean options is `false` there is no need to set a certoraRun --solc solc4.25 --loop_iter 2 ``` would be encoded as: - ``` + ```json { "solc": "solc4.25", "loop_iter": "2" } ``` Note that in conf files numbers are also encoded as strings. From 15b7d340f6a549e3194c0fd12b266757061fa2ee Mon Sep 17 00:00:00 2001 From: Rahav <103361134+rahav-certora@users.noreply.github.com> Date: Wed, 10 Jan 2024 18:19:44 +0200 Subject: [PATCH 56/61] Update docs/prover/cli/options.md Co-authored-by: Michael D. George --- docs/prover/cli/options.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index 1916a673..ae9598d3 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -829,4 +829,4 @@ Using Conf Files For larger projects, the command line for running the Certora Prover can become large and cumbersome. It is therefore recommended to use configuration files instead. These are [JSON5](https://json5.org/) files (with .conf extension) that hold the parameters and options for the Prover. -See more on conf file [here3](./conf-file-api.md) \ No newline at end of file +See {ref}`conf-files` for more information. \ No newline at end of file From 5e56ec2303fd3d9718ad31582a379d5c9c07d723 Mon Sep 17 00:00:00 2001 From: rahav Date: Wed, 10 Jan 2024 18:29:04 +0200 Subject: [PATCH 57/61] Mike's comments --- docs/prover/cli/options.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index ae9598d3..6098b5c5 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -16,6 +16,13 @@ certoraRun contractFile --verify contractName:specFile A short summary of these options can be seen by invoking `certoraRun --help` +Using Conf Files +---------------- +For larger projects, the command line for running the Certora Prover can become large +and cumbersome. It is therefore recommended to use configuration files instead. +These are [JSON5](https://json5.org/) files (with .conf extension) that hold the parameters and options for the Prover. +See {ref}`conf-files` for more information. + ```{contents} Overview ``` @@ -824,9 +831,3 @@ splits generated here is equal to `2^n` where `n` is the initial splitting depth (unless the program has less than `n` branchings, which will be rare in practice). -Using Conf Files ----------------- -For larger projects, the command line for running the Certora Prover can become large -and cumbersome. It is therefore recommended to use configuration files instead. -These are [JSON5](https://json5.org/) files (with .conf extension) that hold the parameters and options for the Prover. -See {ref}`conf-files` for more information. \ No newline at end of file From 7d58aaeda11ac7d928276dee06fddc94fa594284 Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 11 Jan 2024 08:36:11 +0200 Subject: [PATCH 58/61] fix --- docs/prover/cli/conf-file-api.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 044e0253..87610227 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -74,9 +74,8 @@ are encoded as JSON lists. For example, ```sh certoraRun --packages @balancer-labs/v2-solidity-utils=pkg/solidity-utils \ @balancer-labs/v2-vault=pkg/vault - ```json would be encoded as: - ``` + ```json { "packages": [ "@balancer-labs/v2-solidity-utils=pkg/solidity-utils", From f53c9aac617412b19dfe8216c567f7bf66817195 Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 11 Jan 2024 08:38:11 +0200 Subject: [PATCH 59/61] fix --- docs/prover/cli/conf-file-api.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 87610227..6d5986a0 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -90,8 +90,8 @@ are encoded as JSON lists. For example, certoraRun --solc_map A=solc5.11,B=solc5.9,C=solc6.8 ``` would be encoded as: - ```json - + +```json { "solc_map": { "A": "solc5.11", @@ -99,8 +99,7 @@ are encoded as JSON lists. For example, "C": "solc6.8" } } - - ``` +``` and ```sh From 6185a926ac2abe6fb9d5f02c55f95cf23a38c54e Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 11 Jan 2024 08:39:24 +0200 Subject: [PATCH 60/61] fix --- docs/prover/cli/conf-file-api.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 6d5986a0..89d9d67d 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -107,7 +107,7 @@ are encoded as JSON lists. For example, ``` would be encoded as: - ```json +```json { "solc_optimize_map": { "A": "200", @@ -115,8 +115,7 @@ are encoded as JSON lists. For example, "C": "300" } } - - ``` +``` ## Generating a conf file After each successful run of `certoraRun` a conf file is generated and is From a5bc9ff26d92eeeb54cd01b222a47dd0ac377b82 Mon Sep 17 00:00:00 2001 From: rahav Date: Thu, 11 Jan 2024 08:51:20 +0200 Subject: [PATCH 61/61] fix --- docs/prover/cli/conf-file-api.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/prover/cli/conf-file-api.md b/docs/prover/cli/conf-file-api.md index 89d9d67d..46d92d4b 100644 --- a/docs/prover/cli/conf-file-api.md +++ b/docs/prover/cli/conf-file-api.md @@ -1,3 +1,4 @@ +(conf-files)= Conf Files ==========