added Ranger repo #395

urikirsh · 2025-05-12T18:56:47Z

Adding documentation for ranger

Link to generated documentation: https://certora-certora-prover-documentation--395.com.readthedocs.build/en/395/docs/ranger/index.html

naftali-g · 2025-05-18T05:59:00Z

docs/ranger/starting_with_ranger.md

+## 3. Run Ranger
+Use the certoraRanger command to launch the job:
+
+```bash
+certoraRanger ranger.conf
+```
+
+This will start the Ranger process. A link to the Ranger Job Report in the dashboard will be pasted into your command line when the job is submitted.


Do we want to mention somewhere that ranger runs lots of processes/is compute intensive and suggest that users use it with --rule in order to test only one rule/invariant, or use --split_rules "*" so each rule will run in a separate job?

I've added a new warning with this info. IDK if it fits a warning or an info message

docs/ranger/ranger_intro.md

naftali-g

looks ok to me

* start * Added CLI docs * Fixing ref * spelling * CR * Update docs/ranger/ranger_client.md Co-authored-by: urikirsh <[email protected]> * Removed "usage" section and commented range_failure_limit attribute until decided otherwise. * fixed attribute typo * How Ranger Works (#398) * how ranger works * Uri's CR --------- Co-authored-by: urikirsh <[email protected]> Co-authored-by: Naftali Goldstein <[email protected]>

johspaeth

I have some tiny request for changes, overall looks good! Thanks guys.

We should state that Ranger operates on CVL early on.
We should document the setup function.

johspaeth · 2025-05-19T07:13:19Z

docs/ranger/ranger_client.md

+
+[//]: <> (&#40;--ranger_failure_limit&#41;=)
+
+[### `ranger_failure_limit`


Suggested change

[### `ranger_failure_limit`

### `ranger_failure_limit`

It is commented on purpose

Ok, it currently just renders strangely on https://certora-certora-prover-documentation--395.com.readthedocs.build/en/395/docs/ranger/ranger_client.html

I see, thanks!
I tried different ways of commenting out lines in markdown, none worked, I've removed the lines entirely

johspaeth · 2025-05-19T07:13:50Z

docs/ranger/how_ranger_works.md

+# How Ranger Works
+
+**Ranger** is a bounded model checker. This means that, in contrast with "full"
+formal verification, its initial state isn't arbitrary, but is instead reached


Suggested change

formal verification, its initial state isn't arbitrary, but is instead reached

formal verification, its initial state is not arbitrary, but is instead reached

johspaeth · 2025-05-19T07:14:39Z

index.rst

 * :doc:`docs/sunbeam/index` -- instructions for installing and using *Certora Sunbeam*
  for formal verification of `Soroban`_ contracts.
 * :doc:`docs/solana/index` -- instructions for installing and using *Certora Solana Prover*
+* :doc:`docs/ranger/index` -- TODO


Suggested change

* :doc:`docs/ranger/index` -- TODO

* :doc:`docs/ranger/index` -- explains how to use Ranger, Certora's Bounded Model Checker.

Good catch!

johspaeth · 2025-05-19T07:17:39Z

docs/ranger/ranger_intro.md

+- ✅ **Realistic counterexamples**: All violations are reachable from the initial state.
+- ✅ **Faster time to value**: Minimal setup required to get useful results.
+- ✅ **Fewer false positives**: No need to precondition rules to filter out invalid states.
+- ✅ **High coverage**: Symbolically tests all function call sequences from the initial state up to a certain range.


I'd rephrase this slightly.

Suggested change

- ✅ **High coverage**: Symbolically tests all function call sequences from the initial state up to a certain range.

- ✅ **High coverage**: Tests all function call sequences on symbolic inputs from the initial state up to a certain range.

johspaeth · 2025-05-19T07:22:41Z

docs/ranger/starting_with_ranger.md

+
+This guide will help you run your first Ranger job using a Solidity contract and a [CVL](/docs/cvl/index) [invariant](/docs/cvl/invariants).
+
+Ranger uses the same installation process, configuration files, and spec files as the [Certora Prover](/docs/user-guide/index). If you're already familiar with the Prover, getting started with Ranger will feel familiar.


That Ranger uses CVL could be stated also ranger_intro?

docs/ranger/how_ranger_works.md

added Ranger repo

fba3aae

urikirsh added the future documentation for features that haven't landed yet label May 12, 2025

urikirsh added 15 commits May 12, 2025 22:03

added an md besides the index page

9bb35c8

added Ranger to top level toc tree

9879092

adding all files under ranger docs

2247e56

forgot to add content

2e139a0

base text for Ranger

bcfcbd2

first round of upgrades

821c409

trying ref and term tags

41a7e8b

improving links

6cd89a5

text improvements on intro

f21b182

fixing link to CVL

4056511

first version of Ranger user guide

669da9b

fixing titles

4af3d41

minor improvements to Ranger getting started

fb12791

shorter title for Ranger index page

dafa026

Merge remote-tracking branch 'origin/master' into uri/add_ranger_docs

28ff991

naftali-g reviewed May 18, 2025

View reviewed changes

urikirsh added 4 commits May 18, 2025 13:21

ranger now also checks rules

1b686eb

Merge remote-tracking branch 'origin/master' into uri/add_ranger_docs

c7a4b6e

added note about using either --rule or --split_rules

03f3c08

{warn} -> {warning}

22e5da9

naftali-g approved these changes May 18, 2025

View reviewed changes

urikirsh marked this pull request as ready for review May 18, 2025 16:49

urikirsh added 5 commits May 18, 2025 19:50

Merge remote-tracking branch 'origin/master' into uri/add_ranger_docs

bdef21d

trying a new markdown comment style

834dcd9

trying a different style of comment

4be35a0

trying one big multi-line comment

d7d4c2a

spelling

eaed893

urikirsh added 3 commits May 18, 2025 20:10

fixing title sizes under ranger_linet.md

c937873

removing code tags from title

48de033

certora-cli instead of certora Python package

860d84e

johspaeth requested changes May 19, 2025

View reviewed changes

urikirsh added 4 commits May 19, 2025 12:18

Johannes' CR part 1

22967ae

isn't -> is not

ab2f870

removing mentions of requuiring invariants

0f5f5b4

removing ranger failure limit

8f4a1ca

johspaeth approved these changes May 20, 2025

View reviewed changes

urikirsh added 4 commits May 27, 2025 13:16

added note for no Ranger support for multi_example to test how it looks

1a388e9

added notes on all flags Ranger doesn't support

5c0cf4b

Merge remote-tracking branch 'origin/master' into uri/add_ranger_docs

8f41e0e

merge from master after v8 changes

b7ff08e


		[//]: <> ((--ranger_failure_limit)=)

		[### `ranger_failure_limit`

	formal verification, its initial state isn't arbitrary, but is instead reached
	formal verification, its initial state is not arbitrary, but is instead reached

	* :doc:`docs/ranger/index` -- TODO
	* :doc:`docs/ranger/index` -- explains how to use Ranger, Certora's Bounded Model Checker.

	- ✅ High coverage: Symbolically tests all function call sequences from the initial state up to a certain range.
	- ✅ High coverage: Tests all function call sequences on symbolic inputs from the initial state up to a certain range.


		This guide will help you run your first Ranger job using a Solidity contract and a [CVL](/docs/cvl/index) [invariant](/docs/cvl/invariants).

		Ranger uses the same installation process, configuration files, and spec files as the [Certora Prover](/docs/user-guide/index). If you're already familiar with the Prover, getting started with Ranger will feel familiar.

added Ranger repo #395

Are you sure you want to change the base?

added Ranger repo #395

Uh oh!

Conversation

urikirsh commented May 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

naftali-g left a comment

Choose a reason for hiding this comment

Uh oh!

johspaeth left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

urikirsh commented May 12, 2025 •

edited

Loading