-
Notifications
You must be signed in to change notification settings - Fork 20
/
Query.hs
402 lines (355 loc) · 14.5 KB
/
Query.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Ouroboros.Consensus.HardFork.Combinator.Ledger.Query (
BlockQuery (..)
, HardForkQueryResult
, QueryAnytime (..)
, QueryHardFork (..)
, QueryIfCurrent (..)
, decodeQueryAnytimeResult
, decodeQueryHardForkResult
, encodeQueryAnytimeResult
, encodeQueryHardForkResult
, getHardForkQuery
, hardForkQueryInfo
) where
import Cardano.Binary (enforceSize)
import Codec.CBOR.Decoding (Decoder)
import qualified Codec.CBOR.Decoding as Dec
import Codec.CBOR.Encoding (Encoding)
import qualified Codec.CBOR.Encoding as Enc
import Codec.Serialise (Serialise (..))
import Data.Bifunctor
import Data.Functor.Product
import Data.Kind (Type)
import Data.Proxy
import Data.SOP.BasicFunctors
import Data.SOP.Constraint
import Data.SOP.Counting (getExactly)
import Data.SOP.Match (Mismatch (..), mustMatchNS)
import Data.SOP.Strict
import Data.Type.Equality
import Data.Typeable (Typeable)
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.Config
import Ouroboros.Consensus.HardFork.Abstract (hardForkSummary)
import Ouroboros.Consensus.HardFork.Combinator.Abstract
import Ouroboros.Consensus.HardFork.Combinator.AcrossEras
import Ouroboros.Consensus.HardFork.Combinator.Basics
import Ouroboros.Consensus.HardFork.Combinator.Block
import Ouroboros.Consensus.HardFork.Combinator.Info
import Ouroboros.Consensus.HardFork.Combinator.Ledger ()
import Ouroboros.Consensus.HardFork.Combinator.PartialConfig
import Ouroboros.Consensus.HardFork.Combinator.State (Current (..),
Past (..), Situated (..))
import qualified Ouroboros.Consensus.HardFork.Combinator.State as State
import Ouroboros.Consensus.HardFork.History (Bound (..), EraParams,
Shape (..))
import qualified Ouroboros.Consensus.HardFork.History as History
import Ouroboros.Consensus.HeaderValidation
import Ouroboros.Consensus.Ledger.Extended
import Ouroboros.Consensus.Ledger.Query
import Ouroboros.Consensus.Node.Serialisation (Some (..))
import Ouroboros.Consensus.TypeFamilyWrappers (WrapChainDepState (..))
import Ouroboros.Consensus.Util (ShowProxy)
instance Typeable xs => ShowProxy (BlockQuery (HardForkBlock xs)) where
instance All SingleEraBlock xs => ShowQuery (BlockQuery (HardForkBlock xs)) where
showResult (QueryAnytime qry _) result = showResult qry result
showResult (QueryHardFork qry) result = showResult qry result
showResult (QueryIfCurrent qry) mResult =
case mResult of
Left err -> show err
Right result -> showResult qry result
type HardForkQueryResult xs = Either (MismatchEraInfo xs)
data instance BlockQuery (HardForkBlock xs) :: Type -> Type where
-- | Answer a query about an era if it is the current one.
QueryIfCurrent ::
QueryIfCurrent xs result
-> BlockQuery (HardForkBlock xs) (HardForkQueryResult xs result)
-- | Answer a query about an era from /any/ era.
--
-- NOTE: we don't allow this when there is only a single era, so that the
-- HFC applied to a single era is still isomorphic to the single era.
QueryAnytime ::
IsNonEmpty xs
=> QueryAnytime result
-> EraIndex (x ': xs)
-> BlockQuery (HardForkBlock (x ': xs)) result
-- | Answer a query about the hard fork combinator
--
-- NOTE: we don't allow this when there is only a single era, so that the
-- HFC applied to a single era is still isomorphic to the single era.
QueryHardFork ::
IsNonEmpty xs
=> QueryHardFork (x ': xs) result
-> BlockQuery (HardForkBlock (x ': xs)) result
instance All SingleEraBlock xs => BlockSupportsLedgerQuery (HardForkBlock xs) where
answerBlockQuery
(ExtLedgerCfg cfg)
query
ext@(ExtLedgerState st@(HardForkLedgerState hardForkState) _) =
case query of
QueryIfCurrent queryIfCurrent ->
interpretQueryIfCurrent
cfgs
queryIfCurrent
(distribExtLedgerState ext)
QueryAnytime queryAnytime (EraIndex era) ->
interpretQueryAnytime
lcfg
queryAnytime
(EraIndex era)
hardForkState
QueryHardFork queryHardFork ->
interpretQueryHardFork
lcfg
queryHardFork
st
where
cfgs = hmap ExtLedgerCfg $ distribTopLevelConfig ei cfg
lcfg = configLedger cfg
ei = State.epochInfoLedger lcfg hardForkState
-- | Precondition: the 'ledgerState' and 'headerState' should be from the same
-- era. In practice, this is _always_ the case, unless the 'ExtLedgerState' was
-- manually crafted.
distribExtLedgerState ::
All SingleEraBlock xs
=> ExtLedgerState (HardForkBlock xs) -> NS ExtLedgerState xs
distribExtLedgerState (ExtLedgerState ledgerState headerState) =
hmap (\(Pair hst lst) -> ExtLedgerState lst hst) $
mustMatchNS
"HeaderState"
(distribHeaderState headerState)
(State.tip (hardForkLedgerStatePerEra ledgerState))
-- | Precondition: the 'headerStateTip' and 'headerStateChainDep' should be from
-- the same era. In practice, this is _always_ the case, unless the
-- 'HeaderState' was manually crafted.
distribHeaderState ::
All SingleEraBlock xs
=> HeaderState (HardForkBlock xs) -> NS HeaderState xs
distribHeaderState (HeaderState tip chainDepState) =
case tip of
Origin ->
hmap (HeaderState Origin . unwrapChainDepState) (State.tip chainDepState)
NotOrigin annTip ->
hmap
(\(Pair t cds) -> HeaderState (NotOrigin t) (unwrapChainDepState cds))
(mustMatchNS "AnnTip" (distribAnnTip annTip) (State.tip chainDepState))
instance All SingleEraBlock xs => SameDepIndex (BlockQuery (HardForkBlock xs)) where
sameDepIndex (QueryIfCurrent qry) (QueryIfCurrent qry') =
apply Refl <$> sameDepIndex qry qry'
sameDepIndex (QueryIfCurrent {}) _ =
Nothing
sameDepIndex (QueryAnytime qry era) (QueryAnytime qry' era')
| era == era'
= sameDepIndex qry qry'
| otherwise
= Nothing
sameDepIndex (QueryAnytime {}) _ =
Nothing
sameDepIndex (QueryHardFork qry) (QueryHardFork qry') =
sameDepIndex qry qry'
sameDepIndex (QueryHardFork {}) _ =
Nothing
deriving instance All SingleEraBlock xs => Show (BlockQuery (HardForkBlock xs) result)
getHardForkQuery :: BlockQuery (HardForkBlock xs) result
-> (forall result'.
result :~: HardForkQueryResult xs result'
-> QueryIfCurrent xs result'
-> r)
-> (forall x' xs'.
xs :~: x' ': xs'
-> ProofNonEmpty xs'
-> QueryAnytime result
-> EraIndex xs
-> r)
-> (forall x' xs'.
xs :~: x' ': xs'
-> ProofNonEmpty xs'
-> QueryHardFork xs result
-> r)
-> r
getHardForkQuery q k1 k2 k3 = case q of
QueryIfCurrent qry -> k1 Refl qry
QueryAnytime qry era -> k2 Refl (isNonEmpty Proxy) qry era
QueryHardFork qry -> k3 Refl (isNonEmpty Proxy) qry
{-------------------------------------------------------------------------------
Current era queries
-------------------------------------------------------------------------------}
data QueryIfCurrent :: [Type] -> Type -> Type where
QZ :: BlockQuery x result -> QueryIfCurrent (x ': xs) result
QS :: QueryIfCurrent xs result -> QueryIfCurrent (x ': xs) result
deriving instance All SingleEraBlock xs => Show (QueryIfCurrent xs result)
instance All SingleEraBlock xs => ShowQuery (QueryIfCurrent xs) where
showResult (QZ qry) = showResult qry
showResult (QS qry) = showResult qry
instance All SingleEraBlock xs => SameDepIndex (QueryIfCurrent xs) where
sameDepIndex (QZ qry) (QZ qry') = sameDepIndex qry qry'
sameDepIndex (QS qry) (QS qry') = sameDepIndex qry qry'
sameDepIndex _ _ = Nothing
interpretQueryIfCurrent ::
forall result xs. All SingleEraBlock xs
=> NP ExtLedgerCfg xs
-> QueryIfCurrent xs result
-> NS ExtLedgerState xs
-> HardForkQueryResult xs result
interpretQueryIfCurrent = go
where
go :: All SingleEraBlock xs'
=> NP ExtLedgerCfg xs'
-> QueryIfCurrent xs' result
-> NS ExtLedgerState xs'
-> HardForkQueryResult xs' result
go (c :* _) (QZ qry) (Z st) =
Right $ answerBlockQuery c qry st
go (_ :* cs) (QS qry) (S st) =
first shiftMismatch $ go cs qry st
go _ (QZ qry) (S st) =
Left $ MismatchEraInfo $ ML (queryInfo qry) (hcmap proxySingle ledgerInfo st)
go _ (QS qry) (Z st) =
Left $ MismatchEraInfo $ MR (hardForkQueryInfo qry) (ledgerInfo st)
{-------------------------------------------------------------------------------
Any era queries
-------------------------------------------------------------------------------}
data QueryAnytime result where
GetEraStart :: QueryAnytime (Maybe Bound)
deriving instance Show (QueryAnytime result)
instance ShowQuery QueryAnytime where
showResult GetEraStart = show
instance SameDepIndex QueryAnytime where
sameDepIndex GetEraStart GetEraStart = Just Refl
interpretQueryAnytime ::
forall result xs. All SingleEraBlock xs
=> HardForkLedgerConfig xs
-> QueryAnytime result
-> EraIndex xs
-> State.HardForkState LedgerState xs
-> result
interpretQueryAnytime cfg query (EraIndex era) st =
answerQueryAnytime cfg query (State.situate era st)
answerQueryAnytime ::
All SingleEraBlock xs
=> HardForkLedgerConfig xs
-> QueryAnytime result
-> Situated h LedgerState xs
-> result
answerQueryAnytime HardForkLedgerConfig{..} =
go cfgs (getExactly (getShape hardForkLedgerConfigShape))
where
cfgs = getPerEraLedgerConfig hardForkLedgerConfigPerEra
go :: All SingleEraBlock xs'
=> NP WrapPartialLedgerConfig xs'
-> NP (K EraParams) xs'
-> QueryAnytime result
-> Situated h LedgerState xs'
-> result
go Nil _ _ ctxt = case ctxt of {}
go (c :* cs) (K ps :* pss) GetEraStart ctxt = case ctxt of
SituatedShift ctxt' -> go cs pss GetEraStart ctxt'
SituatedFuture _ _ -> Nothing
SituatedPast past _ -> Just $ pastStart $ unK past
SituatedCurrent cur _ -> Just $ currentStart cur
SituatedNext cur _ ->
History.mkUpperBound ps (currentStart cur) <$>
singleEraTransition
(unwrapPartialLedgerConfig c)
ps
(currentStart cur)
(currentState cur)
{-------------------------------------------------------------------------------
Hard fork queries
-------------------------------------------------------------------------------}
data QueryHardFork xs result where
GetInterpreter :: QueryHardFork xs (History.Interpreter xs)
GetCurrentEra :: QueryHardFork xs (EraIndex xs)
deriving instance Show (QueryHardFork xs result)
instance All SingleEraBlock xs => ShowQuery (QueryHardFork xs) where
showResult GetInterpreter = show
showResult GetCurrentEra = show
instance SameDepIndex (QueryHardFork xs) where
sameDepIndex GetInterpreter GetInterpreter =
Just Refl
sameDepIndex GetInterpreter _ =
Nothing
sameDepIndex GetCurrentEra GetCurrentEra =
Just Refl
sameDepIndex GetCurrentEra _ =
Nothing
interpretQueryHardFork ::
All SingleEraBlock xs
=> HardForkLedgerConfig xs
-> QueryHardFork xs result
-> LedgerState (HardForkBlock xs)
-> result
interpretQueryHardFork cfg query st =
case query of
GetInterpreter ->
History.mkInterpreter $ hardForkSummary cfg st
GetCurrentEra ->
eraIndexFromNS $ State.tip $ hardForkLedgerStatePerEra st
{-------------------------------------------------------------------------------
Serialisation
-------------------------------------------------------------------------------}
instance Serialise (Some QueryAnytime) where
encode (Some GetEraStart) = mconcat [
Enc.encodeListLen 1
, Enc.encodeWord8 0
]
decode = do
enforceSize "QueryAnytime" 1
tag <- Dec.decodeWord8
case tag of
0 -> return $ Some GetEraStart
_ -> fail $ "QueryAnytime: invalid tag " ++ show tag
encodeQueryAnytimeResult :: QueryAnytime result -> result -> Encoding
encodeQueryAnytimeResult GetEraStart = encode
decodeQueryAnytimeResult :: QueryAnytime result -> forall s. Decoder s result
decodeQueryAnytimeResult GetEraStart = decode
encodeQueryHardForkResult ::
SListI xs
=> QueryHardFork xs result -> result -> Encoding
encodeQueryHardForkResult = \case
GetInterpreter -> encode
GetCurrentEra -> encode
decodeQueryHardForkResult ::
SListI xs
=> QueryHardFork xs result -> forall s. Decoder s result
decodeQueryHardForkResult = \case
GetInterpreter -> decode
GetCurrentEra -> decode
{-------------------------------------------------------------------------------
Auxiliary
-------------------------------------------------------------------------------}
ledgerInfo :: forall blk. SingleEraBlock blk
=> ExtLedgerState blk
-> LedgerEraInfo blk
ledgerInfo _ = LedgerEraInfo $ singleEraInfo (Proxy @blk)
queryInfo :: forall blk query result. SingleEraBlock blk
=> query blk result -> SingleEraInfo blk
queryInfo _ = singleEraInfo (Proxy @blk)
hardForkQueryInfo :: All SingleEraBlock xs
=> QueryIfCurrent xs result -> NS SingleEraInfo xs
hardForkQueryInfo = go
where
go :: All SingleEraBlock xs'
=> QueryIfCurrent xs' result -> NS SingleEraInfo xs'
go (QZ qry) = Z (queryInfo qry)
go (QS qry) = S (go qry)
shiftMismatch :: MismatchEraInfo xs -> MismatchEraInfo (x ': xs)
shiftMismatch = MismatchEraInfo . MS . getMismatchEraInfo