Document throwable vs structural PredicateFailures

Add comments on `PredicateFailure` data declarations. Rename a few constructors, adding a `S_` prefix to indicate their structural-ness. Document the convention in the class definition.
IntersectMBO · Aug 20, 2019 · 8be14ba · 8be14ba
1 parent 7e77840
commit 8be14ba
Show file tree

Hide file tree

Showing 7 changed files with 49 additions and 17 deletions.
diff --git a/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/BBody.hs b/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/BBody.hs
@@ -43,6 +43,7 @@ instance STS BBODY where
 
   type Signal BBODY = Block
 
+  -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure BBODY
     = InvalidBlockSize
     | InvalidUtxoHash

diff --git a/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/SigCnt.hs b/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/SigCnt.hs
@@ -32,6 +32,7 @@ instance STS SIGCNT where
 
   type Signal SIGCNT = VKey
 
+  -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure SIGCNT
     = TooManyIssuedBlocks VKeyGenesis -- The given genesis key issued too many blocks.
     | NotADelegate

diff --git a/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs b/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs
@@ -51,6 +51,10 @@ instance STS UTXO where
   type Environment UTXO = UTxOEnv
   type State UTXO = UTxOState
   type Signal UTXO = Tx
+
+  -- | These `PredicateFailure`s are all "throwable". The disjunction of the
+  --   rules' preconditions is not `True` - the `PredicateFailure`s represent
+  --   `False` cases.
   data PredicateFailure UTXO
     = EmptyTxInputs
     | EmptyTxOutputs

diff --git a/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOW.hs b/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOW.hs
@@ -32,6 +32,8 @@ instance STS UTXOW where
   type Environment UTXOW = UTxOEnv
   type State UTXOW = UTxOState
   type Signal UTXOW = TxWits
+
+  -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure UTXOW
     = UtxoFailure (PredicateFailure UTXO)
     | InsufficientWitnesses

diff --git a/byron/ledger/executable-spec/src/Ledger/Delegation.hs b/byron/ledger/executable-spec/src/Ledger/Delegation.hs
@@ -255,6 +255,9 @@ instance STS SDELEG where
   type Signal SDELEG = DCert
   type Environment SDELEG = DSEnv
 
+  -- | These `PredicateFailure`s are all "throwable". The disjunction of the
+  --   rules' preconditions is not `True` - the `PredicateFailure`s represent
+  --   `False` cases.
   data PredicateFailure SDELEG
     = IsNotGenesisKey
     | EpochInThePast EpochDiff
@@ -325,14 +328,15 @@ instance STS ADELEG where
   type Signal ADELEG = (Slot, (VKeyGenesis, VKey))
   type Environment ADELEG = Set VKeyGenesis
 
+  -- | None of these `PredicateFailure`s are actually "throwable". The
+  --   disjuction of the rules' preconditions is `True`, which means that one of
+  --   them will pass. The `PredicateFailure` just act as switches to direct
+  --   control flow to the successful one.
   data PredicateFailure ADELEG
-    = BeforeExistingDelegation
-      -- | Not actually a failure; this should just trigger the other rule.
-    | NoLastDelegation
-      -- | Not a failure; this should just pass the other rule
-    | AfterExistingDelegation
-    -- | The given key is a delegate of the given genesis key.
-    | AlreadyADelegateOf VKey VKeyGenesis
+    = S_BeforeExistingDelegation
+    | S_NoLastDelegation
+    | S_AfterExistingDelegation
+    | S_AlreadyADelegateOf VKey VKeyGenesis
     deriving (Eq, Show, Data, Typeable)
 
   initialRules = [
@@ -354,11 +358,11 @@ instance STS ADELEG where
                      }
             , (s, (vks, vkd))
             ) <- judgmentContext
-        vkd ∉ range dms ?! AlreadyADelegateOf vkd (dms !> vkd)
+        vkd ∉ range dms ?! S_AlreadyADelegateOf vkd (dms !> vkd)
         case Map.lookup vks dws of
           Nothing -> pure () -- If vks hasn't delegated, then we proceed and
                              -- update the @ADELEG@ state.
-          Just sp -> sp < s ?! BeforeExistingDelegation
+          Just sp -> sp < s ?! S_BeforeExistingDelegation
         return $!
           DState { _dStateDelegationMap = dms ⨃ [(vks, vkd)]
                  , _dStateLastDelegation = dws ⨃ [(vks, s)]
@@ -374,7 +378,7 @@ instance STS ADELEG where
           then return st
           else do
             case Map.lookup vks dws of
-              Just sp -> sp >= s ?! AfterExistingDelegation
+              Just sp -> sp >= s ?! S_AfterExistingDelegation
               Nothing -> error $  "This can't happen since otherwise "
                                ++ "the previous rule would have been triggered."
             return st

diff --git a/byron/ledger/executable-spec/src/Ledger/Update.hs b/byron/ledger/executable-spec/src/Ledger/Update.hs
@@ -298,6 +298,9 @@ instance STS UPSVV where
   type State UPSVV = Map UpId (ApName, ApVer, Metadata)
   type Signal UPSVV = UProp
 
+  -- | These `PredicateFailure`s are all "throwable". The disjunction of the
+  --   rules' preconditions is not `True` - the `PredicateFailure`s represent
+  --   `False` cases.
   data PredicateFailure UPSVV
     = AlreadyProposedSv
     | CannotFollowSv
@@ -332,6 +335,9 @@ instance STS UPPVV where
   type State UPPVV = Map UpId (ProtVer, PParams)
   type Signal UPPVV = UProp
 
+  -- | These `PredicateFailure`s are all "throwable". The disjunction of the
+  --   rules' preconditions is not `True` - the `PredicateFailure`s represent
+  --   `False` cases.
   data PredicateFailure UPPVV
     = CannotFollowPv
     | CannotUpdatePv [UpdateConstraintViolation]
@@ -369,6 +375,7 @@ instance STS UPV where
 
   type Signal UPV = UProp
 
+  -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure UPV
     = UPPVVFailure (PredicateFailure UPPVV)
     | UPSVVFailure (PredicateFailure UPSVV)
@@ -430,6 +437,7 @@ instance STS UPREG where
     )
   type Signal UPREG = UProp
 
