{-# 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.Ledger.Tables.Utils (forgetLedgerTables)
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) mk ->
    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 mk ->
    Forecast (LedgerView (BlockProtocol blk))

-- | Relation between 'ledgerViewForecastAt' and 'applyChainTick'
_lemma_ledgerViewForecastAt_applyChainTick ::
  ( LedgerSupportsProtocol blk
  , Eq (LedgerView (BlockProtocol blk))
  ) =>
  LedgerConfig blk ->
  LedgerState blk mk ->
  Forecast (LedgerView (BlockProtocol blk)) ->
  SlotNo ->
  Either String ()
_lemma_ledgerViewForecastAt_applyChainTick :: forall blk (mk :: MapKind).
(LedgerSupportsProtocol blk,
 Eq (LedgerView (BlockProtocol blk))) =>
LedgerConfig blk
-> LedgerState blk mk
-> Forecast (LedgerView (BlockProtocol blk))
-> SlotNo
-> Either String ()
_lemma_ledgerViewForecastAt_applyChainTick LedgerCfg (LedgerState blk)
cfg LedgerState blk mk
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 mk -> WithOrigin SlotNo
forall blk (mk :: MapKind).
UpdateLedger blk =>
LedgerState blk mk -> WithOrigin SlotNo
ledgerTipSlot LedgerState blk mk
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) DiffMK
-> LedgerView (BlockProtocol blk)
forall blk (mk :: MapKind).
LedgerSupportsProtocol blk =>
LedgerConfig blk
-> Ticked (LedgerState blk) mk -> LedgerView (BlockProtocol blk)
forall (mk :: MapKind).
LedgerCfg (LedgerState blk)
-> Ticked (LedgerState blk) mk -> LedgerView (BlockProtocol blk)
protocolLedgerView LedgerCfg (LedgerState blk)
cfg
            (Ticked (LedgerState blk) DiffMK -> LedgerView (BlockProtocol blk))
-> (LedgerState blk mk -> Ticked (LedgerState blk) DiffMK)
-> LedgerState blk mk
-> LedgerView (BlockProtocol blk)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputeLedgerEvents
-> LedgerCfg (LedgerState blk)
-> SlotNo
-> LedgerState blk EmptyMK
-> Ticked (LedgerState blk) DiffMK
forall (l :: LedgerStateKind).
IsLedger l =>
ComputeLedgerEvents
-> LedgerCfg l -> SlotNo -> l EmptyMK -> Ticked l DiffMK
applyChainTick ComputeLedgerEvents
OmitLedgerEvents LedgerCfg (LedgerState blk)
cfg SlotNo
for
            (LedgerState blk EmptyMK -> Ticked (LedgerState blk) DiffMK)
-> (LedgerState blk mk -> LedgerState blk EmptyMK)
-> LedgerState blk mk
-> Ticked (LedgerState blk) DiffMK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState blk mk -> LedgerState blk EmptyMK
forall (l :: LedgerStateKind) (mk :: MapKind).
HasLedgerTables l =>
l mk -> l EmptyMK
forgetLedgerTables
            (LedgerState blk mk -> LedgerView (BlockProtocol blk))
-> LedgerState blk mk -> LedgerView (BlockProtocol blk)
forall a b. (a -> b) -> a -> b
$ LedgerState blk mk
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 ()