🦏 Sc_rollups.v
Translated 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.Raw_level_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 : state → 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_arith ⇒ example_arith_pvm
| Wasm_2_0_0 ⇒ wasm_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_value ⇒ k_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 : state → 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_value ⇒ p_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
| None ⇒ Some (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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Raw_level_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 : state → 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_arith ⇒ example_arith_pvm
| Wasm_2_0_0 ⇒ wasm_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_value ⇒ k_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 : state → 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_value ⇒ p_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
| None ⇒ Some (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.