Skip to main content

🦏 Sc_rollup_proof_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "Sc_rollup_proof_check" "Invalid proof"
      "An invalid proof has been submitted"
      (Some
        (fun (fmt : Format.formatter) ⇒
          fun (msg : string) ⇒
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Invalid proof: "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.End_of_format)) "Invalid proof: %s")
              msg))
      (Data_encoding.obj1
        (Data_encoding.req None None "reason" Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Sc_rollup_proof_check" then
            let msg := cast string payload in
            Some msg
          else None
        end)
      (fun (msg : string) ⇒ Build_extensible "Sc_rollup_proof_check" string msg)
    in
  Error_monad.register_error_kind Error_monad.Permanent
    "Sc_rollup_invalid_serialized_inbox_proof" "Invalid serialized inbox proof"
    "The serialized inbox proof can not be de-serialized"
    (Some
      (fun (fmt : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Invalid serialized inbox proof"
                CamlinternalFormatBasics.End_of_format)
              "Invalid serialized inbox proof"))) Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Sc_rollup_invalid_serialized_inbox_proof" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Sc_rollup_invalid_serialized_inbox_proof" unit tt).

Inductive reveal_proof : Set :=
| Raw_data_proof : string reveal_proof.

Definition reveal_proof_encoding : Data_encoding.encoding reveal_proof :=
  let case_raw_data :=
    Data_encoding.case_value "raw data proof" None (Data_encoding.Tag 0)
      (Data_encoding.obj2
        (Data_encoding.req None None "reveal_proof_kind"
          (Data_encoding.constant "raw_data_proof"))
        (Data_encoding.req None None "raw_data"
          (Data_encoding.check_size Constants_repr.sc_rollup_message_size_limit
            Data_encoding.bytes_value)))
      (fun (function_parameter : reveal_proof) ⇒
        let 'Raw_data_proof s_value := function_parameter in
        Some (tt, (Bytes.of_string s_value)))
      (fun (function_parameter : unit × Bytes.t) ⇒
        let '(_, s_value) := function_parameter in
        Raw_data_proof (Bytes.to_string s_value)) in
  Data_encoding.union None [ case_raw_data ].

Records for the constructor parameters
Module ConstructorRecords_input_proof.
  Module input_proof.
    Module Inbox_proof.
      Record record {level message_counter proof : Set} : Set := Build {
        level : level;
        message_counter : message_counter;
        proof : proof;
      }.
      Arguments record : clear implicits.
      Definition with_level {t_level t_message_counter t_proof} level
        (r : record t_level t_message_counter t_proof) :=
        Build t_level t_message_counter t_proof level r.(message_counter)
          r.(proof).
      Definition with_message_counter {t_level t_message_counter t_proof}
        message_counter (r : record t_level t_message_counter t_proof) :=
        Build t_level t_message_counter t_proof r.(level) message_counter
          r.(proof).
      Definition with_proof {t_level t_message_counter t_proof} proof
        (r : record t_level t_message_counter t_proof) :=
        Build t_level t_message_counter t_proof r.(level) r.(message_counter)
          proof.
    End Inbox_proof.
    Definition Inbox_proof_skeleton := Inbox_proof.record.
  End input_proof.
End ConstructorRecords_input_proof.
Import ConstructorRecords_input_proof.

Reserved Notation "'input_proof.Inbox_proof".

Inductive input_proof : Set :=
| Inbox_proof : 'input_proof.Inbox_proof input_proof
| Reveal_proof : reveal_proof input_proof

where "'input_proof.Inbox_proof" :=
  (input_proof.Inbox_proof_skeleton Raw_level_repr.t Z.t
    Sc_rollup_inbox_repr.serialized_proof).

Module input_proof.
  Include ConstructorRecords_input_proof.input_proof.
  Definition Inbox_proof := 'input_proof.Inbox_proof.
End input_proof.

