diff --git a/ouroboros-consensus-cardano/src/byron/Ouroboros/Consensus/Byron/Ledger/Ledger.hs b/ouroboros-consensus-cardano/src/byron/Ouroboros/Consensus/Byron/Ledger/Ledger.hs index f455db7d44..be233d844e 100644 --- a/ouroboros-consensus-cardano/src/byron/Ouroboros/Consensus/Byron/Ledger/Ledger.hs +++ b/ouroboros-consensus-cardano/src/byron/Ouroboros/Consensus/Byron/Ledger/Ledger.hs @@ -83,6 +83,7 @@ import Ouroboros.Consensus.Ledger.Query import Ouroboros.Consensus.Ledger.SupportsPeerSelection import Ouroboros.Consensus.Ledger.SupportsProtocol import Ouroboros.Consensus.Protocol.PBFT +import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util (ShowProxy (..), (..:)) {------------------------------------------------------------------------------- @@ -164,6 +165,7 @@ getByronTip state = -- | The ticked Byron ledger state data instance Ticked (LedgerState ByronBlock) = TickedByronLedgerState { tickedByronLedgerState :: !CC.ChainValidationState + , untickedByronLedgerTipBlockNo :: !(WithOrigin BlockNo) , untickedByronLedgerTransition :: !ByronTransition } deriving (Generic, NoThunks) @@ -178,6 +180,8 @@ instance IsLedger (LedgerState ByronBlock) where TickedByronLedgerState { tickedByronLedgerState = CC.applyChainTick cfg (toByronSlotNo slotNo) byronLedgerState + , untickedByronLedgerTipBlockNo = + byronLedgerTipBlockNo , untickedByronLedgerTransition = byronLedgerTransition } diff --git a/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/CanHardFork.hs b/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/CanHardFork.hs index 8fb6bf08ec..83ea6b6a76 100644 --- a/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/CanHardFork.hs +++ b/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/CanHardFork.hs @@ -25,7 +25,10 @@ module Ouroboros.Consensus.Cardano.CanHardFork ( -- * Re-exports of Shelley code , ShelleyPartialLedgerConfig (..) , crossEraForecastAcrossShelley - , translateChainDepStateAcrossShelley + , forecastAcrossShelley + , tickChainDepStateAcrossShelley + , tickLedgerStateAcrossShelley + , translateLedgerStateByronToShelley ) where import qualified Cardano.Chain.Common as CC @@ -41,6 +44,7 @@ import Cardano.Ledger.Keys (DSignable, Hash) import qualified Cardano.Ledger.Shelley.API as SL import Cardano.Ledger.Shelley.Translation (toFromByronTranslationContext) +import qualified Cardano.Ledger.Shelley.Translation as SL import qualified Cardano.Protocol.TPraos.API as SL import qualified Cardano.Protocol.TPraos.Rules.Prtcl as SL import qualified Cardano.Protocol.TPraos.Rules.Tickn as SL @@ -51,7 +55,8 @@ import qualified Data.Map.Strict as Map import Data.Maybe (listToMaybe, mapMaybe) import Data.Proxy import Data.SOP.BasicFunctors -import Data.SOP.InPairs (RequiringBoth (..), ignoringBoth) +import Data.SOP.InPairs (RequiringBoth, RequiringBoth' (..), + ignoringBoth) import qualified Data.SOP.Strict as SOP import Data.SOP.Tails (Tails (..)) import qualified Data.SOP.Tails as Tails @@ -66,8 +71,7 @@ import Ouroboros.Consensus.Cardano.Block import Ouroboros.Consensus.Forecast import Ouroboros.Consensus.HardFork.Combinator import Ouroboros.Consensus.HardFork.Combinator.State.Types -import Ouroboros.Consensus.HardFork.History (Bound (boundSlot), - addSlots) +import Ouroboros.Consensus.HardFork.History (Bound (..), addSlots) import Ouroboros.Consensus.HardFork.Simple import Ouroboros.Consensus.Ledger.Abstract import Ouroboros.Consensus.Ledger.SupportsMempool (ByteSize32, @@ -280,23 +284,23 @@ instance CardanoHardForkConstraints c => CanHardFork (CardanoEras c) where type HardForkTxMeasure (CardanoEras c) = ConwayMeasure hardForkEraTranslation = EraTranslation { - translateLedgerState = - PCons translateLedgerStateByronToShelleyWrapper - $ PCons translateLedgerStateShelleyToAllegraWrapper - $ PCons translateLedgerStateAllegraToMaryWrapper - $ PCons translateLedgerStateMaryToAlonzoWrapper - $ PCons translateLedgerStateAlonzoToBabbageWrapper - $ PCons translateLedgerStateBabbageToConwayWrapper + crossEraTickLedgerState = + PCons tickLedgerStateByronToShelley + $ PCons tickLedgerStateAcrossShelley + $ PCons tickLedgerStateAcrossShelley + $ PCons tickLedgerStateAcrossShelley + $ PCons tickLedgerStateAcrossShelley + $ PCons tickLedgerStateAcrossShelley $ PNil - , translateChainDepState = - PCons translateChainDepStateByronToShelleyWrapper - $ PCons translateChainDepStateAcrossShelley - $ PCons translateChainDepStateAcrossShelley - $ PCons translateChainDepStateAcrossShelley - $ PCons translateChainDepStateAcrossShelley - $ PCons translateChainDepStateAcrossShelley + , crossEraTickChainDepState = + PCons tickChainDepStateByronToShelley + $ PCons tickChainDepStateAcrossShelley + $ PCons tickChainDepStateAcrossShelley + $ PCons tickChainDepStateAcrossShelley + $ PCons tickChainDepStateAcrossShelley + $ PCons tickChainDepStateAcrossShelley $ PNil - , crossEraForecast = + , crossEraForecast = PCons crossEraForecastByronToShelleyWrapper $ PCons crossEraForecastAcrossShelley $ PCons crossEraForecastAcrossShelley @@ -322,8 +326,8 @@ instance CardanoHardForkConstraints c => CanHardFork (CardanoEras c) where translateTxAllegraToMaryWrapper translateValidatedTxAllegraToMaryWrapper ) - $ PCons (RequireBoth $ \_cfgMary cfgAlonzo -> - let ctxt = getAlonzoTranslationContext cfgAlonzo + $ PCons (RequireBoth $ \_cfgMary (WrapLedgerConfig cfgAlonzo) -> + let ctxt = shelleyLedgerTranslationContext cfgAlonzo in Pair2 (translateTxMaryToAlonzoWrapper ctxt) @@ -336,8 +340,8 @@ instance CardanoHardForkConstraints c => CanHardFork (CardanoEras c) where (translateTxAlonzoToBabbageWrapper ctxt) (translateValidatedTxAlonzoToBabbageWrapper ctxt) ) - $ PCons (RequireBoth $ \_cfgBabbage cfgConway -> - let ctxt = getConwayTranslationContext cfgConway + $ PCons (RequireBoth $ \_cfgBabbage (WrapLedgerConfig cfgConway) -> + let ctxt = shelleyLedgerTranslationContext cfgConway in Pair2 (translateTxBabbageToConwayWrapper ctxt) @@ -413,44 +417,60 @@ translatePointByronToShelley point bNo = _otherwise -> error "translatePointByronToShelley: invalid Byron state" -translateLedgerStateByronToShelleyWrapper :: +tickLedgerStateByronToShelley :: ( ShelleyCompatible (TPraos c) (ShelleyEra c) , HASH c ~ Blake2b_256 , ADDRHASH c ~ Blake2b_224 ) => RequiringBoth WrapLedgerConfig - (Translate LedgerState) + CrossEraTickLedgerState ByronBlock (ShelleyBlock (TPraos c) (ShelleyEra c)) -translateLedgerStateByronToShelleyWrapper = +tickLedgerStateByronToShelley = RequireBoth $ \_ (WrapLedgerConfig cfgShelley) -> - Translate $ \epochNo ledgerByron -> - ShelleyLedgerState { - shelleyLedgerTip = - translatePointByronToShelley - (ledgerTipPoint ledgerByron) - (byronLedgerTipBlockNo ledgerByron) - , shelleyLedgerState = - SL.translateToShelleyLedgerState - (toFromByronTranslationContext (shelleyLedgerGenesis cfgShelley)) - epochNo - (byronLedgerState ledgerByron) - , shelleyLedgerTransition = - ShelleyTransitionInfo{shelleyAfterVoting = 0} - } - -translateChainDepStateByronToShelleyWrapper :: - RequiringBoth + CrossEraTickLedgerState $ \bound slot -> + applyChainTickLedgerResult cfgShelley slot + . translateLedgerStateByronToShelley + (shelleyLedgerTranslationContext cfgShelley) + bound + +translateLedgerStateByronToShelley :: + ( ShelleyCompatible (TPraos c) (ShelleyEra c) + , HASH c ~ Blake2b_256 + , ADDRHASH c ~ Blake2b_224 + ) + => SL.FromByronTranslationContext c + -> Bound -- ^ Start of the new era + -> LedgerState ByronBlock + -> LedgerState (ShelleyBlock (TPraos c) (ShelleyEra c)) +translateLedgerStateByronToShelley ctx bound ledgerByron = + ShelleyLedgerState { + shelleyLedgerTip = + translatePointByronToShelley + (ledgerTipPoint ledgerByron) + (byronLedgerTipBlockNo ledgerByron) + , shelleyLedgerState = + SL.translateToShelleyLedgerState + ctx + (boundEpoch bound) + (byronLedgerState ledgerByron) + , shelleyLedgerTransition = + ShelleyTransitionInfo{shelleyAfterVoting = 0} + } + +tickChainDepStateByronToShelley :: + ConsensusProtocol (TPraos c) + => RequiringBoth WrapConsensusConfig - (Translate WrapChainDepState) + CrossEraTickChainDepState ByronBlock (ShelleyBlock (TPraos c) (ShelleyEra c)) -translateChainDepStateByronToShelleyWrapper = +tickChainDepStateByronToShelley = RequireBoth $ \_ (WrapConsensusConfig cfgShelley) -> - Translate $ \_ (WrapChainDepState pbftState) -> - WrapChainDepState $ - translateChainDepStateByronToShelley cfgShelley pbftState + CrossEraTickChainDepState $ \_bound view slot -> + tickChainDepState cfgShelley view slot + . translateChainDepStateByronToShelley cfgShelley translateChainDepStateByronToShelley :: forall bc c. @@ -541,18 +561,6 @@ crossEraForecastByronToShelleyWrapper = Translation from Shelley to Allegra -------------------------------------------------------------------------------} -translateLedgerStateShelleyToAllegraWrapper :: - (PraosCrypto c, DSignable c (Hash c EraIndependentTxBody)) - => RequiringBoth - WrapLedgerConfig - (Translate LedgerState) - (ShelleyBlock (TPraos c) (ShelleyEra c)) - (ShelleyBlock (TPraos c) (AllegraEra c)) -translateLedgerStateShelleyToAllegraWrapper = - ignoringBoth $ - Translate $ \_epochNo -> - unComp . SL.translateEra' SL.NoGenesis . Comp - translateTxShelleyToAllegraWrapper :: (PraosCrypto c, DSignable c (Hash c EraIndependentTxBody)) => InjectTx @@ -573,18 +581,6 @@ translateValidatedTxShelleyToAllegraWrapper = InjectValidatedTx $ Translation from Allegra to Mary -------------------------------------------------------------------------------} -translateLedgerStateAllegraToMaryWrapper :: - (PraosCrypto c, DSignable c (Hash c EraIndependentTxBody)) - => RequiringBoth - WrapLedgerConfig - (Translate LedgerState) - (ShelleyBlock (TPraos c) (AllegraEra c)) - (ShelleyBlock (TPraos c) (MaryEra c)) -translateLedgerStateAllegraToMaryWrapper = - ignoringBoth $ - Translate $ \_epochNo -> - unComp . SL.translateEra' SL.NoGenesis . Comp - translateTxAllegraToMaryWrapper :: (PraosCrypto c, DSignable c (Hash c EraIndependentTxBody)) => InjectTx @@ -605,24 +601,6 @@ translateValidatedTxAllegraToMaryWrapper = InjectValidatedTx $ Translation from Mary to Alonzo -------------------------------------------------------------------------------} -translateLedgerStateMaryToAlonzoWrapper :: - (PraosCrypto c, DSignable c (Hash c EraIndependentTxBody)) - => RequiringBoth - WrapLedgerConfig - (Translate LedgerState) - (ShelleyBlock (TPraos c) (MaryEra c)) - (ShelleyBlock (TPraos c) (AlonzoEra c)) -translateLedgerStateMaryToAlonzoWrapper = - RequireBoth $ \_cfgMary cfgAlonzo -> - Translate $ \_epochNo -> - unComp . SL.translateEra' (getAlonzoTranslationContext cfgAlonzo) . Comp - -getAlonzoTranslationContext :: - WrapLedgerConfig (ShelleyBlock (TPraos c) (AlonzoEra c)) - -> SL.TranslationContext (AlonzoEra c) -getAlonzoTranslationContext = - shelleyLedgerTranslationContext . unwrapLedgerConfig - translateTxMaryToAlonzoWrapper :: (PraosCrypto c, DSignable c (Hash c EraIndependentTxBody)) => SL.TranslationContext (AlonzoEra c) @@ -646,28 +624,6 @@ translateValidatedTxMaryToAlonzoWrapper ctxt = InjectValidatedTx $ Translation from Alonzo to Babbage -------------------------------------------------------------------------------} -translateLedgerStateAlonzoToBabbageWrapper :: - (Praos.PraosCrypto c, TPraos.PraosCrypto c) - => RequiringBoth - WrapLedgerConfig - (Translate LedgerState) - (ShelleyBlock (TPraos c) (AlonzoEra c)) - (ShelleyBlock (Praos c) (BabbageEra c)) -translateLedgerStateAlonzoToBabbageWrapper = - RequireBoth $ \_cfgAlonzo _cfgBabbage -> - Translate $ \_epochNo -> - unComp . SL.translateEra' SL.NoGenesis . Comp . transPraosLS - where - transPraosLS :: - LedgerState (ShelleyBlock (TPraos c) (AlonzoEra c)) -> - LedgerState (ShelleyBlock (Praos c) (AlonzoEra c)) - transPraosLS (ShelleyLedgerState wo nes st) = - ShelleyLedgerState - { shelleyLedgerTip = fmap castShelleyTip wo - , shelleyLedgerState = nes - , shelleyLedgerTransition = st - } - translateTxAlonzoToBabbageWrapper :: (Praos.PraosCrypto c) => SL.TranslationContext (BabbageEra c) @@ -708,24 +664,6 @@ translateValidatedTxAlonzoToBabbageWrapper ctxt = InjectValidatedTx $ Translation from Babbage to Conway -------------------------------------------------------------------------------} -translateLedgerStateBabbageToConwayWrapper :: - (Praos.PraosCrypto c) - => RequiringBoth - WrapLedgerConfig - (Translate LedgerState) - (ShelleyBlock (Praos c) (BabbageEra c)) - (ShelleyBlock (Praos c) (ConwayEra c)) -translateLedgerStateBabbageToConwayWrapper = - RequireBoth $ \_cfgBabbage cfgConway -> - Translate $ \_epochNo -> - unComp . SL.translateEra' (getConwayTranslationContext cfgConway) . Comp - -getConwayTranslationContext :: - WrapLedgerConfig (ShelleyBlock (Praos c) (ConwayEra c)) - -> SL.TranslationContext (ConwayEra c) -getConwayTranslationContext = - shelleyLedgerTranslationContext . unwrapLedgerConfig - translateTxBabbageToConwayWrapper :: (Praos.PraosCrypto c) => SL.TranslationContext (ConwayEra c) diff --git a/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/Node.hs b/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/Node.hs index 6bf492fc1f..cfa2601add 100644 --- a/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/Node.hs +++ b/ouroboros-consensus-cardano/src/ouroboros-consensus-cardano/Ouroboros/Consensus/Cardano/Node.hs @@ -66,6 +66,7 @@ import qualified Cardano.Ledger.Api.Era as L import qualified Cardano.Ledger.Api.Transition as L import qualified Cardano.Ledger.BaseTypes as SL import qualified Cardano.Ledger.Shelley.API as SL +import qualified Cardano.Ledger.Shelley.Translation as SL import Cardano.Prelude (cborError) import qualified Cardano.Protocol.TPraos.OCert as Absolute (KESPeriod (..), ocertKESPeriod) @@ -96,6 +97,7 @@ import Ouroboros.Consensus.Config import Ouroboros.Consensus.HardFork.Combinator import Ouroboros.Consensus.HardFork.Combinator.Embed.Nary import Ouroboros.Consensus.HardFork.Combinator.Serialisation +import Ouroboros.Consensus.HardFork.Combinator.State.Types import qualified Ouroboros.Consensus.HardFork.History as History import Ouroboros.Consensus.HeaderValidation import Ouroboros.Consensus.Ledger.Extended @@ -103,10 +105,12 @@ import Ouroboros.Consensus.Node.NetworkProtocolVersion import Ouroboros.Consensus.Node.ProtocolInfo import Ouroboros.Consensus.Node.Run import qualified Ouroboros.Consensus.Protocol.Ledger.HotKey as HotKey -import Ouroboros.Consensus.Protocol.Praos (Praos, PraosParams (..)) +import Ouroboros.Consensus.Protocol.Praos (Praos, PraosParams (..), + genesisPraosState) import Ouroboros.Consensus.Protocol.Praos.Common (praosCanBeLeaderOpCert) -import Ouroboros.Consensus.Protocol.TPraos (TPraos, TPraosParams (..)) +import Ouroboros.Consensus.Protocol.TPraos (TPraos, TPraosParams (..), + genesisTPraosState) import qualified Ouroboros.Consensus.Protocol.TPraos as Shelley import Ouroboros.Consensus.Shelley.HFEras () import Ouroboros.Consensus.Shelley.Ledger (ShelleyBlock) @@ -119,6 +123,8 @@ import Ouroboros.Consensus.Shelley.Node.Common (ShelleyEraWithCrypto, shelleyBlockIssuerVKey) import qualified Ouroboros.Consensus.Shelley.Node.Praos as Praos import qualified Ouroboros.Consensus.Shelley.Node.TPraos as TPraos +import Ouroboros.Consensus.Shelley.ShelleyHFC + (translateShelleyLedgerState) import Ouroboros.Consensus.Storage.Serialisation import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util.Assert @@ -543,20 +549,19 @@ toTriggerHardFork = \case CardanoTriggerHardForkAtEpoch epochNo -> TriggerHardForkAtEpoch epochNo -newtype CardanoHardForkTriggers = CardanoHardForkTriggers { +newtype CardanoHardForkTriggers c = CardanoHardForkTriggers { getCardanoHardForkTriggers :: - NP CardanoHardForkTrigger (CardanoShelleyEras StandardCrypto) + NP CardanoHardForkTrigger (CardanoShelleyEras c) } pattern CardanoHardForkTriggers' :: - (c ~ StandardCrypto) - => CardanoHardForkTrigger (ShelleyBlock (TPraos c) (ShelleyEra c)) + CardanoHardForkTrigger (ShelleyBlock (TPraos c) (ShelleyEra c)) -> CardanoHardForkTrigger (ShelleyBlock (TPraos c) (AllegraEra c)) -> CardanoHardForkTrigger (ShelleyBlock (TPraos c) (MaryEra c)) -> CardanoHardForkTrigger (ShelleyBlock (TPraos c) (AlonzoEra c)) -> CardanoHardForkTrigger (ShelleyBlock (Praos c) (BabbageEra c)) -> CardanoHardForkTrigger (ShelleyBlock (Praos c) (ConwayEra c)) - -> CardanoHardForkTriggers + -> CardanoHardForkTriggers c pattern CardanoHardForkTriggers' { triggerHardForkShelley , triggerHardForkAllegra @@ -576,6 +581,21 @@ pattern CardanoHardForkTriggers' { ) {-# COMPLETE CardanoHardForkTriggers' #-} +-- | Get the index of the first era which is not scheduled to end immediately +-- via @'CardanoTriggerHardForkAtEpoch' 0@. +-- +-- For mainnet, which starts in Byron, this returns +-- +-- @'Z' 'Proxy' :: 'NS' 'Proxy' ('CardanoEras' c)@ +getInitialCardanoEra :: CardanoHardForkTriggers c -> NS Proxy (CardanoEras c) +getInitialCardanoEra (CardanoHardForkTriggers triggers) = + go triggers + where + go :: NP CardanoHardForkTrigger xs -> NS Proxy (x : xs) + go = \case + CardanoTriggerHardForkAtEpoch (EpochNo 0) :* ts -> S $ go ts + _ -> Z Proxy + -- | Parameters needed to run Cardano. -- -- __On the relation between 'cardanoHardForkTriggers' and 'cardanoProtocolVersion'__: @@ -602,7 +622,7 @@ pattern CardanoHardForkTriggers' { data CardanoProtocolParams c = CardanoProtocolParams { byronProtocolParams :: ProtocolParamsByron , shelleyBasedProtocolParams :: ProtocolParamsShelleyBased c - , cardanoHardForkTriggers :: CardanoHardForkTriggers + , cardanoHardForkTriggers :: CardanoHardForkTriggers c , cardanoLedgerTransitionConfig :: L.TransitionConfig (L.LatestKnownEra c) , cardanoCheckpoints :: CheckpointsMap (CardanoBlock c) -- | The greatest protocol version that this node's software and config @@ -657,7 +677,7 @@ protocolInfoCardano paramsCardano CardanoProtocolParams { byronProtocolParams , shelleyBasedProtocolParams - , cardanoHardForkTriggers = CardanoHardForkTriggers' { + , cardanoHardForkTriggers = cardanoHardForkTriggers@CardanoHardForkTriggers' { triggerHardForkShelley , triggerHardForkAllegra , triggerHardForkMary @@ -688,6 +708,16 @@ protocolInfoCardano paramsCardano transitionConfigBabbage = transitionConfigConway ^. L.tcPreviousEraConfigL transitionConfigConway = cardanoLedgerTransitionConfig + transitionCfgs :: NP WrapTransitionConfig (CardanoShelleyEras c) + transitionCfgs = + WrapTransitionConfig transitionConfigShelley + :* WrapTransitionConfig transitionConfigAllegra + :* WrapTransitionConfig transitionConfigMary + :* WrapTransitionConfig transitionConfigAlonzo + :* WrapTransitionConfig transitionConfigBabbage + :* WrapTransitionConfig transitionConfigConway + :* Nil + -- The major protocol version of the last era is the maximum major protocol -- version we support. -- @@ -702,7 +732,7 @@ protocolInfoCardano paramsCardano , topLevelConfigLedger = ledgerConfigByron , topLevelConfigBlock = blockConfigByron } - , pInfoInitLedger = initExtLedgerStateByron + , pInfoInitLedger = ExtLedgerState initLedgerStateByron initHeaderStateByron } = protocolInfoByron byronProtocolParams partialConsensusConfigByron :: PartialConsensusConfig (BlockProtocol ByronBlock) @@ -945,42 +975,71 @@ protocolInfoCardano paramsCardano , topLevelConfigCheckpoints = cardanoCheckpoints } - -- When the initial ledger state is not in the Byron era, register various - -- data from the genesis config (if provided) in the ledger state. For - -- example, this includes initial staking and initial funds (useful for - -- testing/benchmarking). + -- See Note [Creating the initial extended ledger state for Cardano] initExtLedgerStateCardano :: ExtLedgerState (CardanoBlock c) - initExtLedgerStateCardano = ExtLedgerState { - headerState = initHeaderState - , ledgerState = - HardForkLedgerState - . hap (fn id :* registerAny) - $ hardForkLedgerStatePerEra initLedgerState - } + initExtLedgerStateCardano = + injectInitialExtLedgerState + $ hliftA3 + (\(Fn injIntoTestState) (WrapChainDepState cds) lst -> + ExtLedgerState { + ledgerState = injIntoTestState lst + , headerState = genesisHeaderState cds + }) + injectIntoTestState + initChainDepStates + initLedgerState where - initHeaderState :: HeaderState (CardanoBlock c) - initLedgerState :: LedgerState (CardanoBlock c) - ExtLedgerState initLedgerState initHeaderState = - injectInitialExtLedgerState cfg initExtLedgerStateByron - - registerAny :: NP (LedgerState -.-> LedgerState) (CardanoShelleyEras c) - registerAny = - hcmap (Proxy @IsShelleyBlock) injectIntoTestState $ - WrapTransitionConfig transitionConfigShelley - :* WrapTransitionConfig transitionConfigAllegra - :* WrapTransitionConfig transitionConfigMary - :* WrapTransitionConfig transitionConfigAlonzo - :* WrapTransitionConfig transitionConfigBabbage - :* WrapTransitionConfig transitionConfigConway - :* Nil - - injectIntoTestState :: - L.EraTransition era - => WrapTransitionConfig (ShelleyBlock proto era) - -> (LedgerState -.-> LedgerState) (ShelleyBlock proto era) - injectIntoTestState (WrapTransitionConfig cfg) = fn $ \st -> st { - Shelley.shelleyLedgerState = L.injectIntoTestState cfg (Shelley.shelleyLedgerState st) - } + initLedgerState :: NS LedgerState (CardanoEras c) + initLedgerState = + mkInitialStateViaTranslation + ledgerStateTranslations + initLedgerStateByron + (getInitialCardanoEra cardanoHardForkTriggers) + + initChainDepStates :: NP WrapChainDepState (CardanoEras c) + initChainDepStates = + WrapChainDepState (headerStateChainDep initHeaderStateByron) + :* WrapChainDepState tpraos + :* WrapChainDepState tpraos + :* WrapChainDepState tpraos + :* WrapChainDepState tpraos + :* WrapChainDepState praos + :* WrapChainDepState praos + :* Nil + where + tpraos = genesisTPraosState initialNonceShelley + praos = genesisPraosState initialNonceShelley + + ledgerStateTranslations :: InPairs (Translate LedgerState) (CardanoEras c) + ledgerStateTranslations = + PCons byronToShelleyTranslation + $ PCons (interShelleyTranslation transitionConfigAllegra) + $ PCons (interShelleyTranslation transitionConfigMary) + $ PCons (interShelleyTranslation transitionConfigAlonzo) + $ PCons (interShelleyTranslation transitionConfigBabbage) + $ PCons (interShelleyTranslation transitionConfigConway) + PNil + where + byronToShelleyTranslation = + CrossEra $ \(Current bound _) -> + translateLedgerStateByronToShelley ctx bound + where + ctx = SL.toFromByronTranslationContext genesisShelley + + interShelleyTranslation transitionConfig = + CrossEra $ \_ -> translateShelleyLedgerState ctx + where + ctx = transitionConfig ^. L.tcTranslationContextL + + injectIntoTestState :: NP (LedgerState -.-> LedgerState) (CardanoEras c) + injectIntoTestState = + fn id -- do nothing in Byron + :* hcmap (Proxy @IsShelleyBlock) + (\(WrapTransitionConfig cfg) -> fn $ \st -> st { + Shelley.shelleyLedgerState = + L.injectIntoTestState cfg (Shelley.shelleyLedgerState st) + }) + transitionCfgs -- | For each element in the list, a block forging thread will be started. -- @@ -1066,6 +1125,32 @@ protocolInfoCardano paramsCardano praos :* Nil +{- Note [Creating the initial extended ledger state for Cardano] + ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + + For mainnet, this is a very simple operation: Create the initial Byron + extended ledger state, and wrap it in the HFC envelope. + + However, for testing/benchmarks, we also want to support starting at genesis + from some /later/, non-Byron era, which is configured by triggering a hard + fork at epoch 0 for a prefix of all eras. + + In this case, we construct the initial header state/chain-dependent state for + that era directly, due to their simple structure. In contrast, we construct + the initial ledger state by (potentially repeatedly) invoking the + Ledger-provided translation functions, in order to retain backwards + compatibility. + + (If we want/can break backwards compatibility, it would be cleaner to + directly use Ledger's 'createInitialState' instead of the iterated + translation. However, this means that usages of eg @nonAvvmBalances@ in the + Byron genesis config would need to be replaced, which seems easy, but tedious + in particular for existing long-lived testnets like preview.) + + Finally, if we start from a post-Byron era, we also register certain initial + data from the genesis config, for example initial staking/funds. +-} + protocolClientInfoCardano :: forall c. -- Byron diff --git a/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Ledger/Ledger.hs b/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Ledger/Ledger.hs index 380f97f562..c80850a788 100644 --- a/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Ledger/Ledger.hs +++ b/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Ledger/Ledger.hs @@ -91,6 +91,7 @@ import Ouroboros.Consensus.Shelley.Ledger.Config import Ouroboros.Consensus.Shelley.Ledger.Protocol () import Ouroboros.Consensus.Shelley.Protocol.Abstract (EnvelopeCheckError, envelopeChecks, mkHeaderView) +import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util ((..:)) import Ouroboros.Consensus.Util.CBOR (decodeWithOrigin, encodeWithOrigin) diff --git a/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Node/TPraos.hs b/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Node/TPraos.hs index 44d13dee75..108a1ceda0 100644 --- a/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Node/TPraos.hs +++ b/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/Node/TPraos.hs @@ -36,7 +36,6 @@ import qualified Cardano.Crypto.VRF as VRF import qualified Cardano.Ledger.Api.Era as L import qualified Cardano.Ledger.Api.Transition as L import qualified Cardano.Ledger.Shelley.API as SL -import qualified Cardano.Protocol.TPraos.API as SL import qualified Cardano.Protocol.TPraos.OCert as Absolute (KESPeriod (..)) import qualified Cardano.Protocol.TPraos.OCert as SL import Cardano.Slotting.EpochInfo @@ -281,12 +280,8 @@ protocolInfoTPraosShelleyBased ProtocolParamsShelleyBased { , shelleyLedgerTransition = ShelleyTransitionInfo {shelleyAfterVoting = 0} } - initChainDepState :: TPraosState c - initChainDepState = TPraosState Origin $ - SL.initialChainDepState initialNonce (SL.sgGenDelegs genesis) - initExtLedgerState :: ExtLedgerState (ShelleyBlock (TPraos c) era) initExtLedgerState = ExtLedgerState { ledgerState = initLedgerState - , headerState = genesisHeaderState initChainDepState + , headerState = genesisHeaderState $ genesisTPraosState initialNonce } diff --git a/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/ShelleyHFC.hs b/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/ShelleyHFC.hs index 1527dc8c6c..491900a432 100644 --- a/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/ShelleyHFC.hs +++ b/ouroboros-consensus-cardano/src/shelley/Ouroboros/Consensus/Shelley/ShelleyHFC.hs @@ -11,6 +11,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -21,7 +22,9 @@ module Ouroboros.Consensus.Shelley.ShelleyHFC ( , ShelleyPartialLedgerConfig (..) , crossEraForecastAcrossShelley , forecastAcrossShelley - , translateChainDepStateAcrossShelley + , tickChainDepStateAcrossShelley + , tickLedgerStateAcrossShelley + , translateShelleyLedgerState ) where import qualified Cardano.Ledger.Api.Era as L @@ -35,7 +38,7 @@ import Control.Monad.Except (runExcept, throwError, withExceptT) import Data.Coerce import qualified Data.Map.Strict as Map import Data.SOP.BasicFunctors -import Data.SOP.InPairs (RequiringBoth (..), ignoringBoth) +import Data.SOP.InPairs (RequiringBoth, RequiringBoth' (..)) import qualified Data.Text as T (pack) import Data.Void (Void) import Data.Word @@ -46,8 +49,7 @@ import Ouroboros.Consensus.Block import Ouroboros.Consensus.Config import Ouroboros.Consensus.Forecast import qualified Ouroboros.Consensus.Forecast as Forecast -import Ouroboros.Consensus.HardFork.Combinator hiding - (translateChainDepState) +import Ouroboros.Consensus.HardFork.Combinator import Ouroboros.Consensus.HardFork.Combinator.Serialisation.Common import Ouroboros.Consensus.HardFork.Combinator.State.Types import Ouroboros.Consensus.HardFork.History (Bound (boundSlot)) @@ -64,6 +66,7 @@ import Ouroboros.Consensus.Shelley.Eras import Ouroboros.Consensus.Shelley.Ledger import Ouroboros.Consensus.Shelley.Ledger.Inspect as Shelley.Inspect import Ouroboros.Consensus.Shelley.Node () +import Ouroboros.Consensus.Shelley.Protocol.Abstract import Ouroboros.Consensus.TypeFamilyWrappers {------------------------------------------------------------------------------- @@ -238,25 +241,9 @@ instance ShelleyCompatible proto era => HasPartialLedgerConfig (ShelleyBlock pro } } -translateChainDepStateAcrossShelley :: - forall eraFrom eraTo protoFrom protoTo. - ( TranslateProto protoFrom protoTo - ) - => RequiringBoth - WrapConsensusConfig - (Translate WrapChainDepState) - (ShelleyBlock protoFrom eraFrom) - (ShelleyBlock protoTo eraTo) -translateChainDepStateAcrossShelley = - ignoringBoth $ - Translate $ \_epochNo (WrapChainDepState chainDepState) -> - -- Same protocol, same 'ChainDepState'. Note that we don't have to apply - -- any changes related to an epoch transition, this is already done when - -- ticking the state. - WrapChainDepState $ translateChainDepState (Proxy @(protoFrom, protoTo)) chainDepState - +-- | Wrapper around 'forecastAcrossShelley'. crossEraForecastAcrossShelley :: - forall eraFrom eraTo protoFrom protoTo. + forall protoFrom protoTo eraFrom eraTo. ( TranslateProto protoFrom protoTo , LedgerSupportsProtocol (ShelleyBlock protoFrom eraFrom) ) @@ -267,7 +254,14 @@ crossEraForecastAcrossShelley :: (ShelleyBlock protoTo eraTo) crossEraForecastAcrossShelley = coerce forecastAcrossShelley --- | Forecast from a Shelley-based era to the next Shelley-based era. +-- | Forecast from a Shelley-based era to the next Shelley-based era. We do so +-- via the "forecast-then-translate" scheme: +-- +-- - First, we forecast for the given slot using the logic of @'ShelleyBlock' +-- protoFrom eraFrom@. +-- +-- - Then, we translate the resulting 'LedgerView' from @protoFrom@ to +-- @protoTo@. forecastAcrossShelley :: forall protoFrom protoTo eraFrom eraTo. ( TranslateProto protoFrom protoTo @@ -308,31 +302,84 @@ forecastAcrossShelley cfgFrom cfgTo transition forecastFor ledgerStateFrom (SL.stabilityWindow (shelleyLedgerGlobals cfgFrom)) (SL.stabilityWindow (shelleyLedgerGlobals cfgTo)) +-- | Tick the ledger state from one Shelley-based era @eraFrom@ to the the next +-- era @eraTo@. We do so via the "translate-then-tick" scheme: +-- +-- - First, we translate the ledger state from @eraFrom@ to @eraTo@. +-- +-- - Then, we tick the ledger state to the target slot using the logic of +-- @eraTo@. +-- +-- Note that this function also allows to change the protocol; this is harmless +-- as the ledger state only depends trivially on the protocol via the +-- @HeaderHash@ contained in the tip. +tickLedgerStateAcrossShelley :: + forall protoFrom protoTo eraFrom eraTo. + ( ShelleyBasedEra eraTo + , eraFrom ~ SL.PreviousEra eraTo + , SL.TranslateEra eraTo SL.NewEpochState + , SL.TranslationError eraTo SL.NewEpochState ~ Void + , ProtoCrypto protoFrom ~ ProtoCrypto protoTo + ) + => RequiringBoth + WrapLedgerConfig + CrossEraTickLedgerState + (ShelleyBlock protoFrom eraFrom) + (ShelleyBlock protoTo eraTo) +tickLedgerStateAcrossShelley = + RequireBoth $ \_cfgFrom (WrapLedgerConfig cfgTo) -> + CrossEraTickLedgerState $ \_bound slot -> + applyChainTickLedgerResult cfgTo slot + . translateShelleyLedgerState + (shelleyLedgerTranslationContext cfgTo) + +-- | Tick the chain-dependent state from one Shelley-based era to the the next, +-- potentially changing the protocol. We do so via the "translate-then-tick" +-- scheme: +-- +-- - First, we translate the chain-dependent state from @protoFrom@ to +-- @protoTo@. +-- +-- - Then, we tick the chain-dependent state to the target slot using the logic +-- of @protoTo@. +-- +-- Note that this function also allows to change the ledger era; this is +-- harmless as the chain-dependent state doesn't depend on it at all. +tickChainDepStateAcrossShelley :: + forall protoFrom protoTo eraFrom eraTo. + ( TranslateProto protoFrom protoTo + , ConsensusProtocol protoTo + ) + => RequiringBoth + WrapConsensusConfig + CrossEraTickChainDepState + (ShelleyBlock protoFrom eraFrom) + (ShelleyBlock protoTo eraTo) +tickChainDepStateAcrossShelley = + RequireBoth $ \_cfgFrom (WrapConsensusConfig cfgTo) -> + CrossEraTickChainDepState $ \_bound view slot -> + tickChainDepState cfgTo view slot + . translateChainDepState (Proxy @(protoFrom, protoTo)) + {------------------------------------------------------------------------------- Translation from one Shelley-based era to another Shelley-based era -------------------------------------------------------------------------------} -instance ( ShelleyBasedEra era - , ShelleyBasedEra (SL.PreviousEra era) - , SL.Era (SL.PreviousEra era) - , EraCrypto (SL.PreviousEra era) ~ EraCrypto era - ) => SL.TranslateEra era (ShelleyTip proto) where - translateEra _ (ShelleyTip sno bno (ShelleyHash hash)) = - return $ ShelleyTip sno bno (ShelleyHash hash) - -instance ( ShelleyBasedEra era - , SL.TranslateEra era (ShelleyTip proto) - , SL.TranslateEra era SL.NewEpochState - , SL.TranslationError era SL.NewEpochState ~ Void - ) => SL.TranslateEra era (LedgerState :.: ShelleyBlock proto) where - translateEra ctxt (Comp (ShelleyLedgerState tip state _transition)) = do - tip' <- mapM (SL.translateEra ctxt) tip - state' <- SL.translateEra ctxt state - return $ Comp $ ShelleyLedgerState { - shelleyLedgerTip = tip' - , shelleyLedgerState = state' - , shelleyLedgerTransition = ShelleyTransitionInfo 0 - } +translateShelleyLedgerState :: + ( eraFrom ~ SL.PreviousEra eraTo + , SL.TranslateEra eraTo SL.NewEpochState + , SL.TranslationError eraTo SL.NewEpochState ~ Void + , ProtoCrypto protoFrom ~ ProtoCrypto protoTo + ) + => SL.TranslationContext eraTo + -> LedgerState (ShelleyBlock protoFrom eraFrom) + -> LedgerState (ShelleyBlock protoTo eraTo ) +translateShelleyLedgerState ctx (ShelleyLedgerState wo nes st) = + ShelleyLedgerState { + shelleyLedgerTip = fmap castShelleyTip wo + , shelleyLedgerState = SL.translateEra' ctx nes + , shelleyLedgerTransition = st + } instance ( ShelleyBasedEra era , SL.TranslateEra era WrapTx diff --git a/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/Consensus/Cardano/ProtocolInfo.hs b/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/Consensus/Cardano/ProtocolInfo.hs index e3943da9f6..a1e66ed9b0 100644 --- a/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/Consensus/Cardano/ProtocolInfo.hs +++ b/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/Consensus/Cardano/ProtocolInfo.hs @@ -90,12 +90,12 @@ protocolVersionZero = SL.ProtVer versionZero 0 versionZero :: SL.Version versionZero = SL.natVersion @0 -hardForkOnDefaultProtocolVersions :: CardanoHardForkTriggers +hardForkOnDefaultProtocolVersions :: CardanoHardForkTriggers c hardForkOnDefaultProtocolVersions = CardanoHardForkTriggers $ hpure CardanoTriggerHardForkAtDefaultVersion -hardForkInto :: Era -> CardanoHardForkTriggers +hardForkInto :: Era -> CardanoHardForkTriggers c hardForkInto Byron = hardForkOnDefaultProtocolVersions hardForkInto Shelley = hardForkOnDefaultProtocolVersions @@ -151,7 +151,7 @@ mkSimpleTestProtocolInfo :: -> ByronSlotLengthInSeconds -> ShelleySlotLengthInSeconds -> SL.ProtVer - -> CardanoHardForkTriggers + -> CardanoHardForkTriggers c -> ProtocolInfo (CardanoBlock c) mkSimpleTestProtocolInfo decentralizationParam @@ -230,7 +230,7 @@ mkTestProtocolInfo :: -- ^ See 'protocolInfoCardano' for the details of what is the -- relation between this version and any 'TriggerHardForkAtVersion' -- that __might__ appear in the 'CardanoHardForkTriggers' parameter. - -> CardanoHardForkTriggers + -> CardanoHardForkTriggers c -- ^ Specification of the era to which the initial state should hard-fork to. -> (ProtocolInfo (CardanoBlock c), m [BlockForging m (CardanoBlock c)]) mkTestProtocolInfo diff --git a/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/ThreadNet/Infra/ShelleyBasedHardFork.hs b/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/ThreadNet/Infra/ShelleyBasedHardFork.hs index d4961835e0..1eedc5e6ac 100644 --- a/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/ThreadNet/Infra/ShelleyBasedHardFork.hs +++ b/ouroboros-consensus-cardano/src/unstable-cardano-testlib/Test/ThreadNet/Infra/ShelleyBasedHardFork.hs @@ -42,12 +42,12 @@ import Ouroboros.Consensus.Block.Forging (BlockForging) import Ouroboros.Consensus.Cardano.CanHardFork (ShelleyPartialLedgerConfig (..), crossEraForecastAcrossShelley, - translateChainDepStateAcrossShelley) + tickChainDepStateAcrossShelley, + tickLedgerStateAcrossShelley) import Ouroboros.Consensus.Cardano.Node (TriggerHardFork (..)) import Ouroboros.Consensus.HardFork.Combinator import Ouroboros.Consensus.HardFork.Combinator.Embed.Binary import Ouroboros.Consensus.HardFork.Combinator.Serialisation -import qualified Ouroboros.Consensus.HardFork.Combinator.State.Types as HFC import qualified Ouroboros.Consensus.HardFork.History as History import Ouroboros.Consensus.Ledger.Basics (LedgerConfig) import Ouroboros.Consensus.Ledger.SupportsMempool @@ -173,25 +173,10 @@ instance ShelleyBasedHardForkConstraints proto1 era1 proto2 era2 TxMeasure (ShelleyBlock proto2 era2) hardForkEraTranslation = EraTranslation { - translateLedgerState = PCons translateLedgerState PNil - , translateChainDepState = PCons translateChainDepStateAcrossShelley PNil - , crossEraForecast = PCons crossEraForecastAcrossShelley PNil + crossEraTickLedgerState = PCons tickLedgerStateAcrossShelley PNil + , crossEraTickChainDepState = PCons tickChainDepStateAcrossShelley PNil + , crossEraForecast = PCons crossEraForecastAcrossShelley PNil } - where - translateLedgerState :: - InPairs.RequiringBoth - WrapLedgerConfig - (HFC.Translate LedgerState) - (ShelleyBlock proto1 era1) - (ShelleyBlock proto2 era2) - translateLedgerState = - InPairs.RequireBoth - $ \_cfg1 cfg2 -> HFC.Translate - $ \_epochNo -> - unComp - . SL.translateEra' - (shelleyLedgerTranslationContext (unwrapLedgerConfig cfg2)) - . Comp hardForkChainSel = Tails.mk2 CompareSameSelectView diff --git a/ouroboros-consensus-cardano/src/unstable-cardano-tools/Cardano/Tools/DBAnalyser/Block/Cardano.hs b/ouroboros-consensus-cardano/src/unstable-cardano-tools/Cardano/Tools/DBAnalyser/Block/Cardano.hs index 341f0bcc08..e7c5a8f264 100644 --- a/ouroboros-consensus-cardano/src/unstable-cardano-tools/Cardano/Tools/DBAnalyser/Block/Cardano.hs +++ b/ouroboros-consensus-cardano/src/unstable-cardano-tools/Cardano/Tools/DBAnalyser/Block/Cardano.hs @@ -189,7 +189,7 @@ data CardanoConfig = CardanoConfig { , conwayGenesisPath :: FilePath -- | @Test*HardForkAtEpoch@ for each Shelley era - , cfgHardForkTriggers :: CardanoHardForkTriggers + , cfgHardForkTriggers :: CardanoHardForkTriggers StandardCrypto } instance AdjustFilePaths CardanoConfig where @@ -363,7 +363,7 @@ mkCardanoProtocolInfo :: -> Maybe PBftSignatureThreshold -> SL.TransitionConfig (L.LatestKnownEra StandardCrypto) -> Nonce - -> CardanoHardForkTriggers + -> CardanoHardForkTriggers StandardCrypto -> ProtocolInfo (CardanoBlock StandardCrypto) mkCardanoProtocolInfo genesisByron signatureThreshold transitionConfig initialNonce triggers = fst $ protocolInfoCardano @_ @IO diff --git a/ouroboros-consensus-cardano/test/cardano-test/Test/Consensus/Cardano/SupportsSanityCheck.hs b/ouroboros-consensus-cardano/test/cardano-test/Test/Consensus/Cardano/SupportsSanityCheck.hs index fa91ae7ac2..e617c98e06 100644 --- a/ouroboros-consensus-cardano/test/cardano-test/Test/Consensus/Cardano/SupportsSanityCheck.hs +++ b/ouroboros-consensus-cardano/test/cardano-test/Test/Consensus/Cardano/SupportsSanityCheck.hs @@ -61,7 +61,7 @@ data SimpleTestProtocolInfoSetup = SimpleTestProtocolInfoSetup , securityParam :: SecurityParam , byronSlotLength :: ByronSlotLengthInSeconds , shelleySlotLength :: ShelleySlotLengthInSeconds - , hardForkTriggers :: CardanoHardForkTriggers + , hardForkTriggers :: CardanoHardForkTriggers StandardCrypto } instance Arbitrary SimpleTestProtocolInfoSetup where diff --git a/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/HardFork/Combinator.hs b/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/HardFork/Combinator.hs index c59f9b27ba..33622af310 100644 --- a/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/HardFork/Combinator.hs +++ b/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/HardFork/Combinator.hs @@ -18,7 +18,7 @@ module Test.Consensus.HardFork.Combinator (tests) where import qualified Data.Map.Strict as Map import Data.SOP.Counting -import Data.SOP.InPairs (RequiringBoth (..)) +import Data.SOP.InPairs (RequiringBoth, RequiringBoth' (..)) import qualified Data.SOP.InPairs as InPairs import Data.SOP.OptNP (OptNP (..)) import Data.SOP.Strict @@ -366,9 +366,9 @@ instance CanHardFork '[BlockA, BlockB] where type HardForkTxMeasure '[BlockA, BlockB] = IgnoringOverflow ByteSize32 hardForkEraTranslation = EraTranslation { - translateLedgerState = PCons ledgerState_AtoB PNil - , translateChainDepState = PCons chainDepState_AtoB PNil - , crossEraForecast = PCons forecast_AtoB PNil + crossEraTickLedgerState = PCons ledgerState_AtoB PNil + , crossEraTickChainDepState = PCons chainDepState_AtoB PNil + , crossEraForecast = PCons forecast_AtoB PNil } hardForkChainSel = Tails.mk2 CompareBlockNo hardForkInjectTxs = InPairs.mk2 injectTx_AtoB @@ -411,21 +411,26 @@ instance SerialiseHFC '[BlockA, BlockB] ledgerState_AtoB :: RequiringBoth WrapLedgerConfig - (Translate LedgerState) + CrossEraTickLedgerState BlockA BlockB -ledgerState_AtoB = InPairs.ignoringBoth $ Translate $ \_ LgrA{..} -> LgrB { - lgrB_tip = castPoint lgrA_tip - } +ledgerState_AtoB = + RequireBoth $ \_cfgA (WrapLedgerConfig cfgB) -> + CrossEraTickLedgerState $ \_ slot LgrA{..} -> + applyChainTickLedgerResult cfgB slot LgrB { + lgrB_tip = castPoint lgrA_tip + } chainDepState_AtoB :: RequiringBoth WrapConsensusConfig - (Translate WrapChainDepState) + CrossEraTickChainDepState BlockA BlockB -chainDepState_AtoB = InPairs.ignoringBoth $ Translate $ \_ _ -> - WrapChainDepState () +chainDepState_AtoB = + InPairs.ignoringBoth $ + CrossEraTickChainDepState $ \_ _ _ _ -> + TickedTrivial forecast_AtoB :: RequiringBoth diff --git a/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/Praos.hs b/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/Praos.hs index c9c54ed4cd..4d845b19c8 100644 --- a/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/Praos.hs +++ b/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/Praos.hs @@ -28,6 +28,7 @@ module Ouroboros.Consensus.Protocol.Praos ( , PraosValidationErr (..) , Ticked (..) , forgePraosFields + , genesisPraosState , praosCheckCanForge ) where @@ -36,7 +37,7 @@ import qualified Cardano.Crypto.DSIGN as DSIGN import qualified Cardano.Crypto.KES as KES import Cardano.Crypto.VRF (hashVerKeyVRF) import qualified Cardano.Crypto.VRF as VRF -import Cardano.Ledger.BaseTypes (ActiveSlotCoeff, Nonce, (⭒)) +import Cardano.Ledger.BaseTypes (ActiveSlotCoeff, Nonce (..), (⭒)) import qualified Cardano.Ledger.BaseTypes as SL import qualified Cardano.Ledger.Chain as SL import Cardano.Ledger.Crypto (Crypto, DSIGN, KES, StandardCrypto, VRF) @@ -58,8 +59,6 @@ import qualified Cardano.Protocol.TPraos.Rules.Prtcl as SL import qualified Cardano.Protocol.TPraos.Rules.Tickn as SL import Cardano.Slotting.EpochInfo (EpochInfo, epochInfoEpoch, epochInfoFirst, hoistEpochInfo) -import Cardano.Slotting.Slot (EpochNo (EpochNo), SlotNo (SlotNo), - WithOrigin, unSlotNo) import qualified Codec.CBOR.Encoding as CBOR import Codec.Serialise (Serialise (decode, encode)) import Control.Exception (throw) @@ -69,13 +68,12 @@ import Data.Coerce (coerce) import Data.Functor.Identity (runIdentity) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map -import Data.Proxy (Proxy (Proxy)) import qualified Data.Set as Set import Data.Word (Word64) import GHC.Generics (Generic) import NoThunks.Class (NoThunks) import Numeric.Natural (Natural) -import Ouroboros.Consensus.Block (WithOrigin (NotOrigin)) +import Ouroboros.Consensus.Block import qualified Ouroboros.Consensus.HardFork.History as History import Ouroboros.Consensus.Protocol.Abstract import Ouroboros.Consensus.Protocol.Ledger.HotKey (HotKey) @@ -259,6 +257,18 @@ data PraosState c = PraosState } deriving (Generic, Show, Eq) +-- | Create the initial Praos state when starting from genesis. +genesisPraosState :: Nonce -> PraosState c +genesisPraosState initialNonce = PraosState { + praosStateLastSlot = Origin + , praosStateOCertCounters = Map.empty + , praosStateEvolvingNonce = initialNonce + , praosStateCandidateNonce = initialNonce + , praosStateEpochNonce = initialNonce + , praosStateLabNonce = NeutralNonce + , praosStateLastEpochBlockNonce = NeutralNonce + } + instance PraosCrypto c => NoThunks (PraosState c) instance PraosCrypto c => ToCBOR (PraosState c) where diff --git a/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/TPraos.hs b/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/TPraos.hs index 37a9475a8b..3c1e27c5bb 100644 --- a/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/TPraos.hs +++ b/ouroboros-consensus-protocol/src/ouroboros-consensus-protocol/Ouroboros/Consensus/Protocol/TPraos.hs @@ -25,6 +25,7 @@ module Ouroboros.Consensus.Protocol.TPraos ( , TPraosToSign (..) , TPraosValidateView , forgeTPraosFields + , genesisTPraosState , mkShelleyGlobals , mkTPraosParams -- * Crypto @@ -251,6 +252,17 @@ data TPraosState c = TPraosState { } deriving (Generic, Show, Eq) +-- | Create the initial TPraos state when starting from genesis. +genesisTPraosState :: SL.Nonce -> TPraosState c +genesisTPraosState initialNonce = TPraosState { + tpraosStateLastSlot = Origin + , tpraosStateChainDepState = + -- The second argument, the map of genesis delegates, is only used to + -- set the OCert counters; however, this is redundant because the OCERT + -- rule also handles the case when they are absent. + SL.initialChainDepState initialNonce Map.empty + } + instance SL.PraosCrypto c => NoThunks (TPraosState c) -- | Version 0 supported rollback, removed in #2575. diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Embed/Nary.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Embed/Nary.hs index 6ed0df1002..e5340a0258 100644 --- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Embed/Nary.hs +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Embed/Nary.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingVia #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -7,6 +8,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module Ouroboros.Consensus.HardFork.Combinator.Embed.Nary ( Inject (..) @@ -16,7 +18,9 @@ module Ouroboros.Consensus.HardFork.Combinator.Embed.Nary ( , injectNestedCtxt_ , injectQuery -- * Initial 'ExtLedgerState' + , Translate , injectInitialExtLedgerState + , mkInitialStateViaTranslation ) where import Data.Bifunctor (first) @@ -25,15 +29,13 @@ import Data.SOP.BasicFunctors import Data.SOP.Counting (Exactly (..)) import Data.SOP.Dict (Dict (..)) import Data.SOP.Index -import qualified Data.SOP.InPairs as InPairs import Data.SOP.Strict import Ouroboros.Consensus.Block -import Ouroboros.Consensus.Config import Ouroboros.Consensus.HardFork.Combinator +import Ouroboros.Consensus.HardFork.Combinator.State import qualified Ouroboros.Consensus.HardFork.Combinator.State as State import qualified Ouroboros.Consensus.HardFork.History as History -import Ouroboros.Consensus.HeaderValidation (AnnTip, HeaderState (..), - genesisHeaderState) +import Ouroboros.Consensus.HeaderValidation (AnnTip, HeaderState (..)) import Ouroboros.Consensus.Ledger.Extended (ExtLedgerState (..)) import Ouroboros.Consensus.Storage.Serialisation import Ouroboros.Consensus.TypeFamilyWrappers @@ -174,62 +176,36 @@ instance Inject ExtLedgerState where Initial ExtLedgerState -------------------------------------------------------------------------------} --- | Inject the first era's initial 'ExtLedgerState' and trigger any --- translations that should take place in the very first slot. --- --- Performs any hard forks scheduled via 'TriggerHardForkAtEpoch'. --- --- Note: we can translate across multiple eras when computing the initial ledger --- state, but we do not support translation across multiple eras in general; --- extending 'applyChainTick' to translate across more than one era is not --- problematic, but extending 'ledgerViewForecastAt' is a lot more subtle; see --- @forecastNotFinal@. +-- | Inject the genesis 'ExtLedgerState' of some era into an 'ExtLedgerState' +-- for a 'HardForkBlock'. All eras before @x@ (if any) are empty. injectInitialExtLedgerState :: - forall x xs. CanHardFork (x ': xs) - => TopLevelConfig (HardForkBlock (x ': xs)) - -> ExtLedgerState x - -> ExtLedgerState (HardForkBlock (x ': xs)) -injectInitialExtLedgerState cfg extLedgerState0 = - ExtLedgerState { - ledgerState = targetEraLedgerState - , headerState = targetEraHeaderState - } + forall xs. CanHardFork xs + => NS ExtLedgerState xs + -> ExtLedgerState (HardForkBlock xs) +injectInitialExtLedgerState = + hcollapse + . himap (K .: inject initBounds) + where + initBounds :: Exactly xs History.Bound + initBounds = Exactly $ hpure $ K History.initBound + +type Translate f = CrossEra f Proxy f + +-- | Translate the given @f x@ until it has the same index as the n-ary sum. The +-- translations happen at 'History.initBound'. +mkInitialStateViaTranslation :: + InPairs (Translate f) (x : xs) + -> f x + -> NS g (x : xs) + -> NS f (x : xs) +mkInitialStateViaTranslation = go where - cfgs :: NP TopLevelConfig (x ': xs) - cfgs = - distribTopLevelConfig - (State.epochInfoLedger - (configLedger cfg) - (hardForkLedgerStatePerEra targetEraLedgerState)) - cfg - - targetEraLedgerState :: LedgerState (HardForkBlock (x ': xs)) - targetEraLedgerState = - HardForkLedgerState $ - -- We can immediately extend it to the right slot, executing any - -- scheduled hard forks in the first slot - State.extendToSlot - (configLedger cfg) - (SlotNo 0) - (initHardForkState (ledgerState extLedgerState0)) - - firstEraChainDepState :: HardForkChainDepState (x ': xs) - firstEraChainDepState = - initHardForkState $ - WrapChainDepState $ - headerStateChainDep $ - headerState extLedgerState0 - - targetEraChainDepState :: HardForkChainDepState (x ': xs) - targetEraChainDepState = - -- Align the 'ChainDepState' with the ledger state of the target era. - State.align - (InPairs.requiringBoth - (hmap (WrapConsensusConfig . configConsensus) cfgs) - (translateChainDepState hardForkEraTranslation)) - (hpure (fn_2 (\_ st -> st))) - (hardForkLedgerStatePerEra targetEraLedgerState) - firstEraChainDepState - - targetEraHeaderState :: HeaderState (HardForkBlock (x ': xs)) - targetEraHeaderState = genesisHeaderState targetEraChainDepState + go :: + InPairs (Translate f) (x : xs) + -> f x + -> NS g (x : xs) + -> NS f (x : xs) + go _ fx Z{} = Z fx + go (PCons t ts) fx (S gxs) = S $ go ts fx' gxs + where + fx' = crossEra t (Current History.initBound Proxy) fx diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Ledger.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Ledger.hs index aaa001f0b8..fb368663e0 100644 --- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Ledger.hs +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Ledger.hs @@ -37,11 +37,12 @@ import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Counting (getExactly) import Data.SOP.Index -import Data.SOP.InPairs (InPairs (..)) +import Data.SOP.InPairs (InPairs (..), Requiring (..), + RequiringBoth' (..)) import qualified Data.SOP.InPairs as InPairs import qualified Data.SOP.Match as Match import Data.SOP.Strict -import Data.SOP.Telescope (Telescope (..)) +import Data.SOP.Telescope (Extend (..), Telescope (..)) import qualified Data.SOP.Telescope as Telescope import GHC.Generics (Generic) import NoThunks.Class (NoThunks (..)) @@ -58,6 +59,7 @@ import Ouroboros.Consensus.HardFork.Combinator.PartialConfig import Ouroboros.Consensus.HardFork.Combinator.Protocol () import Ouroboros.Consensus.HardFork.Combinator.Protocol.LedgerView import qualified Ouroboros.Consensus.HardFork.Combinator.State as State +import qualified Ouroboros.Consensus.HardFork.Combinator.State.Lift as State import Ouroboros.Consensus.HardFork.Combinator.State.Types import Ouroboros.Consensus.HardFork.Combinator.Translation import Ouroboros.Consensus.HardFork.History (Bound (..), EraParams, @@ -68,6 +70,7 @@ import Ouroboros.Consensus.Ledger.Abstract import Ouroboros.Consensus.Ledger.Inspect import Ouroboros.Consensus.Ledger.SupportsProtocol import Ouroboros.Consensus.TypeFamilyWrappers +import Ouroboros.Consensus.Util ((.:)) import Ouroboros.Consensus.Util.Condense {------------------------------------------------------------------------------- @@ -117,53 +120,110 @@ instance CanHardFork xs => IsLedger (LedgerState (HardForkBlock xs)) where type AuxLedgerEvent (LedgerState (HardForkBlock xs)) = OneEraLedgerEvent xs - applyChainTickLedgerResult cfg@HardForkLedgerConfig{..} slot (HardForkLedgerState st) = - sequenceHardForkState - (hcizipWith proxySingle (tickOne ei slot) cfgs extended) <&> \l' -> + applyChainTickLedgerResult cfg slot lst@(HardForkLedgerState st) = + ticked <&> \st' -> TickedHardForkLedgerState { tickedHardForkLedgerStateTransition = - -- We are bundling a 'TransitionInfo' with a /ticked/ ledger state, - -- but /derive/ that 'TransitionInfo' from the /unticked/ (albeit - -- extended) state. That requires justification. Three cases: - -- - -- o 'TransitionUnknown'. If the transition is unknown, then it - -- cannot become known due to ticking. In this case, we record - -- the tip of the ledger, which ticking also does not modify - -- (this is an explicit postcondition of 'applyChainTick'). - -- o 'TransitionKnown'. If the transition to the next epoch is - -- already known, then ticking does not change that information. - -- It can't be the case that the 'SlotNo' we're ticking to is - -- /in/ that next era, because if was, then 'extendToSlot' would - -- have extended the telescope further. - -- (This does mean however that it is important to use the - -- /extended/ ledger state, not the original, to determine the - -- 'TransitionInfo'.) - -- o 'TransitionImpossible'. This has two subcases: either we are - -- in the final era, in which case ticking certainly won't be able - -- to change that, or we're forecasting, which is simply not - -- applicable here. - State.mostRecentTransitionInfo cfg extended - , tickedHardForkLedgerStatePerEra = l' + -- TODO justify + case State.match (State.tip st) st' of + -- TODO Previously, this might have been 'TransitionKnown' if the + -- next era uses 'TriggerHardForkAtEpoch'. It /seems/ + -- inconsequential that we know a bit less here. + Left _ -> TransitionUnknown (ledgerTipSlot lst) + Right _ -> State.mostRecentTransitionInfo cfg st + , tickedHardForkLedgerStatePerEra = st' } where - cfgs = getPerEraLedgerConfig hardForkLedgerConfigPerEra - ei = State.epochInfoLedger cfg st - - extended :: HardForkState LedgerState xs - extended = State.extendToSlot cfg slot st - -tickOne :: SingleEraBlock blk - => EpochInfo (Except PastHorizonException) - -> SlotNo - -> Index xs blk - -> WrapPartialLedgerConfig blk - -> LedgerState blk - -> ( LedgerResult (LedgerState (HardForkBlock xs)) - :.: (Ticked :.: LedgerState) - ) blk -tickOne ei slot index pcfg st = Comp $ fmap Comp $ - embedLedgerResult (injectLedgerEvent index) - $ applyChainTickLedgerResult (completeLedgerConfig' ei pcfg) slot st + ticked :: HardForkLedgerResult xs (HardForkState (Ticked :.: LedgerState) xs) + ticked = tick cfg slot st + +type HardForkLedgerResult xs = LedgerResult (LedgerState (HardForkBlock xs)) + +tick :: + forall xs. CanHardFork xs + => HardForkLedgerConfig xs + -> SlotNo + -> HardForkState LedgerState xs + -> HardForkLedgerResult xs (HardForkState (Ticked :.: LedgerState) xs) +tick ledgerCfg@HardForkLedgerConfig{..} slot ledgerSt@(HardForkState st) = + sequenceHardForkState + . HardForkState + . unI + . Telescope.extend + (hczipWith + proxySingle + (fn .: whenExtend) + pcfgs + (getExactly (History.getShape hardForkLedgerConfigShape))) + ( InPairs.requiringBoth indices + $ InPairs.hmap (\f -> RequireBoth $ \_ ix + -> Require $ \(K t) + -> Extend $ \cur + -> I $ tickCross f ix t cur) + $ InPairs.requiringBoth cfgs + $ crossEraTickLedgerState hardForkEraTranslation + ) + (hcimap proxySingle ((fn . State.lift) .: tickOne) cfgs) + $ st + where + pcfgs = getPerEraLedgerConfig hardForkLedgerConfigPerEra + cfgs = hcmap proxySingle (completeLedgerConfig'' ei) pcfgs + ei = State.epochInfoLedger ledgerCfg ledgerSt + + -- Return the end of this era if we should transition to the next + whenExtend :: SingleEraBlock blk + => WrapPartialLedgerConfig blk + -> K History.EraParams blk + -> Current LedgerState blk + -> (Maybe :.: K History.Bound) blk + whenExtend pcfg (K eraParams) cur = Comp $ K <$> do + transition <- singleEraTransition' + pcfg + eraParams + (currentStart cur) + (currentState cur) + let endBound = History.mkUpperBound + eraParams + (currentStart cur) + transition + guard (slot >= History.boundSlot endBound) + return endBound + + tickCross :: + CrossEraTickLedgerState blk blk' + -> Index xs blk' + -> History.Bound + -> Current LedgerState blk + -> ( K Past blk + , Current (HardForkLedgerResult xs :.: Ticked :.: LedgerState) blk' + ) + tickCross f index currentEnd cur = ( + K Past { + pastStart = currentStart cur + , pastEnd = currentEnd + } + , Current { + currentStart = currentEnd + , currentState = + Comp $ fmap Comp + $ embedLedgerResult (injectLedgerEvent index) + $ crossEraTickLedgerStateWith f + currentEnd + slot + (currentState cur) + } + ) + + tickOne :: + SingleEraBlock blk + => Index xs blk + -> WrapLedgerConfig blk + -> LedgerState blk + -> (HardForkLedgerResult xs :.: (Ticked :.: LedgerState)) blk + tickOne index (WrapLedgerConfig cfg) = + Comp . fmap Comp + . embedLedgerResult (injectLedgerEvent index) + . applyChainTickLedgerResult cfg slot {------------------------------------------------------------------------------- ApplyBlock diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Protocol.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Protocol.hs index bdbcb9960d..472e49be15 100644 --- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Protocol.hs +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Protocol.hs @@ -50,10 +50,11 @@ import Ouroboros.Consensus.HardFork.Combinator.PartialConfig import Ouroboros.Consensus.HardFork.Combinator.Protocol.ChainSel import Ouroboros.Consensus.HardFork.Combinator.Protocol.LedgerView (HardForkLedgerView, HardForkLedgerView_ (..)) -import Ouroboros.Consensus.HardFork.Combinator.State (HardForkState, - Translate (..)) +import Ouroboros.Consensus.HardFork.Combinator.State (CrossEra (..), + CrossEraTickChainDepState (..), Current (..), + HardForkState) import qualified Ouroboros.Consensus.HardFork.Combinator.State as State -import Ouroboros.Consensus.HardFork.Combinator.Translation as HFTranslation +import qualified Ouroboros.Consensus.HardFork.Combinator.Translation as HFTranslation import Ouroboros.Consensus.Protocol.Abstract import Ouroboros.Consensus.TypeFamilyWrappers import Ouroboros.Consensus.Util ((.:)) @@ -181,7 +182,7 @@ tick cfg@HardForkConsensusConfig{..} tickedHardForkChainDepStateEpochInfo = ei , tickedHardForkChainDepStatePerEra = State.align - (translateConsensus ei cfg) + (crossEraTickChainDepState ei cfg slot) (hcmap proxySingle (fn_2 . tickOne) cfgs) ledgerView chainDepState @@ -367,13 +368,25 @@ chainDepStateInfo :: forall blk. SingleEraBlock blk => (Ticked :.: WrapChainDepState) blk -> SingleEraInfo blk chainDepStateInfo _ = singleEraInfo (Proxy @blk) -translateConsensus :: forall xs. CanHardFork xs - => EpochInfo (Except PastHorizonException) - -> ConsensusConfig (HardForkProtocol xs) - -> InPairs (Translate WrapChainDepState) xs -translateConsensus ei HardForkConsensusConfig{..} = - InPairs.requiringBoth cfgs $ - HFTranslation.translateChainDepState hardForkEraTranslation +type CrossEraTickChainDepState' = + CrossEra + WrapChainDepState + WrapLedgerView + (Ticked :.: WrapChainDepState) + +crossEraTickChainDepState :: + forall xs. CanHardFork xs + => EpochInfo (Except PastHorizonException) + -> ConsensusConfig (HardForkProtocol xs) + -> SlotNo + -> InPairs CrossEraTickChainDepState' xs +crossEraTickChainDepState ei HardForkConsensusConfig{..} slot = + InPairs.hmap (\(CrossEraTickChainDepState f) -> + CrossEra $ \(Current start view) cds -> + Comp $ WrapTickedChainDepState $ + f start (unwrapLedgerView view) slot (unwrapChainDepState cds)) + $ InPairs.requiringBoth cfgs + $ HFTranslation.crossEraTickChainDepState hardForkEraTranslation where pcfgs = getPerEraConsensusConfig hardForkConsensusConfigPerEra cfgs = hcmap proxySingle (completeConsensusConfig'' ei) pcfgs diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State.hs index a4fc808490..3f2ffe47d0 100644 --- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State.hs +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State.hs @@ -6,7 +6,6 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -- | Intended for qualified import @@ -24,20 +23,16 @@ module Ouroboros.Consensus.HardFork.Combinator.State ( , epochInfoPrecomputedTransitionInfo , mostRecentTransitionInfo , reconstructSummaryLedger - -- * Ledger specific functionality - , extendToSlot ) where -import Control.Monad (guard) import Data.Functor.Product import Data.Proxy import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Counting (getExactly) -import Data.SOP.InPairs (InPairs, Requiring (..)) import qualified Data.SOP.InPairs as InPairs import Data.SOP.Strict -import Data.SOP.Telescope (Extend (..), ScanNext (..), Telescope) +import Data.SOP.Telescope (ScanNext (..), Telescope) import qualified Data.SOP.Telescope as Telescope import Ouroboros.Consensus.Block import Ouroboros.Consensus.HardFork.Combinator.Abstract @@ -47,10 +42,8 @@ import Ouroboros.Consensus.HardFork.Combinator.PartialConfig import Ouroboros.Consensus.HardFork.Combinator.State.Infra as X import Ouroboros.Consensus.HardFork.Combinator.State.Instances as X () import Ouroboros.Consensus.HardFork.Combinator.State.Types as X -import Ouroboros.Consensus.HardFork.Combinator.Translation import qualified Ouroboros.Consensus.HardFork.History as History import Ouroboros.Consensus.Ledger.Abstract hiding (getTip) -import Ouroboros.Consensus.Util ((.:)) import Prelude hiding (sequence) {------------------------------------------------------------------------------- @@ -163,71 +156,3 @@ epochInfoPrecomputedTransitionInfo :: epochInfoPrecomputedTransitionInfo shape transition st = History.summaryToEpochInfo $ reconstructSummary shape transition st - -{------------------------------------------------------------------------------- - Extending --------------------------------------------------------------------------------} - --- | Extend the telescope until the specified slot is within the era at the tip -extendToSlot :: forall xs. CanHardFork xs - => HardForkLedgerConfig xs - -> SlotNo - -> HardForkState LedgerState xs -> HardForkState LedgerState xs -extendToSlot ledgerCfg@HardForkLedgerConfig{..} slot ledgerSt@(HardForkState st) = - HardForkState . unI - . Telescope.extend - ( InPairs.hmap (\f -> Require $ \(K t) - -> Extend $ \cur - -> I $ howExtend f t cur) - $ translate - ) - (hczipWith - proxySingle - (fn .: whenExtend) - pcfgs - (getExactly (History.getShape hardForkLedgerConfigShape))) - $ st - where - pcfgs = getPerEraLedgerConfig hardForkLedgerConfigPerEra - cfgs = hcmap proxySingle (completeLedgerConfig'' ei) pcfgs - ei = epochInfoLedger ledgerCfg ledgerSt - - -- Return the end of this era if we should transition to the next - whenExtend :: SingleEraBlock blk - => WrapPartialLedgerConfig blk - -> K History.EraParams blk - -> Current LedgerState blk - -> (Maybe :.: K History.Bound) blk - whenExtend pcfg (K eraParams) cur = Comp $ K <$> do - transition <- singleEraTransition' - pcfg - eraParams - (currentStart cur) - (currentState cur) - let endBound = History.mkUpperBound - eraParams - (currentStart cur) - transition - guard (slot >= History.boundSlot endBound) - return endBound - - howExtend :: Translate LedgerState blk blk' - -> History.Bound - -> Current LedgerState blk - -> (K Past blk, Current LedgerState blk') - howExtend f currentEnd cur = ( - K Past { - pastStart = currentStart cur - , pastEnd = currentEnd - } - , Current { - currentStart = currentEnd - , currentState = translateWith f - (History.boundEpoch currentEnd) - (currentState cur) - } - ) - - translate :: InPairs (Translate LedgerState) xs - translate = InPairs.requiringBoth cfgs $ - translateLedgerState hardForkEraTranslation diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Infra.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Infra.hs index b9a7d09d22..0acd6ba704 100644 --- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Infra.hs +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Infra.hs @@ -19,7 +19,7 @@ module Ouroboros.Consensus.HardFork.Combinator.State.Infra ( -- * Situated , Situated (..) , situate - -- * Aligning + -- * Extend and align , align -- * EpochInfo/Summary , reconstructSummary @@ -29,7 +29,7 @@ import Data.Functor.Product import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Counting -import Data.SOP.InPairs (InPairs, Requiring (..)) +import Data.SOP.InPairs (InPairs, RequiringBoth' (..)) import qualified Data.SOP.InPairs as InPairs import Data.SOP.Match (Mismatch) import qualified Data.SOP.Match as Match @@ -38,12 +38,12 @@ import Data.SOP.Strict import Data.SOP.Telescope (Extend (..), Telescope (..)) import qualified Data.SOP.Telescope as Telescope import Ouroboros.Consensus.Block -import Ouroboros.Consensus.HardFork.Combinator.Abstract.SingleEraBlock import Ouroboros.Consensus.HardFork.Combinator.State.Lift import Ouroboros.Consensus.HardFork.Combinator.State.Types import Ouroboros.Consensus.HardFork.History (Bound (..), EraEnd (..), EraParams (..), EraSummary (..), SafeZone (..)) import qualified Ouroboros.Consensus.HardFork.History as History +import Ouroboros.Consensus.Util.CallStack import Prelude hiding (sequence) {------------------------------------------------------------------------------- @@ -114,19 +114,28 @@ situate ns = go ns . getHardForkState Aligning -------------------------------------------------------------------------------} -align :: forall xs f f' f''. All SingleEraBlock xs - => InPairs (Translate f) xs - -> NP (f' -.-> f -.-> f'') xs - -> HardForkState f' xs -- ^ State we are aligning with - -> HardForkState f xs -- ^ State we are aligning - -> HardForkState f'' xs -align fs updTip (HardForkState alignWith) (HardForkState toAlign) = +-- TODO docs +align :: + forall f f' f'' xs. (SListI xs, HasCallStack) + => InPairs (CrossEra f f' f'') xs + -- ^ How to cross the era boundary. + -> NP (f' -.-> f -.-> f'') xs + -- ^ What to do if the states are already in the same era. + -> HardForkState f' xs + -- ^ State we are aligning with. + -> HardForkState f xs + -- ^ State we are aligning. Must be exactly one era ahead if not already + -- aligned. + -> HardForkState f'' xs + -- ^ In the same era as the state we are aligning with, and therefore + -- either in the same era or one era ahead as the to-be-aligned state. +align cross updTip (HardForkState alignWith) (HardForkState toAlign) = HardForkState . unI $ - Telescope.alignExtend - (InPairs.hmap (\f -> Require $ - \past -> Extend $ - \cur -> I $ - newCurrent f past cur) fs) + Telescope.align + (InPairs.hmap (\(CrossEra f) -> RequireBoth $ + \past newEra -> Extend $ + \(Current _ cur) -> I $ + (past, newEra { currentState = f newEra cur })) cross) (hmap (fn_2 . liftUpdTip) updTip) alignWith toAlign @@ -135,24 +144,6 @@ align fs updTip (HardForkState alignWith) (HardForkState toAlign) = -> Current f' blk -> Current f blk -> Current f'' blk liftUpdTip f = lift . apFn . apFn f . currentState - newCurrent :: Translate f blk blk' - -> K Past blk - -> Current f blk - -> (K Past blk, Current f blk') - newCurrent f (K past) curF = ( - K Past { pastStart = currentStart curF - , pastEnd = curEnd - } - , Current { currentStart = curEnd - , currentState = translateWith f - (boundEpoch curEnd) - (currentState curF) - } - ) - where - curEnd :: Bound - curEnd = pastEnd past - {------------------------------------------------------------------------------- Summary/EpochInfo -------------------------------------------------------------------------------} diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Types.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Types.hs index 8821d1af08..ef46039173 100644 --- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Types.hs +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/State/Types.hs @@ -11,9 +11,11 @@ module Ouroboros.Consensus.HardFork.Combinator.State.Types ( , Past (..) , sequenceHardForkState -- * Supporting types + , CrossEra (..) , CrossEraForecaster (..) + , CrossEraTickChainDepState (..) + , CrossEraTickLedgerState (..) , TransitionInfo (..) - , Translate (..) ) where import Control.Monad.Except @@ -27,6 +29,9 @@ import NoThunks.Class (NoThunks (..)) import Ouroboros.Consensus.Block import Ouroboros.Consensus.Forecast import Ouroboros.Consensus.HardFork.History (Bound) +import Ouroboros.Consensus.Ledger.Abstract +import Ouroboros.Consensus.Protocol.Abstract +import Ouroboros.Consensus.Ticked import Prelude {------------------------------------------------------------------------------- @@ -108,11 +113,30 @@ sequenceHardForkState (HardForkState tel) = Supporting types -------------------------------------------------------------------------------} --- | Translate @f x@ to @f y@ across an era transition --- --- Typically @f@ will be 'LedgerState' or 'WrapChainDepState'. -newtype Translate f x y = Translate { - translateWith :: EpochNo -> f x -> f y +newtype CrossEra f f' f'' x y = CrossEra { + crossEra :: + Current f' y -- State that already is in the new era + -> f x -- State in the old era + -> f'' y -- State to compute for the new era + } + +-- TODO docs +newtype CrossEraTickLedgerState x y = CrossEraTickLedgerState { + crossEraTickLedgerStateWith :: + Bound -- 'Bound' of the transition (start of the new era) + -> SlotNo -- 'SlotNo' we are ticking to + -> LedgerState x + -> LedgerResult (LedgerState y) (TickedLedgerState y) + } + +-- TODO docs +newtype CrossEraTickChainDepState x y = CrossEraTickChainDepState { + crossEraTickChainDepStateWith :: + Bound -- 'Bound' of the transition (start of the new era) + -> LedgerView (BlockProtocol y) + -> SlotNo -- 'SlotNo' we are ticking to + -> ChainDepState (BlockProtocol x) + -> Ticked (ChainDepState (BlockProtocol y)) } -- | Forecast a @view y@ from a @state x@ across an era transition. diff --git a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Translation.hs b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Translation.hs index 1528b9a578..3b74d150b1 100644 --- a/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Translation.hs +++ b/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/HardFork/Combinator/Translation.hs @@ -7,7 +7,7 @@ module Ouroboros.Consensus.HardFork.Combinator.Translation ( , trivialEraTranslation ) where -import Data.SOP.InPairs (InPairs (..), RequiringBoth (..)) +import Data.SOP.InPairs (InPairs (..), RequiringBoth) import NoThunks.Class (NoThunks, OnlyCheckWhnfNamed (..)) import Ouroboros.Consensus.HardFork.Combinator.State.Types import Ouroboros.Consensus.Ledger.Abstract @@ -17,16 +17,19 @@ import Ouroboros.Consensus.TypeFamilyWrappers -------------------------------------------------------------------------------} data EraTranslation xs = EraTranslation { - translateLedgerState :: InPairs (RequiringBoth WrapLedgerConfig (Translate LedgerState)) xs - , translateChainDepState :: InPairs (RequiringBoth WrapConsensusConfig (Translate WrapChainDepState)) xs - , crossEraForecast :: InPairs (RequiringBoth WrapLedgerConfig (CrossEraForecaster LedgerState WrapLedgerView)) xs + crossEraTickLedgerState :: + InPairs (RequiringBoth WrapLedgerConfig CrossEraTickLedgerState) xs + , crossEraTickChainDepState :: + InPairs (RequiringBoth WrapConsensusConfig CrossEraTickChainDepState) xs + , crossEraForecast :: + InPairs (RequiringBoth WrapLedgerConfig (CrossEraForecaster LedgerState WrapLedgerView)) xs } deriving NoThunks via OnlyCheckWhnfNamed "EraTranslation" (EraTranslation xs) trivialEraTranslation :: EraTranslation '[blk] trivialEraTranslation = EraTranslation { - translateLedgerState = PNil - , crossEraForecast = PNil - , translateChainDepState = PNil + crossEraTickLedgerState = PNil + , crossEraTickChainDepState = PNil + , crossEraForecast = PNil } diff --git a/sop-extras/src/Data/SOP/InPairs.hs b/sop-extras/src/Data/SOP/InPairs.hs index f00eff6f19..04c7c49c0a 100644 --- a/sop-extras/src/Data/SOP/InPairs.hs +++ b/sop-extras/src/Data/SOP/InPairs.hs @@ -28,7 +28,8 @@ module Data.SOP.InPairs ( , hpure -- * Requiring , Requiring (..) - , RequiringBoth (..) + , RequiringBoth + , RequiringBoth' (..) , ignoring , ignoringBoth , requiring @@ -117,14 +118,16 @@ newtype Requiring h f x y = Require { provide :: h x -> f x y } -newtype RequiringBoth h f x y = RequireBoth { - provideBoth :: h x -> h y -> f x y +newtype RequiringBoth' h h' f x y = RequireBoth { + provideBoth :: h x -> h' y -> f x y } +type RequiringBoth h = RequiringBoth' h h + ignoring :: f x y -> Requiring h f x y ignoring fxy = Require $ const fxy -ignoringBoth :: f x y -> RequiringBoth h f x y +ignoringBoth :: f x y -> RequiringBoth' h h' f x y ignoringBoth fxy = RequireBoth $ \_ _ -> fxy requiring :: SListI xs => NP h xs -> InPairs (Requiring h f) xs -> InPairs f xs diff --git a/sop-extras/src/Data/SOP/Telescope.hs b/sop-extras/src/Data/SOP/Telescope.hs index 74695de94a..9e49ca65f0 100644 --- a/sop-extras/src/Data/SOP/Telescope.hs +++ b/sop-extras/src/Data/SOP/Telescope.hs @@ -35,17 +35,10 @@ module Data.SOP.Telescope ( , bihczipWith , bihmap , bihzipWith - -- * Extension, retraction, alignment + -- * Extension and alignment , Extend (..) - , Retract (..) , align , extend - , retract - -- ** Simplified API - , alignExtend - , alignExtendNS - , extendIf - , retractIf -- * Additional API , ScanNext (..) , SimpleTelescope (..) @@ -59,11 +52,9 @@ import Data.Proxy import Data.SOP.BasicFunctors import Data.SOP.Constraint import Data.SOP.Counting -import Data.SOP.InPairs (InPairs (..), Requiring (..)) -import qualified Data.SOP.InPairs as InPairs +import Data.SOP.InPairs (InPairs (..), Requiring (..), + RequiringBoth' (..)) import Data.SOP.Strict -import Data.SOP.Tails (Tails (..)) -import qualified Data.SOP.Tails as Tails import GHC.Stack import NoThunks.Class (NoThunks (..), allNoThunks) import Prelude hiding (scanl, sequence, zipWith) @@ -299,151 +290,66 @@ fromTZ :: Telescope g f '[x] -> f x fromTZ (TZ fx) = fx {------------------------------------------------------------------------------- - Extension and retraction + Extension and alignment -------------------------------------------------------------------------------} -newtype Extend m g f x y = Extend { extendWith :: f x -> m (g x, f y) } +newtype Extend m g f f' x y = Extend { extendWith :: f x -> m (g x, f' y) } --- | Extend the telescope +-- | Extend the telescope by at most one segment. -- -- We will not attempt to extend the telescope past its final segment. -extend :: forall m h g f xs. Monad m - => InPairs (Requiring h (Extend m g f)) xs -- ^ How to extend - -> NP (f -.-> Maybe :.: h) xs -- ^ Where to extend /from/ - -> Telescope g f xs -> m (Telescope g f xs) +extend :: + forall m g h f f' xs. Monad m + => NP (f -.-> Maybe :.: h) xs -- ^ Whether to extend + -> InPairs (Requiring h (Extend m g f f')) xs -- ^ How to extend + -> NP (f -.-> f') xs -- ^ How not to extend + -> Telescope g f xs -> m (Telescope g f' xs) extend = go where - go :: InPairs (Requiring h (Extend m g f)) xs' - -> NP (f -.-> Maybe :.: h) xs' - -> Telescope g f xs' -> m (Telescope g f xs') - go PNil _ (TZ fx) = - return (TZ fx) - go (PCons e es) (p :* ps) (TZ fx) = - case unComp $ apFn p fx of - Nothing -> - return (TZ fx) - Just hx -> do - (gx, fy) <- extendWith (provide e hx) fx - TS gx <$> go es ps (TZ fy) - go (PCons _ es) (_ :* ps) (TS gx fx) = - TS gx <$> go es ps fx - -newtype Retract m g f x y = Retract { retractWith :: g x -> f y -> m (f x) } - --- | Retract a telescope -retract :: forall m h g f xs. Monad m - => Tails (Requiring h (Retract m g f)) xs -- ^ How to retract - -> NP (g -.-> Maybe :.: h) xs -- ^ Where to retract /to/ - -> Telescope g f xs -> m (Telescope g f xs) -retract = - \tails np -> - npToSListI np $ go tails np - where - go :: SListI xs' - => Tails (Requiring h (Retract m g f)) xs' - -> NP (g -.-> Maybe :.: h) xs' - -> Telescope g f xs' -> m (Telescope g f xs') - go _ _ (TZ fx) = return $ TZ fx - go (TCons r rs) (p :* ps) (TS gx t) = - case unComp (apFn p gx) of - Just hx -> - fmap (TZ . hcollapse) $ hsequence' $ - hzipWith (retractAux hx gx) r (tip t) - Nothing -> - TS gx <$> go rs ps t - --- | Internal auxiliary to 'retract' and 'alignWith' -retractAux :: Functor m - => h x -- Proof that we need to retract - -> g x -- Era we are retracting to - -> Requiring h (Retract m g f) x z - -> f z -- Current tip (what we are retracting from) - -> (m :.: K (f x)) z -retractAux hx gx r fz = Comp $ K <$> retractWith (provide r hx) gx fz - --- | Align a telescope with another, then apply a function to the tips --- --- Aligning is a combination of extension and retraction, extending or --- retracting the telescope as required to match up with the other telescope. -align :: forall m g' g f' f f'' xs. Monad m - => InPairs (Requiring g' (Extend m g f)) xs -- ^ How to extend - -> Tails (Requiring f' (Retract m g f)) xs -- ^ How to retract - -> NP (f' -.-> f -.-> f'') xs -- ^ Function to apply at the tip - -> Telescope g' f' xs -- ^ Telescope we are aligning with - -> Telescope g f xs -> m (Telescope g f'' xs) -align = \es rs atTip -> - npToSListI atTip $ go es rs atTip - where - go :: SListI xs' - => InPairs (Requiring g' (Extend m g f)) xs' - -> Tails (Requiring f' (Retract m g f)) xs' - -> NP (f' -.-> f -.-> f'') xs' - -> Telescope g' f' xs' -> Telescope g f xs' -> m (Telescope g f'' xs') - go _ _ (f :* _) (TZ f'x) (TZ fx) = - return $ TZ (f `apFn` f'x `apFn` fx) - go (PCons _ es) (TCons _ rs) (_ :* fs) (TS _ f'x) (TS gx fx) = - TS gx <$> go es rs fs f'x fx - go _ (TCons r _) (f :* _) (TZ f'x) (TS gx fx) = - fmap (TZ . (\fx' -> f `apFn` f'x `apFn` fx') . hcollapse) $ hsequence' $ - hzipWith (retractAux f'x gx) r (tip fx) - go (PCons e es) (TCons _ rs) (_ :* fs) (TS g'x t'x) (TZ fx) = do - (gx, fy) <- extendWith (provide e g'x) fx - TS gx <$> go es rs fs t'x (TZ fy) - -{------------------------------------------------------------------------------- - Derived API --------------------------------------------------------------------------------} - --- | Version of 'extend' where the evidence is a simple 'Bool' -extendIf :: Monad m - => InPairs (Extend m g f) xs -- ^ How to extend - -> NP (f -.-> K Bool) xs -- ^ Where to extend /from/ - -> Telescope g f xs -> m (Telescope g f xs) -extendIf es ps = npToSListI ps $ - extend - (InPairs.hmap (Require . const) es) - (hmap (\f -> fn $ fromBool . apFn f) ps) - --- | Version of 'retract' where the evidence is a simple 'Bool' -retractIf :: Monad m - => Tails (Retract m g f) xs -- ^ How to retract - -> NP (g -.-> K Bool) xs -- ^ Where to retract /to/ - -> Telescope g f xs -> m (Telescope g f xs) -retractIf rs ps = npToSListI ps $ - retract - (Tails.hmap (Require . const) rs) - (hmap (\f -> fn $ fromBool . apFn f) ps) - --- | Version of 'align' that never retracts, only extends + go :: + NP (f -.-> Maybe :.: h) xs' + -> InPairs (Requiring h (Extend m g f f')) xs' + -> NP (f -.-> f') xs' + -> Telescope g f xs' -> m (Telescope g f' xs') + go _ PNil (ne :* _) (TZ fx) = + pure (TZ (apFn ne fx)) + go (c :* _) (PCons e _) (ne :* _) (TZ fx) = + case unComp $ apFn c fx of + Nothing -> pure $ TZ $ apFn ne fx + Just hx -> do + (gx, f'y) <- extendWith (provide e hx) fx + pure $ TS gx $ TZ f'y + go (_ :* cs) (PCons _ es) (_ :* nes) (TS gx fys) = + TS gx <$> go cs es nes fys + +-- | Align the telescope with another by at most one segment. -- --- PRE: The telescope we are aligning with cannot be behind us. -alignExtend :: (Monad m, HasCallStack) - => InPairs (Requiring g' (Extend m g f)) xs -- ^ How to extend - -> NP (f' -.-> f -.-> f'') xs -- ^ Function to apply at the tip - -> Telescope g' f' xs -- ^ Telescope we are aligning with - -> Telescope g f xs -> m (Telescope g f'' xs) -alignExtend es atTip = npToSListI atTip $ - align es (Tails.hpure $ Require $ \_ -> error precondition) atTip +-- PRE: The telescope we are aligning with is in the same segment or one segment +-- ahead. +align :: + forall m g g' f f' f'' xs. (Monad m, HasCallStack) + => InPairs (RequiringBoth' g' f' (Extend m g f f'')) xs -- ^ How to extend + -> NP (f' -.-> f -.-> f'') xs -- ^ Function to apply at the tip + -> Telescope g' f' xs -- ^ Telescope we are aligning with + -> Telescope g f xs -> m (Telescope g f'' xs) +align = go where - precondition :: String - precondition = "alignExtend: precondition violated" - --- | Version of 'alignExtend' that extends with an NS instead -alignExtendNS :: (Monad m, HasCallStack) - => InPairs (Extend m g f) xs -- ^ How to extend - -> NP (f' -.-> f -.-> f'') xs -- ^ Function to apply at the tip - -> NS f' xs -- ^ NS we are aligning with - -> Telescope g f xs -> m (Telescope g f'' xs) -alignExtendNS es atTip ns = npToSListI atTip $ - alignExtend - (InPairs.hmap (Require . const) es) - atTip - (fromTip ns) - --- | Internal auxiliary to 'extendIf' and 'retractIf' -fromBool :: K Bool x -> (Maybe :.: K ()) x -fromBool (K True) = Comp $ Just $ K () -fromBool (K False) = Comp Nothing + go :: + InPairs (RequiringBoth' g' f' (Extend m g f f'')) xs' + -> NP (f' -.-> f -.-> f'') xs' + -> Telescope g' f' xs' + -> Telescope g f xs' -> m (Telescope g f'' xs') + go _ (atTip :* _) (TZ f'x) (TZ fx) = + pure $ TZ (atTip `apFn` f'x `apFn` fx) + go (PCons e _) _ (TS g'x (TZ f'x)) (TZ fx) = do + (gx, f''y) <- extendWith (provideBoth e g'x f'x) fx + pure $ TS gx $ TZ f''y + go (PCons _ es) (_ :* atTips) (TS _ f'ys) (TS gx fys) = + TS gx <$> go es atTips f'ys fys + go _ _ TZ{} TS{} = + error "precondition: behind" + go _ _ (TS _ TS{}) TZ{} = + error "precondition: more than one ahead" {------------------------------------------------------------------------------- Additional API