{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}

-- | The node's LeiosNotify codec, at the Cardano block, against the CDDL.
module Test.Consensus.Cardano.LeiosNotify (tests) where

import Cardano.Crypto.DSIGN.Class (genKeyDSIGN, signDSIGN)
import Cardano.Crypto.Leios (LeiosSeatId (..), leiosSignContext)
import Cardano.Crypto.Seed (mkSeedFromBytes)
import Codec.CBOR.Read (DeserialiseFailure)
import qualified Data.ByteString as BS
import Data.ByteString.Lazy (ByteString, toStrict)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Proxy (Proxy (..))
import qualified Data.Text as T
import Network.TypedProtocol.Codec (AnyMessage (..), Codec, CodecF (..))
import Ouroboros.Consensus.Block (Header, SlotNo (..))
import Ouroboros.Consensus.Cardano.Block (CardanoBlock, StandardCrypto)
import Ouroboros.Consensus.Cardano.Node ()
import Ouroboros.Consensus.Leios.Types
  ( EbHash (..)
  , LeiosPoint (..)
  , LeiosVote (..)
  , RbHash (..)
  , decodeLeiosPoint
  , decodeLeiosVote
  , encodeLeiosPoint
  , encodeLeiosVote
  )
import Ouroboros.Consensus.MiniProtocol.LeiosNotify.Type
import Ouroboros.Consensus.Node.NetworkProtocolVersion
  ( NodeToNodeVersion (..)
  , SupportedNetworkProtocolVersion (..)
  )
import Ouroboros.Consensus.Node.Serialisation (decodeNodeToNode, encodeNodeToNode)
import qualified Test.Consensus.Cardano.Examples as Cardano.Examples
import Test.Tasty
import Test.Tasty.QuickCheck
import Test.Util.Serialisation.CDDL (cddlTest, isCDDLCDisabled)
import Test.Util.Serialisation.Examples (Examples (..))

type Blk = CardanoBlock StandardCrypto

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"LeiosNotify" ([TestTree] -> TestTree) -> [TestTree] -> TestTree
forall a b. (a -> b) -> a -> b
$
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"the node's codec encodes each message as the CDDL specifies" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$
        Property
prop_nodeCodecMatchesCDDL
    | Bool -> Bool
not Bool
isCDDLCDisabled
    ]

prop_nodeCodecMatchesCDDL :: Property
prop_nodeCodecMatchesCDDL :: Property
prop_nodeCodecMatchesCDDL =
  Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
