{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | The claim a block's Leios certificate makes, and whether the certificate
-- establishes it.
module Ouroboros.Consensus.Leios.Cert
  ( LeiosClaim (..)
  , LeiosCertRejection (..)
  , leiosClaim
  , verifyLeiosClaim
  ) where

import Cardano.Crypto.Leios (LeiosCert, VerificationError, verifyLeiosCert)
import Cardano.Ledger.BaseTypes (unboundRational)
import Control.Monad.Except (Except, throwError, withExcept)
import Control.Monad.Trans.Except (except)
import Data.Functor (void)
import Data.Maybe.Strict (StrictMaybe (..))
import NoThunks.Class (InspectHeapNamed (..), NoThunks)
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.Leios.Protocol (LeiosLedgerView (..))
import Ouroboros.Consensus.Leios.Types (RankingBlockHash, toRankingBlockHash)

-- | What a block containing a certificate claims: that the endorser block its
-- predecessor announced is certified. The predecessor's hash identifies the
-- claim.
data LeiosClaim = LeiosClaim
  { LeiosClaim -> SlotNo
leiosClaimSlot :: !SlotNo
  -- ^ The predecessor's slot
  , LeiosClaim -> RankingBlockHash
leiosClaimRbHash :: !RankingBlockHash
  -- ^ The predecessor's hash
  }
  deriving stock (LeiosClaim -> LeiosClaim -> Bool
(LeiosClaim -> LeiosClaim -> Bool)
-> (LeiosClaim -> LeiosClaim -> Bool) -> Eq LeiosClaim
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LeiosClaim -> LeiosClaim -> Bool
== :: LeiosClaim -> LeiosClaim -> Bool
$c/= :: LeiosClaim -> LeiosClaim -> Bool
/= :: LeiosClaim -> LeiosClaim -> Bool
Eq, Int -> LeiosClaim -> ShowS
[LeiosClaim] -> ShowS
LeiosClaim -> String
(Int -> LeiosClaim -> ShowS)
-> (LeiosClaim -> String)
-> ([LeiosClaim] -> ShowS)
-> Show LeiosClaim
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LeiosClaim -> ShowS
showsPrec :: Int -> LeiosClaim -> ShowS
$cshow :: LeiosClaim -> String
show :: LeiosClaim -> String
$cshowList :: [LeiosClaim] -> ShowS
showList :: [LeiosClaim] -> ShowS
Show)

-- | Why a block's Leios certificate is invalid
data LeiosCertRejection
  = -- | The block's predecessor is genesis, which announces nothing.
    LeiosCertAtGenesis
  | -- | The ledger view at the block's slot has no Leios committee.
    LeiosCertWithoutCommittee
  | LeiosCertInvalid !VerificationError
  deriving stock (LeiosCertRejection -> LeiosCertRejection -> Bool
(LeiosCertRejection -> LeiosCertRejection -> Bool)
-> (LeiosCertRejection -> LeiosCertRejection -> Bool)
-> Eq LeiosCertRejection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LeiosCertRejection -> LeiosCertRejection -> Bool
== :: LeiosCertRejection -> LeiosCertRejection -> Bool
$c/= :: LeiosCertRejection -> LeiosCertRejection -> Bool
/= :: LeiosCertRejection -> LeiosCertRejection -> Bool
Eq, Int -> LeiosCertRejection -> ShowS
[LeiosCertRejection] -> ShowS
LeiosCertRejection -> String
(Int -> LeiosCertRejection -> ShowS)
-> (LeiosCertRejection -> String)
-> ([LeiosCertRejection] -> ShowS)
-> Show LeiosCertRejection
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LeiosCertRejection -> ShowS
showsPrec :: Int -> LeiosCertRejection -> ShowS
$cshow :: LeiosCertRejection -> String
show :: LeiosCertRejection -> String
$cshowList :: [LeiosCertRejection] -> ShowS
showList :: [LeiosCertRejection] -> ShowS
Show)
  deriving Context -> LeiosCertRejection -> IO (Maybe ThunkInfo)
Proxy LeiosCertRejection -> String
(Context -> LeiosCertRejection -> IO (Maybe ThunkInfo))
-> (Context -> LeiosCertRejection -> IO (Maybe ThunkInfo))
-> (Proxy LeiosCertRejection -> String)
-> NoThunks LeiosCertRejection
forall a.
(Context -> a -> IO (Maybe ThunkInfo))
-> (Context -> a -> IO (Maybe ThunkInfo))
-> (Proxy a -> String)
-> NoThunks a
$cnoThunks :: Context -> LeiosCertRejection -> IO (Maybe ThunkInfo)
noThunks :: Context -> LeiosCertRejection -> IO (Maybe ThunkInfo)
$cwNoThunks :: Context -> LeiosCertRejection -> IO (Maybe ThunkInfo)
wNoThunks :: Context -> LeiosCertRejection -> IO (Maybe ThunkInfo)
$cshowTypeOf :: Proxy LeiosCertRejection -> String
showTypeOf :: Proxy LeiosCertRejection -> String
NoThunks via InspectHeapNamed "LeiosCertRejection" LeiosCertRejection

-- | The claim of a block containing a certificate, given the block's
-- predecessor's hash and slot.
leiosClaim ::
  forall blk.
  ConvertRawHash blk =>
  ChainHash blk ->
  WithOrigin SlotNo ->
  Except LeiosCertRejection LeiosClaim
leiosClaim :: forall blk.
ConvertRawHash blk =>
ChainHash blk
-> WithOrigin SlotNo -> Except LeiosCertRejection LeiosClaim
leiosClaim ChainHash blk
prevHash WithOrigin SlotNo
predecessorSlot = case (ChainHash blk
prevHash, WithOrigin SlotNo
predecessorSlot) of
  (BlockHash HeaderHash blk
h, NotOrigin SlotNo
slot) ->
    LeiosClaim -> Except LeiosCertRejection LeiosClaim
forall a. a -> ExceptT LeiosCertRejection Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LeiosClaim -> Except LeiosCertRejection LeiosClaim)
-> LeiosClaim -> Except LeiosCertRejection LeiosClaim
forall a b. (a -> b) -> a -> b
$ SlotNo -> RankingBlockHash -> LeiosClaim
LeiosClaim SlotNo
slot (Proxy blk -> HeaderHash blk -> RankingBlockHash
forall blk.
ConvertRawHash blk =>
Proxy blk -> HeaderHash blk -> RankingBlockHash
toRankingBlockHash (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @blk) HeaderHash blk
h)
  (ChainHash blk
GenesisHash, WithOrigin SlotNo
Origin) -> LeiosCertRejection -> Except LeiosCertRejection LeiosClaim
forall a.
LeiosCertRejection -> ExceptT LeiosCertRejection Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError LeiosCertRejection
LeiosCertAtGenesis
  -- The envelope check rules out these two, since a block's predecessor is
  -- genesis exactly when its slot is 'Origin'. Rejecting them as at genesis is
  -- harmless even so.
  (ChainHash blk
GenesisHash, NotOrigin SlotNo
_) -> LeiosCertRejection -> Except LeiosCertRejection LeiosClaim
forall a.
LeiosCertRejection -> ExceptT LeiosCertRejection Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError LeiosCertRejection
LeiosCertAtGenesis
  (BlockHash HeaderHash blk
_, WithOrigin SlotNo
Origin) -> LeiosCertRejection -> Except LeiosCertRejection LeiosClaim
forall a.
LeiosCertRejection -> ExceptT LeiosCertRejection Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError LeiosCertRejection
LeiosCertAtGenesis

