Skip to content

Commit

Permalink
ChainDB q-s-m: make loeHasImmutableAnchor an invariant (#1313)
Browse files Browse the repository at this point in the history
Tiny follow-up to #1308, see the commit description
  • Loading branch information
amesgen authored Nov 21, 2024
2 parents 7aeafae + c02712b commit 244ea9f
Showing 1 changed file with 10 additions and 10 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -1075,7 +1075,6 @@ precondition :: forall m blk. TestConstraints blk
precondition Model {..} (At cmd) =
forAll (iters cmd) (`member` RE.keys knownIters) .&&
forAll (flrs cmd) (`member` RE.keys knownFollowers) .&&
loeHasImmutableAnchor .&&
case cmd of
-- Even though we ensure this in the generator, shrinking might change
-- it.
Expand Down Expand Up @@ -1103,14 +1102,6 @@ precondition Model {..} (At cmd) =
garbageCollectableIteratorNext it = Boolean $
Model.garbageCollectableIteratorNext secParam dbModel (knownIters RE.! it)

loeHasImmutableAnchor :: Logic
loeHasImmutableAnchor = case Model.getLoEFragment dbModel of
LoEEnabled frag ->
Boolean $ Chain.pointOnChain (AF.anchorPoint frag) immChain
LoEDisabled -> Top
where
immChain = Model.immutableChain secParam dbModel

cfg :: TopLevelConfig blk
cfg = unOpaque modelConfig

Expand Down Expand Up @@ -1139,7 +1130,8 @@ invariant ::
-> Model blk m Concrete
-> Logic
invariant cfg Model {..} =
forAll ptsOnCurChain (Boolean . fromMaybe False . Model.getIsValid dbModel)
forAll ptsOnCurChain (Boolean . fromMaybe False . Model.getIsValid dbModel) .&&
loeHasImmutableAnchor
where
-- | The blocks occurring on the current volatile chain fragment
ptsOnCurChain :: [RealPoint blk]
Expand All @@ -1149,6 +1141,14 @@ invariant cfg Model {..} =
. Model.volatileChain (configSecurityParam cfg) id
$ dbModel

loeHasImmutableAnchor :: Logic
loeHasImmutableAnchor = case Model.getLoEFragment dbModel of
LoEEnabled frag ->
Boolean $ Chain.pointOnChain (AF.anchorPoint frag) immChain
LoEDisabled -> Top
where
immChain = Model.immutableChain (configSecurityParam cfg) dbModel

postcondition :: TestConstraints blk
=> Model blk m Concrete
-> At Cmd blk m Concrete
Expand Down

0 comments on commit 244ea9f

Please sign in to comment.