Skip to main content

🦏 Sc_rollup_PVM_sig.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.

Module inbox_message.
  Record record : Set := Build {
    inbox_level : Raw_level_repr.t;
    message_counter : Z.t;
    payload : Sc_rollup_inbox_message_repr.serialized;
  }.
  Definition with_inbox_level inbox_level (r : record) :=
    Build inbox_level r.(message_counter) r.(payload).
  Definition with_message_counter message_counter (r : record) :=
    Build r.(inbox_level) message_counter r.(payload).
  Definition with_payload payload (r : record) :=
    Build r.(inbox_level) r.(message_counter) payload.
End inbox_message.
Definition inbox_message := inbox_message.record.

Inductive reveal_data : Set :=
| Raw_data : string reveal_data
| Metadata : Sc_rollup_metadata_repr.t reveal_data
| Dal_page : option Dal_slot_repr.Page.content reveal_data.

Inductive input : Set :=
| Inbox_message : inbox_message input
| Reveal : reveal_data input.

Definition pp_inbox_message
  (fmt : Format.formatter) (function_parameter : inbox_message) : unit :=
  let '{|
    inbox_message.inbox_level := inbox_level;
      inbox_message.message_counter := message_counter
      |} := function_parameter in
  Format.fprintf fmt
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "<v 2>"
              CamlinternalFormatBasics.End_of_format) "<v 2>"))
        (CamlinternalFormatBasics.String_literal "level: "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@," 0 0)
              (CamlinternalFormatBasics.String_literal "message index: "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Formatting_lit
                    CamlinternalFormatBasics.Close_box
                    CamlinternalFormatBasics.End_of_format)))))))
      "@[<v 2>level: %a@,message index: %a@]") Raw_level_repr.pp inbox_level
    Z.pp_print message_counter.

Definition pp_reveal_data
  (fmt : Format.formatter) (function_parameter : reveal_data) : unit :=
  match function_parameter with
  | Raw_data _Format.pp_print_string fmt "raw data"
  | Metadata metadataSc_rollup_metadata_repr.pp fmt metadata
  | Dal_page content_opt
    Format.pp_print_option
      (Some
        (fun (fmt : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string fmt "<No_dal_data>"))
      (fun (fmt : Format.formatter) ⇒
        fun (_a : Dal_slot_repr.Page.content) ⇒
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<Some_dal_data>"
                CamlinternalFormatBasics.End_of_format) "<Some_dal_data>")) fmt
      content_opt
  end.

Definition pp_input (fmt : Format.formatter) (function_parameter : input)
  : unit :=
  match function_parameter with
  | Inbox_message msg
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<v 2>"
                CamlinternalFormatBasics.End_of_format) "<v 2>"))
          (CamlinternalFormatBasics.String_literal "inbox message:"
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@," 0 0)
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Formatting_lit
                  CamlinternalFormatBasics.Close_box
                  CamlinternalFormatBasics.End_of_format)))))
        "@[<v 2>inbox message:@,%a@]") pp_inbox_message msg
  | Reveal reveal
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<v 2>"
                CamlinternalFormatBasics.End_of_format) "<v 2>"))
          (CamlinternalFormatBasics.String_literal "reveal: "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.Formatting_lit
                CamlinternalFormatBasics.Close_box
                CamlinternalFormatBasics.End_of_format)))) "@[<v 2>reveal: %a@]")
      pp_reveal_data reveal
  end.

