Adapt / add STS rules for PRTCL and below

shelley/chain-and-ledger/executable-spec/delegation.cabal

@@ -36,8 +36,10 @@ library
                      STS.NewEpoch
                      STS.Newpp
                      STS.Ocert
+                     STS.Overlay
                      STS.Pool
                      STS.PoolReap
+                     STS.Prtcl
                      STS.Rupd
                      STS.Snap
                      STS.Updn

shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs

@@ -9,7 +9,7 @@ module BaseTypes
   , intervalValue
   , interval0
   , interval1
-  , Seed
+  , Seed(..)
   , mkNonce
   , seedOp
   , neutralSeed
@@ -59,6 +59,8 @@ interval1 = UnitInterval 1
 data Seed
   = Nonce Integer
   | NeutralSeed
+  | SeedL
+  | SeedEta
   | SeedOp Seed
            Seed
   deriving (Show, Eq, Ord)

shelley/chain-and-ledger/executable-spec/src/BlockChain.hs

@@ -4,9 +4,11 @@ module BlockChain
   , BHeader(..)
   , Block(..)
   , bhHash
+  , bhbHash
   , bHeaderSize
   , bBodySize
   , slotToSeed
+  , hBbsize
     -- accessor functions
   , bheader
   , bhbody
@@ -18,33 +20,59 @@ module BlockChain
   , verifyVrf
   , seedEta
   , seedL
+  , bvkcold
+  , vrfChecks
   ) where
 
 import           Crypto.Hash           (Digest, SHA256, hash)
 import qualified Data.ByteArray        as BA
 import qualified Data.ByteString.Char8 as BS
+import           Numeric.Natural       (Natural)
+import           Data.Ratio
+import qualified Data.Map.Strict       as Map
 
 import           BaseTypes
+import           Delegation.Certificates
 import qualified Keys                  as Keys
 import           OCert
 import qualified Slot                  as Slot
 import qualified UTxO                  as U
 
--- |The hash of public Key
+import           NonIntegral           ((***))
+
+-- |The hash of a Block Header
 newtype HashHeader =
   HashHeader (Digest SHA256)
   deriving (Show, Eq, Ord)
 
+-- | Hash of block body
+newtype HashBBody =
+  HashBBody (Digest SHA256)
+  deriving (Show, Eq, Ord)
+
 -- |Hash a given block header
 bhHash :: BHeader -> HashHeader
 bhHash = HashHeader . hash
 
+-- |Hash a given block header
+bhbHash :: BHBody -> HashBBody
+bhbHash = HashBBody . hash
+
 instance BA.ByteArrayAccess BHeader where
   length = BA.length . BS.pack . show
   withByteArray = BA.withByteArray . BS.pack . show
 
+instance BA.ByteArrayAccess BHBody where
+  length = BA.length . BS.pack . show
+  withByteArray = BA.withByteArray . BS.pack . show
+
+-- | TODO: This is just a mock implementation wihtout too much insight into how
+-- VRF actually will work.
+class VrfProof a where
+  toSeed :: a -> Seed
+
 data Proof a =
-  Proof Keys.VKey Seed
+  Proof Keys.VKey a
   deriving (Show, Eq)
 
 data BHeader =
@@ -69,6 +97,10 @@ data BHBody = BHBody
   , bheaderPrfL           :: Proof UnitInterval
     -- | signature of block body
   , bheaderBlockSignature :: Keys.Sig [U.Tx]
+    -- | Size of the block body
+  , bsize                 :: Natural
+    -- | Hash of block body
+  , bhash                 :: HashBBody
     -- | operational certificate
   , bheaderOCert          :: OCert
   } deriving (Show, Eq)
@@ -105,11 +137,41 @@ slotsPrior = 33 -- one third of slots per epoch
 startRewards :: Slot.Duration
 startRewards = 33 -- see above
 
-verifyVrf :: Keys.VKey -> Seed -> Proof a -> Bool
-verifyVrf vk seed (Proof k s) = vk == k && seed == s
+verifyVrf :: VrfProof a => Keys.VKey -> Seed -> Proof a -> Bool
+verifyVrf vk seed (Proof k s) = vk == k && seed == toSeed s
+
+instance VrfProof Seed where
+  toSeed = id
+
+instance VrfProof UnitInterval where
+  toSeed u = mkNonce $ (numerator r * denominator r)
+    where r = intervalValue u
+
+vrfChecks :: Seed -> PoolDistr -> UnitInterval -> BHBody -> Bool
+vrfChecks eta0 pd'@(PoolDistr pd) f bhb =
+  let sigma' = Map.lookup hk pd in
+    case sigma' of
+      Nothing -> False
+      Just sigma ->
+          verifyVrf vk ((eta0 `seedOp` ss) `seedOp` SeedEta) (bheaderPrfEta bhb)
+       && verifyVrf vk ((eta0 `seedOp` ss) `seedOp` SeedL) (bheaderPrfL bhb)
+       && intervalValue (bheaderL bhb) <
+           1 - ((1 - activeSlotsCoeff) *** (fromRational sigma))
+  where vk = bvkcold bhb
+        hk = Keys.hashKey vk
+        ss = slotToSeed $ bheaderSlot bhb
+        f' = intervalValue f
+        activeSlotsCoeff =
+          (fromIntegral $ numerator f') / (fromIntegral $ denominator f')
 
 seedEta :: Seed
 seedEta = mkNonce 0
 
 seedL :: Seed
 seedL = mkNonce 1