-- | Verify that the certificate establishes the claim
--
-- The certificate must be signed by a quorum of the committee that was seated
-- when the predecessor announced the endorser block. The given view, however,
-- is the Leios part of the ledger view at the certifying block's slot, not at
-- the predecessor's slot. It nonetheless seats the right committee, because the
-- committee is fixed for a whole epoch and because a header that certifies an
-- announcement from an earlier epoch is invalid: so the certifying block and
-- its predecessor are in the same epoch, and therefore have the same committee.
--
-- If the view is 'SNothing', then the certifying block's era has no Leios, and
-- so the certificate is invalid.
verifyLeiosClaim ::
  StrictMaybe LeiosLedgerView ->
  LeiosCert ->
  LeiosClaim ->
  Except LeiosCertRejection ()
verifyLeiosClaim :: StrictMaybe LeiosLedgerView
-> LeiosCert -> LeiosClaim -> Except LeiosCertRejection ()
verifyLeiosClaim StrictMaybe LeiosLedgerView
mbView LeiosCert
cert LeiosClaim
claim = case StrictMaybe LeiosLedgerView
mbView of
  StrictMaybe LeiosLedgerView
SNothing -> LeiosCertRejection -> Except LeiosCertRejection ()
forall a.
LeiosCertRejection -> ExceptT LeiosCertRejection Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError LeiosCertRejection
LeiosCertWithoutCommittee
  SJust LeiosLedgerView
llv ->
    ExceptT LeiosCertRejection Identity Weight
-> Except LeiosCertRejection ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ExceptT LeiosCertRejection Identity Weight
 -> Except LeiosCertRejection ())
-> ExceptT LeiosCertRejection Identity Weight
-> Except LeiosCertRejection ()
forall a b. (a -> b) -> a -> b
$
      (VerificationError -> LeiosCertRejection)
-> Except VerificationError Weight
-> ExceptT LeiosCertRejection Identity Weight
forall e e' a. (e -> e') -> Except e a -> Except e' a
withExcept VerificationError -> LeiosCertRejection
LeiosCertInvalid (Except VerificationError Weight
 -> ExceptT LeiosCertRejection Identity Weight)
-> Except VerificationError Weight
-> ExceptT LeiosCertRejection Identity Weight
forall a b. (a -> b) -> a -> b
$
        Either VerificationError Weight -> Except VerificationError Weight
forall (m :: * -> *) e a. Monad m => Either e a -> ExceptT e m a
except (Either VerificationError Weight
 -> Except VerificationError Weight)
-> Either VerificationError Weight
-> Except VerificationError Weight
forall a b. (a -> b) -> a -> b
$
          LeiosCommittee
-> Weight
-> RankingBlockHash
-> LeiosCert
-> Either VerificationError Weight
forall msg.
SignableRepresentation msg =>
LeiosCommittee
-> Weight -> msg -> LeiosCert -> Either VerificationError Weight
verifyLeiosCert
            (LeiosLedgerView -> LeiosCommittee
llvCommittee LeiosLedgerView
llv)
            (UnitInterval -> Weight
forall r. BoundedRational r => r -> Weight
unboundRational (LeiosLedgerView -> UnitInterval
llvQuorumStakeThreshold LeiosLedgerView
llv))
            (LeiosClaim -> RankingBlockHash
leiosClaimRbHash LeiosClaim
claim)
            LeiosCert
cert