[Pipelining] S1: Explicit preconditions and effects for each existing operation
Properly specify the notion/property of validity for operations by following each operation's control flow and dissociating "preconditions" (with their classification) from "effects" -- preconditions might also do effects in the validity state.
- Consensus: Preendorsement, Endorsement, Seed_nonce_revelation
- Anonymous: Double_consensus_operation_evidence, Double_baking_evidence, Activate_account
- Votes: Proposals, Ballot
- Managers: Reveal, Transaction, Origination, Delegation, Set_deposits_limit, Register_global_constant, Tx_rollup_origination, Tx_rollup_submit_batch, Tx_rollup_commit, Sc_rollup_originate, Sc_rollup_add_messages
Edited by Mehdi Bouaziz