Merge pull request #1861 from input-output-hk/jc/audit-changes-2020-0…

…9-15 Formal Spec Syncing from Audit Issues
IntersectMBO · Sep 16, 2020 · e9e3123 · e9e3123
2 parents 156154d + 9865baa
commit e9e3123
Show file tree

Hide file tree

Showing 8 changed files with 42 additions and 25 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/BlockChain.hs
@@ -23,6 +23,7 @@ module Shelley.Spec.Ledger.BlockChain
     lastAppliedHash,
     BHBody (..),
     poolIDfromBHBody,
+    issuerIDfromBHBody,
     BHeader (BHeader),
     Block (Block),
     LaxBlock (..),
@@ -489,6 +490,12 @@ instance
 -- from the body of the block header.
 poolIDfromBHBody :: Era era => BHBody era -> KeyHash 'BlockIssuer era
 poolIDfromBHBody = hashKey . bheaderVk
+{-# DEPRECATED poolIDfromBHBody "poolIDfromBHBody has been deprecated (the name is misleading), use issuerIDfromBHBody" #-}
+
+-- | Retrieve the issuer id (the hash of the cold key) from the body of the block header.
+-- This corresponds to either a genesis/core node or a stake pool.
+issuerIDfromBHBody :: Era era => BHBody era -> KeyHash 'BlockIssuer era
+issuerIDfromBHBody = hashKey . bheaderVk
 
 -- | Retrieve the new nonce from the block header body.
 bnonce :: BHBody era -> Nonce

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
@@ -44,7 +44,7 @@ import Shelley.Spec.Ledger.BlockChain
     bbHash,
     hBbsize,
     incrBlocks,
-    poolIDfromBHBody,
+    issuerIDfromBHBody,
   )
 import Shelley.Spec.Ledger.EpochBoundary (BlocksMade)
 import Shelley.Spec.Ledger.Keys (DSignable, Hash, coerceKeyRole)
@@ -134,7 +134,7 @@ bbodyTransition =
         -- Note that this may not actually be a stake pool - it could be a genesis key
         -- delegate. However, this would only entail an overhead of 7 counts, and it's
         -- easier than differentiating here.
-        let hkAsStakePool = coerceKeyRole . poolIDfromBHBody $ bhb
+        let hkAsStakePool = coerceKeyRole . issuerIDfromBHBody $ bhb
             slot = bheaderSlotNo bhb
         firstSlotNo <- liftSTS $ do
           ei <- asks epochInfo

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs
@@ -94,7 +94,7 @@ data DelegPredicateFailure era
     --   This error is now redundant with StakeKeyAlreadyRegisteredDELEG.
     --   We should remove it and replace its one use with StakeKeyAlreadyRegisteredDELEG.
     StakeKeyInRewardsDELEG