Definition input_proof_encoding : Data_encoding.encoding input_proof :=
  let case_inbox_proof :=
    Data_encoding.case_value "inbox proof" None (Data_encoding.Tag 0)
      (Data_encoding.obj4
        (Data_encoding.req None None "input_proof_kind"
          (Data_encoding.constant "inbox_proof"))
        (Data_encoding.req None None "level" Raw_level_repr.encoding)
        (Data_encoding.req None None "message_counter" Data_encoding.n_value)
        (Data_encoding.req None None "serialized_proof"
          Sc_rollup_inbox_repr.serialized_proof_encoding))
      (fun (function_parameter : input_proof) ⇒
        match function_parameter with
        |
          Inbox_proof {|
            input_proof.Inbox_proof.level := level;
              input_proof.Inbox_proof.message_counter := message_counter;
              input_proof.Inbox_proof.proof := proof_value
              |} ⇒ Some (tt, level, message_counter, proof_value)
        | _None
        end)
      (fun (function_parameter :
        unit × Raw_level_repr.raw_level × Z.t ×
          Sc_rollup_inbox_repr.serialized_proof) ⇒
        let '(_, level, message_counter, proof_value) := function_parameter in
        Inbox_proof
          {| input_proof.Inbox_proof.level := level;
            input_proof.Inbox_proof.message_counter := message_counter;
            input_proof.Inbox_proof.proof := proof_value; |}) in
  let case_reveal_proof :=
    Data_encoding.case_value "reveal proof" None (Data_encoding.Tag 1)
      (Data_encoding.obj2
        (Data_encoding.req None None "input_proof_kind"
          (Data_encoding.constant "reveal_proof"))
        (Data_encoding.req None None "reveal_proof" reveal_proof_encoding))
      (fun (function_parameter : input_proof) ⇒
        match function_parameter with
        | Reveal_proof s_valueSome (tt, s_value)
        | _None
        end)
      (fun (function_parameter : unit × reveal_proof) ⇒
        let '(_, s_value) := function_parameter in
        Reveal_proof s_value) in
  Data_encoding.union None [ case_inbox_proof; case_reveal_proof ].

Module t.
  Record record : Set := Build {
    pvm_step : Sc_rollups.wrapped_proof;
    input_proof : option input_proof;
  }.
  Definition with_pvm_step pvm_step (r : record) :=
    Build pvm_step r.(input_proof).
  Definition with_input_proof input_proof (r : record) :=
    Build r.(pvm_step) input_proof.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{| t.pvm_step := pvm_step; t.input_proof := input_proof |} :=
        function_parameter in
      (pvm_step, input_proof))
    (fun (function_parameter : Sc_rollups.wrapped_proof × option input_proof) ⇒
      let '(pvm_step, input_proof) := function_parameter in
      {| t.pvm_step := pvm_step; t.input_proof := input_proof; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "pvm_step" Sc_rollups.wrapped_proof_encoding)
      (Data_encoding.opt None None "input_proof" input_proof_encoding)).

Definition pp {A : Set} (ppf : Format.formatter) (function_parameter : A)
  : unit :=
  let '_ := function_parameter in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal "Refutation game proof"
        CamlinternalFormatBasics.End_of_format) "Refutation game proof").

Definition start (proof_value : t) : Sc_rollup_repr.State_hash.t :=
  let P := Sc_rollups.wrapped_proof_module proof_value.(t.pvm_step) in
  let 'existS _ _ P := P in
  P.(Sc_rollups.PVM_with_proof.proof_start_state)
    P.(Sc_rollups.PVM_with_proof.proof_val).

Definition stop (proof_value : t) : Sc_rollup_repr.State_hash.t :=
  let P := Sc_rollups.wrapped_proof_module proof_value.(t.pvm_step) in
  let 'existS _ _ P := P in
  P.(Sc_rollups.PVM_with_proof.proof_stop_state)
    P.(Sc_rollups.PVM_with_proof.proof_val).

Definition cut_at_level
  (level : Raw_level_repr.raw_level) (input : Sc_rollup_PVM_sig.input)
  : option Sc_rollup_PVM_sig.input :=
  match input with
  |
    Sc_rollup_PVM_sig.Inbox_message {|
      Sc_rollup_PVM_sig.inbox_message.inbox_level := input_level |} ⇒
    if Raw_level_repr.op_lteq level input_level then
      None
    else
      Some input
  | Sc_rollup_PVM_sig.Reveal _dataSome input
  end.

