[DOC-351] Document control flow splitting #164

alexandernutz · 2023-10-27T13:43:11Z

Add a conceptual explanation for the (control flow) splitting feature. This understanding is helpful for mitigating timeouts using the corresponding collection of cli options.

Jira ticket: https://certora.atlassian.net/browse/DOC-351
Link to generated documentation: https://certora-certora-prover-documentation--164.com.readthedocs.build/en/164/docs/prover/techniques/index.html#control-flow-splitting

otakar-trunda

I left two minor comments, otherwise it looks good.

docs/prover/cli/options.md

mdgeorge4153

Looking good! There's a bit much low-level detail, but I think that's unavoidable for this information, and I think it is well scoped. I have some editorial comments.

docs/prover/techniques/index.md

mdgeorge4153 · 2023-12-12T22:03:26Z

docs/prover/techniques/index.md

+splittings along a fixed sequence of split points up to the maximum splitting
+depth. We call the splits at maximum splitting depth *split leafs*. The
+exploration stops in either of the following three cases:
+ - if one split was found that is SAT (reasoning: if one split is SAT, then the


I think SAT and UNSAT require some mental gymnastics. I think something like "if a counterexample is found for any split, then the process stops" would be clearer.

the problem is that it's not always a counterexample, sometimes it's a "witness example" ...
-- so I chose SAT because it's the more "stable" concept here ...
I made a glossary entry explaining the background there.

Not needing the mental gymnastics is of course better 🤔

I can try how it looks with "counterexample", and on first mention, or in a footnote, mention witness examples and SAT/UNSAT, pointing to the glossary ...

hm, after revisiting this again, I feel like for this very technical section, SAT and UNSAT might be best, since they're just the most concise thing to put e.g. into the pseudo code ...
-- there is a glossary entry for them, which also relates them to the concepts of counterexample and witness example.

I'll also add a sentence to the top of this section mentioning this relationship
-- let me know if you think this won't do ...

mdgeorge4153 · 2023-12-12T22:05:14Z

docs/prover/techniques/index.md

+Splitting is best illustrated using the {term}`control flow graph` (CFG) of a given
+CVL rule.
+
+A single splitting step proceeds as follows:


I think there is a high-level idea that might get lost in the details. Essentially whenever we find a branch (e.g. an if statement or loop guard), we sometimes look for counterexamples in each branch separately. We could also include a small example, something like:

For example, consider a rule with an `if` statement: ```cvl rule example { ... if (owner == spender) { assert balance_after == balance_before; } else { assert balance_after == balance_before + amount; } } ``` To simplify the search for a counterexample, the Prover may internally split this single rule into two rules: ```cvl rule example_split_1 { ... require owner == spender; assert balance_after == balance_before; } rule example_split_2 { ... require owner != spender; assert balance_after == balance_before + amount; } ``` A counterexample for either of the split rules will also be a counterexample for the original rule, and any counterexample for the original rule must violate one of the two split rules, so this splitting doesn't change the meaning of the rule. However, in some cases the split rule is easier for the Prover to reason about.

Right, making this into an intro section -- should be nice!

mdgeorge4153 · 2023-12-12T22:15:12Z

docs/prover/techniques/index.md


 (storage-and-memory-analysis)=
-# Storage and Memory Analysis
+# Storage and Memory analysis

 The Certora Prover works on EVM bytecode as its input. To the bytecode, the
 address space of both Storage and Memory are flat number lines. That two


I don't think Storage and Memory should be capitalized.

The idea of capitalizing was to indicate that I'm referring to the terms as defined by EVM, not to the general concepts (in which case I wouldn't be sure what the difference between the two even is exactly) ...

Maybe I make them glossary references instead of capitalizing (first occurrence at least .. make new glossary entries, too, if necessary)?..
I'll try that for now, open to comments.

I'll use the terms "EVM storage" and "EVM memory" instead of the capitalized Storage and Memory ..

mdgeorge4153 · 2023-12-12T22:24:07Z

docs/prover/cli/options.md

+the other hand, if something will be split further anyway, this can save the
+run time spent on intermediate "TIMEOUT" results. Use
+{ref}`-smt_initialSplitDepth` to eliminate that time investment altogether up to
+a given depth.


This probably doesn't belong right here (but maybe in the main page on splitting), but this reminds me: Is there a way to know how much time was spent on different splits to help with this kind of tuning?

It is on my list for things to implement in the new "Live Stats" tab. -- once we have that, we should document it here.

mdgeorge4153 · 2023-12-12T22:25:15Z

docs/prover/cli/options.md

+
+
+
+% The regular SMT timeout determines how much time is maximally spent on checking


not sure why this is commented out