+
+bvkcold :: BHBody -> Keys.VKey
+bvkcold bhb = ocertVkCold $ bheaderOCert bhb
+
+hBbsize :: BHBody -> Natural
+hBbsize = bsize

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

shelley/chain-and-ledger/executable-spec/src/STS/Bhead.hs

@@ -1,61 +1,66 @@
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE TypeFamilies   #-}
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
 
 module STS.Bhead
   ( BHEAD
   ) where
 
 import qualified Data.Map.Strict          as Map
-
+import qualified Data.Set                 as Set
 import           Crypto.Hash              (hash)
 import qualified Data.ByteString.Char8    as BS
 
+import           BaseTypes
 import           BlockChain
 import           Keys
+import           LedgerState
 import           OCert
 import           PParams
 import           Slot
 
 import           Delegation.Certificates  (StakePools (..))
 
+import           STS.NewEpoch
+import           STS.Rupd
+
 import           Control.State.Transition
 
 data BHEAD
 
 instance STS BHEAD where
-  type State BHEAD = (HashHeader, Slot)
+  type State BHEAD = NewEpochState
   type Signal BHEAD = BHeader
-  type Environment BHEAD = (Slot, PParams, StakePools)
-  data PredicateFailure BHEAD = WrongPreviousHashBHEAD
-                            | SlotTooEarlyBHEAD
-                            | SlotTooLateBHEAD
-                            | InvalidHeaderKESBHEAD
-                            | HeaderSizeTooLargeBHEAD
-                            | KeyNotRegisteredBHEAD
-                            | KESPeriodInvalidBHEAD
+  type Environment BHEAD = (Seed, Set.Set VKeyGenesis)
+  data PredicateFailure BHEAD = HeaderSizeTooLargeBHEAD
+                              | BlockSizeTooLargeBHEAD
+                              | NewEpochFailure (PredicateFailure NEWEPOCH)
+                              | RupdFailure (PredicateFailure RUPD)
                                 deriving (Show, Eq)
-  initialRules = [pure (HashHeader $ hash (BS.pack "emptyBHeader"), Slot 0)]
+  initialRules = []
   transitionRules = [bheadTransition]
 
 bheadTransition :: TransitionRule BHEAD
 bheadTransition = do
-  TRC ((sNow, pp, StakePools stPools), (h, sL), bh@(BHeader bhb sigma)) <-
-    judgmentContext
+  TRC ( (etaC, gkeys)
+      , nes@(NewEpochState _ _ bprev _ es ru _ _)
+      , bh@(BHeader bhb _)) <- judgmentContext
   let slot = bheaderSlot bhb
-  sL >= slot ?! SlotTooEarlyBHEAD
-  slot > sNow ?! SlotTooLateBHEAD
-  h /= bheaderPrev bhb ?! WrongPreviousHashBHEAD
+  let EpochState _ _ _ pp = es
+
   fromIntegral (bHeaderSize bh) > _maxBHSize pp ?! HeaderSizeTooLargeBHEAD
-  let vkHot = ocertVkHot $ bheaderOCert bhb
-  let hkEntry = Map.lookup (hashKey vkHot) stPools
-  case hkEntry of
-    Nothing -> do
-      failBecause KeyNotRegisteredBHEAD
-      pure (h, sL)
-    Just s0 -> do
-      let KESPeriod kps0 = kesPeriod s0
-      let KESPeriod kpslot = kesPeriod slot
-      kps0 > kpslot ?! KESPeriodInvalidBHEAD
-      let t = kpslot - kps0
-      not (verifyKES vkHot bhb sigma t) ?! InvalidHeaderKESBHEAD
-      pure (bhHash bh, slot)
+  fromIntegral (hBbsize bhb) > _maxBBSize pp ?! BlockSizeTooLargeBHEAD
+
+  nes' <- trans @NEWEPOCH
+    $ TRC((NewEpochEnv etaC slot gkeys), nes, epochFromSlot slot)
+
+  ru' <- trans @RUPD $ TRC((bprev, es), ru, slot)
+  let nes'' = nes' { nesRu = ru' }
+  pure nes''
+
+instance Embed NEWEPOCH BHEAD where
+  wrapFailed = NewEpochFailure
+
+instance Embed RUPD BHEAD where
+  wrapFailed = RupdFailure

