Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

DOC-308: Documentation for conf file #134

Merged
merged 68 commits into from
Jan 11, 2024
Merged
Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
68 commits
Select commit Hold shift + click to select a range
18b68cc
conf file api
rahav-certora Aug 22, 2023
01f8528
fix content
rahav-certora Aug 22, 2023
0678a26
json5 refernce
rahav-certora Aug 22, 2023
f125ae2
spelling
rahav-certora Aug 22, 2023
87400d1
Chandra's comments
rahav-certora Aug 23, 2023
fcf769f
Chandra's comments
rahav-certora Aug 23, 2023
6452ca4
Chandra's comments
rahav-certora Aug 23, 2023
b5b14ee
Chandra's comments
rahav-certora Aug 23, 2023
10fd1b7
Update docs/prover/cli/conf-file-api.md
rahav-certora Sep 5, 2023
e1de9f5
Update docs/prover/cli/conf-file-api.md
rahav-certora Sep 5, 2023
4c96266
Update docs/prover/cli/conf-file-api.md
rahav-certora Sep 7, 2023
0d227af
Mike's comments
rahav-certora Sep 7, 2023
ddb1e16
Mike's comments
rahav-certora Sep 7, 2023
b1e2f30
Merge branch 'master' into rahav/conf_file_api
mdgeorge4153 Oct 31, 2023
c6a496a
Merge branch 'master' into rahav/conf_file_api
rahav-certora Nov 13, 2023
d4e29b1
Merge branch 'rahav/conf_file_api' of https://github.com/Certora/Docu…
rahav-certora Nov 13, 2023
48179a2
fix
rahav-certora Nov 14, 2023
378125f
fix
rahav-certora Nov 14, 2023
b2c2c5c
fix ref
rahav-certora Nov 16, 2023
8c698c2
fix ref
rahav-certora Nov 16, 2023
ebc0af8
fix ref
rahav-certora Nov 16, 2023
0a661f3
remove redundent text
rahav-certora Nov 16, 2023
228ddac
Merge branch 'master' into rahav/conf_file_api
rahav-certora Dec 13, 2023
6703df4
Update docs/prover/cli/conf-file-api.md
rahav-certora Dec 13, 2023
5deca4a
Update docs/prover/cli/conf-file-api.md
rahav-certora Dec 13, 2023
5a6310f
Update docs/prover/cli/conf-file-api.md
rahav-certora Dec 13, 2023
ce4fcd9
Update docs/prover/cli/conf-file-api.md
rahav-certora Dec 13, 2023
9c9fe3e
Mike's comments
rahav-certora Dec 13, 2023
a16014d
Mike's comments
rahav-certora Dec 13, 2023
64c8cb2
Mike's comments
rahav-certora Dec 13, 2023
35090a6
ref
rahav-certora Dec 13, 2023
b8721a5
test_ref
rahav-certora Dec 13, 2023
a4d1e99
ref
rahav-certora Dec 13, 2023
86624af
clean
rahav-certora Dec 14, 2023
eabbcec
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
7a170f3
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
8acdd86
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
8b38c09
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
055b3dc
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
45bcdf3
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
64fedaa
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
3d91b32
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
eb99063
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
8c7e90d
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
ca6e80c
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
d810aeb
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
e944fda
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
82b0b58
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
ff2bbe9
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
177cf9e
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
21bceee
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
05678f3
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
eacc988
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
f7ac815
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
4fce2ca
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
b326d35
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
8797697
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
37b8ebe
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
06eac96
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
286a0b1
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
45c3d9e
Update docs/prover/cli/conf-file-api.md
rahav-certora Jan 10, 2024
15b7d34
Update docs/prover/cli/options.md
rahav-certora Jan 10, 2024
5e56ec2
Mike's comments
rahav-certora Jan 10, 2024
93aca46
merge
rahav-certora Jan 11, 2024
7d58aae
fix
rahav-certora Jan 11, 2024
f53c9aa
fix
rahav-certora Jan 11, 2024
6185a92
fix
rahav-certora Jan 11, 2024
a5bc9ff
fix
rahav-certora Jan 11, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 102 additions & 0 deletions docs/prover/cli/conf-file-api.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,102 @@
Certora Prover Conf File API
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
============================

rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
The **Conf File API** is an alternative API for  `certoraRun` . In terms of functionality
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
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/)):
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved

```
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
certoraRun my_params.conf
```

Conf files must use the <strong>.conf</strong> suffix
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved


How CLI Options are mapped to JSON
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
----------------------------------

**JSON Keys**
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved

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**

Flags in CLI API that accept a single string will be stored as **JSON Strings**. Example:
```
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
"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:
chandrakananandi marked this conversation as resolved.
Show resolved Hide resolved

```
"smt_timeout": "600"
```

**Boolean Value CLI Options**

Since boolean flags in the CLI API do not get a value they will be stored as **JSON true**. Example:
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved

```
"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**
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be consistent with the other sections above (i.e. bullets).

Also, avoid manual formatting (like **) in favor of section headers (like ###).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done


Flags in CLI API that are maps will be stored as **JSON Objects**. Example:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How do I know whether a flag is a map?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

listed the 2 map flags --solc_map and --solc_optimize_map

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think "Objects" should be lowercase. Also, I wouldn't bold here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

```
"solc_map": {
mdgeorge4153 marked this conversation as resolved.
Show resolved Hide resolved
"A": "solc5.11",
"B": "solc5.9",
"C": "solc6.8"
}
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved

```

A conf file is generated each time `certoraRun` completes execution successfully.
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
The conf file is stored as `**run.conf**` in the build directory under **`.certora_internal`**.
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
<p>Conf file of the latest run can be found in:
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved

```
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
./.certora_internal/latest/run.conf
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
```


**Complete Example**

The command line:
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
```
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would break this into several lines - the generated page is hard to read because you have to scroll.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

done

```

will generate the conf file below:
```
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
{
"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"
}
rahav-certora marked this conversation as resolved.
Show resolved Hide resolved
```
1 change: 1 addition & 0 deletions docs/prover/cli/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,5 +8,6 @@ Certora Prover CLI
verification.md
linking.md
options.md
conf-file-api.md
```