Adapt BBODY STS rule

IntersectMBO · Jun 21, 2019 · 0815970 · 0815970
1 parent 0815197
commit 0815970
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 6 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs
@@ -107,6 +107,8 @@ module LedgerState
   , NewEpochEnv(..)
   , overlaySchedule
   , getGKeys
+  , setIssueNumbers
+  , updateNES
   ) where
 
 import           Control.Monad           (foldM)
@@ -947,3 +949,16 @@ overlaySchedule
   -> PParams
   -> Map.Map Slot (Maybe VKeyGenesis)
 overlaySchedule = undefined
+
+-- | Set issue numbers
+setIssueNumbers :: LedgerState -> Map.Map HashKey Natural -> LedgerState
+setIssueNumbers (LedgerState u
+                 (DPState _dstate
+                  (PState stpools poolParams _retiring _ )) i) cs =
+  LedgerState u (DPState _dstate (PState stpools poolParams _retiring cs)) i
+
+-- | Update new epoch state
+updateNES :: NewEpochState -> BlocksMade -> LedgerState ->NewEpochState
+updateNES (NewEpochState eL eta0 bprev _
+           (EpochState acnt ss _ pp) ru pd osched) bcur ls =
+  NewEpochState eL eta0 bprev bcur (EpochState acnt ss ls pp) ru pd osched
diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs
@@ -8,6 +8,8 @@ module STS.Chain
   )
 where
 
+import qualified Data.Map.Strict               as Map
+
 import           BaseTypes
 import           BlockChain
 import           LedgerState
@@ -38,18 +40,27 @@ instance STS CHAIN where
 
 chainTransition :: TransitionRule CHAIN
 chainTransition = do
-  TRC (sNow, (nes, etaV, etaC, h, sL), (Block bh _)) <- judgmentContext
+  TRC (sNow, (nes, etaV, etaC, h, sL), block@(Block bh _)) <- judgmentContext
 
   let gkeys = getGKeys nes
   nes' <- trans @BHEAD $ TRC ((etaC, gkeys), nes, bh)
 
-  let NewEpochState _ eta0 _ _ es _ _pd osched = nes'
-  let EpochState _ _ ls pp = es
+  let NewEpochState _ eta0 _ bcur es _ _pd osched = nes'
+  let EpochState _ _ ls pp                        = es
   let LedgerState _ (DPState (DState _ _ _ _ _dms) (PState _ _ _ cs)) _ = ls
 
-  _ <- trans @PRTCL $ TRC(((pp, osched, eta0, _pd, _dms), sNow), (cs, h, sL, etaV, etaC), bh)
+  (cs', h', sL', etaV', etaC') <- trans @PRTCL
+    $ TRC (((pp, osched, eta0, _pd, _dms), sNow), (cs, h, sL, etaV, etaC), bh)
+
+  let ls' = setIssueNumbers ls cs' -- TODO: is this cs or cs' ?
+                                   -- (formal spec ignored cs')
+
+  (ls'', bcur') <- trans @BBODY
+    $ TRC ((Map.keysSet osched, pp), (ls', bcur), block)
+
+  let nes'' = updateNES nes' bcur' ls''
 
-  pure undefined
+  pure (nes'', etaV', etaC', h', sL')
 
 instance Embed BBODY CHAIN where
   wrapFailed = BbodyFailure

diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex
@@ -1383,7 +1383,8 @@ \subsection{Chain Transition}
               \eta_c' \\
         \end{array}\right)}
       } \\~\\~\\
-      \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs} \\
+      \var{ls'}\leteq\fun{setIssueNumbers}~\var{ls}~\var{cs} \\ % TODO should
+                                % this be cs' ?
       {
         {\left(\begin{array}{c}
               \dom{osched} \\

diff --git a/shelley/chain-and-ledger/formal-spec/epoch.tex b/shelley/chain-and-ledger/formal-spec/epoch.tex
@@ -900,6 +900,8 @@ \subsection{Complete Epoch Boundary Transition}
       \\~\\~\\
       \var{(\wcard,~\wcard,~\wcard,~(\var{pup},~\wcard,~\wcard,~\wcard))}\leteq\var{utxoSt'}\\
       \var{pp_{new}}\leteq\fun{votedValue_{PParams}}~\var{pup}\\
+      % TODO: I think this isn't the right type, `pup` is PPUpdate which is not
+      % a complete set of `PParams`.
       {
         \begin{array}{l}
           \var{pp_{new}}\\