On 2/13/24 10:14 AM, Eduard Zingerman wrote:
Updated diagram with a few fixes, line numbers would be removed in the
final version.
--- 8< ---------------------------------
.------------------------------------- Checkpoint / State name
| .-------------------------------- Code point number
| | .---------------------------- Stack state {ctx.a,ctx.b,ctx.c}
| | | .------------------- Callback depth in frame #0
v v v v
1 - (0) {7P,7P,7},depth=0
2 - (3) {7P,7P,7},depth=1
3 - (0) {7P,7P,42},depth=1
(a) - (3) {7P,7,42},depth=2
4 - (0) {7P,7,42},depth=2 loop terminates because of depth limit
5 - (4) {7P,7,42},depth=0 predicted false, ctx.a marked precise
6 - (6) exit
7 - (2) {7P,7,42},depth=2
8 - (0) {7P,42,42},depth=2 loop terminates because of depth limit
9 - (4) {7P,42,42},depth=0 predicted false, ctx.a marked precise
10 - (6) exit
(b) - (1) {7P,7P,42},depth=2
11 - (0) {42P,7P,42},depth=2 loop terminates because of depth limit
12 - (4) {42P,7P,42},depth=0 predicted false, ctx.{a,b} marked precise
13 - (6) exit
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
For the above line
(c) - (1) {7P,7P,7},depth=1 considered safe, pruned using checkpoint (b)
I would change to
(c) - (1) {7P,7P,7},depth=1
- (0) {42P, 7P, 7},depth = 1 considered safe, pruned using checkpoint (11)
For
14 - (2) {7P,7,7},depth=1
15 - (0) {7P,42,7},depth=1 considered safe, pruned using checkpoint (a)
I suspect for line 15, the pruning uses checking point at line (8).
Other than the above, the diagram LGTM.
Here checkpoint (b) has callback_depth of 2, meaning that it would
never reach state {42,42,7}.
While checkpoint (c) has callback_depth of 1, and thus
could yet explore the state {42,42,7} if not pruned prematurely.
This commit makes forbids such premature pruning,
allowing verifier to explore states sub-tree starting at (c):
(c) - (1) {7,7,7P},depth=1
16 - (0) {42P,7,7P},depth=1
...
17 - (2) {42,7,7},depth=2
18 - (0) {42,42,7},depth=2 loop terminates because of depth limit
19 - (4) {42,42,7},depth=0 predicted true, ctx.{a,b,c} marked precise
20 - (5) division by zero
--------------------------------- >8 ---
