Soundness property with concurrent actions (#236)

* Added extendable-votes property to block-tree * Using with-abstraction in `mapMaybe` * Properties for `insertCert`
input-output-hk · Oct 10, 2024 · c999a60 · c999a60
1 parent 15dcc08
commit c999a60
Show file tree

Hide file tree

Showing 11 changed files with 574 additions and 606 deletions.
diff --git a/peras-simulation/src/Peras/Chain.hs b/peras-simulation/src/Peras/Chain.hs
@@ -8,8 +8,9 @@
 
 module Peras.Chain where
 
+import Data.Maybe (mapMaybe)
 import Numeric.Natural (Natural)
-import Peras.Block (Block (slotNumber), Certificate, PartyId)
+import Peras.Block (Block (certificate, slotNumber), Certificate, PartyId)
 import Peras.Crypto (Hash, MembershipProof, Signature)
 import Peras.Numbering (RoundNumber, SlotNumber (MkSlotNumber))
 
@@ -36,6 +37,9 @@ instance Eq Vote where
 
 type Chain = [Block]
 
+certsFromChain :: Chain -> [Certificate]
+certsFromChain = mapMaybe (\r -> certificate r)
+
 insertCert :: Certificate -> [Certificate] -> [Certificate]
 insertCert cert [] = [cert]
 insertCert cert (cert' : certs) =

diff --git a/peras-simulation/src/Peras/Conformance/Model.hs b/peras-simulation/src/Peras/Conformance/Model.hs
@@ -14,12 +14,12 @@ module Peras.Conformance.Model where
 import Control.Monad (guard)
 import Numeric.Natural (Natural)
 import Peras.Block (Block (MkBlock, bodyHash, certificate, creatorId, leadershipProof, parentBlock, signature, slotNumber), Certificate (MkCertificate, blockRef, round), PartyId, tipHash)
-import Peras.Chain (Chain, Vote (MkVote, blockHash, votingRound), insertCert, lastSlot)
+import Peras.Chain (Chain, Vote (MkVote, blockHash, votingRound), certsFromChain, insertCert, lastSlot)
 import Peras.Conformance.Params (PerasParams (MkPerasParams, perasA, perasB, perasK, perasL, perasR, perasU, perasτ), defaultPerasParams)
 import Peras.Crypto (Hash (MkHash), Hashable (hash), emptyBS)
 import Peras.Foreign (checkLeadershipProof, checkSignedBlock, checkSignedVote, createLeadershipProof, createMembershipProof, createSignedBlock, createSignedVote, mkParty)
 import Peras.Numbering (RoundNumber (getRoundNumber), SlotNumber (getSlotNumber), nextRound, nextSlot, slotInRound, slotToRound)
-import Peras.Util (comparing, decP, decS, eqDec, ge, gt, isYes, mapMaybe, maximumBy, maybeToList)
+import Peras.Util (comparing, decP, decS, eqDec, ge, gt, isYes, maximumBy, maybeToList)
 
 import Control.Monad.Identity
 import Data.Function (on)
@@ -142,7 +142,7 @@ certS s =
   maximumBy
     genesisCert
     (comparing (\r -> round r))
-    (mapMaybe (\r -> certificate r) (pref s))
+    (certsFromChain (pref s))
 
 testParams :: PerasParams
 testParams =
@@ -190,11 +190,7 @@ addChain' s c =
     (protocol s)
     (c : allChains s)
     (allVotes s)
-    ( foldr
-        insertCert
-        (allSeenCerts s)
-        (mapMaybe (\r -> certificate r) c)
-    )
+    (foldr insertCert (allSeenCerts s) (certsFromChain c))
 
 newQuora :: Natural -> [Certificate] -> [Vote] -> [Certificate]
 newQuora _ _ [] = []
@@ -366,6 +362,20 @@ votesInState sutIsVoter = maybeToList . voteInState sutIsVoter
 
 type SutIsSlotLeader = SlotNumber -> Bool
 
+needCert' :: NodeModel -> Bool
+needCert' s =
+  not
+    ( any
+        ( \c ->
+            getRoundNumber (round c) + 2
+              == getRoundNumber (slotToRound (protocol s) (clock s))
+        )
+        (allSeenCerts s)
+    )
+    && getRoundNumber (slotToRound (protocol s) (clock s))
+      <= perasA (protocol s) + getRoundNumber (round (cert' s))
+    && getRoundNumber (round (certS s)) < getRoundNumber (round (cert' s))
+
 chainInState :: SutIsSlotLeader -> NodeModel -> Maybe Chain
 chainInState sutIsSlotLeader s =
   do
@@ -378,54 +388,28 @@ chainInState sutIsSlotLeader s =
     guard (checkLeadershipProof (leadershipProof block))
     guard (lastSlot rest < slotNumber block)
     guard (bodyHash block == hash [])
+    guard
+      ( certificate block == Just (cert' s) && needCert' s
+          || certificate block == Nothing && not (needCert' s)
+      )
     pure (block : rest)
  where
   rest :: Chain
   rest = pref s
-  notPenultimateCert :: Certificate -> Bool
-  notPenultimateCert cert =
-    getRoundNumber (round cert) + 2 /= getRoundNumber (rFromSlot s)
-  noPenultimateCert :: Bool
-  noPenultimateCert = all notPenultimateCert (allSeenCerts s)
-  unexpiredCert' :: Bool
-  unexpiredCert' =
-    getRoundNumber (round (cert' s)) + perasA (protocol s)
-      >= getRoundNumber (rFromSlot s)
-  newerCert' :: Bool
-  newerCert' =
-    getRoundNumber (round (cert' s))
-      > getRoundNumber (round (certS s))
-  includeCert' :: Bool
-  includeCert' = noPenultimateCert && unexpiredCert' && newerCert'
   block :: Block
   block =
     createSignedBlock
       (mkParty sutId [] [])
       (clock s)
       (tipHash rest)
-      (if includeCert' then Just (cert' s) else Nothing)
+      (if needCert' s then Just (cert' s) else Nothing)
       (createLeadershipProof (clock s) [mkParty sutId [] []])
       (MkHash emptyBS)
 
 chainsInState :: SutIsSlotLeader -> NodeModel -> [Chain]
 chainsInState sutIsSlotLeader =
   maybeToList . chainInState sutIsSlotLeader
 
-needCert' :: NodeModel -> Bool
-needCert' s =
-  not
-    ( any
-        ( \c ->
-            getRoundNumber (round c) + 2
-              == getRoundNumber (slotToRound (protocol s) (clock s))
-        )
-        (allSeenCerts s)
-    )
-    && getRoundNumber (slotToRound (protocol s) (clock s))
-      <= perasA (protocol s) + getRoundNumber (round (cert' s))
-    && getRoundNumber (round (certS s))
-      <= getRoundNumber (round (cert' s))
-
 transition ::
   (SutIsSlotLeader, SutIsVoter) ->
   NodeModel ->
@@ -513,173 +497,33 @@ transition (sutIsSlotLeader, sutIsVoter) s Tick =
         )
     )
 transition _ _ (NewChain []) = Nothing
-transition
-  _
-  s
-  ( NewChain
-      ( MkBlock
-          slotNumber
-          creatorId
-          parentBlock
-          Nothing
-          leadershipProof
-          signature
-          bodyHash
-          : rest
-        )
-    ) =
-    do
-      guard (not $ needCert' s)
-      guard (slotNumber == clock s)
-      guard
-        ( checkBlockFromOther
-            ( MkBlock
-                slotNumber
-                creatorId
-                parentBlock
-                Nothing
-                leadershipProof
-                signature
-                bodyHash
-            )
-        )
-      guard (parentBlock == tipHash rest)
-      guard (rest == pref s)
-      guard
-        ( checkSignedBlock
-            ( MkBlock
-                slotNumber
-                creatorId
-                parentBlock
-                Nothing
-                leadershipProof
-                signature
-                bodyHash
-            )
-        )
-      guard (checkLeadershipProof leadershipProof)
-      guard (lastSlot rest < slotNumber)
-      guard (bodyHash == hash [])
-      Just
-        ( ([], [])
-        , NodeModel
-            (clock s)
-            (protocol s)
-            ( ( MkBlock
-                  slotNumber
-                  creatorId
-                  parentBlock
-                  Nothing
-                  leadershipProof
-                  signature
-                  bodyHash
-                  : rest
-              )
-                : allChains s
-            )
-            (allVotes s)
-            ( foldr
-                insertCert
-                (allSeenCerts s)
-                ( mapMaybe
-                    (\r -> certificate r)
-                    ( MkBlock
-                        slotNumber
-                        creatorId
-                        parentBlock
-                        Nothing
-                        leadershipProof
-                        signature
-                        bodyHash
-                        : rest
-                    )
-                )
-            )
-        )
-transition
-  _
-  s
-  ( NewChain
-      ( MkBlock
-          slotNumber
-          creatorId
-          parentBlock
-          (Just cert)
-          leadershipProof
-          signature
-          bodyHash
-          : rest
-        )
-    ) =
-    do
-      guard (needCert' s)
-      guard (cert == cert' s)
-      guard (slotNumber == clock s)
-      guard
-        ( checkBlockFromOther
-            ( MkBlock
-                slotNumber
-                creatorId
-                parentBlock
-                (Just cert)
-                leadershipProof
-                signature
-                bodyHash
-            )
-        )
-      guard (parentBlock == tipHash rest)
-      guard (rest == pref s)
-      guard
-        ( checkSignedBlock
-            ( MkBlock
-                slotNumber
-                creatorId
-                parentBlock
-                (Just cert)
-                leadershipProof
-                signature
-                bodyHash
-            )
-        )
-      guard (checkLeadershipProof leadershipProof)
-      guard (lastSlot rest < slotNumber)
-      guard (bodyHash == hash [])
-      Just
-        ( ([], [])
-        , NodeModel
-            (clock s)
-            (protocol s)
-            ( ( MkBlock
-                  slotNumber
-                  creatorId
-                  parentBlock
-                  (Just cert)
-                  leadershipProof
-                  signature
-                  bodyHash
-                  : rest
-              )
-                : allChains s
-            )
-            (allVotes s)
-            ( foldr
-                insertCert
-                (allSeenCerts s)
-                ( mapMaybe
-                    (\r -> certificate r)
-                    ( MkBlock
-                        slotNumber
-                        creatorId
-                        parentBlock
-                        (Just cert)
-                        leadershipProof
-                        signature
-                        bodyHash
-                        : rest
-                    )
-                )
-            )
-        )
+transition _ s (NewChain (block : rest)) =
+  do
+    guard
+      ( certificate block == Just (cert' s) && needCert' s
+          || certificate block == Nothing && not (needCert' s)
+      )
+    guard (slotNumber block == clock s)
+    guard (checkBlockFromOther block)
+    guard (parentBlock block == tipHash rest)
+    guard (rest == pref s)
+    guard (checkSignedBlock block)
+    guard (checkLeadershipProof (leadershipProof block))
+    guard (lastSlot rest < slotNumber block)
+    guard (bodyHash block == hash [])
+    Just
+      ( ([], [])
+      , NodeModel
+          (clock s)
+          (protocol s)
+          ((block : rest) : allChains s)
+          (allVotes s)
+          ( foldr
+              insertCert
+              (allSeenCerts s)
+              (certsFromChain (block : rest))
+          )
+      )
 transition _ s (NewVote v) =
   do
     guard (slotInRound (protocol s) (clock s) == 0)

diff --git a/peras-simulation/src/Peras/Util.hs b/peras-simulation/src/Peras/Util.hs
@@ -29,13 +29,6 @@ maximumBy candidate f (x : xs) =
 comparing :: Ord b => (a -> b) -> a -> a -> Ordering
 comparing f x y = compare (f x) (f y)
 
-mapMaybe :: (a -> Maybe b) -> [a] -> [b]
-mapMaybe p [] = []
-mapMaybe p (x : xs) =
-  case p x of
-    Just y -> y : mapMaybe p xs
-    Nothing -> mapMaybe p xs
-
 isYes :: Bool -> Bool
 isYes True = True
 isYes False = False

diff --git a/rewrites.yaml b/rewrites.yaml
@@ -2,3 +2,6 @@ rewrites:
   - from: "Peras.Crypto.ByteString"
     to: "ByteString"
     importing: "Data.ByteString"
+  - from: "Peras.Util.mapMaybe"
+    to: "mapMaybe"
+    importing: "Data.Maybe"
diff --git a/src/Peras/Chain.lagda.md b/src/Peras/Chain.lagda.md
@@ -115,6 +115,8 @@ Chain = List Block
 ```agda
 certsFromChain : Chain → List Certificate
 certsFromChain = mapMaybe certificate
+
+{-# COMPILE AGDA2HS certsFromChain #-}
 ```
 ```agda
 insertCert : Certificate → List Certificate → List Certificate