From ff4ce4eb2cae4648f634d344bffcabdd23c55d3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Thu, 30 May 2019 14:13:58 +0200 Subject: [PATCH] Issue #512: implements property #2 of UPIEC STS --- .../src/Ledger/Update/Generators.hs | 27 +++++++- .../test/Ledger/Upiec/Properties.hs | 27 +++++++- byron/ledger/executable-spec/test/Main.hs | 63 ++++++++++++------- 3 files changed, 92 insertions(+), 25 deletions(-) diff --git a/byron/ledger/executable-spec/src/Ledger/Update/Generators.hs b/byron/ledger/executable-spec/src/Ledger/Update/Generators.hs index b8269f1c21c..973881cdc4b 100644 --- a/byron/ledger/executable-spec/src/Ledger/Update/Generators.hs +++ b/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)) diff --git a/byron/ledger/executable-spec/test/Ledger/Upiec/Properties.hs b/byron/ledger/executable-spec/test/Ledger/Upiec/Properties.hs index 509ca704752..a11676b06c2 100644 --- a/byron/ledger/executable-spec/test/Ledger/Upiec/Properties.hs +++ b/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 diff --git a/byron/ledger/executable-spec/test/Main.hs b/byron/ledger/executable-spec/test/Main.hs index 0a421c5b6be..b8518dc31e8 100644 --- a/byron/ledger/executable-spec/test/Main.hs +++ b/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 ]