We currently use { i \in 0..MAX_SLOT: i <= node_state.current_slot } to fold over.
However, we don't constrain single_node_state.current_slot in Init, so the additional filter is unsound. We replace it with just 0..MAX_SLOT.
The bounds on get_blockchain and have_common_ancestor can be tightened to 1..MAX_SLOT.
For is_ancestor_descendant_relationship we do the same by pulling the comparison one step out of the fold.
For ffg.tla:
Replace non-constant checkpoint.chkp_slot with MAX_SLOT.
ApaFoldSeqLeft over MkSeq would require a type annotation on the lambda. Replace it with ApaFoldSet over 1..N to emphasize that order of the underlying structure is irrelevant.
Fix and tighten the bounds on folds.
For helpers.tla:
We currently use
{ i \in 0..MAX_SLOT: i <= node_state.current_slot }to fold over. However, we don't constrainsingle_node_state.current_slotinInit, so the additional filter is unsound. We replace it with just0..MAX_SLOT.The bounds on
get_blockchainandhave_common_ancestorcan be tightened to1..MAX_SLOT.For
is_ancestor_descendant_relationshipwe do the same by pulling the comparison one step out of the fold.For ffg.tla:
checkpoint.chkp_slotwithMAX_SLOT.ApaFoldSeqLeftoverMkSeqwould require a type annotation on the lambda. Replace it withApaFoldSetover1..Nto emphasize that order of the underlying structure is irrelevant.