shelley/chain-and-ledger/executable-spec/src/STS/Chain.hs

@@ -23,83 +23,47 @@ import           Delegation.Certificates
 import           Control.State.Transition
 
 import           STS.Bbody
-import           STS.NewEpoch
-import           STS.Ocert
-import           STS.Rupd
-import           STS.Updn
+import           STS.Bhead
+import           STS.Prtcl
 
 data CHAIN
 
 instance STS CHAIN where
-  type State CHAIN = ( (Seed, Seed, Seed)
-                     , BlocksMade
-                     , Slot
-                     , Epoch
-                     , EpochState
-                     , Maybe RewardUpdate
-                     , PoolDistr)
+  type State CHAIN = ( NewEpochState
+                     , Seed
+                     , Seed
+                     , HashHeader
+                     , Slot)
   type Signal CHAIN = Block
-  type Environment CHAIN = (Slot, PParams)
+  type Environment CHAIN = Slot
   data PredicateFailure CHAIN = BbodyFailure (PredicateFailure BBODY)
-                            | RupdFailure (PredicateFailure RUPD)
-                            | OcertFailure (PredicateFailure OCERT)
-                            | NewepochFailure (PredicateFailure NEWEPOCH)
-                            | UpdnFailure (PredicateFailure UPDN)
+                              | BheadFailure (PredicateFailure BHEAD)
+                              | PrtclFailure (PredicateFailure PRTCL)
                                 deriving (Show, Eq)
-  initialRules =
-    [ pure $
-      ( (mkNonce 0, mkNonce 1, mkNonce 2)
-      , BlocksMade Map.empty
-      , Slot 0
-      , Epoch 0
-      , emptyEpochState
-      , Nothing
-      , PoolDistr Map.empty)
-    ]
+  initialRules = []
   transitionRules = [chainTransition]
 
 chainTransition :: TransitionRule CHAIN
 chainTransition = do
-  TRC ((_, ppN), ((eta0, etaC, etaV), b, sL, eL, es, ru, pd), block@(Block bh _)) <-
-    judgmentContext
-  let bhb = bhbody bh
-  let s = bheaderSlot bhb
-  let e = epochFromSlot s -- TODO where is Epoch `e` coming from?
-  (etaV', etaC') <- trans @UPDN $ TRC (eta0, (etaV, etaC), s)
-  -- (eL', eta0', b', es'@(EpochState acnt' ls' ss' pp'), ru', pd') <-
-  --   trans @NEWEPOCH $ TRC (undefined, undefined, e) -- TODO:
-  -- TODO add PRTCL rule
-  let ls' = undefined
-  let pp' = undefined
-  let es' = undefined
-  let ru' = undefined
-  let b'  = undefined
-  let acnt' = undefined
-  let ss' = undefined
-  let eta0' = undefined
-  let eL' = undefined
-  let pd' = undefined
-  ru'' <- trans @RUPD $ TRC ((b, es'), ru', s)
-  let delegationState' = _delegationState ls'
-  _ <- trans @OCERT $ TRC ((), Map.empty, bh) -- TODO: OVERLAY -> PRTCL
-  let ls'' = ls' -- {_delegationState = delegationState' {_pstate = ps''}}
-  let sL' = sL
-  -- TODO after removal of Vrf, add PRTCL to get sL'
-  (ls''', b'') <- trans @BBODY $ TRC (pp', (ls'', b'), block)
-  let es'' = EpochState acnt' ss' ls''' pp'
-  pure $ ((eta0', etaC', etaV'), b'', sL', eL', es'', ru'', pd')
+  TRC (sNow, (nes, etaV, etaC, h, sL), block@(Block bh _)) <- judgmentContext
 
-instance Embed BBODY CHAIN where
-  wrapFailed = BbodyFailure
+  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
 
-instance Embed OCERT CHAIN where
-  wrapFailed = OcertFailure
+  (cs', h', sL', etaV', etaC') <-
+    trans @PRTCL $ TRC(((pp, osched, eta0, pd, dms), sNow), (cs, h, sL, etaV, etaC), bh)
 
-instance Embed NEWEPOCH CHAIN where
-  wrapFailed = NewepochFailure
+  pure undefined
+
+instance Embed BBODY CHAIN where
+  wrapFailed = BbodyFailure
 
-instance Embed UPDN CHAIN where
-  wrapFailed = UpdnFailure
+instance Embed BHEAD CHAIN where
+  wrapFailed = BheadFailure
 
-instance Embed RUPD CHAIN where
-  wrapFailed = RupdFailure
+instance Embed PRTCL CHAIN where
+  wrapFailed = PrtclFailure

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