DOC-433 | Added solana cli options #335

yoav-el-certora · 2025-01-20T09:01:47Z

Naming convention:

PRs for features that are in design should have the "proposal" label
PRs for features that haven't landed yet should have the "future" label
PRs for upcoming releases should have the "release" label
PRs with new documentation for existing features should have the "existing feature" label

Before requesting review:

Make sure there is a ticket in the DOC board in Jira
Make sure CI is passing
- Spell check failure may require adding backticks around code or updating spelling_wordlist.txt
- See README.md for information about style and markdown syntax
- If the CI Details link gives a 404, you need to log in to readthedocs.com
Add link to generated documentation here
- you can find this by following the read the docs link from the CI check
Ask for help in #documentation

Jira ticket: https://certora.atlassian.net/browse/CERT-7992
Link to generated documentation: TODO

johspaeth

Mostly good - minor nits. Thanks.

@phreppo can you please add information about the missing parts where Yoav requested Jorge's support, I believe you should be familiar with the flags that miss explanations?

johspaeth · 2025-01-20T11:17:01Z

docs/solana/options.rst

+The build script must output the following:
+
+- `project_directory`: Path to the project root directory.
+- `sources`: List of files or directories used or imported in the program.


Can this list contain a regular expression? Or does the user need to list all files explicitly?

Suggested change

- `sources`: List of files or directories used or imported in the program.

- `sources`: List of source files or directories used or imported in the program. All files declared in this list will be uploaded as sources to cloud and displayed in the rule report. Source files are required, for instance, for the jump to source feature to work.

johspaeth · 2025-01-20T11:19:25Z

docs/solana/options.rst

+Modes of Operation
+------------------
+
+The Certora Solana Prover has two modes of operation. These modes are mutually exclusive - you cannot run the tool with more than one mode at a time.


What are the two modes of operations here?

Are you referring to --build_script and precompiled binary here? That's not clear to me - state them explicitly?

johspaeth · 2025-01-20T11:20:49Z

docs/solana/options.rst

