Skip to content

Commit

Permalink
ChainDB q-s-m: maintain valid points cumulatively
Browse files Browse the repository at this point in the history
Previously, the model might forget about disconnected blocks still in the
VolatileDB that it had validated previously, which is not something that can
happen with the SUT, resulting in a test failure. This can arise in specific
cases after garbage collection, see
IntersectMBO/ouroboros-network#3389 for a concrete
example.

Co-authored-by: Joris Dral <[email protected]>
  • Loading branch information
amesgen and jorisdral committed Aug 16, 2023
1 parent a82bf37 commit b4a3f2e
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 22 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,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
Expand Down Expand Up @@ -304,28 +305,23 @@ 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
getIsValid m = \(RealPoint _ hash) -> if
-- Note that we are not checking whether the block is in the VolatileDB.
-- This is justified as we already assume that the model knows more about
-- valid blocks (see 'IsValidResult') and garbage collection of invalid
-- blocks differs between the model and the SUT (see the "Invalid blocks"
-- note in @./StateMachine.hs@).
| Set.member hash (valid m) -> 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

isValid :: forall blk. LedgerSupportsProtocol blk
=> TopLevelConfig blk
-> RealPoint blk
=> RealPoint blk
-> Model blk
-> Maybe Bool
isValid = flip . getIsValid
isValid = flip getIsValid

getLedgerDB ::
LedgerSupportsProtocol blk
Expand Down Expand Up @@ -361,6 +357,7 @@ empty initLedger maxClockSkew = Model {
, currentLedger = initLedger
, initLedger = initLedger
, iterators = Map.empty
, valid = Set.empty
, invalid = Map.empty
, currentSlot = 0
, maxClockSkew = maxClockSkew
Expand All @@ -385,6 +382,7 @@ addBlock cfg blk m = Model {
, currentLedger = newLedger
, initLedger = initLedger m
, iterators = iterators m
, valid = valid'
, invalid = invalid'
, currentSlot = currentSlot m
, maxClockSkew = maxClockSkew m
Expand Down Expand Up @@ -429,6 +427,10 @@ addBlock cfg blk m = Model {
immutableChainHashes `isPrefixOf`
map blockHash (Chain.toOldestFirst fork)

-- Note that this includes the currently selected chain, but that does not
-- influence chain selection via 'selectChain'.
consideredCandidates = filter (extendsImmutableChain . fst) candidates

newChain :: Chain blk
newLedger :: ExtLedgerState blk
(newChain, newLedger) =
Expand All @@ -437,8 +439,16 @@ addBlock cfg blk m = Model {
(Proxy @(BlockProtocol blk))
(selectView (configBlock cfg) . getHeader)
(currentChain m)
. filter (extendsImmutableChain . fst)
$ candidates
$ consideredCandidates

-- We update the set of valid blocks with all valid blocks on all candidate
-- chains that are considered by the modeled chain selection. This ensures
-- that the model always knows about more valid blocks than the system under
-- test. See 'IsValidResult' for more context.
valid' =
valid m <> foldMap
(Set.fromList . map blockHash . Chain.toOldestFirst . fst)
consideredCandidates

addBlocks :: LedgerSupportsProtocol blk
=> TopLevelConfig blk
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -635,7 +635,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)
Expand Down Expand Up @@ -1150,7 +1150,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]
Expand All @@ -1160,9 +1160,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
Expand Down

0 comments on commit b4a3f2e

Please sign in to comment.