Skip to main content

🦏 Sc_rollups.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.V7.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_arith.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_wasm.

Module PVM.
  Definition boot_sector : Set := string.

  Module S.
    Record signature {state context proof output_proof : Set} : Set := {
      name : string;
      parse_boot_sector : string option boot_sector;
      pp_boot_sector : Format.formatter 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; *)
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_ _ _ _}.

  Definition t : Set :=
    {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
      S (state := state) (context := context) (proof := proof)
        (output_proof := output_proof)}.
End PVM.

Module Kind.
  Inductive t : Set :=
  | Example_arith : t
  | Wasm_2_0_0 : t.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.string_enum
      [ ("arith_pvm_kind", Example_arith); ("wasm_2_0_0_pvm_kind", Wasm_2_0_0) ].

  Definition equal (x_value : t) (y_value : t) : bool :=
    match (x_value, y_value) with
    | (Example_arith, Example_arith)true
    | (Wasm_2_0_0, Wasm_2_0_0)true
    | _false
    end.

  Definition all : list t := [ Example_arith; Wasm_2_0_0 ].

  Definition of_name (function_parameter : string) : option t :=
    match function_parameter with
    | "arith" ⇒ Some Example_arith
    | "wasm_2_0_0" ⇒ Some Wasm_2_0_0
    | _None
    end.

  Definition example_arith_pvm
    : {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
      PVM.S (state := state) (context := context) (proof := proof)
        (output_proof := output_proof)} :=
    existS (A := [Set ** Set ** Set ** Set]) _ [_, _, _, _]
      {|
        PVM.S.name :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.name);
        PVM.S.parse_boot_sector :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.parse_boot_sector);
        PVM.S.pp_boot_sector :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp_boot_sector);
        PVM.S.pp :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp);
        PVM.S.proof_encoding :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_encoding);
        PVM.S.proof_start_state :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_start_state);
        PVM.S.proof_stop_state :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_stop_state);
        PVM.S.state_hash :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state_hash);
        PVM.S.initial_state :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.initial_state);
        PVM.S.install_boot_sector :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.install_boot_sector);
        PVM.S.is_input_state :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.is_input_state);
        PVM.S.set_input :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.set_input);
        PVM.S.eval :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.eval);
        PVM.S.verify_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_proof);
        PVM.S.produce_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_proof);
        PVM.S.verify_origination_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_origination_proof);
        PVM.S.produce_origination_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_origination_proof);
        PVM.S.output_proof_encoding :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_proof_encoding);
        PVM.S.output_of_output_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_of_output_proof);
        PVM.S.state_of_output_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state_of_output_proof);
        PVM.S.verify_output_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_output_proof);
        PVM.S.produce_output_proof :=
          Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_output_proof)
      |}.

  Definition wasm_2_0_0_pvm
    : {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
      PVM.S (state := state) (context := context) (proof := proof)
        (output_proof := output_proof)} :=
    existS (A := [Set ** Set ** Set ** Set]) _ [_, _, _, _]
      {|
        PVM.S.name :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.name);
        PVM.S.parse_boot_sector :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.parse_boot_sector);
        PVM.S.pp_boot_sector :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.pp_boot_sector);
        PVM.S.pp :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.pp);
        PVM.S.proof_encoding :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_encoding);
        PVM.S.proof_start_state :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_start_state);
        PVM.S.proof_stop_state :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_stop_state);
        PVM.S.state_hash :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state_hash);
        PVM.S.initial_state :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.initial_state);
        PVM.S.install_boot_sector :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.install_boot_sector);
        PVM.S.is_input_state :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.is_input_state);
        PVM.S.set_input :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.set_input);
        PVM.S.eval :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.eval);
        PVM.S.verify_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_proof);
        PVM.S.produce_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_proof);
        PVM.S.verify_origination_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_origination_proof);
        PVM.S.produce_origination_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_origination_proof);
        PVM.S.output_proof_encoding :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_proof_encoding);
        PVM.S.output_of_output_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_of_output_proof);
        PVM.S.state_of_output_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state_of_output_proof);
        PVM.S.verify_output_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_output_proof);
        PVM.S.produce_output_proof :=
          Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_output_proof)
      |}.

  Definition pvm_of (function_parameter : t)
    : {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
      PVM.S (state := state) (context := context) (proof := proof)
        (output_proof := output_proof)} :=
    match function_parameter with
    | Example_arithexample_arith_pvm
    | Wasm_2_0_0wasm_2_0_0_pvm
    end.

  Definition of_pvm
    (M :
      {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
        PVM.S (state := state) (context := context) (proof := proof)
          (output_proof := output_proof)}) : t :=
    let 'existS _ _ M := M in
    match of_name M.(PVM.S.name) with
    | Some k_valuek_value
    | None
      Pervasives.failwith
        (Format.sprintf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "The module named "
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                (CamlinternalFormatBasics.String_literal
                  " is not in Sc_rollups.all."
                  CamlinternalFormatBasics.End_of_format)))
            "The module named %s is not in Sc_rollups.all.") M.(PVM.S.name))
    end.

  Definition pvm_of_name (name : string)
    : option
      {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
        PVM.S (state := state) (context := context) (proof := proof)
          (output_proof := output_proof)} := Option.map pvm_of (of_name name).

  Definition all_names : list string :=
    List.map
      (fun (k_value : t) ⇒
        let 'M := pvm_of k_value in
        let 'existS _ _ M := M in
        M.(PVM.S.name)) all.

  Definition name_of (k_value : t) : string :=
    let M := pvm_of k_value in
    let 'existS _ _ M := M in
    M.(PVM.S.name).

  Definition pp (fmt : Format.formatter) (k_value : t) : unit :=
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
          CamlinternalFormatBasics.End_of_format) "%s") (name_of k_value).