[inbox_message_encoding] encoding value for {!inbox_message}.
Definition inbox_message_encoding : Data_encoding.encoding inbox_message :=
  Data_encoding.conv
    (fun (function_parameter : inbox_message) ⇒
      let '{|
        inbox_message.inbox_level := inbox_level;
          inbox_message.message_counter := message_counter;
          inbox_message.payload := payload
          |} := function_parameter in
      (inbox_level, message_counter, payload))
    (fun (function_parameter : Raw_level_repr.t × Z.t × string) ⇒
      let '(inbox_level, message_counter, payload) := function_parameter in
      let payload := Sc_rollup_inbox_message_repr.unsafe_of_string payload in
      {| inbox_message.inbox_level := inbox_level;
        inbox_message.message_counter := message_counter;
        inbox_message.payload := payload; |}) None
    (Data_encoding.obj3
      (Data_encoding.req None None "inbox_level" Raw_level_repr.encoding)
      (Data_encoding.req None None "message_counter" Data_encoding.n_value)
      (Data_encoding.req None None "payload"
        (Data_encoding.string' None Data_encoding.Hex))).

Definition reveal_data_encoding : Data_encoding.encoding reveal_data :=
  let case_raw_data : Data_encoding.case reveal_data :=
    Data_encoding.case_value "raw data" None (Data_encoding.Tag 0)
      (Data_encoding.obj2
        (Data_encoding.req None None "reveal_data_kind"
          (Data_encoding.constant "raw_data"))
        (Data_encoding.req None None "raw_data"
          (Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
            (Data_encoding.string' None Data_encoding.Hex))))
      (fun (function_parameter : reveal_data) ⇒
        match function_parameter with
        | Raw_data m_valueSome (tt, m_value)
        | _None
        end)
      (fun (function_parameter : unit × string) ⇒
        let '(_, m_value) := function_parameter in
        Raw_data m_value)
  in let case_metadata : Data_encoding.case reveal_data :=
    Data_encoding.case_value "metadata" None (Data_encoding.Tag 1)
      (Data_encoding.obj2
        (Data_encoding.req None None "reveal_data_kind"
          (Data_encoding.constant "metadata"))
        (Data_encoding.req None None "metadata" Sc_rollup_metadata_repr.encoding))
      (fun (function_parameter : reveal_data) ⇒
        match function_parameter with
        | Metadata mdSome (tt, md)
        | _None
        end)
      (fun (function_parameter : unit × Sc_rollup_metadata_repr.t) ⇒
        let '(_, md) := function_parameter in
        Metadata md) in
  let case_dal_page :=
    Data_encoding.case_value "dal page" None (Data_encoding.Tag 2)
      (Data_encoding.obj2
        (Data_encoding.req None None "reveal_data_kind"
          (Data_encoding.constant "dal_page"))
        (Data_encoding.req None None "dal_page_content"
          (Data_encoding.option_value Data_encoding.bytes_value)))
      (fun (function_parameter : reveal_data) ⇒
        match function_parameter with
        | Dal_page p_valueSome (tt, p_value)
        | _None
        end)
      (fun (function_parameter : unit × option Bytes.t) ⇒
        let '(_, p_value) := function_parameter in
        Dal_page p_value) in
  Data_encoding.union None [ case_raw_data; case_metadata; case_dal_page ].

Definition input_encoding : Data_encoding.encoding input :=
  let case_inbox_message : Data_encoding.case input :=
    Data_encoding.case_value "inbox msg" None (Data_encoding.Tag 0)
      (Data_encoding.obj2
        (Data_encoding.req None None "input_kind"
          (Data_encoding.constant "inbox_message"))
        (Data_encoding.req None None "inbox_message" inbox_message_encoding))
      (fun (function_parameter : input) ⇒
        match function_parameter with
        | Inbox_message m_valueSome (tt, m_value)
        | _None
        end)
      (fun (function_parameter : unit × inbox_message) ⇒
        let '(_, m_value) := function_parameter in
        Inbox_message m_value)
  in let case_reveal_revelation : Data_encoding.case input :=
    Data_encoding.case_value "reveal" None (Data_encoding.Tag 1)
      (Data_encoding.obj2
        (Data_encoding.req None None "input_kind"
          (Data_encoding.constant "reveal_revelation"))
        (Data_encoding.req None None "reveal_data" reveal_data_encoding))
      (fun (function_parameter : input) ⇒
        match function_parameter with
        | Reveal d_valueSome (tt, d_value)
        | _None
        end)
      (fun (function_parameter : unit × reveal_data) ⇒
        let '(_, d_value) := function_parameter in
        Reveal d_value) in
  Data_encoding.union None [ case_inbox_message; case_reveal_revelation ].

[input_equal i1 i2] return whether [i1] and [i2] are equal.
Definition inbox_message_equal
  (a_value : inbox_message) (b_value : inbox_message) : bool :=
  let '{|
    inbox_message.inbox_level := inbox_level;
      inbox_message.message_counter := message_counter;
      inbox_message.payload := payload
      |} := a_value in
  (Raw_level_repr.equal inbox_level b_value.(inbox_message.inbox_level)) &&
  ((Z.equal message_counter b_value.(inbox_message.message_counter)) &&
  (String.equal payload b_value.(inbox_message.payload))).

Definition reveal_data_equal (a_value : reveal_data) (b_value : reveal_data)
  : bool :=
  match (a_value, b_value) with
  | (Raw_data a_value, Raw_data b_value)String.equal a_value b_value
  | (Raw_data _, _)false
  | (Metadata a_value, Metadata b_value)
    Sc_rollup_metadata_repr.equal a_value b_value
  | (Metadata _, _)false
  | (Dal_page a_value, Dal_page b_value)
    Option.equal Bytes.equal a_value b_value
  | (Dal_page _, _)false
  end.

Definition input_equal (a_value : input) (b_value : input) : bool :=
  match (a_value, b_value) with
  | (Inbox_message a_value, Inbox_message b_value)
    inbox_message_equal a_value b_value
  | (Inbox_message _, _)false
  | (Reveal a_value, Reveal b_value)reveal_data_equal a_value b_value
  | (Reveal _, _)false
  end.

Definition Input_hash :=
  Blake2B.Make
    {|
      Blake2B.Register.register_encoding _ := Base58.register_encoding
    |}
    (let name := "Sc_rollup_input_hash" in
    let title := "A smart contract rollup input hash" in
    let b58check_prefix := String.String "001" ("v}" ++ String.String "135" "")
      in
    let size_value := Some 20 in
    {|
      Blake2B.PrefixedName.name := name;
      Blake2B.PrefixedName.title := title;
      Blake2B.PrefixedName.size_value := size_value;
      Blake2B.PrefixedName.b58check_prefix := b58check_prefix
    |}).

Module Reveal_hash.
  Definition V0 :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "Sc_rollup_reveal_data_hash" in
      let title := "A smart contract rollup reveal hash" in
      let b58check_prefix :=
        String.String "017"
          (String.String "144"
            ("y" ++ String.String "209" (String.String "203" ""))) in
      let size_value := Some 31 in
      {|
        Blake2B.PrefixedName.name := name;
        Blake2B.PrefixedName.title := title;
        Blake2B.PrefixedName.size_value := size_value;
        Blake2B.PrefixedName.b58check_prefix := b58check_prefix
      |}).

Init function; without side-effects in Coq
  Definition init_module : unit :=
    Base58.check_encoded_prefix V0.(S.HASH.b58check_encoding) "scrrh1" 54.

Inclusion of the module [V0]
  Definition t := V0.(S.HASH.t).

  Definition name := V0.(S.HASH.name).

  Definition title := V0.(S.HASH.title).

  Definition pp := V0.(S.HASH.pp).

  Definition pp_short := V0.(S.HASH.pp_short).

  Definition op_eq := V0.(S.HASH.op_eq).

  Definition op_ltgt := V0.(S.HASH.op_ltgt).

  Definition op_lt := V0.(S.HASH.op_lt).

  Definition op_lteq := V0.(S.HASH.op_lteq).

  Definition op_gteq := V0.(S.HASH.op_gteq).

  Definition op_gt := V0.(S.HASH.op_gt).

  Definition compare := V0.(S.HASH.compare).

  Definition equal := V0.(S.HASH.equal).

  Definition max := V0.(S.HASH.max).

  Definition min := V0.(S.HASH.min).

  Definition hash_bytes := V0.(S.HASH.hash_bytes).

  Definition hash_string := V0.(S.HASH.hash_string).

  Definition zero := V0.(S.HASH.zero).

  Definition size_value := V0.(S.HASH.size_value).

  Definition to_bytes := V0.(S.HASH.to_bytes).

  Definition of_bytes_opt := V0.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn := V0.(S.HASH.of_bytes_exn).

  Definition to_b58check := V0.(S.HASH.to_b58check).

  Definition to_short_b58check := V0.(S.HASH.to_short_b58check).

  Definition of_b58check_exn := V0.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt := V0.(S.HASH.of_b58check_opt).

  Definition b58check_encoding := V0.(S.HASH.b58check_encoding).

  Definition rpc_arg := V0.(S.HASH.rpc_arg).

  Definition encoding : Data_encoding.encoding V0.(S.HASH.t) :=
    Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
      [
        Data_encoding.case_value "Reveal_data_hash_v0" None
          (Data_encoding.Tag 0) V0.(S.HASH.encoding)
          (fun (s_value : V0.(S.HASH.t)) ⇒ Some s_value)
          (fun (s_value : V0.(S.HASH.t)) ⇒ s_value)
      ].
End Reveal_hash.

Inductive reveal : Set :=
| Reveal_raw_data : Reveal_hash.t reveal
| Reveal_metadata : reveal
| Request_dal_page : Dal_slot_repr.Page.t reveal.

Definition reveal_encoding : Data_encoding.encoding reveal :=
  let case_raw_data : Data_encoding.case reveal :=
    Data_encoding.case_value "Reveal_raw_data" None (Data_encoding.Tag 0)
      (Data_encoding.obj2
        (Data_encoding.req None None "reveal_kind"
          (Data_encoding.constant "reveal_raw_data"))
        (Data_encoding.req None None "input_hash" Reveal_hash.encoding))
      (fun (function_parameter : reveal) ⇒
        match function_parameter with
        | Reveal_raw_data s_valueSome (tt, s_value)
        | _None
        end)
      (fun (function_parameter : unit × Reveal_hash.t) ⇒
        let '(_, s_value) := function_parameter in
        Reveal_raw_data s_value)
  in let case_metadata : Data_encoding.case reveal :=
    Data_encoding.case_value "Reveal_metadata" None (Data_encoding.Tag 1)
      (Data_encoding.obj1
        (Data_encoding.req None None "reveal_kind"
          (Data_encoding.constant "reveal_metadata")))
      (fun (function_parameter : reveal) ⇒
        match function_parameter with
        | Reveal_metadataSome tt
        | _None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Reveal_metadata) in
  let case_dal_page :=
    Data_encoding.case_value "Request_dal_page" None (Data_encoding.Tag 2)
      (Data_encoding.obj2
        (Data_encoding.req None None "reveal_kind"
          (Data_encoding.constant "request_dal_page"))
        (Data_encoding.req None None "page_id" Dal_slot_repr.Page.encoding))
      (fun (function_parameter : reveal) ⇒
        match function_parameter with
        | Request_dal_page s_valueSome (tt, s_value)
        | _None
        end)
      (fun (function_parameter : unit × Dal_slot_repr.Page.t) ⇒
        let '(_, s_value) := function_parameter in
        Request_dal_page s_value) in
  Data_encoding.union None [ case_raw_data; case_metadata; case_dal_page ].

The PVM's current input expectations: [No_input_required] if the machine is busy and has no need for new input. - [Initial] if the machine has never received an input so expects the very first item in the inbox. - [First_after (level, counter)] expects whatever comes next after that position in the inbox. - [Needs_metadata] if the machine needs the metadata to continue its execution.
[input_request_encoding] encoding value for {!input_request}.
Definition input_request_encoding : Data_encoding.encoding input_request :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "No_input_required" None (Data_encoding.Tag 0)
        (Data_encoding.obj1
          (Data_encoding.req None None "input_request_kind"
            (Data_encoding.constant "no_input_required")))
        (fun (function_parameter : input_request) ⇒
          match function_parameter with
          | No_input_requiredSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          No_input_required);
      Data_encoding.case_value "Initial" None (Data_encoding.Tag 1)
        (Data_encoding.obj1
          (Data_encoding.req None None "input_request_kind"
            (Data_encoding.constant "initial")))
        (fun (function_parameter : input_request) ⇒
          match function_parameter with
          | InitialSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Initial);
      Data_encoding.case_value "First_after" None (Data_encoding.Tag 2)
        (Data_encoding.obj3
          (Data_encoding.req None None "input_request_kind"
            (Data_encoding.constant "first_after"))
          (Data_encoding.req None None "level" Raw_level_repr.encoding)
          (Data_encoding.req None None "counter" Data_encoding.n_value))
        (fun (function_parameter : input_request) ⇒
          match function_parameter with
          | First_after level counterSome (tt, level, counter)
          | _None
          end)
        (fun (function_parameter : unit × Raw_level_repr.raw_level × Z.t) ⇒
          let '(_, level, counter) := function_parameter in
          First_after level counter);
      Data_encoding.case_value "Needs_reveal" None (Data_encoding.Tag 3)
        (Data_encoding.obj2
          (Data_encoding.req None None "input_request_kind"
            (Data_encoding.constant "needs_reveal"))
          (Data_encoding.req None None "reveal" reveal_encoding))
        (fun (function_parameter : input_request) ⇒
          match function_parameter with
          | Needs_reveal p_valueSome (tt, p_value)
          | _None
          end)
        (fun (function_parameter : unit × reveal) ⇒
          let '(_, p_value) := function_parameter in
          Needs_reveal p_value)
    ].

Definition pp_reveal (fmt : Format.formatter) (function_parameter : reveal)
  : unit :=
  match function_parameter with
  | Reveal_raw_data hash_valueReveal_hash.pp fmt hash_value
  | Reveal_metadataFormat.pp_print_string fmt "Reveal metadata"
  | Request_dal_page idDal_slot_repr.Page.pp fmt id
  end.

[pp_input_request fmt i] pretty prints the given input [i] to the formatter [fmt].
Definition pp_input_request (fmt : Format.formatter) (request : input_request)
  : unit :=
  match request with
  | No_input_required
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "No_input_required"
          CamlinternalFormatBasics.End_of_format) "No_input_required")
  | Initial
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Initial"
          CamlinternalFormatBasics.End_of_format) "Initial")
  | First_after l_value n_value
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "First_after (level = "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal ", counter = "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Char_literal ")" % char
                  CamlinternalFormatBasics.End_of_format)))))
        "First_after (level = %a, counter = %a)") Raw_level_repr.pp l_value
      Z.pp_print n_value
  | Needs_reveal reveal
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Needs reveal of "
          (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
        "Needs reveal of %a") pp_reveal reveal
  end.

