[466] Remove dms map from EPOCH STS/latex spec

IntersectMBO · May 30, 2019 · 7df3607 · 7df3607
1 parent 6183a28
commit 7df3607
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 32 deletions.
diff --git a/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/BHead.hs b/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/BHead.hs
@@ -41,7 +41,7 @@ instance STS BHEAD where
   transitionRules =
     [ do
         TRC ((epochEnv, sLast), us, bh) <- judgmentContext
-        us' <- trans @EPOCH $ TRC ((epochEnv, sEpoch sLast), us, bh ^. bhSlot)
+        us' <- trans @EPOCH $ TRC (sEpoch sLast, us, bh ^. bhSlot)
         let sMax = snd (us' ^. _1) ^. maxHdrSz
         bHeaderSize bh <= sMax ?! HeaderSizeTooBig
         return $! us'

diff --git a/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/Epoch.hs b/byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/Epoch.hs
@@ -19,10 +19,7 @@ sEpoch (Slot s) = Epoch $ s `div` 21600
 data EPOCH
 
 instance STS EPOCH where
-  type Environment EPOCH =
-    ( Bimap VKeyGenesis VKey
-    , Epoch
-    )
+  type Environment EPOCH = Epoch
   type State EPOCH = UPIState
 
   type Signal EPOCH = Slot
@@ -34,15 +31,15 @@ instance STS EPOCH where
 
   transitionRules =
     [ do
-        TRC ((_, e_c), _, s) <- judgmentContext
+        TRC (e_c, _, s) <- judgmentContext
         case e_c >= sEpoch s of
           True  -> onOrAfterCurrentEpoch
           False -> beforeCurrentEpoch
     ]
    where
     beforeCurrentEpoch :: TransitionRule EPOCH
     beforeCurrentEpoch = do
-      TRC ((_dms, _), us, s) <- judgmentContext
+      TRC (_, us, s) <- judgmentContext
       us' <- trans @UPIEC $ TRC (s, us, ())
       return $! us'
 

diff --git a/byron/chain/formal-spec/blockchain-spec.tex b/byron/chain/formal-spec/blockchain-spec.tex
@@ -671,10 +671,9 @@ \section{Epoch transitions}
   \begin{align*}
     & \ETEnv
       = \left(
-      \begin{array}{r@{~\in~}lr}
-        \var{dms} & \VKeyGen \mapsto \VKey & \text{delegation map}\\
-        \var{e_c} & \Epoch & \text{Current epoch}
-      \end{array}\right)
+          \begin{array}{r@{~\in~}lr}
+            \var{e_c} & \Epoch & \text{current epoch}
+          \end{array}\right)
   \end{align*}
 
   \emph{Epoch transition states}
@@ -702,30 +701,20 @@ \section{Epoch transitions}
     {
       \var{e_c} \geq \sepoch{s}
     }
-    {
-      {\left(
-        \begin{array}{l}
-          \var{dms}\\
-          \var{e_c}
-        \end{array}
-      \right)}
+    {\var{e_c}
       \vdash
       {
-        \left(
           {\begin{array}{c}
              \var{us}
            \end{array}
          }
-       \right)
      }
      \trans{epoch}{s}
      {
-       \left(
          {\begin{array}{c}
             \var{us}
           \end{array}
         }
-      \right)
     }
   }
 \end{equation*}
@@ -738,29 +727,20 @@ \section{Epoch transitions}
     s\vdash \var{us} \trans{\hyperlink{byron_ledger_spec_link}{upiec}}{} \var{us'}
   }
   {
-    {\left(
-      \begin{array}{l}
-        \var{dms}\\
-        \var{e_c}
-      \end{array}
-    \right)}
+    \var{e_c}
     \vdash
     {
-      \left(
         {\begin{array}{c}
            \var{us}
          \end{array}
        }
-     \right)
    }
    \trans{epoch}{s}
    {
-     \left(
        {\begin{array}{c}
           \var{us'}
         \end{array}
       }
-    \right)
   }
 }
 \end{equation*}