-> (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
    -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
genMessage ((AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
  -> Property)
 -> Property)
-> (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
    -> Property)
-> Property
forall a b. (a -> b) -> a -> b
$ \(AnyMessage Message (LeiosNotify LeiosPoint (Header Blk) LeiosVote) st st'
msg) ->
    IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$ do
      let codec ::
            Codec (LeiosNotify LeiosPoint (Header Blk) LeiosVote) DeserialiseFailure IO ByteString
          codec :: Codec
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
  DeserialiseFailure
  IO
  ByteString
codec =
            (LeiosPoint -> Encoding)
-> (forall s. Decoder s LeiosPoint)
-> (Header Blk -> Encoding)
-> (forall s. Decoder s (Header Blk))
-> (LeiosVote -> Encoding)
-> (forall s. Decoder s LeiosVote)
-> Codec
     (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
     DeserialiseFailure
     IO
     ByteString
forall point announcement vote (m :: * -> *).
MonadST m =>
(point -> Encoding)
-> (forall s. Decoder s point)
-> (announcement -> Encoding)
-> (forall s. Decoder s announcement)
-> (vote -> Encoding)
-> (forall s. Decoder s vote)
-> Codec
     (LeiosNotify point announcement vote)
     DeserialiseFailure
     m
     ByteString
codecLeiosNotify
              LeiosPoint -> Encoding
encodeLeiosPoint
              Decoder s LeiosPoint
forall s. Decoder s LeiosPoint
decodeLeiosPoint
              (CodecConfig Blk
-> BlockNodeToNodeVersion Blk -> Header Blk -> Encoding
forall blk a.
SerialiseNodeToNode blk a =>
CodecConfig blk -> BlockNodeToNodeVersion blk -> a -> Encoding
encodeNodeToNode CodecConfig Blk
Cardano.Examples.codecConfig BlockNodeToNodeVersion Blk
HardForkNodeToNodeVersion
  (ByronBlock : CardanoShelleyEras StandardCrypto)
leiosVersion)
              (CodecConfig Blk
-> BlockNodeToNodeVersion Blk -> forall s. Decoder s (Header Blk)
forall blk a.
SerialiseNodeToNode blk a =>
CodecConfig blk
-> BlockNodeToNodeVersion blk -> forall s. Decoder s a
decodeNodeToNode CodecConfig Blk
Cardano.Examples.codecConfig BlockNodeToNodeVersion Blk
HardForkNodeToNodeVersion
  (ByronBlock : CardanoShelleyEras StandardCrypto)
leiosVersion)
              LeiosVote -> Encoding
encodeLeiosVote
              Decoder s LeiosVote
forall s. Decoder s LeiosVote
decodeLeiosVote
      result <-
        IO ByteString -> TestName -> Text -> IO (Either TestName ())
cddlTest
          (ByteString -> IO ByteString
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> IO ByteString) -> ByteString -> IO ByteString
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
toStrict (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Codec
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
  DeserialiseFailure
  IO
  ByteString
-> forall (st :: LeiosNotify LeiosPoint (Header Blk) LeiosVote)
          (st' :: LeiosNotify LeiosPoint (Header Blk) LeiosVote).
   (StateTokenI st, ActiveState st) =>
   Message (LeiosNotify LeiosPoint (Header Blk) LeiosVote) st st'
   -> ByteString
forall ps failure (m :: * -> *) (f :: ps -> *) bytes.
CodecF ps failure m f bytes
-> forall (st :: ps) (st' :: ps).
   (StateTokenI st, ActiveState st) =>
   Message ps st st' -> bytes
encode Codec
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
  DeserialiseFailure
  IO
  ByteString
codec Message (LeiosNotify LeiosPoint (Header Blk) LeiosVote) st st'
msg)
          TestName
"ntnleiosnotify.cddl"
          (TestName -> Text
T.pack TestName
"leiosNotifyMessage")
      pure $ either (`counterexample` False) (const $ property True) result
 where
  genMessage :: Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
  genMessage :: Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
genMessage =
    [Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))]
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a. HasCallStack => [Gen a] -> Gen a
oneof
      [ AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
 -> Gen
      (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)))
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a b. (a -> b) -> a -> b
$ Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StQuit 'StDone
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StQuit 'StDone
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StQuit 'StDone
MsgDone
      , AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
 -> Gen
      (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)))
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a b. (a -> b) -> a -> b
$ Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StIdle 'StQuit
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StIdle 'StQuit
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StIdle 'StQuit
MsgQuit
      , AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
 -> Gen
      (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)))
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a b. (a -> b) -> a -> b
$ Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
MsgCanceled
      , AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
 -> Gen
      (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)))
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a b. (a -> b) -> a -> b
$ Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StIdle 'StBusy
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StIdle 'StBusy
forall point announcement vote.
Message (LeiosNotify point announcement vote) 'StIdle 'StBusy
MsgLeiosNotificationRequestNext
      , -- The golden tests check these headers against the CDDL.
        --
        -- TODO Generate the headers instead, Dijkstra's among them, once
        -- TODO(dijkstra_serialisation) is resolved and the Shelley header
        -- generators choose a major protocol version the era admits, as the
        -- ledger's @genEraProtVer@ does.
        Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage (Message
   (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
 -> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
-> (Header Blk
    -> Message
         (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
-> Header Blk
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header Blk
-> Message
     (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
forall announcement point vote.
announcement
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
MsgLeiosBlockAnnouncement
          (Header Blk
 -> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
-> Gen (Header Blk)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Header Blk] -> Gen (Header Blk)
forall a. HasCallStack => [a] -> Gen a
elements (((Maybe TestName, Header Blk) -> Header Blk)
-> [(Maybe TestName, Header Blk)] -> [Header Blk]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe TestName, Header Blk) -> Header Blk
forall a b. (a, b) -> b
snd (Examples Blk -> [(Maybe TestName, Header Blk)]
forall blk. Examples blk -> Labelled (Header blk)
exampleHeader Examples Blk
Cardano.Examples.examples))
      , (Message
   (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
 -> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
-> Gen
     (Message
        (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage (Gen
   (Message
      (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
 -> Gen
      (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)))
-> Gen
     (Message
        (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall a b. (a -> b) -> a -> b
$ LeiosPoint
-> Word32
-> Message
     (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
forall point announcement vote.
point
-> Word32
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
MsgLeiosBlockOffer (LeiosPoint
 -> Word32
 -> Message
      (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
-> Gen LeiosPoint
-> Gen
     (Word32
      -> Message
           (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen LeiosPoint
genPoint Gen
  (Word32
   -> Message
        (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
-> Gen Word32
-> Gen
     (Message
        (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Word32
forall a. Arbitrary a => Gen a
arbitrary
      , Message
  (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall ps (st :: ps) (st' :: ps).
(StateTokenI st, ActiveState st) =>
Message ps st st' -> AnyMessage ps
AnyMessage (Message
   (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
 -> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
-> (LeiosPoint
    -> Message
         (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle)
-> LeiosPoint
-> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeiosPoint
-> Message
     (LeiosNotify LeiosPoint (Header Blk) LeiosVote) 'StBusy 'StIdle
forall point announcement vote.
point
-> Message (LeiosNotify point announcement vote) 'StBusy 'StIdle
MsgLeiosBlockTxsOffer (LeiosPoint
 -> AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
-> Gen LeiosPoint
-> Gen (AnyMessage (LeiosNotify LeiosPoint (Header Blk) LeiosVote))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen LeiosPoint
genPoint
      , do
          n <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
maxLeiosVotesPerMessage)
          AnyMessage . MsgLeiosVotes . NE.fromList <$> vectorOf n genVote
      ]

  -- LeiosNotify runs only from 'NodeToNodeV_16' on.
  leiosVersion :: HardForkNodeToNodeVersion
  (ByronBlock : CardanoShelleyEras StandardCrypto)
leiosVersion = Proxy Blk -> Map NodeToNodeVersion (BlockNodeToNodeVersion Blk)
forall blk.
SupportedNetworkProtocolVersion blk =>
Proxy blk -> Map NodeToNodeVersion (BlockNodeToNodeVersion blk)
supportedNodeToNodeVersions (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Blk) Map
  NodeToNodeVersion
  (HardForkNodeToNodeVersion
     (ByronBlock : CardanoShelleyEras StandardCrypto))
-> NodeToNodeVersion
-> HardForkNodeToNodeVersion
     (ByronBlock : CardanoShelleyEras StandardCrypto)
forall k a. Ord k => Map k a -> k -> a
Map.! NodeToNodeVersion
NodeToNodeV_16

  genPoint :: Gen LeiosPoint
genPoint = SlotNo -> EbHash -> LeiosPoint
MkLeiosPoint (SlotNo -> EbHash -> LeiosPoint)
-> Gen SlotNo -> Gen (EbHash -> LeiosPoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word64
forall a. Arbitrary a => Gen a
arbitrary) Gen (EbHash -> LeiosPoint) -> Gen EbHash -> Gen LeiosPoint
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ByteString -> EbHash
MkEbHash (ByteString -> EbHash) -> Gen ByteString -> Gen EbHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen ByteString
genHash)

  -- The codec does not check a vote's signature, so any key will do.
  genVote :: Gen LeiosVote
genVote = do
    rbHash <- ByteString -> RbHash
MkRbHash (ByteString -> RbHash) -> Gen ByteString -> Gen RbHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen ByteString
genHash
    seat <- LeiosSeatId <$> arbitrary
    pure $
      MkLeiosVote rbHash seat $
        signDSIGN leiosSignContext rbHash (genKeyDSIGN (mkSeedFromBytes (BS.replicate 32 0)))

  genHash :: Gen ByteString
genHash = [Word8] -> ByteString
BS.pack ([Word8] -> ByteString) -> Gen [Word8] -> Gen ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen Word8 -> Gen [Word8]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
32 Gen Word8
forall a. Arbitrary a => Gen a
arbitrary