Issue #512: implements properties #3 and #4 of the UPIEC STS

byron/ledger/executable-spec/test/Ledger/Upiec/Properties.hs

@@ -1,10 +1,19 @@
 {-# LANGUAGE TypeApplications #-}
 
-module Ledger.Upiec.Properties where
+module Ledger.Upiec.Properties
+  ( noProtVerChange
+  , protVerChangeAdopt
+  , protVerChangeSameComponents
+  , protVerChangeEmptyComponents
+  ) where
 
-import           Control.Lens (_1, _2, (^.))
+import           Control.Lens (_1, _2, _3, _4, _5, _6, _7, _8, _9, (^.))
 import           Control.State.Transition (applySTS, TRC(..))
-import           Ledger.Core (Slot)
+import           Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
+import           Ledger.Core (Slot, PairSet(..))
+import           Ledger.Update (UpId)
 import qualified Ledger.Update.Generators as G
 import           Hedgehog
 import           Ledger.Update (PVBUMP, UPIEC, ProtVer, PParams)
@@ -44,3 +53,76 @@ protVerChangeAdopt = property $ do
           pv'  === pvst'
           pps' === ppsst'
         Left _    -> failure
+
+-- Property #3 for the UPIEC STS
+--
+-- If PVBUMP transitions into a state with a new different protocol
+-- version, the application versions (avs) and registered software
+-- update proposals (raus) components of UPIEC's state stay the same.
+protVerChangeSameComponents :: Property
+protVerChangeSameComponents = property $ do
+  jc <- forAll G.protVerChangeJC
+  let
+    (s_n, st, _) = jc
+    (pv, pps)    = st ^. _1 :: (ProtVer, PParams)
+    fads         = st ^. _2 :: [(Slot, (ProtVer, PParams))]
+  case applySTS @PVBUMP (TRC ((s_n, fads), (pv, pps), ())) of
+    Left  _ -> failure
+    Right _ -> do
+      case applySTS @UPIEC (TRC jc) of
+        Right st' -> do
+          let
+            pvst' = fst (st' ^. _1) :: ProtVer
+
+            avs   = st  ^. _3
+            avs'  = st' ^. _3
+
+            raus  = st  ^. _5
+            raus' = st' ^. _5
+
+          pv   /== pvst'
+          avs  === avs'
+          raus === raus'
+        Left _    -> failure
+
+-- Property #4 for the UPIEC STS
+--
+-- If PVBUMP transitions into a state with a new different protocol
+-- version, the following components of UPIEC's state are set to an
+-- empty set or map (according to the component's type):
+--
+--   future protocol version adoptions (fads)
+--   registered protocol update proposals (rpus)
+--   confirmed proposals (cps)
+--   proposal votes (vts)
+--   endorsement-key pairs (bvs)
+--   proposal timestamps (pws)
+protVerChangeEmptyComponents :: Property
+protVerChangeEmptyComponents = property $ do
+  jc <- forAll G.protVerChangeJC
+  let
+    (s_n, st, _) = jc
+    (pv, pps)    = st ^. _1 :: (ProtVer, PParams)
+    fads         = st ^. _2 :: [(Slot, (ProtVer, PParams))]
+  case applySTS @PVBUMP (TRC ((s_n, fads), (pv, pps), ())) of
+    Left  _ -> failure
+    Right _ -> do
+      case applySTS @UPIEC (TRC jc) of
+        Right st' -> do
+          let
+            pvst' = fst (st' ^. _1) :: ProtVer
+            fads' = st' ^. _2 :: [(Slot, (ProtVer, PParams))]
+            rpus' = st' ^. _4
+            cps'  = st' ^. _6
+            vts'  = st' ^. _7
+            bvs'  = st' ^. _8
+            pws'  = st' ^. _9 :: Map UpId Slot
+
+          pv /== pvst'
+          assert $     null fads'
+          assert $ Map.null rpus'
+          assert $ Map.null cps'
+          assert $ Set.null . unPairSet $ vts'
+          assert $ Set.null . unPairSet $ bvs'
+          assert $ Map.null pws'
+        Left _    -> failure

byron/ledger/executable-spec/test/Main.hs

@@ -17,7 +17,7 @@ import Test.Tasty.Ingredients.ConsoleReporter (UseColor(Auto))
 import Ledger.Delegation.Examples (deleg)
 import Ledger.Delegation.Properties (dcertsAreTriggered, rejectDupSchedDelegs)
 import Ledger.Pvbump.Properties (emptyPVUpdate, beginningsNoUpdate, lastProposal)
-import Ledger.Upiec.Properties (noProtVerChange, protVerChangeAdopt)
+import Ledger.Upiec.Properties (noProtVerChange, protVerChangeAdopt, protVerChangeSameComponents, protVerChangeEmptyComponents)
 import qualified Ledger.Delegation.Properties as DELEG
 import Ledger.UTxO.Properties (moneyIsConstant)
 import qualified Ledger.UTxO.Properties as UTxO
@@ -47,8 +47,10 @@ testGroupPvbump =  testGroup "PVBUMP properties"
 
 testGroupUpiec :: TestTree
 testGroupUpiec = testGroup "UPIEC properties"
-  [ testProperty "Same state for same prot. ver." noProtVerChange
+  [ testProperty "Same state for the same protocol version" noProtVerChange
   , testProperty "New protocol version adopted"   protVerChangeAdopt
+  , testProperty "App. vers and registered sw upd. proposals stay the same" protVerChangeSameComponents
+  , testProperty "fads, rpus, cps, vts, bvs and pws get reset" protVerChangeEmptyComponents
   ]
 
 main :: IO ()