diff --git a/executable-spec/decentralized-updates.cabal b/executable-spec/decentralized-updates.cabal index e48be41d..184250b7 100644 --- a/executable-spec/decentralized-updates.cabal +++ b/executable-spec/decentralized-updates.cabal @@ -92,7 +92,6 @@ test-suite ledger-rules-test , Test.Cardano.Ledger.Update.Properties.UpdateSUT , Test.Cardano.Ledger.Update.Properties.UpdateTraceGen , Test.Cardano.Ledger.Update.Properties.Liveness - , Test.Cardano.Ledger.Update.Properties.Safety , Test.Cardano.Ledger.Update.Properties.StateChangeValidity , Test.Cardano.Ledger.Update.Events , Test.Cardano.Ledger.Update.Properties.Examples diff --git a/executable-spec/test/README.md b/executable-spec/test/README.md index 6924fc09..00780365 100644 --- a/executable-spec/test/README.md +++ b/executable-spec/test/README.md @@ -95,12 +95,18 @@ revealed (which means that its voting period is open), then: - In the last voting period, the reached verdict coincides with the outcome we expect (from counting the votes in that period). -This means that if an SIP should be not be approved according to the votes we -see in any of its voting periods, then the system should report it as -not-approved. +The checks above ensure that if an SIP should be not be approved according to +the votes we see in any of its voting periods, then the system should report it +as not-approved. Conversely, they also ensure the proposals with enough votes +are reported as approved by the system. + + We check as well that implementation submissions are always +accepted (one per proposal), and once an implementation is stably +submitted, the corresponding revelation is not rejected. We also check that the system can only enter in the `implementation submitted` -state if the SIP is approved. +state if the SIP is approved. This ensures that a software update that hasn't +been approved will not be allowed to pass to the next phase. ### TODO: similar considerations for implementation votes and endorsements @@ -163,3 +169,45 @@ a different tally result (either because the interval that the system under test considers will be shorter or longer, and contain a different number of votes). ## Dependency and conflict resolving + +# Alternative way to test requirements + +For each proposal `p`: + +- while `p` is in the `unknown` state: + - the system should not reject a valid SIP submission for `p`, this is, a + submission with a valid signature. This is a necessary condition for open + participation. +- when `p` transitions from `unknown` to `SIP submitted`: + - the action that led to the `SIP submitted` state must be the SIP submission + of `p`. + - the length of the trace fragment in which the system is in the `SIP + submitted` state must be less than the length of the stability window. + Otherwise the system would be reporting the state of the SIP incorrectly. +- when `p` transitions from `SIP submitted` to `SIP stably submitted`: + - the difference between the first slot in which `p` was in the `SIP + submitted` state, and the first slot in which `p` was in the `SIP stably + submitted` state must be exactly the length of the stability window. + - there should be no rejections of valid SIP revelations for the commit of + `p`. This is a necessary condition for open participation. + + +# The third option + +## How and why do we test with traces. + +## How and why we divide a trace into events, per update proposal. + +## How do we define the validation criteria + +Per each requirement: + +- Enumerate the state changes that are relevant to it. This means stating which + changes are allowed, and which changes aren't. +- Enumerate the conditions (relative to the requirement) that the transition has + to satisfy. + + +TODO: the fact that no unexpected payload is allowed might have to do with the +no negative impact on performance: allowing votes outside the voting period will +increase the blockchain size. diff --git a/executable-spec/test/Test/Cardano/Ledger/Update/Properties.hs b/executable-spec/test/Test/Cardano/Ledger/Update/Properties.hs index 1e126493..3dd3465d 100644 --- a/executable-spec/test/Test/Cardano/Ledger/Update/Properties.hs +++ b/executable-spec/test/Test/Cardano/Ledger/Update/Properties.hs @@ -21,7 +21,6 @@ import Properties import Test.Cardano.Ledger.UpdateSpec import Test.Cardano.Ledger.Update.Properties.Liveness -import Test.Cardano.Ledger.Update.Properties.Safety hiding (st) import qualified Test.Cardano.Ledger.Update.Properties.StateChangeValidity as StateChangeValidity import Test.Cardano.Ledger.Update.Properties.UpdateSUT import Test.Cardano.Ledger.Update.Properties.UpdateTraceGen @@ -99,29 +98,13 @@ runTests = [ $ forAllTracesShow (updatesAreNotDiscardedDueToBeing Update.Unsupported) showActionsAndStateOfUpdateSpec - -- , testProperty "Updates are discarded due to being superseded" - -- $ expectFailure - -- $ withMaxSuccess 10000 - -- $ forAllTracesShow - -- (updatesAreNotDiscardedDueToBeing Update.Superseded) - -- showActionsAndStateOfUpdateSpec --------------------------------------------------------------------- -- Update system safety properties --------------------------------------------------------------------- - , testProperty "Approved SIP's meet the adoption threshold" - $ withMaxSuccess 5000 - $ prop_approvedSIPsHaveEnoughVotes - , testProperty "Endorsements are correctly tallied" - $ withMaxSuccess 10000 - $ forAllTracesShow prop_endorsementsAreCorrectlyTallied prettyShow - -- TODO: scheduled proposals cannot be canceled. - --------------------------------------------------------------------- - -- Global properties - --------------------------------------------------------------------- - , testProperty "Changes in state of update proposals are valid" - $ withMaxSuccess 5000 - $ forAllTracesShow prop_changesInStateOfAreValid - showActionsAndStateOfUpdateSpec + -- , testProperty "Changes in state of update proposals are valid" + -- $ withMaxSuccess 5000 + -- $ forAllTracesShow prop_changesInStateOfAreValid + -- showActionsAndStateOfUpdateSpec , testProperty "wip: Changes in state of update proposals are valid" $ withMaxSuccess 2000 $ forAllTracesShow diff --git a/executable-spec/test/Test/Cardano/Ledger/Update/Properties/Safety.hs b/executable-spec/test/Test/Cardano/Ledger/Update/Properties/Safety.hs deleted file mode 100644 index fe0bfa83..00000000 --- a/executable-spec/test/Test/Cardano/Ledger/Update/Properties/Safety.hs +++ /dev/null @@ -1,981 +0,0 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} - -module Test.Cardano.Ledger.Update.Properties.Safety where - -import Control.Arrow (second) -import Data.List (find) -import Data.Maybe (catMaybes, fromMaybe, maybeToList) -import Data.Set (Set) - -import qualified Data.Set as Set - -import Cardano.Slotting.Slot (SlotNo) - -import Cardano.Ledger.Assert (Assertion, assert, assertAndReturn, - cShow, exists, failBecause, forall, orElseShow, pass, - (/=!), ( Assert -prop_approvedSIPsHaveEnoughVotes trace = Assert $ - forall (approvedSIPs trace) - (\sip -> exists (votingPeriods sip Update.isSIPRevealed trace) - (hasMajority (_id sip)) - ) --- TODO: we need to introduce coverage testing. Otherwise the properties here --- vacuously hold. - --- | The length of the voting period of an SIP must correspond with the voting --- period length specified in its metadata. --- --- Expired SIP's must have gone through a voting period with the same length as --- declared in the SIP metadata. --- --- Part of requirements: --- --- 8. Metadata-driven update logic. --- --- TODO: you could merge this with @prop_stateOfSIPsAreCorrectlyReported@: when --- a verdict is reached and the verdict says "expired" then the tally slot must --- be the last one, as specified by the voting period duration. -prop_sipVotingPeriodLengthHonorsMetadata - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_sipVotingPeriodLengthHonorsMetadata = undefined - --- | Votes for an SIP are only allowed during the SIP voting intervals. --- --- Part of requirements: --- --- 8. Metadata-driven update logic. -prop_sipVotesAreOnlyAllowedDuringVotingPeriods - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_sipVotesAreOnlyAllowedDuringVotingPeriods = undefined - -hasMajority - :: Id MockSIP - -> (TraceFragment UpdateSUT, SUTSt UpdateSUT) - -> Assertion -hasMajority sipId (votingPeriod, tallyState) = - threshold [MockSIP] -approvedSIPs trace = - filter sipIsApproved traceSIPs - where - traceSIPs - = fmap getSIP - $ tsUpdateSpecs - $ testSetup trace - sipIsApproved sip - = any (Update.isSIP (_id sip) Approved) (validStates trace) - --- | If a revelation signal for `p` exists in the trace, return the slot at --- which it occurred. -revelationSlot - :: Identifiable p - => p - -> (Id p -> SUTSt UpdateSUT -> Bool) - -> Trace UpdateSUT UpdateTraceGen - -> Maybe SlotNo -revelationSlot p isRevealed trace = - case dropWhile (not . isRevealed (_id p)) (validStates trace) of - [] -> Nothing - st:_ -> Just $ currentSlot $ unUpdateSt st - --------------------------------------------------------------------------------- --- Properties of the approval phase --------------------------------------------------------------------------------- - --- | For every stably approved SIP it is possible to summit a commit for its --- implementation and reveal it once the commit is stable on the chain. --- --- Part of requirements: --- --- 2. Decentralized decision making. Part of Property 1: updates voted by the --- majority of the honest stake will eventually move to the next phase. In this --- case, we can only check that an approved SIP is in the (implementation) --- approval phase by making sure the implementation payload for the approved SIP --- is not rejected. --- --- TODO: how to check this? We could take traces with an approved SIP in it, and --- show that we can submit a commit for the implementation. Then we need another --- property in which we take implementations with stable commits, and submit a --- revelation and check that it is accepted. A better alternative might be to --- check in the trace that there are no rejected implementation commits for an --- approved SIP, and that there are no rejected implementation revelations for --- an stable committed implementation. -prop_approvedSIPsEnterTheApprovalPhase - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_approvedSIPsEnterTheApprovalPhase = undefined - --- | Every accepted implementation commit must correspond to an approved SIP. --- --- Part of requirements: --- --- 2. Decentralized decision making. Security goal A: a software update that --- hasn't been approved will not be allowed to pass to the next phase. -prop_acceptedImplementationsCorrespondToApprovedSIPs - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_acceptedImplementationsCorrespondToApprovedSIPs = undefined - --- | See @prop_sipVotingPeriodLengthHonorsMetadata@. -prop_implVotingPeriodLengthHonorsMetadata - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_implVotingPeriodLengthHonorsMetadata = undefined - --- | See @prop_sipVotesAreOnlyAllowedDuringVotingPeriods@. -prop_implVotesAreOnlyAllowedDuringVotingPeriods - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_implVotesAreOnlyAllowedDuringVotingPeriods = undefined - --------------------------------------------------------------------------------- --- Properties of the endorsement phase --------------------------------------------------------------------------------- - --- | Proposals are queued in the activation phase according to their priority. --- --- This property is related property 11: updates with higher priority are --- activated before the ones with lower priorities. In this property we make --- sure that the system handles the priorities in the way specified by the --- proposals' metadata. --- --- Part of requirements: --- --- 8. Metadata-driven update logic. The system must honor the priorities --- specified in the update proposals' metadata. -prop_queueingOfProposals :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_queueingOfProposals = undefined - --- | An approved implementation will enter the activation phase. --- --- TODO: We consider a proposal to be in the activation phase if its state is --- @Queued@ or @BeingEndorsed@. Shouldn't we simply check that endorsements of --- proposals being endorsed are not rejected? --- -prop_approvedImplementationsEnterActivationPhase - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_approvedImplementationsEnterActivationPhase = undefined - --- | The endorsement period of a proposal has __at most__ length specified by --- its metadata, and can be shorter only if said proposal is canceled, or --- scheduled. --- --- Part of requirements: --- --- 8. Metadata-driven update logic. The system must honor the endorsement period --- length specified in the proposals' metadata. -prop_lengthOfEndorsementPeriodIsCorrect - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_lengthOfEndorsementPeriodIsCorrect = undefined - --- | Honest actors cannot be prevented from submitting endorsements. --- --- TODO: here is a possible way of checking this: we can define a function such --- that given an honest participant, for all states of the update system it --- returns an endorsement that is accepted by the update system. - --- TODO: property: allowed state changes. How does this property relates to the --- requirements? Why is this property relevant? Is this a helper property for --- @prop_endorsementsAreCorrectlyTallied@? --- --- We also need a property that states that we can rely on the information given --- by `stateOf`. For instance @stateOf@ should return that a proposal is being --- endorsed exactly when we expect it to. - --- | The state of a proposal at an endorsements-tally-point coincides with the --- tally results. --- --- Part of requirements: --- --- 2. Decentralized decision making: the stakeholders decide with the voting --- power conferred by their stake whether a proposal will be activated. Relates --- to Property 2: updates endorsed by the majority of the stakeholders will be --- eventually applied. --- -prop_endorsementsAreCorrectlyTallied :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_endorsementsAreCorrectlyTallied trace = Assert $ - forall (protocolUpdates trace) - (\pUpdate -> - forall (endorsementPeriods pUpdate trace) - (\period -> - forall (intervals period) - ( \(es, tallySt, threshold, isLast) -> - stateOf pUpdate tallySt ==! ActivationCanceled - ||! - stateOf pUpdate tallySt ==! Queued - ||! - (stateOf pUpdate tallySt - ==! - expectedState pUpdate es tallySt threshold isLast - ) - ) - ) - ) - where - expectedState pUpdate intervalFragment st threshold isLast - | threshold <= stakeOfKeys' es (stakeDistribution st) = Scheduled - | isLast = ActivationExpired - | otherwise = BeingEndorsed - where - es = endorsements pUpdate (validActions intervalFragment) - --- | Scheduled update proposals are eventually applied. --- --- Part of requirements: --- --- 2. Decentralized decision making. This, in combination with --- @prop_endorsementsAreCorrectlyTallied@ imply Property 2. -prop_scheduledProposalsAreApplied :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_scheduledProposalsAreApplied = undefined - --- | Updates are applied to compatible versions. --- --- For every update in the trace, it is applied to the version it declares to --- supersede. --- -prop_updatesAreAppliedToCompatibleVersions - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_updatesAreAppliedToCompatibleVersions = undefined --- TODO: cover test the number of protocol changes in the chain. - --- | Extract the protocol updates from the given trace. -protocolUpdates :: Trace UpdateSUT UpdateTraceGen -> [UpdateSpec] -protocolUpdates trace - = filter (containsAProtocolUpdate . getImpl) - $ tsUpdateSpecs - $ testSetup trace - --- | Determine the endorsement periods of the trace. --- --- An endorsement period starts at the trace state when the given update --- __switches__ to the 'BeingEndorsed' state, and it continues till the update --- is no longer in that state (either because it was activated, canceled, or --- simply not-adopted). --- --- TODO: document what to do in case of incomplete intervals (and hence periods) due to shrinking. -endorsementPeriods - :: UpdateSpec -> Trace UpdateSUT UpdateTraceGen -> [EndorsementPeriod] -endorsementPeriods uspec trace - = fmap (EndorsementPeriod . endorsementIntervals uspec) - $ endorsementPeriods' - $ transitionsList trace - where - endorsementPeriods' [] = [] - endorsementPeriods' aFragment = - case dropWhile (not . inAValidEventState uspecIsBeingEndorsed) aFragment of - [] -> [] -- The update proposal was not endorsed in this fragment, - -- therefore there aren't any endorsement periods in this - -- fragment. - xs -> case spanPlusOne (inAnEventState uspecIsBeingEndorsed) xs of - -- In the interval we also need to return the first state in - -- which the state of the update stopped being endorsed. The - -- reason for this is that it is this state when the tally takes - -- place, and it must therefore be part of the interval. - -- Therefore we use the @spanPlusOne@ function. - -- - -- Due to shrinking it is possible that the state when a - -- proposal stops being endorsed is removed from the trace. In - -- the shrinking we could filter incomplete traces. But this - -- will add some complexity. So in such case we return no - -- endorsement period. - Nothing -> [] -- No interval could be found. - Just (interval, rest) -> interval: endorsementPeriods' rest - where - uspecIsBeingEndorsed st = stateOf uspec st == BeingEndorsed - --- | This function returns a tuple where the first component is the longest --- prefix of the sequence that satisfies the predicate followed by an extra --- element (which does not satisfy the predicate), and the second component is --- the rest of the sequence. If no such prefix could be found, or no element --- that does not satisfy the predicate could be found then this function returns --- @Nothing@. -spanPlusOne :: (a -> Bool) -> [a] -> Maybe ([a], [a]) -spanPlusOne _ [] = Nothing -spanPlusOne p (x:xs) - | p x = - case spanPlusOne p xs of - Nothing -> Nothing -- We could not find a state where @uspec@ is not being endorsed. - Just (ys, zs) -> Just (x:ys, zs) - | otherwise = - Just ([x], xs) - -- In this case @x@ is the first state that doesn't satisfy @p@. - -- Unlike span, we return @x@ in the first component of the tuple so - -- that it becomes part of the endorsement period. - -newtype EndorsementPeriod = - EndorsementPeriod { intervals :: [EndorsementInterval] } - deriving (Show) - --- | Compute the endorsement intervals for the given update specification. The --- trace fragment should correspond to an endorsement period, this is: --- --- - the trace fragment must contain the beginning of the endorsement period. --- --- - the state of the update specification in the first state is --- 'BeingEndorsed'. --- --- - the state of the update specification in the last state should not be --- 'BeingEndorsed'. --- --- The conditions above imply that the trace fragment cannot be empty. --- --- PRECONDITION: --- --- - The trace fragment cannot be empty. --- --- - The update specification should be in the 'BeingEndorsed' state in the --- first state of the trace fragment. --- --- - The update specification is in a state different from 'BeingEndorsed' in --- the last state of the fragment. --- -endorsementIntervals - :: UpdateSpec -> TraceFragment UpdateSUT -> [EndorsementInterval] -endorsementIntervals uspec period = - assert preconditionsHold - [ ( takeWhile - (slotIs (< cutoffSlot)) - period - , tallyState - , adjustedAdoptionThreshold tallyState - , isLast tallyState - ) - | (cutoffSlot, tallySlot) <- cutoffAndTallySlots startSt endSt - , let tallyState = unUpdateSt $ period `firstStateWithSlot` tallySlot - ] - where - preconditionsHold = do - not (null period) `orElseShow` "A trace fragment cannot be empty when computing the endorsement intervals." - stateOf uspec startSt ==! BeingEndorsed - stateOf uspec endSt /=! BeingEndorsed - - startSt = unUpdateSt $ firstState period - - endSt = unUpdateSt $ lastState period - - isLast st = endOfSafetyLag <= currentSlot st + stableAfter st - -- Here we also also need to add stableAfter since the end of the safety lag - -- coincides with the first slot of an epoch: - -- - -- > tallySlot env = nextEpochFirstSlot env - (stableAfter env) - where - endOfSafetyLag = - -- TODO: see if we can remove this duplication w.r.t. module @Activation@. - nextEpochFirstSlot startSt + slotsPerEpoch startSt - - adjustedAdoptionThreshold st = - if isLast st - then - ceiling $ 0.51 * (fromIntegral totalStake' :: Double) - else - stakeThreshold (adversarialStakeRatio st) totalStake' - where - totalStake' = - totalStake @(IState MockSIP MockImpl) - @(EndorserId (Protocol MockImpl)) - st - - --- | Determine the slots at which endorsements stop being counted for each epoch --- (i.e. cutoff slots) between and including the start and end state. --- --- Henceforth we refer to the slot of the start state as __start slot__ and the --- slot of the end state as the __end slot__. --- --- A cutoff slot occurs @2 * stableAfter@ slots before the end of an epoch, --- where @stableAfter@ is maximum number of slots the ledger can rollback. --- --- For each first slot of an epoch @s_i@ that lies in the interval --- --- > [start slot, end slot] --- --- we calculate the cutoff point of the previous epoch as: --- --- > s_i - 2 * stableAfter --- --- This function returns all the cutoff slots that lie in --- --- > [start slot, end slot] --- --- PRECONDITION: --- --- - the current slot of the initial state has to be less or equal than the --- current slot of the final state. --- --- - the number of slots per epoch is greater than twice the value of --- @stableAfter@. -cutoffSlots - :: TracksSlotTime st - => st - -- ^ Initial state from which to start looking for cutoff points. - -> st - -- ^ Final state at which we stop looking for cutoff points. The final state - -- is considered as a potential cutoff point. - -> [SlotNo] -cutoffSlots startSt endSt - = assert preconditionsHold - $ dropWhile (< currentSlot startSt) - $ takeWhile (<= currentSlot endSt) - $ [ slot i | i <- [0..] ] - where - preconditionsHold = do - currentSlot startSt <=! currentSlot endSt - 2 * stableAfter startSt [start slot, end slot] --- --- See function @cutoffSlots@ for more details. --- --- PRECONDITION: --- --- - the current slot of the initial state has to be less or equal than the --- current slot of the final state. --- --- - the number of slots per epoch is greater than twice the value of --- @stableAfter@. --- --- POSTCONDITION: --- --- - All the returned slots are in the range [start slot, end slot] -cutoffAndTallySlots - :: TracksSlotTime st - => st - -- ^ Initial state from which to start looking for cutoff and tally points. - -> st - -- ^ Final state at which we stop looking for cutoff and tally points. The - -- final state is considered as a potential cutoff point. - -> [(SlotNo, SlotNo)] -cutoffAndTallySlots startSt endSt - = assertAndReturn postconditionsHold - $ takeWhile ((<= currentSlot endSt) . snd) - $ [ (cutoffSlot, cutoffSlot + stableAfter startSt) - | cutoffSlot <- cutoffSlots startSt endSt - ] - where - postconditionsHold slotPairs = - forall slotPairs (\(s, t) -> do - currentSlot startSt <=! s - currentSlot startSt <=! t - s <=! currentSlot endSt - t <=! currentSlot endSt - ) - - --- Gather the endorsements of the update given update specification that --- occur in the list of action. -endorsements - :: UpdateSpec -> [SUTAct UpdateSUT] -> Set (EndorserId (Protocol MockImpl)) -endorsements uspec = Set.fromList . catMaybes . fmap extractEndorsement - where - extractEndorsement (UpdateAct (Update.Activation e)) - | Update.endorsedVersion e == protocolVersion uspec - = Just $ Update.endorserId e - extractEndorsement _ - = Nothing - --- | An endorsement interval for a proposal @p@ consists of: --- --- - The trace fragment (actions and states) for that interval. --- --- - The state at which the endorsements are tallied for that interval. --- --- - The activation threshold that holds for that interval. --- --- - Whether this is the last interval of an endorsements period. --- -type EndorsementInterval = - ( [TraceEvent UpdateSUT] - , IState MockSIP MockImpl - , Cardano.Ledger.Update.Env.StakeDistribution.Stake - , Bool - ) - --- | TODO: property: in an endorsement period, the state of a proposal changes --- at tally-endorsement points. - --------------------------------------------------------------------------------- --- Global properties --------------------------------------------------------------------------------- - --- | The changes in the state of an update specification are valid. --- --- Part of requirements: --- --- 3. The update mechanism is a protocol driven process. --- -prop_changesInStateOfAreValid - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_changesInStateOfAreValid trace = Assert $ - forall (tsUpdateSpecs (testSetup trace)) (`changesInStateOfUpdateSpecAreValid` trace) - --- | Function @stateOf@ does not miss any update-proposal state-changes. -prop_changesInUpdateStateAreRegistered - :: Trace UpdateSUT UpdateTraceGen -> Assert -prop_changesInUpdateStateAreRegistered = undefined - -changesInStateOfUpdateSpecAreValid - :: UpdateSpec -> Trace UpdateSUT UpdateTraceGen -> Assertion -changesInStateOfUpdateSpecAreValid updateSpec trace = - eventsAreValid Nothing (updateEvents updateSpec trace) - -- - -- TODO: we also need to check the converse: - -- - -- - after a submission the state is SIP Submitted - -- - after a submission is stable the state should be SIP StablySubmitted - -- - ... the same with a revelation - -- - I'm not sure about the changes in verdict. We might cover this in @prop_sipVotesAreCorrectlyTallied@ - where - eventsAreValid _ [] = pass - eventsAreValid mPrevEvt (nextEvt:xs) = do - validateEvent mPrevEvt nextEvt - eventsAreValid (Just nextEvt) xs - - validateEvent Nothing (SIPSubmission s') = do - stateOf updateSpec (previousSt s') ==! Unknown - getSubmittedSIP (act s') ==! Just (getSIPSubmission updateSpec) - validateEvent Nothing evt = - failBecause $ "First event is not an SIP submission. Seen event: \n" - <> cShow evt - validateEvent (Just prevEvt) evt = - validateEvent' prevEvt evt - - validateEvent' (SIPSubmission s) (SIPStableSubmission s') = do - validateStabilityEvent s s' - validateEvent' (SIPStableSubmission _) (SIPRevelation s') = do - getRevealedSIP (act s') ==! Just (getSIPRevelation updateSpec) - validateEvent' (SIPRevelation s) (SIPStableRevelation s') = do - validateStabilityEvent s s' - validateEvent' (SIPStableRevelation s) (SIPVerdict s') = - validateApprovalEvent (getSIP updateSpec) s s' - validateEvent' (SIPStableRevelation s) (ImplSubmission s') = do - -- If a verdict is reached and there is an implementation already - -- submitted, then we go directly to the @Implementation Submitted@ - -- or @Implementation StablySubmitted@ state. - validateApprovalEvent (getSIP updateSpec) s s' - validateEvent' (SIPStableRevelation s) (ImplStableSubmission s') = do - validateApprovalEvent (getSIP updateSpec) s s' - validateEvent' (SIPVerdict s) (SIPStableVerdict s') = - validateStabilityEvent s s' - validateEvent' (SIPStableVerdict s) (ImplSubmission s') = - getSubmittedImpl (act s') ==! Just (getImplSubmission updateSpec) - validateEvent' (SIPVerdict s) (ImplSubmission s') = - getSubmittedImpl (act s') ==! Just (getImplSubmission updateSpec) - validateEvent' (ImplSubmission s) (ImplStableSubmission s') = - -- TODO: we cannot rely on @stateOf@ to provide accurate information about - -- when an implementation was submitted. The problem is that @stateOf@ does not - -- report the earliest slot at which an implementation was submitted if - -- there is an unapproved SIP. We might need to stop using this function - -- and augmenting the state space of the events if we want higher accuracy. - -- - -- In this case we cannot check anything meaningful. - pass - validateEvent' (ImplStableSubmission s) (ImplRevelation s') = do - -- TODO: We also need to make sure that there is a corresponding stable - -- submission. We cannot check that the implementation submission event - -- since it might not be visible if there is an unapproved SIP. - getRevealedImpl (act s') ==! Just (getImplRevelation updateSpec) - where - implCommit = revelationCommit (getImplSubmission updateSpec) - validateEvent' (ImplRevelation s) (ImplStableRevelation s') = - validateStabilityEvent s s' - validateEvent' (ImplStableRevelation s) (ImplVerdict s') = - validateApprovalEvent (getImpl updateSpec) s s' - validateEvent' (ImplVerdict s) (ImplStableVerdict s') = - validateStabilityEvent s s' - validateEvent' (ImplStableRevelation s) (Queueing s') = - -- In this case the SIP was queued due to being approved and not the - -- highest priority proposal that can be applied to the current version. - validateApprovalEvent (getImpl updateSpec) s s' - validateEvent' (ImplStableRevelation s) (StartOfEndorsement s') = - validateApprovalEvent (getImpl updateSpec) s s' - validateEvent' (ImplStableRevelation s) (Cancellation s') = do - -- A proposal can get from the stable revelation state to being canceled - -- if it was approved at slot @s'@ (i.e. which means it should be a tally - -- slot), and it was either explicitly canceled by a cancellation proposal - -- or implicitly by a proposal with the same version that was approved in - -- the same slot. - validateApprovalEvent (getSIP updateSpec) s s' - -- TODO: if the proposal was canceled then it was due to an implicit - -- cancellation. We do not support explicit cancellations yet. - exists (Update.candidateProtocols (st s')) - (\protocol -> version protocol ==! version (getProtocol updateSpec)) - validateEvent' (ImplStableRevelation s) (Obsoletion s') = - -- A revealed proposal can get approved and immediately obsoleted if the - -- version it supersedes is lower than either the current version or a - -- (potential) scheduled version. - (supersedesVersion (getProtocol updateSpec) version protocol ==! version (getProtocol updateSpec)) - validateEvent' (Queueing s) (Obsoletion s') = - -- A queued proposal can become obsolete if the version it supersedes can - -- never be adopted. - ( supersedesVersion (getProtocol updateSpec) version (getProtocol updateSpec) version protocol version protocol ==! version (getProtocol updateSpec)) - -- TODO: There is an approved explicit cancellation in @s'@. We cannot - -- check this as we do not record the cancellations. - validateEvent' (Scheduling s) (Activation s') = do - -- Proposals are activated at the beginning of an epoch. - currentSlot (st s') ==! nextEpochFirstSlot (st s) - validateEvent' (Activation s) (Obsoletion s') = do - protocolVersion updateSpec " from: " - <> cShow (eventName prevEvt) - <> " to: " - <> cShow (eventName evt) - - validateStabilityEvent s s' = do - currentSlot (previousSt s') tallySlot ==! currentSlot (st s')) - where - revelationSlot = currentSlot (st s) - stableAfter (st s) - maxVotingPeriods = tsMaxVotingPeriods (testSetup trace) - - isAEndorsementTallyPoint s' = - currentSlot (st s') ==! nextEpochFirstSlot (st s') - stableAfter (st s') - --- | Update state change event -data UpdateEvent - = SIPSubmission PreStActSt - -- ^ The SIP is registered as submitted. - | SIPStableSubmission PreStActSt - | SIPRevelation PreStActSt - | SIPStableRevelation PreStActSt - | SIPVerdict PreStActSt - | SIPStableVerdict PreStActSt - | ImplSubmission PreStActSt - | ImplStableSubmission PreStActSt - | ImplRevelation PreStActSt - | ImplStableRevelation PreStActSt - | ImplVerdict PreStActSt - | ImplStableVerdict PreStActSt - | Obsoletion PreStActSt - | Cancellation PreStActSt - | Expiration PreStActSt - | Queueing PreStActSt - | StartOfEndorsement PreStActSt - | Scheduling PreStActSt - | Activation PreStActSt - deriving (Show) - -data PreStActSt = - PreStActSt - { previousSt :: IState MockSIP MockImpl - , act :: SUTAct UpdateSUT - , st :: IState MockSIP MockImpl - } deriving (Show) - -eventName :: UpdateEvent -> String -eventName = takeWhile (/= ' ') . show - --- | Correspondence between update states and update event constructors. -updateStateXupdateEventCtr :: [(UpdateState, PreStActSt -> UpdateEvent)] -updateStateXupdateEventCtr = - [ -- Ideation phase - (SIP Submitted, SIPSubmission) - , (SIP StablySubmitted, SIPStableSubmission) - , (SIP Revealed, SIPRevelation) - , (SIP StablyRevealed, SIPStableRevelation) - , (SIP (Is Approved), SIPVerdict) - , (SIP (Is Rejected), SIPVerdict) - , (SIP (Is WithNoQuorum), SIPVerdict) - , (SIP (Is Expired), SIPVerdict) - , (SIP (IsStably Approved), SIPStableVerdict) - , (SIP (IsStably Rejected), SIPStableVerdict) - , (SIP (IsStably WithNoQuorum), SIPStableVerdict) - , (SIP (IsStably Expired), SIPStableVerdict) - -- Approval phase - , (Implementation Submitted, ImplSubmission) - , (Implementation StablySubmitted, ImplStableSubmission) - , (Implementation Revealed, ImplRevelation) - , (Implementation StablyRevealed, ImplStableRevelation) - , (Implementation (Is Approved), ImplVerdict) - , (Implementation (Is Rejected), ImplVerdict) - , (Implementation (Is WithNoQuorum), ImplVerdict) - , (Implementation (Is Expired), ImplVerdict) - , (Implementation (IsStably Approved), ImplStableVerdict) - , (Implementation (IsStably Rejected), ImplStableVerdict) - , (Implementation (IsStably WithNoQuorum), ImplStableVerdict) - , (Implementation (IsStably Expired), ImplStableVerdict) - -- Activation phase - , (ActivationUnsupported, Obsoletion) - , (ActivationCanceled, Cancellation) - , (ActivationExpired, Expiration) - , (Queued, Queueing) - , (BeingEndorsed, StartOfEndorsement) - , (Scheduled, Scheduling) - , (Activated, Activation) - ] - -updateEvents :: UpdateSpec -> Trace UpdateSUT UpdateTraceGen -> [UpdateEvent] -updateEvents updateSpec trace = - go $ dropWhile ((== Unknown) . stateOfPostState) - $ validTransitionsWithPreviousStates trace - where - go [] = [] - go (preStActSt:xs) = - let (updateState, evt) = mkUpdateEvent updateSpec preStActSt in - evt: go (dropWhile ((== updateState) . stateOfPostState) xs) - stateOfPostState = stateOf updateSpec . unUpdateSt . thrd - where - thrd (x, y, z) = z - --- | Create an update event depending on the state of the given update --- specification, and return the matching update state associated to that event. -mkUpdateEvent - :: UpdateSpec - -> (SUTSt UpdateSUT, SUTAct UpdateSUT, SUTSt UpdateSUT) - -> (UpdateState, UpdateEvent) -mkUpdateEvent updateSpec (aPreSt, anAct, aSt) - = second ($ preStActSt) - $ fromMaybe err - $ find ((== updateSt) . fst) updateStateXupdateEventCtr - where - updateSt = stateOf updateSpec (unUpdateSt aSt) - preStActSt = - PreStActSt - { previousSt = unUpdateSt aPreSt - , act = anAct - , st = unUpdateSt aSt - } - err = error $ "Unmatched update state " - ++ "(no corresponding update event for the given update state): " - ++ show updateSt - --------------------------------------------------------------------------------- --- Generic auxiliary definitions --------------------------------------------------------------------------------- - --- | Get the fragments of a trace where the voting period for the given proposal --- was open, paired with the state at which the tally for that period should --- have taken place. -votingPeriods - :: Proposal p - => p - -> (Id p -> SUTSt UpdateSUT -> Bool) - -> Trace UpdateSUT UpdateTraceGen - -> [(TraceFragment UpdateSUT, SUTSt UpdateSUT)] -votingPeriods prop isRevealed trace = - [ ( trace `fragment` ( tallySlot - (stableAfter env + votingPeriodDuration prop) - , votingPeriodDuration prop - ) - , trace `firstStateWithSlot` tallySlot - ) - | revealedAt <- maybeToList $ revelationSlot prop isRevealed trace - , tallySlot <- tallySlots env prop revealedAt maxVotingPeriods - ] - where - env = unUpdateSt $ initialState trace - maxVotingPeriods = tsMaxVotingPeriods (testSetup trace) - --- | Compute the tally slots for a proposal. --- --- The tally slots of a proposal depend on the proposal's revelation slot, the --- stability parameter, the voting period duration, and the number of voting --- periods. -tallySlots - :: (TracksSlotTime env, Proposal p) - => env - -- ^ Environment that provides the stability parameter. - -> p - -- ^ Proposal for which the tally slots are computed. The proposal determines - -- the maximum number of voting periods. - -> SlotNo - -- ^ Slot in which the proposal was revealed. - -> VotingPeriod - -- ^ Number of voting periods - -> [SlotNo] -tallySlots env prop revealedAt maxVotingPeriods = - [ vpStart + votingPeriodDuration prop + stableAfter env - | vpStart <- votingPeriodStartSlots env prop revealedAt maxVotingPeriods - ] - - -- [ revealedAt + periodOffset (p + 1) + stableAfter env - -- | p <- [0 .. (fromInteger (toInteger maxVotingPeriods) - 1)] - -- ] - -- where - -- periodOffset p = p * (stableAfter env + votingPeriodDuration prop) - --- | Compute the slots at which voting periods start. --- -votingPeriodStartSlots - :: (TracksSlotTime env, Proposal p) - => env - -- ^ Environment that provides the stability parameter. - -> p - -- ^ Proposal for which the start of the voting periods are computed. The - -- proposal determines the maximum number of voting periods. - -> SlotNo - -- ^ Slot in which the proposal was revealed. - -> VotingPeriod - -- ^ Number of voting periods - -> [SlotNo] -votingPeriodStartSlots env prop revealedAt maxVotingPeriods = - [ revealedAt + periodOffset p + stableAfter env - | p <- [0 .. (fromInteger (toInteger maxVotingPeriods) - 1)] - ] - where - periodOffset p = p * (stableAfter env + votingPeriodDuration prop) - -fragment - :: Trace UpdateSUT UpdateTraceGen - -> (SlotNo, SlotNo) - -> TraceFragment UpdateSUT -fragment trace (slotFrom, fragmentLength) - = takeWhile ( slotIs inRange) - $ dropWhile (not . validEventSlotIs inRange) - $ transitionsList trace - -- If there are invalid actions in the range we take them into the fragment. - -- If invalid actions were considered invalid, then the @takeWhile@ above - -- would terminate before reaching the desired slot. - where - inRange slot = slotFrom <= slot && slot < slotFrom + fragmentLength - --- | Return the first state that has a slot equal to the given one. If no such --- state exists an error is thrown. -firstStateWithSlot - :: IsTraceFragment f UpdateSUT => f -> SlotNo -> SUTSt UpdateSUT -firstStateWithSlot trace slot = - case dropWhile ((/= slot) . currentSlot . unUpdateSt) $ validStates trace of - st:_ -> st - [] -> error $ "No state with slot " ++ show slot ++ " was found in the trace." - --- | Determine whether the slot of the event satisfies the predicate. If the --- event is invalid, and therefore carries no state and has no associated slot, --- then the function return true. -slotIs :: (SlotNo -> Bool) -> TraceEvent UpdateSUT -> Bool -slotIs p = inAnEventState (p . currentSlot) - --- | Determine whether the event is valid and the state of the event satisfies --- the given predicate. -validEventSlotIs :: (SlotNo -> Bool) -> TraceEvent UpdateSUT -> Bool -validEventSlotIs p = inAValidEventState (p . currentSlot) - --- | Determine whether the state of the event satisfies the predicate. If the --- event has no state (this is, it is an invalid event) then this function --- returns true. -inAnEventState - :: (IState MockSIP MockImpl -> Bool) - -> TraceEvent UpdateSUT - -> Bool -inAnEventState _ (Invalid {} ) = True -inAnEventState p (Valid {ensuingState}) = p . unUpdateSt $ ensuingState - --- | Determine whether the event is valid and its associated state satisfies the --- predicate. -inAValidEventState - :: (IState MockSIP MockImpl -> Bool) - -> TraceEvent UpdateSUT - -> Bool -inAValidEventState p evt = validEvent evt && inAnEventState p evt diff --git a/executable-spec/test/Test/Cardano/Ledger/Update/Properties/StateChangeValidity.hs b/executable-spec/test/Test/Cardano/Ledger/Update/Properties/StateChangeValidity.hs index 1d7537b6..d11c28b9 100644 --- a/executable-spec/test/Test/Cardano/Ledger/Update/Properties/StateChangeValidity.hs +++ b/executable-spec/test/Test/Cardano/Ledger/Update/Properties/StateChangeValidity.hs @@ -49,6 +49,11 @@ prop_updateEventTransitionsAreValid trace = Assert $ (`updateEventTransitionsForUpdateSpecAreValid` trace) -- TODO: we also need coverage tests for the transitions. +-- +-- TODO: pending checks (which we might be forced to do outside this property): +-- +-- - the first valid implementation submission is never rejected, and subsequent +-- submissions of the same proposal should be. updateEventTransitionsForUpdateSpecAreValid :: UpdateSpec -> Trace UpdateSUT UpdateTraceGen -> Assertion updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do @@ -376,6 +381,9 @@ updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do -- the same version since such proposals should never make it to the -- endorsement period. noActionsAreAllowed updateSpec fragment' + -- TODO: check that if a proposal is scheduled, then @fragment'@ cannot + -- span an epoch boundary. This ensures that scheduled proposals are + -- eventually applied. Required by: decentralized decision making. where st' = unUpdateSt $ firstState fragment' validateTransition (E BeingEndorsed fragment) @@ -539,7 +547,9 @@ validateVerdictEvent prop extractVote votingFragment tallyEvt decision = do -- periods. length proposalVotingPeriods <=! proposalMaxVotingPeriodsI -- If the verdict was @Expired@ then the number of voting periods should equal - -- the maximum number of voting periods. + -- the maximum number of voting periods. This means that expired proposals + -- should have gone through the maximum number of voting periods as specified + -- in its metadata. when (decision == Expired) $ length proposalVotingPeriods ==! proposalMaxVotingPeriodsI -- The slot of the tally state coincides with a tally slot. @@ -559,6 +569,13 @@ validateVerdictEvent prop extractVote votingFragment tallyEvt decision = do -- the SUT) outside the voting period, but not tallied. So it might be better -- to be explicit about this property. -- + -- Also note that this implicitly tests the duration of the voting period: if + -- the voting period allowed by the system differed with regard to the + -- expected length, the we will either see an unexpected vote rejection, or + -- the tally results of the tests will differ due to a vote outside the voting + -- period being accepted and tallied by the update system, but not by our + -- tests. + -- -- TODO: we leave this unchecked for now as it is (partially) checked by the -- tallying tests above. If time allows we might add an explicit check. where