Address PR #772 review feedback

IntersectMBO · Aug 20, 2019 · ef891b2 · ef891b2
1 parent 8be14ba
commit ef891b2
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 8 deletions.
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
@@ -34,7 +34,8 @@ instance STS SIGCNT where
 
   -- | These `PredicateFailure`s are all throwable.
   data PredicateFailure SIGCNT
-    = TooManyIssuedBlocks VKeyGenesis -- The given genesis key issued too many blocks.
+    = TooManyIssuedBlocks VKeyGenesis
+    -- ^ The given genesis key issued too many blocks.
     | NotADelegate
     -- ^ The key signing the block is not a delegate of a genesis key.
 

diff --git a/byron/ledger/executable-spec/src/Ledger/Update.hs b/byron/ledger/executable-spec/src/Ledger/Update.hs
@@ -530,14 +530,14 @@ instance STS UPVOTE where
     )
   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.
+  -- | The 3 non-embedded `PredicateFailure`s here are all structural. The
+  -- disjuntion of the preconditions is `True` - one rule either fires or the
+  -- other does.
   data PredicateFailure UPVOTE
     = ADDVOTEFailure (PredicateFailure ADDVOTE)
-    | HigherThanThdAndNotAlreadyConfirmed
+    | S_HigherThanThdAndNotAlreadyConfirmed
     | S_CfmThdNotReached
-    | AlreadyConfirmed
+    | S_AlreadyConfirmed
     deriving (Eq, Show)
 
   initialRules = []
@@ -549,7 +549,7 @@ instance STS UPVOTE where
             ) <- judgmentContext
         vts' <- trans @ADDVOTE $ TRC ((rups, dms), vts, vote)
         let pid = vote ^. vPropId
-        size ([pid] ◁ vts') < t || pid ∈ dom cps ?! HigherThanThdAndNotAlreadyConfirmed
+        size ([pid] ◁ vts') < t || pid ∈ dom cps ?! S_HigherThanThdAndNotAlreadyConfirmed
         pure $! ( cps
                 , vts'
                 )
@@ -561,7 +561,7 @@ instance STS UPVOTE where
         vts' <- trans @ADDVOTE $ TRC ((rups, dms), vts, vote)
         let pid = vote ^. vPropId
         t <= size ([pid] ◁ vts') ?! S_CfmThdNotReached
-        pid ∉ dom cps ?! AlreadyConfirmed
+        pid ∉ dom cps ?! S_AlreadyConfirmed
         pure $! ( cps ⨃ [(pid, sn)]
                 , vts'
                 )

diff --git a/byron/semantics/executable-spec/src/Control/State/Transition.hs b/byron/semantics/executable-spec/src/Control/State/Transition.hs
@@ -82,6 +82,11 @@ class ( Eq (PredicateFailure a)
   -- 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_`.
+  --
+  -- Structural `PredicateFailure`s represent conditions between rules where
+  -- the disjunction of all rules' preconditions is equal to `True`. That is,
+  -- either one rule will throw a structural `PredicateFailure` and the other
+  -- will succeed, or vice-versa.
   data PredicateFailure a :: *
 
   -- | Rules governing transition under this system.