🦏 Sc_rollup_operations.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_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_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_management_protocol.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_wasm.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_operations_diff.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Module execute_outbox_message_result.
Record record : Set := Build {
paid_storage_size_diff : Z.t;
operations : list Script_typed_ir.packed_internal_operation;
}.
Definition with_paid_storage_size_diff paid_storage_size_diff (r : record) :=
Build paid_storage_size_diff r.(operations).
Definition with_operations operations (r : record) :=
Build r.(paid_storage_size_diff) operations.
End execute_outbox_message_result.
Definition execute_outbox_message_result :=
execute_outbox_message_result.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_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_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_management_protocol.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_wasm.
Require TezosOfOCaml.Proto_alpha.Sc_rollups.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_operations_diff.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Module execute_outbox_message_result.
Record record : Set := Build {
paid_storage_size_diff : Z.t;
operations : list Script_typed_ir.packed_internal_operation;
}.
Definition with_paid_storage_size_diff paid_storage_size_diff (r : record) :=
Build paid_storage_size_diff r.(operations).
Definition with_operations operations (r : record) :=
Build r.(paid_storage_size_diff) operations.
End execute_outbox_message_result.
Definition execute_outbox_message_result :=
execute_outbox_message_result.record.
Init function; without side-effects in Coq
Definition init_module : unit :=
let description := "Invalid parameters type for rollup" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_parameters_type" "Invalid parameters type" description
(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") description))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_parameters_type" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_parameters_type" unit tt) in
let description := "Invalid last-cemented-commitment" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_last_cemented_commitment" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_last_cemented_commitment" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_last_cemented_commitment" unit tt)
in
let description := "Invalid output proof" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_output_proof" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_output_proof" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_output_proof" unit tt) in
let description := "Invalid outbox level" in
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_outbox_level" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_outbox_level" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_outbox_level" unit tt).
Module origination_result.
Record record : Set := Build {
address : Alpha_context.Sc_rollup.Address.t;
size : Z.t;
genesis_commitment_hash : Alpha_context.Sc_rollup.Commitment.Hash.t;
}.
Definition with_address address (r : record) :=
Build address r.(size) r.(genesis_commitment_hash).
Definition with_size size (r : record) :=
Build r.(address) size r.(genesis_commitment_hash).
Definition with_genesis_commitment_hash genesis_commitment_hash
(r : record) :=
Build r.(address) r.(size) genesis_commitment_hash.
End origination_result.
Definition origination_result := origination_result.record.
Definition origination_proof_of_string
(origination_proof : string) (kind_value : Alpha_context.Sc_rollup.Kind.t)
: M? Alpha_context.Sc_rollup.wrapped_proof :=
match kind_value with
| Alpha_context.Sc_rollup.Kind.Example_arith ⇒
let? proof_value :=
match
Data_encoding.Binary.of_string_opt
Alpha_context.Sc_rollup.ArithPVM.Protocol_implementation.(Sc_rollup_arith.S.proof_encoding)
origination_proof with
| Some x_value ⇒ return? x_value
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_proof_check" string
"invalid encoding for Arith origination proof")
end in
let 'PVM :=
existS (A := [Set ** Set ** Set]) _ [_, _, _]
(let Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include :=
Alpha_context.Sc_rollup.ArithPVM.Protocol_implementation in
let state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.state)
in
let pp :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.pp)
in
let context :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.context)
in
let hash :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.hash)
in
let proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof)
in
let proof_encoding :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof_encoding)
in
let proof_start_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof_start_state)
in
let proof_stop_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof_stop_state)
in
let state_hash :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.state_hash)
in
let initial_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.initial_state)
in
let install_boot_sector :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.install_boot_sector)
in
let is_input_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.is_input_state)
in
let set_input :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.set_input)
in
let eval :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.eval)
in
let verify_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.verify_proof)
in
let produce_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.produce_proof)
in
let verify_origination_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.verify_origination_proof)
in
let produce_origination_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.produce_origination_proof)
in
let output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.output_proof)
in
let output_proof_encoding :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.output_proof_encoding)
in
let output_of_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.output_of_output_proof)
in
let state_of_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.state_of_output_proof)
in
let verify_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.verify_output_proof)
in
let produce_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.produce_output_proof)
in
let name :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.name)
in
let parse_boot_sector :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.parse_boot_sector)
in
let pp_boot_sector :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.pp_boot_sector)
in
let get_tick :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_tick)
in
let status :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.status)
in
let get_status :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_status)
in
let get_outbox :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_outbox)
in
let instruction :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.instruction)
in
let equal_instruction :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.equal_instruction)
in
let pp_instruction :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.pp_instruction)
in
let get_parsing_result :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_parsing_result)
in
let get_code :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_code)
in
let get_stack :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_stack)
in
let get_var :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_var)
in
let get_evaluation_result :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_evaluation_result)
in
let get_is_stuck :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_is_stuck)
in
let proof_val := proof_value in
{|
Sc_rollups.PVM_with_proof.name := name;
Sc_rollups.PVM_with_proof.parse_boot_sector := parse_boot_sector;
Sc_rollups.PVM_with_proof.pp_boot_sector := pp_boot_sector;
Sc_rollups.PVM_with_proof.pp := pp;
Sc_rollups.PVM_with_proof.proof_encoding := proof_encoding;
Sc_rollups.PVM_with_proof.proof_start_state := proof_start_state;
Sc_rollups.PVM_with_proof.proof_stop_state := proof_stop_state;
Sc_rollups.PVM_with_proof.state_hash := state_hash;
Sc_rollups.PVM_with_proof.initial_state := initial_state;
Sc_rollups.PVM_with_proof.install_boot_sector := install_boot_sector;
Sc_rollups.PVM_with_proof.is_input_state := is_input_state;
Sc_rollups.PVM_with_proof.set_input := set_input;
Sc_rollups.PVM_with_proof.eval := eval;
Sc_rollups.PVM_with_proof.verify_proof := verify_proof;
Sc_rollups.PVM_with_proof.produce_proof := produce_proof;
Sc_rollups.PVM_with_proof.verify_origination_proof :=
verify_origination_proof;
Sc_rollups.PVM_with_proof.produce_origination_proof :=
produce_origination_proof;
Sc_rollups.PVM_with_proof.output_proof_encoding :=
output_proof_encoding;
Sc_rollups.PVM_with_proof.output_of_output_proof :=
output_of_output_proof;
Sc_rollups.PVM_with_proof.state_of_output_proof :=
state_of_output_proof;
Sc_rollups.PVM_with_proof.verify_output_proof := verify_output_proof;
Sc_rollups.PVM_with_proof.produce_output_proof := produce_output_proof;
Sc_rollups.PVM_with_proof.proof_val := proof_val
|}) in
let 'existS _ _ PVM := PVM in
return?
(Alpha_context.Sc_rollup.Arith_pvm_with_proof
(existS (A := [Set ** Set ** Set]) _ [_, _, _] PVM))
| Alpha_context.Sc_rollup.Kind.Wasm_2_0_0 ⇒
let? proof_value :=
match
Data_encoding.Binary.of_string_opt
Alpha_context.Sc_rollup.Wasm_2_0_0PVM.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)
origination_proof with
| Some x_value ⇒ return? x_value
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_proof_check" string
"invalid encoding for Wasm_2_0_0 origination proof")
end in
let 'PVM :=
existS (A := [Set ** Set ** Set]) _ [_, _, _]
(let
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include
:= Alpha_context.Sc_rollup.Wasm_2_0_0PVM.Protocol_implementation in
let state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.state)
in
let pp :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.pp)
in
let context :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.context)
in
let hash :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.hash)
in
let proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof)
in
let proof_encoding :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)
in
let proof_start_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof_start_state)
in
let proof_stop_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof_stop_state)
in
let state_hash :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.state_hash)
in
let initial_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.initial_state)
in
let install_boot_sector :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.install_boot_sector)
in
let is_input_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.is_input_state)
in
let set_input :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.set_input)
in
let eval :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.eval)
in
let verify_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.verify_proof)
in
let produce_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.produce_proof)
in
let verify_origination_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.verify_origination_proof)
in
let produce_origination_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.produce_origination_proof)
in
let output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.output_proof)
in
let output_proof_encoding :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.output_proof_encoding)
in
let output_of_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.output_of_output_proof)
in
let state_of_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.state_of_output_proof)
in
let verify_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.verify_output_proof)
in
let produce_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.produce_output_proof)
in
let name :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.name)
in
let parse_boot_sector :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.parse_boot_sector)
in
let pp_boot_sector :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.pp_boot_sector)
in
let get_tick :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.get_tick)
in
let status :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.status)
in
let get_status :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.get_status)
in
let get_outbox :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.get_outbox)
in
let proof_val := proof_value in
{|
Sc_rollups.PVM_with_proof.name := name;
Sc_rollups.PVM_with_proof.parse_boot_sector := parse_boot_sector;
Sc_rollups.PVM_with_proof.pp_boot_sector := pp_boot_sector;
Sc_rollups.PVM_with_proof.pp := pp;
Sc_rollups.PVM_with_proof.proof_encoding := proof_encoding;
Sc_rollups.PVM_with_proof.proof_start_state := proof_start_state;
Sc_rollups.PVM_with_proof.proof_stop_state := proof_stop_state;
Sc_rollups.PVM_with_proof.state_hash := state_hash;
Sc_rollups.PVM_with_proof.initial_state := initial_state;
Sc_rollups.PVM_with_proof.install_boot_sector := install_boot_sector;
Sc_rollups.PVM_with_proof.is_input_state := is_input_state;
Sc_rollups.PVM_with_proof.set_input := set_input;
Sc_rollups.PVM_with_proof.eval := eval;
Sc_rollups.PVM_with_proof.verify_proof := verify_proof;
Sc_rollups.PVM_with_proof.produce_proof := produce_proof;
Sc_rollups.PVM_with_proof.verify_origination_proof :=
verify_origination_proof;
Sc_rollups.PVM_with_proof.produce_origination_proof :=
produce_origination_proof;
Sc_rollups.PVM_with_proof.output_proof_encoding :=
output_proof_encoding;
Sc_rollups.PVM_with_proof.output_of_output_proof :=
output_of_output_proof;
Sc_rollups.PVM_with_proof.state_of_output_proof :=
state_of_output_proof;
Sc_rollups.PVM_with_proof.verify_output_proof := verify_output_proof;
Sc_rollups.PVM_with_proof.produce_output_proof := produce_output_proof;
Sc_rollups.PVM_with_proof.proof_val := proof_val
|}) in
let 'existS _ _ PVM := PVM in
return?
(Alpha_context.Sc_rollup.Wasm_2_0_0_pvm_with_proof
(existS (A := [Set ** Set ** Set]) _ [_, _, _] PVM))
end.
Definition continuation (ret : Set) : Set := unit → M? ret.
Reserved Notation "'validate_two_tys".
Fixpoint validate_ty {ret : Set}
(ty_value : Script_typed_ir.ty) (k_value : continuation ret) : M? ret :=
let validate_two_tys {ret} := 'validate_two_tys ret in
match ty_value with
| Script_typed_ir.Unit_t ⇒ k_value tt
| Script_typed_ir.Int_t ⇒ k_value tt
| Script_typed_ir.Nat_t ⇒ k_value tt
| Script_typed_ir.Signature_t ⇒ k_value tt
| Script_typed_ir.String_t ⇒ k_value tt
| Script_typed_ir.Bytes_t ⇒ k_value tt
| Script_typed_ir.Key_hash_t ⇒ k_value tt
| Script_typed_ir.Key_t ⇒ k_value tt
| Script_typed_ir.Timestamp_t ⇒ k_value tt
| Script_typed_ir.Address_t ⇒ k_value tt
| Script_typed_ir.Bls12_381_g1_t ⇒ k_value tt
| Script_typed_ir.Bls12_381_g2_t ⇒ k_value tt
| Script_typed_ir.Bls12_381_fr_t ⇒ k_value tt
| Script_typed_ir.Bool_t ⇒ k_value tt
| Script_typed_ir.Never_t ⇒ k_value tt
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value tt
| Script_typed_ir.Chain_id_t ⇒ k_value tt
| Script_typed_ir.Ticket_t ty_value _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.Set_t ty_value _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.Option_t ty_value _ _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.List_t ty_value _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.Pair_t ty1 ty2 _ _ ⇒ validate_two_tys ty1 ty2 k_value
| Script_typed_ir.Union_t ty1 ty2 _ _ ⇒ validate_two_tys ty1 ty2 k_value
| Script_typed_ir.Map_t key_ty val_ty _ ⇒
validate_two_tys key_ty val_ty k_value
| Script_typed_ir.Mutez_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Big_map_t _key_ty _val_ty _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Contract_t _ _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Sapling_transaction_t _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Sapling_transaction_deprecated_t _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Sapling_state_t _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Operation_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Chest_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Chest_key_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Lambda_t _ _ _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
end
where "'validate_two_tys" :=
(fun (ret : Set) ⇒ fun
(ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.ty)
(k_value : continuation ret) ⇒
validate_ty ty1
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
validate_ty ty2 k_value)).
Definition validate_two_tys {ret : Set} := 'validate_two_tys ret.
Definition validate_parameters_ty
(ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
: M? Alpha_context.context :=
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Sc_rollup_costs.is_valid_parameters_ty_cost
(Script_typed_ir.Type_size.to_int
(Script_typed_ir.ty_size parameters_ty))) in
Error_monad.Result_syntax.op_letplus
(validate_ty parameters_ty Error_monad.ok)
(fun function_parameter ⇒
let '_ := function_parameter in
ctxt).
Definition validate_untyped_parameters_ty
(ctxt : Alpha_context.context)
(parameters_ty : Micheline.canonical Alpha_context.Script.prim)
: M? Alpha_context.context :=
let?
'(Script_ir_translator.Ex_parameter_ty_and_entrypoints {|
Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.arg_type
:= arg_type;
Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.entrypoints
:= _
|}, ctxt) :=
Script_ir_translator.parse_parameter_ty_and_entrypoints ctxt false
(Micheline.root_value parameters_ty) in
validate_parameters_ty ctxt arg_type.
Definition check_origination_proof
(kind_value : Alpha_context.Sc_rollup.Kind.t) (boot_sector : string)
(origination_proof : Alpha_context.Sc_rollup.wrapped_proof)
: M? Alpha_context.Sc_rollup.State_hash.t :=
let PVM := Alpha_context.Sc_rollup.wrapped_proof_module origination_proof in
let 'existS _ _ PVM := PVM in
let kind' := Alpha_context.Sc_rollup.wrapped_proof_kind_exn origination_proof
in
let? '_ :=
Error_monad.fail_when
(Compare.String.(Compare.S.op_ltgt)
(Alpha_context.Sc_rollup.Kind.name_of kind_value)
(Alpha_context.Sc_rollup.Kind.name_of kind'))
(Build_extensible "Sc_rollup_proof_check" string "incorrect kind proof")
in
let is_valid :=
PVM.(Sc_rollups.PVM_with_proof.verify_origination_proof)
PVM.(Sc_rollups.PVM_with_proof.proof_val) boot_sector in
let? '_ :=
Error_monad.fail_when (Pervasives.not is_valid)
(Build_extensible "Sc_rollup_proof_check" string
"invalid origination proof") in
return?
(PVM.(Sc_rollups.PVM_with_proof.proof_stop_state)
PVM.(Sc_rollups.PVM_with_proof.proof_val)).
Definition originate
(ctxt : Alpha_context.context) (kind_value : Alpha_context.Sc_rollup.Kind.t)
(boot_sector : string) (origination_proof : string)
(parameters_ty : Alpha_context.Script.lazy_expr)
: M? (origination_result × Alpha_context.context) :=
let? ctxt :=
let? '(parameters_ty, ctxt) :=
Alpha_context.Script.force_decode_in_context
Alpha_context.Script.When_needed ctxt parameters_ty in
validate_untyped_parameters_ty ctxt parameters_ty in
let? origination_proof :=
origination_proof_of_string origination_proof kind_value in
let? genesis_hash :=
check_origination_proof kind_value boot_sector origination_proof in
let? genesis_commitment :=
Alpha_context.Sc_rollup.Commitment.genesis_commitment
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level)
genesis_hash in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Sc_rollup.originate ctxt kind_value parameters_ty
genesis_commitment)
(fun function_parameter ⇒
let '(address, size_value, genesis_commitment_hash, ctxt) :=
function_parameter in
({| origination_result.address := address;
origination_result.size := size_value;
origination_result.genesis_commitment_hash := genesis_commitment_hash;
|}, ctxt)).
Definition to_transaction_operation
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
(function_parameter : Sc_rollup_management_protocol.transaction)
: M? (Script_typed_ir.packed_internal_operation × Alpha_context.context) :=
let
'Sc_rollup_management_protocol.Transaction {|
Sc_rollup_management_protocol.transaction.Transaction.destination :=
destination;
Sc_rollup_management_protocol.transaction.Transaction.entrypoint :=
entrypoint;
Sc_rollup_management_protocol.transaction.Transaction.parameters_ty :=
parameters_ty;
Sc_rollup_management_protocol.transaction.Transaction.parameters :=
parameters;
Sc_rollup_management_protocol.transaction.Transaction.unparsed_parameters
:= unparsed_parameters
|} := function_parameter in
let? '(ctxt, nonce_value) := Alpha_context.fresh_internal_nonce ctxt in
let? ctxt := validate_parameters_ty ctxt parameters_ty in
let operation :=
Script_typed_ir.Transaction_to_smart_contract
{|
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
:= destination;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
:= Alpha_context.Tez.zero;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
:= entrypoint;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.location
:= Micheline.dummy_location;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters_ty
:= parameters_ty;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters
:= parameters;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
:= unparsed_parameters; |} in
return?
((Script_typed_ir.Internal_operation
{|
Script_typed_ir.internal_operation.source :=
Contract_repr.Implicit source;
Script_typed_ir.internal_operation.operation := operation;
Script_typed_ir.internal_operation.nonce := nonce_value; |}), ctxt).
Definition transfer_ticket_token
(ctxt : Alpha_context.context)
(source_destination : Alpha_context.Destination.t)
(target_destination : Alpha_context.Destination.t) (amount : Z.t)
(ticket_token : Ticket_token.ex_token) : M? (Z.t × Alpha_context.context) :=
let? '(source_key_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt source_destination ticket_token in
let? '(target_key_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt target_destination ticket_token in
let? '(source_storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_balance ctxt source_key_hash
(Z.neg amount) in
let? '(target_storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_balance ctxt target_key_hash amount in
let? '(storage_diff_to_pay, ctxt) :=
Alpha_context.Ticket_balance.adjust_storage_space ctxt
(source_storage_diff +Z target_storage_diff) in
return? (storage_diff_to_pay, ctxt).
Definition transfer_ticket_tokens
(ctxt : Alpha_context.context)
(source_destination : Alpha_context.Destination.t) (acc_storage_diff : Z.t)
(function_parameter : Ticket_operations_diff.ticket_token_diff)
: M? (Z.t × Alpha_context.context) :=
let '{|
Ticket_operations_diff.ticket_token_diff.ticket_token := ticket_token;
Ticket_operations_diff.ticket_token_diff.total_amount := _;
Ticket_operations_diff.ticket_token_diff.destinations := destinations
|} := function_parameter in
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(acc_storage_diff, ctxt) := function_parameter in
fun (function_parameter :
Alpha_context.Destination.t × Script_typed_ir.ticket_amount) ⇒
let '(target_destination, amount) := function_parameter in
let? '(storage_diff, ctxt) :=
transfer_ticket_token ctxt source_destination target_destination
(Script_int.to_zint amount) ticket_token in
return? ((acc_storage_diff +Z storage_diff), ctxt))
(acc_storage_diff, ctxt) destinations.
Axiom validate_and_decode_output_proof :
Alpha_context.context → Alpha_context.Sc_rollup.Commitment.Hash.t →
Alpha_context.Sc_rollup.t → string →
M? (Alpha_context.Sc_rollup.output × Alpha_context.context).
Definition validate_outbox_level
(ctxt : Alpha_context.context)
(outbox_level : Alpha_context.Raw_level.raw_level)
(lcc_level : Alpha_context.Raw_level.raw_level) : M? unit :=
let max_active_levels :=
Int32.to_int
(Alpha_context.Constants.sc_rollup_max_active_outbox_levels ctxt) in
let outbox_level_is_active :=
let min_allowed_level :=
(Alpha_context.Raw_level.to_int32 lcc_level) -i32
(Int32.of_int max_active_levels) in
min_allowed_level <i32 (Alpha_context.Raw_level.to_int32 outbox_level) in
Error_monad.fail_unless
((Alpha_context.Raw_level.op_lteq outbox_level lcc_level) &&
outbox_level_is_active)
(Build_extensible "Sc_rollup_invalid_outbox_level" unit tt).
Definition execute_outbox_message_aux {A : Set}
(ctxt : Alpha_context.context)
(validate_and_decode_output_proof :
Alpha_context.context → Alpha_context.Sc_rollup.Commitment.Hash.t →
Alpha_context.Sc_rollup.t → A →
M? (Alpha_context.Sc_rollup.output × Alpha_context.context))
(rollup : Alpha_context.Sc_rollup.t)
(cemented_commitment : Alpha_context.Sc_rollup.Commitment.Hash.t)
(source : Alpha_context.public_key_hash) (output_proof : A)
: M? (execute_outbox_message_result × Alpha_context.context) :=
let? '(lcc_hash, lcc_level, ctxt) :=
Alpha_context.Sc_rollup.Commitment.last_cemented_commitment_hash_with_level
ctxt rollup in
let? '_ :=
Error_monad.fail_unless
(Alpha_context.Sc_rollup.Commitment.Hash.op_eq lcc_hash
cemented_commitment)
(Build_extensible "Sc_rollup_invalid_last_cemented_commitment" unit tt) in
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
|}, ctxt) :=
validate_and_decode_output_proof ctxt lcc_hash rollup output_proof in
let? '_ := validate_outbox_level ctxt outbox_level lcc_level in
let?
'(Sc_rollup_management_protocol.Atomic_transaction_batch {|
Sc_rollup_management_protocol.atomic_transaction_batch.transactions :=
transactions
|}, ctxt) :=
Sc_rollup_management_protocol.outbox_message_of_outbox_message_repr ctxt
message in
let? '(ctxt, operations) :=
List.fold_left_map_e
(fun (ctxt : Alpha_context.context) ⇒
fun (transaction : Sc_rollup_management_protocol.transaction) ⇒
Error_monad.Result_syntax.op_letplus
(to_transaction_operation ctxt source transaction)
(fun function_parameter ⇒
let '(op, ctxt) := function_parameter in
(ctxt, op))) ctxt transactions in
let? '(applied_msg_size_diff, ctxt) :=
Alpha_context.Sc_rollup.Outbox.record_applied_message ctxt rollup
outbox_level (Z.to_int message_index) in
let paid_storage_size_diff := Z.max Z.zero applied_msg_size_diff in
let? '(ticket_token_diffs, ctxt) :=
Ticket_operations_diff.ticket_diffs_of_operations ctxt operations in
let? '(paid_storage_size_diff, ctxt) :=
let source_destination := Alpha_context.Destination.Sc_rollup rollup in
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(acc_storage_diff, ctxt) := function_parameter in
fun (ticket_token_diff : Ticket_operations_diff.ticket_token_diff) ⇒
transfer_ticket_tokens ctxt source_destination acc_storage_diff
ticket_token_diff) (paid_storage_size_diff, ctxt) ticket_token_diffs
in
return?
({|
execute_outbox_message_result.paid_storage_size_diff :=
paid_storage_size_diff;
execute_outbox_message_result.operations := operations; |}, ctxt).
Definition execute_outbox_message (ctxt : Alpha_context.context)
: Alpha_context.Sc_rollup.t → Alpha_context.Sc_rollup.Commitment.Hash.t →
Alpha_context.public_key_hash → string →
M? (execute_outbox_message_result × Alpha_context.context) :=
execute_outbox_message_aux ctxt validate_and_decode_output_proof.
let description := "Invalid parameters type for rollup" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_parameters_type" "Invalid parameters type" description
(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") description))
Data_encoding.unit_value
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_parameters_type" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_parameters_type" unit tt) in
let description := "Invalid last-cemented-commitment" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_last_cemented_commitment" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_last_cemented_commitment" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_last_cemented_commitment" unit tt)
in
let description := "Invalid output proof" in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_output_proof" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_output_proof" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_output_proof" unit tt) in
let description := "Invalid outbox level" in
Error_monad.register_error_kind Error_monad.Permanent
"Sc_rollup_invalid_outbox_level" description description
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s") description))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Sc_rollup_invalid_outbox_level" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Sc_rollup_invalid_outbox_level" unit tt).
Module origination_result.
Record record : Set := Build {
address : Alpha_context.Sc_rollup.Address.t;
size : Z.t;
genesis_commitment_hash : Alpha_context.Sc_rollup.Commitment.Hash.t;
}.
Definition with_address address (r : record) :=
Build address r.(size) r.(genesis_commitment_hash).
Definition with_size size (r : record) :=
Build r.(address) size r.(genesis_commitment_hash).
Definition with_genesis_commitment_hash genesis_commitment_hash
(r : record) :=
Build r.(address) r.(size) genesis_commitment_hash.
End origination_result.
Definition origination_result := origination_result.record.
Definition origination_proof_of_string
(origination_proof : string) (kind_value : Alpha_context.Sc_rollup.Kind.t)
: M? Alpha_context.Sc_rollup.wrapped_proof :=
match kind_value with
| Alpha_context.Sc_rollup.Kind.Example_arith ⇒
let? proof_value :=
match
Data_encoding.Binary.of_string_opt
Alpha_context.Sc_rollup.ArithPVM.Protocol_implementation.(Sc_rollup_arith.S.proof_encoding)
origination_proof with
| Some x_value ⇒ return? x_value
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_proof_check" string
"invalid encoding for Arith origination proof")
end in
let 'PVM :=
existS (A := [Set ** Set ** Set]) _ [_, _, _]
(let Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include :=
Alpha_context.Sc_rollup.ArithPVM.Protocol_implementation in
let state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.state)
in
let pp :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.pp)
in
let context :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.context)
in
let hash :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.hash)
in
let proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof)
in
let proof_encoding :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof_encoding)
in
let proof_start_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof_start_state)
in
let proof_stop_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.proof_stop_state)
in
let state_hash :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.state_hash)
in
let initial_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.initial_state)
in
let install_boot_sector :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.install_boot_sector)
in
let is_input_state :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.is_input_state)
in
let set_input :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.set_input)
in
let eval :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.eval)
in
let verify_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.verify_proof)
in
let produce_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.produce_proof)
in
let verify_origination_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.verify_origination_proof)
in
let produce_origination_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.produce_origination_proof)
in
let output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.output_proof)
in
let output_proof_encoding :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.output_proof_encoding)
in
let output_of_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.output_of_output_proof)
in
let state_of_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.state_of_output_proof)
in
let verify_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.verify_output_proof)
in
let produce_output_proof :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.produce_output_proof)
in
let name :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.name)
in
let parse_boot_sector :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.parse_boot_sector)
in
let pp_boot_sector :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.pp_boot_sector)
in
let get_tick :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_tick)
in
let status :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.status)
in
let get_status :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_status)
in
let get_outbox :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_outbox)
in
let instruction :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.instruction)
in
let equal_instruction :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.equal_instruction)
in
let pp_instruction :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.pp_instruction)
in
let get_parsing_result :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_parsing_result)
in
let get_code :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_code)
in
let get_stack :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_stack)
in
let get_var :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_var)
in
let get_evaluation_result :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_evaluation_result)
in
let get_is_stuck :=
Alpha_context_Sc_rollup_ArithPVM_Protocol_implementation_include.(Sc_rollup_arith.S.get_is_stuck)
in
let proof_val := proof_value in
{|
Sc_rollups.PVM_with_proof.name := name;
Sc_rollups.PVM_with_proof.parse_boot_sector := parse_boot_sector;
Sc_rollups.PVM_with_proof.pp_boot_sector := pp_boot_sector;
Sc_rollups.PVM_with_proof.pp := pp;
Sc_rollups.PVM_with_proof.proof_encoding := proof_encoding;
Sc_rollups.PVM_with_proof.proof_start_state := proof_start_state;
Sc_rollups.PVM_with_proof.proof_stop_state := proof_stop_state;
Sc_rollups.PVM_with_proof.state_hash := state_hash;
Sc_rollups.PVM_with_proof.initial_state := initial_state;
Sc_rollups.PVM_with_proof.install_boot_sector := install_boot_sector;
Sc_rollups.PVM_with_proof.is_input_state := is_input_state;
Sc_rollups.PVM_with_proof.set_input := set_input;
Sc_rollups.PVM_with_proof.eval := eval;
Sc_rollups.PVM_with_proof.verify_proof := verify_proof;
Sc_rollups.PVM_with_proof.produce_proof := produce_proof;
Sc_rollups.PVM_with_proof.verify_origination_proof :=
verify_origination_proof;
Sc_rollups.PVM_with_proof.produce_origination_proof :=
produce_origination_proof;
Sc_rollups.PVM_with_proof.output_proof_encoding :=
output_proof_encoding;
Sc_rollups.PVM_with_proof.output_of_output_proof :=
output_of_output_proof;
Sc_rollups.PVM_with_proof.state_of_output_proof :=
state_of_output_proof;
Sc_rollups.PVM_with_proof.verify_output_proof := verify_output_proof;
Sc_rollups.PVM_with_proof.produce_output_proof := produce_output_proof;
Sc_rollups.PVM_with_proof.proof_val := proof_val
|}) in
let 'existS _ _ PVM := PVM in
return?
(Alpha_context.Sc_rollup.Arith_pvm_with_proof
(existS (A := [Set ** Set ** Set]) _ [_, _, _] PVM))
| Alpha_context.Sc_rollup.Kind.Wasm_2_0_0 ⇒
let? proof_value :=
match
Data_encoding.Binary.of_string_opt
Alpha_context.Sc_rollup.Wasm_2_0_0PVM.Protocol_implementation.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)
origination_proof with
| Some x_value ⇒ return? x_value
| None ⇒
Error_monad.Lwt_result_syntax.tzfail
(Build_extensible "Sc_rollup_proof_check" string
"invalid encoding for Wasm_2_0_0 origination proof")
end in
let 'PVM :=
existS (A := [Set ** Set ** Set]) _ [_, _, _]
(let
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include
:= Alpha_context.Sc_rollup.Wasm_2_0_0PVM.Protocol_implementation in
let state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.state)
in
let pp :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.pp)
in
let context :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.context)
in
let hash :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.hash)
in
let proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof)
in
let proof_encoding :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof_encoding)
in
let proof_start_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof_start_state)
in
let proof_stop_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.proof_stop_state)
in
let state_hash :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.state_hash)
in
let initial_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.initial_state)
in
let install_boot_sector :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.install_boot_sector)
in
let is_input_state :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.is_input_state)
in
let set_input :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.set_input)
in
let eval :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.eval)
in
let verify_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.verify_proof)
in
let produce_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.produce_proof)
in
let verify_origination_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.verify_origination_proof)
in
let produce_origination_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.produce_origination_proof)
in
let output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.output_proof)
in
let output_proof_encoding :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.output_proof_encoding)
in
let output_of_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.output_of_output_proof)
in
let state_of_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.state_of_output_proof)
in
let verify_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.verify_output_proof)
in
let produce_output_proof :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.produce_output_proof)
in
let name :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.name)
in
let parse_boot_sector :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.parse_boot_sector)
in
let pp_boot_sector :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.pp_boot_sector)
in
let get_tick :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.get_tick)
in
let status :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.status)
in
let get_status :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.get_status)
in
let get_outbox :=
Alpha_context_Sc_rollup_Wasm_2_0_0PVM_Protocol_implementation_include.(Sc_rollup_wasm.V2_0_0.S.get_outbox)
in
let proof_val := proof_value in
{|
Sc_rollups.PVM_with_proof.name := name;
Sc_rollups.PVM_with_proof.parse_boot_sector := parse_boot_sector;
Sc_rollups.PVM_with_proof.pp_boot_sector := pp_boot_sector;
Sc_rollups.PVM_with_proof.pp := pp;
Sc_rollups.PVM_with_proof.proof_encoding := proof_encoding;
Sc_rollups.PVM_with_proof.proof_start_state := proof_start_state;
Sc_rollups.PVM_with_proof.proof_stop_state := proof_stop_state;
Sc_rollups.PVM_with_proof.state_hash := state_hash;
Sc_rollups.PVM_with_proof.initial_state := initial_state;
Sc_rollups.PVM_with_proof.install_boot_sector := install_boot_sector;
Sc_rollups.PVM_with_proof.is_input_state := is_input_state;
Sc_rollups.PVM_with_proof.set_input := set_input;
Sc_rollups.PVM_with_proof.eval := eval;
Sc_rollups.PVM_with_proof.verify_proof := verify_proof;
Sc_rollups.PVM_with_proof.produce_proof := produce_proof;
Sc_rollups.PVM_with_proof.verify_origination_proof :=
verify_origination_proof;
Sc_rollups.PVM_with_proof.produce_origination_proof :=
produce_origination_proof;
Sc_rollups.PVM_with_proof.output_proof_encoding :=
output_proof_encoding;
Sc_rollups.PVM_with_proof.output_of_output_proof :=
output_of_output_proof;
Sc_rollups.PVM_with_proof.state_of_output_proof :=
state_of_output_proof;
Sc_rollups.PVM_with_proof.verify_output_proof := verify_output_proof;
Sc_rollups.PVM_with_proof.produce_output_proof := produce_output_proof;
Sc_rollups.PVM_with_proof.proof_val := proof_val
|}) in
let 'existS _ _ PVM := PVM in
return?
(Alpha_context.Sc_rollup.Wasm_2_0_0_pvm_with_proof
(existS (A := [Set ** Set ** Set]) _ [_, _, _] PVM))
end.
Definition continuation (ret : Set) : Set := unit → M? ret.
Reserved Notation "'validate_two_tys".
Fixpoint validate_ty {ret : Set}
(ty_value : Script_typed_ir.ty) (k_value : continuation ret) : M? ret :=
let validate_two_tys {ret} := 'validate_two_tys ret in
match ty_value with
| Script_typed_ir.Unit_t ⇒ k_value tt
| Script_typed_ir.Int_t ⇒ k_value tt
| Script_typed_ir.Nat_t ⇒ k_value tt
| Script_typed_ir.Signature_t ⇒ k_value tt
| Script_typed_ir.String_t ⇒ k_value tt
| Script_typed_ir.Bytes_t ⇒ k_value tt
| Script_typed_ir.Key_hash_t ⇒ k_value tt
| Script_typed_ir.Key_t ⇒ k_value tt
| Script_typed_ir.Timestamp_t ⇒ k_value tt
| Script_typed_ir.Address_t ⇒ k_value tt
| Script_typed_ir.Bls12_381_g1_t ⇒ k_value tt
| Script_typed_ir.Bls12_381_g2_t ⇒ k_value tt
| Script_typed_ir.Bls12_381_fr_t ⇒ k_value tt
| Script_typed_ir.Bool_t ⇒ k_value tt
| Script_typed_ir.Never_t ⇒ k_value tt
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value tt
| Script_typed_ir.Chain_id_t ⇒ k_value tt
| Script_typed_ir.Ticket_t ty_value _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.Set_t ty_value _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.Option_t ty_value _ _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.List_t ty_value _ ⇒ validate_ty ty_value k_value
| Script_typed_ir.Pair_t ty1 ty2 _ _ ⇒ validate_two_tys ty1 ty2 k_value
| Script_typed_ir.Union_t ty1 ty2 _ _ ⇒ validate_two_tys ty1 ty2 k_value
| Script_typed_ir.Map_t key_ty val_ty _ ⇒
validate_two_tys key_ty val_ty k_value
| Script_typed_ir.Mutez_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Big_map_t _key_ty _val_ty _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Contract_t _ _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Sapling_transaction_t _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Sapling_transaction_deprecated_t _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Sapling_state_t _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Operation_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Chest_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Chest_key_t ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
| Script_typed_ir.Lambda_t _ _ _ ⇒
Error_monad.error_value
(Build_extensible "Sc_rollup_invalid_parameters_type" unit tt)
end
where "'validate_two_tys" :=
(fun (ret : Set) ⇒ fun
(ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.ty)
(k_value : continuation ret) ⇒
validate_ty ty1
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
validate_ty ty2 k_value)).
Definition validate_two_tys {ret : Set} := 'validate_two_tys ret.
Definition validate_parameters_ty
(ctxt : Alpha_context.context) (parameters_ty : Script_typed_ir.ty)
: M? Alpha_context.context :=
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Sc_rollup_costs.is_valid_parameters_ty_cost
(Script_typed_ir.Type_size.to_int
(Script_typed_ir.ty_size parameters_ty))) in
Error_monad.Result_syntax.op_letplus
(validate_ty parameters_ty Error_monad.ok)
(fun function_parameter ⇒
let '_ := function_parameter in
ctxt).
Definition validate_untyped_parameters_ty
(ctxt : Alpha_context.context)
(parameters_ty : Micheline.canonical Alpha_context.Script.prim)
: M? Alpha_context.context :=
let?
'(Script_ir_translator.Ex_parameter_ty_and_entrypoints {|
Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.arg_type
:= arg_type;
Script_ir_translator.ex_parameter_ty_and_entrypoints.Ex_parameter_ty_and_entrypoints.entrypoints
:= _
|}, ctxt) :=
Script_ir_translator.parse_parameter_ty_and_entrypoints ctxt false
(Micheline.root_value parameters_ty) in
validate_parameters_ty ctxt arg_type.
Definition check_origination_proof
(kind_value : Alpha_context.Sc_rollup.Kind.t) (boot_sector : string)
(origination_proof : Alpha_context.Sc_rollup.wrapped_proof)
: M? Alpha_context.Sc_rollup.State_hash.t :=
let PVM := Alpha_context.Sc_rollup.wrapped_proof_module origination_proof in
let 'existS _ _ PVM := PVM in
let kind' := Alpha_context.Sc_rollup.wrapped_proof_kind_exn origination_proof
in
let? '_ :=
Error_monad.fail_when
(Compare.String.(Compare.S.op_ltgt)
(Alpha_context.Sc_rollup.Kind.name_of kind_value)
(Alpha_context.Sc_rollup.Kind.name_of kind'))
(Build_extensible "Sc_rollup_proof_check" string "incorrect kind proof")
in
let is_valid :=
PVM.(Sc_rollups.PVM_with_proof.verify_origination_proof)
PVM.(Sc_rollups.PVM_with_proof.proof_val) boot_sector in
let? '_ :=
Error_monad.fail_when (Pervasives.not is_valid)
(Build_extensible "Sc_rollup_proof_check" string
"invalid origination proof") in
return?
(PVM.(Sc_rollups.PVM_with_proof.proof_stop_state)
PVM.(Sc_rollups.PVM_with_proof.proof_val)).
Definition originate
(ctxt : Alpha_context.context) (kind_value : Alpha_context.Sc_rollup.Kind.t)
(boot_sector : string) (origination_proof : string)
(parameters_ty : Alpha_context.Script.lazy_expr)
: M? (origination_result × Alpha_context.context) :=
let? ctxt :=
let? '(parameters_ty, ctxt) :=
Alpha_context.Script.force_decode_in_context
Alpha_context.Script.When_needed ctxt parameters_ty in
validate_untyped_parameters_ty ctxt parameters_ty in
let? origination_proof :=
origination_proof_of_string origination_proof kind_value in
let? genesis_hash :=
check_origination_proof kind_value boot_sector origination_proof in
let? genesis_commitment :=
Alpha_context.Sc_rollup.Commitment.genesis_commitment
(Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level)
genesis_hash in
Error_monad.Lwt_result_syntax.op_letplus
(Alpha_context.Sc_rollup.originate ctxt kind_value parameters_ty
genesis_commitment)
(fun function_parameter ⇒
let '(address, size_value, genesis_commitment_hash, ctxt) :=
function_parameter in
({| origination_result.address := address;
origination_result.size := size_value;
origination_result.genesis_commitment_hash := genesis_commitment_hash;
|}, ctxt)).
Definition to_transaction_operation
(ctxt : Alpha_context.context) (source : Alpha_context.public_key_hash)
(function_parameter : Sc_rollup_management_protocol.transaction)
: M? (Script_typed_ir.packed_internal_operation × Alpha_context.context) :=
let
'Sc_rollup_management_protocol.Transaction {|
Sc_rollup_management_protocol.transaction.Transaction.destination :=
destination;
Sc_rollup_management_protocol.transaction.Transaction.entrypoint :=
entrypoint;
Sc_rollup_management_protocol.transaction.Transaction.parameters_ty :=
parameters_ty;
Sc_rollup_management_protocol.transaction.Transaction.parameters :=
parameters;
Sc_rollup_management_protocol.transaction.Transaction.unparsed_parameters
:= unparsed_parameters
|} := function_parameter in
let? '(ctxt, nonce_value) := Alpha_context.fresh_internal_nonce ctxt in
let? ctxt := validate_parameters_ty ctxt parameters_ty in
let operation :=
Script_typed_ir.Transaction_to_smart_contract
{|
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
:= destination;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
:= Alpha_context.Tez.zero;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
:= entrypoint;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.location
:= Micheline.dummy_location;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters_ty
:= parameters_ty;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters
:= parameters;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
:= unparsed_parameters; |} in
return?
((Script_typed_ir.Internal_operation
{|
Script_typed_ir.internal_operation.source :=
Contract_repr.Implicit source;
Script_typed_ir.internal_operation.operation := operation;
Script_typed_ir.internal_operation.nonce := nonce_value; |}), ctxt).
Definition transfer_ticket_token
(ctxt : Alpha_context.context)
(source_destination : Alpha_context.Destination.t)
(target_destination : Alpha_context.Destination.t) (amount : Z.t)
(ticket_token : Ticket_token.ex_token) : M? (Z.t × Alpha_context.context) :=
let? '(source_key_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt source_destination ticket_token in
let? '(target_key_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt target_destination ticket_token in
let? '(source_storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_balance ctxt source_key_hash
(Z.neg amount) in
let? '(target_storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_balance ctxt target_key_hash amount in
let? '(storage_diff_to_pay, ctxt) :=
Alpha_context.Ticket_balance.adjust_storage_space ctxt
(source_storage_diff +Z target_storage_diff) in
return? (storage_diff_to_pay, ctxt).
Definition transfer_ticket_tokens
(ctxt : Alpha_context.context)
(source_destination : Alpha_context.Destination.t) (acc_storage_diff : Z.t)
(function_parameter : Ticket_operations_diff.ticket_token_diff)
: M? (Z.t × Alpha_context.context) :=
let '{|
Ticket_operations_diff.ticket_token_diff.ticket_token := ticket_token;
Ticket_operations_diff.ticket_token_diff.total_amount := _;
Ticket_operations_diff.ticket_token_diff.destinations := destinations
|} := function_parameter in
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(acc_storage_diff, ctxt) := function_parameter in
fun (function_parameter :
Alpha_context.Destination.t × Script_typed_ir.ticket_amount) ⇒
let '(target_destination, amount) := function_parameter in
let? '(storage_diff, ctxt) :=
transfer_ticket_token ctxt source_destination target_destination
(Script_int.to_zint amount) ticket_token in
return? ((acc_storage_diff +Z storage_diff), ctxt))
(acc_storage_diff, ctxt) destinations.
Axiom validate_and_decode_output_proof :
Alpha_context.context → Alpha_context.Sc_rollup.Commitment.Hash.t →
Alpha_context.Sc_rollup.t → string →
M? (Alpha_context.Sc_rollup.output × Alpha_context.context).
Definition validate_outbox_level
(ctxt : Alpha_context.context)
(outbox_level : Alpha_context.Raw_level.raw_level)
(lcc_level : Alpha_context.Raw_level.raw_level) : M? unit :=
let max_active_levels :=
Int32.to_int
(Alpha_context.Constants.sc_rollup_max_active_outbox_levels ctxt) in
let outbox_level_is_active :=
let min_allowed_level :=
(Alpha_context.Raw_level.to_int32 lcc_level) -i32
(Int32.of_int max_active_levels) in
min_allowed_level <i32 (Alpha_context.Raw_level.to_int32 outbox_level) in
Error_monad.fail_unless
((Alpha_context.Raw_level.op_lteq outbox_level lcc_level) &&
outbox_level_is_active)
(Build_extensible "Sc_rollup_invalid_outbox_level" unit tt).
Definition execute_outbox_message_aux {A : Set}
(ctxt : Alpha_context.context)
(validate_and_decode_output_proof :
Alpha_context.context → Alpha_context.Sc_rollup.Commitment.Hash.t →
Alpha_context.Sc_rollup.t → A →
M? (Alpha_context.Sc_rollup.output × Alpha_context.context))
(rollup : Alpha_context.Sc_rollup.t)
(cemented_commitment : Alpha_context.Sc_rollup.Commitment.Hash.t)
(source : Alpha_context.public_key_hash) (output_proof : A)
: M? (execute_outbox_message_result × Alpha_context.context) :=
let? '(lcc_hash, lcc_level, ctxt) :=
Alpha_context.Sc_rollup.Commitment.last_cemented_commitment_hash_with_level
ctxt rollup in
let? '_ :=
Error_monad.fail_unless
(Alpha_context.Sc_rollup.Commitment.Hash.op_eq lcc_hash
cemented_commitment)
(Build_extensible "Sc_rollup_invalid_last_cemented_commitment" unit tt) in
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
|}, ctxt) :=
validate_and_decode_output_proof ctxt lcc_hash rollup output_proof in
let? '_ := validate_outbox_level ctxt outbox_level lcc_level in
let?
'(Sc_rollup_management_protocol.Atomic_transaction_batch {|
Sc_rollup_management_protocol.atomic_transaction_batch.transactions :=
transactions
|}, ctxt) :=
Sc_rollup_management_protocol.outbox_message_of_outbox_message_repr ctxt
message in
let? '(ctxt, operations) :=
List.fold_left_map_e
(fun (ctxt : Alpha_context.context) ⇒
fun (transaction : Sc_rollup_management_protocol.transaction) ⇒
Error_monad.Result_syntax.op_letplus
(to_transaction_operation ctxt source transaction)
(fun function_parameter ⇒
let '(op, ctxt) := function_parameter in
(ctxt, op))) ctxt transactions in
let? '(applied_msg_size_diff, ctxt) :=
Alpha_context.Sc_rollup.Outbox.record_applied_message ctxt rollup
outbox_level (Z.to_int message_index) in
let paid_storage_size_diff := Z.max Z.zero applied_msg_size_diff in
let? '(ticket_token_diffs, ctxt) :=
Ticket_operations_diff.ticket_diffs_of_operations ctxt operations in
let? '(paid_storage_size_diff, ctxt) :=
let source_destination := Alpha_context.Destination.Sc_rollup rollup in
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(acc_storage_diff, ctxt) := function_parameter in
fun (ticket_token_diff : Ticket_operations_diff.ticket_token_diff) ⇒
transfer_ticket_tokens ctxt source_destination acc_storage_diff
ticket_token_diff) (paid_storage_size_diff, ctxt) ticket_token_diffs
in
return?
({|
execute_outbox_message_result.paid_storage_size_diff :=
paid_storage_size_diff;
execute_outbox_message_result.operations := operations; |}, ctxt).
Definition execute_outbox_message (ctxt : Alpha_context.context)
: Alpha_context.Sc_rollup.t → Alpha_context.Sc_rollup.Commitment.Hash.t →
Alpha_context.public_key_hash → string →
M? (execute_outbox_message_result × Alpha_context.context) :=
execute_outbox_message_aux ctxt validate_and_decode_output_proof.