Add a document explaining how and why the properties of the update me…

…chanism are

tested.

Check that stabilization fragments cannot be longer than the stability window.

[skip ci]

executable-spec/test/README.md

@@ -0,0 +1,165 @@
+# Approach to property based testing
+
+We generate traces of update events. These traces are analyzed per-update
+proposal. Given a trace and an update proposal, we divide the trace in
+_fragments_, where in each fragment the state of a proposal (as reported by the
+update system) remains unchanged. The states a proposal can be in are enumerated
+below:
+
+- unknown: the SIP for the update proposal is not know to the update system.
+
+The division of the trace in fragments depend on the update system giving the
+right information. For instance, it should report the earliest state when an SIP
+was submitted. We have tests in place to make sure the update system reports the
+correct state. These are described in the next section.
+
+# State query tests
+
+## State of an SIP is correctly reported
+- It the update system reports that an SIP submission is unknown in the system,
+  then only implementation submissions corresponding to that SIP are allowed.
+- If the system transitions from `unknown` to `SIP submitted` for a given SIP,
+  then the action that led to the new state must be the submission of said SIP.
+- If an SIP is in a `submitted` state, then only implementation submissions
+  are allowed.
+- If an SIP transitions from `submitted` to `stably submitted`, then the
+  difference between the first slot in which the SIP was reported as `submitted`
+  and the first slot in which it was reported as `stably submitted` is equal to
+  the slot length stability window.
+- The length in slots of a `submitted` fragment cannot exceed the slot length of
+  the stability window.
+
+# Update system requirements
+
+
+
+## Open participation
+
+<!-- what does it mean? -->
+
+<!-- why is it important -->
+
+### No valid update payload is rejected
+
+As long as an update payload is valid, and pays the required fees the system
+should not reject it.
+
+This property is validated through several properties.
+
+> if a SIP submission is rejected, it is because either the signature is
+> invalid, or it was submitted before. The reciprocal of this property implies
+> that a valid submission should be accepted.
+
+In the code we check that for all SIP's, and fragments where the SIP is in an
+`unknown` state, if a submission of a SIP was rejected in that fragment, then
+it is because the signature was invalid.
+
+This ensures that an SIP can always be submitted if it was not submitted before.
+If it was submitted before then the system will not report it as `unknown` (this
+is checked in a different property-test) so this case is not interested for this
+property.
+
+> if a SIP revelation is rejected, it is because either:
+> - the revelation was submitted before
+> - there is no corresponding stable SIP
+
+In the code we check that when an SIP is in the `stably submitted` state, then
+the revelation of this SIP cannot be rejected.
+
+*TODO* we can make an analogous consideration for votes.
+
+## Decentralized decision making
+
+### A SIP voted by enough participants can move to the next phase
+
+In the code we check that for any SIP, in the fragment when the SIP is stably
+revealed (which means that its voting period is open), then:
+
+- No verdict can be reached earlier than the last voting period.
+- 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 approved according to the votes we see in
+any of its voting periods, then the system should report it as approved.
+
+We also check that once an SIP is approved and its implementation submitted, it
+can go into the `implementation submitted` state (and from there proceed with
+the approval phase).
+
+### A SIP not voted by enough participants cannot move to the next phase
+
+It the code we check that for any SIP, in the fragment when the SIP is stably
+revealed (which means that its voting period is open), then:
+
+- No verdict can be reached earlier than the last voting period.
+- 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.
+
+We also check that the system can only enter in the `implementation submitted`
+state if the SIP is approved.
+
+### TODO: similar considerations for implementation votes and endorsements
+
+## On-chain and protocol-driven
+
+### Uniqueness of proposals
+
+For every update proposal there is an unique author that submitted it to the
+chain.
+
+We ensure this by enforcing a commit-reveal scheme.
+
+In the code we check that SIP's and implementations can only be revealed when
+their submissions are stable.
+
+## Transparent and auditable
+
+## Securely activated
+
+### The endorsement threshold at the end of the safety lag is 51%
+
+At the end of the safety lag the activation of a proposal requires 51% of stake
+endorsed.
+
+In the tests we make sure that the threshold we consider at the last endorsement
+interval is 51%.
+
+## Low impact on blockchain performance
+
+## Scalable
+
+## Metadata-driven
+
+### Priorities are honored
+
+Updates with higher priority are activated before the ones with lower priorities
+(priorities are specified in the proposal's metadata)
+
+In the tests we check that when a proposal starts an endorsement period, then
+all the other candidate proposals have lower priority. On the other hand, we
+check that when a proposal is put in the endorsements queue, then any proposal
+`being endorsed` must have a higher priority. Furthermore, we ensure that only
+`scheduled` proposals can be `activated`, and the `activated` state can only be
+reached from the `being endorsed` state. This guarantees that when a proposal is
+activated, the there is no other proposal with higher priority that could have
+been endorsed.
+
+### Voting period duration is honored
+
+The voting period duration of a proposal coincides with the one specified in its
+metadata.
+
+In the tests we divide the fragment in which a proposal is in the `stably
+revealed` state (i.e. its voting interval) in voting periods according to the
+proposal's metadata. The we tally the votes in those periods and make sure no
+valid votes are rejected in any of those period. Thus if the system would have a
+different voting period duration a property based tests with good coverage
+should detect a case in which either a valid vote was rejected, or we arrive at
+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

executable-spec/test/Test/Cardano/Ledger/Update/Events.hs

@@ -84,7 +84,6 @@ noValidActionsFor updateSpec fragment = undefined
 -- TODO: duplicated from module Test.Cardano.Ledger.Update.Properties.Safety
 --------------------------------------------------------------------------------
 
-
 -- | 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.

executable-spec/test/Test/Cardano/Ledger/Update/Properties/StateChangeValidity.hs

@@ -86,11 +86,13 @@ updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do
       -- system has no way to determine if the submission corresponds to an
       -- approved SIP. This information is only available once we have a
       -- revelation.
-      --
       onlyImplementationSubmissionAllowed updateSpec fragment
+      -- A valid SIP's submission corresponding to @updateSpec@ should not be
+      -- rejected in fragment, since in @fragment@ the system under test reports
+      -- that such submission didn't occur.
       forall (invalidActions fragment)
              (\act -> getSubmittedSIP act /=! Just (getSIPSubmission updateSpec)
-                      ||! (not (signatureVerifies (getSIPSubmission updateSpec)))
+                      ||! (not $ signatureVerifies $ getSIPSubmission updateSpec)
                           `orElseShow` "Unexpected SIP submission rejection."
              )
     noUnrightfulRejectionsInUnknowState _                        =
@@ -110,16 +112,9 @@ updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do
       -- allowed, besides implementation commits.
       onlyImplementationSubmissionAllowed updateSpec
                                           (dropFirstValidAction fragment')
-      -- A valid SIP's submission corresponding to @updateSpec@ should not be
-      -- rejected in fragment, since in @fragment@ the system under test reports
-      -- that such submission didn't occur.
-      forall (invalidActions fragment)
-             (\act -> (getSubmittedSIP act /=! Just (getSIPSubmission updateSpec))
-                      ||!
-                      ((not $ signatureVerifies $ getSIPSubmission updateSpec)
-                         `orElseShow` "Unexpected SIP submission rejection."
-                      )
-             )
+      fragmentLengthInSlots fragment' <! stableAfter env
+      where
+        env = unUpdateSt (firstState fragment')
     validateTransition (E (SIP Submitted) fragment)
                        (E (SIP StablySubmitted) fragment') = do
       -- The difference between the two states must be @stableAfter@. Note that
@@ -168,6 +163,9 @@ updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do
         ==! Just (getSIPRevelation updateSpec)
       onlyImplementationSubmissionAllowed updateSpec
                                           (dropFirstValidAction fragment')
+      fragmentLengthInSlots fragment' <! stableAfter env
+      where
+        env = unUpdateSt (firstState fragment')
     validateTransition (E (SIP Revealed) fragment)
                        (E (SIP StablyRevealed) fragment') = do
       validateStabilityEvent fragment fragment'
@@ -176,6 +174,8 @@ updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do
       onlyImplementationSubmissionOrSIPVotesAllowed
         updateSpec
         (dropFirstValidAction fragment')
+      -- TODO: we need to test also that if the trace terminates in a
+      -- @StablyRevealed@ state, then no verdict was possible in that fragment.
     validateTransition (E (SIP StablyRevealed) fragment)
                        (E (SIP (Is what)) fragment') = do
       validateVerdictEvent (getSIP updateSpec)
@@ -231,11 +231,17 @@ updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do
       getSubmittedImpl (firstAction fragment')
         ==! Just (getImplSubmission updateSpec)
       onlyEndorsementsAreAllowed updateSpec (dropFirstValidAction fragment')
+      fragmentLengthInSlots fragment' <! stableAfter env
+      where
+        env = unUpdateSt (firstState fragment')
     validateTransition (E (SIP (IsStably Approved)) fragment)
                        (E (Implementation Submitted) fragment') = do
       getSubmittedImpl (firstAction fragment')
         ==! Just (getImplSubmission updateSpec)
       onlyEndorsementsAreAllowed updateSpec (dropFirstValidAction fragment')
+      fragmentLengthInSlots fragment' <! stableAfter env
+      where
+        env = unUpdateSt (firstState fragment')
     validateTransition (E (Implementation Submitted) fragment)
                        (E (Implementation StablySubmitted) fragment') = do
       -- Because the implementation submission might have occurred before
@@ -251,6 +257,9 @@ updateEventTransitionsForUpdateSpecAreValid updateSpec trace = do
       getRevealedImpl (firstAction fragment')
         ==! Just (getImplRevelation updateSpec)
       onlyEndorsementsAreAllowed updateSpec (dropFirstValidAction fragment')
+      fragmentLengthInSlots fragment' <! stableAfter env
+      where
+        env = unUpdateSt (firstState fragment')
     validateTransition (E (Implementation Revealed) fragment)
                        (E (Implementation StablyRevealed) fragment') = do
       -- TODO: check this transition
@@ -1085,6 +1094,13 @@ mapAdjacent :: (a -> a -> b) -> [a] -> [b]
 mapAdjacent _ [] = []
 mapAdjacent f xs = zipWith f xs (tail xs)
 
+-- | Compute the difference between the first and last slot of the fragment.
+fragmentLengthInSlots :: TraceFragment UpdateSUT -> SlotNo
+fragmentLengthInSlots fragment =
+  currentSlot stN - currentSlot st0
+  where
+    st0  = unUpdateSt (firstState fragment)
+    stN  = unUpdateSt (lastState fragment)
 --------------------------------------------------------------------------------
 -- TODO: duplicated from module Test.Cardano.Ledger.Update.Properties.Safety
 --------------------------------------------------------------------------------