Issue #473: reworks forAll generators in PVBUMP STS properties to mak…

…e them in line with how UPIEC STS properties will be written

byron/ledger/executable-spec/src/Ledger/Update/Generators.hs

@@ -5,6 +5,11 @@
 module Ledger.Update.Generators
   ( pparams
   , protVer
+  -- PVBUMP judgement contexts
+  , emptyPVUpdateJC
+  , beginningsNoUpdateJC
+  , lastProposalJC
+  -- UPIEC state generators
   , apName
   , apVer
   , metadata
@@ -26,7 +31,7 @@ module Ledger.Update.Generators
   )
 where
 
-import           Control.State.Transition (Environment, State)
+import           Control.State.Transition (Environment, State, Signal)
 import           Data.Map.Strict (Map)
 import           Data.Word (Word64)
 import           Hedgehog
@@ -155,6 +160,27 @@ pvbumpAfter2kEnv =
 pvbumpState :: Gen (State PVBUMP)
 pvbumpState = (,) <$> protVer <*> pparams
 
+-- | Generates a judgement context for the PVBUMP STS for its property #1
+emptyPVUpdateJC :: Gen (Environment PVBUMP, State PVBUMP, Signal PVBUMP)
+emptyPVUpdateJC = (,,)
+  <$> pvbumpEmptyListEnv
+  <*> pvbumpState
+  <*> pure ()
+
+-- | Generates a judgement context for the PVBUMP STS for its property #2
+beginningsNoUpdateJC :: Gen (Environment PVBUMP, State PVBUMP, Signal PVBUMP)
+beginningsNoUpdateJC = (,,)
+  <$> pvbumpBeginningsEnv
+  <*> pvbumpState
+  <*> pure ()
+
+-- | Generates a judgement context for the PVBUMP STS for its property #3
+lastProposalJC :: Gen (Environment PVBUMP, State PVBUMP, Signal PVBUMP)
+lastProposalJC = (,,)
+  <$> pvbumpAfter2kEnv
+  <*> pvbumpState
+  <*> pure ()
+
 -- | Generates an @ApName@
 apName :: Gen ApName
 apName = ApName <$> Gen.element ["byron", "shelley", "praos"]

byron/ledger/executable-spec/test/Ledger/Pvbump/Properties.hs

@@ -19,13 +19,9 @@ import           Ledger.Update (PVBUMP)
 -- in.
 emptyPVUpdate :: Property
 emptyPVUpdate = property $ do
-  judgementContext <-
-    forAll $ fmap TRC $ (,,)
-      <$> G.pvbumpEmptyListEnv
-      <*> G.pvbumpState
-      <*> pure ()
-  let TRC (_, st, _) = judgementContext
-  case applySTS @PVBUMP judgementContext of
+  jc <- forAll G.emptyPVUpdateJC
+  let (_, st, _) = jc
+  case applySTS @PVBUMP (TRC jc) of
     Right st' -> st === st'
     Left _    -> failure
 
@@ -35,13 +31,9 @@ emptyPVUpdate = property $ do
 -- system started in.
 beginningsNoUpdate :: Property
 beginningsNoUpdate = property $ do
-  judgementContext <-
-    forAll $ fmap TRC $ (,,)
-      <$> G.pvbumpBeginningsEnv
-      <*> G.pvbumpState
-      <*> pure ()
-  let TRC (_, st, _) = judgementContext
-  case applySTS @PVBUMP $ judgementContext of
+  jc <- forAll G.beginningsNoUpdateJC
+  let (_, st, _) = jc
+  case applySTS @PVBUMP (TRC jc) of
     Right st' -> st === st'
     Left _    -> failure
 
@@ -53,19 +45,15 @@ beginningsNoUpdate = property $ do
 -- slot s > 2 * k.
 lastProposal :: Property
 lastProposal = property $ do
-  judgementContext <-
-    forAll $ fmap TRC $ (,,)
-      <$> G.pvbumpAfter2kEnv
-      <*> G.pvbumpState
-      <*> pure ()
+  jc <- forAll G.lastProposalJC
   let
-    TRC ((s_n, fads), _, _) = judgementContext
+    ((s_n, fads), _, _) = jc
     s = fromMaybe
       (error
         "An improper slot generator used! Constraint violated: s_n > 2*k")
       (minusSlotMaybe s_n (SlotCount . (2 *) . unBlockCount $ k))
     expectedSt = snd . last . (filter ((<= s) . fst)) $ fads
 
-  case applySTS @PVBUMP $ judgementContext of
+  case applySTS @PVBUMP (TRC jc) of
     Right st' -> expectedSt === st'
     Left _    -> failure

byron/semantics/executable-spec/src/Control/State/Transition.hs

@@ -52,12 +52,6 @@ newtype IRC sts = IRC (Environment sts)
 -- | Context available to transition rules.
 newtype TRC sts = TRC (Environment sts, State sts, Signal sts)
 
-deriving instance
-  ( Show (Environment sts)
-  , Show (State sts)
-  , Show (Signal sts)
-  ) => Show (TRC sts)
-
 type family RuleContext (t :: RuleType) = (ctx :: Type -> Type) | ctx -> t where
   RuleContext 'Initial = IRC
   RuleContext 'Transition = TRC