-      !(Credential 'Staking era) -- Credential which is already registered
+      !(Credential 'Staking era) -- DEPRECATED, now redundant with StakeKeyAlreadyRegisteredDELEG
   | StakeKeyNotRegisteredDELEG
       !(Credential 'Staking era) -- Credential which is not registered
   | StakeKeyNonZeroAccountBalanceDELEG
@@ -210,10 +210,7 @@ delegationTransition = do
   TRC (DelegEnv slot ptr acnt, ds, c) <- judgmentContext
   case c of
     DCertDeleg (RegKey hk) -> do
-      -- note that pattern match is used instead of regCred, as in the spec
-      -- TODO we can remove the failure StakeKeyInRewardsDELEG and replace
-      -- the use below with StakeKeyAlreadyRegisteredDELEG
-      eval (hk ∉ dom (_rewards ds)) ?! StakeKeyInRewardsDELEG hk
+      eval (hk ∉ dom (_rewards ds)) ?! StakeKeyAlreadyRegisteredDELEG hk
 
       pure $
         ds

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs
@@ -83,8 +83,8 @@ ocertTransition ::
 ocertTransition =
   judgmentContext >>= \(TRC (env, cs, BHeader bhb sigma)) -> do
     let OCert vk_hot n c0@(KESPeriod c0_) tau = bheaderOCert bhb
-        vkey = bheaderVk bhb
-        hk = hashKey vkey
+        vkcold = bheaderVk bhb
+        hk = hashKey vkcold
         s = bheaderSlotNo bhb
     kp@(KESPeriod kp_) <- liftSTS $ kesPeriod s
 
@@ -100,7 +100,7 @@ ocertTransition =
     -- above `KESBeforeStartOCERT`
     -- predicate failure in the
     -- transition.
-    verifySignedDSIGN vkey (ocertToSignable $ bheaderOCert bhb) tau ?! InvalidSignatureOCERT n c0
+    verifySignedDSIGN vkcold (ocertToSignable $ bheaderOCert bhb) tau ?! InvalidSignatureOCERT n c0
     verifySignedKES () vk_hot t bhb sigma ?!: InvalidKesSignatureOCERT kp_ c0_ t
 
     case currentIssueNo env cs hk of

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs
@@ -48,8 +48,8 @@ import Shelley.Spec.Ledger.BlockChain
   ( BHBody (..),
     BHeader (..),
     checkLeaderValue,
+    issuerIDfromBHBody,
     mkSeed,
-    poolIDfromBHBody,
     seedEta,
     seedL,
   )
@@ -212,7 +212,7 @@ praosVrfChecks eta0 (PoolDistr pd) f bhb = do
         (throwError $ VRFLeaderValueTooBig (VRF.certifiedOutput $ bheaderL bhb) sigma f)
       pure ()
   where
-    hk = coerceKeyRole . poolIDfromBHBody $ bhb
+    hk = coerceKeyRole . issuerIDfromBHBody $ bhb
     vrfK = bheaderVrfVk bhb
 
 pbftVrfChecks ::
@@ -232,7 +232,7 @@ pbftVrfChecks vrfHK eta0 bhb = do
   vrfChecks eta0 bhb
   pure ()
   where
-    hk = poolIDfromBHBody bhb
+    hk = issuerIDfromBHBody bhb
     vrfK = bheaderVrfVk bhb
 
 overlayTransition ::

diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex
@@ -158,6 +158,7 @@ \subsection{Block Definitions}
         \var{prev} & \HashHeader^? & \text{hash of previous block header}\\
         \var{vk} & \VKey & \text{block issuer}\\
         \var{vrfVk} & \VKey & \text{VRF verification key}\\
+        \var{blockno} & \BlockNo & \text{block number}\\
         \var{slot} & \Slot & \text{block slot}\\
         \eta & \Seed & \text{nonce}\\
         \var{prf}_{\eta} & \Proof & \text{nonce proof}\\
@@ -1240,40 +1241,52 @@ \subsection{Verifiable Random Function}
 
 \begin{figure}
   \emph{VRF helper function}
+  \begin{align*}
+      & \fun{issuerIDfromBHBody} \in \BHBody \to \KeyHash_{pool} \\
+      & \fun{issuerIDfromBHBody} = \hashKey{} \circ \bvkcold{} \\
+  \end{align*}
+  %
+  \begin{align*}
+      & \fun{mkSeed} \in \Seed \to \Slot \to \Seed \to \Seed \\
+      & \fun{mkSeed}~\var{ucNonce}~\var{slot}~\eta_0 =
+        \var{ucNonce}~\mathsf{XOR}~(\slotToSeed{slot}\seedOp\eta_0)\\
+  \end{align*}
+  %
   \begin{align*}
       & \fun{vrfChecks} \in \Seed \to \BHBody \to \Bool \\
       & \fun{vrfChecks}~\eta_0~\var{bhb} = \\
       & \begin{array}{cl}
         ~~~~ &
-             \verifyVrf{\Seed}{\var{vrfVk}}{((\eta_0\seedOp ss)\seedOp\Seede)}
+        \verifyVrf{\Seed}{\var{vrfK}}{(\fun{mkSeed}~\Seede~\var{slot}~\eta_0)}
                {(\bprfn{bhb},~\bnonce{bhb}}) \\
         ~~~~ \land &
-             \verifyVrf{\unitInterval}{\var{vrfVk}}{((\eta_0\seedOp ss)\seedOp\Seedl)}
+               \verifyVrf{\unitInterval}{\var{vrfK}}{(\fun{mkSeed}~\Seedl~\var{slot}~\eta_0)}
                {(\bprfl{bhb},~\bleader{bhb}}) \\
       \end{array} \\
       & ~~~~\where \\
-      & ~~~~~~~~~~\var{ss} \leteq \slotToSeed{(\bslot{bhb})} \\
-      & ~~~~~~~~~~\var{vrfVk} \leteq \fun{bvkvrf}~\var{bhb} \\
+      & ~~~~~~~~~~\var{slot} \leteq \bslot{bhb} \\
+      & ~~~~~~~~~~\var{vrfK} \leteq \fun{bvkvrf}~\var{bhb} \\
   \end{align*}
   %
   \begin{align*}
-      & \fun{praosVrfChecks} \in \Seed \to \PoolDistr \to \unitInterval \to \BHBody \to \Bool \\
+      & \fun{praosVrfChecks} \in \Seed \to \PoolDistr \to \unitIntervalNonNull \to \BHBody \to \Bool \\
       & \fun{praosVrfChecks}~\eta_0~\var{pd}~\var{f}~\var{bhb} = \\
       & \begin{array}{cl}
-        ~~~~ & \var{hk}\mapsto (\sigma,~\var{hk_{vrf}})\in\var{pd} \\
+        ~~~~ & \var{hk}\mapsto (\sigma,~\var{vrfHK})\in\var{pd} \\
+        ~~~~ \land & \var{vrfHK} = \hashKey{vrfK} \\
         ~~~~ \land & \fun{vrfChecks}~\eta_0~\var{bhb} \\
         ~~~~ \land & \fun{checkLeaderVal}~(\fun{bleader}~\var{bhb})~\sigma~\var{f} \\
       \end{array} \\
       & ~~~~\where \\
-      & ~~~~~~~~~~\var{hk} \leteq \hashKey{(\bvkcold bhb)} \\
-      & ~~~~~~~~~~\var{hk_{vrf}} \leteq \hashKey{(\fun{bvkvrf}~\var{bhb})} \\
+      & ~~~~~~~~~~\var{hk} \leteq \fun{issuerIDfromBHBody}~\var{bhb} \\
+      & ~~~~~~~~~~\var{vrfK} \leteq \fun{bvkvrf}~\var{bhb} \\
   \end{align*}
   %
   \begin{align*}
       & \fun{pbftVrfChecks} \in \KeyHash_{vrf} \to \Seed \to \BHBody \to \Bool \\
-      & \fun{pbftVrfChecks}~\var{vrfh}~\eta_0~~\var{bhb} = \\
+      & \fun{pbftVrfChecks}~\var{vrfHK}~\eta_0~~\var{bhb} = \\
       & \begin{array}{cl}
-        ~~~~ & \var{vrfh} = \hashKey{(\fun{bvkvrf}~\var{bhb})} \\
+        ~~~~ & \var{vrfHK} = \hashKey{(\fun{bvkvrf}~\var{bhb})} \\
         ~~~~ \land & \fun{vrfChecks}~\eta_0~\var{bhb} \\
       \end{array} \\
   \end{align*}

diff --git a/shelley/chain-and-ledger/formal-spec/ledger.tex b/shelley/chain-and-ledger/formal-spec/ledger.tex
@@ -143,7 +143,7 @@ \section{Ledger State Transition}
         \var{pp}\\
         \var{acnt}
       \end{array}
-      \vdash \var{ls} \trans{ledgers}{\epsilon} \varUpdate{\var{ls'}}
+      \vdash \var{ls} \trans{ledgers}{\epsilon} \var{ls}
     }
   \end{equation}
 

diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex
@@ -241,7 +241,7 @@ \subsection{Protocol Parameter Update Proposals}
       \\
       \var{slot} \geq \fun{firstSlot}~((\epoch{slot}) + 1) - 2\cdot\StabilityWindow
       \\
-      \epoch{slot} = e + 1
+      (\epoch{slot})  +1 = e
     }
     {
       \begin{array}{c}