Definition proof_error {A : Set} (reason_value : string) : M? A :=
  Error_monad.Lwt_tzresult_syntax.fail
    (Build_extensible "Sc_rollup_proof_check" string reason_value).

Definition check (p_value : bool) (reason_value : string) : M? unit :=
  if p_value then
    return? tt
  else
    proof_error reason_value.

Definition check_inbox_proof
  (snapshot_value : Sc_rollup_inbox_repr.history_proof)
  (serialized_inbox_proof : Sc_rollup_inbox_repr.serialized_proof)
  (function_parameter : Raw_level_repr.t × Z.t)
  : M? (option Sc_rollup_PVM_sig.inbox_message) :=
  let '(level, counter) := function_parameter in
  match Sc_rollup_inbox_repr.of_serialized_proof serialized_inbox_proof with
  | None
    Error_monad.fail
      (Build_extensible "Sc_rollup_invalid_serialized_inbox_proof" unit tt)
  | Some inbox_proof
    Sc_rollup_inbox_repr.verify_proof (level, counter) snapshot_value
      inbox_proof
  end.

Definition valid
  (snapshot_value : Sc_rollup_inbox_repr.history_proof)
  (commit_level : Raw_level_repr.raw_level) (pvm_name : String.t)
  (proof_value : t)
  : M? (option Sc_rollup_PVM_sig.input × Sc_rollup_PVM_sig.input_request) :=
  let P := Sc_rollups.wrapped_proof_module proof_value.(t.pvm_step) in
  let 'existS _ _ P := P in
  let? '_ :=
    check (String.equal P.(Sc_rollups.PVM_with_proof.name) pvm_name)
      "Incorrect PVM kind" in
  let? input :=
    match proof_value.(t.input_proof) with
    | NoneError_monad.Lwt_tzresult_syntax.return_none
    |
      Some
        (Inbox_proof {|
          input_proof.Inbox_proof.level := level;
            input_proof.Inbox_proof.message_counter := message_counter;
            input_proof.Inbox_proof.proof := proof_value
            |}) ⇒
      Error_monad.Lwt_tzresult_syntax.op_letplus
        (check_inbox_proof snapshot_value proof_value
          (level, (Z.succ message_counter)))
        (fun inbox_message
          Option.map
            (fun (i_value : Sc_rollup_PVM_sig.inbox_message) ⇒
              Sc_rollup_PVM_sig.Inbox_message i_value) inbox_message)
    | Some (Reveal_proof (Raw_data_proof data)) ⇒
      Error_monad.Lwt_tzresult_syntax.return_some
        (Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Raw_data data))
    end in
  let input := Option.bind input (cut_at_level commit_level) in
  let? input_requested :=
    P.(Sc_rollups.PVM_with_proof.verify_proof) input
      P.(Sc_rollups.PVM_with_proof.proof_val) in
  let? '_ :=
    match (proof_value.(t.input_proof), input_requested) with
    | (None, Sc_rollup_PVM_sig.No_input_required)
      Error_monad.Lwt_tzresult_syntax.return_unit
    |
      (Some
        (Inbox_proof {|
          input_proof.Inbox_proof.level := level;
            input_proof.Inbox_proof.message_counter := message_counter;
            input_proof.Inbox_proof.proof := _
            |}), Sc_rollup_PVM_sig.Initial)
      check
        ((Raw_level_repr.op_eq level Raw_level_repr.root_value) &&
        (Z.equal message_counter Z.zero))
        "Inbox proof is not about the initial input request."
    |
      (Some
        (Inbox_proof {|
          input_proof.Inbox_proof.level := level;
            input_proof.Inbox_proof.message_counter := message_counter;
            input_proof.Inbox_proof.proof := _
            |}), Sc_rollup_PVM_sig.First_after l_value n_value)
      check
        ((Raw_level_repr.op_eq level l_value) &&
        (Z.equal message_counter n_value))
        "Level and index of inbox proof are not equal to the one expected in input request."
    |
      (Some (Reveal_proof (Raw_data_proof data)),
        Sc_rollup_PVM_sig.Needs_reveal
          (Sc_rollup_PVM_sig.Reveal_raw_data expected_hash))
      let data_hash :=
        Sc_rollup_PVM_sig.Input_hash.(S.HASH.hash_string) None [ data ] in
      check
        (Sc_rollup_PVM_sig.Input_hash.(S.HASH.equal) data_hash expected_hash)
        "Invalid reveal"
    |
      ((None,
        (Sc_rollup_PVM_sig.Initial | Sc_rollup_PVM_sig.First_after _ _ |
        Sc_rollup_PVM_sig.Needs_reveal _)) |
      (Some _, Sc_rollup_PVM_sig.No_input_required) |
      (Some (Inbox_proof _), Sc_rollup_PVM_sig.Needs_reveal _) |
      (Some (Reveal_proof _),
        (Sc_rollup_PVM_sig.Initial | Sc_rollup_PVM_sig.First_after _ _))) ⇒
      proof_error "Inbox proof and input request are dissociated."
    end in
  return? (input, input_requested).