Definition reveal_equal (p1 : reveal) (p2 : reveal) : bool :=
  match (p1, p2) with
  | (Reveal_raw_data h1, Reveal_raw_data h2)Reveal_hash.equal h1 h2
  | (Reveal_metadata, Reveal_metadata)true
  | (Request_dal_page a_value, Request_dal_page b_value)
    Dal_slot_repr.Page.equal a_value b_value
  | ((Reveal_raw_data _ | Reveal_metadata | Request_dal_page _), _)false
  end.

[input_request_equal i1 i2] return whether [i1] and [i2] are equal.
Definition input_request_equal
  (a_value : input_request) (b_value : input_request) : bool :=
  match (a_value, b_value) with
  | (No_input_required, No_input_required)true
  | (No_input_required, _)false
  | (Initial, Initial)true
  | (Initial, _)false
  | (First_after l_value n_value, First_after m_value o_value)
    (Raw_level_repr.equal l_value m_value) && (Z.equal n_value o_value)
  | (First_after _ _, _)false
  | (Needs_reveal p1, Needs_reveal p2)reveal_equal p1 p2
  | (Needs_reveal _, _)false
  end.

Type that describes output values.
Module output.
  Record record : Set := Build {
    outbox_level : Raw_level_repr.t;
    message_index : Z.t;
    message : Sc_rollup_outbox_message_repr.t;
  }.
  Definition with_outbox_level outbox_level (r : record) :=
    Build outbox_level r.(message_index) r.(message).
  Definition with_message_index message_index (r : record) :=
    Build r.(outbox_level) message_index r.(message).
  Definition with_message message (r : record) :=
    Build r.(outbox_level) r.(message_index) message.