End Kind.

Module PVM_with_proof.
  Record signature {state context proof output_proof : Set} : Set := {
    name : string;
    parse_boot_sector : string option PVM.boot_sector;
    pp_boot_sector : Format.formatter 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; *)
    proof_val : proof;
  }.
End PVM_with_proof.
Definition PVM_with_proof := @PVM_with_proof.signature.
Arguments PVM_with_proof {_ _ _ _}.

Inductive wrapped_proof : Set :=
| Unencodable :
  {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
    PVM_with_proof (state := state) (context := context) (proof := proof)
      (output_proof := output_proof)} wrapped_proof
| Arith_pvm_with_proof :
  {'[state, context, output_proof] : [Set ** Set ** Set] @
    PVM_with_proof (state := state) (context := context)
      (proof :=
        Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof))
      (output_proof := output_proof)} wrapped_proof
| Wasm_2_0_0_pvm_with_proof :
  {'[state, context, output_proof] : [Set ** Set ** Set] @
    PVM_with_proof (state := state) (context := context)
      (proof :=
        Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof))
      (output_proof := output_proof)} wrapped_proof.

Definition wrapped_proof_module (p_value : wrapped_proof)
  : {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
    PVM_with_proof (state := state) (context := context) (proof := proof)
      (output_proof := output_proof)} :=
  match p_value with
  | Unencodable p_valuep_value
  | Arith_pvm_with_proof p_value
    let P := p_value in
    let 'existS _ _ P := P in
    existS (A := [Set ** Set ** Set ** Set]) _ [_, _, _, _]
      (let name := P.(PVM_with_proof.name) in
      let parse_boot_sector := P.(PVM_with_proof.parse_boot_sector) in
      let pp_boot_sector := P.(PVM_with_proof.pp_boot_sector) in
      let state := P.(PVM_with_proof.state) in
      let pp := P.(PVM_with_proof.pp) in
      let context := P.(PVM_with_proof.context) in
      let hash := P.(PVM_with_proof.hash) in
      let proof := P.(PVM_with_proof.proof) in
      let proof_encoding := P.(PVM_with_proof.proof_encoding) in
      let proof_start_state := P.(PVM_with_proof.proof_start_state) in
      let proof_stop_state := P.(PVM_with_proof.proof_stop_state) in
      let state_hash := P.(PVM_with_proof.state_hash) in
      let initial_state := P.(PVM_with_proof.initial_state) in
      let install_boot_sector := P.(PVM_with_proof.install_boot_sector) in
      let is_input_state := P.(PVM_with_proof.is_input_state) in
      let set_input := P.(PVM_with_proof.set_input) in
      let eval := P.(PVM_with_proof.eval) in
      let verify_proof := P.(PVM_with_proof.verify_proof) in
      let produce_proof := P.(PVM_with_proof.produce_proof) in
      let verify_origination_proof :=
        P.(PVM_with_proof.verify_origination_proof) in
      let produce_origination_proof :=
        P.(PVM_with_proof.produce_origination_proof) in
      let output_proof := P.(PVM_with_proof.output_proof) in
      let output_proof_encoding := P.(PVM_with_proof.output_proof_encoding) in
      let output_of_output_proof := P.(PVM_with_proof.output_of_output_proof) in
      let state_of_output_proof := P.(PVM_with_proof.state_of_output_proof) in
      let verify_output_proof := P.(PVM_with_proof.verify_output_proof) in
      let produce_output_proof := P.(PVM_with_proof.produce_output_proof) in
      let proof_val := P.(PVM_with_proof.proof_val) in
      {|
        PVM_with_proof.name := name;
        PVM_with_proof.parse_boot_sector := parse_boot_sector;
        PVM_with_proof.pp_boot_sector := pp_boot_sector;
        PVM_with_proof.pp := pp;
        PVM_with_proof.proof_encoding := proof_encoding;
        PVM_with_proof.proof_start_state := proof_start_state;
        PVM_with_proof.proof_stop_state := proof_stop_state;
        PVM_with_proof.state_hash := state_hash;
        PVM_with_proof.initial_state := initial_state;
        PVM_with_proof.install_boot_sector := install_boot_sector;
        PVM_with_proof.is_input_state := is_input_state;
        PVM_with_proof.set_input := set_input;
        PVM_with_proof.eval := eval;
        PVM_with_proof.verify_proof := verify_proof;
        PVM_with_proof.produce_proof := produce_proof;
        PVM_with_proof.verify_origination_proof := verify_origination_proof;
        PVM_with_proof.produce_origination_proof := produce_origination_proof;
        PVM_with_proof.output_proof_encoding := output_proof_encoding;
        PVM_with_proof.output_of_output_proof := output_of_output_proof;
        PVM_with_proof.state_of_output_proof := state_of_output_proof;
        PVM_with_proof.verify_output_proof := verify_output_proof;
        PVM_with_proof.produce_output_proof := produce_output_proof;
        PVM_with_proof.proof_val := proof_val
      |})
  | Wasm_2_0_0_pvm_with_proof p_value
    let P := p_value in
    let 'existS _ _ P := P in
    existS (A := [Set ** Set ** Set ** Set]) _ [_, _, _, _]
      (let name := P.(PVM_with_proof.name) in
      let parse_boot_sector := P.(PVM_with_proof.parse_boot_sector) in
      let pp_boot_sector := P.(PVM_with_proof.pp_boot_sector) in
      let state := P.(PVM_with_proof.state) in
      let pp := P.(PVM_with_proof.pp) in
      let context := P.(PVM_with_proof.context) in
      let hash := P.(PVM_with_proof.hash) in
      let proof := P.(PVM_with_proof.proof) in
      let proof_encoding := P.(PVM_with_proof.proof_encoding) in
      let proof_start_state := P.(PVM_with_proof.proof_start_state) in
      let proof_stop_state := P.(PVM_with_proof.proof_stop_state) in
      let state_hash := P.(PVM_with_proof.state_hash) in
      let initial_state := P.(PVM_with_proof.initial_state) in
      let install_boot_sector := P.(PVM_with_proof.install_boot_sector) in
      let is_input_state := P.(PVM_with_proof.is_input_state) in
      let set_input := P.(PVM_with_proof.set_input) in
      let eval := P.(PVM_with_proof.eval) in
      let verify_proof := P.(PVM_with_proof.verify_proof) in
      let produce_proof := P.(PVM_with_proof.produce_proof) in
      let verify_origination_proof :=
        P.(PVM_with_proof.verify_origination_proof) in
      let produce_origination_proof :=
        P.(PVM_with_proof.produce_origination_proof) in
      let output_proof := P.(PVM_with_proof.output_proof) in
      let output_proof_encoding := P.(PVM_with_proof.output_proof_encoding) in
      let output_of_output_proof := P.(PVM_with_proof.output_of_output_proof) in
      let state_of_output_proof := P.(PVM_with_proof.state_of_output_proof) in
      let verify_output_proof := P.(PVM_with_proof.verify_output_proof) in
      let produce_output_proof := P.(PVM_with_proof.produce_output_proof) in
      let proof_val := P.(PVM_with_proof.proof_val) in
      {|
        PVM_with_proof.name := name;
        PVM_with_proof.parse_boot_sector := parse_boot_sector;
        PVM_with_proof.pp_boot_sector := pp_boot_sector;
        PVM_with_proof.pp := pp;
        PVM_with_proof.proof_encoding := proof_encoding;
        PVM_with_proof.proof_start_state := proof_start_state;
        PVM_with_proof.proof_stop_state := proof_stop_state;
        PVM_with_proof.state_hash := state_hash;
        PVM_with_proof.initial_state := initial_state;
        PVM_with_proof.install_boot_sector := install_boot_sector;
        PVM_with_proof.is_input_state := is_input_state;
        PVM_with_proof.set_input := set_input;
        PVM_with_proof.eval := eval;
        PVM_with_proof.verify_proof := verify_proof;
        PVM_with_proof.produce_proof := produce_proof;
        PVM_with_proof.verify_origination_proof := verify_origination_proof;
        PVM_with_proof.produce_origination_proof := produce_origination_proof;
        PVM_with_proof.output_proof_encoding := output_proof_encoding;
        PVM_with_proof.output_of_output_proof := output_of_output_proof;
        PVM_with_proof.state_of_output_proof := state_of_output_proof;
        PVM_with_proof.verify_output_proof := verify_output_proof;
        PVM_with_proof.produce_output_proof := produce_output_proof;
        PVM_with_proof.proof_val := proof_val
      |})
  end.