+
+These files are in [JSON5](https://json5.org/) format and use a `.conf` extension. They hold the parameters and options for the Prover.
+
+For more details, see `Conf File <https://docs.certora.com/en/latest/docs/prover/cli/conf-file-api.html#conf-files>`_


Suggested change

For more details, see `Conf File <https://docs.certora.com/en/latest/docs/prover/cli/conf-file-api.html#conf-files>`_

For more details, see `Conf File <https://docs.certora.com/en/latest/docs/prover/cli/conf-file-api.html#conf-files>`.

johspaeth · 2025-01-20T11:23:46Z

docs/solana/options.rst

+This option saves a lot of run time. Use it whenever you care about only a
+specific subset of a specification's properties. The most common case is when
+This option saves runtime and is useful for verifying specific subsets of a specification. Common cases include testing new rules or investigating specific failures.
+you add a new rule to an existing specification. The other is when code changes
+cause a specific rule to fail; in the process of fixing the code, updating the
+rule, and understanding counterexamples, you likely want to verify only that
+specific rule.


I think it's sufficient to just write:

Suggested change

This option saves a lot of run time. Use it whenever you care about only a

specific subset of a specification's properties. The most common case is when

This option saves runtime and is useful for verifying specific subsets of a specification. Common cases include testing new rules or investigating specific failures.

you add a new rule to an existing specification. The other is when code changes

cause a specific rule to fail; in the process of fixing the code, updating the

rule, and understanding counterexamples, you likely want to verify only that

specific rule.

This option saves a lot of run time as it only executes a specific rule. This option saves runtime and is useful for verifying specific subsets of a specification. Common cases include testing new rules or investigating specific failures.

johspaeth · 2025-01-20T11:25:15Z

docs/solana/options.rst

+
+**What does it do?**
+
+Adds a description message to your run, similar to a commit message. This message appears in the title of the completion email.


The message is more important in the prover dashboard / rule report. I think we should rather state this here.

Suggested change

Adds a description message to your run, similar to a commit message. This message appears in the title of the completion email.

Adds a description message to your run, similar to a commit message. This message appears on the Prover dashboard and in the rule report.

johspaeth · 2025-01-20T11:25:32Z

docs/solana/options.rst

+
+**When to use it?**
+
+TODO: @Jorge please advise.


@phreppo can you add a few words on the usage of it?

johspaeth · 2025-01-20T11:25:41Z

docs/solana/options.rst

+
+**When to use it?**
+
+TODO: @Jorge please advise.


@phreppo can you add a few words on the usage of it?

johspaeth · 2025-01-20T11:25:52Z

docs/solana/options.rst

+
+**When to use it?**
+
+TODO: @Jorge please advise.


@phreppo are you familiar with this, can you add a few words on the usage of it?

phreppo · 2025-01-20T11:43:22Z

docs/solana/options.rst

+
+**What does it do?**
+
+Runs formal verification of specified properties while providing an automatic method to compile a Rust project.


I might be wrong here, but I thought that the build script is the Python script that builds the project without running the formal verification.
Am I wrong?

phreppo · 2025-01-20T11:53:10Z

docs/solana/options.rst

+**What does it do?**
+
+Provides the prover with a whitespace-separated list of extra features passed to the build script.
+
+**When to use it?**
+
+TODO: @Jorge please advise.


Suggested change

**What does it do?**

Provides the prover with a whitespace-separated list of extra features passed to the build script.

**When to use it?**

TODO: @Jorge please advise.

**What does it do?**

Provides the prover with a whitespace-separated list of extra `Cargo features <https://doc.rust-lang.org/cargo/reference/features.html>` passed to the build script.

These features are then passed to ``cargo`` to build the project.

**When to use it?**

Use it when there is a need to enable a specific `Cargo feature <https://doc.rust-lang.org/cargo/reference/features.html>` to compile the source code.

Added solana cli options

76f8d8a

yoav-el-certora requested review from shoham-certora, johspaeth and rahav-certora January 20, 2025 09:02

johspaeth reviewed Jan 20, 2025

View reviewed changes

phreppo reviewed Jan 20, 2025

View reviewed changes

johspaeth mentioned this pull request Jan 20, 2025

DOC-431: Solana troubleshooting section #336

Open

johspaeth changed the title ~~Added solana cli options~~ DOC-433 | Added solana cli options Jan 20, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

DOC-433 | Added solana cli options #335

DOC-433 | Added solana cli options #335

yoav-el-certora commented Jan 20, 2025

johspaeth left a comment

johspaeth Jan 20, 2025

johspaeth Jan 20, 2025

johspaeth Jan 20, 2025

johspaeth Jan 20, 2025

johspaeth Jan 20, 2025

johspaeth Jan 20, 2025

johspaeth Jan 20, 2025

johspaeth Jan 20, 2025

phreppo Jan 20, 2025

phreppo Jan 20, 2025

	- `sources`: List of files or directories used or imported in the program.
	- `sources`: List of source files or directories used or imported in the program. All files declared in this list will be uploaded as sources to cloud and displayed in the rule report. Source files are required, for instance, for the jump to source feature to work.


		These files are in [JSON5](https://json5.org/) format and use a `.conf` extension. They hold the parameters and options for the Prover.

		For more details, see `Conf File <https://docs.certora.com/en/latest/docs/prover/cli/conf-file-api.html#conf-files>`_


		What does it do?

		Adds a description message to your run, similar to a commit message. This message appears in the title of the completion email.


		What does it do?

		Runs formal verification of specified properties while providing an automatic method to compile a Rust project.

DOC-433 | Added solana cli options #335

Are you sure you want to change the base?

DOC-433 | Added solana cli options #335

Conversation

yoav-el-certora commented Jan 20, 2025

johspaeth left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment