Issue #729 Sync executable with formal spec - PPUP

IntersectMBO · Aug 14, 2019 · 19af2e8 · 19af2e8
1 parent 11421e1
commit 19af2e8
Show file tree

Hide file tree

Showing 6 changed files with 38 additions and 9 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs b/shelley/chain-and-ledger/executable-spec/src/BaseTypes.hs
@@ -14,6 +14,7 @@ module BaseTypes
   , Seed(..)
   , mkNonce
   , (⭒)
+  , (==>)
   ) where
 
 
@@ -82,3 +83,7 @@ a ⭒ b = SeedOp a b
 
 mkNonce :: Integer -> Seed
 mkNonce = Nonce
+
+(==>) :: Bool -> Bool -> Bool
+a ==> b = not a || b
+infix 1 ==>
diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Ppup.hs
@@ -10,22 +10,27 @@ where
 import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 
+import           BaseTypes
 import           BlockChain
 import           Keys
+import           PParams
 import           Slot
 import           Updates
 
 import           Control.State.Transition
+import           Data.Ix (inRange)
+import           Numeric.Natural (Natural)
 
 data PPUP dsignAlgo
 
 instance DSIGNAlgorithm dsignAlgo => STS (PPUP dsignAlgo) where
   type State (PPUP dsignAlgo) = PPUpdate dsignAlgo
   type Signal (PPUP dsignAlgo) = PPUpdate dsignAlgo
-  type Environment (PPUP dsignAlgo) = (Slot, Dms dsignAlgo)
+  type Environment (PPUP dsignAlgo) = (Slot, PParams, Dms dsignAlgo)
   data PredicateFailure (PPUP dsignAlgo)
     = NonGenesisUpdatePPUP (Set.Set (VKeyGenesis dsignAlgo)) (Set.Set (VKeyGenesis dsignAlgo))
     | PPUpdateTooEarlyPPUP
+    | PPUpdateEmpty
     | PPUpdateNonEmpty
     | PVCannotFollowPPUP
     deriving (Show, Eq)
@@ -34,19 +39,29 @@ instance DSIGNAlgorithm dsignAlgo => STS (PPUP dsignAlgo) where
 
   transitionRules = [ppupTransitionEmpty, ppupTransitionNonEmpty]
 
+pvCanFollow :: (Natural, Natural, Natural) -> Ppm -> Bool
+pvCanFollow (mjp, mip, ap) (ProtocolVersion (mjn, mn, an))
+  = (mjp, mip, ap) < (mjn, mn, an)
+  && inRange (0,1) (mjn - mjp)
+  && ((mjp == mjn) ==> (mip + 1 == mn))
+  && ((mjp + 1 == mjn) ==> (mn == 0))
+pvCanFollow _ _ = True
+
 ppupTransitionEmpty :: TransitionRule (PPUP dsignAlgo)
 ppupTransitionEmpty = do
-  TRC ((_, _), pupS, PPUpdate pup') <-
+  TRC ((_, _, _), pupS, PPUpdate pup') <-
     judgmentContext
   do
     Map.null pup' ?! PPUpdateNonEmpty
     pure pupS
 
 ppupTransitionNonEmpty :: DSIGNAlgorithm dsignAlgo => TransitionRule (PPUP dsignAlgo)
 ppupTransitionNonEmpty = do
-  TRC ((s, Dms _dms), pupS, pup@(PPUpdate pup')) <-
+  TRC ((s, pp, Dms _dms), pupS, pup@(PPUpdate pup')) <-
     judgmentContext
   do
+    pup' /= Map.empty ?! PPUpdateEmpty
+    all (all (pvCanFollow (_protocolVersion pp))) pup' ?! PVCannotFollowPPUP
     (Map.keysSet pup' `Set.isSubsetOf` Map.keysSet _dms)
       ?! NonGenesisUpdatePPUP (Map.keysSet pup') (Map.keysSet _dms)
     let Epoch slotEpoch = epochFromSlot (Slot 1)

diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Up.hs
@@ -12,6 +12,7 @@ where
 import qualified Data.Map.Strict as Map
 
 import           Keys
+import           PParams
 import           Slot
 import           Updates
 
@@ -30,7 +31,7 @@ instance DSIGNAlgorithm dsignAlgo => STS (UP dsignAlgo) where
       , Applications
       )
   type Signal (UP dsignAlgo) = Update dsignAlgo
-  type Environment (UP dsignAlgo) = (Slot, Dms dsignAlgo)
+  type Environment (UP dsignAlgo) = (Slot, PParams, Dms dsignAlgo)
   data PredicateFailure (UP dsignAlgo)
     = NonGenesisUpdateUP
     | AvupFailure (PredicateFailure (AVUP dsignAlgo))
@@ -45,11 +46,11 @@ upTransition
    . DSIGNAlgorithm dsignAlgo
   => TransitionRule (UP dsignAlgo)
 upTransition = do
-  TRC (env, (pupS, aupS, favs, avs), Update pup _aup) <- judgmentContext
+  TRC ((_slot, pp, _dms), (pupS, aupS, favs, avs), Update pup _aup) <- judgmentContext
 
-  pup' <- trans @(PPUP dsignAlgo) $ TRC (env, pupS, pup)
+  pup' <- trans @(PPUP dsignAlgo) $ TRC ((_slot, pp, _dms), pupS, pup)
   (aup', favs', avs') <-
-    trans @(AVUP dsignAlgo) $ TRC (env, (aupS, favs, avs), _aup)
+    trans @(AVUP dsignAlgo) $ TRC ((_slot, _dms), (aupS, favs, avs), _aup)
 
   pure (pup', aup', favs', avs')
 

diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs
@@ -90,7 +90,7 @@ utxoInductive = do
   let u' = applyUTxOUpdate u txbody  -- change UTxO
 
   -- process Update Proposals
-  ups' <- trans @(UP dsignAlgo) $ TRC ((_slot, _dms), u ^. ups, txup tx)
+  ups' <- trans @(UP dsignAlgo) $ TRC ((_slot, pp, _dms), u ^. ups, txup tx)
 
   pure
     $  u'

diff --git a/shelley/chain-and-ledger/formal-spec/update.tex b/shelley/chain-and-ledger/formal-spec/update.tex
@@ -30,6 +30,7 @@ \section{Updates}
     \left(
       \begin{array}{r@{~\in~}lr}
         \var{slot} & \Slot & \text{current slot}\\
+        \var{pp} & \PParams & \text{protocol parameters}\\
         \var{dms} & \VKeyGen\mapsto\VKey & \text{genesis key delegations} \\
       \end{array}
     \right)
@@ -55,6 +56,7 @@ \section{Updates}
     {
       \begin{array}{l}
         \var{slot}\\
+        \var{pp}\\
         \var{dms}\\
       \end{array}
       \vdash \var{pup_s}\trans{ppup}{pup}\var{pup_s}
@@ -70,13 +72,15 @@ \section{Updates}
       &
       \dom{pup}\subseteq\dom{dms}
       \\
-      \var{ppv}\mapsto\var{v}\in\var{pup}\implies\fun{pvCanFollow}~(\fun{ppv}~\var{pup_s})~\var{v}
+      \forall\var{ps}\in\range{pup},~
+        \var{pv}\mapsto\var{v}\in\var{ps}\implies\fun{pvCanFollow}~(\fun{pv}~\var{pp})~\var{v}
       \\
       \var{slot} < \firstSlot{((\epoch{slot}) + 1) - \SlotsPrior}
     }
     {
       \begin{array}{l}
         \var{slot}\\
+        \var{pp}\\
         \var{dms}\\
       \end{array}
       \vdash
@@ -321,6 +325,7 @@ \section{Updates}
     \left(
       \begin{array}{r@{~\in~}lr}
         \var{slot} & \Slot & \text{current slot}\\
+        \var{pp} & \PParams & \text{protocol parameters}\\
         \var{dms} & \VKeyGen\mapsto\VKey & \text{genesis key delegations} \\
       \end{array}
     \right)
@@ -360,6 +365,7 @@ \section{Updates}
         \left(
           \begin{array}{r}
             \var{slot} \\
+            \var{pp} \\
             \var{dms} \\
           \end{array}
         \right)
@@ -401,6 +407,7 @@ \section{Updates}
     {
       \begin{array}{l}
         \var{slot}\\
+        \var{pp} \\
         \var{dms}\\
       \end{array}
       \vdash

diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex
@@ -301,6 +301,7 @@ \subsection{UTxO Transitions}
         \left(
           \begin{array}{r}
             \var{slot} \\
+            \var{pp} \\
             \var{dms} \\
           \end{array}
         \right)