Add update mechanism and related STS rules

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

@@ -29,6 +29,8 @@ library
                      Delegation.PoolParams
                      Delegation.Certificates
                      OCert
+                     Updates
+                     STS.Avup
                      STS.Bbody
                      STS.Bhead
                      STS.Chain
@@ -41,10 +43,14 @@ library
                      STS.NewEpoch
                      STS.Newpp
                      STS.Ocert
+                     STS.Overlay
                      STS.Pool
                      STS.PoolReap
+                     STS.Ppup
+                     STS.Prtcl
                      STS.Rupd
                      STS.Snap
+                     STS.Up
                      STS.Updn
                      STS.Utxo
                      STS.Utxow

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

@@ -9,17 +9,14 @@ module BaseTypes
   , intervalValue
   , interval0
   , interval1
-  , Seed
+  , Seed(..)
   , mkNonce
   , seedOp
   , neutralSeed
-  , EEnt(..)
   ) where
 
-import qualified Data.Map.Strict as Map
 
 import qualified Data.Fixed as FP
-import qualified Keys       as Keys
 
 data E34
 
@@ -59,6 +56,8 @@ interval1 = UnitInterval 1
 data Seed
   = Nonce Integer
   | NeutralSeed
+  | SeedL
+  | SeedEta
   | SeedOp Seed
            Seed
   deriving (Show, Eq, Ord)
@@ -73,7 +72,3 @@ neutralSeed = NeutralSeed
 
 mkNonce :: Integer -> Seed
 mkNonce = Nonce
-
--- | Extra entropy
-newtype EEnt = EEnt (Map.Map Keys.VKeyGenesis Seed)
-  deriving (Show, Ord, Eq)

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,65 @@ module BlockChain
   , verifyVrf
   , seedEta
   , seedL
-  ) where
-
-import           Crypto.Hash           (Digest, SHA256, hash)
-import qualified Data.ByteArray        as BA
-import qualified Data.ByteString.Char8 as BS
+  , bvkcold
+  , vrfChecks
+  , incrBlocks
+  )
+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 qualified Keys                  as Keys
+import           Delegation.Certificates
+import           EpochBoundary
+import qualified Keys                          as Keys
 import           OCert
-import qualified Slot                  as Slot
-import qualified UTxO                  as U
+import qualified Slot                          as Slot
+import qualified UTxO                          as U
+
+import           NonIntegral                    ( (***) )
 
--- |The hash of public Key
+-- |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 +103,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 +143,53 @@ 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 (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
+
+incrBlocks :: Bool -> Keys.HashKey -> BlocksMade -> BlocksMade
+incrBlocks isOverlay hk b'@(BlocksMade b)
+  | isOverlay = b'
+  | otherwise = BlocksMade $ case hkVal of
+    Nothing -> Map.insert hk 1 b
+    Just n  -> Map.insert hk (n + 1) b
+  where hkVal = Map.lookup hk b

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

@@ -59,7 +59,7 @@ verifyKES :: Eq a => VKey -> a -> KESig a -> Natural -> Bool
 verifyKES (VKey vk) vd (KESig (Sig sd sk) m) n = vk == sk && vd == sd && m == n
 
 newtype Dms = Dms (Map.Map VKeyGenesis VKey)
-  deriving (Show, Eq)
+  deriving (Show, Ord, Eq)
 
 newtype GKeys = GKeys (Set.Set VKeyGenesis)
-  deriving (Show, Eq)
+  deriving (Show, Ord, Eq)