Module PVM_with_context_and_state.
  Record signature
    {state context proof output_proof Inbox_with_history_tree
      Inbox_with_history_inclusion_proof Inbox_with_history_proof : Set} : Set
    := {
    name : string;
    parse_boot_sector : string option Sc_rollups.PVM.boot_sector;
    pp_boot_sector : Format.formatter Sc_rollups.PVM.boot_sector unit;
    state := state;
    pp : state (Format.formatter unit unit);
    context := context;
    hash := Sc_rollup_repr.State_hash.t;
    proof := proof;
    proof_encoding : Data_encoding.t proof;
    proof_start_state : proof hash;
    proof_stop_state : proof hash;
    state_hash : state hash;
    initial_state : context state;
    install_boot_sector : state string state;
    is_input_state : state Sc_rollup_PVM_sig.input_request;
    set_input : Sc_rollup_PVM_sig.input state state;
    eval : state state;
    verify_proof :
      option Sc_rollup_PVM_sig.input proof
      M? Sc_rollup_PVM_sig.input_request;
    produce_proof :
      context option Sc_rollup_PVM_sig.input state M? proof;
    verify_origination_proof : proof string bool;
    produce_origination_proof : context string M? proof;
    output_proof := output_proof;
    output_proof_encoding : Data_encoding.t output_proof;
    output_of_output_proof : output_proof Sc_rollup_PVM_sig.output;
    state_of_output_proof : output_proof hash;
    verify_output_proof : output_proof bool;
    produce_output_proof :
      context state Sc_rollup_PVM_sig.output
      Pervasives.result output_proof Error_monad._error;
    Internal_for_tests_insert_failure : state state;
    context_value : context;
    state_value : state;
    reveal : Sc_rollup_PVM_sig.Input_hash.(S.HASH.t) option string;
    Inbox_with_history_tree := Inbox_with_history_tree;
    Inbox_with_history_inbox_context := context;
    Inbox_with_history_hash_level_tree :
      Inbox_with_history_tree Sc_rollup_inbox_repr.Hash.t;
    Inbox_with_history_new_level_tree :
      Inbox_with_history_inbox_context Raw_level_repr.t
      Inbox_with_history_tree;
    Inbox_with_history_add_messages :
      Inbox_with_history_inbox_context
      Sc_rollup_inbox_repr.History.(Bounded_history_repr.S.t)
      Sc_rollup_inbox_repr.t Raw_level_repr.t
      list Sc_rollup_inbox_message_repr.serialized
      option Inbox_with_history_tree
      M?
        (Inbox_with_history_tree ×
          Sc_rollup_inbox_repr.History.(Bounded_history_repr.S.t) ×
          Sc_rollup_inbox_repr.t);
    Inbox_with_history_add_messages_no_history :
      Inbox_with_history_inbox_context Sc_rollup_inbox_repr.t
      Raw_level_repr.t list Sc_rollup_inbox_message_repr.serialized
      option Inbox_with_history_tree
      M? (Inbox_with_history_tree × Sc_rollup_inbox_repr.t);
    Inbox_with_history_get_message_payload :
      Inbox_with_history_tree Z.t
      option Sc_rollup_inbox_message_repr.serialized;
    Inbox_with_history_form_history_proof :
      Inbox_with_history_inbox_context
      Sc_rollup_inbox_repr.History.(Bounded_history_repr.S.t)
      Sc_rollup_inbox_repr.t option Inbox_with_history_tree
      M?
        (Sc_rollup_inbox_repr.History.(Bounded_history_repr.S.t) ×
          Sc_rollup_inbox_repr.history_proof);
    Inbox_with_history_take_snapshot :
      Sc_rollup_inbox_repr.t Sc_rollup_inbox_repr.history_proof;
    Inbox_with_history_inclusion_proof := Inbox_with_history_inclusion_proof;
    Inbox_with_history_inclusion_proof_encoding :
      Data_encoding.t Inbox_with_history_inclusion_proof;
    Inbox_with_history_pp_inclusion_proof :
      Format.formatter Inbox_with_history_inclusion_proof unit;
    Inbox_with_history_number_of_proof_steps :
      Inbox_with_history_inclusion_proof int;
    Inbox_with_history_verify_inclusion_proof :
      Inbox_with_history_inclusion_proof
      Sc_rollup_inbox_repr.history_proof
      Sc_rollup_inbox_repr.history_proof bool;
    Inbox_with_history_proof := Inbox_with_history_proof;
    Inbox_with_history_pp_proof :
      Format.formatter Inbox_with_history_proof unit;
    Inbox_with_history_to_serialized_proof :
      Inbox_with_history_proof Sc_rollup_inbox_repr.serialized_proof;
    Inbox_with_history_of_serialized_proof :
      Sc_rollup_inbox_repr.serialized_proof option Inbox_with_history_proof;
    Inbox_with_history_verify_proof :
      Raw_level_repr.t × Z.t Sc_rollup_inbox_repr.history_proof
      Inbox_with_history_proof M? (option Sc_rollup_PVM_sig.inbox_message);
    Inbox_with_history_produce_proof :
      Inbox_with_history_inbox_context
      Sc_rollup_inbox_repr.History.(Bounded_history_repr.S.t)
      Sc_rollup_inbox_repr.history_proof Raw_level_repr.t × Z.t
      M? (Inbox_with_history_proof × option Sc_rollup_PVM_sig.inbox_message);
    Inbox_with_history_empty :
      Inbox_with_history_inbox_context Sc_rollup_repr.t
      Raw_level_repr.t Sc_rollup_inbox_repr.t;
    Inbox_with_history_Internal_for_tests_eq_tree :
      Inbox_with_history_tree Inbox_with_history_tree bool;
    Inbox_with_history_Internal_for_tests_produce_inclusion_proof :
      Sc_rollup_inbox_repr.History.(Bounded_history_repr.S.t)
      Sc_rollup_inbox_repr.history_proof
      Sc_rollup_inbox_repr.history_proof
      M? (option Inbox_with_history_inclusion_proof);
    Inbox_with_history_Internal_for_tests_serialized_proof_of_string :
      string Sc_rollup_inbox_repr.serialized_proof;
    Inbox_with_history_inbox : Sc_rollup_inbox_repr.history_proof;
    Inbox_with_history_history :
      Sc_rollup_inbox_repr.History.(Bounded_history_repr.S.t);
  }.
