{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Ouroboros.Consensus.Ledger.SupportsProtocol (
    GenesisWindow (..)
  , LedgerSupportsProtocol (..)
  ) where

import           Control.Monad.Except
import           GHC.Stack (HasCallStack)
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.Forecast
import           Ouroboros.Consensus.HeaderValidation
import           Ouroboros.Consensus.Ledger.Abstract
import           Ouroboros.Consensus.Protocol.Abstract

-- | Link protocol to ledger
class ( BlockSupportsProtocol blk
      , UpdateLedger          blk
      , ValidateEnvelope      blk
      ) => LedgerSupportsProtocol blk where
  -- | Extract the ledger view from the given ticked ledger state
  --
  -- See 'ledgerViewForecastAt' for a discussion and precise definition of the
  -- relation between this and forecasting.
  protocolLedgerView :: LedgerConfig blk
                     -> Ticked (LedgerState blk)
                     -> LedgerView (BlockProtocol blk)

  -- | Get a forecast at the given ledger state.
  --
  -- This forecast can be used to validate headers of blocks within the range of
  -- the forecast. These blocks need to live on a chain that fits on the last
  -- applied block of the given ledger.
  --
  -- The range of the forecast should allow to validate a sufficient number of
  -- headers to validate an alternative chain longer than ours, so that chain
  -- selection can decide whether or not we prefer the alternative chain to our
  -- current chain. In addition, it would be helpful, though not essential, if
  -- we can look further ahead than that, as this would improve sync
  -- performance.
  --
  -- NOTE (difference between 'ledgerViewForecastAt' and 'applyChainTick'):
  -- Both 'ledgerViewForecastAt' and 'applyChainTick' can be used to obtain
  -- a protocol ledger view for a future slot. The difference between the two
  -- is that 'applyChainTick' assumes no blocks are present between the current
  -- ledger tip and the specified 'SlotNo', whereas 'ledgerViewForecastAt'
  -- cannot make such an assumption. Thus, 'applyChainTick' cannot fail, whereas
  -- the forecast returned by 'ledgerViewForecastAt' might report an
  -- 'OutsideForecastRange' for the same 'SlotNo'. We expect the two functions
  -- to produce the same view whenever the 'SlotNo' /is/ in range, however.
  -- More precisely:
  --
  -- If
  --
  -- >    forecastFor (ledgerViewForecastAt cfg st) for
  -- > == Just view
  --
  -- then
  --
  -- >    protocolLedgerView cfg (applyChainTick cfg for st)
  -- > == view
  --
  -- See 'lemma_ledgerViewForecastAt_applyChainTick'.
  ledgerViewForecastAt ::
       HasCallStack
    => LedgerConfig blk
    -> LedgerState blk
    -> Forecast (LedgerView (BlockProtocol blk))

-- | Relation between 'ledgerViewForecastAt' and 'applyChainTick'
_lemma_ledgerViewForecastAt_applyChainTick
  :: ( LedgerSupportsProtocol blk
     , Eq (LedgerView (BlockProtocol blk))
     )
  => LedgerConfig blk
  -> LedgerState blk
  -> Forecast (LedgerView (BlockProtocol blk))
  -> SlotNo
  -> Either String ()
_lemma_ledgerViewForecastAt_applyChainTick :: forall blk.
(LedgerSupportsProtocol blk,
 Eq (LedgerView (BlockProtocol blk))) =>
LedgerConfig blk
-> LedgerState blk
-> Forecast (LedgerView (BlockProtocol blk))
-> SlotNo
-> Either String ()
_lemma_ledgerViewForecastAt_applyChainTick LedgerCfg (LedgerState blk)
cfg LedgerState blk
st Forecast (LedgerView (BlockProtocol blk))
forecast SlotNo
for
    | SlotNo -> WithOrigin SlotNo
forall t. t -> WithOrigin t
NotOrigin SlotNo
for WithOrigin SlotNo -> WithOrigin SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= LedgerState blk -> WithOrigin SlotNo
forall blk.
UpdateLedger blk =>
LedgerState blk -> WithOrigin SlotNo
ledgerTipSlot LedgerState blk
st
    , let lhs :: Except OutsideForecastRange (LedgerView (BlockProtocol blk))
lhs = Forecast (LedgerView (BlockProtocol blk))
-> SlotNo
-> Except OutsideForecastRange (LedgerView (BlockProtocol blk))
forall a. Forecast a -> SlotNo -> Except OutsideForecastRange a
forecastFor Forecast (LedgerView (BlockProtocol blk))
forecast SlotNo
for
          rhs :: LedgerView (BlockProtocol blk)
rhs = LedgerCfg (LedgerState blk)
-> Ticked (LedgerState blk) -> LedgerView (BlockProtocol blk)
forall blk.
LedgerSupportsProtocol blk =>
LedgerConfig blk
-> Ticked (LedgerState blk) -> LedgerView (BlockProtocol blk)
protocolLedgerView LedgerCfg (LedgerState blk)
cfg
              (Ticked (LedgerState blk) -> LedgerView (BlockProtocol blk))
-> (LedgerState blk -> Ticked (LedgerState blk))
-> LedgerState blk
-> LedgerView (BlockProtocol blk)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerCfg (LedgerState blk)
-> SlotNo -> LedgerState blk -> Ticked (LedgerState blk)
forall l. IsLedger l => LedgerCfg l -> SlotNo -> l -> Ticked l
applyChainTick LedgerCfg (LedgerState blk)
cfg SlotNo
for
              (LedgerState blk -> LedgerView (BlockProtocol blk))
-> LedgerState blk -> LedgerView (BlockProtocol blk)
forall a b. (a -> b) -> a -> b
$ LedgerState blk
st
    , Right LedgerView (BlockProtocol blk)
lhs' <- Except OutsideForecastRange (LedgerView (BlockProtocol blk))
-> Either OutsideForecastRange (LedgerView (BlockProtocol blk))
forall e a. Except e a -> Either e a
runExcept Except OutsideForecastRange (LedgerView (BlockProtocol blk))
lhs
    , LedgerView (BlockProtocol blk)
lhs' LedgerView (BlockProtocol blk)
-> LedgerView (BlockProtocol blk) -> Bool
forall a. Eq a => a -> a -> Bool
/= LedgerView (BlockProtocol blk)
rhs
    = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"ledgerViewForecastAt /= protocolLedgerView . applyChainTick:"
      , LedgerView (BlockProtocol blk) -> String
forall a. Show a => a -> String
show LedgerView (BlockProtocol blk)
lhs'
      , String
" /= "
      , LedgerView (BlockProtocol blk) -> String
forall a. Show a => a -> String
show LedgerView (BlockProtocol blk)
rhs
      ]
    | Bool
otherwise
    = () -> Either String ()
forall a b. b -> Either a b
Right ()