Remove Safety module, which was superseded by StateChangeValidity…

…. [skip ci]

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

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.
+
+<!-- TODO: --> We check as well that implementation submissions are always
+accepted (one per proposal), and <!-- DONE: --> 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.

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