End PVM_with_context_and_state.
Definition PVM_with_context_and_state := @PVM_with_context_and_state.signature.
Arguments PVM_with_context_and_state {_ _ _ _ _ _ _}.

Definition produce
  (pvm_and_state :
    {'[state, context, proof, output_proof, Inbox_with_history_tree,
      Inbox_with_history_inclusion_proof, Inbox_with_history_proof] :
      [Set ** Set ** Set ** Set ** Set ** Set ** Set] @
      PVM_with_context_and_state (state := state) (context := context)
        (proof := proof) (output_proof := output_proof)
        (Inbox_with_history_tree := Inbox_with_history_tree)
        (Inbox_with_history_inclusion_proof :=
          Inbox_with_history_inclusion_proof)
        (Inbox_with_history_proof := Inbox_with_history_proof)})
  (commit_level : Raw_level_repr.raw_level) : M? t :=
  let 'P := pvm_and_state in
  let 'existS _ _ P := P in
  let 'request :=
    P.(PVM_with_context_and_state.is_input_state)
      P.(PVM_with_context_and_state.state_value) in
  let? '(input_proof, input_given) :=
    match request with
    | Sc_rollup_PVM_sig.No_input_requiredreturn? (None, None)
    | Sc_rollup_PVM_sig.Initial
      let level := Raw_level_repr.root_value in
      let message_counter := Z.zero in
      let? '(inbox_proof, input) :=
        P.(PVM_with_context_and_state.Inbox_with_history_produce_proof)
          P.(PVM_with_context_and_state.context_value)
          P.(PVM_with_context_and_state.Inbox_with_history_history)
          P.(PVM_with_context_and_state.Inbox_with_history_inbox)
          (level, message_counter) in
      let input :=
        Option.map
          (fun (msg : Sc_rollup_PVM_sig.inbox_message) ⇒
            Sc_rollup_PVM_sig.Inbox_message msg) input in
      let inbox_proof :=
        Inbox_proof
          {| input_proof.Inbox_proof.level := level;
            input_proof.Inbox_proof.message_counter := message_counter;
            input_proof.Inbox_proof.proof :=
              P.(PVM_with_context_and_state.Inbox_with_history_to_serialized_proof)
                inbox_proof; |} in
      return? ((Some inbox_proof), input)
    | Sc_rollup_PVM_sig.First_after level message_counter
      let? '(inbox_proof, input) :=
        P.(PVM_with_context_and_state.Inbox_with_history_produce_proof)
          P.(PVM_with_context_and_state.context_value)
          P.(PVM_with_context_and_state.Inbox_with_history_history)
          P.(PVM_with_context_and_state.Inbox_with_history_inbox)
          (level, (Z.succ message_counter)) in
      let input :=
        Option.map
          (fun (msg : Sc_rollup_PVM_sig.inbox_message) ⇒
            Sc_rollup_PVM_sig.Inbox_message msg) input in
      let inbox_proof :=
        Inbox_proof
          {| input_proof.Inbox_proof.level := level;
            input_proof.Inbox_proof.message_counter := message_counter;
            input_proof.Inbox_proof.proof :=
              P.(PVM_with_context_and_state.Inbox_with_history_to_serialized_proof)
                inbox_proof; |} in
      return? ((Some inbox_proof), input)
    | Sc_rollup_PVM_sig.Needs_reveal (Sc_rollup_PVM_sig.Reveal_raw_data h_value)
      ⇒
      match P.(PVM_with_context_and_state.reveal) h_value with
      | Noneproof_error "No reveal"
      | Some data
        return?
          ((Some (Reveal_proof (Raw_data_proof data))),
            (Some (Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Raw_data data))))
      end
    end in
  let input_given := Option.bind input_given (cut_at_level commit_level) in
  let? pvm_step_proof :=
    P.(PVM_with_context_and_state.produce_proof)
      P.(PVM_with_context_and_state.context_value) input_given
      P.(PVM_with_context_and_state.state_value) in
  let P_with_proof :=
    let name := P.(PVM_with_context_and_state.name) in
    let parse_boot_sector := P.(PVM_with_context_and_state.parse_boot_sector) in
    let pp_boot_sector := P.(PVM_with_context_and_state.pp_boot_sector) in
    let state := P.(PVM_with_context_and_state.state) in
    let pp := P.(PVM_with_context_and_state.pp) in
    let context := P.(PVM_with_context_and_state.context) in
    let hash := P.(PVM_with_context_and_state.hash) in
    let proof := P.(PVM_with_context_and_state.proof) in
    let proof_encoding := P.(PVM_with_context_and_state.proof_encoding) in
    let proof_start_state := P.(PVM_with_context_and_state.proof_start_state) in
    let proof_stop_state := P.(PVM_with_context_and_state.proof_stop_state) in
    let state_hash := P.(PVM_with_context_and_state.state_hash) in
    let initial_state := P.(PVM_with_context_and_state.initial_state) in
    let install_boot_sector :=
      P.(PVM_with_context_and_state.install_boot_sector) in
    let is_input_state := P.(PVM_with_context_and_state.is_input_state) in
    let set_input := P.(PVM_with_context_and_state.set_input) in
    let eval := P.(PVM_with_context_and_state.eval) in
    let verify_proof := P.(PVM_with_context_and_state.verify_proof) in
    let produce_proof := P.(PVM_with_context_and_state.produce_proof) in
    let verify_origination_proof :=
      P.(PVM_with_context_and_state.verify_origination_proof) in
    let produce_origination_proof :=
      P.(PVM_with_context_and_state.produce_origination_proof) in
    let output_proof := P.(PVM_with_context_and_state.output_proof) in
    let output_proof_encoding :=
      P.(PVM_with_context_and_state.output_proof_encoding) in
    let output_of_output_proof :=
      P.(PVM_with_context_and_state.output_of_output_proof) in
    let state_of_output_proof :=
      P.(PVM_with_context_and_state.state_of_output_proof) in
    let verify_output_proof :=
      P.(PVM_with_context_and_state.verify_output_proof) in
    let produce_output_proof :=
      P.(PVM_with_context_and_state.produce_output_proof) in
    let context_value := P.(PVM_with_context_and_state.context_value) in
    let state_value := P.(PVM_with_context_and_state.state_value) in
    let reveal := P.(PVM_with_context_and_state.reveal) in
    let proof_val := pvm_step_proof in
    {|
      Sc_rollups.PVM_with_proof.name := name;
      Sc_rollups.PVM_with_proof.parse_boot_sector := parse_boot_sector;
      Sc_rollups.PVM_with_proof.pp_boot_sector := pp_boot_sector;
      Sc_rollups.PVM_with_proof.pp := pp;
      Sc_rollups.PVM_with_proof.proof_encoding := proof_encoding;
      Sc_rollups.PVM_with_proof.proof_start_state := proof_start_state;
      Sc_rollups.PVM_with_proof.proof_stop_state := proof_stop_state;
      Sc_rollups.PVM_with_proof.state_hash := state_hash;
      Sc_rollups.PVM_with_proof.initial_state := initial_state;
      Sc_rollups.PVM_with_proof.install_boot_sector := install_boot_sector;
      Sc_rollups.PVM_with_proof.is_input_state := is_input_state;
      Sc_rollups.PVM_with_proof.set_input := set_input;
      Sc_rollups.PVM_with_proof.eval := eval;
      Sc_rollups.PVM_with_proof.verify_proof := verify_proof;
      Sc_rollups.PVM_with_proof.produce_proof := produce_proof;
      Sc_rollups.PVM_with_proof.verify_origination_proof :=
        verify_origination_proof;
      Sc_rollups.PVM_with_proof.produce_origination_proof :=
        produce_origination_proof;
      Sc_rollups.PVM_with_proof.output_proof_encoding := output_proof_encoding;
      Sc_rollups.PVM_with_proof.output_of_output_proof := output_of_output_proof;
      Sc_rollups.PVM_with_proof.state_of_output_proof := state_of_output_proof;
      Sc_rollups.PVM_with_proof.verify_output_proof := verify_output_proof;
      Sc_rollups.PVM_with_proof.produce_output_proof := produce_output_proof;
      Sc_rollups.PVM_with_proof.proof_val := proof_val
    |} in
  match
    Sc_rollups.wrap_proof
      (existS (A := [Set ** Set ** Set ** Set]) _ [_, _, _, _] P_with_proof)
    with
  | Some pvm_step
    return? {| t.pvm_step := pvm_step; t.input_proof := input_proof; |}
  | Noneproof_error "Could not wrap proof"
  end.