Merge #3651

3651: Fix: ChainDB QSM test flakyness r=Jasagredo a=Jasagredo

ChainDB QSM didn't have a notion of validity for blocks that were in
chain suffixes no longer connected to the Genesis block. It now carries
a Set of known-valid blocks to answer the `GetIsValid` query.

Closes CAD-4002
Closes CAD-3590
Closes CAD-3601
Closes #3389
Closes #3440

Co-authored-by: Javier Sagredo <[email protected]>

ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/Model.hs

@@ -133,6 +133,7 @@ data Model blk = Model {
     , currentLedger    :: ExtLedgerState blk
     , initLedger       :: ExtLedgerState blk
     , iterators        :: Map IteratorId [blk]
+    , valid            :: Set (HeaderHash blk)
     , invalid          :: InvalidBlocks blk
     , currentSlot      :: SlotNo
     , maxClockSkew     :: Word64
@@ -313,28 +314,20 @@ immutableSlotNo :: HasHeader blk
 immutableSlotNo k = Chain.headSlot . immutableChain k
 
 getIsValid :: forall blk. LedgerSupportsProtocol blk
-           => TopLevelConfig blk
-           -> Model blk
+           => Model blk
            -> (RealPoint blk -> Maybe Bool)
-getIsValid cfg m = \pt@(RealPoint _ hash) -> if
-    | Set.member pt validPoints   -> Just True
-    | Map.member hash (invalid m) -> Just False
-    | otherwise                   -> Nothing
-  where
-    validPoints :: Set (RealPoint blk)
-    validPoints =
-          foldMap (Set.fromList . map blockRealPoint . Chain.toOldestFirst . fst)
-        . snd
-        . validChains cfg m
-        . blocks
-        $ m
+getIsValid m = \(RealPoint _ hash) -> if
+    | Map.member hash (volatileDbBlocks m) &&
+      Set.member hash (valid m)               -> Just True
+    | Map.member hash (volatileDbBlocks m) &&
+      Map.member hash (invalid m)             -> Just False
+    | otherwise                               -> Nothing
 
 isValid :: forall blk. LedgerSupportsProtocol blk
-        => TopLevelConfig blk
-        -> RealPoint blk
+        => RealPoint blk
         -> Model blk
         -> Maybe Bool
-isValid = flip . getIsValid
+isValid = flip getIsValid
 
 getLedgerDB ::
      LedgerSupportsProtocol blk
@@ -371,6 +364,7 @@ empty initLedger maxClockSkew = Model {
     , initLedger       = initLedger
     , iterators        = Map.empty
     , invalid          = Map.empty
+    , valid            = Set.empty
     , currentSlot      = 0
     , maxClockSkew     = maxClockSkew
     , isOpen           = True
@@ -383,7 +377,7 @@ advanceCurSlot
   -> Model blk -> Model blk
 advanceCurSlot curSlot m = m { currentSlot = curSlot `max` currentSlot m }
 
-addBlock :: forall blk. LedgerSupportsProtocol blk
+addBlock :: forall blk. (Eq blk, LedgerSupportsProtocol blk)
          => TopLevelConfig blk
          -> blk
          -> Model blk -> Model blk
@@ -395,6 +389,7 @@ addBlock cfg blk m = Model {
     , initLedger       = initLedger m
     , iterators        = iterators  m
     , invalid          = invalid'
+    , valid            = valid'
     , currentSlot      = currentSlot  m
     , maxClockSkew     = maxClockSkew m
     , isOpen           = True
@@ -438,6 +433,9 @@ addBlock cfg blk m = Model {
       immutableChainHashes `isPrefixOf`
       map blockHash (Chain.toOldestFirst fork)
 
+    consideredCandidates = filter (extendsImmutableChain . fst)
+      $ candidates
+
     newChain  :: Chain blk
     newLedger :: ExtLedgerState blk
     (newChain, newLedger) =
@@ -446,18 +444,120 @@ addBlock cfg blk m = Model {
           (Proxy @(BlockProtocol blk))
           (selectView (configBlock cfg) . getHeader)
           (currentChain m)
-      . filter (extendsImmutableChain . fst)
-      $ candidates
+      $ consideredCandidates
+
+    -- See note [Getting the valid blocks] just below
+    valid' = foldl
+               (Chain.foldChain (\s b -> Set.insert (blockHash b) s))
+               (valid m)
+               (takeWhile (not . Chain.isPrefixOf newChain) (map fst consideredCandidates) ++ [newChain])
+
+-- = Getting the valid blocks
+--
+-- The chain selection algorithms implemented by the model and by the SUT differ
+-- but have the same outcome.We illustrate this with an example. Imagine having
+-- the following candidate chains where @v@ represents a valid block and @x@
+-- represents an invalid block:
+--
+-- > C0: vvvvvxxxxx
+-- > C1: vvvvvvvx
+-- > C2: vvv
+--
+-- For candidate Cx, we will call CxV the valid prefix and CxI the invalid suffix.
+--
+-- The chain selection algorithm will run whenever we add a block, although it
+-- will only select a new chain when adding a block results in a chain that is
+-- longer than the currently selected chain. Note that the chain selection
+-- algorithm doesn't know beforehand the validity of the blocks in the
+-- candidates. The process it follows will be:
+--
+-- 1. Sort the chains by 'SelectView'. Note that for Praos this will trivially
+-- imply first consider the candidates by length.
+--
+--    > sortedCandidates == [C0, C1, C2]
+--
+-- 2. Until a candidate is found to be valid and longer than the currently selected
+--    chain, take the head of the (sorted) list of candidates and validate the
+--    blocks in it one by one.
+--
+--    If a block in the candidate is found to be invalid, the candidate is
+--    truncated, added back to the list, and the algorithm starts again at step 1.
+--    The valid blocks in the candidate are recorded in the set of known-valid
+--    blocks, so that the next time they are applied, it is known that applying
+--    said block can't fail and therefore some checks can be skipped. The invalid
+--    blocks in the candidate are recorded in the set of known-invalid blocks so
+--    that they are not applied again.
+--
+--    The steps on the example are as follows:
+--
+--    1.  Start with the sorted candidate chains: [C0, C1, C2]
+--    2.  Validate first chain C0 resulting in C0V and C0I.
+--    3.  Append C0V to the list of remaining candidates: [C1, C2] ++ [C0V]
+--    4.  Add the valid blocks to the state:
+--        > knownValid = append C0V knownValid
+--    5.  Add the invalid blocks to the state:
+--        > knownInvalid = append C0I knownInvalid
+--    6.  Re-sort list
+--        > sortBy `selectView` [C1, C2, C0V] == [C1, C0V, C2]
+--    7.  Validate first chain C1 resulting in C1V and C1I.
+--    8.  Append C1V to the list of remaining candidates: [C0V, C2] ++ [C1V]
+--    9.  Add the valid blocks to the state:
+--        > knownValid   = append C1V knownValid
+--    10. Add the invalid blocks to the state:
+--        > knownInvalid = append C1I knownInvalid
+--    11. Re-sort list
+--        > sortBy `selectView` [C0V, C2, C1V] == [C1V, C0V, C2]
+--    12. Validate first chain C1V, which is fully valid and returned.
+--
+-- 3. If such a candidate is found, the algorithm will return it as a result.
+--    Otherwise, the algorithm will return a 'Nothing'.
+--
+--    > chainSelection [C0, C1, C2] = Just C1V
+--
+-- On the other hand, the chain selection on the model takes some shortcuts to
+-- achieve the same result:
+--
+-- 1. 'validChains' will return the list of candidates sorted by 'SelectView' and
+--    each candidate is truncated to its valid prefix.
+--
+--    > validChains [C0, C1, C2] = (invalid == C0I + C1I, candidates == [C0V, C1V, C2])
+--
+-- 2. 'selectChain' will sort the chains by 'SelectView' but note that now it will
+--    use the 'SelectView' of the already truncated candidate.
+--
+--    > selectChain [C0V, C1V, C2] = listToMaybe (sortBy `selectView` [C0V, C1V, C2])
+--    >                            = listToMaybe ([C1V, C0V, C2])
+--    >                            = Just C1V
+--
+--    The selected candidate will be the same one that the chain selection
+--    algorithm would choose. However, as the chain selection algorithm will
+--    consider the candidates as they were sorted by 'SelectView' on the
+--    non-truncated candidates, blocks in 'C0V' are also considered valid by the
+--    real algorithm.
+--
+--    To get as a result a set of valid blocks that mirrors the one from the
+--    real algorithm, the model can process the list of candidates returned by
+--    'validChains' until it find the one 'selectChain' chose as these will be
+--    the ones that the real algorithm would test and re-add to the list once
+--    truncated.
+--
+--    > knownInvalid = append (C0I + C1I) knownInvalid
+--    > knownValid   = foldl append knownValid (takeWhile (/= C1V) candidates ++ [C1V])
+--
+--    Note that the set of known valid blocks is equivalent to the set computed
+--    by real algorithm, but the set of known invalid blocks is a superset of
+--    the ones known by the real algorithm. See the note
+--    Ouroboros.Storage.ChainDB.StateMachine.[Invalid blocks].
 
-addBlocks :: LedgerSupportsProtocol blk
+addBlocks :: (Eq blk, LedgerSupportsProtocol blk)
           => TopLevelConfig blk
           -> [blk]
           -> Model blk -> Model blk
 addBlocks cfg = repeatedly (addBlock cfg)
 
 -- | Wrapper around 'addBlock' that returns an 'AddBlockPromise'.
 addBlockPromise
-  :: forall m blk. (LedgerSupportsProtocol blk, MonadSTM m)
+  :: forall m blk. (Eq blk, LedgerSupportsProtocol blk, MonadSTM m)
   => TopLevelConfig blk
   -> blk
   -> Model blk
@@ -620,7 +720,7 @@ class ( HasHeader blk
   Internal auxiliary
 -------------------------------------------------------------------------------}
 
-type InvalidBlocks blk = Map (HeaderHash blk) (InvalidBlockReason blk, SlotNo)
+type InvalidBlocks blk = Map (HeaderHash blk) (InvalidBlockReason blk, Slot
 
 -- | Result of 'validate', also used internally.
 data ValidatedChain blk =

ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/StateMachine.hs

@@ -581,7 +581,7 @@ runPure cfg = \case
     GetBlockComponent pt     -> err MbAllComponents     $ query   (Model.getBlockComponentByPoint allComponents pt)
     GetGCedBlockComponent pt -> err mbGCedAllComponents $ query   (Model.getBlockComponentByPoint allComponents pt)
     GetMaxSlotNo             -> ok  MaxSlot             $ query    Model.getMaxSlotNo
-    GetIsValid pt            -> ok  isValidResult       $ query   (Model.isValid cfg pt)
+    GetIsValid pt            -> ok  isValidResult       $ query   (Model.isValid pt)
     Stream from to           -> err iter                $ updateE (Model.stream k from to)
     IteratorNext  it         -> ok  IterResult          $ update  (Model.iteratorNext it allComponents)
     IteratorNextGCed it      -> ok  iterResultGCed      $ update  (Model.iteratorNext it allComponents)
@@ -1076,7 +1076,7 @@ invariant ::
   -> Model blk m Concrete
   -> Logic
 invariant cfg Model {..} =
-    forall ptsOnCurChain (Boolean . fromMaybe False . isValid)
+    forall ptsOnCurChain (Boolean . fromMaybe False . Model.getIsValid dbModel)
   where
     -- | The blocks occurring on the current volatile chain fragment
     ptsOnCurChain :: [RealPoint blk]
@@ -1086,9 +1086,6 @@ invariant cfg Model {..} =
         . Model.volatileChain (configSecurityParam cfg) id
         $ dbModel
 
-    isValid :: RealPoint blk -> Maybe Bool
-    isValid = Model.getIsValid cfg dbModel
-
 postcondition :: TestConstraints blk
               => Model   blk m Concrete
               -> At Cmd  blk m Concrete