Call BHEAD from CHAIN

IntersectMBO · Jun 18, 2019 · 0815f74 · 0815f74
1 parent 0815014
commit 0815f74
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 6 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/delegation.cabal b/shelley/chain-and-ledger/executable-spec/delegation.cabal
@@ -39,6 +39,7 @@ library
                      STS.Overlay
                      STS.Pool
                      STS.PoolReap
+                     STS.Prtcl
                      STS.Rupd
                      STS.Snap
                      STS.Updn

diff --git a/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs b/shelley/chain-and-ledger/executable-spec/src/LedgerState.hs
@@ -108,6 +108,7 @@ module LedgerState
   , NewEpochState(..)
   , NewEpochEnv(..)
   , overlaySchedule
+  , getGKeys
   ) where
 
 import           Control.Monad           (foldM)
@@ -317,6 +318,12 @@ data NewEpochState =
   , nesOsched :: Map.Map Slot (Maybe VKeyGenesis)
   } deriving (Show, Eq)
 
+getGKeys :: NewEpochState -> Set VKeyGenesis
+getGKeys nes = Map.keysSet dms
+  where NewEpochState _ _ _ _ es _ _ _ = nes
+        EpochState _ _ ls _ = es
+        LedgerState _ (DPState (DState _ _ _ _ (Dms dms)) _) _ _ _ _ = ls
+
 data NewEpochEnv =
   NewEpochEnv {
     neeEta1  :: Seed

diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs
@@ -47,7 +47,10 @@ chainTransition :: TransitionRule CHAIN
 chainTransition = do
   TRC (sNow, (nes, etaV, etaC, h, sL), block@(Block bh _)) <- judgmentContext
 
-  let nes'@(NewEpochState _ eta0 _ bCur es _ pd osched) = nes -- TODO: converge BHEAD
+  let gkeys = getGKeys nes
+  nes' <- trans @BHEAD $ TRC((etaC, gkeys), nes, bh)
+
+  let NewEpochState _ eta0 _ bCur es _ pd osched = nes'
   let EpochState _ _ ls pp = es
   let LedgerState _ (DPState (DState _ _ _ _ dms) (PState _ _ _ cs)) _ _ _ _ = ls
 

diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Ocert.hs
@@ -10,7 +10,6 @@ import           Numeric.Natural          (Natural)
 
 import           BlockChain
 import           Keys
-import           LedgerState
 import           OCert
 
 import           Control.State.Transition

diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Overlay.hs
@@ -49,13 +49,11 @@ overlayTransition = do
   let gkey'' = Map.lookup (bheaderSlot bhb) osched
   let vk     = bvkcold bhb
   case gkey'' of
-    -- | Praos schedule
-    Nothing -> do
+    Nothing -> do     -- | Praos schedule
       vrfChecks eta0 pd (_activeSlotCoeff pp) bhb ?! NotPraosLeaderOVERLAY
       cs' <- trans @OCERT $ TRC ((), cs, bh)
       pure cs'
-    -- | Found in OBFT overlay schedule
-    Just gkey' -> do
+    Just gkey' -> do  -- | Found in OBFT overlay schedule
       case gkey' of
         -- | osched is a mapping `Slot |-> Maybe VKeyGenesis`, so `gkey''` can
         -- be `Just Nothing`