More refined precondition on PerasCertDB StateModel tests

Co-authored-by: Agustin Mista <agustin.mista@moduscreate.com>
Co-authored-by: Alexander Esgen <alexander.esgen@iohk.io>
Co-authored-by: Georgy Lukyanov <georgy.lukyanov@iohk.io>
Co-authored-by: Thomas BAGREL <thomas.bagrel@tweag.io>
Co-authored-by: Nicolas BACQUEY <nicolas.bacquey@tweag.io>
Co-authored-by: Nicolas "Niols" Jeannerod <nicolas.jeannerod@moduscreate.com>

Author: 6 people

ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/PerasCertDB/StateMachine.hs

@@ -113,7 +113,18 @@ instance StateModel Model where
 
   precondition (Model model) = \case
     OpenDB -> not model.open
-    _ -> model.open
+    action ->
+      model.open && case action of
+        CloseDB -> True
+        -- Equivocating certificates are not possible by construction,
+        -- so we should ensure that adding a certificate with the same round
+        -- number but different content is rejected.
+        -- See https://tweag.github.io/cardano-peras/peras-design.pdf#subsection.2.2.2
+        AddCert cert -> all p model.certs
+         where
+          p cert' = getPerasCertRound cert /= getPerasCertRound cert' || cert == cert'
+        GetWeightSnapshot -> True
+        GarbageCollect _slot -> True
 
 deriving stock instance Show (Action Model a)
 deriving stock instance Eq (Action Model a)