Definition wrapped_proof_kind_exn (function_parameter : wrapped_proof)
  : Kind.t :=
  match function_parameter with
  | Unencodable _
    Pervasives.raise
      (Build_extensible "Invalid_argument" string
        "wrapped_proof_kind_exn: Unencodable")
  | Arith_pvm_with_proof _Kind.Example_arith
  | Wasm_2_0_0_pvm_with_proof _Kind.Wasm_2_0_0
  end.

Definition wrapped_proof_encoding : Data_encoding.encoding wrapped_proof :=
  let encoding :=
    Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
      [
        Data_encoding.case_value "Arithmetic PVM with proof" None
          (Data_encoding.Tag 0)
          (Data_encoding.obj2
            (Data_encoding.req None None "kind"
              (Data_encoding.constant "arith_pvm_kind"))
            (Data_encoding.req None None "proof"
              Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_encoding)))
          (fun (function_parameter : wrapped_proof) ⇒
            match function_parameter with
            | Arith_pvm_with_proof P
              let 'existS _ _ P := P in
              Some (tt, P.(PVM_with_proof.proof_val))
            | _None
            end)
          (fun (function_parameter :
            unit ×
              Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof))
            ⇒
            let '(_, proof_value) := function_parameter in
            Arith_pvm_with_proof
              (existS (A := [Set ** Set ** Set]) _ [_, _, _]
                (let state :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state)
                  in
                let pp :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp)
                  in
                let context :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.context)
                  in
                let hash :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.hash)
                  in
                let proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof)
                  in
                let proof_encoding :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_encoding)
                  in
                let proof_start_state :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_start_state)
                  in
                let proof_stop_state :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_stop_state)
                  in
                let state_hash :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state_hash)
                  in
                let initial_state :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.initial_state)
                  in
                let install_boot_sector :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.install_boot_sector)
                  in
                let is_input_state :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.is_input_state)
                  in
                let set_input :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.set_input)
                  in
                let eval :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.eval)
                  in
                let verify_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_proof)
                  in
                let produce_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_proof)
                  in
                let verify_origination_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_origination_proof)
                  in
                let produce_origination_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_origination_proof)
                  in
                let output_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_proof)
                  in
                let output_proof_encoding :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_proof_encoding)
                  in
                let output_of_output_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_of_output_proof)
                  in
                let state_of_output_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state_of_output_proof)
                  in
                let verify_output_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_output_proof)
                  in
                let produce_output_proof :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_output_proof)
                  in
                let name :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.name)
                  in
                let parse_boot_sector :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.parse_boot_sector)
                  in
                let pp_boot_sector :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp_boot_sector)
                  in
                let get_tick :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_tick)
                  in
                let status :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.status)
                  in
                let get_status :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_status)
                  in
                let get_outbox :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_outbox)
                  in
                let instruction :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.instruction)
                  in
                let equal_instruction :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.equal_instruction)
                  in
                let pp_instruction :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp_instruction)
                  in
                let get_parsing_result :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_parsing_result)
                  in
                let get_code :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_code)
                  in
                let get_stack :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_stack)
                  in
                let get_var :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_var)
                  in
                let get_evaluation_result :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_evaluation_result)
                  in
                let get_is_stuck :=
                  Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_is_stuck)
                  in
                let proof_val := proof_value in
                {|
                  PVM_with_proof.name := name;
                  PVM_with_proof.parse_boot_sector :=
                    parse_boot_sector;
                  PVM_with_proof.pp_boot_sector :=
                    pp_boot_sector;
                  PVM_with_proof.pp := pp;
                  PVM_with_proof.proof_encoding :=
                    proof_encoding;
                  PVM_with_proof.proof_start_state :=
                    proof_start_state;
                  PVM_with_proof.proof_stop_state :=
                    proof_stop_state;
                  PVM_with_proof.state_hash := state_hash;
                  PVM_with_proof.initial_state :=
                    initial_state;
                  PVM_with_proof.install_boot_sector :=
                    install_boot_sector;
                  PVM_with_proof.is_input_state :=
                    is_input_state;
                  PVM_with_proof.set_input := set_input;
                  PVM_with_proof.eval := eval;
                  PVM_with_proof.verify_proof :=
                    verify_proof;
                  PVM_with_proof.produce_proof :=
                    produce_proof;
                  PVM_with_proof.verify_origination_proof :=
                    verify_origination_proof;
                  PVM_with_proof.produce_origination_proof :=
                    produce_origination_proof;
                  PVM_with_proof.output_proof_encoding :=
                    output_proof_encoding;
                  PVM_with_proof.output_of_output_proof :=
                    output_of_output_proof;
                  PVM_with_proof.state_of_output_proof :=
                    state_of_output_proof;
                  PVM_with_proof.verify_output_proof :=
                    verify_output_proof;
                  PVM_with_proof.produce_output_proof :=
                    produce_output_proof;
                  PVM_with_proof.proof_val := proof_val
                |})));
        Data_encoding.case_value "Wasm 2.0.0 PVM with proof" None
          (Data_encoding.Tag 1)
          (Data_encoding.obj2
            (Data_encoding.req None None "kind"
              (Data_encoding.constant "wasm_2_0_0_pvm_kind"))
            (Data_encoding.req None None "proof"
              Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)))
          (fun (function_parameter : wrapped_proof) ⇒
            match function_parameter with
            | Wasm_2_0_0_pvm_with_proof pvm
              let 'P := pvm in
              let 'existS _ _ P := P in
              Some (tt, P.(PVM_with_proof.proof_val))
            | _None
            end)
          (fun (function_parameter :
            unit ×
              Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof))
            ⇒
            let '(_, proof_value) := function_parameter in
            Wasm_2_0_0_pvm_with_proof
              (existS (A := [Set ** Set ** Set]) _ [_, _, _]
                (let state :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state)
                  in
                let pp :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.pp)
                  in
                let context :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.context)
                  in
                let hash :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.hash)
                  in
                let proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof)
                  in
                let proof_encoding :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)
                  in
                let proof_start_state :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_start_state)
                  in
                let proof_stop_state :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_stop_state)
                  in
                let state_hash :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state_hash)
                  in
                let initial_state :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.initial_state)
                  in
                let install_boot_sector :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.install_boot_sector)
                  in
                let is_input_state :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.is_input_state)
                  in
                let set_input :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.set_input)
                  in
                let eval :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.eval)
                  in
                let verify_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_proof)
                  in
                let produce_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_proof)
                  in
                let verify_origination_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_origination_proof)
                  in
                let produce_origination_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_origination_proof)
                  in
                let output_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_proof)
                  in
                let output_proof_encoding :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_proof_encoding)
                  in
                let output_of_output_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_of_output_proof)
                  in
                let state_of_output_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state_of_output_proof)
                  in
                let verify_output_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_output_proof)
                  in
                let produce_output_proof :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_output_proof)
                  in
                let name :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.name)
                  in
                let parse_boot_sector :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.parse_boot_sector)
                  in
                let pp_boot_sector :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.pp_boot_sector)
                  in
                let get_tick :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.get_tick)
                  in
                let status :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.status)
                  in
                let get_status :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.get_status)
                  in
                let get_outbox :=
                  Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.get_outbox)
                  in
                let proof_val := proof_value in
                {|
                  PVM_with_proof.name := name;
                  PVM_with_proof.parse_boot_sector :=
                    parse_boot_sector;
                  PVM_with_proof.pp_boot_sector :=
                    pp_boot_sector;
                  PVM_with_proof.pp := pp;
                  PVM_with_proof.proof_encoding :=
                    proof_encoding;
                  PVM_with_proof.proof_start_state :=
                    proof_start_state;
                  PVM_with_proof.proof_stop_state :=
                    proof_stop_state;
                  PVM_with_proof.state_hash := state_hash;
                  PVM_with_proof.initial_state :=
                    initial_state;
                  PVM_with_proof.install_boot_sector :=
                    install_boot_sector;
                  PVM_with_proof.is_input_state :=
                    is_input_state;
                  PVM_with_proof.set_input := set_input;
                  PVM_with_proof.eval := eval;
                  PVM_with_proof.verify_proof :=
                    verify_proof;
                  PVM_with_proof.produce_proof :=
                    produce_proof;
                  PVM_with_proof.verify_origination_proof :=
                    verify_origination_proof;
                  PVM_with_proof.produce_origination_proof :=
                    produce_origination_proof;
                  PVM_with_proof.output_proof_encoding :=
                    output_proof_encoding;
                  PVM_with_proof.output_of_output_proof :=
                    output_of_output_proof;
                  PVM_with_proof.state_of_output_proof :=
                    state_of_output_proof;
                  PVM_with_proof.verify_output_proof :=
                    verify_output_proof;
                  PVM_with_proof.produce_output_proof :=
                    produce_output_proof;
                  PVM_with_proof.proof_val := proof_val
                |})));
        Data_encoding.case_value "Unencodable" None (Data_encoding.Tag 255)
          Data_encoding.empty
          (fun (function_parameter : wrapped_proof) ⇒
            match function_parameter with
            | Unencodable P
              let 'existS _ _ P := P in
              Pervasives.raise
                (Build_extensible "Invalid_argument" string
                  (Format.sprintf
                    (CamlinternalFormatBasics.Format
                      (CamlinternalFormatBasics.String_literal
                        "cannot encode Unencodable (PVM "
                        (CamlinternalFormatBasics.String
                          CamlinternalFormatBasics.No_padding
                          (CamlinternalFormatBasics.Char_literal
                            ")" % char
                            CamlinternalFormatBasics.End_of_format)))
                      "cannot encode Unencodable (PVM %s)")
                    P.(PVM_with_proof.name)))
            | _None
            end)
          (fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Pervasives.raise
              (Build_extensible "Invalid_argument" string
                "cannot decode Unencodable"))
      ] in
  Data_encoding.check_size Constants_repr.sc_max_wrapped_proof_binary_size
    encoding.

