tezos-protocol-014-PtKathma 20.1

The Proof module wraps the more specific proof types provided earlier in this file into the inbox proof as it is required by a refutation.

type starting_point = {

inbox_level : Raw_level_repr.t;
message_counter : Tezos_protocol_environment_014_PtKathma.Z.t;

}

type t = {

skips : (inbox * inclusion_proof) list;
level : inbox;
inc : inclusion_proof;
message_proof : Tezos_protocol_environment_014_PtKathma.Context.Proof.tree Tezos_protocol_environment_014_PtKathma.Context.Proof.t;

}

An inbox proof has three parameters:

the starting_point specifying a location in the inbox ;

the message, of type Sc_rollup_PVM_sem.input option ;

and a reference inbox.

A valid inbox proof implies the following semantics: beginning at starting_point and reading forward through inbox, the first message you reach will be message.

Usually this is very simple because there will actually be a message at the location specified by starting_point. But in some cases starting_point is past the last message within a level, and then the inbox proof must prove that and also provide another proof starting at the beginning of the next level. This can in theory happen across multiple levels if they are empty, which is why we need a list skips of sub-inboxes.

TODO #2997: an issue to fix the problem of unbounded inbox proofs if the list below can be arbitrarily long (if there are many consecutive empty levels).

val pp : Tezos_protocol_environment_014_PtKathma.Format.formatter -> t -> unit

val encoding : t Tezos_protocol_environment_014_PtKathma.Data_encoding.t

val valid : 
  starting_point ->
  inbox ->
  t ->
  (Sc_rollup_PVM_sem.input option,
    Tezos_protocol_environment_014_PtKathma.Error_monad.error)
    Tezos_protocol_environment_014_PtKathma.Pervasives.result
    Tezos_protocol_environment_014_PtKathma.Lwt.t

See the docstring for

for details of proof semantics.

valid starting_point inbox proof will return the third parameter of the proof, message, iff the proof is valid.

val produce_proof : 
  inbox ->
  (Raw_level_repr.t * Tezos_protocol_environment_014_PtKathma.Z.t) ->
  (t * Sc_rollup_PVM_sem.input option,
    Tezos_protocol_environment_014_PtKathma.Error_monad.error)
    Tezos_protocol_environment_014_PtKathma.Pervasives.result
    Tezos_protocol_environment_014_PtKathma.Lwt.t

TODO #2997 Currently a placeholder, needs implementation.

produce_proof inbox (level, counter) creates an inbox proof proving the first message after the index counter at location level. This will fail if the inbox given doesn't have sufficient data (it needs to be run on an inbox with the full history).

package tezos-protocol-014-PtKathma