🦏 Sc_rollup_wasm.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.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Internal_errors.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Internal_errors.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_outbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Init function; without side-effects in Coq
Definition init_module : unit :=
let msg := "Invalid claim about outbox" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_wasm_invalid_claim_about_outbox" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt msg)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "WASM_invalid_claim_about_outbox" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "WASM_invalid_claim_about_outbox" unit tt) in
let msg := "Output proof production failed" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_wasm_output_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "WASM_output_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "WASM_output_proof_production_failed" unit tt) in
let msg := "Proof production failed" in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_wasm_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "WASM_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "WASM_proof_production_failed" unit tt).
Module V2_0_0.
Definition reference_initial_state_hash : Sc_rollup_repr.State_hash.t :=
Sc_rollup_repr.State_hash.of_b58check_exn
"scs11pDQTn37TBnWgQAiCPdMAcQPiXARjg9ZZVmLx26sZwxeSxovE5".
Module PS := Sc_rollup_PVM_sig.
Module P.
Record signature {Tree_t Tree_tree proof : Set} : Set := {
Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes);
tree := Tree.(Context.TREE.tree);
proof := proof;
proof_encoding : Data_encoding.t proof;
proof_before : proof → Sc_rollup_repr.State_hash.t;
proof_after : proof → Sc_rollup_repr.State_hash.t;
verify_proof :
∀ {a : Set}, proof → (tree → tree × a) → option (tree × a);
produce_proof :
∀ {a : Set},
Tree.(Context.TREE.t) → tree → (tree → tree × a) →
option (proof × a);
}.
End P.
Definition P := @P.signature.
Arguments P {_ _ _}.
Module S.
Record signature {state context proof output_proof status : Set} : Set := {
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; *)
name : string;
parse_boot_sector : string → option string;
pp_boot_sector : Format.formatter → string → unit;
let msg := "Invalid claim about outbox" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_wasm_invalid_claim_about_outbox" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt msg)) Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "WASM_invalid_claim_about_outbox" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "WASM_invalid_claim_about_outbox" unit tt) in
let msg := "Output proof production failed" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_wasm_output_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "WASM_output_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "WASM_output_proof_production_failed" unit tt) in
let msg := "Proof production failed" in
Error_monad.register_error_kind Error_monad.Permanent
"sc_rollup_wasm_proof_production_failed" msg msg
(Some
(fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") msg))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "WASM_proof_production_failed" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "WASM_proof_production_failed" unit tt).
Module V2_0_0.
Definition reference_initial_state_hash : Sc_rollup_repr.State_hash.t :=
Sc_rollup_repr.State_hash.of_b58check_exn
"scs11pDQTn37TBnWgQAiCPdMAcQPiXARjg9ZZVmLx26sZwxeSxovE5".
Module PS := Sc_rollup_PVM_sig.
Module P.
Record signature {Tree_t Tree_tree proof : Set} : Set := {
Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes);
tree := Tree.(Context.TREE.tree);
proof := proof;
proof_encoding : Data_encoding.t proof;
proof_before : proof → Sc_rollup_repr.State_hash.t;
proof_after : proof → Sc_rollup_repr.State_hash.t;
verify_proof :
∀ {a : Set}, proof → (tree → tree × a) → option (tree × a);
produce_proof :
∀ {a : Set},
Tree.(Context.TREE.t) → tree → (tree → tree × a) →
option (proof × a);
}.
End P.
Definition P := @P.signature.
Arguments P {_ _ _}.
Module S.
Record signature {state context proof output_proof status : Set} : Set := {
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; *)
name : string;
parse_boot_sector : string → option string;
pp_boot_sector : Format.formatter → string → unit;
[get_tick state] gets the total tick counter for the given PVM state.
PVM status
[get_status state] gives you the current execution status for the PVM.
get_status : state → status;
get_outbox : Raw_level_repr.t → state → list Sc_rollup_PVM_sig.output;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _ _}.
Module Make.
Class FArgs {Context_Tree_t Context_Tree_tree Context_proof : Set} := {
Make_backend :
∀ {Tree_t Tree_tree : Set},
∀ (Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes)), Wasm_2_0_0.S (tree := Tree.(Context.TREE.tree));
Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof);
}.
Arguments Build_FArgs {_ _ _}.
Definition Tree `{FArgs} := Context.(P.Tree).
Definition context `{FArgs} : Set := Context.(P.Tree).(Context.TREE.t).
Definition hash `{FArgs} : Set := Sc_rollup_repr.State_hash.t.
Definition proof `{FArgs} : Set := Context.(P.proof).
Definition proof_encoding `{FArgs} : Data_encoding.t proof :=
Context.(P.proof_encoding).
Definition proof_start_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_before) proof_value.
Definition proof_stop_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_after) proof_value.
Definition name `{FArgs} : string := "wasm_2_0_0".
Definition parse_boot_sector `{FArgs} (s_value : string) : option string :=
Hex.to_string (Hex.Hex s_value).
Definition pp_boot_sector `{FArgs}
(fmt : Format.formatter) (s_value : string) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") s_value.
Definition tree `{FArgs} : Set := Context.(P.Tree).(Context.TREE.tree).
Inductive status `{FArgs} : Set :=
| Computing : status
| Waiting_for_input_message : status
| Waiting_for_reveal : Sc_rollup_PVM_sig.reveal → status.
Module State.
Definition state `{FArgs} : Set := tree.
Module Monad.
Definition t `{FArgs} (a : Set) : Set := state → state × a.
Definition _return `{FArgs} {A B : Set} (x_value : A) (state_value : B)
: B × A := (state_value, x_value).
Definition bind `{FArgs} {A B C D : Set}
(m_value : A → B × C) (f_value : C → B → D) (state_value : A)
: D :=
let '(state_value, res) := m_value state_value in
f_value res state_value.
Module Syntax.
Definition op_letstar `{FArgs} {A B C D : Set}
: (A → B × C) → (C → B → D) → A → D := bind.
End Syntax.
Definition run `{FArgs} {A B : Set} (m_value : A → B) (state_value : A)
: B := m_value state_value.
Definition get `{FArgs} {A : Set} (s_value : A) : A × A :=
(s_value, s_value).
Definition set `{FArgs} {A B : Set}
(s_value : A) (function_parameter : B) : A × unit :=
let '_ := function_parameter in
(s_value, tt).
Definition lift `{FArgs} {A B : Set} (m_value : A) (s_value : B)
: B × A := id (fun (r_value : A) ⇒ (s_value, r_value)) m_value.
End Monad.
End State.
Definition state `{FArgs} : Set := State.state.
Definition WASM_machine `{FArgs} := Make_backend Tree.
Definition pp `{FArgs} {A : Set} (_state : A)
: Format.formatter → unit → unit :=
fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt "<wasm-state>".
Definition initial_state `{FArgs}
(empty : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) :=
let state_value :=
Tree.(Context.TREE.add) empty [ "wasm-version" ]
(Bytes.of_string "2.0.0") in
state_value.
Definition install_boot_sector `{FArgs}
(state_value : Context.(P.Tree).(Context.TREE.tree))
(boot_sector : string) : Context.(P.Tree).(Context.TREE.tree) :=
WASM_machine.(Wasm_2_0_0.S.install_boot_sector) boot_sector state_value.
Definition state_hash `{FArgs}
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Sc_rollup_repr.State_hash.t :=
let context_hash := Tree.(Context.TREE.hash_value) state_value in
match Sc_rollup_repr.State_hash.context_hash_to_state_hash context_hash
with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end.
Definition result_of `{FArgs} {A : Set}
(m_value : State.Monad.t A) (state_value : State.state) : A :=
let '(_, v_value) := State.Monad.run m_value state_value in
v_value.
Definition state_of `{FArgs} {A : Set}
(m_value : State.Monad.t A) (state_value : State.state) : State.state :=
let '(s_value, _) := State.Monad.run m_value state_value in
s_value.
Definition get_tick_aux `{FArgs} : State.Monad.t Sc_rollup_tick_repr.t :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
(fun info_value ⇒
State.Monad._return
(Sc_rollup_tick_repr.of_z
info_value.(Wasm_2_0_0.info.current_tick)))).
Definition get_tick `{FArgs} : State.state → Sc_rollup_tick_repr.t :=
result_of get_tick_aux.
Definition get_status_aux `{FArgs} : State.Monad.t status :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
(fun info_value ⇒
State.Monad._return
match info_value.(Wasm_2_0_0.info.input_request) with
| Wasm_2_0_0.No_input_required ⇒ Computing
| Wasm_2_0_0.Input_required ⇒ Waiting_for_input_message
|
Wasm_2_0_0.Reveal_required
(Wasm_2_0_0.Reveal_raw_data hash_value) ⇒
match
Data_encoding.Binary.of_string_opt
Sc_rollup_PVM_sig.Reveal_hash.encoding
(Wasm_2_0_0.reveal_hash_to_string hash_value) with
| Some hash_value ⇒
Waiting_for_reveal
(Sc_rollup_PVM_sig.Reveal_raw_data hash_value)
| None ⇒
Waiting_for_reveal
(Sc_rollup_PVM_sig.Reveal_raw_data
Sc_rollup_PVM_sig.Reveal_hash.zero)
end
| Wasm_2_0_0.Reveal_required Wasm_2_0_0.Reveal_metadata ⇒
Waiting_for_reveal Sc_rollup_PVM_sig.Reveal_metadata
end)).
Definition get_last_message_read `{FArgs}
: State.Monad.t (option (M? Raw_level_repr.raw_level × Z.t)) :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
(fun info_value ⇒
State.Monad._return
match info_value.(Wasm_2_0_0.info.last_input_read) with
|
Some {|
Wasm_2_0_0.input.inbox_level := inbox_level;
Wasm_2_0_0.input.message_counter := message_counter
|} ⇒
let inbox_level :=
Raw_level_repr.of_int32_non_negative inbox_level in
Some (inbox_level, message_counter)
| _ ⇒ None
end)).
Definition is_input_state_aux `{FArgs} : State.Monad.t PS.input_request :=
State.Monad.Syntax.op_letstar get_status_aux
(fun status ⇒
match status with
| Waiting_for_input_message ⇒
State.Monad.Syntax.op_letstar get_last_message_read
(fun last_read ⇒
match last_read with
| Some (level, n_value) ⇒
match level with
| Pervasives.Ok lvl ⇒
State.Monad._return
(Sc_rollup_PVM_sig.First_after lvl n_value)
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert (State.Monad.t PS.input_request) false
end
| None ⇒ State.Monad._return Sc_rollup_PVM_sig.Initial
end)
| Computing ⇒ State.Monad._return Sc_rollup_PVM_sig.No_input_required
| Waiting_for_reveal reveal ⇒
State.Monad._return (Sc_rollup_PVM_sig.Needs_reveal reveal)
end).
Definition is_input_state `{FArgs} : State.state → PS.input_request :=
result_of is_input_state_aux.
Definition get_status `{FArgs} : State.state → status :=
result_of get_status_aux.
#[bypass_check(guard)]
Definition get_outbox `{FArgs}
(outbox_level : Raw_level_repr.raw_level)
(state_value : Context.(P.Tree).(Context.TREE.tree)) : list PS.output :=
let outbox_level_int32 :=
Internal_errors.ignore_errors
(Raw_level_repr.to_int32_non_negative outbox_level) in
let fix aux (outbox : list PS.output) (message_index : Z.t)
{struct message_index} : list PS.output :=
let output :=
{| Wasm_2_0_0.output.outbox_level := outbox_level_int32;
Wasm_2_0_0.output.message_index := message_index; |} in
let res := WASM_machine.(Wasm_2_0_0.S.get_output) output state_value in
match res with
| None ⇒ List.rev outbox
| Some msg ⇒
let serialized := Sc_rollup_outbox_message_repr.unsafe_of_string msg
in
match Sc_rollup_outbox_message_repr.deserialize serialized with
| Pervasives.Error _ ⇒ aux outbox (Z.succ message_index)
| Pervasives.Ok message ⇒
let output :=
{| Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
Sc_rollup_PVM_sig.output.message_index := message_index;
Sc_rollup_PVM_sig.output.message := message; |} in
aux (cons output outbox) (Z.succ message_index)
end
end in
aux nil Z.zero.
Definition set_input_state `{FArgs} (input : PS.input)
: State.Monad.t unit :=
match input with
| Sc_rollup_PVM_sig.Inbox_message input ⇒
let '{|
Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload
|} := input in
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
let inbox_level :=
match Raw_level_repr.to_int32_non_negative inbox_level with
| Pervasives.Ok lvl ⇒ lvl
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Bounded.Non_negative_int32.(Bounded.S.t) false
end in
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.set_input_step)
{| Wasm_2_0_0.input.inbox_level := inbox_level;
Wasm_2_0_0.input.message_counter := message_counter; |}
payload s_value)) (fun s_value ⇒ State.Monad.set s_value))
| Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Raw_data data) ⇒
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.reveal_step) (Bytes.of_string data)
s_value)) (fun s_value ⇒ State.Monad.set s_value))
| Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Metadata metadata) ⇒
let metadata_bytes :=
Data_encoding.Binary.to_bytes_exn None
Sc_rollup_metadata_repr.encoding metadata in
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.reveal_step) metadata_bytes s_value))
(fun s_value ⇒ State.Monad.set s_value))
| Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Dal_page _content_opt) ⇒
(* ❌ Assert instruction is not handled. *)
assert (State.Monad.t unit) false
end.
Definition set_input `{FArgs} (input : PS.input)
: State.state → State.state := state_of (set_input_state input).
Definition eval_step `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.compute_step) s_value))
(fun s_value ⇒ State.Monad.set s_value)).
Definition eval `{FArgs} (state_value : State.state) : State.state :=
state_of eval_step state_value.
Definition step_transition `{FArgs}
(input_given : option PS.input) (state_value : State.state)
: State.state × PS.input_request :=
let request := is_input_state state_value in
let state_value :=
match request with
| Sc_rollup_PVM_sig.No_input_required ⇒ eval state_value
| _ ⇒
match input_given with
| Some input ⇒ set_input input state_value
| None ⇒ state_value
end
end in
(state_value, request).
Definition verify_proof `{FArgs}
(input_given : option PS.input) (proof_value : proof)
: M? PS.input_request :=
let result_value :=
Context.(P.verify_proof) proof_value (step_transition input_given) in
match result_value with
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "WASM_proof_verification_failed" unit tt)
| Some (_state, request) ⇒ return? request
end.
Definition produce_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(input_given : option PS.input)
(state_value : Context.(P.Tree).(Context.TREE.tree)) : M? proof :=
let result_value :=
Context.(P.produce_proof) context_value state_value
(step_transition input_given) in
match result_value with
| Some (tree_proof, _requested) ⇒ return? tree_proof
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "WASM_proof_production_failed" unit tt)
end.
Definition verify_origination_proof `{FArgs}
(proof_value : proof) (boot_sector : string) : bool :=
let before := Context.(P.proof_before) proof_value in
if
Sc_rollup_repr.State_hash.op_ltgt before reference_initial_state_hash
then
false
else
let result_value :=
Context.(P.verify_proof) proof_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| None ⇒ false
| Some (_, _) ⇒ true
end.
Definition produce_origination_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t)) (boot_sector : string)
: M? proof :=
let state_value := initial_state (Tree.(Context.TREE.empty) context_value)
in
let result_value :=
Context.(P.produce_proof) context_value state_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| Some (tree_proof, _) ⇒ return? tree_proof
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "WASM_proof_production_failed" unit tt)
end.
Module output_proof.
Record record `{FArgs} : Set := Build {
output_proof : Context.(P.proof);
output_proof_state : hash;
output_proof_output : PS.output;
}.
Definition with_output_proof `{FArgs} output_proof (r : record) :=
Build _ _ _ _ output_proof r.(output_proof_state)
r.(output_proof_output).
Definition with_output_proof_state `{FArgs} output_proof_state
(r : record) :=
Build _ _ _ _ r.(output_proof) output_proof_state
r.(output_proof_output).
Definition with_output_proof_output `{FArgs} output_proof_output
(r : record) :=
Build _ _ _ _ r.(output_proof) r.(output_proof_state)
output_proof_output.
End output_proof.
Definition output_proof `{FArgs} := output_proof.record.
Definition output_proof_encoding `{FArgs}
: Data_encoding.encoding output_proof :=
Data_encoding.conv
(fun (function_parameter : output_proof) ⇒
let '{|
output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output
|} := function_parameter in
(output_proof, output_proof_state, output_proof_output))
(fun (function_parameter : Context.(P.proof) × hash × PS.output) ⇒
let '(output_proof, output_proof_state, output_proof_output) :=
function_parameter in
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "output_proof" Context.(P.proof_encoding))
(Data_encoding.req None None "output_proof_state"
Sc_rollup_repr.State_hash.encoding)
(Data_encoding.req None None "output_proof_output" PS.output_encoding)).
Definition output_of_output_proof `{FArgs} (s_value : output_proof)
: PS.output := s_value.(output_proof.output_proof_output).
Definition state_of_output_proof `{FArgs} (s_value : output_proof) : hash :=
s_value.(output_proof.output_proof_state).
Definition has_output `{FArgs} (function_parameter : PS.output)
: State.Monad.t bool :=
let '{|
Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
Sc_rollup_PVM_sig.output.message_index := message_index;
Sc_rollup_PVM_sig.output.message := message
|} := function_parameter in
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
let lvl :=
match Raw_level_repr.to_int32_non_negative outbox_level with
| Pervasives.Ok lvl ⇒ lvl
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Bounded.Non_negative_int32.(Bounded.S.t) false
end in
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.get_output)
{| Wasm_2_0_0.output.outbox_level := lvl;
Wasm_2_0_0.output.message_index := message_index; |} s_value))
(fun result_value ⇒
let message_encoded :=
Data_encoding.Binary.to_string_exn None
Sc_rollup_outbox_message_repr.encoding message in
State.Monad._return
match result_value with
| Some result_value ⇒
Compare.String.(Compare.S.op_eq) result_value message_encoded
| None ⇒ false
end)).
Definition verify_output_proof `{FArgs} (p_value : output_proof) : bool :=
let transition :=
State.Monad.run (has_output p_value.(output_proof.output_proof_output))
in
let result_value :=
Context.(P.verify_proof) p_value.(output_proof.output_proof) transition
in
match result_value with
| None ⇒ false
| Some _ ⇒ true
end.
Definition produce_output_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(state_value : Context.(P.Tree).(Context.TREE.tree))
(output_proof_output : PS.output)
: Pervasives.result output_proof Error_monad._error :=
let output_proof_state := state_hash state_value in
let result_value :=
Context.(P.produce_proof) context_value state_value
(State.Monad.run (has_output output_proof_output)) in
match result_value with
| Some (output_proof, true) ⇒
return?
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}
| Some (_, false) ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "WASM_invalid_claim_about_outbox" unit tt)
| None ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "WASM_output_proof_production_failed" unit tt)
end.
(* Make *)
Definition functor `{FArgs} :=
{|
S.pp := pp;
S.proof_encoding := proof_encoding;
S.proof_start_state := proof_start_state;
S.proof_stop_state := proof_stop_state;
S.state_hash := state_hash;
S.initial_state := initial_state;
S.install_boot_sector := install_boot_sector;
S.is_input_state := is_input_state;
S.set_input := set_input;
S.eval := eval;
S.verify_proof := verify_proof;
S.produce_proof := produce_proof;
S.verify_origination_proof := verify_origination_proof;
S.produce_origination_proof := produce_origination_proof;
S.output_proof_encoding := output_proof_encoding;
S.output_of_output_proof := output_of_output_proof;
S.state_of_output_proof := state_of_output_proof;
S.verify_output_proof := verify_output_proof;
S.produce_output_proof := produce_output_proof;
S.name := name;
S.parse_boot_sector := parse_boot_sector;
S.pp_boot_sector := pp_boot_sector;
S.get_tick := get_tick;
S.get_status := get_status;
S.get_outbox := get_outbox
|}.
End Make.
Definition Make {Context_Tree_t Context_Tree_tree Context_proof : Set}
(Make_backend :
∀ {Tree_t Tree_tree : Set},
∀ (Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes)), Wasm_2_0_0.S (tree := Tree.(Context.TREE.tree)))
(Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof))
: S (state := Context.(P.Tree).(Context.TREE.tree))
(context := Context.(P.Tree).(Context.TREE.t))
(proof := Context.(P.proof)) (output_proof := _) (status := _) :=
let '_ := Make.Build_FArgs (@Make_backend) Context in
Make.functor.
Definition Protocol_implementation :=
Make (@Wasm_2_0_0.Make)
(let Tree :=
let mem := Context.Tree.(Context.TREE.mem) in
let mem_tree := Context.Tree.(Context.TREE.mem_tree) in
let find := Context.Tree.(Context.TREE.find) in
let find_tree := Context.Tree.(Context.TREE.find_tree) in
let list_value := Context.Tree.(Context.TREE.list_value) in
let length := Context.Tree.(Context.TREE.length) in
let add := Context.Tree.(Context.TREE.add) in
let add_tree := Context.Tree.(Context.TREE.add_tree) in
let remove := Context.Tree.(Context.TREE.remove) in
let fold {a : Set} := Context.Tree.(Context.TREE.fold) in
let config_value := Context.Tree.(Context.TREE.config_value) in
let empty := Context.Tree.(Context.TREE.empty) in
let is_empty := Context.Tree.(Context.TREE.is_empty) in
let kind_value := Context.Tree.(Context.TREE.kind_value) in
let to_value := Context.Tree.(Context.TREE.to_value) in
let of_value := Context.Tree.(Context.TREE.of_value) in
let hash_value := Context.Tree.(Context.TREE.hash_value) in
let equal := Context.Tree.(Context.TREE.equal) in
let clear := Context.Tree.(Context.TREE.clear) in
let tree : Set := Context.tree in
let t : Set := Context.t in
let key : Set := list string in
let value : Set := bytes in
{|
Context.TREE.mem := mem;
Context.TREE.mem_tree := mem_tree;
Context.TREE.find := find;
Context.TREE.find_tree := find_tree;
Context.TREE.list_value := list_value;
Context.TREE.length := length;
Context.TREE.add := add;
Context.TREE.add_tree := add_tree;
Context.TREE.remove := remove;
Context.TREE.fold _ := fold;
Context.TREE.config_value := config_value;
Context.TREE.empty := empty;
Context.TREE.is_empty := is_empty;
Context.TREE.kind_value := kind_value;
Context.TREE.to_value := to_value;
Context.TREE.of_value := of_value;
Context.TREE.hash_value := hash_value;
Context.TREE.equal := equal;
Context.TREE.clear := clear
|} in
let tree : Set := Context.tree in
let proof : Set := Context.Proof.t Context.Proof.tree in
let verify_proof {A : Set}
(p_value : Context.Proof.t Context.Proof.tree)
(f_value : Context.tree → Context.tree × A)
: option (Context.tree × A) :=
id Result.to_option (Context.verify_tree_proof p_value f_value) in
let produce_proof {A B C D : Set} (_context : A) (_state : B) (_f : C)
: option D :=
None in
let kinded_hash_to_state_hash
(function_parameter : Context.Proof.kinded_hash)
: M? Sc_rollup_repr.State_hash.t :=
match function_parameter with
| (Context.Proof.KValue hash_value | Context.Proof.KNode hash_value) ⇒
Sc_rollup_repr.State_hash.context_hash_to_state_hash hash_value
end in
let proof_before {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.before)
with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_after {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.after) with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_encoding :=
Context.Proof_encoding.V2.Tree32.(Context.PROOF_ENCODING.tree_proof_encoding)
in
{|
P.Tree := Tree;
P.proof_encoding := proof_encoding;
P.proof_before := proof_before;
P.proof_after := proof_after;
P.verify_proof _ := verify_proof;
P.produce_proof _ := produce_proof
|}).
End V2_0_0.
get_outbox : Raw_level_repr.t → state → list Sc_rollup_PVM_sig.output;
}.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _ _}.
Module Make.
Class FArgs {Context_Tree_t Context_Tree_tree Context_proof : Set} := {
Make_backend :
∀ {Tree_t Tree_tree : Set},
∀ (Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes)), Wasm_2_0_0.S (tree := Tree.(Context.TREE.tree));
Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof);
}.
Arguments Build_FArgs {_ _ _}.
Definition Tree `{FArgs} := Context.(P.Tree).
Definition context `{FArgs} : Set := Context.(P.Tree).(Context.TREE.t).
Definition hash `{FArgs} : Set := Sc_rollup_repr.State_hash.t.
Definition proof `{FArgs} : Set := Context.(P.proof).
Definition proof_encoding `{FArgs} : Data_encoding.t proof :=
Context.(P.proof_encoding).
Definition proof_start_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_before) proof_value.
Definition proof_stop_state `{FArgs} (proof_value : proof)
: Sc_rollup_repr.State_hash.t := Context.(P.proof_after) proof_value.
Definition name `{FArgs} : string := "wasm_2_0_0".
Definition parse_boot_sector `{FArgs} (s_value : string) : option string :=
Hex.to_string (Hex.Hex s_value).
Definition pp_boot_sector `{FArgs}
(fmt : Format.formatter) (s_value : string) : unit :=
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") s_value.
Definition tree `{FArgs} : Set := Context.(P.Tree).(Context.TREE.tree).
Inductive status `{FArgs} : Set :=
| Computing : status
| Waiting_for_input_message : status
| Waiting_for_reveal : Sc_rollup_PVM_sig.reveal → status.
Module State.
Definition state `{FArgs} : Set := tree.
Module Monad.
Definition t `{FArgs} (a : Set) : Set := state → state × a.
Definition _return `{FArgs} {A B : Set} (x_value : A) (state_value : B)
: B × A := (state_value, x_value).
Definition bind `{FArgs} {A B C D : Set}
(m_value : A → B × C) (f_value : C → B → D) (state_value : A)
: D :=
let '(state_value, res) := m_value state_value in
f_value res state_value.
Module Syntax.
Definition op_letstar `{FArgs} {A B C D : Set}
: (A → B × C) → (C → B → D) → A → D := bind.
End Syntax.
Definition run `{FArgs} {A B : Set} (m_value : A → B) (state_value : A)
: B := m_value state_value.
Definition get `{FArgs} {A : Set} (s_value : A) : A × A :=
(s_value, s_value).
Definition set `{FArgs} {A B : Set}
(s_value : A) (function_parameter : B) : A × unit :=
let '_ := function_parameter in
(s_value, tt).
Definition lift `{FArgs} {A B : Set} (m_value : A) (s_value : B)
: B × A := id (fun (r_value : A) ⇒ (s_value, r_value)) m_value.
End Monad.
End State.
Definition state `{FArgs} : Set := State.state.
Definition WASM_machine `{FArgs} := Make_backend Tree.
Definition pp `{FArgs} {A : Set} (_state : A)
: Format.formatter → unit → unit :=
fun (fmt : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.pp_print_string fmt "<wasm-state>".
Definition initial_state `{FArgs}
(empty : Context.(P.Tree).(Context.TREE.tree))
: Context.(P.Tree).(Context.TREE.tree) :=
let state_value :=
Tree.(Context.TREE.add) empty [ "wasm-version" ]
(Bytes.of_string "2.0.0") in
state_value.
Definition install_boot_sector `{FArgs}
(state_value : Context.(P.Tree).(Context.TREE.tree))
(boot_sector : string) : Context.(P.Tree).(Context.TREE.tree) :=
WASM_machine.(Wasm_2_0_0.S.install_boot_sector) boot_sector state_value.
Definition state_hash `{FArgs}
(state_value : Context.(P.Tree).(Context.TREE.tree))
: Sc_rollup_repr.State_hash.t :=
let context_hash := Tree.(Context.TREE.hash_value) state_value in
match Sc_rollup_repr.State_hash.context_hash_to_state_hash context_hash
with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end.
Definition result_of `{FArgs} {A : Set}
(m_value : State.Monad.t A) (state_value : State.state) : A :=
let '(_, v_value) := State.Monad.run m_value state_value in
v_value.
Definition state_of `{FArgs} {A : Set}
(m_value : State.Monad.t A) (state_value : State.state) : State.state :=
let '(s_value, _) := State.Monad.run m_value state_value in
s_value.
Definition get_tick_aux `{FArgs} : State.Monad.t Sc_rollup_tick_repr.t :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
(fun info_value ⇒
State.Monad._return
(Sc_rollup_tick_repr.of_z
info_value.(Wasm_2_0_0.info.current_tick)))).
Definition get_tick `{FArgs} : State.state → Sc_rollup_tick_repr.t :=
result_of get_tick_aux.
Definition get_status_aux `{FArgs} : State.Monad.t status :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
(fun info_value ⇒
State.Monad._return
match info_value.(Wasm_2_0_0.info.input_request) with
| Wasm_2_0_0.No_input_required ⇒ Computing
| Wasm_2_0_0.Input_required ⇒ Waiting_for_input_message
|
Wasm_2_0_0.Reveal_required
(Wasm_2_0_0.Reveal_raw_data hash_value) ⇒
match
Data_encoding.Binary.of_string_opt
Sc_rollup_PVM_sig.Reveal_hash.encoding
(Wasm_2_0_0.reveal_hash_to_string hash_value) with
| Some hash_value ⇒
Waiting_for_reveal
(Sc_rollup_PVM_sig.Reveal_raw_data hash_value)
| None ⇒
Waiting_for_reveal
(Sc_rollup_PVM_sig.Reveal_raw_data
Sc_rollup_PVM_sig.Reveal_hash.zero)
end
| Wasm_2_0_0.Reveal_required Wasm_2_0_0.Reveal_metadata ⇒
Waiting_for_reveal Sc_rollup_PVM_sig.Reveal_metadata
end)).
Definition get_last_message_read `{FArgs}
: State.Monad.t (option (M? Raw_level_repr.raw_level × Z.t)) :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
(fun info_value ⇒
State.Monad._return
match info_value.(Wasm_2_0_0.info.last_input_read) with
|
Some {|
Wasm_2_0_0.input.inbox_level := inbox_level;
Wasm_2_0_0.input.message_counter := message_counter
|} ⇒
let inbox_level :=
Raw_level_repr.of_int32_non_negative inbox_level in
Some (inbox_level, message_counter)
| _ ⇒ None
end)).
Definition is_input_state_aux `{FArgs} : State.Monad.t PS.input_request :=
State.Monad.Syntax.op_letstar get_status_aux
(fun status ⇒
match status with
| Waiting_for_input_message ⇒
State.Monad.Syntax.op_letstar get_last_message_read
(fun last_read ⇒
match last_read with
| Some (level, n_value) ⇒
match level with
| Pervasives.Ok lvl ⇒
State.Monad._return
(Sc_rollup_PVM_sig.First_after lvl n_value)
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert (State.Monad.t PS.input_request) false
end
| None ⇒ State.Monad._return Sc_rollup_PVM_sig.Initial
end)
| Computing ⇒ State.Monad._return Sc_rollup_PVM_sig.No_input_required
| Waiting_for_reveal reveal ⇒
State.Monad._return (Sc_rollup_PVM_sig.Needs_reveal reveal)
end).
Definition is_input_state `{FArgs} : State.state → PS.input_request :=
result_of is_input_state_aux.
Definition get_status `{FArgs} : State.state → status :=
result_of get_status_aux.
#[bypass_check(guard)]
Definition get_outbox `{FArgs}
(outbox_level : Raw_level_repr.raw_level)
(state_value : Context.(P.Tree).(Context.TREE.tree)) : list PS.output :=
let outbox_level_int32 :=
Internal_errors.ignore_errors
(Raw_level_repr.to_int32_non_negative outbox_level) in
let fix aux (outbox : list PS.output) (message_index : Z.t)
{struct message_index} : list PS.output :=
let output :=
{| Wasm_2_0_0.output.outbox_level := outbox_level_int32;
Wasm_2_0_0.output.message_index := message_index; |} in
let res := WASM_machine.(Wasm_2_0_0.S.get_output) output state_value in
match res with
| None ⇒ List.rev outbox
| Some msg ⇒
let serialized := Sc_rollup_outbox_message_repr.unsafe_of_string msg
in
match Sc_rollup_outbox_message_repr.deserialize serialized with
| Pervasives.Error _ ⇒ aux outbox (Z.succ message_index)
| Pervasives.Ok message ⇒
let output :=
{| Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
Sc_rollup_PVM_sig.output.message_index := message_index;
Sc_rollup_PVM_sig.output.message := message; |} in
aux (cons output outbox) (Z.succ message_index)
end
end in
aux nil Z.zero.
Definition set_input_state `{FArgs} (input : PS.input)
: State.Monad.t unit :=
match input with
| Sc_rollup_PVM_sig.Inbox_message input ⇒
let '{|
Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
Sc_rollup_PVM_sig.inbox_message.payload := payload
|} := input in
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
let inbox_level :=
match Raw_level_repr.to_int32_non_negative inbox_level with
| Pervasives.Ok lvl ⇒ lvl
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Bounded.Non_negative_int32.(Bounded.S.t) false
end in
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.set_input_step)
{| Wasm_2_0_0.input.inbox_level := inbox_level;
Wasm_2_0_0.input.message_counter := message_counter; |}
payload s_value)) (fun s_value ⇒ State.Monad.set s_value))
| Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Raw_data data) ⇒
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.reveal_step) (Bytes.of_string data)
s_value)) (fun s_value ⇒ State.Monad.set s_value))
| Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Metadata metadata) ⇒
let metadata_bytes :=
Data_encoding.Binary.to_bytes_exn None
Sc_rollup_metadata_repr.encoding metadata in
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.reveal_step) metadata_bytes s_value))
(fun s_value ⇒ State.Monad.set s_value))
| Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Dal_page _content_opt) ⇒
(* ❌ Assert instruction is not handled. *)
assert (State.Monad.t unit) false
end.
Definition set_input `{FArgs} (input : PS.input)
: State.state → State.state := state_of (set_input_state input).
Definition eval_step `{FArgs} : State.Monad.t unit :=
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
State.Monad.Syntax.op_letstar
(State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.compute_step) s_value))
(fun s_value ⇒ State.Monad.set s_value)).
Definition eval `{FArgs} (state_value : State.state) : State.state :=
state_of eval_step state_value.
Definition step_transition `{FArgs}
(input_given : option PS.input) (state_value : State.state)
: State.state × PS.input_request :=
let request := is_input_state state_value in
let state_value :=
match request with
| Sc_rollup_PVM_sig.No_input_required ⇒ eval state_value
| _ ⇒
match input_given with
| Some input ⇒ set_input input state_value
| None ⇒ state_value
end
end in
(state_value, request).
Definition verify_proof `{FArgs}
(input_given : option PS.input) (proof_value : proof)
: M? PS.input_request :=
let result_value :=
Context.(P.verify_proof) proof_value (step_transition input_given) in
match result_value with
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "WASM_proof_verification_failed" unit tt)
| Some (_state, request) ⇒ return? request
end.
Definition produce_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(input_given : option PS.input)
(state_value : Context.(P.Tree).(Context.TREE.tree)) : M? proof :=
let result_value :=
Context.(P.produce_proof) context_value state_value
(step_transition input_given) in
match result_value with
| Some (tree_proof, _requested) ⇒ return? tree_proof
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "WASM_proof_production_failed" unit tt)
end.
Definition verify_origination_proof `{FArgs}
(proof_value : proof) (boot_sector : string) : bool :=
let before := Context.(P.proof_before) proof_value in
if
Sc_rollup_repr.State_hash.op_ltgt before reference_initial_state_hash
then
false
else
let result_value :=
Context.(P.verify_proof) proof_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| None ⇒ false
| Some (_, _) ⇒ true
end.
Definition produce_origination_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t)) (boot_sector : string)
: M? proof :=
let state_value := initial_state (Tree.(Context.TREE.empty) context_value)
in
let result_value :=
Context.(P.produce_proof) context_value state_value
(fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
let state_value := install_boot_sector state_value boot_sector in
(state_value, tt)) in
match result_value with
| Some (tree_proof, _) ⇒ return? tree_proof
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "WASM_proof_production_failed" unit tt)
end.
Module output_proof.
Record record `{FArgs} : Set := Build {
output_proof : Context.(P.proof);
output_proof_state : hash;
output_proof_output : PS.output;
}.
Definition with_output_proof `{FArgs} output_proof (r : record) :=
Build _ _ _ _ output_proof r.(output_proof_state)
r.(output_proof_output).
Definition with_output_proof_state `{FArgs} output_proof_state
(r : record) :=
Build _ _ _ _ r.(output_proof) output_proof_state
r.(output_proof_output).
Definition with_output_proof_output `{FArgs} output_proof_output
(r : record) :=
Build _ _ _ _ r.(output_proof) r.(output_proof_state)
output_proof_output.
End output_proof.
Definition output_proof `{FArgs} := output_proof.record.
Definition output_proof_encoding `{FArgs}
: Data_encoding.encoding output_proof :=
Data_encoding.conv
(fun (function_parameter : output_proof) ⇒
let '{|
output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output
|} := function_parameter in
(output_proof, output_proof_state, output_proof_output))
(fun (function_parameter : Context.(P.proof) × hash × PS.output) ⇒
let '(output_proof, output_proof_state, output_proof_output) :=
function_parameter in
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}) None
(Data_encoding.obj3
(Data_encoding.req None None "output_proof" Context.(P.proof_encoding))
(Data_encoding.req None None "output_proof_state"
Sc_rollup_repr.State_hash.encoding)
(Data_encoding.req None None "output_proof_output" PS.output_encoding)).
Definition output_of_output_proof `{FArgs} (s_value : output_proof)
: PS.output := s_value.(output_proof.output_proof_output).
Definition state_of_output_proof `{FArgs} (s_value : output_proof) : hash :=
s_value.(output_proof.output_proof_state).
Definition has_output `{FArgs} (function_parameter : PS.output)
: State.Monad.t bool :=
let '{|
Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
Sc_rollup_PVM_sig.output.message_index := message_index;
Sc_rollup_PVM_sig.output.message := message
|} := function_parameter in
State.Monad.Syntax.op_letstar State.Monad.get
(fun s_value ⇒
let lvl :=
match Raw_level_repr.to_int32_non_negative outbox_level with
| Pervasives.Ok lvl ⇒ lvl
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Bounded.Non_negative_int32.(Bounded.S.t) false
end in
State.Monad.Syntax.op_letstar
(State.Monad.lift
(WASM_machine.(Wasm_2_0_0.S.get_output)
{| Wasm_2_0_0.output.outbox_level := lvl;
Wasm_2_0_0.output.message_index := message_index; |} s_value))
(fun result_value ⇒
let message_encoded :=
Data_encoding.Binary.to_string_exn None
Sc_rollup_outbox_message_repr.encoding message in
State.Monad._return
match result_value with
| Some result_value ⇒
Compare.String.(Compare.S.op_eq) result_value message_encoded
| None ⇒ false
end)).
Definition verify_output_proof `{FArgs} (p_value : output_proof) : bool :=
let transition :=
State.Monad.run (has_output p_value.(output_proof.output_proof_output))
in
let result_value :=
Context.(P.verify_proof) p_value.(output_proof.output_proof) transition
in
match result_value with
| None ⇒ false
| Some _ ⇒ true
end.
Definition produce_output_proof `{FArgs}
(context_value : Context.(P.Tree).(Context.TREE.t))
(state_value : Context.(P.Tree).(Context.TREE.tree))
(output_proof_output : PS.output)
: Pervasives.result output_proof Error_monad._error :=
let output_proof_state := state_hash state_value in
let result_value :=
Context.(P.produce_proof) context_value state_value
(State.Monad.run (has_output output_proof_output)) in
match result_value with
| Some (output_proof, true) ⇒
return?
{| output_proof.output_proof := output_proof;
output_proof.output_proof_state := output_proof_state;
output_proof.output_proof_output := output_proof_output; |}
| Some (_, false) ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "WASM_invalid_claim_about_outbox" unit tt)
| None ⇒
Error_monad.Lwt_result_syntax.fail
(Build_extensible "WASM_output_proof_production_failed" unit tt)
end.
(* Make *)
Definition functor `{FArgs} :=
{|
S.pp := pp;
S.proof_encoding := proof_encoding;
S.proof_start_state := proof_start_state;
S.proof_stop_state := proof_stop_state;
S.state_hash := state_hash;
S.initial_state := initial_state;
S.install_boot_sector := install_boot_sector;
S.is_input_state := is_input_state;
S.set_input := set_input;
S.eval := eval;
S.verify_proof := verify_proof;
S.produce_proof := produce_proof;
S.verify_origination_proof := verify_origination_proof;
S.produce_origination_proof := produce_origination_proof;
S.output_proof_encoding := output_proof_encoding;
S.output_of_output_proof := output_of_output_proof;
S.state_of_output_proof := state_of_output_proof;
S.verify_output_proof := verify_output_proof;
S.produce_output_proof := produce_output_proof;
S.name := name;
S.parse_boot_sector := parse_boot_sector;
S.pp_boot_sector := pp_boot_sector;
S.get_tick := get_tick;
S.get_status := get_status;
S.get_outbox := get_outbox
|}.
End Make.
Definition Make {Context_Tree_t Context_Tree_tree Context_proof : Set}
(Make_backend :
∀ {Tree_t Tree_tree : Set},
∀ (Tree :
Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
(value := bytes)), Wasm_2_0_0.S (tree := Tree.(Context.TREE.tree)))
(Context :
P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
(proof := Context_proof))
: S (state := Context.(P.Tree).(Context.TREE.tree))
(context := Context.(P.Tree).(Context.TREE.t))
(proof := Context.(P.proof)) (output_proof := _) (status := _) :=
let '_ := Make.Build_FArgs (@Make_backend) Context in
Make.functor.
Definition Protocol_implementation :=
Make (@Wasm_2_0_0.Make)
(let Tree :=
let mem := Context.Tree.(Context.TREE.mem) in
let mem_tree := Context.Tree.(Context.TREE.mem_tree) in
let find := Context.Tree.(Context.TREE.find) in
let find_tree := Context.Tree.(Context.TREE.find_tree) in
let list_value := Context.Tree.(Context.TREE.list_value) in
let length := Context.Tree.(Context.TREE.length) in
let add := Context.Tree.(Context.TREE.add) in
let add_tree := Context.Tree.(Context.TREE.add_tree) in
let remove := Context.Tree.(Context.TREE.remove) in
let fold {a : Set} := Context.Tree.(Context.TREE.fold) in
let config_value := Context.Tree.(Context.TREE.config_value) in
let empty := Context.Tree.(Context.TREE.empty) in
let is_empty := Context.Tree.(Context.TREE.is_empty) in
let kind_value := Context.Tree.(Context.TREE.kind_value) in
let to_value := Context.Tree.(Context.TREE.to_value) in
let of_value := Context.Tree.(Context.TREE.of_value) in
let hash_value := Context.Tree.(Context.TREE.hash_value) in
let equal := Context.Tree.(Context.TREE.equal) in
let clear := Context.Tree.(Context.TREE.clear) in
let tree : Set := Context.tree in
let t : Set := Context.t in
let key : Set := list string in
let value : Set := bytes in
{|
Context.TREE.mem := mem;
Context.TREE.mem_tree := mem_tree;
Context.TREE.find := find;
Context.TREE.find_tree := find_tree;
Context.TREE.list_value := list_value;
Context.TREE.length := length;
Context.TREE.add := add;
Context.TREE.add_tree := add_tree;
Context.TREE.remove := remove;
Context.TREE.fold _ := fold;
Context.TREE.config_value := config_value;
Context.TREE.empty := empty;
Context.TREE.is_empty := is_empty;
Context.TREE.kind_value := kind_value;
Context.TREE.to_value := to_value;
Context.TREE.of_value := of_value;
Context.TREE.hash_value := hash_value;
Context.TREE.equal := equal;
Context.TREE.clear := clear
|} in
let tree : Set := Context.tree in
let proof : Set := Context.Proof.t Context.Proof.tree in
let verify_proof {A : Set}
(p_value : Context.Proof.t Context.Proof.tree)
(f_value : Context.tree → Context.tree × A)
: option (Context.tree × A) :=
id Result.to_option (Context.verify_tree_proof p_value f_value) in
let produce_proof {A B C D : Set} (_context : A) (_state : B) (_f : C)
: option D :=
None in
let kinded_hash_to_state_hash
(function_parameter : Context.Proof.kinded_hash)
: M? Sc_rollup_repr.State_hash.t :=
match function_parameter with
| (Context.Proof.KValue hash_value | Context.Proof.KNode hash_value) ⇒
Sc_rollup_repr.State_hash.context_hash_to_state_hash hash_value
end in
let proof_before {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.before)
with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_after {A : Set} (proof_value : Context.Proof.t A)
: Sc_rollup_repr.State_hash.t :=
match kinded_hash_to_state_hash proof_value.(Context.Proof.t.after) with
| Pervasives.Ok sth ⇒ sth
| Pervasives.Error _ ⇒
(* ❌ Assert instruction is not handled. *)
assert Sc_rollup_repr.State_hash.t false
end in
let proof_encoding :=
Context.Proof_encoding.V2.Tree32.(Context.PROOF_ENCODING.tree_proof_encoding)
in
{|
P.Tree := Tree;
P.proof_encoding := proof_encoding;
P.proof_before := proof_before;
P.proof_after := proof_after;
P.verify_proof _ := verify_proof;
P.produce_proof _ := produce_proof
|}).
End V2_0_0.