Definition wrap_proof
  (pvm_with_proof :
    {'[state, context, proof, output_proof] : [Set ** Set ** Set ** Set] @
      PVM_with_proof (state := state) (context := context) (proof := proof)
        (output_proof := output_proof)}) : option wrapped_proof :=
  let 'P := pvm_with_proof in
  let 'existS _ _ P := P in
  match Kind.of_name P.(PVM_with_proof.name) with
  | NoneSome (Unencodable pvm_with_proof)
  | Some Kind.Example_arith
    Option.map
      (fun (arith_proof : Context.Proof.t Context.Proof.tree) ⇒
        let P_arith :=
          let state :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state) in
          let pp :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp) in
          let context :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.context)
            in
          let hash :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.hash) in
          let proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof) in
          let proof_encoding :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_encoding)
            in
          let proof_start_state :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_start_state)
            in
          let proof_stop_state :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_stop_state)
            in
          let state_hash :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state_hash)
            in
          let initial_state :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.initial_state)
            in
          let install_boot_sector :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.install_boot_sector)
            in
          let is_input_state :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.is_input_state)
            in
          let set_input :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.set_input)
            in
          let eval :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.eval) in
          let verify_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_proof)
            in
          let produce_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_proof)
            in
          let verify_origination_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_origination_proof)
            in
          let produce_origination_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_origination_proof)
            in
          let output_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_proof)
            in
          let output_proof_encoding :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_proof_encoding)
            in
          let output_of_output_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.output_of_output_proof)
            in
          let state_of_output_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.state_of_output_proof)
            in
          let verify_output_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.verify_output_proof)
            in
          let produce_output_proof :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.produce_output_proof)
            in
          let name :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.name) in
          let parse_boot_sector :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.parse_boot_sector)
            in
          let pp_boot_sector :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp_boot_sector)
            in
          let get_tick :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_tick)
            in
          let status :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.status)
            in
          let get_status :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_status)
            in
          let get_outbox :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_outbox)
            in
          let instruction :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.instruction)
            in
          let equal_instruction :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.equal_instruction)
            in
          let pp_instruction :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.pp_instruction)
            in
          let get_parsing_result :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_parsing_result)
            in
          let get_code :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_code)
            in
          let get_stack :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_stack)
            in
          let get_var :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_var)
            in
          let get_evaluation_result :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_evaluation_result)
            in
          let get_is_stuck :=
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.get_is_stuck)
            in
          let proof_val := arith_proof in
          {|
            PVM_with_proof.name := name;
            PVM_with_proof.parse_boot_sector := parse_boot_sector;
            PVM_with_proof.pp_boot_sector := pp_boot_sector;
            PVM_with_proof.pp := pp;
            PVM_with_proof.proof_encoding := proof_encoding;
            PVM_with_proof.proof_start_state := proof_start_state;
            PVM_with_proof.proof_stop_state := proof_stop_state;
            PVM_with_proof.state_hash := state_hash;
            PVM_with_proof.initial_state := initial_state;
            PVM_with_proof.install_boot_sector := install_boot_sector;
            PVM_with_proof.is_input_state := is_input_state;
            PVM_with_proof.set_input := set_input;
            PVM_with_proof.eval := eval;
            PVM_with_proof.verify_proof := verify_proof;
            PVM_with_proof.produce_proof := produce_proof;
            PVM_with_proof.verify_origination_proof := verify_origination_proof;
            PVM_with_proof.produce_origination_proof :=
              produce_origination_proof;
            PVM_with_proof.output_proof_encoding := output_proof_encoding;
            PVM_with_proof.output_of_output_proof := output_of_output_proof;
            PVM_with_proof.state_of_output_proof := state_of_output_proof;
            PVM_with_proof.verify_output_proof := verify_output_proof;
            PVM_with_proof.produce_output_proof := produce_output_proof;
            PVM_with_proof.proof_val := proof_val
          |} in
        Arith_pvm_with_proof
          (existS (A := [Set ** Set ** Set]) _ [_, _, _] P_arith))
      (Option.bind
        (Data_encoding.Binary.to_bytes_opt None
          P.(PVM_with_proof.proof_encoding) P.(PVM_with_proof.proof_val))
        (fun (bytes_value : bytes) ⇒
          Data_encoding.Binary.of_bytes_opt
            Sc_rollup_arith.Protocol_implementation.(Sc_rollup_arith.S.proof_encoding)
            bytes_value))
  | Some Kind.Wasm_2_0_0
    Option.map
      (fun (wasm_proof : Context.Proof.t Context.Proof.tree) ⇒
        let P_wasm2_0_0 :=
          let state :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state)
            in
          let pp :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.pp)
            in
          let context :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.context)
            in
          let hash :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.hash)
            in
          let proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof)
            in
          let proof_encoding :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)
            in
          let proof_start_state :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_start_state)
            in
          let proof_stop_state :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_stop_state)
            in
          let state_hash :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state_hash)
            in
          let initial_state :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.initial_state)
            in
          let install_boot_sector :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.install_boot_sector)
            in
          let is_input_state :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.is_input_state)
            in
          let set_input :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.set_input)
            in
          let eval :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.eval)
            in
          let verify_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_proof)
            in
          let produce_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_proof)
            in
          let verify_origination_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_origination_proof)
            in
          let produce_origination_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_origination_proof)
            in
          let output_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_proof)
            in
          let output_proof_encoding :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_proof_encoding)
            in
          let output_of_output_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.output_of_output_proof)
            in
          let state_of_output_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.state_of_output_proof)
            in
          let verify_output_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.verify_output_proof)
            in
          let produce_output_proof :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.produce_output_proof)
            in
          let name :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.name)
            in
          let parse_boot_sector :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.parse_boot_sector)
            in
          let pp_boot_sector :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.pp_boot_sector)
            in
          let get_tick :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.get_tick)
            in
          let status :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.status)
            in
          let get_status :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.get_status)
            in
          let get_outbox :=
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.get_outbox)
            in
          let proof_val := wasm_proof in
          {|
            PVM_with_proof.name := name;
            PVM_with_proof.parse_boot_sector := parse_boot_sector;
            PVM_with_proof.pp_boot_sector := pp_boot_sector;
            PVM_with_proof.pp := pp;
            PVM_with_proof.proof_encoding := proof_encoding;
            PVM_with_proof.proof_start_state := proof_start_state;
            PVM_with_proof.proof_stop_state := proof_stop_state;
            PVM_with_proof.state_hash := state_hash;
            PVM_with_proof.initial_state := initial_state;
            PVM_with_proof.install_boot_sector := install_boot_sector;
            PVM_with_proof.is_input_state := is_input_state;
            PVM_with_proof.set_input := set_input;
            PVM_with_proof.eval := eval;
            PVM_with_proof.verify_proof := verify_proof;
            PVM_with_proof.produce_proof := produce_proof;
            PVM_with_proof.verify_origination_proof := verify_origination_proof;
            PVM_with_proof.produce_origination_proof :=
              produce_origination_proof;
            PVM_with_proof.output_proof_encoding := output_proof_encoding;
            PVM_with_proof.output_of_output_proof := output_of_output_proof;
            PVM_with_proof.state_of_output_proof := state_of_output_proof;
            PVM_with_proof.verify_output_proof := verify_output_proof;
            PVM_with_proof.produce_output_proof := produce_output_proof;
            PVM_with_proof.proof_val := proof_val
          |} in
        Wasm_2_0_0_pvm_with_proof
          (existS (A := [Set ** Set ** Set]) _ [_, _, _] P_wasm2_0_0))
      (Option.bind
        (Data_encoding.Binary.to_bytes_opt None
          P.(PVM_with_proof.proof_encoding) P.(PVM_with_proof.proof_val))
        (fun (bytes_value : bytes) ⇒
          Data_encoding.Binary.of_bytes_opt
            Sc_rollup_wasm.V2_0_0.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)
            bytes_value))
  end.