Skip to content

Commit

Permalink
Some fixes and polishing
Browse files Browse the repository at this point in the history
  • Loading branch information
Niols committed Apr 29, 2024
1 parent 3486ae7 commit c061d05
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
module Test.Consensus.Genesis.Tests.CSJ (tests) where

import Control.Monad (replicateM)
import Data.Containers.ListUtils (nubOrd)
import Data.Functor (($>))
import Data.List (nub)
import Data.Maybe (mapMaybe)
Expand Down Expand Up @@ -65,16 +66,24 @@ prop_happyPath synchronized =
mapMaybe
(\case
TraceChainSyncClientEvent pid (TraceDownloadedHeader hdr)
| isOlderThanJumpSizeFromTip gt hdr
| not (isNewerThanJumpSizeFromTip gt hdr)
-> Just (pid, hdr)
_ -> Nothing
_ -> Nothing
)
svTrace
receivedHeadersOnlyOnce = length (nub $ snd <$> headerDownloadEvents) == length headerDownloadEvents
receivedHeadersFromOnlyOnePeer = length (nub $ fst <$> headerDownloadEvents) == 1
-- NOTE: If all the headers are newer than jumpSize from the tip, then
-- 'headerDownloadEvents' is empty and the following condition would
-- violated if we used @==@.
receivedHeadersFromOnlyOnePeer = length (nubOrd $ fst <$> headerDownloadEvents) <= 1
in
tabulate ""
[ if headerDownloadEvents == []
then "All headers may be downloaded twice"
else "There exist headers that have to be downloaded exactly once"
] $
counterexample
("Downloaded headers:\n" ++
("Downloaded headers (except jumpSize slots near the tip):\n" ++
( unlines $ fmap (" " ++) $ zipWith
(\peer header -> peer ++ " | " ++ header)
(condenseListWithPadding PadRight $ fst <$> headerDownloadEvents)
Expand All @@ -92,9 +101,14 @@ prop_happyPath synchronized =
ps <- genUniformSchedulePoints gt
pure $ value $ honest ps

isOlderThanJumpSizeFromTip :: GenesisTestFull TestBlock -> Header TestBlock -> Bool
isOlderThanJumpSizeFromTip gt hdr =
-- NOTE: We might change the way the jumps are decided, which would require
-- also changing this condition. cf
-- https://github.com/IntersectMBO/ouroboros-consensus/pull/1081/files#r1583263224
isNewerThanJumpSizeFromTip :: GenesisTestFull TestBlock -> Header TestBlock -> Bool
isNewerThanJumpSizeFromTip gt hdr =
let jumpSize = csjpJumpSize $ gtCSJParams gt
tipSlot = AF.headSlot $ btTrunk $ gtBlockTree gt
hdrSlot = blockSlot hdr
in hdrSlot + jumpSize < succWithOrigin tipSlot
in
-- Sanity check: add @1 +@ after @>@ and watch the World burn.
hdrSlot + jumpSize > succWithOrigin tipSlot
Original file line number Diff line number Diff line change
Expand Up @@ -369,7 +369,9 @@ nextInstruction context = whenEnabled context RunNormally $
-- validating it.
--
-- We request jumpers to jump here if the next header received by the dynamo is
-- at least jump size slots after the last jump.
-- at least jump size slots after the last jump. Note that, since this function
-- runs before validating the next header, it will not be part of the fragment
-- considered for the jump.
--
-- We also check that the Objector disagrees with the header sent at its
-- rejected jump. If it agrees to it, we disengage it.
Expand Down

0 comments on commit c061d05

Please sign in to comment.