tezos-protocol-020-PsParisC 20.1

A refutation game proof is required as part of the final move in a game.

This proof is basically a combination of a PVM proof (provided by each implementation of the PVM signature) and an input proof. To check the proof we must check each part separately and then also check that they match on the two points where they touch:

the input_requested of the PVM proof should match the starting point of the input proof ;

the input_given of the PVM proof should match the output message of the input proof.

It is also often the case that the PVM proof has No_input_required for its input_requested and None for its input_given. If this is the case, we don't need the input proof at all and the input_proof parameter in our proof should be None.

type reveal_proof =

| Raw_data_proof of string
(*
The existence of reveal for a given hash when the input_requested is the Needs_reveal Reveal_raw_data.
*)
| Metadata_proof
| Dal_page_proof of {
1. page_id : Dal_slot_repr.Page.t;
2. proof : Dal_slot_repr.History.proof;
}
(*
The existence or not of a confirmed slot for a given page ID when the input_requested is the Needs_reveal Request_dal_page.
*)
| Dal_parameters_proof
(*
Proof for revealing DAL parameters that were used for the slots published at published_level. The published_level parameter enables the kernel to retrieve historical DAL parameters, eliminating the need for each kernel to store past DAL parameters.
*)

The proof that a reveal is valid.

A PVM proof pvm_step is combined with an input_proof to provide the proof necessary to validate a single step in the refutation game.

If the step doesn't involve any input, proof_input_requested pvm_step and proof_input_given pvm_step will be No_input_required and None respectively, and in this case inbox should also be None.

In the case that input is involved, input_proof is either:

a proof of the next inbox message available from the inbox after a given location; this must match up with pvm_step to give a valid refutation proof ; or

a proof of a reveal satisfiability.

a claim that the input involved is the first input of the inbox, which does not need to be proved as we know by construction what is the input (i.e. the Start_of_level of the level after the rollup's origination level).

type input_proof =

| Inbox_proof of {
1. level : Raw_level_repr.t;
2. message_counter : Tezos_protocol_environment_020_PsParisC.Z.t;
3. proof : Sc_rollup_inbox_repr.serialized_proof;
}
| Reveal_proof of reveal_proof
| First_inbox_message

type 'proof t = {

pvm_step : 'proof;
input_proof : input_proof option;

}

type serialized = private string

val serialize_pvm_step : 
  pvm:('state, 'proof, 'output) Sc_rollups.PVM.implementation ->
  'proof ->
  serialized Tezos_protocol_environment_020_PsParisC.Error_monad.tzresult

serialize_pvm_step ~pvm proof turns a structured representation of a step proof of pvm into its serialized representation.

val unserialize_pvm_step : 
  pvm:('state, 'proof, 'output) Sc_rollups.PVM.implementation ->
  serialized ->
  'proof Tezos_protocol_environment_020_PsParisC.Error_monad.tzresult

unserialize_pvm_step ~pvm proof turns a serialized representation of a step proof of pvm into its structured representation.

type Tezos_protocol_environment_020_PsParisC.Error_monad.error +=

| Sc_rollup_proof_check of string

type Tezos_protocol_environment_020_PsParisC.Error_monad.error +=

| Sc_rollup_invalid_serialized_inbox_proof

val serialized_encoding : 
  serialized Tezos_protocol_environment_020_PsParisC.Data_encoding.t

val encoding : 
  serialized t Tezos_protocol_environment_020_PsParisC.Data_encoding.t

val pp : 
  Tezos_protocol_environment_020_PsParisC.Format.formatter ->
  'a t ->
  unit

val start_of_pvm_step : 
  pvm:('state, 'proof, 'output) Sc_rollups.PVM.implementation ->
  'proof ->
  Sc_rollup_repr.State_hash.t

The state hash of the machine before the step. This must be checked against the value in the refutation game as well as checking the proof is valid.

val stop_of_pvm_step : 
  pvm:('state, 'proof, 'output) Sc_rollups.PVM.implementation ->
  'proof ->
  Sc_rollup_repr.State_hash.t

The state hash of the machine after the step. This must be checked against the value in the refutation game as well as checking the proof is valid.

val valid : 
  pvm:('state, 'proof, 'output) Sc_rollups.PVM.implementation ->
  metadata:Sc_rollup_metadata_repr.t ->
  Sc_rollup_inbox_repr.history_proof ->
  Raw_level_repr.t ->
  Dal_slot_repr.History.t ->
  Dal_slot_repr.parameters ->
  dal_activation_level:Raw_level_repr.t option ->
  dal_attestation_lag:int ->
  dal_number_of_slots:int ->
  is_reveal_enabled:Sc_rollup_PVM_sig.is_reveal_enabled ->
  dal_attested_slots_validity_lag:int ->
  'proof t ->
  (Sc_rollup_PVM_sig.input option * Sc_rollup_PVM_sig.input_request)
    Tezos_protocol_environment_020_PsParisC.Error_monad.tzresult
    Tezos_protocol_environment_020_PsParisC.Lwt.t

Check the validity of a proof.

This function requires a few bits of data (available from the refutation game record in the storage):

a snapshot of the inbox, that may be used by the input proof in case it's an inbox message ;

a snapshot of the DAL confirmed slots structure, that may be used by the input proof in case the input is a DAL page ;

the inbox level of the commitment, used to determine if an output from the input proof is too recent to be allowed into the PVM proof ;

DAL related parameters, to be able to check the page content membership to a slot or check the revealed parameters if needed ;

the pvm_name, used to check that the proof given has the right PVM kind.

The level at which DAL is activated (None if the DAL is not enabled). It also returns the optional input executed during the proof and the input_request for the state at the beginning of the proof.

module type PVM_with_context_and_state = sig ... end

val produce : 
  metadata:Sc_rollup_metadata_repr.t ->
  (module PVM_with_context_and_state) ->
  Raw_level_repr.t ->
  is_reveal_enabled:Sc_rollup_PVM_sig.is_reveal_enabled ->
  serialized t Tezos_protocol_environment_020_PsParisC.Error_monad.tzresult
    Tezos_protocol_environment_020_PsParisC.Lwt.t

produce ~metadata pvm_and_state inbox_context inbox_history commit_inbox_level will construct a full refutation game proof out of the state given in pvm_and_state. It uses the inbox if necessary to provide input in the proof. If the input is above or at commit_level it will block it, and produce a proof that the PVM is blocked. If the input requested is a reveal the proof production will also fail.

This will fail if any of the context, inbox_context, inbox_history or dal_slots_history_cache given doesn't have enough data to make the proof. For example, the 'protocol implementation' version of each PVM won't be able to run this function. Similarly, the version of the inbox stored in the L1 won't be enough because it forgets old levels.

This uses the name in the pvm_and_state module to produce an encodable wrapped_proof if possible. See the wrap_proof function in Sc_rollups.

It also need the metadata if it produces a proof for the Needs_metadata state.

module Dal_helpers : sig ... end

package tezos-protocol-020-PsParisC