{-# 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 ()