Issue #512: implements property #2 of UPIEC STS

byron/ledger/executable-spec/src/Ledger/Update/Generators.hs

@@ -15,6 +15,7 @@ module Ledger.Update.Generators
   , metadata
   -- UPIEC judgement context generators
   , noProtVerChangeJC
+  , protVerChangeJC
   )
 where
 
@@ -25,7 +26,7 @@ import           Hedgehog
 import           Hedgehog.Gen.Aux (doubleInc)
 import qualified Hedgehog.Gen    as Gen
 import qualified Hedgehog.Range  as Range
-import           Ledger.Core (Slot(..), SlotCount(..), BlockCount(..), VKeyGenesis(..), PairSet(..))
+import           Ledger.Core (Slot(..), SlotCount(..), BlockCount(..), VKeyGenesis(..), PairSet(..), minusSlot)
 import qualified Ledger.Core.Generators as CG
 import           Ledger.GlobalParams (k)
 import           Ledger.Update (ProtVer(..), PParams(..), PVBUMP, ApName(..), ApVer(..), Metadata(..), UpId(..), UPIState, UPIEC)
@@ -269,3 +270,27 @@ noProtVerChangeJC = do
  where
   pvbumpNoChangeJC :: Gen (JC PVBUMP)
   pvbumpNoChangeJC = Gen.choice [emptyPVUpdateJC, beginningsNoUpdateJC]
+
+
+-- | Generates a judgement context for properties #2, #3 and #4 of the
+-- UPIEC STS
+protVerChangeJC :: Gen (JC UPIEC)
+protVerChangeJC = do
+  ((s_n, fads), (pv, pps), ()) <- lastProposalJC
+  s'                           <- CG.slot 0 $ upper s_n -- so that it
+                                                        -- passes
+                                                        -- domain
+                                                        -- restriction
+                                                        -- on fads
+  let
+    fad = ( s'
+          , ( pv { _pvMin = _pvMin pv + 1 } -- so that pv != pv'
+            , pps
+            )
+          )
+    fads' = fads ++ [fad]
+  st                           <- upiecState pv pps fads'
+  pure (s_n, st, ())
+ where
+  upper :: Slot -> Word64
+  upper s = unSlot (minusSlot s (SlotCount . (2 *) . unBlockCount $ k))

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

@@ -2,10 +2,12 @@
 
 module Ledger.Upiec.Properties where
 
+import           Control.Lens (_1, _2, (^.))
 import           Control.State.Transition (applySTS, TRC(..))
+import           Ledger.Core (Slot)
 import qualified Ledger.Update.Generators as G
 import           Hedgehog
-import           Ledger.Update (UPIEC)
+import           Ledger.Update (PVBUMP, UPIEC, ProtVer, PParams)
 
 
 -- Property #1 for the UPIEC STS
@@ -19,3 +21,26 @@ noProtVerChange = property $ do
   case applySTS @UPIEC (TRC jc) of
     Right st' -> st === st'
     Left _    -> failure
+
+-- Property #2 for the UPIEC STS
+--
+-- If PVBUMP transitions into a state with a new different protocol
+-- version, the UPIEC STS results in a state that adopts the new
+-- protocol version (pv) and new protocol parameters (pps).
+protVerChangeAdopt :: Property
+protVerChangeAdopt = 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 (pv', pps') -> do
+      case applySTS @UPIEC (TRC jc) of
+        Right st' -> do
+          let (pvst', ppsst') = st' ^. _1 :: (ProtVer, PParams)
+          pv   /== pvst'
+          pv'  === pvst'
+          pps' === ppsst'
+        Left _    -> failure

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

@@ -2,6 +2,11 @@
 
 module Main
   ( main
+  , testGroupDelegEx
+  , testGroupDeleg
+  , testGroupUtxo
+  , testGroupPvbump
+  , testGroupUpiec
   )
 where
 
@@ -12,37 +17,49 @@ 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)
+import Ledger.Upiec.Properties (noProtVerChange, protVerChangeAdopt)
 import qualified Ledger.Delegation.Properties as DELEG
 import Ledger.UTxO.Properties (moneyIsConstant)
 import qualified Ledger.UTxO.Properties as UTxO
 
+testGroupDelegEx :: TestTree
+testGroupDelegEx = testGroup "Delegation Examples" deleg
+
+testGroupDeleg :: TestTree
+testGroupDeleg = testGroup "Delegation Properties"
+  [ testProperty "Certificates are triggered"           dcertsAreTriggered
+  , testProperty "Duplicated certificates are rejected" rejectDupSchedDelegs
+  , testProperty "Traces are classified"                DELEG.tracesAreClassified
+  ]
+
+testGroupUtxo :: TestTree
+testGroupUtxo = testGroup "UTxO Properties"
+  [ testProperty "Money is constant" moneyIsConstant
+  , testProperty "Traces are classified" UTxO.tracesAreClassified
+  ]
+
+testGroupPvbump :: TestTree
+testGroupPvbump =  testGroup "PVBUMP properties"
+  [ testProperty "Same state for no updates"         emptyPVUpdate
+  , testProperty "Same state for early on in chain"  beginningsNoUpdate
+  , testProperty "State determined by last proposal" lastProposal
+  ]
+
+testGroupUpiec :: TestTree
+testGroupUpiec = testGroup "UPIEC properties"
+  [ testProperty "Same state for same prot. ver." noProtVerChange
+  , testProperty "New protocol version adopted"   protVerChangeAdopt
+  ]
+
 main :: IO ()
 main = defaultMain tests
  where
   tests :: TestTree
   tests = localOption Auto $ testGroup
     "Ledger"
-    [ testGroup "Delegation Examples" deleg
-    , testGroup
-      "Delegation Properties"
-      [ testProperty "Certificates are triggered"           dcertsAreTriggered
-      , testProperty "Duplicated certificates are rejected" rejectDupSchedDelegs
-      , testProperty "Traces are classified"                DELEG.tracesAreClassified
-      ]
-    , testGroup
-      "PVBUMP properties"
-      [ testProperty "Same state for no updates"         emptyPVUpdate
-      , testProperty "Same state for early on in chain"  beginningsNoUpdate
-      , testProperty "State determined by last proposal" lastProposal
-      ]
-    , testGroup
-      "UPIEC properties"
-      [ testProperty "Same state for same prot. ver." noProtVerChange
-      ]
-    , testGroup
-      "UTxO Properties"
-      [ testProperty "Money is constant" moneyIsConstant
-      , testProperty "Traces are classified" UTxO.tracesAreClassified
-      ]
+    [ testGroupDelegEx
+    , testGroupDeleg
+    , testGroupUtxo
+    , testGroupPvbump
+    , testGroupUpiec
     ]