removed and added an extra sentence to the description of -mediumTimeout right above

mdgeorge4153 · 2023-12-12T22:25:46Z

docs/prover/cli/options.md

-is enough that one split is UNSAT.
+**What does it do?**
+
+We can tell the Certora Prover to continue even when the first split has had a


as above, split should be a glossary link here.

right, so I'm linking every first occurrence under each option ... (or other "entry point")

mdgeorge4153 · 2023-12-12T22:26:38Z

docs/prover/cli/options.md

+**What does it do?**
+
+We can tell the Certora Prover to continue even when the first split has had a
+maximum-depth timeout. Note that this is only useful for {term}`SAT result`s,


As above, I think SAT / UNSAT is almost always more confusing for users than something like "finds a counterexample" / "successfully proves".

yeah, rewrote for counterexample / witness example ... clunky as well, but perhaps clearer ..

mdgeorge4153 · 2023-12-12T22:29:46Z

docs/prover/cli/options.md

@@ -793,29 +793,117 @@ Advanced options that control control flow splitting

 See [here](control-flow-splitting) for an explanation of control flow splitting.


I would shorten "Advanced options that control control flow splitting" to "Control flow splitting options". It also looks like the header levels are inconsistent; take a look at the generated table of contents at the top of the page.

header: right, much better ...

hm, the toc looks okay-ish to me (maybe something changed in the meantime ..) -- "Control flow splitting options" is on one level with the other groups ("Options that control the soldiity compiler", "Advanced Options", etc .. though whether Advanced options is a great category might be subject for discussion ..)

shellygr

Great! nits

shellygr · 2024-01-20T22:15:53Z

docs/prover/cli/options.md

@@ -949,7 +953,7 @@ This option disables the storage splitting optimization.


 (--allow_solidity_calls_in_quantifiers)=
-### --allow_solidity_calls_in_quantifiers
+### `--allow_solidity_calls_in_quantifiers`


an aside - if you're faster than me... can you fix to --prover_args instead of --settings in line 938 --settings -smt_groundQuantifiers=false? just noticed it's out of date...

hm, the accent seems to be on master already; changed --settings (in separate branch, PR upcoming ..)

shellygr · 2024-01-20T22:16:34Z

docs/prover/cli/options.md

+**When to use it?** 
+
+When the deepest {term}`split`s are too heavy to solve, but not too high in
+number, increasing this will lead to smaller, but more {term}`split leaves`, which run


Suggested change

number, increasing this will lead to smaller, but more {term}`split leaves`, which run

number, increasing this will lead to smaller, but more numerous {term}`split leaves`, which run

rright 💯

shellygr · 2024-01-20T22:17:40Z

docs/prover/cli/options.md

+number, increasing this will lead to smaller, but more {term}`split leaves`, which run
+at the full SMT timeout (as set by {ref}`--smt_timeout`). Conversely, if run
+time is too high because there are too many splits, decreasing this number means
+that more time is spent on fewer, but bigger split leaves.


do we have a tip on when to increase or decrease?

should we state the current default (10)?

