Operation Validation

Operation Validation ==================== **Goal:** This document gives elements to drive the validation definition of new operations. First, it recalls some documentation pointers, then provides higher-level specifications and focus on the special case of manager operations. Finally, it gives some guidance for designing and testing new operation validity. **Spoiler** This is also a draft in progress for a new entry in `docs/developers` ## Existing documentation - [Online](https://tezos.gitlab.io/lima/validation.html) - [Ocaml documentation](https://tezos.gitlab.io/api/odoc/_html/tezos-protocol-alpha/Tezos_raw_protocol_alpha/Validate/index.html) extracted from the `.mli` file as well as [here](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml) for the `.ml` file that can contain some more inforamtion. - [Regression and new operations Testing](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_sanity.ml) Please, do not hesitate to make remarks or directly add documentation to improve the clarity, and let us know in case of information lacking. ## High-level specification A **block** is **valid** in a context if it can be applied successfully in this context (ie. the effects of all its operations take place, e.g. balance updates, as well as global effects like liquidity baking or baking fees, and the chain progresses). The **validity of an operation** is examined in either of two contexts: - (BV) When the operation is included in a given block that is being validated, the context for the validation of the operation is the context of the block and the other previously validated operations of the block. - (MV) When the operation is being validated by the shell for potential inclusion in the mempool, the context for its validation is the current head of the mempool and the other validated operations that are already present in the mempool. In (BV) case, the operation is **valid** if its application does not fail, or in other words if it does not make the block invalid. In (MV) case, the operation is **valid** if it is possible to craft a valid block containing this operation as well as any desired subset of the operations already present in the mempool (adding supplemental consensus operations if needed to reach quorum). Operation validity may be split into two separate properties: 1. **Individual validity**: The application effects of the considered operation must succeed in the context of the block or mempool head. This property consists in a set of predicates on the operation payload and context (e.g. the operation is correctly signed), and is implemented by the `check_operation` function of `validate.ml`. Except for manager operations that will be detailled later, the conditions are defined by the operation logic/semantics. 2. **Conflict-freeness**: The operation must be compatible with the other valid operations in the block or mempool, i.e. the application effects of one operation must not break the applicability of another operation. This property is implemented by the `check_operation_conflict` function of `validate.ml`. ### Conflict-freeness The second property is a form of commutativity of a set of valid operations (though we do not require that their application in any order always yield the same result, only that it always succeed). It is more appropriate to talk about **the conflict-freeness applicability of valid operations in a context**. **Motivation**: In the (MV) case, we don't now yet in which order the mempool operations will be included in a block. We don't want to impose an order on them, to be able to replace old operations when we get a similar one with better fees, and to give more freedom to the baker when it selects operations. Therefore, we require a strong conflict-freeness property: any subset of valid operations must be applicable in any order (as long as validation pass order is respected). In the (BV) case, the property could have been loosened since the operations already are in a fixed order; however we decided to demand the same strong property for 1) consistency and 2) to allow for potential concurrent validation of the block's operations in the future. More specifically, let's denote $appliable(op,C)$ the applicability of the operation $op$ in the context $C$. We define the **co-validity** of two operations $op_1$ et $op_2$ in context $C$ as follows: $$appliable(op_1,C) ~\land~appliable(op_2,C)$$$$\land~ appliable(op_2, ~apply(op_1,C)~)~\land~ appliable(op_1,~apply(op_2,C)~).$$ However, our goal is to avoid applying for defining validation :) Rather than computing $apply(op_1,C)$, we see it as $C \leftarrow effects(op_1)$, where $effects(op)$ denotes the effect set on a context defining $op$ semantics. An effect is either the allocation, deallocation or updating of a location (a "key") in a context. Hence, to obtain the *co-validity* property, one should determine the location interferences between $op_1$ effects -- $modifies(effects(op_1))$ -- and $op_2$ applicability -- $accesses(appliable (op_2))$: $$interference(op_1,op_2) = modifies(effects(op_1)) \cap accesses(appliable(op_2)).$$ Naively, enforcing $interference(op_1,op_2) = \epsilon \land interference(op_2,op_1)$ provides *co-validity* but it is not realistics. More reasonably, allowing interference that preserves applicability satisfaction fits more realism for any location $l$ in $interference(op_1,op_2)$, the effects on $l$ in $effect(op_1)$ do not change the satisfaction of $appliable(op_2)$. Finally, defining **restrictions that enforce the preservation of applicability satisfaction** provides the optimal result. This is the option we choose, since the definition of the *one-manager* restriction. In the design phase of operation validation, we performed a non-automatic static analysis to compute interferences and restrictions as well as the applicability: https://hackmd.io/tmL-DE0JSBulGecOwFN2Kg Their implementation is documented in https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml ## Manager Operations Validity Now let's focus on the tricky ones, the manager operations. *A contrario* to the other kind of operations, they have two phases in their applications: - **take fee**, and then - **semantics application** on the context. A very important property of manager operation application is that as long as *take fee* succeeds, any *semantics application* failure is handled **locally** and is **not** considered a failure at the scale of operation/block validation or application. More specifically in practice, if *semantics application* fails, then the operation has no other effects than fee taking, but the block application is perfectly happy with this and succeeds. Therefore, the *applicability* of a manager operation only concerns its *take fee* success. However its conflict-freeness and restrictions definitions do take its *semantics application* into account. ### Conflict-freeness The conflict-freeness for manager operations relies on the *One Manager Operation per Manager restriction* **(1M)**, where a batch is one operation according to the definition of operations. Consider two manager operations, $op_1$ and $op_2$, $bal(manager(op_1),bal(manager(op_2)),counter(manager(op_1)),counter(manager(op_2)) \in interference(op_1,op_2)). $counter(manager(op_1))$ is increases while $counter(manager(op_2))$ must match the one awaiting in the context; and $fee(op_1)$ is withdraw from $bal(manager(op_1))$ when *take fee* of $op_1$ application succeeds while $bal(manager(op_2))$ should contain enough tez to pay $fee(op_2)$. (a) In case $manager(op_1)=manager(op_2)(=manager)$, we have $appliable(op_1,C)$, $appliable(op_2,C)$ but $apply(op_1,C) = C' \land \lnot appliable(op_2,C'),$. For sure $counter(manager,C')$ is in the past. Even with another anti-replay mechanism (another counter algebra), we could have $bal(manager, C) \geq fee(op_2)$ but $bal(manager, C') < fee(op_2)$. (b) Besides, it is possible that during the semantics application of $op_1$, $bal(manager(op_1))$ decreases. However, this will happen only once $op_1$ *take fee* is performed. **1M** avoids situations as (a) and (b), there is no other operation effect that decreases a manager operation balance or increases its counter. ### Applicability $appliable(op,C) \rightarrow \exists C', take fee(op,C) = C'.$ *take fee* does more than transfering $fee(op)$ to the baker, it increases $counter(manager(op))$ and decreases the available gas in the block. Counter algebra and gas consumption are part of the security mechanism guaranteeing consistency and liveness of the blockchain: counter algebra is an anti-replay mechanism, while the gas consumption limits on chain executions. Any manager operation applicability must guarantee that those mechanisms applications will succeed, and check that the manager balance enables the fee payment. While the anti-replay mechanism is generic to any manager operations, only certain ones consume more than the minimal consumption of any manager operation, such as smart contract origination. In that case, the applicability checks the consistency of the announced gas consumption aka `consume_decoding_gas`: [consume decoding gas](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L2239) Manager operation validation is documented in the code: https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L2070 ## Tests As operation validation is a critical component of the protocol, it comes with a regression testing flow. Every operation validity must be checked: https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_sanity.ml ensures that every operation has a defined generator. ### Manager Operations Manager operations generators are defined in [manager operation generators](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/manager_operation_helpers.ml#L650) Their compliance observation is defined in [behavior observations](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/manager_operation_helpers.ml#L1279) The test for applicability are in [manager validity](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_manager_operation_validation.ml) and for batches in [batch validity](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_validation_batch.ml) **(1M)** is tested in [1M](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_1m_restriction.ml) ### Applicability of Non-Manager Operations We complete the existing tests with observational tests such as for the voting ones [Voting validity](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/operations/test_voting.ml#L1234) ### Co-validity testing It requires building a set of operations and a context in which those operations are valid. A generation descriptor must be provided for each kind of operation [generator description](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/generator_descriptors.mli) The tests are implemented in [co-validity](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_covalidity.ml) This implementation has been validated by tests as follows: - for *applicability* (see tests in `integration/consensus/` and `integration/operation/test_voting`) - for *conflict-freeness* (see `integration/validate/test_covalidity.ml`) ## Validation of New Operations ### At design time #### New Manager Operation - identify its applicability predicates, and - define the restrictions that will ensure the conflict-freeness property. #### New Non Manager Operation - make sure that 1M restriction is enough to ensure conflict freeness, - if the operation consumes more than the minimal gas for any manager operation, check the consistency of the announced gas consumption using [consume_decoding_gas](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L2070). ### In the implementation For each validation pass, a module is defined in [Validate](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml) in which for each operation of this validation pass there must be 3 functions: - `check_<op>` that is the appliable predicate for <op> - `add_<op>` that checks <op> application is conflict-free with the applicability of already validated operations and update the validation state to ensure that future valid operation will not be in conflict with it. - `remove_<op>` in Mempool mode, when a conflict occurs, according to the conflict handler, one of the operations involved in this conflict will be invalidated: it is then required to remove its information from the validation state. The Validation state contains an [operation_conflict_state](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L435) that aggregates a set of sets of states by validation pass. Each state by validation pass is the set of state that implements the restriction related to each operation kind in this validation pass. By validation pass module and restriction state: - [Consensus module](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L513) and [Consensus state](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L127) - [Voting](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L1204) and [Voting state](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L192) - [Anonymous](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L1507) and [Anonymous state](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L267) - [Manager](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L2070) and [Manager state](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L350) #### New Manager Operation - Make sure that 1M is enough, if not, well let's meet - Add the 3 required functions for this new manager operation. If this new manager operation consumes more than the minimal gas for any manager operation, make sure that [consume_decoding_gas](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/validate.ml#L2070) is part of the `check_<op>` function. #### New Non Manager Operation - Make sure that the module for its validation pass and the corresponding state exist, if not, well let's meet - Add in the state what it is required to handle the restriction for this new operation, - Add in the module the 3 required functions ### Testing and regression testing Launching the protocol tests will fail when adding a new operation thanks to the [sanity test](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_sanity.ml), unless a generator for it has been implemented. This enforces testing the new operation validity and not breaking the existing operation validity. #### New Manager Operation For adding the generator of a new manager operation, follows the instruction [here](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_sanity.ml#L39). If the operation consumes more gas than the minimal consumption for any manager operation, its kind should return true in [is_consumer](https://gitlab.com/nomadic-labs/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/manager_operation_helpers.ml#L1615) #### New Non Manager Operation For adding a new non-manager operation generator follows [these ones](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/test_sanity.ml#L117) which leads [here](https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/test/integration/validate/generator_descriptors.mli#L113).