diff --git a/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/Model.hs b/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/Model.hs index 832eb32ef06..1051cfa0675 100644 --- a/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/Model.hs +++ b/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,10 +444,112 @@ 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 @@ -457,7 +557,7 @@ 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 = diff --git a/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/StateMachine.hs b/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/StateMachine.hs index 9c33f4c3478..b9363c04b14 100644 --- a/ouroboros-consensus-test/test-storage/Test/Ouroboros/Storage/ChainDB/StateMachine.hs +++ b/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