Skip to content

Commit

Permalink
TOSQUASH: small changes, esp to avoid long lines
Browse files Browse the repository at this point in the history
  • Loading branch information
nfrisby committed Mar 27, 2023
1 parent 6fd790d commit 4488c38
Show file tree
Hide file tree
Showing 9 changed files with 262 additions and 134 deletions.
@@ -1,3 +1,4 @@
### Non-Breaking

- Added `ChainGenerators`. See `checkAdversarialChain` and `checkHonestChain` for the invariants these generators ensure.
- Added `ChainGenerators`.
See `checkAdversarialChain` and `checkHonestChain` for the invariants these generators ensure.
Expand Up @@ -133,10 +133,12 @@ checkAdversarialChain recipe adv = do
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
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)

when (C.frWinVar precedingSlots (C.toVar pc) /= arPrefix) $ Exn.throwError $ BadAnchor WrongNumberOfHonestPredecessors
when (C.frWinVar precedingSlots (C.toVar pc) /= arPrefix) $ do
Exn.throwError $ BadAnchor WrongNumberOfHonestPredecessors

checkCount = do
let pc = BV.countActivesInV S.notInverted vA
Expand All @@ -148,7 +150,9 @@ checkAdversarialChain recipe adv = do
youngestStableA :: C.Index adv SlotE
youngestStableA =
case BV.findIthEmptyInV S.inverted vA (C.Count 0) of
BV.JustFound firstActiveA -> firstActiveA C.+ s -- if s=0, then the slot of their block is the youngest stable slot
BV.JustFound firstActiveA ->
-- if s=0, then the slot of their block is the youngest stable slot
firstActiveA C.+ s
BV.NothingFound ->
-- the rest of the function won' force this since there are no
-- adverarial active slots
Expand Down Expand Up @@ -201,7 +205,9 @@ checkAdversarialChain recipe adv = do
-- advance the honest Race Window
| otherwise -> case RI.next vH iterH <|> RI.nextConservative (Scg s) (Delta d) vH iterH of
Just iterH' -> go iterH' iterA
Nothing -> pure () -- there are no remaining honest active slots TODO hpc shows this never executes
Nothing -> pure () -- there are no remaining honest active slots
--
-- TODO hpc shows this never executes

-----

Expand Down Expand Up @@ -267,11 +273,14 @@ data NoSuchAdversarialChainSchedule =
--
-- * @k=0@
--
-- Suppose k=0 and slot x and slot y are two honest active slots with only honest empty slots between them.
-- Suppose k=0 and slot x and slot y are two honest active slots with only
-- honest empty slots between them.
--
-- The Praos Race Assumption 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...
-- 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'
Expand Down Expand Up @@ -420,7 +429,9 @@ uniformAdversarialChain mbAsc recipe g0 = wrap $ C.createV $ do
(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
(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
Expand Down Expand Up @@ -448,11 +459,19 @@ uniformAdversarialChain mbAsc recipe g0 = wrap $ C.createV $ do
(C.windowLast rwin C.+ d)

-- at most k can be active in this race window, so at least size - k must be empty
let req = C.Count $ max 0 $ C.getCount (C.windowSize win) - k :: C.Var (C.Win RaceAssumptionLbl skolem) EmptySlotE
let req =
C.Count
$ max 0
$ C.getCount (C.windowSize win) - k
:: C.Var (C.Win RaceAssumptionLbl skolem) EmptySlotE

-- Discount that basic requirement by the number of zeros already
-- in the untouchable portion of this race window.
let req' = C.Count $ max 0 $ C.getCount req - C.getCount untouchZeroCount :: C.Var (C.Win TouchableLbl skolem2) EmptySlotE
let req' =
C.Count
$ max 0
$ C.getCount req - C.getCount untouchZeroCount
:: C.Var (C.Win TouchableLbl skolem2) EmptySlotE

void $ BV.fillInWindow
S.inverted
Expand All @@ -468,7 +487,8 @@ uniformAdversarialChain mbAsc recipe g0 = wrap $ C.createV $ do
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
-- check whether the slots that are settled as of just
-- now contain the first adversarial active slot
C.SomeWindow Proxy settledSlots <-
pure
$ C.withWindowBetween
Expand All @@ -480,8 +500,10 @@ uniformAdversarialChain mbAsc recipe g0 = wrap $ C.createV $ do
pure $! case mbFound of
BV.NothingFound -> 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.)
-- 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.)
KnownYS $! C.frWin settledSlots x C.+ s C.+ 1
unfillRaces (C.windowLast win C.+ 1) mbYS' iter' g mv

Expand Down
Expand Up @@ -222,7 +222,9 @@ instance Read (SomeWindow lbl outer elem) where
<*> Some.readArg
<*> Some.readArg

-- | Create a fresh 'Window' within a given 'Size' that starts with the given 'Index' and contains however many of the given smaller 'Size' of elements exist within the larger 'Size'
-- | Create a fresh 'Window' within a given 'Size' that starts with the given
-- 'Index' and contains however many of the given smaller 'Size' of elements
-- exist within the larger 'Size'
--
-- NOTE: the requested window size is truncated if necessary to ensure it fits in the containing sequence
--
Expand Down
Expand Up @@ -42,9 +42,11 @@ import qualified Test.QuickCheck as QC
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
-- 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
-- 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)
Expand Down Expand Up @@ -115,11 +117,19 @@ class POL (pol :: Pol) where
test :: proxy pol -> S -> Bool

-- | 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 ::
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 ::
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
Expand Down
Expand Up @@ -41,10 +41,21 @@ 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 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 (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 = ()

-----
Expand Down

0 comments on commit 4488c38

Please sign in to comment.