End output.
Definition output := output.record.

[output_encoding] encoding value for {!output}.
Definition output_encoding : Data_encoding.encoding output :=
  Data_encoding.conv
    (fun (function_parameter : output) ⇒
      let '{|
        output.outbox_level := outbox_level;
          output.message_index := message_index;
          output.message := message
          |} := function_parameter in
      (outbox_level, message_index, message))
    (fun (function_parameter :
      Raw_level_repr.t × Z.t × Sc_rollup_outbox_message_repr.t) ⇒
      let '(outbox_level, message_index, message) := function_parameter in
      {| output.outbox_level := outbox_level;
        output.message_index := message_index; output.message := message; |})
    None
    (Data_encoding.obj3
      (Data_encoding.req None None "outbox_level" Raw_level_repr.encoding)
      (Data_encoding.req None None "message_index" Data_encoding.n_value)
      (Data_encoding.req None None "message"
        Sc_rollup_outbox_message_repr.encoding)).

[pp_output fmt o] pretty prints the given output [o] to the formatter [fmt].
Definition pp_output (fmt : Format.formatter) (function_parameter : output)
  : unit :=
  let '{|
    output.outbox_level := outbox_level;
      output.message_index := message_index;
      output.message := message
      |} := function_parameter in
  Format.fprintf fmt
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_gen
        (CamlinternalFormatBasics.Open_box
          (CamlinternalFormatBasics.Format
            CamlinternalFormatBasics.End_of_format ""))
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.Formatting_lit
            (CamlinternalFormatBasics.Break "@;" 1 0)
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@;" 1 0)
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Formatting_lit
                    (CamlinternalFormatBasics.Break "@;" 1 0)
                    (CamlinternalFormatBasics.Formatting_lit
                      CamlinternalFormatBasics.Close_box
                      CamlinternalFormatBasics.End_of_format))))))))
      "@[%a@;%a@;%a@;@]") Raw_level_repr.pp outbox_level Z.pp_print
    message_index Sc_rollup_outbox_message_repr.pp message.

