From c02712b9d314421e344e79783cb9b86890afdf83 Mon Sep 17 00:00:00 2001
From: Alexander Esgen <alexander.esgen@iohk.io>
Date: Wed, 20 Nov 2024 15:02:58 +0100
Subject: [PATCH] ChainDB q-s-m: make `loeHasImmutableAnchor` an invariant

instead of a precondition, which doesn't really make sense as it doesn't depend
on the command
---
 .../Ouroboros/Storage/ChainDB/StateMachine.hs | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs
index b0bd2dc63c..eed9f661ea 100644
--- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs
+++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs
@@ -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.
@@ -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
 
@@ -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]
@@ -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