re 1: well .. this is supposed to be it ... but it's rather abstract, I admit .. I'll give it another shot
re 2: sure (increased maintenance effort / failure potential is a con, but I guess I'll add it and see how it goes ..)

hm, actually, I'm still not sure what to write, as changing this should really be a reaction to where CVT is spending its time ... which currently can only be observed in statsdata.json ...
however, there are plans to condense this info to a live stat -- so I propose to update this when introducing these stats.

shellygr · 2024-01-20T22:18:56Z

docs/prover/cli/options.md

+
+**Example**
+
+```sh


again, maybe mention default

alexandernutz · 2024-01-26T21:33:24Z

ugh, I guess I landed this rashly, will make an extra PR for your nits, Shelly

alexandernutz added 7 commits October 25, 2023 15:44

switching ..

4964cdd

steps

a0dc06a

splitting algo description

0a9ed1f

Merge branch 'alex/timeouts-update' into alex/control-flow-splitting

d46efb3

spelling

c2d6ad6

optical and didactic tweaks

f430aad

minor

f5aa4d3

alexandernutz mentioned this pull request Nov 3, 2023

[DOC-81] Update "Managing Timeouts" Section #159

Merged

Merge branch 'alex/timeouts-update' into alex/control-flow-splitting

64c6e30

alexandernutz added the existing feature new documentation for an existing feature label Nov 7, 2023

fill some gaps, polish

d693572

Base automatically changed from alex/timeouts-update to master November 21, 2023 13:35

alexandernutz added 2 commits November 21, 2023 16:31

Merge remote-tracking branch 'origin' into alex/control-flow-splitting

484ea1a

incremental improvements

15d791a

alexandernutz requested review from shoham-certora and mdgeorge4153 November 21, 2023 16:04

alexandernutz assigned shoham-certora Nov 21, 2023

alexandernutz marked this pull request as ready for review November 21, 2023 16:05

alexandernutz requested a review from a team as a code owner November 21, 2023 16:05

alexandernutz changed the title ~~Alex/control flow splitting~~ Document control flow splitting Nov 23, 2023

alexandernutz added 2 commits November 23, 2023 15:39

Merge remote-tracking branch 'origin' into alex/control-flow-splitting

324a910

language/style (david's review)

6cb5ff5

alexandernutz requested a review from otakar-trunda November 27, 2023 15:57

alexandernutz assigned otakar-trunda Nov 27, 2023

Merge remote-tracking branch 'origin' into alex/control-flow-splitting

e8c2432

otakar-trunda approved these changes Dec 11, 2023

View reviewed changes

docs/prover/cli/options.md Outdated Show resolved Hide resolved

docs/prover/cli/options.md Show resolved Hide resolved

fix things according to review

2796479

alexandernutz requested a review from nd-certora December 12, 2023 12:55

mdgeorge4153 changed the title ~~Document control flow splitting~~ [DOC-351] Document control flow splitting Dec 12, 2023

mdgeorge4153 suggested changes Dec 12, 2023

View reviewed changes

alexandernutz added 2 commits January 12, 2024 16:24

steps

d8dc81c

finish this review iteration

952272f

alexandernutz requested review from mdgeorge4153 and shellygr and removed request for mdgeorge4153 January 12, 2024 17:02

alexandernutz added 2 commits January 18, 2024 16:11

Merge remote-tracking branch 'origin' into alex/control-flow-splitting

56cf76f

Merge remote-tracking branch 'origin' into alex/control-flow-splitting

92578e6

alexandernutz requested a review from otakar-trunda January 19, 2024 17:05

shellygr approved these changes Jan 20, 2024

View reviewed changes

Merge branch 'master' into alex/control-flow-splitting

f4a7448

alexandernutz merged commit 3abf130 into master Jan 26, 2024
2 checks passed

alexandernutz deleted the alex/control-flow-splitting branch January 26, 2024 21:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[DOC-351] Document control flow splitting #164

[DOC-351] Document control flow splitting #164

alexandernutz commented Oct 27, 2023 •

edited

Loading

otakar-trunda left a comment

mdgeorge4153 left a comment

mdgeorge4153 Dec 12, 2023

alexandernutz Dec 18, 2023 •

edited

Loading

alexandernutz Jan 12, 2024

mdgeorge4153 Dec 12, 2023

alexandernutz Jan 12, 2024

mdgeorge4153 Dec 12, 2023

alexandernutz Dec 15, 2023

alexandernutz Jan 12, 2024

mdgeorge4153 Dec 12, 2023

alexandernutz Jan 12, 2024

mdgeorge4153 Dec 12, 2023

alexandernutz Jan 12, 2024

mdgeorge4153 Dec 12, 2023

alexandernutz Jan 12, 2024

mdgeorge4153 Dec 12, 2023

alexandernutz Jan 12, 2024

mdgeorge4153 Dec 12, 2023

alexandernutz Jan 12, 2024 •

edited

Loading

shellygr left a comment

shellygr Jan 20, 2024

alexandernutz Jan 26, 2024

shellygr Jan 20, 2024

alexandernutz Jan 26, 2024

shellygr Jan 20, 2024

alexandernutz Jan 26, 2024

alexandernutz Jan 26, 2024

shellygr Jan 20, 2024

alexandernutz commented Jan 26, 2024




		% The regular SMT timeout determines how much time is maximally spent on checking

		@@ -793,29 +793,117 @@ Advanced options that control control flow splitting

		See [here](control-flow-splitting) for an explanation of control flow splitting.

	number, increasing this will lead to smaller, but more {term}`split leaves`, which run
	number, increasing this will lead to smaller, but more numerous {term}`split leaves`, which run


		Example

		```sh

[DOC-351] Document control flow splitting #164

[DOC-351] Document control flow splitting #164

Conversation

alexandernutz commented Oct 27, 2023 • edited Loading

otakar-trunda left a comment

Choose a reason for hiding this comment

mdgeorge4153 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alexandernutz Dec 18, 2023 • edited Loading

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

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

alexandernutz Jan 12, 2024 • edited Loading

Choose a reason for hiding this comment

shellygr 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

alexandernutz commented Jan 26, 2024

alexandernutz commented Oct 27, 2023 •

edited

Loading

alexandernutz Dec 18, 2023 •

edited

Loading

alexandernutz Jan 12, 2024 •

edited

Loading