Precompute fold-based operators

[thpani]

With the current specification, Apalache goes out-of-memory even if Java heap size is increased to 20GiB.

This PR precomputes expensive fold-based operators in variables, s.t. they are only emitted once.

Three strategies for constructing the precomputes were implemented and benchmarked (a fourth – not benchmarked – can be found in https://github.com/freespek/ssf-mc/commit/494851ecdc802938313f6b56934cd3191f2770c2).

```tla \* The following variables encode precomputed sets, to avoid emitting nested folds Precompute_Naive == LET all_blocks == get_all_blocks(single_node_state) IN /\ PRECOMPUTED__IS_COMPLETE_CHAIN = { block \in all_blocks : is_complete_chain(block, single_node_state) } /\ PRECOMPUTED__IS_ANCESTOR_DESCENDANT_RELATIONSHIP = [ descendant \in all_blocks |-> { ancestor \in all_blocks : is_ancestor_descendant_relationship(ancestor, descendant, single_node_state) } ] Precompute_Fixpoint == LET all_blocks == get_all_blocks(single_node_state) IN /\ PRECOMPUTED__IS_COMPLETE_CHAIN = LET \* Update single-step completeness \* @type: (Set($block), Int) => Set($block); UpdateCompletenessFromParent(aggregate, i) == { block \in all_blocks : block \in aggregate \/ (has_parent(block, single_node_state) /\ get_parent(block, single_node_state) \in aggregate) } IN ApaFoldSeqLeft( UpdateCompletenessFromParent, { GenesisBlock }, MkSeq(MAX_SLOT, (* @type: Int => Int; *) LAMBDA i: i) ) /\ PRECOMPUTED__IS_ANCESTOR_DESCENDANT_RELATIONSHIP = LET \* Add single-step ancestors to the aggregate \* @type: ($block -> Set($block), Int) => $block -> Set($block); AddAncestorsOfParents(aggregate, i) == [ block \in all_blocks |-> IF has_parent(block, single_node_state) THEN aggregate[block] \union aggregate[get_parent(block, single_node_state)] ELSE aggregate[block] ] IN ApaFoldSeqLeft( AddAncestorsOfParents, [ block \in all_blocks |-> { block } ], MkSeq(MAX_SLOT, (* @type: Int => Int; *) LAMBDA i: i) ) Precompute_Horizon == LET all_blocks == get_all_blocks(single_node_state) IN /\ PRECOMPUTED__IS_COMPLETE_CHAIN = LET \* @type: (<>, Int) => <>; HorizonWithDescendants(horizon_and_aggregate, i) == LET horizon == horizon_and_aggregate[1] aggregate == horizon_and_aggregate[2] one_step_descendants == { block \in all_blocks : has_parent(block, single_node_state) /\ get_parent(block, single_node_state) \in horizon } IN << one_step_descendants, aggregate \union one_step_descendants >> IN ApaFoldSeqLeft( HorizonWithDescendants, << { GenesisBlock }, { GenesisBlock } >>, MkSeq(MAX_SLOT, (* @type: Int => Int; *) LAMBDA i: i) )[2] /\ PRECOMPUTED__IS_ANCESTOR_DESCENDANT_RELATIONSHIP = LET \* @type: (< Set($block)>>, Int) => < Set($block)>>; HorizonWithDescendants(horizon_and_aggregate, i) == LET horizon == horizon_and_aggregate[1] aggregate == horizon_and_aggregate[2] one_step_descendants == { block \in all_blocks : get_parent(block, single_node_state) \in horizon } new_aggregate == [ block \in DOMAIN aggregate \union one_step_descendants |-> IF block \in one_step_descendants /\ has_parent(block, single_node_state) THEN { block } \union aggregate[get_parent(block, single_node_state)] ELSE aggregate[block] ] IN << one_step_descendants, new_aggregate >> roots == { block \in all_blocks : ~has_parent(block, single_node_state) } IN ApaFoldSeqLeft(HorizonWithDescendants, << roots, [ root \in roots |-> { root } ] >>, MkSeq(MAX_SLOT, (* @type: Int => Int; *) LAMBDA i: i)) [2] ```

I benchmarked the strategies on a falsy invariants (producing finalizing votes for a checkpoint) and two different block views (a linear chain, and a single fork at genesis). All benchmark runs were fastest for Precompute_Native:

``` Benchmark 1: apalache-mc check --length=0 --discard-disabled --init=Init_SingleChain_Precompute_Naive --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla Time (mean ± σ): 24.683 s ± 1.116 s [User: 43.012 s, System: 1.274 s] Range (min … max): 23.462 s … 25.650 s 3 runs Warning: Ignoring non-zero exit code. Benchmark 2: apalache-mc check --length=0 --discard-disabled --init=Init_SingleChain_Precompute_Fixpoint --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla Time (mean ± σ): 41.849 s ± 3.202 s [User: 61.733 s, System: 1.326 s] Range (min … max): 39.981 s … 45.546 s 3 runs Warning: Ignoring non-zero exit code. Warning: Statistical outliers were detected. Consider re-running this benchmark on a quiet PC without any interferences from other programs. It might help to use the '--warmup' or '--prepare' options. Benchmark 3: apalache-mc check --length=0 --discard-disabled --init=Init_SingleChain_Precompute_Horizon --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla Time (mean ± σ): 150.777 s ± 21.313 s [User: 178.281 s, System: 1.859 s] Range (min … max): 135.268 s … 175.080 s 3 runs Warning: Ignoring non-zero exit code. Summary 'apalache-mc check --length=0 --discard-disabled --init=Init_SingleChain_Precompute_Naive --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla' ran 1.70 ± 0.15 times faster than 'apalache-mc check --length=0 --discard-disabled --init=Init_SingleChain_Precompute_Fixpoint --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla' 6.11 ± 0.91 times faster than 'apalache-mc check --length=0 --discard-disabled --init=Init_SingleChain_Precompute_Horizon --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla' Benchmark 1: apalache-mc check --length=0 --discard-disabled --init=Init_Forest_Precompute_Naive --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla Time (mean ± σ): 46.743 s ± 2.176 s [User: 76.008 s, System: 2.148 s] Range (min … max): 45.418 s … 49.254 s 3 runs Warning: Ignoring non-zero exit code. Warning: Statistical outliers were detected. Consider re-running this benchmark on a quiet PC without any interferences from other programs. It might help to use the '--warmup' or '--prepare' options. Benchmark 2: apalache-mc check --length=0 --discard-disabled --init=Init_Forest_Precompute_Fixpoint --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla Time (mean ± σ): 75.415 s ± 9.134 s [User: 116.256 s, System: 2.541 s] Range (min … max): 68.793 s … 85.835 s 3 runs Warning: Ignoring non-zero exit code. Benchmark 3: apalache-mc check --length=0 --discard-disabled --init=Init_Forest_Precompute_Horizon --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla Time (mean ± σ): 526.378 s ± 120.217 s [User: 577.057 s, System: 2.898 s] Range (min … max): 414.723 s … 653.633 s 3 runs Warning: Ignoring non-zero exit code. Summary 'apalache-mc check --length=0 --discard-disabled --init=Init_Forest_Precompute_Naive --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla' ran 1.61 ± 0.21 times faster than 'apalache-mc check --length=0 --discard-disabled --init=Init_Forest_Precompute_Fixpoint --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla' 11.26 ± 2.62 times faster than 'apalache-mc check --length=0 --discard-disabled --init=Init_Forest_Precompute_Horizon --inv=FinalizedCheckpoint_Example MC_ffg_examples.tla' ```

[thpani]

Lgtm, just one question about the benchmarks, was Warning: Ignoring non-zero exit code. because of the simplifier stack overflow in Apalache, or something else?

no, this is still for the Python-translated spec. non-zero because it's producing a counter-example – then Apalache's exit code is 12.