+  -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure UPREG
     = UPVFailure (PredicateFailure UPV)
     | NotGenesisDelegate
@@ -483,6 +491,7 @@ instance STS ADDVOTE where
   type State ADDVOTE = Set (UpId, Core.VKeyGenesis)
   type Signal ADDVOTE = Vote
 
+  -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure ADDVOTE
     = AVSigDoesNotVerify
     | NoUpdateProposal UpId
@@ -520,10 +529,14 @@ instance STS UPVOTE where
     , Set (UpId, Core.VKeyGenesis)
     )
   type Signal UPVOTE = Vote
+
+  -- | `S_CfmThdNotReached` is a structural `PredicateFailure`, used to fail
+  -- from one transition rule to the other. The other `PredicateFailure`s are
+  -- all throwable.
   data PredicateFailure UPVOTE
     = ADDVOTEFailure (PredicateFailure ADDVOTE)
     | HigherThanThdAndNotAlreadyConfirmed
-    | CfmThdNotReached
+    | S_CfmThdNotReached
     | AlreadyConfirmed
     deriving (Eq, Show)
 
@@ -547,7 +560,7 @@ instance STS UPVOTE where
             ) <- judgmentContext
         vts' <- trans @ADDVOTE $ TRC ((rups, dms), vts, vote)
         let pid = vote ^. vPropId
-        t <= size ([pid] ◁ vts') ?! CfmThdNotReached
+        t <= size ([pid] ◁ vts') ?! S_CfmThdNotReached
         pid ∉ dom cps ?! AlreadyConfirmed
         pure $! ( cps ⨃ [(pid, sn)]
                 , vts'
@@ -613,9 +626,12 @@ instance STS UPEND where
     )
   type Signal UPEND = (ProtVer, Core.VKey)
 
+  -- | `S_TryNextRule` is a structural `PredicateFailure`, used to fail from
+  -- one transition rule to the other. The other `PredicateFailure`s are all
+  -- throwable.
   data PredicateFailure UPEND
     = ProtVerUnknown ProtVer
-    | TryNextRule
+    | S_TryNextRule
     | CanAdopt ProtVer
     | CannotAdopt ProtVer
     | NotADelegate VKey
@@ -634,7 +650,7 @@ instance STS UPEND where
           Just (pid, _) -> do
             -- If we found the proposal id that corresponds to 'bv' then we
             -- have to check that it isn't confirmed for this rule to succeed.
-            pid ∉ dom (cps ▷<= sn  -. 2 *. k) ?! TryNextRule
+            pid ∉ dom (cps ▷<= sn  -. 2 *. k) ?! S_TryNextRule
             pure $! (fads, bvs)
           Nothing ->
             -- If we didn't find the proposal id that corresponds to 'bv' then
@@ -654,17 +670,17 @@ instance STS UPEND where
             ) <- judgmentContext
         case lookupR vk dms of
           Nothing  -> do
-            False ?! TryNextRule
+            False ?! S_TryNextRule
             pure $! (fads, bvs)
           Just vks -> do
             let bvs' = bvs ∪ singleton bv vks
             size ([bv] ◁ bvs') < t ?! CanAdopt bv
             case findKey ((== bv) . fst) rpus of
               Just (pid, _) -> do
-                pid ∈ dom (cps ▷<= sn -. 2 *. k) ?! TryNextRule
+                pid ∈ dom (cps ▷<= sn -. 2 *. k) ?! S_TryNextRule
                 pure $! (fads, bvs')
               Nothing -> do
-                False ?! TryNextRule
+                False ?! S_TryNextRule
                 pure $! (fads, bvs')
 
     , do

diff --git a/byron/semantics/executable-spec/src/Control/State/Transition.hs b/byron/semantics/executable-spec/src/Control/State/Transition.hs
@@ -78,6 +78,10 @@ class ( Eq (PredicateFailure a)
 
   -- | Descriptive type for the possible failures which might cause a transition
   -- to fail.
+  --
+  -- As a convention, `PredicateFailure`s which are "structural" (meaning that
+  -- they are not "throwable" in practice, and are used to pass control from
+  -- one transition rule to another) are prefixed with `S_`.
   data PredicateFailure a :: *
 
   -- | Rules governing transition under this system.