Module S.
  Record signature {state context proof output_proof : Set} : Set := {
    
The state of the PVM denotes a state of the rollup.
The life cycle of the PVM is as follows. It starts its execution from an {!initial_state}. The initial state is specialized at origination with a [boot_sector], using the {!install_boot_sector} function. The resulting state is call the “genesis” of the rollup.
Afterwards, we classify states into two categories: "internal\n states" do not require any external information to be executed while "input states" are waiting for some information from the inbox to be executable.
    state := state;
    pp : state (Format.formatter unit unit);
    
A [context] represents the executable environment needed by the state to exist. Typically, the rollup node storage can be part of this context to allow the PVM state to be persistent.
    context := context;
    
A [hash] characterizes the contents of a state.
    hash := Sc_rollup_repr.State_hash.t;
    
During interactive refutation games, a player may need to provide a proof that a given execution step is valid. The PVM implementation is responsible for ensuring that this proof type has the correct semantics.
A proof [p] has four parameters: - [start_hash := proof_start_state p] [stop_hash := proof_stop_state p] [input_requested := proof_input_requested p] [input_given := proof_input_given p]
The following predicate must hold of a valid proof:
[exists start_state, stop_state. (state_hash start_state == start_hash) AND (Option.map state_hash stop_state == stop_hash) AND (is_input_state start_state == input_requested) AND (match (input_given, input_requested) with | (None, No_input_required) -> eval start_state == stop_state | (None, Initial) -> stop_state == None | (None, First_after (l, n)) -> stop_state == None | (Some input, No_input_required) -> true | (Some input, Initial) -> set_input input_given start_state == stop_state | (Some input, First_after (l, n)) -> set_input input_given start_state == stop_state)]
In natural language---the two hash parameters [start_hash] and [stop_hash] must have actual [state] values (or possibly [None] in the case of [stop_hash]) of which they are the hashes. The [input_requested] parameter must be the correct request from the [start_hash], given according to [is_input_state]. Finally there are four possibilities of [input_requested] and [input_given]. - if no input is required, or given, the proof is a simple [eval] step ; if input was required but not given, the [stop_hash] must be [None] (the machine is blocked) ; if no input was required but some was given, this makes no sense and it doesn't matter if the proof is valid or invalid (this case will be ruled out by the inbox proof anyway) ; finally, if input was required and given, the proof is a [set_input] step.
    proof := proof;
    
[proof]s are embedded in L1 refutation game operations using [proof_encoding]. Given that the size of L1 operations are limited, it is of *critical* importance to make sure that no execution step of the PVM can generate proofs that do not fit in L1 operations when encoded. If such a proof existed, the rollup could get stuck.
    proof_encoding : Data_encoding.t proof;
    
[proof_start_state proof] returns the initial state hash of the [proof] execution step.
    proof_start_state : proof hash;
    
[proof_stop_state proof] returns the final state hash of the [proof] execution step.
    proof_stop_state : proof hash;
    
[state_hash state] returns a compressed representation of [state].
    state_hash : state hash;
    
[initial_state ~empty] is the initial state of the PVM, before its specialization with a given [boot_sector]. The initial state is built on the [empty] state which must be provided.
    initial_state : state state;
    
[install_boot_sector state boot_sector] specializes the initial [state] of a PVM using a dedicated [boot_sector], submitted at the origination of the rollup.
    install_boot_sector : state string state;
    
[is_input_state state] returns the input expectations of the [state]---does it need input, and if so, how far through the inbox has it read so far?
    is_input_state : state input_request;
    
[set_input input state] sets [input] in [state] as the next input to be processed. This must answer the [input_request] from [is_input_state state].
    set_input : input state state;
    
[eval s0] returns a state [s1] resulting from the execution of an atomic step of the rollup at state [s0].
    eval : state state;
    
[verify_proof input p] checks the proof [p] with input [input] and returns the [input_request] before the evaluation of the proof. See the doc-string for the [proof] type.
[verify_proof input p] fails when the proof is invalid in regards to the given input.
    verify_proof : option input proof M? input_request;
    
[produce_proof ctxt input_given state] should return a [proof] for the PVM step starting from [state], if possible. This may fail for a few reasons: the [input_given] doesn't match the expectations of [state] ; the [context] for this instance of the PVM doesn't have access to enough of the [state] to build the proof.
    produce_proof : context option input state M? proof;
    
[verify_origination_proof proof boot_sector] verifies a proof supposedly generated by [produce_origination_proof].
    verify_origination_proof : proof string bool;
    
[produce_origination_proof context boot_sector] produces a proof [p] covering the specialization of a PVM, from the [initial_state] up to the genesis state wherein the [boot_sector] has been installed.
    produce_origination_proof : context string M? proof;
    
The following type is inhabited by the proofs that a given [output] is part of the outbox of a given [state].
    output_proof := output_proof;
    
[output_proof_encoding] encoding value for [output_proof]s.
[output_of_output_proof proof] returns the [output] that is referred to in [proof]'s statement.
    output_of_output_proof : output_proof output;
    
[state_of_output_proof proof] returns the [state] hash that is referred to in [proof]'s statement.
    state_of_output_proof : output_proof hash;
    
[verify_output_proof output_proof] returns [true] iff [proof] is a valid witness that its [output] is part of its [state]'s outbox.
    verify_output_proof : output_proof bool;
    
[produce_output_proof ctxt state output] returns a proof that witnesses the fact that [output] is part of [state]'s outbox.
    produce_output_proof :
      context state output
      Pervasives.result output_proof Error_monad._error;
  }.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _}.