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

module Ouroboros.Consensus.Ledger.SupportsProtocol (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 ticked ledger view from ticked ledger state
  --
  -- See 'ledgerViewForecastAt' for a discussion and precise definition of the
  -- relation between this and forecasting.
  protocolLedgerView :: LedgerConfig blk
                     -> Ticked (LedgerState blk)
                     -> Ticked (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   (Ticked (LedgerView (BlockProtocol blk)))
     , Show (Ticked (LedgerView (BlockProtocol blk)))
     )
  => LedgerConfig blk
  -> LedgerState blk
  -> Forecast (LedgerView (BlockProtocol blk))
  -> SlotNo
  -> Either String ()
_lemma_ledgerViewForecastAt_applyChainTick :: LedgerConfig blk
-> LedgerState blk
-> Forecast (LedgerView (BlockProtocol blk))
-> SlotNo
-> Either String ()
_lemma_ledgerViewForecastAt_applyChainTick LedgerConfig 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 (Ticked (LedgerView (BlockProtocol blk)))
lhs = Forecast (LedgerView (BlockProtocol blk))
-> SlotNo
-> Except
     OutsideForecastRange (Ticked (LedgerView (BlockProtocol blk)))
forall a.
Forecast a -> SlotNo -> Except OutsideForecastRange (Ticked a)
forecastFor Forecast (LedgerView (BlockProtocol blk))
forecast SlotNo
for
          rhs :: Ticked (LedgerView (BlockProtocol blk))
rhs = LedgerConfig blk
-> Ticked (LedgerState blk)
-> Ticked (LedgerView (BlockProtocol blk))
forall blk.
LedgerSupportsProtocol blk =>
LedgerConfig blk
-> Ticked (LedgerState blk)
-> Ticked (LedgerView (BlockProtocol blk))
protocolLedgerView LedgerConfig blk
cfg
              (Ticked (LedgerState blk)
 -> Ticked (LedgerView (BlockProtocol blk)))
-> (LedgerState blk -> Ticked (LedgerState blk))
-> LedgerState blk
-> Ticked (LedgerView (BlockProtocol blk))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerConfig blk
-> SlotNo -> LedgerState blk -> Ticked (LedgerState blk)
forall l. IsLedger l => LedgerCfg l -> SlotNo -> l -> Ticked l
applyChainTick LedgerConfig blk
cfg SlotNo
for
              (LedgerState blk -> Ticked (LedgerView (BlockProtocol blk)))
-> LedgerState blk -> Ticked (LedgerView (BlockProtocol blk))
forall a b. (a -> b) -> a -> b
$ LedgerState blk
st
    , Right Ticked (LedgerView (BlockProtocol blk))
lhs' <- Except
  OutsideForecastRange (Ticked (LedgerView (BlockProtocol blk)))
-> Either
     OutsideForecastRange (Ticked (LedgerView (BlockProtocol blk)))
forall e a. Except e a -> Either e a
runExcept Except
  OutsideForecastRange (Ticked (LedgerView (BlockProtocol blk)))
lhs
    , Ticked (LedgerView (BlockProtocol blk))
lhs' Ticked (LedgerView (BlockProtocol blk))
-> Ticked (LedgerView (BlockProtocol blk)) -> Bool
forall a. Eq a => a -> a -> Bool
/= Ticked (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:"
      , Ticked (LedgerView (BlockProtocol blk)) -> String
forall a. Show a => a -> String
show Ticked (LedgerView (BlockProtocol blk))
lhs'
      , String
" /= "
      , Ticked (LedgerView (BlockProtocol blk)) -> String
forall a. Show a => a -> String
show Ticked (LedgerView (BlockProtocol blk))
rhs
      ]
    | Bool
otherwise
    = () -> Either String ()
forall a b. b -> Either a b
Right ()