From ecfbdd62e493d1b48176ad9e5ee1c48d31d974bb Mon Sep 17 00:00:00 2001 From: Nicolas Frisby Date: Thu, 31 Aug 2023 13:46:28 -0700 Subject: [PATCH] consensus-testlib: add ChainGenerators MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit For those involved in this PR's development, this commit is a manual full "squash" of 8f3b50b5530635dd7d0563ef842222eaf761484e. Co-authored-by: Facundo Domínguez Co-authored-by: amesgen --- ...326_225413_nick.frisby_chain_generators.md | 4 + ouroboros-consensus/ouroboros-consensus.cabal | 17 + .../Consensus/ChainGenerator/Adversarial.hs | 572 ++++++++++++++++++ .../Consensus/ChainGenerator/BitVector.hs | 209 +++++++ .../Consensus/ChainGenerator/Counting.hs | 388 ++++++++++++ .../Consensus/ChainGenerator/Honest.hs | 523 ++++++++++++++++ .../Consensus/ChainGenerator/Params.hs | 89 +++ .../Consensus/ChainGenerator/README.md | 14 + .../Consensus/ChainGenerator/RaceIterator.hs | 152 +++++ .../Consensus/ChainGenerator/Slot.hs | 163 +++++ .../Consensus/ChainGenerator/Some.hs | 108 ++++ ouroboros-consensus/test/infra-test/Main.hs | 4 +- .../Consensus/ChainGenerator/Tests.hs | 16 + .../ChainGenerator/Tests/Adversarial.hs | 477 +++++++++++++++ .../ChainGenerator/Tests/BitVector.hs | 143 +++++ .../ChainGenerator/Tests/Counting.hs | 34 ++ .../Consensus/ChainGenerator/Tests/Honest.hs | 206 +++++++ 17 files changed, 3118 insertions(+), 1 deletion(-) create mode 100644 ouroboros-consensus/changelog.d/20230326_225413_nick.frisby_chain_generators.md create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Adversarial.hs create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/BitVector.hs create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Counting.hs create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Honest.hs create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Params.hs create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/README.md create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/RaceIterator.hs create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Slot.hs create mode 100644 ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Some.hs create mode 100644 ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests.hs create mode 100644 ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Adversarial.hs create mode 100644 ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/BitVector.hs create mode 100644 ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Counting.hs create mode 100644 ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Honest.hs diff --git a/ouroboros-consensus/changelog.d/20230326_225413_nick.frisby_chain_generators.md b/ouroboros-consensus/changelog.d/20230326_225413_nick.frisby_chain_generators.md new file mode 100644 index 0000000000..6ebb98ad0b --- /dev/null +++ b/ouroboros-consensus/changelog.d/20230326_225413_nick.frisby_chain_generators.md @@ -0,0 +1,4 @@ +### Non-Breaking + +- Added `ChainGenerators`. + See `checkAdversarialChain` and `checkHonestChain` for the invariants these generators ensure. diff --git a/ouroboros-consensus/ouroboros-consensus.cabal b/ouroboros-consensus/ouroboros-consensus.cabal index b8211ca783..1e1271edc2 100644 --- a/ouroboros-consensus/ouroboros-consensus.cabal +++ b/ouroboros-consensus/ouroboros-consensus.cabal @@ -286,6 +286,14 @@ library unstable-consensus-testlib visibility: public hs-source-dirs: src/unstable-consensus-testlib exposed-modules: + Test.Ouroboros.Consensus.ChainGenerator.Adversarial + Test.Ouroboros.Consensus.ChainGenerator.BitVector + Test.Ouroboros.Consensus.ChainGenerator.Counting + Test.Ouroboros.Consensus.ChainGenerator.Honest + Test.Ouroboros.Consensus.ChainGenerator.Params + Test.Ouroboros.Consensus.ChainGenerator.RaceIterator + Test.Ouroboros.Consensus.ChainGenerator.Slot + Test.Ouroboros.Consensus.ChainGenerator.Some Test.Util.BoolProps Test.Util.ChainDB Test.Util.ChainUpdates @@ -362,6 +370,7 @@ library unstable-consensus-testlib , time , tree-diff , utf8-string + , vector library unstable-mock-block import: common-lib @@ -507,16 +516,24 @@ test-suite infra-test main-is: Main.hs other-modules: Ouroboros.Consensus.Util.Tests + Test.Ouroboros.Consensus.ChainGenerator.Tests + Test.Ouroboros.Consensus.ChainGenerator.Tests.Adversarial + Test.Ouroboros.Consensus.ChainGenerator.Tests.BitVector + Test.Ouroboros.Consensus.ChainGenerator.Tests.Counting + Test.Ouroboros.Consensus.ChainGenerator.Tests.Honest Test.Util.ChainUpdates.Tests Test.Util.Schedule.Tests Test.Util.Split.Tests build-depends: , base + , mtl , ouroboros-consensus:{ouroboros-consensus, unstable-consensus-testlib} , QuickCheck + , random , tasty , tasty-quickcheck + , vector test-suite storage-test import: common-test diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Adversarial.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Adversarial.hs new file mode 100644 index 0000000000..5b3a7c758d --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Adversarial.hs @@ -0,0 +1,572 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +-- TODO rename to .Alternative? +module Test.Ouroboros.Consensus.ChainGenerator.Adversarial ( + -- * Generating + AdversarialRecipe (AdversarialRecipe, arHonest, arParams, arPrefix) + , CheckedAdversarialRecipe (UnsafeCheckedAdversarialRecipe, carHonest, carParams, carWin) + , NoSuchAdversarialChainSchema (NoSuchAdversarialBlock, NoSuchCompetitor, NoSuchIntersection) + , SomeCheckedAdversarialRecipe (SomeCheckedAdversarialRecipe) + , checkAdversarialRecipe + , uniformAdversarialChain + -- * Testing + , AdversarialViolation (BadAnchor, BadCount, BadRace) + , AnchorViolation (HonestActiveMustAnchorAdversarial) + , ChainSchema (ChainSchema) + , RaceViolation (AdversaryWonRace, rvAdv, rvHon) + , checkAdversarialChain + ) where + +import Control.Applicative ((<|>)) +import Control.Monad (void, when) +import qualified Control.Monad.Except as Exn +import Data.Proxy (Proxy (Proxy)) +import qualified System.Random.Stateful as R +import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import Test.Ouroboros.Consensus.ChainGenerator.Honest + (ChainSchema (ChainSchema)) +import Test.Ouroboros.Consensus.ChainGenerator.Params (Asc, + Delta (Delta), Kcp (Kcp), Scg (Scg)) +import qualified Test.Ouroboros.Consensus.ChainGenerator.RaceIterator as RI +import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S +import Test.Ouroboros.Consensus.ChainGenerator.Slot + (E (ActiveSlotE, EmptySlotE, SlotE)) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some + +----- + +data AnchorViolation = + -- | An honest active slot must immediately precede the adversarial interval + HonestActiveMustAnchorAdversarial + | + -- | The were not exactly 'arPrefix' many active slots preceding @adv@ + WrongNumberOfHonestPredecessors + deriving (Eq, Read, Show) + +-- | A violation of Races Before Acceleration Assumption +-- +-- INVARIANT: @'C.windowLast' 'rvAdv' < 'C.windowLast' 'rvHon' + 'Delta'@ +-- +-- INVARIANT: @'C.windowStart' 'rvHon' <= 'C.windowStart' 'rvAdv'@ +data RaceViolation hon adv = AdversaryWonRace { + -- | The adversarial race window + rvAdv :: !(RI.Race adv) + , + -- | The honest race window + rvHon :: !(RI.Race hon) + } + deriving (Eq, Read, Show) + +data AdversarialViolation hon adv = + BadAnchor !AnchorViolation + | + -- | The schema does not contain a positive number of active slots + BadCount + | + BadRace !(RaceViolation hon adv) + deriving (Eq, Read, Show) + +-- | Check the chain matches the given 'AdversarialRecipe'. +-- +-- * It must intersect the honest chain at an active slot +-- * It must satisfy the Races Before Acceleration Assumption +-- (which implies the Length of Competing Chains Assumption) +-- +-- Definition of a /Praos Race Window/ of a chain. It is an interval of slots +-- that contains at least @k+1@ blocks of the chain and exactly 'Delta' slots +-- after the @k+1@st block. +-- +-- Definition of the /Length of Competing Chains Assumption/. We assume every adversarial +-- chain contains at most @k@ blocks in the Praos Race Window anchored at the +-- the intersection. +-- +-- Definition of /Acceleration Lower Bound of an Adversarial Chain/. It is +-- the lowest slot at which an adversary could speed up its elections on a +-- given adversarial chain. It is defined as the 'Scg'-th slot after the first +-- adversarial block or the 'Delta'-th slot after the @k+1@st honest block after the +-- intersection, whichever is greater. +-- +-- Definition of the /Races Before Acceleration Assumption/. Every adversarial +-- chain has at most @k@ blocks in every Praos Race Window of the honest chain +-- that starts after the intersection and ends before the acceleration lower +-- bound. +-- +-- Definition of the /Genesis Implication Conjecture/. We conjecture that +-- assuming that the Genesis window length is no greater than the Stability +-- Window and that every possible adversarial chain satisfies the Races +-- in Stability Windows Assumption, then the honest chain strictly wins every possible density +-- comparison from the Ouroboros Genesis paper. The key intuition is that a less +-- dense chain would have to lose at least one Praos race within the Genesis window. +checkAdversarialChain :: + forall base hon adv. + AdversarialRecipe base hon + -> ChainSchema base adv + -> Exn.Except (AdversarialViolation hon adv) () +checkAdversarialChain recipe adv = do + checkStart + checkCount + checkRaces + where + AdversarialRecipe { + arHonest = ChainSchema winH vH + , + arParams = (Kcp k, Scg s, Delta d) + , + arPrefix + } = recipe + + ChainSchema winA vA = adv + + checkStart = do + let startA = C.windowStart winA :: C.Index base SlotE + intersection = startA C.- 1 :: C.Index base SlotE + + -- The intersection must be at an active slot in the honest chain. + case C.toWindow winH intersection of + Nothing -> do + -- the genesis block is the only permissible anchor outside of @hon@ + when (startA /= C.Count 0) $ Exn.throwError $ BadAnchor HonestActiveMustAnchorAdversarial + when (arPrefix /= C.Count 0) $ Exn.throwError $ BadAnchor WrongNumberOfHonestPredecessors + + Just i -> do + let _ = i :: C.Index hon SlotE + + when (BV.testV S.inverted vH i) $ do + Exn.throwError $ BadAnchor HonestActiveMustAnchorAdversarial + + C.SomeWindow Proxy precedingSlots <- + pure $ C.withWindowBetween (C.windowSize winH) (C.Lbl @"foo") (C.Count 0) i + let pc = BV.countActivesInV S.notInverted (C.sliceV precedingSlots vH) + + -- arPrefix must correctly count the active slots in the part of + -- the chain upto the intersection + when (C.fromWindowVar precedingSlots (C.toVar pc) /= arPrefix) $ do + Exn.throwError $ BadAnchor WrongNumberOfHonestPredecessors + + checkCount = do + let pc = BV.countActivesInV S.notInverted vA + when (C.toVar pc <= 0) $ Exn.throwError BadCount + + -- the youngest slot in which the adversarial schedule cannot have accelerated + -- + -- (IE @s@ past the first active adversarial slot, or @d@ past the @k+1@st + -- slot after the intersection) + youngestStableA :: C.Index base SlotE + youngestStableA = + let sYoungest = case BV.findIthEmptyInV S.inverted vA (C.Count 0) of + BV.JustFound firstActiveA -> + -- if s=0, then the slot of their block is the youngest stable slot + C.fromWindow winA $ firstActiveA C.+ s + BV.NothingFound -> + -- the rest of the function won't force this since there are no + -- adversarial active slots + error "dead code" + kPlus1stYoungest = case BV.findIthEmptyInV S.inverted vH (C.toIndex arPrefix C.+ k) of + BV.JustFound kPlus1st -> C.fromWindow winH kPlus1st + BV.NothingFound -> + -- If the honest fork didn't reach @k+1@ before it ended, then + -- the conservative assumption that all slots after 'Len' are + -- active on the honest chain implies the @k+1@st block is in + -- slot @C.windowLast winH + (k+1-x)@, where the honest chain + -- has @x@ remaining blocks such that @x>= RI.next vA of + Nothing -> pure () -- there are <= k total adversarial active slots + Just iterA -> + -- TODO optimization: how to skip all the honest Race Windows that + -- don't reach beyond the intersection? Perhaps skip to i - s + d? + go iterH iterA + + -- INVARIANT iterH spans k+1 active slots (possibly conservatively) + -- + -- INVARIANT iterA spans k active slots (actually, not conservatively) + go !iterH !iterA = do + C.SomeWindow Proxy raceWinH <- pure $ let RI.Race x = iterH in x + C.SomeWindow Proxy raceWinA <- pure $ let RI.Race x = iterA in x + + -- lift both windows to @base@ so that they're comparable + let raceWinH' = C.joinWin winH raceWinH + raceWinA' = C.joinWin winA raceWinA + + if + + -- any Race Window that ends /after/ the adversary can accelerate is unconstrained + | youngestStableA < C.windowLast raceWinH' C.+ d -> pure () + + -- advance the adversarial Race Window if its start is <= the honest Race Window's start + | C.windowStart raceWinA' <= C.windowStart raceWinH' -> + case RI.next vA iterA of + Just iterA' -> go iterH iterA' + Nothing -> pure () -- there are < k remaining adversarial active slots + + -- fail if the adversary won or tied the race + | C.windowLast raceWinA' <= C.windowLast raceWinH' C.+ d -> + -- iterA contains exactly k active slots, but A) it's anchored + -- in an active slot and B) iterH contains that anchor. Thus + -- adv has k+1 in iterH. + Exn.throwError $ BadRace AdversaryWonRace { + rvAdv = iterA + , + rvHon = iterH + } + + -- advance the honest Race Window + | otherwise -> case RI.next vH iterH <|> RI.nextConservative vH iterH of + Just iterH' -> go iterH' iterA + Nothing -> pure () -- there are no remaining honest active slots + -- + -- TODO hpc shows this never executes + +----- + +-- | Named arguments for 'checkAdversarialRecipe' +data AdversarialRecipe base hon = + AdversarialRecipe { + -- | The honest chain to branch off of + arHonest :: !(ChainSchema base hon) + , + -- | protocol parameters + arParams :: (Kcp, Scg, Delta) + , + -- | Where to branch off of 'arHonest' + -- + -- It is the amount of blocks shared by the honest and the adversarial + -- chain. In other words, the 0-based index of their intersection + -- in blocks, such that + -- + -- * @0@ identifies the genesis block + -- * @1@ identifies the first block in arHonest + -- * @2@ identifies the second block in arHonest + -- * etc + arPrefix :: !(C.Var hon ActiveSlotE) + } + deriving (Eq, Read, Show) + +-- | See 'CheckedAdversarialRecipe' +data SomeCheckedAdversarialRecipe base hon = + forall adv. + SomeCheckedAdversarialRecipe + !(Proxy adv) + !(CheckedAdversarialRecipe base hon adv) + +instance Show (SomeCheckedAdversarialRecipe base hon) where + showsPrec p (SomeCheckedAdversarialRecipe adv car) = + Some.runShowsPrec p + $ Some.showCtor SomeCheckedAdversarialRecipe "SomeCheckedAdversarialRecipe" + `Some.showArg` adv + `Some.showArg` car + +instance Read (SomeCheckedAdversarialRecipe base hon) where + readPrec = + Some.runReadPrec + $ Some.readCtor SomeCheckedAdversarialRecipe "SomeCheckedAdversarialRecipe" + <*> Some.readArg + <*> Some.readArg + +-- | Image of 'checkAdversarialRecipe' when it accepts the recipe +data CheckedAdversarialRecipe base hon adv = + UnsafeCheckedAdversarialRecipe { + -- | The honest chain to branch off of + carHonest :: !(ChainSchema base hon) + , + -- | protocol parameters + carParams :: (Kcp, Scg, Delta) + , + -- | The window starting at the first slot after the intersection + -- and ending at the last slot of 'carHonest'. + -- + -- INVARIANT: there is at least one active honest slot in @adv@ + -- + -- In other words, the adversarial leader schedule does not /extend/ the + -- chain represented by 'carHonest', it competes with it. + carWin :: !(C.Contains SlotE hon adv) + } + deriving (Eq, Read, Show) + +-- | Image of 'checkAdversarialRecipe' when it rejects the recipe +data NoSuchAdversarialChainSchema = + -- | There is no slot the adversary can lead + -- + -- Two possible reasons, where @X@ is the slot of 'arPrefix' and Y is the youngest slot of 'arHonest'. + -- + -- * The interval @[X, Y)@ is empty. + -- + -- * @k=0@ + -- + -- Suppose k=0 and slot x and slot y are two honest active slots with only + -- honest empty slots between them. + -- + -- Length of Competing Chains prohibits the adversary from leading in the interval (x,y]. + -- + -- In fact, by induction, the adversary can never lead: suppose the same y + -- and a slot z are two honest active slots with only honest empty slots + -- between them... + NoSuchAdversarialBlock + | + -- | @not ('arPrefix' < C)@ where @C@ is the number of active slots in 'arHonest' + NoSuchCompetitor + | + -- | @not (0 <= 'arPrefix' <= C)@ where @C@ is the number of active slots in 'arHonest' + NoSuchIntersection + deriving (Eq, Show) + +----- + +-- | The suffix of the slots starting strictly /after/ the intersection +data AdvLbl + +-- | The interval of slots that have most recently attained their final value +data SettledLbl + +-- | Reject a bad 'AdversarialRecipe' +checkAdversarialRecipe :: + forall base hon. + AdversarialRecipe base hon + -> Exn.Except + NoSuchAdversarialChainSchema + (SomeCheckedAdversarialRecipe base hon) +checkAdversarialRecipe recipe = do + when (0 == k) $ Exn.throwError NoSuchAdversarialBlock + + -- validate 'arPrefix' + firstAdvSlot <- case compare arPrefix 0 of + LT -> Exn.throwError NoSuchIntersection + EQ -> pure $ C.Count 0 + GT -> case BV.findIthEmptyInV S.inverted vH $ C.toIndex $ arPrefix - 1 of + BV.NothingFound -> Exn.throwError NoSuchIntersection + BV.JustFound x -> do + when (x == C.lastIndex (C.windowSize winH)) $ Exn.throwError NoSuchAdversarialBlock + pure (x C.+ 1) + + C.SomeWindow Proxy winA <- pure $ C.withSuffixWindow (C.windowSize winH) (C.Lbl @AdvLbl) firstAdvSlot + + -- there must be at least one honest active slot in @adv@ + case BV.findIthEmptyInV S.inverted (C.sliceV winA vH) (C.Count 0) of + BV.NothingFound -> Exn.throwError NoSuchCompetitor + BV.JustFound{} -> pure () + + pure $ SomeCheckedAdversarialRecipe Proxy $ UnsafeCheckedAdversarialRecipe { + carHonest = arHonest + , + carParams = arParams + , + carWin = winA + } + where + AdversarialRecipe { + arHonest + , + arParams + , + arPrefix + } = recipe + + (Kcp k, _scg, _delta) = arParams + + ChainSchema winH vH = arHonest + +----- + +data RaceAssumptionLbl +data UntouchableLbl +data TouchableLbl + +-- | Generate an adversarial 'ChainSchema' that satifies 'checkExtendedRaceAssumption' +-- +-- The distribution this function samples from is not simple to describe. It +-- begins by drawing a sample of length 'adv' from the Bernoulli process +-- induced by the active slot coefficient 'Asc'. (IE 'adv' many i.i.d. samples +-- from @Uniform(f)@). Then it visits the Extended Praos Race Windows that +-- overlap with the prefix of that leader schedule that ends one stability +-- window after the first (remaining) active adversarial slot in it. In each +-- such Window, it removes the youngest active slots from the adversarial +-- leader schedule until it loses that Race. +uniformAdversarialChain :: + forall g base hon adv. + R.RandomGen g + => Maybe Asc -- ^ 'Nothing' means @1@ + -> CheckedAdversarialRecipe base hon adv + -> g + -> ChainSchema base adv +{-# INLINABLE uniformAdversarialChain #-} +uniformAdversarialChain mbAsc recipe g0 = wrap $ C.createV $ do + g <- R.newSTGenM g0 + + let sz = C.windowSize carWin :: C.Size adv SlotE + + -- randomly initialize the bitstring + mv <- C.replicateMV sz $ case mbAsc of + Nothing -> pure $ S.mkActive S.notInverted + Just asc -> S.genS asc `R.applySTGen` g + + -- ensure the adversarial leader schedule is not empty + do void $ BV.fillInWindow + S.notInverted + (BV.SomeDensityWindow (C.Count 1) (C.windowSize carWin)) + g + mv + + -- find the slot of the k+1 honest block + let kPlus1st :: C.Index adv SlotE + kPlus1st = case BV.findIthEmptyInV S.inverted (C.sliceV carWin vH) (C.Count k) of + BV.NothingFound -> maybe (error "dead code") id $ C.toWindow carWin $ C.windowLast carWin + BV.JustFound x -> x + + + -- ensure the adversarial leader schedule does not win any of the races for + -- which the honest Race Window fits within the Stability Window anchored at + -- the first adversarial active slot + -- + -- TODO Why is it ok to skip early honest races, some of which overlap with + -- @adv@? Is it because not having >k in some prefix [0, n] of adv ensures + -- you can't have >k in the interval [0, C.frWindow adv n] either? + let iterH :: RI.Race adv + iterH = + maybe (RI.initConservative vA) id + $ RI.init kcp vA + unfillRaces kPlus1st (C.Count 0) UnknownYS iterH g mv + + pure mv + where + UnsafeCheckedAdversarialRecipe { + carHonest + , + carParams = (kcp, scg, delta) + , + carWin + } = recipe + + wrap v = ChainSchema (C.joinWin winH carWin) v + + Kcp k = kcp + Scg s = scg + Delta d = delta + + ChainSchema winH vH = carHonest + + vA = C.sliceV carWin vH + + -- ensure the adversary loses this 'RI.Race' and each subsequent race that ends before it can accelerate + unfillRaces kPlus1st !scope !mbYS !iter !g !mv = when (withinYS delta mbYS iter) $ do + C.SomeWindow Proxy rwin <- pure $ let RI.Race x = iter in x + + C.SomeWindow (Proxy :: Proxy skolem) win <- + pure + $ C.withWindowBetween + (C.windowSize carWin) + (C.Lbl @RaceAssumptionLbl) + (C.windowStart rwin) + (C.windowLast rwin C.+ d) -- rwin ends in a block, so if d=0 + -- then the slot after that block + -- is unconstrained; hence no +1 + + -- INVARIANT: @win@ contains @scope@ + let _ = scope :: C.Index adv SlotE + + -- remove adversarial active slots as needed + -- + -- But only remove them from /after/ @scope@ (ie do not remove them + -- from slots in the previous Race Window). + do untouchZeroCount :: C.Var adv EmptySlotE <- do + C.SomeWindow Proxy untouch <- -- untouchable slots + pure + $ C.withWindowBetween + (C.windowSize carWin) + (C.Lbl @UntouchableLbl) + (C.windowStart rwin) + (scope C.- 1) -- window will be empty if scope is 0 + C.fromWindowVar untouch <$> BV.countActivesInMV S.inverted (C.sliceMV untouch mv) + + C.SomeWindow (Proxy :: Proxy skolem2) touch <- -- touchable slots + pure + $ C.withWindowBetween + (C.windowSize carWin) + (C.Lbl @TouchableLbl) + scope + (C.windowLast rwin C.+ d) + + + let + maxActive :: C.Var (C.Win RaceAssumptionLbl skolem) ActiveSlotE + maxActive = C.Count k + + -- at most k can be active in this race window, so at least size - k must be empty + minEmpty :: C.Var (C.Win RaceAssumptionLbl skolem) EmptySlotE + minEmpty = S.complementActive S.notInverted (C.windowSize win) maxActive + + -- Discount that basic requirement by the number of zeros already + -- in the untouchable portion of this race window. + let touchableEmpty = + max 0 + $ C.fromWindowVar win minEmpty - untouchZeroCount + :: C.Var adv EmptySlotE + + void $ BV.fillInWindow + S.inverted + (BV.SomeDensityWindow (C.toWindowVar touch touchableEmpty) (C.windowSize touch)) + g + (C.sliceMV touch mv) + + case RI.next vA iter <|> RI.nextConservative vA iter of + Nothing -> pure () -- there are no remaining honest active slots + + Just iter' -> do + C.SomeWindow Proxy rwin' <- pure $ let RI.Race x = iter' in x + mbYS' <- case mbYS of + KnownYS{} -> pure mbYS + UnknownYS -> do + -- check whether the slots that are settled as of just + -- now contain the first adversarial active slot + C.SomeWindow Proxy settledSlots <- + pure + $ C.withWindowBetween + (C.windowSize carWin) + (C.Lbl @SettledLbl) + (C.windowStart rwin) + (C.windowStart rwin' C.- 1) + mbFound <- BV.findIthEmptyInMV S.inverted (C.sliceMV settledSlots mv) (C.Count 0) + case mbFound of + BV.NothingFound -> pure UnknownYS + BV.JustFound x -> + -- x is the first settled adversarial slot, so + -- the adversary can accelerate its growth as + -- of x+s+1 (If s were 0, it could accelerate + -- in the very next slot, thus the plus 1.) + pure $! KnownYS $! + max + (kPlus1st C.+ d C.+ 1) + (C.fromWindow settledSlots x C.+ s C.+ 1) + unfillRaces kPlus1st (C.windowLast win C.+ 1) mbYS' iter' g mv + +-- | The youngest stable slot +-- +-- If @x@ is the first adversarial active slot, then @x+s@ (see 'Scg') is the youngest stable slot. +data MaybeYS base = UnknownYS | KnownYS !(C.Index base SlotE) + deriving (Eq, Read, Show) + +-- | Does the Race Window end in a stable slot? +withinYS :: Delta -> MaybeYS base -> RI.Race base -> Bool +withinYS (Delta d) !mbYS !(RI.Race (C.SomeWindow Proxy win)) = case mbYS of + KnownYS ys -> C.windowLast win C.+ d < ys + UnknownYS -> True -- Honest Chain Growth ensures every Race Window is at most @'Scg' - 'Delta'@ slots wide diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/BitVector.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/BitVector.hs new file mode 100644 index 0000000000..6463deba6f --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/BitVector.hs @@ -0,0 +1,209 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Test.Ouroboros.Consensus.ChainGenerator.BitVector ( + -- * Finding + MaybeFound (JustFound, NothingFound) + , findIthActiveInV + , findIthEmptyInMV + , findIthEmptyInV + -- * Counting + , countActivesInMV + , countActivesInV + -- * Slots + , setMV + , testMV + , testV + -- * Generating + , SomeDensityWindow (SomeDensityWindow) + , fillInWindow + ) where + +import Control.Monad.ST (ST, runST) +import Data.Functor ((<&>)) +import qualified Data.Vector.Unboxed.Mutable as MV +import qualified System.Random.Stateful as R +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S +import Test.Ouroboros.Consensus.ChainGenerator.Slot + (E (ActiveSlotE, EmptySlotE, SlotE), POL, PreImage, S) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some + +----- + +data MaybeFound base = + NothingFound + | + JustFound + {-# UNPACK #-} !(C.Index base SlotE) + deriving (Eq, Read, Show) + +-- | Trivial wrapper around 'findIthEmptyInMV' +findIthEmptyInV :: + POL pol + => proxy pol + -> C.Vector base SlotE S + -> C.Index base (PreImage pol EmptySlotE) + -> MaybeFound base +findIthEmptyInV pol v i = + runST $ C.unsafeThawV v >>= \mv -> findIthEmptyInMV pol mv i + +-- | Find the (i+1)st empty slot in a window +-- +-- * @findIthEmptyInMV notInverted v 0@ yields the first empty slot +-- * @findIthEmptyInMV notInverted v 1@ yields the second empty slot +-- * @findIthEmptyInMV notInverted v k@ yields the @k+1@st empty slot +-- +-- > findIthEmptyInMV notInverted 01101 0 == JustFound 0 +-- > findIthEmptyInMV notInverted 01101 1 == JustFound 3 +-- > findIthEmptyInMV notInverted 01101 2 == NothingFound +-- +findIthEmptyInMV :: + forall proxy pol base s. + POL pol + => proxy pol + -> C.MVector base SlotE s S + -> C.Index base (PreImage pol EmptySlotE) + -> ST s (MaybeFound base) +findIthEmptyInMV pol mv i = + go 0 (C.toVar i) + where + go !j !toSkip = if C.getCount (C.lengthMV mv) <= j then pure NothingFound else do + w <- C.readMV mv (C.Count j) + if + | S.test pol w -> go (j + 1) toSkip + | 0 == toSkip -> pure $ JustFound (C.Count j) + | otherwise -> go (j + 1) (toSkip - 1) + +findIthActiveInV :: + C.Vector base SlotE S + -> C.Index base ActiveSlotE + -> MaybeFound base +findIthActiveInV = + findIthEmptyInV S.inverted + +----- + +-- | Trivial wrapper around 'countActivesInMV' +countActivesInV :: + POL pol + => proxy pol + -> C.Vector base SlotE S + -> C.Size base (PreImage pol ActiveSlotE) +countActivesInV pol v = + C.toSize $ runST $ C.unsafeThawV v >>= \mv -> countActivesInMV pol mv + +-- | The number of active slots in the vector +countActivesInMV :: + POL pol + => proxy pol + -> C.MVector base SlotE s S + -> ST s (C.Var base (PreImage pol ActiveSlotE)) +countActivesInMV pol mv = + MV.foldl' + (\acc w -> if S.test pol w then acc + 1 else acc) + 0 + mv' + where + C.MVector mv' = mv + +----- + +-- | A density of active slots in a given window +-- +-- @pol@ is the polarity to use for the active slots +-- +-- TODO: rename to SomeDensity +data SomeDensityWindow pol = + forall slidingWindow. + SomeDensityWindow + !(C.Var slidingWindow (PreImage pol ActiveSlotE)) -- ^ Numerator: The active slots + !(C.Size slidingWindow SlotE) -- ^ Denominator: The total amount of slots + +instance Eq (SomeDensityWindow pol) where + SomeDensityWindow l1 l2 == SomeDensityWindow r1 r2 = + C.forgetBase l1 == C.forgetBase r1 && C.forgetBase l2 == C.forgetBase r2 + +instance Show (SomeDensityWindow pol) where + showsPrec p (SomeDensityWindow numer denom) = + Some.runShowsPrec p + $ Some.showCtor (SomeDensityWindow @pol) "SomeDensityWindow" + `Some.showArg` numer + `Some.showArg` denom + +instance Read (SomeDensityWindow pol) where + readPrec = + Some.runReadPrec + $ Some.readCtor SomeDensityWindow "SomeDensityWindow" + <*> Some.readArg + <*> Some.readArg + +-- | @fillInWindow pol (SomeDensityWindow k s) g mv@ mutates @mv@ to ensure +-- that the vector @take s $ mv ++ repeat (mkActive pol)@ has at least @k@ +-- slots polarizely active. +-- +-- Precondition: @lengthMV mv <= s@ +fillInWindow :: + forall proxy pol base g s. + (POL pol, R.StatefulGen g (ST s)) + => proxy pol + -> SomeDensityWindow pol + -> g + -> C.MVector base SlotE s S + -> ST s (C.Var base (PreImage pol ActiveSlotE)) -- ^ the count after filling +fillInWindow pol (SomeDensityWindow k s) g mv = do + -- how many active polarized slots @actual@ currently has + initialActives <- countActivesInMV pol mv + + let sz = C.lengthMV mv :: C.Size base SlotE + + -- discount the numerator accordingly if @actual@ is smaller than @s@ + -- + -- EG when a full-size @actual@ would reach past the 'Len'. + -- + -- This discount reflects that we (very conservatively!) assume every + -- truncated slot would be an active polarized slot. + let discountedK :: C.Var base (PreImage pol ActiveSlotE) + discountedK = C.Count $ C.getCount k - (C.getCount s - C.getCount sz) -- TODO assert sz <= s + + -- how many active polarized slots need to be added to @actual@ + let adding = C.toVar discountedK - initialActives :: C.Var base (PreImage pol ActiveSlotE) + + -- draw from the empty polarized slots uniformly without replacement, a la Fisher-Yates shuffle + C.forRange_ (C.toSize adding) $ \alreadyAdded -> do + let currentActives = C.toSize $ initialActives + C.toVar alreadyAdded + currentEmpties = S.complementActive pol sz currentActives + + whichEmptyToFlip <- C.uniformIndex currentEmpties g + + slot <- findIthEmptyInMV pol mv whichEmptyToFlip <&> \case + JustFound i -> i + NothingFound -> error "impossible! fillInWindow" + + setMV pol mv slot + + pure $ initialActives + adding + +----- + +testV :: POL pol => proxy pol -> C.Vector base SlotE S -> C.Index base SlotE -> Bool +testV pol mv i = S.test pol (C.readV mv i) + +testMV :: POL pol => proxy pol -> C.MVector base SlotE s S -> C.Index base SlotE -> ST s Bool +testMV pol mv i = do + w <- C.readMV mv i + pure $ S.test pol w + +setMV :: POL pol => proxy pol -> C.MVector base SlotE s S -> C.Index base SlotE -> ST s () +setMV pol mv i = C.writeMV mv i $ S.mkActive pol diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Counting.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Counting.hs new file mode 100644 index 0000000000..fcc63b40b5 --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Counting.hs @@ -0,0 +1,388 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +-- | Very strong types for working with indices, counts, etc within sequences. +module Test.Ouroboros.Consensus.ChainGenerator.Counting ( + -- * general counts + Count (Count) + , forgetBase + , forgetElem + , getCount + , (+) + , (-) + -- * indices and sizes + , Index + , Preds + , Size + , Total + , forRange_ + , lastIndex + , range + , uniformIndex + -- * windows + , Contains (Contains, UnsafeContains) + , Lbl (Lbl) + , SomeWindow (SomeWindow) + , Win + , forgetWindow + , fromWindow + , fromWindowVar + , joinWin + , toWindow + , toWindowVar + , windowLast + , windowSize + , windowStart + , withSuffixWindow + , withTopWindow + , withWindow + , withWindowBetween + -- * vectors + , MVector (MVector) + , Vector (Vector) + , createV + , getMVector + , getVector + , lengthMV + , lengthV + , modifyMV + , readMV + , readV + , replicateMV + , sliceMV + , sliceV + , unsafeThawV + , writeMV + -- * variables + , Other + , Var + , joinVar + , toIndex + , toSize + , toVar + ) where + +import Control.Monad.ST (ST) +import Data.Coerce (coerce) +import Data.Foldable (for_) +import Data.Kind (Type) +import Data.Proxy (Proxy (Proxy)) +import qualified Data.Type.Equality as TypeEq +import qualified Data.Vector.Unboxed as V +import qualified Data.Vector.Unboxed.Mutable as MV +import GHC.OverloadedLabels (IsLabel (fromLabel)) +import Prelude hiding ((+), (-)) +import qualified Prelude +import qualified System.Random.Stateful as R +import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some +import qualified Test.QuickCheck as QC + +----- + +infixl 6 .+, .- + +(.+) :: Int -> Int -> Int +(.+) = (Prelude.+) + +(.-) :: Int -> Int -> Int +(.-) = (Prelude.-) + +----- + +-- | A type-indexed Int to represent counts of elements in containers +-- +-- * @base@ is the type-level name of the container in which we are counting (e.g. @Win (Lbl HonestLbl) skolem1@) +-- * @elem@ is the type-level name of the elements in the container (e.g. 'Test.Ouroboros.Consensus.ChainGenerator.Slot.SlotE') +-- * @which@ is the type-level name of some property that identifies the +-- particular elements that we are counting (e.g. 'Pred', 'Total', or 'Other') +-- +-- TODO: rename @base@ to @container@ +newtype Count (base :: Type) (elem :: kelem) (which :: kwhich) = Count Int + deriving (QC.Arbitrary, Eq, Ord, Read, Show) + +getCount :: Count base elem which -> Int +getCount (Count n) = n + +infixl 6 +, - + +(+) :: Count base elem which -> Int -> Count base elem which +(+) (Count i) j = Count (i .+ j) + +(-) :: Count base elem which -> Int -> Count base elem which +(-) (Count i) j = Count (i .- j) + +forgetBase :: Count base elem which -> Some.Forgotten (Count () elem which) +forgetBase (Count x) = Some.forgotten $ Count x + +forgetElem :: Count base elem which -> Some.Forgotten (Count base () which) +forgetElem (Count x) = Some.forgotten $ Count x + +----- + +-- | Type-level name for counting elements with an index smaller +-- than a given value +data Preds + +-- | Type-level name for counting all elements in a container +data Total + +type Index base elem = Count base elem Preds +type Size base elem = Count base elem Total + +-- | The 'Index' of the rightmost element in the sequence of the given 'Size' +lastIndex :: Size base elem -> Index base elem +lastIndex (Count n) = Count (n .- 1) + +range :: Size base elem -> [Index base elem] +range (Count n) = coerce [0 .. max 0 n .- 1] + +forRange_ :: Applicative f => Size base elem -> (Index base elem -> f a) -> f () +forRange_ c = for_ (range c) + +uniformIndex :: R.StatefulGen g m => Size base elem -> g -> m (Index base elem) +uniformIndex n g = Count <$> R.uniformRM (0, getCount $ lastIndex n) g + +----- + +-- | A human-readable label for a 'Win' +data Lbl lbl = Lbl -- no explicit kind var so that type applications don't + -- need to provide the kind + -- + -- TODO as of GHC 9.0, use a standalone kind signature to + -- declare k as /inferred/ instead of /specified/ +instance (lbl TypeEq.~~ s) => IsLabel s (Lbl lbl) where fromLabel = Lbl + +-- | A type-level name for a window within some containing sequence +-- +-- * @lbl@ is a name component that can be used in multiple names +-- * @skolem@ is a component to differentiate between names which use the +-- same @lbl@ +-- +-- TODO: rename Win to WinLabel +data Win (lbl :: klbl) (skolem :: Type) + +-- | Values of this type describe a window in a sequence of elements. +-- +-- A window is an infix of the sequence, and it is described with an +-- offset and a length or size (the number of elements in the window). +-- +-- * @elem@ is a type-level name of the elements in the containing sequence (e.g. 'Test.Ouroboros.Consensus.ChainGenerator.Slot.SlotE') +-- * @outer@ is a type-level name identifying the containing sequence (e.g. @Win (Lbl HonestLbl) skolem1@) +-- * @inner@ is a type-level name for the window that the value describes (e.g. @Win (Lbl ScgLbl) skolem2@) +-- +-- Note that nothing is said about the containing sequence other +-- than its type name. +-- +-- TODO: rename Contains to Window +data Contains (elem :: kelem) (outer :: Type) (inner :: Type) = + UnsafeContains + !(Index outer elem) -- ^ index of the start of the window as + -- an offset in the containing sequence. + !(Size inner elem) -- ^ size of the window + -- INVARIANT: does not reach past the end of the containing + -- sequence (whatever that end is) + deriving (Eq, Read, Show) + +pattern Contains :: Index outer elem -> Size inner elem -> Contains elem outer inner +pattern Contains x y <- UnsafeContains x y + +{-# COMPLETE Contains #-} + +forgetWindow :: Contains elem outer inner -> Some.Forgotten (Index outer elem, Index outer elem) +forgetWindow win = Some.forgotten (windowStart win, windowLast win) + +-- | Converts an index of a window into an index in the containing sequence. +fromWindow :: Contains elem outer inner -> Index inner elem -> Index outer elem +fromWindow (Contains (Count i) _n) (Count j) = Count (i .+ j) + +-- | Converts a count of elements in a window to a count of elements in the +-- containing sequence. +fromWindowVar :: Contains elem outer inner -> Var inner x -> Var outer x +fromWindowVar _ (Count x) = Count x + +toWindow :: Contains elem outer inner -> Index outer elem -> Maybe (Index inner elem) +{-# INLINE toWindow #-} +toWindow (Contains (Count i) (Count n)) (Count j) = if i <= j && j < i .+ n then Just (Count (j .- i)) else Nothing + +toWindowVar :: Contains elem outer inner -> Var outer x -> Var inner x +toWindowVar _ (Count x) = Count x + +windowSize :: Contains elem outer inner -> Size inner elem +windowSize (Contains _i (Count n)) = Count n + +windowStart :: Contains elem outer inner -> Index outer elem +windowStart win = fromWindow win (Count 0) + +windowLast :: Contains elem outer inner -> Index outer elem +windowLast win = fromWindow win $ lastIndex $ windowSize win + +-- | 'Contains' is a 'Data.Semigroupoid.Semigroupoid' +joinWin :: Contains elem outer mid -> Contains elem mid inner -> Contains elem outer inner +{-# INLINE joinWin #-} +joinWin win win2 = UnsafeContains (fromWindow win $ windowStart win2) (windowSize win2) + +data SomeWindow (lbl :: klbl) (outer :: Type) (elem :: kelem) = + forall (skolem :: Type). + SomeWindow + !(Proxy skolem) + !(Contains elem outer (Win lbl skolem)) + +instance Eq (SomeWindow lbl outer elem) where + SomeWindow _l1 l2 == SomeWindow _r1 r2 = + forgetWindow l2 == forgetWindow r2 + +instance Show (SomeWindow lbl outer elem) where + showsPrec p (SomeWindow prx win) = + Some.runShowsPrec p + $ Some.showCtor SomeWindow "SomeWindow" + `Some.showArg` prx + `Some.showArg` win + +instance Read (SomeWindow lbl outer elem) where + readPrec = + Some.runReadPrec + $ Some.readCtor SomeWindow "SomeWindow" + <*> Some.readArg + <*> Some.readArg + +-- | @withWindow outerSz lbl offset innerSz@ is a window of length @innerSz@ +-- with name @lbl@ starting at @offset@ in a sequence with length @outerSz@. +-- +-- If the window doesn't fit in the containing sequence, it is clipped so the +-- resulting (possibly empty) window is contained. +-- +-- Note that the window can spill either on the right if @i + innerSz > outerSz@, +-- or it can spill on the left if @i < 0@, or it can spill on both sides +-- simultaneously. +-- +withWindow :: Size outer elem -> Lbl lbl -> Index outer elem -> Size x elem -> SomeWindow lbl outer elem +withWindow (Count n) _lbl (Count i) (Count m) = + SomeWindow Proxy $ UnsafeContains (Count i') (Count m') + where + i' = min n (max 0 i) + + -- we compute the elements that fall outside the containing sequence + precedingElements = i' .- i + trailingElements = max 0 $ i .+ m .- n + + m' = max 0 $ m .- precedingElements .- trailingElements + +-- | @withWindowBetween outerSz lbl i j@ is the window between indices @i@ +-- and @j@ with name @lbl@ in a containing sequence of length @outerSz@. +withWindowBetween :: Size outer elem -> Lbl lbl -> Index outer elem -> Index outer elem -> SomeWindow lbl outer elem +withWindowBetween n lbl (Count i) (Count j) = withWindow n lbl (Count i) (Count $ j .- i .+ 1) + +-- | @withSuffixWindow outerSz lbl i@ is the window between indices @i@ and the +-- end of the containing sequence of length @outerSz@ with name @lbl@. +withSuffixWindow :: Size outer elem -> Lbl lbl -> Index outer elem -> SomeWindow lbl outer elem +withSuffixWindow n lbl i = withWindow n lbl i (Count $ getCount n .- getCount i) + +-- | @withTopWindow lbl sz k@ passes to @k@ a window of size @sz@ with name +-- @lbl@ at offset @0@ of some containing sequence with a unique name @base@. +withTopWindow :: + Lbl lbl + -> Int + -> (forall base. Proxy base -> SomeWindow lbl base elem -> ans) + -> ans +withTopWindow _lbl n k = + k Proxy $ SomeWindow Proxy $ UnsafeContains (Count 0) (Count n) + +----- + +-- | Same indices as 'Index' and 'Size' +newtype Vector base elem a = Vector (V.Vector a) + deriving (Eq, Read, Show) + +instance (QC.Arbitrary a, V.Unbox a) => QC.Arbitrary (Vector base elem a) where + arbitrary = (Vector . V.fromList) <$> QC.arbitrary + shrink = map (Vector . V.fromList) . QC.shrink . V.toList . getVector + +getVector :: Vector base elem a -> V.Vector a +getVector (Vector v) = v + +lengthV :: V.Unbox a => Vector base elem a -> Size base elem +lengthV = Count . V.length . getVector + +sliceV :: MV.Unbox a => Contains elem outer inner -> Vector outer elem a -> Vector inner elem a +{-# INLINE sliceV #-} +sliceV win (Vector v) = + Vector $ V.slice i n v + where + Count i = fromWindow win (Count 0) + Count n = windowSize win + +unsafeThawV :: MV.Unbox a => Vector base elem a -> ST s (MVector base elem s a) +unsafeThawV (Vector v) = MVector <$> V.unsafeThaw v + +createV :: MV.Unbox a => (forall s. ST s (MVector base elem s a)) -> Vector base elem a +createV m = Vector $ V.create (getMVector <$> m) + +-- | A type-indexed vector carrying values of a container +-- +-- * @base@ is a type-level name identifying the container (e.g. @Win (Lbl HonestLbl) skolem1@) +-- * @elem@ is a type-level name of the elements in the container (e.g. 'Test.Ouroboros.Consensus.ChainGenerator.Slot.SlotE') +-- +newtype MVector base elem s a = MVector (MV.MVector s a) + +getMVector :: MVector base elem s a -> MV.MVector s a +getMVector (MVector mv) = mv + +lengthMV :: MV.Unbox a => MVector base elem s a -> Size base elem +lengthMV = Count . MV.length . getMVector + +sliceMV :: MV.Unbox a => Contains elem outer inner -> MVector outer elem s a -> MVector inner elem s a +{-# INLINE sliceMV #-} +sliceMV win (MVector mv) = + MVector $ MV.slice i n mv + where + Count i = fromWindow win (Count 0) + Count n = windowSize win + +replicateMV :: MV.Unbox a => Size base elem -> ST s a -> ST s (MVector base elem s a) +replicateMV (Count n) m = fmap MVector $ MV.replicateM n m + +readMV :: MV.Unbox a => MVector base elem s a -> Index base elem -> ST s a +writeMV :: MV.Unbox a => MVector base elem s a -> Index base elem -> a -> ST s () +modifyMV :: MV.Unbox a => MVector base elem s a -> (a -> a) -> Index base elem -> ST s () + +readMV (MVector mv) (Count i) = MV.read mv i +writeMV (MVector mv) (Count i) x = MV.write mv i x +modifyMV (MVector mv) f (Count i) = MV.modify mv f i + +readV :: MV.Unbox a => Vector base elem a -> Index base elem -> a +readV (Vector v) (Count i) = v V.! i + +----- + +-- | A type-level name for counting elements without a specific property +data Other + +deriving instance (which TypeEq.~~ Other) => Enum (Count base elem which) +deriving instance (which TypeEq.~~ Other) => Num (Count base elem which) + +type Var base elem = Count base elem Other + +-- | For initializing a 'Var' +toVar :: Count base elem which -> Var base elem +toVar (Count n) = Count n + +-- | When the 'Var' has become a 'Size' +toSize :: Var base elem -> Size base elem +toSize (Count n) = Count n + +-- | When the 'Var' has become a 'Index' +toIndex :: Var base elem -> Index base elem +toIndex (Count i) = Count i + +-- | A count of things in an element can be lifted to a count of things in a vector +joinVar :: MVector base elem s a -> Var a x -> Var base x +joinVar _ = \(Count n) -> Count n diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Honest.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Honest.hs new file mode 100644 index 0000000000..8ad9a62e77 --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Honest.hs @@ -0,0 +1,523 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +module Test.Ouroboros.Consensus.ChainGenerator.Honest ( + -- * Generating + ChainSchema (ChainSchema) + , CheckedHonestRecipe (UnsafeCheckedHonestRecipe, chrScgDensity, chrWin) + , HonestLbl + , HonestRecipe (HonestRecipe) + , NoSuchHonestChainSchema (BadKcp, BadLen) + , SomeCheckedHonestRecipe (SomeCheckedHonestRecipe) + , SomeHonestChainSchema (SomeHonestChainSchema) + , checkHonestRecipe + , countChainSchema + , uniformTheHonestChain + -- * Testing + , HonestChainViolation (BadCount, BadScgWindow, BadLength) + , ScgLbl + , ScgViolation (ScgViolation, scgvPopCount, scgvWindow) + , checkHonestChain + , prettyChainSchema + , prettyWindow + ) where + +import Control.Monad (void, when) +import qualified Control.Monad.Except as Exn +import Data.Monoid (Endo (Endo, appEndo)) +import Data.Proxy (Proxy (Proxy)) +import Data.STRef (newSTRef, readSTRef, writeSTRef) +import qualified Data.Vector.Unboxed as V +import Prelude hiding (words) +import qualified System.Random.Stateful as R +import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import Test.Ouroboros.Consensus.ChainGenerator.Params (Asc, + Delta (Delta), Kcp (Kcp), Len (Len), Scg (Scg)) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S +import Test.Ouroboros.Consensus.ChainGenerator.Slot + (E (ActiveSlotE, SlotE), S) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some + +----- + +-- | The argument of checkHonestRecipe' +data HonestRecipe = HonestRecipe !Kcp !Scg !Delta !Len + deriving (Eq, Read, Show) + +-- | The argument of 'uniformTheHonestChain' and the output of 'checkHonestRecipe' +-- +-- * @base@ the type-level name of the top-level timeline +-- * @hon@ the type-level name of the honest chain's slot interval +-- +-- TODO: Rename to CheckedHonestSchemaSpec +data CheckedHonestRecipe base hon = UnsafeCheckedHonestRecipe { + -- | Desired density + chrScgDensity :: !(BV.SomeDensityWindow S.NotInverted) + , -- | Window in the @base@ containing sequence where the density should be + -- ensured + chrWin :: !(C.Contains SlotE base hon) + } + deriving (Eq, Read, Show) + +-- TODO: Rename to SomeCheckedHonestSpec +data SomeCheckedHonestRecipe = + forall base hon. + SomeCheckedHonestRecipe + !(Proxy base) + !(Proxy hon) + !(CheckedHonestRecipe base hon) + +instance Show SomeCheckedHonestRecipe where + showsPrec p (SomeCheckedHonestRecipe base hon recipe) = + Some.runShowsPrec p + $ Some.showCtor SomeCheckedHonestRecipe "SomeCheckedHonestRecipe" + `Some.showArg` base + `Some.showArg` hon + `Some.showArg` recipe + +instance Read SomeCheckedHonestRecipe where + readPrec = + Some.runReadPrec + $ Some.readCtor SomeCheckedHonestRecipe "SomeCheckedHonestRecipe" + <*> Some.readArg + <*> Some.readArg + <*> Some.readArg + +data NoSuchHonestChainSchema = + -- | must have @0 <= 'Kcp' <= 'Scg'@ + BadKcp + | + -- | 'Len' must be positive + BadLen + deriving (Eq, Read, Show) + +-- | Checks whether the given 'HonestRecipe' determines a valid input to +-- 'uniformTheHonestChain' +checkHonestRecipe :: HonestRecipe -> Exn.Except NoSuchHonestChainSchema SomeCheckedHonestRecipe +checkHonestRecipe recipe = do + when (l <= 0) $ Exn.throwError BadLen + + when (k < 0 || s < k) $ Exn.throwError BadKcp + + C.withTopWindow (C.Lbl @HonestLbl) l $ \base topWindow -> do + C.SomeWindow Proxy slots <- pure topWindow + + pure $ SomeCheckedHonestRecipe base Proxy UnsafeCheckedHonestRecipe { + chrScgDensity = BV.SomeDensityWindow (C.Count k) (C.Count s) + , + chrWin = slots + } + where + HonestRecipe (Kcp k) (Scg s) (Delta _d) (Len l) = recipe + +----- + +-- | The leader schedule of an honest /chain/ +-- +-- The represented chain grows by one block per active slot. A different data +-- type would represent a leader schedule in which leaders do not necessarily +-- extend the block from the previous active slot. +-- +-- INVARIANT: at least one active slot +data ChainSchema base inner = + ChainSchema + !(C.Contains SlotE base inner) + !(C.Vector inner SlotE S) + deriving (Eq, Read, Show) + +countChainSchema :: ChainSchema base inner -> C.Size inner ActiveSlotE +countChainSchema sched = + BV.countActivesInV S.notInverted v + where + ChainSchema _slots v = sched + +prettyWindow :: C.Contains SlotE base inner -> String -> String +prettyWindow win s = + -- for example, i=0 n=1 should be "[)" + replicate i ' ' <> "[" <> replicate (n - theOpenBracket) ' ' <> ")" <> s + where + C.Count i = C.windowStart win + C.Count n = C.windowSize win + + theOpenBracket = 1 + +prettyChainSchema :: + forall base inner. + ChainSchema base inner + -> String + -> [String] +prettyChainSchema sched s = + map (replicate (C.getCount shift) ' ' <>) + $ [ prettyWindow slots s + , V.foldMap (Endo . S.showS) (C.getVector v) `appEndo` "" + ] + where + ChainSchema slots v = sched + + shift = C.windowStart slots + +data SomeHonestChainSchema = + forall base hon. + SomeHonestChainSchema + !(Proxy base) + !(Proxy hon) + !(ChainSchema base hon) + +instance Show SomeHonestChainSchema where + showsPrec p (SomeHonestChainSchema base hon sched) = + Some.runShowsPrec p + $ Some.showCtor SomeHonestChainSchema "SomeHonestChainSchema" + `Some.showArg` base + `Some.showArg` hon + `Some.showArg` sched + +instance Read SomeHonestChainSchema where + readPrec = + Some.runReadPrec + $ Some.readCtor SomeHonestChainSchema "SomeHonestChainSchema" + <*> Some.readArg + <*> Some.readArg + <*> Some.readArg + +data HonestLbl + +data RemainingHcgWindowsLbl + +{- TODO + +Our original intent was for 'uniformTheHonestChain' to generate a chain +according to the given 'Asc' and then toggle /as few as possible/ empty slots +to active such that the Chain Growth Assumption is satisfied. + +However, the minimality of that is very difficult to ensure, in general. It's +an integer linear programming (ILP) problem, where: + + * Each empty slot in a sparse window is a binary aka ("zero-one") variable. + + * The objective is to minimize the sum of those binary variables. + + * Each sparse window imposes a minimum bound on the number of variables in + that window that must be toggled. + +Because all of the coefficients in the objective (the minimization) and each +constraint (one per window) are positive, this is a /set covering problem/: +each variable is an empty slot in some number of sparse windows, and we want to +choose as few such slots as possible such that no sparse window remain. + +Moreover, each window needs a different number of slots (because some windows +may be more sparse than others). Because some windows may require multiple +empty slots, this is a /set multi-covering problem/. + +Lastly, we can only toggle an empty slot once (recall that it's a /zero-one/ +variable), so this is a /set multi-cover with multiplicity constraints +problem/. + +After some searching, I found this reference + + * Qiang-Sheng Hua, Yuexuan Wang, Dongxiao Yu, Francis C. M. Lau: Dynamic + programming based algorithms for set multicover and multiset multicover + problems. Theor. Comput. Sci. 411(26-28): 2467-2474 (2010) + +which includes the claim "[...] we give the first known exact algorithm for the +MSMC or the SMC with multiplicity constraints problem". + +It /may/ be the case that our problem is particularly degenerate, and so easier +to solve. In particular, our variables are binary, their coefficients in the +constraints are binary, and in fact our constraints form a banded matrix. Only +the lower bound of each constraint can be greater than 1. But I have not yet +recognized how to do it. + +The closest I have come to a solution is an incremental algorithm that toggles +one empty slot at a time. I /think/ the completeness of this algorithm requires +that the next toggle is one of the empty slots that occurs in the most number +of sparse windows. However, I have not proved that. Moreover, even if it is +true, a counterexample proves that choosing an arbitrary such slot is not +sufficient: + +> A B C +> ----- ----- +> 01110111011101110 +> ----- ----- + +In this example, only slots A, B, and C occur in two sparse windows, so those +are the candidates for the next toggle by my conjecture. If we suppose that +each window is only missing one active slot (eg need 4 actives per 5 slots), +then toggling B would require three toggles in total, whereas toggling A and C +would solve the problem with just two toggles. + +-} + +-- | A 'ChainSchema' that satisfies 'checkHonestChain' +-- +-- This generator proceeds in three stages to create a random schema that +-- satisfies the requirement of at least @k@ blocks in every @s@ slots. +-- +-- * It begins by drawing a sample of length 'Len' from the Bernoulli process +-- induced by the active slot coefficient 'Asc', just like in Praos. (IE +-- 'Len' many i.i.d. samples from @Uniform(asc)@). +-- * It then visits the first window in that sampled vector. If it has less +-- than @k@ active slots, the generator randomly toggles empty slots to be +-- active until the window contains exactly @k@ active slots. +-- * It then visits the rest of the windows in oldest-to-youngest order. Each +-- window must contain at least @k-1@ active slots when visited, since it +-- shares all but its youngest slot with the previous window, which was +-- already visited. In particular, when the window contains only @k-1@ active +-- slots, that youngest slot must be empty, and so the generator will toggle +-- it, thereby re-establishing the required density. +-- +-- NOTE: This process may add more active slots to the initial sampled vector +-- than strictly necessary---ensuring the minimum number of toggles would be an +-- integer programming optimization problem as far as we can tell. We have +-- settled for this relatively simple algorithm that approaches the minimal +-- number of toggled slots (TODO calculate how tight the bounds are). +-- +-- NOTE: When visting windows after the first, only the youngest slot can be +-- toggled. If we activated any other slot in the sliding window, then older +-- windows, which already have at least @k@ active slots, would unnecessarily +-- end up with even more active slots. +-- +-- NOTE: The larger 'Asc' is, the more active slots there will be when sampling +-- from the Bernoulli process. When 'Asc' is much larger than @k/s@ the sample +-- will require toggling very few additional slots. +-- +-- NOTE: When no 'Asc' value is provided, we start with a vector with no active +-- slots, and the second phasesliding window causes the first window to end up with @k@ +-- active slots in a pattern that is then repeated exactly for the rest of the +-- chain. For instance, +-- +-- > k=3, s=6 +-- > +-- > 000000000000000000000000 -- stage 1 +-- > 1 11 -- stage 2 +-- > 1 11 1 11 1 11 -- stage 3 +-- > 101100101100101100101100 -- final +-- +-- > k=3, s=6 +-- > +-- > 000000000000000000000000 -- stage 1 +-- > 111 -- stage 2 +-- > 111 111 111 -- stage 3 +-- > 000111000111000111000111 -- final +-- +-- NOTE: When @'Asc'@ is close to 0, the sample will have a few active slots. +-- In the relatively common case where none of those initially active slots are +-- in the same window, the final schema will be periodic between the active +-- slots from the sample, but the patterns in those intervals may vary. For +-- instance, +-- +-- > k=3, s=6 +-- > +-- > 000000000000010000000000000000001000000000000000000 -- stage 1 +-- > 1 1 1 -- stage 2 +-- > 1 1 1 1 1 11 1 11 1 11 111 111 111 -- stage 3 +-- > 101010101010110010110010110010111000111000111000111 -- final +-- +-- TODO sample from a disjunction of generators that explore interesting +-- boundary conditions. i.e. different windows could use different strategies +-- to fill each of the windows. For instance, we could arrange for some windows +-- to start with empty slots and be dense at the end. +uniformTheHonestChain :: + forall base hon g. + R.RandomGen g + => Maybe Asc -- ^ When @Nothing@, the generated schema has a minimal amount + -- of active slots. Deactivating any of them would violate + -- safety properties. Such a minimal schema is necessarily + -- completely periodic. + -> CheckedHonestRecipe base hon + -> g + -> ChainSchema base hon +{-# INLINABLE uniformTheHonestChain #-} +uniformTheHonestChain mbAsc recipe g0 = wrap $ C.createV $ do + BV.SomeDensityWindow (C.Count (toEnum -> numerator)) (C.Count (toEnum -> denominator)) <- pure chrScgDensity + let _ = numerator :: C.Var hon ActiveSlotE + _ = denominator :: C.Var hon SlotE + + g <- R.newSTGenM g0 + + -- randomly initialize the bitstring + mv <- C.replicateMV sz $ case mbAsc of + Nothing -> pure $ S.mkActive S.inverted + Just asc -> S.genS asc `R.applySTGen` g + + -- /always/ ensure at least one slot is filled + void $ BV.fillInWindow S.notInverted (C.Count 1 `BV.SomeDensityWindow` sz) g mv + + -- fill the first window up to @k@ + rtot <- do + -- NB @withWindow@ truncates if it would reach past @slots@ + C.SomeWindow Proxy scg <- pure $ C.withWindow sz (C.Lbl @ScgLbl) (C.Count 0) (C.toSize denominator) + tot <- C.fromWindowVar scg <$> BV.fillInWindow S.notInverted chrScgDensity g (C.sliceMV scg mv) + + firstSlot <- BV.testMV S.notInverted mv (C.Count 0) + newSTRef $ (if firstSlot then subtract 1 else id) $ (tot :: C.Var hon ActiveSlotE) + + C.SomeWindow Proxy remainingFullWindows <- do + -- "number of windows that fit" is usually "total - windowWidth + 1", + -- but we do not add the one here because the previous init step above + -- already handled the first window + let numRemainingFullWindows = sz C.- C.getCount denominator + pure $ C.withWindow sz (C.Lbl @RemainingHcgWindowsLbl) (C.Count 1) numRemainingFullWindows + + -- visit all subsequent windows that do not reach beyond @slots@ + -- + -- Visiting a window ensures it has at least k active slots; thus the + -- first window beyond @slots@ will have at least k-1 actives in its actual + -- slots. We assume slots beyond @slots@ are active; thus the first window + -- beyond has at least k active slots. And subsequent windows can only have + -- more active slots than that; thus we don't need to visit windows that + -- reach beyond @slots@. + -- + -- LOOP INVARIANT: @rtot@ contains the count active slots in the current window excluding its youngest slot + -- + -- LOOP INVARIANT: @numerator - 1 <= rtot@ + -- + -- This loop only alters the final slot in each window. That is key to this + -- whole function being a /uniform/ sampler. In particular: + -- + -- * Every excessive empty slot in the first window has an equal chance + -- to be filled in (by the init step above). + -- + -- * If some subsequent window is sparse, then its final slot is filled + -- in (by this loop). It must never fill in any older slot in the + -- window because those slots have already been sampled (either by + -- the init step above or by previous iterations of this loop). + -- + -- * Every slot that was not filled in was drawn from @mbAsc@. + -- + -- * In total: the init step uniformly fills the first window up to + -- @numerator@, and then each slot not in the first window is either + -- forced to @1@ by its preceding @denominator - 1@ samples or is + -- sampled from @mbAsc@. + C.forRange_ (C.windowSize remainingFullWindows) $ \(C.fromWindow remainingFullWindows -> islot) -> do + -- NB will not be truncated + C.SomeWindow Proxy scgSlots <- pure $ C.withWindow sz (C.Lbl @ScgLbl) islot (C.toSize denominator) + + tot <- do + tot <- readSTRef rtot + end <- BV.testMV S.notInverted mv (C.windowLast scgSlots) + pure $ (if end then (+1) else id) $ tot + + let sparse = tot == numerator - 1 -- see LOOP INVARIANT + + tot' <- if not sparse then pure tot else do + BV.setMV S.notInverted mv (C.windowLast scgSlots) + pure numerator + + start <- BV.testMV S.notInverted mv (C.windowStart scgSlots) + writeSTRef rtot $! (if start then subtract 1 else id) $ tot' + + pure mv + where + UnsafeCheckedHonestRecipe { + chrScgDensity + , + chrWin = slots + } = recipe + + sz = C.windowSize slots :: C.Size hon SlotE -- ie 'Len' + + wrap v = ChainSchema slots v + +----- + +data ScgViolation hon = + forall skolem. + ScgViolation { + -- | How many active slots 'scgvWindow' has + scgvPopCount :: !(C.Size (C.Win ScgLbl skolem) ActiveSlotE) + , + -- | The ChainGrowth window that doesn't have enough active slots + scgvWindow :: !(C.Contains SlotE hon (C.Win ScgLbl skolem)) + } + +instance Eq (ScgViolation hon) where + ScgViolation l1 l2 == ScgViolation r1 r2 = + C.forgetBase l1 == C.forgetBase r1 + && + C.forgetWindow l2 == C.forgetWindow r2 + +instance Show (ScgViolation hon) where + showsPrec p (ScgViolation x y) = + Some.runShowsPrec p + $ Some.showCtor ScgViolation "ScgViolation" + `Some.showArg` x + `Some.showArg` y + +instance Read (ScgViolation hon) where + readPrec = + Some.runReadPrec + $ Some.readCtor ScgViolation "ScgViolation" + <*> Some.readArg + <*> Some.readArg + +data HonestChainViolation hon = + -- | The schema does not contain a positive number of active slots + BadCount + | + -- | The schema has some window of 'Scg' slots that contains less than + -- 'Kcp' active slots, even despite optimistically assuming that all slots + -- beyond 'Len' are active + BadScgWindow !(ScgViolation hon) + | + -- | The schema does not span exactly 'Len' slots + BadLength !(C.Size hon SlotE) + deriving (Eq, Read, Show) + +-- | A stability window +data ScgLbl + +-- | Check the Praos Chain Growth assumption +-- +-- Definition of /window/ and /anchored window/. A window is a contiguous +-- sequence of slots. A window anchored at a block starts with the slot +-- immediately after that block. +-- +-- Definition of /Praos Chain Growth Assumption/. We assume the honest chain +-- contains at least @k@ blocks in every window that contains @s@ slots. +-- +-- Definition of /Stability Window/. The @s@ parameter from the Praos Chain +-- Growth property. (At the time of writing, this is @2k@ during Byron and +-- @3k/f@ after Byron on Cardano @mainnet@.) +checkHonestChain :: + forall base hon. + HonestRecipe + -> ChainSchema base hon + -> Exn.Except (HonestChainViolation hon) () +checkHonestChain recipe sched = do + when (C.getCount sz /= l) $ Exn.throwError $ BadLength sz + + do let pc = countChainSchema sched + when (C.toVar pc <= 0) $ Exn.throwError BadCount + + -- every slot is the first slot of a unique stability window + C.forRange_ sz $ \i -> do + -- note that withWindow truncates if the requested slots reach past 'Len' + C.SomeWindow Proxy scg <- pure $ C.withWindow sz (C.Lbl @ScgLbl) i (C.Count s) + + let pc = BV.countActivesInV S.notInverted (C.sliceV scg v) + + -- generously assume that the slots of this stability window that extend past 'Len' are active + let benefitOfTheDoubt = s - C.getCount (C.windowSize scg) + + -- check the density in the stability window + when (C.getCount pc + benefitOfTheDoubt < k) $ do + Exn.throwError $ BadScgWindow $ ScgViolation { + scgvPopCount = pc + , + scgvWindow = scg + } + + where + HonestRecipe (Kcp k) (Scg s) (Delta _d) (Len l) = recipe + + ChainSchema hon v = sched + + sz = C.windowSize hon diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Params.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Params.hs new file mode 100644 index 0000000000..f5480dcc63 --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Params.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE PatternSynonyms #-} + +module Test.Ouroboros.Consensus.ChainGenerator.Params ( + Asc (Asc, UnsafeAsc) + , Delta (Delta) + , Kcp (Kcp) + , Len (Len) + , Scg (Scg) + , ascFromBits + , ascFromDouble + , ascVal + ) where + +import qualified Data.Bits as B + +----- + +-- | The Δ parameter of the Praos theorems and so also of the Praos Race +-- Assumption +-- +-- ASSUMPTION: If an honest block @b@ is minted at the start of slot @x@, then +-- every (healthy) honest node will have selected a chain no worse than @b@ by +-- the onset of slot @x + Δ + 1@. +-- +-- NOTE: If @Δ=0@, then the best block minted in each slot is selected by every +-- (healthy) honset before the onset of the next slot. +-- +-- NOTE: If the honest block @k+1@ after its intersection with an alternative +-- chain was minted in slot @x@, then the alternative block @k+1@ after the +-- intersection can be minted no sooner than slot @x + Δ + 1@. Thus @x + Δ@ is +-- the youngest slot in the Praos Race Window. +newtype Delta = Delta Int + deriving (Eq, Ord, Show, Read) + +-- | The maximum length of any leader schedule +-- +-- This can be interpreted as the /end of time/, the final moment simulated +-- during a test. +newtype Len = Len Int + deriving (Eq, Ord, Show, Read) + +-- | The @k@ parameter of the Praos Common Prefix property +-- +-- Also known as the 'Ouroboros.Consensus.Config.SecurityParam.SecurityParam'. +newtype Kcp = Kcp Int + deriving (Eq, Ord, Show, Read) + +-- | The @s@ parameter of the Praos Chain Growth property +-- +-- Also known as the width of the /stability window/. In particular, we assume +-- that an adversarial stake holder cannot drastically increase their rate of +-- election until at least @s@ many slots after the first block on an +-- adversarial chain. +-- +-- In other words: we're assuming that any serious attempt to corrupt the leader +-- schedule would be isolated to a private adversarial chain. +newtype Scg = Scg Int + deriving (Eq, Ord, Show, Read) + +----- + +-- | The /active slot coefficient/ +-- +-- INVARIANT: 0 < x < 1 +-- +-- It's as precise as 'Double', which likely suffices for all of our needs. +newtype Asc = UnsafeAsc Double + deriving (Eq, Read, Show) + +pattern Asc :: Double -> Asc +pattern Asc d <- UnsafeAsc d + +{-# COMPLETE Asc #-} + +ascFromDouble :: Double -> Asc +ascFromDouble d + | d <= 0 = error "Asc must be > 0" + | 1 <= d = error "Asc must be < 1" + | otherwise = UnsafeAsc d + +-- | PRECONDITION: the bits aren't all the same +-- +-- The 'Asc' that equals the fraction @w \/ 2^widthW@. +ascFromBits :: (Enum w, B.FiniteBits w) => w -> Asc +ascFromBits w = ascFromDouble $ toEnum (fromEnum w) / (2 ^ B.finiteBitSize w) + +-- | Interpret 'Asc' as a 'Double' +ascVal :: Asc -> Double +ascVal (Asc x) = x diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/README.md b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/README.md new file mode 100644 index 0000000000..51298d1936 --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/README.md @@ -0,0 +1,14 @@ +The ChainGenerators are documented in the Genesis test plan. +This file is a terse summary. + +These generators yield a schema for "the honest chain" and a schema for one alternative chain that intersects with the honest one. + +A _schema of a chain_ merely indicates in which slots a block exists on that chain. +If there are only empty slots between two active slots in a schema, then it is required that the block in the younger slot extends the block in the older slot. + +This generated pair of schemas will satisfy various concrete properties that the Praos and Genesis papers' theorems imply. +Those properties are always preserved by adding active slots to the honest schema and/or by removing active slots from the alternative schema. +However, it is generally assumed that tests will use the generated schemas without modifiying them---though counterexample shrinkers might rely on the above, for example. + +The generators themselves have some tests in the ouroboros-consensus:test:infra-test suite, but they merely test that the generators are behaving as expected. +(If the "mutation" subset of tests in that suite seem flaky, try increasing the number of seeds attempted per QuickCheck counterexample candidate.) diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/RaceIterator.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/RaceIterator.hs new file mode 100644 index 0000000000..122631782d --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/RaceIterator.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +{- | These functions iteratively produce all race windows in a slot vector. + +The first window is produced by 'init', which unconditionally starts the window at the first slot. +This window can then be passed to 'next', which starts the new window after the first active slot. + +@ +---X--X--X--X-- ... +^ start of window 1 from 'init' + ^ start of window 2 from 'next' + ^ start of window 3 from 'next' +@ + +Valid windows must have @k+1@ active slots. +If the vector doesn't have sufficient slots to meet this condition, 'init' and 'next' return 'Nothing' and we fall back +to 'initConservative' and 'nextConservative', which return windows truncated at the end of time. +-} +module Test.Ouroboros.Consensus.ChainGenerator.RaceIterator ( + Race (Race, UnsafeRace) + , RaceLbl + , init + , initConservative + , next + , nextConservative + ) where + +import Control.Monad (when) +import Data.Proxy (Proxy (Proxy)) +import Prelude hiding (init) +import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import Test.Ouroboros.Consensus.ChainGenerator.Params (Kcp (Kcp)) +import Test.Ouroboros.Consensus.ChainGenerator.Slot + (E (ActiveSlotE, SlotE), S) + +----- + +-- | See 'Race' +data RaceLbl + +-- | A window whose last slot contains the @k+1@st active slot in it +newtype Race base = UnsafeRace (C.SomeWindow RaceLbl base SlotE) + deriving (Eq, Read, Show) + +pattern Race :: C.SomeWindow RaceLbl base SlotE -> Race base +pattern Race x <- UnsafeRace x + +{-# COMPLETE Race #-} + +----- + +-- | Find the nth active slot /in/ the given race window and return the slot number in the context of the entire chain. +-- +-- Race windows are anchored in an active slot, and so could start with an empty or active slot. +nthActiveSlotIndex :: + forall base adv. + C.Index adv ActiveSlotE + -> C.Vector base SlotE S + -> C.Contains SlotE base adv + -> Maybe (C.Index base SlotE) +nthActiveSlotIndex n v raceWin = + -- the given race window has at least k+1 blocks in it and 0<=k, so this pattern can't fail + -- TODO by invariant during construction of the honest chain? + case BV.findIthActiveInV (C.sliceV raceWin v) n of + BV.NothingFound -> Nothing -- would be impossible if we never called next after *Conservative + BV.JustFound slot -> pure $! C.fromWindow raceWin slot + +-- | Yields the race window starting at position 0 of the given +-- vector if the @k+1@ active slot exists. +init :: Kcp -> C.Vector base SlotE S -> Maybe (Race base) +init (Kcp k) v = + -- find the @k+1@st active slot in the given race window + case BV.findIthActiveInV v (C.Count k) of + BV.NothingFound -> Nothing + BV.JustFound kPlus1st -> + Just + $! UnsafeRace + $ C.withWindowBetween + (C.lengthV v) + (C.Lbl @RaceLbl) + (C.Count 0) + kPlus1st + +-- | @initConservative@ creates a window for the whole vector. +initConservative :: C.Vector base SlotE S -> Race base +initConservative v = + let sz = C.lengthV v + in UnsafeRace + $ C.withWindow + sz + (C.Lbl @RaceLbl) + (C.Count 0) + (C.Count $ C.getCount sz) + +data RaceStepLbl + +-- | @next v r@ yields the race window anchored at the first +-- active slot of @r@ if there is an active slot after @r@. +next :: + forall base. + C.Vector base SlotE S + -> Race base + -> Maybe (Race base) +next v (UnsafeRace (C.SomeWindow Proxy raceWin)) = do + next0 <- nthActiveSlotIndex (C.Count 0) v raceWin + + -- find the first active slot /after/ the given race window + -- + -- Race windows end in an active slot. + nextK <- do + C.SomeWindow Proxy searchWin <- + pure + $ C.withWindowBetween + sz + (C.Lbl @RaceStepLbl) + (C.windowLast raceWin) + (C.lastIndex sz) + nthActiveSlotIndex (C.Count 1) v searchWin + + pure $! UnsafeRace $ C.withWindowBetween + sz + (C.Lbl @RaceLbl) + (next0 C.+ 1) + nextK + where + sz = C.lengthV v + +-- | @nextConservative v r@ yields a window anchored at the first +-- active slot of @r@ if it exists, and extending until the end of @v@. +nextConservative :: + forall base. + C.Vector base SlotE S + -> Race base + -> Maybe (Race base) +nextConservative v (UnsafeRace (C.SomeWindow Proxy raceWin)) = do + next0 <- nthActiveSlotIndex (C.Count 0) v raceWin + + -- do not return a Race Window that starts after 'Len' + when (next0 == C.lastIndex sz) Nothing + + pure $! UnsafeRace $ C.withWindowBetween + sz + (C.Lbl @RaceLbl) + (next0 C.+ 1) + (C.lastIndex sz) + where + sz = C.lengthV v diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Slot.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Slot.hs new file mode 100644 index 0000000000..ed76d08600 --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Slot.hs @@ -0,0 +1,163 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +module Test.Ouroboros.Consensus.ChainGenerator.Slot ( + -- * Counting + E (ActiveSlotE, EmptySlotE, SlotE) + , complementActive + , complementEmpty + -- * Slot + , S + , Test.Ouroboros.Consensus.ChainGenerator.Slot.showS + , genS + -- * Reuse + , POL (mkActive, test) + , Pol (Inverted, NotInverted) + , PreImage + , inverted + , notInverted + ) where + +import Data.Coerce (coerce) +import Data.Proxy (Proxy (Proxy)) +import qualified Data.Vector.Generic as VG +import qualified Data.Vector.Generic.Mutable as MVG +import qualified Data.Vector.Unboxed as V +import qualified Data.Vector.Unboxed.Mutable as MV +import qualified System.Random.Stateful as R +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import Test.Ouroboros.Consensus.ChainGenerator.Params (Asc, ascVal) +import qualified Test.QuickCheck as QC + +-- | The activeness of some slot +newtype S = S Bool + deriving (QC.Arbitrary, Eq, Ord, Read, Show) + +-- these instances adapted from +-- https://github.com/minoki/unboxing-vector/blob/3a152014b9660ef1e2885d6b9c66423064223f63/test/Foo.hs#L36-L63 +-- +-- vector 0.13 lets us derive the two big instances; +-- see the top of https://hackage.haskell.org/package/vector-0.13.0.0/docs/Data-Vector-Unboxed.html +-- +-- TODO do so once we eventually bump our dependency on vector to include that feature +newtype instance MV.MVector s S = MV_S (MV.MVector s Bool) +newtype instance V.Vector S = V_S (V.Vector Bool) +instance MVG.MVector MV.MVector S where + basicLength (MV_S mv) = MVG.basicLength mv + basicUnsafeSlice i l (MV_S mv) = MV_S (MVG.basicUnsafeSlice i l mv) + basicOverlaps (MV_S mv) (MV_S mv') = MVG.basicOverlaps mv mv' + basicUnsafeNew l = MV_S <$> MVG.basicUnsafeNew l + basicInitialize (MV_S mv) = MVG.basicInitialize mv + basicUnsafeReplicate i x = MV_S <$> MVG.basicUnsafeReplicate i (coerce x) + basicUnsafeRead (MV_S mv) i = coerce <$> MVG.basicUnsafeRead mv i + basicUnsafeWrite (MV_S mv) i x = MVG.basicUnsafeWrite mv i (coerce x) + basicClear (MV_S mv) = MVG.basicClear mv + basicSet (MV_S mv) x = MVG.basicSet mv (coerce x) + basicUnsafeCopy (MV_S mv) (MV_S mv') = MVG.basicUnsafeCopy mv mv' + basicUnsafeMove (MV_S mv) (MV_S mv') = MVG.basicUnsafeMove mv mv' + basicUnsafeGrow (MV_S mv) n = MV_S <$> MVG.basicUnsafeGrow mv n +instance VG.Vector V.Vector S where + basicUnsafeFreeze (MV_S mv) = V_S <$> VG.basicUnsafeFreeze mv + basicUnsafeThaw (V_S v) = MV_S <$> VG.basicUnsafeThaw v + basicLength (V_S v) = VG.basicLength v + basicUnsafeSlice i l (V_S v) = V_S (VG.basicUnsafeSlice i l v) + basicUnsafeIndexM (V_S v) i = coerce <$> VG.basicUnsafeIndexM v i + basicUnsafeCopy (MV_S mv) (V_S v) = VG.basicUnsafeCopy mv v + elemseq (V_S v) x y = VG.elemseq v (coerce x) y +instance V.Unbox S + +----- + +genS :: R.RandomGen g => Asc -> g -> (S, g) +genS asc g = + bool `seq` (S bool, g') + where + (q, g') = R.random g -- note 0 <= q <= 1 + + bool = q < ascVal asc + +showS :: S -> ShowS +showS (S bool) = showChar $ if bool then '1' else '0' + +----- + +-- | Type-level names for the different kinds of slots counted in this library +-- +-- The data constructors of this type are used in promoted form with +-- @-XDataKinds@. +-- +data E = + -- | Active slots must be filled on the honest chain and may be filled on an alternative chain. + ActiveSlotE + -- | Empty slots may be filled on the honest chain and must not be filled on an alternative chain. + | EmptySlotE + -- | @SlotE@ is the union of 'ActiveSlotE' and 'EmptySlotE' + | SlotE + +inverted :: Proxy Inverted +inverted = Proxy + +notInverted :: Proxy NotInverted +notInverted = Proxy + +-- | The polarity of a type +-- +-- This is used to toggle how functions in this library interact with vectors +-- of 'S' values. +-- +-- If the polarity is 'Inverted', then the function will treat all 'S' values as +-- if they were first complemented. +-- +-- The 'PreImage' type family does the corresponding parameterization of +-- 'ActiveSlotE' and 'EmptySlotE' at the type level. +-- +-- NOTE: No 'S' value is ever actually complemented because of 'Inverted', but +-- the functions parameterized by 'pol' will treat them as if they were. +data Pol = Inverted | NotInverted + +-- | Overloaded slot operations for the two polarities +class POL (pol :: Pol) where + -- | Make an active slot + mkActive :: proxy pol -> S + -- | Test whether @pol@ maps the given bit to one + test :: proxy pol -> S -> Bool + +-- Both 'complementActive' and 'complementEmpty' are offered for simplicity +-- instead of a generalized function that works in both cases (it would need +-- another proxy parameter for the element type). + +-- | Every slot is either active or empty +complementActive :: + proxy pol + -> C.Size base SlotE + -> C.Count base (PreImage pol ActiveSlotE) which + -> C.Count base (PreImage pol EmptySlotE ) which +complementActive _pol (C.Count n) (C.Count i) = C.Count (n - i) + +-- | Every slot is either active or empty +complementEmpty :: + proxy pol + -> C.Size base SlotE + -> C.Count base (PreImage pol EmptySlotE ) which + -> C.Count base (PreImage pol ActiveSlotE) which +complementEmpty _pol (C.Count n) (C.Count i) = C.Count (n - i) + +instance POL Inverted where + mkActive _pol = coerce False + test _pol = coerce not + +instance POL NotInverted where + mkActive _pol = coerce True + test _pol = coerce + +-- | @PreImage pol e@ is the complement of @e@ if @pol@ is 'Inverted' and simply @e@ if it's 'NotInverted' +type family PreImage (pol :: Pol) (e :: E) where + PreImage Inverted EmptySlotE = ActiveSlotE + PreImage Inverted ActiveSlotE = EmptySlotE + PreImage NotInverted e = e diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Some.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Some.hs new file mode 100644 index 0000000000..dcc78e2183 --- /dev/null +++ b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/ChainGenerator/Some.hs @@ -0,0 +1,108 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- | Utilities that avoid repetition when declaring instances for types +-- that are not amenable to @deriving@, and in particular, types with +-- existential quantification. +-- +-- For existentials that only quantify one type variable, this module's +-- functionality is mostly superseded by the @some@ Hackage package. However, +-- this library involves many existentials that quantify multiple variables. +-- That can be shoehorned into @some@ with some encoding, but I believe this +-- module's weight is preferable to the overhead of using that encoding in our +-- existential data types' declarations. +module Test.Ouroboros.Consensus.ChainGenerator.Some ( + -- * 'Show' + runShowsPrec + , showArg + , showCtor + , showCtorProxy + -- * 'Read' + , Read.readPrec + , readArg + , readCtor + , runReadPrec + -- * 'Eq' + , Forgotten + , forgotten + ) where + +import Data.Kind (Constraint, Type) +import Data.Proxy (Proxy (Proxy)) +import Data.Void (Void) +import qualified GHC.Read as Read +import GHC.TypeLits (Symbol) +import qualified GHC.TypeLits as TE +import qualified Text.ParserCombinators.ReadPrec as Read +import qualified Text.Read.Lex as Read + +----- + +type family AbsError (s :: Symbol) (a :: Type) :: Void where + AbsError s a = TE.TypeError ( + TE.Text "You have accidentaly applied `" + TE.:<>: TE.Text s + TE.:<>: TE.Text "' to a non-concrete type: " + TE.:<>: TE.ShowType a + ) + +type family NoFun (s :: Symbol) (a :: Type) (absError :: Void) :: Constraint where + NoFun s (a -> b) abs = TE.TypeError ( + TE.Text "You have accidentaly applied `" + TE.:<>: TE.Text s + TE.:<>: TE.Text "' to a function type: " + TE.:<>: TE.ShowType (a -> b) + ) + NoFun s t abs = () + +----- + +newtype ShowBuilder a = ShowBuilder ShowS + +infixl 1 `showArg` + +-- | The context is satisfied by any type @a@ that is manifestly apart from @->@ +runShowsPrec :: NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) => Int -> ShowBuilder a -> ShowS +runShowsPrec p (ShowBuilder x) = showParen (p >= 11) x + +showCtor :: a -> String -> ShowBuilder a +showCtor a s = + showCtorProxy (toProxy a) s + where + toProxy :: a -> Proxy a + toProxy = const Proxy + +showCtorProxy :: proxy a -> String -> ShowBuilder a +showCtorProxy _a s = ShowBuilder $ showString s + +showArg :: Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b +ShowBuilder l `showArg` r = ShowBuilder $ l . showString " " . showsPrec 11 r + +----- + +newtype ReadBuilder a = ReadBuilder (Read.ReadPrec a) + deriving (Applicative, Functor) + +-- | The context is satisfied by any type @a@ that is manifestly apart from @->@ +runReadPrec :: NoFun "runReadPrec" a (AbsError "runReadPrec" a) => ReadBuilder a -> Read.ReadPrec a +runReadPrec (ReadBuilder x) = Read.parens $ Read.prec 10 x + +readCtor :: a -> String -> ReadBuilder a +readCtor a s = ReadBuilder $ a <$ Read.expectP (Read.Ident s) + +readArg :: Read a => ReadBuilder a +readArg = ReadBuilder $ Read.step Read.readPrec + +----- + +-- | An opaque type that only allows for 'Eq' and human inspection +newtype Forgotten a = Forgotten a + deriving (Eq, Show) + +forgotten :: a -> Forgotten a +forgotten = Forgotten diff --git a/ouroboros-consensus/test/infra-test/Main.hs b/ouroboros-consensus/test/infra-test/Main.hs index 0f16950be5..78792f4060 100644 --- a/ouroboros-consensus/test/infra-test/Main.hs +++ b/ouroboros-consensus/test/infra-test/Main.hs @@ -13,7 +13,8 @@ module Main (main) where import qualified Ouroboros.Consensus.Util.Tests (tests) -import Test.Tasty +import qualified Test.Ouroboros.Consensus.ChainGenerator.Tests (tests) +import Test.Tasty (TestTree, testGroup) import qualified Test.Util.ChainUpdates.Tests (tests) import qualified Test.Util.Schedule.Tests (tests) import qualified Test.Util.Split.Tests (tests) @@ -27,6 +28,7 @@ tests :: TestTree tests = testGroup "test-infra" [ Ouroboros.Consensus.Util.Tests.tests + , Test.Ouroboros.Consensus.ChainGenerator.Tests.tests , Test.Util.ChainUpdates.Tests.tests , Test.Util.Schedule.Tests.tests , Test.Util.Split.Tests.tests diff --git a/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests.hs b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests.hs new file mode 100644 index 0000000000..af8638ca3c --- /dev/null +++ b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests.hs @@ -0,0 +1,16 @@ +module Test.Ouroboros.Consensus.ChainGenerator.Tests (tests) where + +import qualified Test.Ouroboros.Consensus.ChainGenerator.Tests.Adversarial as A +import qualified Test.Ouroboros.Consensus.ChainGenerator.Tests.BitVector as BV +import qualified Test.Ouroboros.Consensus.ChainGenerator.Tests.Counting as C +import qualified Test.Ouroboros.Consensus.ChainGenerator.Tests.Honest as H +import qualified Test.Tasty as TT + +----- + +tests :: TT.TestTree +tests = TT.testGroup "ChainGenerator" $ [] + <> A.tests + <> BV.tests + <> C.tests + <> H.tests diff --git a/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Adversarial.hs b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Adversarial.hs new file mode 100644 index 0000000000..a3787614a3 --- /dev/null +++ b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Adversarial.hs @@ -0,0 +1,477 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE TypeApplications #-} + +module Test.Ouroboros.Consensus.ChainGenerator.Tests.Adversarial (tests) where + +import Control.Applicative ((<|>)) +import qualified Control.Monad.Except as Exn +import Data.Functor ((<&>)) +import Data.Functor.Identity (runIdentity) +import Data.IORef (modifyIORef', newIORef, readIORef, writeIORef) +import Data.Proxy (Proxy (Proxy)) +import Data.Word (Word8) +import qualified System.Random as R +import qualified System.Random.Stateful as R +import qualified System.Timeout as IO (timeout) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Adversarial as A +import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import qualified Test.Ouroboros.Consensus.ChainGenerator.Honest as H +import Test.Ouroboros.Consensus.ChainGenerator.Params (Asc, + Delta (Delta), Kcp (Kcp), Len (Len), Scg (Scg), + ascFromBits) +import qualified Test.Ouroboros.Consensus.ChainGenerator.RaceIterator as RI +import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S +import Test.Ouroboros.Consensus.ChainGenerator.Slot + (E (ActiveSlotE, SlotE)) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some +import qualified Test.Ouroboros.Consensus.ChainGenerator.Tests.Honest as H +import qualified Test.QuickCheck as QC +import Test.QuickCheck.Random (QCGen) +import qualified Test.Tasty as TT +import qualified Test.Tasty.QuickCheck as TT + +----- + +tests :: [TT.TestTree] +tests = [ + TT.testProperty "prop_adversarialChain" prop_adversarialChain + , + TT.localOption (TT.QuickCheckMaxSize 14) $ TT.testProperty "prop_adversarialChainMutation" prop_adversarialChainMutation + ] + +----- + +data SomeTestAdversarial = + forall base hon. + SomeTestAdversarial + !(Proxy base) + !(Proxy hon) + !(TestAdversarial base hon) + +instance Show SomeTestAdversarial where + showsPrec p (SomeTestAdversarial base hon test) = + Some.runShowsPrec p + $ Some.showCtor SomeTestAdversarial "SomeTestAdversarial" + `Some.showArg` base + `Some.showArg` hon + `Some.showArg` test + +instance Read SomeTestAdversarial where + readPrec = + Some.runReadPrec + $ Some.readCtor SomeTestAdversarial "SomeTestAdversarial" + <*> Some.readArg + <*> Some.readArg + <*> Some.readArg + +data TestAdversarial base hon = TestAdversarial { + testAscA :: !Asc + , + testAscH :: !Asc + , + testRecipeA :: !(A.AdversarialRecipe base hon) + , + testRecipeA' :: !(A.SomeCheckedAdversarialRecipe base hon) + , + testRecipeH :: !H.HonestRecipe + , + testRecipeH' :: !(H.CheckedHonestRecipe base hon) + , + testSeedH :: !QCGen + } + deriving (Read, Show) + +genArPrefix :: H.ChainSchema base hon -> QC.Gen (C.Var hon ActiveSlotE) +genArPrefix schedH = + if C.toVar numChoices < 2 then pure (C.Count 0) {- can always pick genesis -} else do + g <- QC.arbitrary + pure $ C.toVar $ R.runSTGen_ (g :: QCGen) $ C.uniformIndex numChoices + where + H.ChainSchema _slots v = schedH + + numChoices = pc C.- 1 -- can't pick the last active slot + + -- 'H.uniformTheHonestChain' ensures 0 < pc + pc = BV.countActivesInV S.notInverted v + +instance QC.Arbitrary SomeTestAdversarial where + arbitrary = H.unsafeMapSuchThatJust $ do + H.TestHonest { + H.testAsc = testAscH + , + H.testRecipe = testRecipeH + , + H.testRecipe' = someTestRecipeH' + } <- QC.arbitrary + + H.SomeCheckedHonestRecipe Proxy Proxy testRecipeH' <- pure someTestRecipeH' + + testSeedH <- QC.arbitrary + + let arHonest = H.uniformTheHonestChain (Just testAscH) testRecipeH' testSeedH + + arPrefix <- genArPrefix arHonest + + let H.HonestRecipe kcp scg delta _len = testRecipeH + + testRecipeA = A.AdversarialRecipe { + A.arPrefix + , + A.arParams = (kcp, scg, delta) + , + A.arHonest + } + + testAscA <- ascFromBits <$> QC.choose (1 :: Word8, maxBound - 1) + + case Exn.runExcept $ A.checkAdversarialRecipe testRecipeA of + Left e -> case e of + A.NoSuchAdversarialBlock -> pure Nothing + A.NoSuchCompetitor -> error $ "impossible! " <> show e + A.NoSuchIntersection -> error $ "impossible! " <> show e + + Right testRecipeA' -> do + pure $ Just $ SomeTestAdversarial Proxy Proxy $ TestAdversarial { + testAscA + , + testAscH + , + testRecipeA + , + testRecipeA' + , + testRecipeH + , + testRecipeH' + , + testSeedH + } + +-- | No seed exists such that each 'A.checkAdversarialChain' rejects the result of 'A.uniformAdversarialChain' +prop_adversarialChain :: SomeTestAdversarial -> QCGen -> QC.Property +prop_adversarialChain someTestAdversarial testSeedA = runIdentity $ do + SomeTestAdversarial Proxy Proxy TestAdversarial { + testAscA + , + testRecipeA + , + testRecipeA' + } <- pure someTestAdversarial + A.SomeCheckedAdversarialRecipe Proxy recipeA' <- pure testRecipeA' + + let A.AdversarialRecipe { A.arHonest = schedH } = testRecipeA + + schedA = A.uniformAdversarialChain (Just testAscA) recipeA' testSeedA + + let H.ChainSchema winA _vA = schedA + + C.SomeWindow Proxy stabWin <- do + let A.AdversarialRecipe { A.arParams = (_kcp, scg, _delta) } = testRecipeA + pure $ calculateStability scg schedA + + pure $ case Exn.runExcept $ A.checkAdversarialChain testRecipeA schedA of + Right () -> QC.property () + Left e -> case e of + A.BadAnchor{} -> QC.counterexample (show e) False + A.BadCount{} -> QC.counterexample (show e) False + A.BadRace rv -> case rv of + A.AdversaryWonRace { + A.rvAdv = RI.Race (C.SomeWindow Proxy rAdv) + , + A.rvHon = RI.Race (C.SomeWindow Proxy rHon) + } -> id + $ QC.counterexample (advCounterexample schedH schedA winA stabWin rv) + $ QC.counterexample ("arPrefix = " <> show (A.arPrefix testRecipeA)) + $ QC.counterexample ("rvAdv = " <> show rAdv) + $ QC.counterexample ("rvAdv' = " <> show (C.joinWin winA rAdv)) + $ QC.counterexample ("rvHon = " <> show rHon) + $ QC.counterexample ("stabWin = " <> show stabWin) + $ QC.counterexample ("stabWin' = " <> show (C.joinWin winA stabWin)) + $ QC.counterexample (show e) + $ False + +data AdvStabLbl + +-- | Calculate the interval in which the adversary can not yet have accelerated +calculateStability :: Scg -> H.ChainSchema base adv -> C.SomeWindow AdvStabLbl adv SlotE +calculateStability (Scg s) schedA = + C.withWindow (C.windowSize winA) (C.Lbl @AdvStabLbl) (C.Count 0) (C.Count $ firstActive + theBlockItself + s) + where + H.ChainSchema winA vA = schedA + + C.Count firstActive = case BV.findIthEmptyInV S.inverted vA (C.Count 0) of + BV.JustFound x -> x + BV.NothingFound -> error $ "impossible! " <> H.unlines' (H.prettyChainSchema schedA "A") + theBlockItself = 1 + +-- | A nice rendering for failures of 'prop_adversarialChain' +advCounterexample :: + A.ChainSchema base hon + -> A.ChainSchema base adv + -> C.Contains 'SlotE base adv + -> C.Contains 'SlotE adv stab + -> A.RaceViolation hon adv + -> String +advCounterexample schedH schedA winA stabWin rv = + case rv of + A.AdversaryWonRace { + A.rvAdv = RI.Race (C.SomeWindow Proxy rAdv) + , + A.rvHon = RI.Race (C.SomeWindow Proxy rHon) + } -> + H.unlines' $ [] + <> [H.prettyWindow rHon "rHon"] + <> reverse (H.prettyChainSchema schedH "H") + <> H.prettyChainSchema schedA "A" + <> [H.prettyWindow (C.joinWin winA rAdv) "rAdv'"] + <> [H.prettyWindow (C.joinWin winA stabWin) "stabWin'"] + +----- + +-- | A mutation that causes some honest Race Windows to end one slot sooner +data AdversarialMutation = + -- | Increasing 'Delta' by one may cause the adversary to win a race + AdversarialMutateDelta + | + -- | Decreasing 'Kcp' by one may cause the adversary to win a race + AdversarialMutateKcp +{- + | + -- | Decreasing 'Scg' by one may case the adversary to win a (conservative) race + AdversarialMutateScgNeg + | + -- | Increasing 'Scg' by one may case the adversary to accelerate prematurely + AdversarialMutateScgPos +-} + deriving (Bounded, Eq, Enum, Read, Show) + +data TestAdversarialMutation base hon = + TestAdversarialMutation + !H.HonestRecipe + !(H.CheckedHonestRecipe base hon) + !(A.AdversarialRecipe base hon) + !(A.SomeCheckedAdversarialRecipe base hon) + !AdversarialMutation + deriving (Read, Show) + +data SomeTestAdversarialMutation = + forall base hon. + SomeTestAdversarialMutation + !(Proxy base) + !(Proxy hon) + !(TestAdversarialMutation base hon) + +instance Show SomeTestAdversarialMutation where + showsPrec p (SomeTestAdversarialMutation base hon testMut) = + Some.runShowsPrec p + $ Some.showCtor SomeTestAdversarialMutation "SomeTestAdversarialMutation" + `Some.showArg` base + `Some.showArg` hon + `Some.showArg` testMut + +instance Read SomeTestAdversarialMutation where + readPrec = + Some.runReadPrec + $ Some.readCtor SomeTestAdversarialMutation "SomeTestAdversarialMutation" + <*> Some.readArg + <*> Some.readArg + <*> Some.readArg + +mutateAdversarial :: A.AdversarialRecipe base hon -> AdversarialMutation -> A.AdversarialRecipe base hon +mutateAdversarial recipe mut = + A.AdversarialRecipe { A.arHonest, A.arParams = (Kcp k', Scg s', Delta d'), A.arPrefix } + where + A.AdversarialRecipe { A.arHonest, A.arParams = (Kcp k, Scg s, Delta d ), A.arPrefix } = recipe + + (k', s', d') = case mut of + AdversarialMutateDelta -> (k, s, d + 1) + AdversarialMutateKcp -> (k - 1, s, d ) +-- AdversarialMutateScgNeg -> (k, s - 1, d ) +-- AdversarialMutateScgPos -> (k, s + 1, d ) + +instance QC.Arbitrary SomeTestAdversarialMutation where + arbitrary = do + mut <- QC.elements [minBound .. maxBound :: AdversarialMutation] + H.unsafeMapSuchThatJust $ do + (kcp, scg, delta, len) <- H.sized1 $ \sz -> do + (kcp, Scg s, delta) <- H.genKSD + + l <- (+ s) <$> QC.choose (0, 5 * sz) + + pure (kcp, Scg s, delta, Len l) + + let recipeH = H.HonestRecipe kcp scg delta len + + someTestRecipeH' <- case Exn.runExcept $ H.checkHonestRecipe recipeH of + Left e -> error $ "impossible! " <> show (recipeH, e) + Right x -> pure x + + H.SomeCheckedHonestRecipe Proxy Proxy recipeH' <- pure someTestRecipeH' + + seedH <- QC.arbitrary @QCGen + + let arHonest = H.uniformTheHonestChain Nothing recipeH' seedH + + arPrefix <- genArPrefix arHonest + + let recipeA = A.AdversarialRecipe { + A.arPrefix + , + A.arParams = (kcp, scg, delta) + , + A.arHonest + } + + pure $ case Exn.runExcept $ A.checkAdversarialRecipe recipeA of + Left e -> case e of + A.NoSuchAdversarialBlock -> Nothing + A.NoSuchCompetitor -> error $ "impossible! " <> show e + A.NoSuchIntersection -> error $ "impossible! " <> show e + + Right recipeA' -> case Exn.runExcept $ A.checkAdversarialRecipe $ mutateAdversarial recipeA mut of + Left{} -> Nothing + + Right (A.SomeCheckedAdversarialRecipe Proxy mutRecipeA) + -- no mutation matters if the adversary doesn't even + -- have k+1 slots of any kind, let alone active slots + | let A.UnsafeCheckedAdversarialRecipe { + A.carParams = (Kcp k', _scg', _delta') + , + A.carWin + } = mutRecipeA + , C.getCount (C.windowSize carWin) < k' + 1 + -> Nothing + + -- ASSUMPTION: the adversary has k blocks in the first race. + -- + -- If there's no slot after the first race, then the + -- increment of delta cannot make a difference. + -- + -- If there are not at least k+1 slots in the honest schema, + -- then decreasing k cannot make the schema check fail. + | let H.ChainSchema _winH vH = arHonest + , let Len l = len + , let (Kcp k', _scg', Delta d') = A.carParams mutRecipeA + -- slot of the k+1 honest active + , endOfFirstRace <- case BV.findIthEmptyInV S.inverted vH (C.toIndex arPrefix C.+ k') of + BV.NothingFound{} -> l + BV.JustFound x -> C.getCount x + d' + , l <= endOfFirstRace + -> Nothing + + | otherwise -> + Just + $ SomeTestAdversarialMutation Proxy Proxy + $ TestAdversarialMutation + recipeH + recipeH' + recipeA + recipeA' + mut + +-- | There exists a seed such that each 'TestAdversarialMutation' causes +-- 'A.checkAdversarialChain' to reject the result of 'A.uniformAdversarialChain' +-- +-- TODO this did fail after >500,000 tests. Is that amount of flakiness acceptable? +prop_adversarialChainMutation :: SomeTestAdversarialMutation -> QCGen -> QC.Property +prop_adversarialChainMutation (SomeTestAdversarialMutation Proxy Proxy testAdversarialMut) testSeedAsSeed0 = + QC.ioProperty $ do + A.SomeCheckedAdversarialRecipe Proxy recipeA' <- pure someRecipeA' + + counter <- newIORef @Int 0 + catch <- newIORef @(QCGen, [String]) (undefined, []) + + -- we're willing to wait up to 2s to find a failure for each 'TestHonestMutation' + IO.timeout + (2 * 10^(6::Int)) + (go catch counter recipeA' testSeedAsSeed0) >>= \case + Just prop -> pure prop + Nothing -> -- did not find a failure caused by the mutation + ((,) <$> readIORef catch <*> readIORef counter) <&> \((seedA, schedA'), n) -> id + $ QC.counterexample ("n = " <> show n) + $ QC.counterexample + (advMutCounterexample testAdversarialMut mutatedRecipe schedA' seedA) + $ False + where + TestAdversarialMutation recipeH _recipeH' recipeA someRecipeA' mut = testAdversarialMut + + H.HonestRecipe _kcp scg _delta _len = recipeH + + mutatedRecipe = mutateAdversarial recipeA mut + + go catch counter recipeA' testSeedAsSeed = do + modifyIORef' counter (+1) + let -- TODO is this a low quality random stream? Why is there no @'R.Random' 'QCGen'@ instance? + (testSeedA, testSeedAsSeed') = R.split testSeedAsSeed + + schedA = A.uniformAdversarialChain Nothing recipeA' (testSeedA :: QCGen) + m = A.checkAdversarialChain mutatedRecipe schedA + -- We discard tests where the first race ends past the acceleration bound + -- as these race windows are unconstrained + case Exn.runExcept m of + Right () -> do + let A.UnsafeCheckedAdversarialRecipe { A.carWin } = recipeA' + pretty = case calculateStability scg schedA of + C.SomeWindow Proxy win -> + [H.prettyWindow (C.joinWin carWin win) "no accel"] + <> [show (H.countChainSchema schedA)] + writeIORef catch (testSeedA, H.prettyChainSchema schedA "A" <> pretty) + go catch counter recipeA' testSeedAsSeed' + Left e -> case e of + A.BadAnchor{} -> error $ "impossible! " <> show e + A.BadCount{} -> error $ "impossible! " <> show e + A.BadRace{} -> pure $ QC.property () + +----- + +-- | A nice rendering for failures of 'prop_adversarialChainMutation' +advMutCounterexample :: + TestAdversarialMutation base hon + -> A.AdversarialRecipe base hon + -> [String] + -> QCGen + -> String +advMutCounterexample testAdversarialMut mutatedRecipe schedA' seedA = + H.unlines' $ [] + <> [show seedA] + <> [show ch <> " - " <> show arPrefix <> " = " <> show (C.toVar ch - arPrefix) <> " vs " <> show (kcp, mut)] + <> schedH' + <> schedA' + <> go' (((,) False <$> RI.init kcp' vH) <|> Just (True, RI.initConservative vH)) + where + TestAdversarialMutation recipeH _recipeH' recipeA someRecipeA' mut = testAdversarialMut + + H.HonestRecipe kcp _scg _delta _len = recipeH + + A.AdversarialRecipe { A.arHonest, A.arPrefix } = recipeA + + H.ChainSchema _winH vH = arHonest + + A.AdversarialRecipe { A.arParams = (kcp', _scg', _delta') } = mutatedRecipe + + schedH' = H.prettyChainSchema arHonest "H" + + ch = H.countChainSchema arHonest + + next iter = + ((,) False <$> RI.next vH iter) + <|> + ((,) True <$> RI.nextConservative vH iter) + + go' = \case + Nothing -> [] + Just (cons, iter@(RI.Race (C.SomeWindow Proxy win))) + | A.SomeCheckedAdversarialRecipe Proxy recipeA' <- someRecipeA' + , A.UnsafeCheckedAdversarialRecipe { A.carWin } <- recipeA' + , C.windowStart win < C.windowStart carWin + -> go' (next iter) + + | otherwise -> + "" + : head (tail schedH') + : H.prettyWindow win ("raceH" <> if cons then " (conservative)" else "") + : take 2 (tail schedA') diff --git a/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/BitVector.hs b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/BitVector.hs new file mode 100644 index 0000000000..8e0cfef905 --- /dev/null +++ b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/BitVector.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Test.Ouroboros.Consensus.ChainGenerator.Tests.BitVector (tests) where + +import Data.Monoid (Endo (Endo, appEndo)) +import qualified Data.Vector.Unboxed as V +import GHC.Generics (Generic) +import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S +import Test.Ouroboros.Consensus.ChainGenerator.Slot + (E (EmptySlotE, SlotE), POL, PreImage, S) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some +import qualified Test.QuickCheck as QC +import qualified Test.Tasty as TT +import qualified Test.Tasty.QuickCheck as TT + +----- + +tests :: [TT.TestTree] +tests = [ + TT.testProperty "prop_findIthZeroInV" prop_findIthZeroInV + ] + +----- + +data SomeFindTestSetup = forall pol. TestPOL pol => SomeFindTestSetup (FindTestSetup pol) + +instance Show SomeFindTestSetup where + showsPrec p (SomeFindTestSetup testSetup) = + showParen (p >= 11) + $ showString "SomeFindTestSetup " . showsPrec 11 testSetup + +data ProxyPol (pol :: S.Pol) = ProxyPol + deriving (Eq) + +instance TestPOL pol => Show (ProxyPol pol) where + showsPrec p pol = + Some.runShowsPrec p + $ Some.showCtor pol ("ProxyPol :: ProxyPol " <> showPol pol) + +instance TestPOL pol => Read (ProxyPol pol) where + readPrec = + Some.runReadPrec + $ Some.readCtor pol (show pol) + where + pol = ProxyPol :: ProxyPol pol + +data TestB + +instance QC.Arbitrary (ProxyPol pol) where + arbitrary = pure ProxyPol + shrink = QC.shrinkNothing + +data FindTestSetup (pol :: S.Pol) = FindTestSetup { + testPol :: ProxyPol pol + , + -- | INVARIANT @'testIndex' < V.sum (V.map ('countZeros' 'testPol') 'testV')@ + testIndex :: C.Index TestB (PreImage pol EmptySlotE) + , + testV :: C.Vector TestB SlotE S + } + deriving (Eq, Generic, Read, Show) + +instance QC.Arbitrary SomeFindTestSetup where + arbitrary = do + pol <- QC.arbitrary + case pol of + True -> SomeFindTestSetup <$> (QC.arbitrary :: QC.Gen (FindTestSetup S.Inverted )) + False -> SomeFindTestSetup <$> (QC.arbitrary :: QC.Gen (FindTestSetup S.NotInverted)) + + shrink (SomeFindTestSetup x) = [ SomeFindTestSetup y | y <- QC.shrink x ] + +instance TestPOL pol => QC.Arbitrary (FindTestSetup pol) where + arbitrary = do + let testPol = ProxyPol :: ProxyPol pol + + v <- V.fromList <$> QC.arbitrary + + let tc = targetCount testPol v + i <- if 0 == tc then QC.discard else QC.choose (0, tc - 1) + + pure FindTestSetup { + testPol + , + testIndex = C.Count i + , + testV = C.Vector v + } + + shrink x = + [ y + | y <- QC.genericShrink x + , let FindTestSetup {testIndex, testPol, testV} = y + , C.getCount testIndex < targetCount testPol (C.getVector testV) + ] + +targetCount :: TestPOL pol => proxy pol -> V.Vector S -> Int +targetCount pol = V.length . V.filter (not . S.test pol) + +----- + +class POL pol => TestPOL (pol :: S.Pol) where showPol :: proxy pol -> String +instance TestPOL S.Inverted where showPol _pol = "Inverted" +instance TestPOL S.NotInverted where showPol _pol = "NotInverted" + +prop_findIthZeroInV :: SomeFindTestSetup -> QC.Property +prop_findIthZeroInV testSetup = case testSetup of + SomeFindTestSetup FindTestSetup { + testIndex + , + testPol + , + testV + } -> case BV.findIthEmptyInV testPol testV testIndex of + BV.NothingFound -> QC.counterexample "NothingFound" False + BV.JustFound i -> + id + $ QC.counterexample (showPol testPol) + $ QC.counterexample + (let C.Vector v = testV + in + "v =" <> V.foldMap (Endo . S.showS) v `appEndo` "" + ) + $ QC.counterexample ("i = " <> show i) + $ + ( id + $ QC.counterexample "i isn't the position of a post-polarization-0 in w!" + $ BV.testV testPol testV i QC.=== False + ) + QC..&&. + ( let targetsInPrecedingWords = + targetCount testPol $ V.take (C.getCount i) $ C.getVector testV + in + id + $ QC.counterexample "There are not testIndex-many post-polarization-0s preceding i!" + $ targetsInPrecedingWords QC.=== C.getCount testIndex + ) diff --git a/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Counting.hs b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Counting.hs new file mode 100644 index 0000000000..275a74a8f0 --- /dev/null +++ b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Counting.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE DataKinds #-} + +module Test.Ouroboros.Consensus.ChainGenerator.Tests.Counting (tests) where + +import Data.Proxy (Proxy (Proxy)) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C +import qualified Test.QuickCheck as QC +import qualified Test.Tasty as TT +import qualified Test.Tasty.QuickCheck as TT + +----- + +tests :: [TT.TestTree] +tests = [ + TT.testProperty "prop_withWindow" prop_withWindow + ] + +----- + +prop_withWindow :: QC.NonNegative Int -> Int -> Int -> QC.Property +prop_withWindow (QC.NonNegative n) i m = + case C.withWindow (C.Count n) (C.Lbl :: C.Lbl "test") (C.Count i) (C.Count m) of + C.SomeWindow Proxy (C.Contains (C.Count i') (C.Count m')) -> + QC.counterexample (show (i', m')) + $ QC.conjoin [ + if i < 0 + then QC.counterexample "neg i" $ i' QC.=== 0 + else if i > n + then QC.counterexample "too large i" $ i' QC.=== n + else QC.counterexample "nonneg i" $ i' QC.=== i + , if m < 0 + then QC.counterexample "neg m" $ m' QC.=== 0 + else QC.counterexample "nonneg m" $ min (n - 1) i' + m' <= n + ] diff --git a/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Honest.hs b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Honest.hs new file mode 100644 index 0000000000..39fbfae4bf --- /dev/null +++ b/ouroboros-consensus/test/infra-test/Test/Ouroboros/Consensus/ChainGenerator/Tests/Honest.hs @@ -0,0 +1,206 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} + +module Test.Ouroboros.Consensus.ChainGenerator.Tests.Honest ( + -- * Re-use + TestHonest (TestHonest, testAsc, testRecipe, testRecipe') + , genKSD + , sized1 + , unlines' + , unsafeMapSuchThatJust + -- * Tests + , tests + ) where + +import qualified Control.Exception as IO (evaluate) +import qualified Control.Monad.Except as Exn +import Data.Functor ((<&>)) +import Data.Functor.Identity (runIdentity) +import Data.List (intercalate) +import Data.Proxy (Proxy (Proxy)) +import Data.Word (Word8) +import qualified System.Random as R +import qualified System.Timeout as IO (timeout) +import qualified Test.Ouroboros.Consensus.ChainGenerator.Honest as H +import Test.Ouroboros.Consensus.ChainGenerator.Params (Asc, + Delta (Delta), Kcp (Kcp), Len (Len), Scg (Scg), + ascFromBits) +import qualified Test.QuickCheck as QC +import Test.QuickCheck.Random (QCGen) +import qualified Test.Tasty as TT +import qualified Test.Tasty.QuickCheck as TT + +----- + +tests :: [TT.TestTree] +tests = [ + TT.testProperty "prop_honestChain" prop_honestChain + , + TT.testProperty "prop_honestChainMutation" prop_honestChainMutation + ] + +----- + +sized1 :: (Int -> QC.Gen a) -> QC.Gen a +sized1 f = QC.sized (f . succ) + +-- | A generator that checks its own satisfaction +-- +-- WARNING: 'QC.suchThat' et al often causes a /very/ confusing +-- non-termination when its argument is impossible/extremely unlikely +unsafeMapSuchThatJust :: QC.Gen (Maybe a) -> QC.Gen a +unsafeMapSuchThatJust m = QC.suchThatMap m id + +----- + +data TestHonest = TestHonest { + testAsc :: !Asc + , + testRecipe :: !H.HonestRecipe + , + testRecipe' :: !H.SomeCheckedHonestRecipe + } + deriving (Read, Show) + +genKSD :: QC.Gen (Kcp, Scg, Delta) +genKSD = sized1 $ \sz -> do + d <- QC.choose (0, div sz 4) + k <- QC.choose (1, 2 * sz) + s <- (\x -> x + k) <$> QC.choose (0, 3 * sz) -- ensures @k / s <= 1@ + pure (Kcp k, Scg s, Delta d) + +instance QC.Arbitrary TestHonest where + arbitrary = sized1 $ \sz -> do + testAsc <- ascFromBits <$> QC.choose (1 :: Word8, maxBound - 1) + + testRecipe <- do + (kcp, Scg s, delta) <- genKSD + + -- s <= l, most of the time + l <- QC.frequency [(9, (+ s) <$> QC.choose (0, 5 * sz)), (1, QC.choose (1, s))] + + pure $ H.HonestRecipe kcp (Scg s) delta (Len l) + + testRecipe' <- case Exn.runExcept $ H.checkHonestRecipe testRecipe of + Left e -> error $ "impossible! " <> show (testRecipe, e) + Right x -> pure x + + pure TestHonest { + testAsc + , + testRecipe + , + testRecipe' + } + +-- | No seed exists such that each 'H.checkHonestChain' rejects the result of 'H.uniformTheHonestChain' +prop_honestChain :: TestHonest -> QCGen -> QC.Property +prop_honestChain testHonest testSeed = runIdentity $ do + H.SomeCheckedHonestRecipe Proxy Proxy recipe' <- pure testRecipe' + + let sched = H.uniformTheHonestChain (Just testAsc) recipe' testSeed + + QC.counterexample (unlines' $ H.prettyChainSchema sched "H") <$> do + pure $ case Exn.runExcept $ H.checkHonestChain testRecipe sched of + Right () -> QC.property () + Left e -> case e of + H.BadCount{} -> QC.counterexample (show e) False + H.BadLength{} -> QC.counterexample (show e) False + H.BadScgWindow v -> + let str = case v of + H.ScgViolation { + H.scgvWindow = win + } -> H.prettyWindow win "SCGV" + in + id + $ QC.counterexample str + $ QC.counterexample (show e) + $ False + where + TestHonest { + testAsc + , + testRecipe + , + testRecipe' + } = testHonest + +-- 'unlines' adds a trailing newline, this function never does +unlines' :: [String] -> String +unlines' = intercalate "\n" + +----- + +-- | A mutation that minimally increases the threshold density of an 'H.HonestRecipe''s SCG constraint +data HonestMutation = + -- | Increasing 'Kcp' by one increases the SCG numerator + HonestMutateKcp + | + -- | Decreasing 'Scg' by one decreases the SCG denominator + HonestMutateScg + deriving (Eq, Read, Show) + +data TestHonestMutation = + TestHonestMutation + !H.HonestRecipe + !H.SomeCheckedHonestRecipe + !HonestMutation + deriving (Read, Show) + +mutateHonest :: H.HonestRecipe -> HonestMutation -> H.HonestRecipe +mutateHonest recipe mut = + H.HonestRecipe (Kcp k') (Scg s') (Delta d') len + where + H.HonestRecipe (Kcp k) (Scg s) (Delta d) len = recipe + + (k', s', d') = case mut of + HonestMutateKcp -> (k + 1, s, d ) + HonestMutateScg -> (k, s - 1, d ) + +instance QC.Arbitrary TestHonestMutation where + arbitrary = sized1 $ \sz -> unsafeMapSuchThatJust $ do + (kcp, Scg s, delta) <- genKSD + l <- (+ s) <$> QC.choose (0, 5 * sz) + + let testRecipe = H.HonestRecipe kcp (Scg s) delta (Len l) + + testRecipe' <- case Exn.runExcept $ H.checkHonestRecipe testRecipe of + Left e -> error $ "impossible! " <> show (testRecipe, e) + Right x -> pure x + + mut <- QC.elements [HonestMutateKcp, HonestMutateScg] + + pure $ case Exn.runExcept $ H.checkHonestRecipe $ mutateHonest testRecipe mut of + Left{} -> Nothing + Right{} -> Just $ TestHonestMutation testRecipe testRecipe' mut + +-- | There exists a seed such that each 'TestHonestMutation' causes +-- 'H.checkHonestChain' to reject the result of 'H.uniformTheHonestChain' +prop_honestChainMutation :: TestHonestMutation -> QCGen -> QC.Property +prop_honestChainMutation testHonestMut testSeedsSeed0 = QC.ioProperty $ do + H.SomeCheckedHonestRecipe Proxy Proxy recipe' <- pure someRecipe' + + -- we're willing to wait up to 500ms to find a failure for each 'TestHonestMutation' + IO.timeout + (5 * 10^(5::Int)) + (IO.evaluate $ go recipe' testSeedsSeed0) <&> \case + Nothing -> False -- did not find a failure caused by the mutation + Just bool -> bool + where + TestHonestMutation recipe someRecipe' mut = testHonestMut + + mutatedRecipe = mutateHonest recipe mut + + go recipe' testSeedsSeed = + let -- TODO is this a low quality random stream? Why is there no @'R.Random' 'QCGen'@ instance? + (testSeed, testSeedsSeed') = R.split testSeedsSeed + + sched = H.uniformTheHonestChain Nothing recipe' (testSeed :: QCGen) + m = H.checkHonestChain mutatedRecipe sched + in + case Exn.runExcept m of + Right () -> go recipe' testSeedsSeed' + Left e -> case e of + H.BadCount{} -> error $ "impossible! " <> show e + H.BadScgWindow{} -> True + H.BadLength{} -> error $ "impossible! " <> show e