🍬 Script_interpreter_mli.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.Local_gas_counter.
Require TezosOfOCaml.Proto_alpha.Script_interpreter_defs.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Module execution_result.
Record record : Set := Build {
script : Script_ir_translator.ex_script;
code_size : int;
storage : Alpha_context.Script.expr;
lazy_storage_diff : option Alpha_context.Lazy_storage.diffs;
operations : list Script_typed_ir.packed_internal_operation;
ticket_diffs : Ticket_token_map.t Z.t;
ticket_receipt : Ticket_receipt.t;
}.
Definition with_script script (r : record) :=
Build script r.(code_size) r.(storage) r.(lazy_storage_diff) r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_code_size code_size (r : record) :=
Build r.(script) code_size r.(storage) r.(lazy_storage_diff) r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_storage storage (r : record) :=
Build r.(script) r.(code_size) storage r.(lazy_storage_diff) r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_lazy_storage_diff lazy_storage_diff (r : record) :=
Build r.(script) r.(code_size) r.(storage) lazy_storage_diff r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_operations operations (r : record) :=
Build r.(script) r.(code_size) r.(storage) r.(lazy_storage_diff) operations
r.(ticket_diffs) r.(ticket_receipt).
Definition with_ticket_diffs ticket_diffs (r : record) :=
Build r.(script) r.(code_size) r.(storage) r.(lazy_storage_diff)
r.(operations) ticket_diffs r.(ticket_receipt).
Definition with_ticket_receipt ticket_receipt (r : record) :=
Build r.(script) r.(code_size) r.(storage) r.(lazy_storage_diff)
r.(operations) r.(ticket_diffs) ticket_receipt.
End execution_result.
Definition execution_result := execution_result.record.
Definition step_constants : Set := Script_typed_ir.step_constants.
Parameter execute :
option Script_typed_ir.logger → Alpha_context.t →
option Script_ir_translator.ex_script → Script_ir_unparser.unparsing_mode →
step_constants → Alpha_context.Script.t → Alpha_context.Entrypoint.t →
Alpha_context.Script.expr → bool →
M? (execution_result × Alpha_context.context).
Parameter execute_with_typed_parameter : ∀ {a : Set},
option Script_typed_ir.logger → Alpha_context.context →
option Script_ir_translator.ex_script → Script_ir_unparser.unparsing_mode →
step_constants → Alpha_context.Script.t → Alpha_context.Entrypoint.t →
Script_typed_ir.ty → Alpha_context.Script.location → a → bool →
M? (execution_result × Alpha_context.context).
Module Internals.
Parameter next : ∀ {a f r s : Set},
option Script_typed_ir.logger →
Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → Script_typed_ir.stack_ty →
Script_typed_ir.continuation → a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter).
Parameter step : ∀ {a f r s : Set},
Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → Script_typed_ir.kinstr → a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter).
Parameter step_descr : ∀ {a f r s : Set},
option Script_typed_ir.logger → Alpha_context.context →
Script_typed_ir.step_constants → Script_typed_ir.kdescr → a → s →
M? (r × f × Alpha_context.context).
Parameter kstep : ∀ {a f r s : Set},
option Script_typed_ir.logger → Alpha_context.context → step_constants →
Script_typed_ir.stack_ty → Script_typed_ir.kinstr → a → s →
M? (r × f × Alpha_context.context).
Module Raw.
Parameter kmap_exit : ∀ {a b e f m n o : Set},
Script_interpreter_defs.kmap_exit_type a b e f m n o.
Parameter kmap_enter : ∀ {a b c d f j k : Set},
Script_interpreter_defs.kmap_enter_type a b c d f j k.
Parameter klist_exit : ∀ {a b c d i j : Set},
Script_interpreter_defs.klist_exit_type a b c d i j.
Parameter klist_enter : ∀ {a b c d e j : Set},
Script_interpreter_defs.klist_enter_type a b c d e j.
Parameter kloop_in_left : ∀ {a b e f g : Set},
Script_interpreter_defs.kloop_in_left_type a b e f g.
Parameter kloop_in : ∀ {a f r s : Set},
Script_interpreter_defs.kloop_in_type a r f s.
Parameter kiter : ∀ {a b f r s : Set},
Script_interpreter_defs.kiter_type a b s r f.
Parameter next : ∀ {a f r s : Set},
Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → Script_typed_ir.continuation →
a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter).
Parameter ilist_map : ∀ {a b c d e : Set},
Script_interpreter_defs.ilist_map_type a b c d e.
Parameter ilist_iter : ∀ {a b c d e : Set},
Script_interpreter_defs.ilist_iter_type a b c d e.
Parameter iset_iter : ∀ {a b c d e : Set},
Script_interpreter_defs.iset_iter_type a b c d e.
Parameter imap_map : ∀ {a b c d e f : Set},
Script_interpreter_defs.imap_map_type a b c d e f.
Parameter imap_iter : ∀ {a b c d e f : Set},
Script_interpreter_defs.imap_iter_type a b c d e f.
Parameter imul_teznat : ∀ {b e f : Set},
Script_interpreter_defs.imul_teznat_type b e f.
Parameter imul_nattez : ∀ {b e f : Set},
Script_interpreter_defs.imul_nattez_type b e f.
Parameter ilsl_nat : ∀ {b e f : Set},
Script_interpreter_defs.ilsl_nat_type b e f.
Parameter ilsr_nat : ∀ {b e f : Set},
Script_interpreter_defs.ilsr_nat_type b e f.
Parameter ifailwith : Script_interpreter_defs.ifailwith_type.
Parameter iexec : ∀ {b e f g : Set},
Script_interpreter_defs.iexec_type b e f g.
Parameter iview : ∀ {a b e f i : Set},
Script_interpreter_defs.iview_type a b e f i.
Parameter step : ∀ {a f r s : Set}, Script_typed_ir.step_type a s r f.
End Raw.
End Internals.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Local_gas_counter.
Require TezosOfOCaml.Proto_alpha.Script_interpreter_defs.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Module execution_result.
Record record : Set := Build {
script : Script_ir_translator.ex_script;
code_size : int;
storage : Alpha_context.Script.expr;
lazy_storage_diff : option Alpha_context.Lazy_storage.diffs;
operations : list Script_typed_ir.packed_internal_operation;
ticket_diffs : Ticket_token_map.t Z.t;
ticket_receipt : Ticket_receipt.t;
}.
Definition with_script script (r : record) :=
Build script r.(code_size) r.(storage) r.(lazy_storage_diff) r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_code_size code_size (r : record) :=
Build r.(script) code_size r.(storage) r.(lazy_storage_diff) r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_storage storage (r : record) :=
Build r.(script) r.(code_size) storage r.(lazy_storage_diff) r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_lazy_storage_diff lazy_storage_diff (r : record) :=
Build r.(script) r.(code_size) r.(storage) lazy_storage_diff r.(operations)
r.(ticket_diffs) r.(ticket_receipt).
Definition with_operations operations (r : record) :=
Build r.(script) r.(code_size) r.(storage) r.(lazy_storage_diff) operations
r.(ticket_diffs) r.(ticket_receipt).
Definition with_ticket_diffs ticket_diffs (r : record) :=
Build r.(script) r.(code_size) r.(storage) r.(lazy_storage_diff)
r.(operations) ticket_diffs r.(ticket_receipt).
Definition with_ticket_receipt ticket_receipt (r : record) :=
Build r.(script) r.(code_size) r.(storage) r.(lazy_storage_diff)
r.(operations) r.(ticket_diffs) ticket_receipt.
End execution_result.
Definition execution_result := execution_result.record.
Definition step_constants : Set := Script_typed_ir.step_constants.
Parameter execute :
option Script_typed_ir.logger → Alpha_context.t →
option Script_ir_translator.ex_script → Script_ir_unparser.unparsing_mode →
step_constants → Alpha_context.Script.t → Alpha_context.Entrypoint.t →
Alpha_context.Script.expr → bool →
M? (execution_result × Alpha_context.context).
Parameter execute_with_typed_parameter : ∀ {a : Set},
option Script_typed_ir.logger → Alpha_context.context →
option Script_ir_translator.ex_script → Script_ir_unparser.unparsing_mode →
step_constants → Alpha_context.Script.t → Alpha_context.Entrypoint.t →
Script_typed_ir.ty → Alpha_context.Script.location → a → bool →
M? (execution_result × Alpha_context.context).
Module Internals.
Parameter next : ∀ {a f r s : Set},
option Script_typed_ir.logger →
Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → Script_typed_ir.stack_ty →
Script_typed_ir.continuation → a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter).
Parameter step : ∀ {a f r s : Set},
Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → Script_typed_ir.kinstr → a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter).
Parameter step_descr : ∀ {a f r s : Set},
option Script_typed_ir.logger → Alpha_context.context →
Script_typed_ir.step_constants → Script_typed_ir.kdescr → a → s →
M? (r × f × Alpha_context.context).
Parameter kstep : ∀ {a f r s : Set},
option Script_typed_ir.logger → Alpha_context.context → step_constants →
Script_typed_ir.stack_ty → Script_typed_ir.kinstr → a → s →
M? (r × f × Alpha_context.context).
Module Raw.
Parameter kmap_exit : ∀ {a b e f m n o : Set},
Script_interpreter_defs.kmap_exit_type a b e f m n o.
Parameter kmap_enter : ∀ {a b c d f j k : Set},
Script_interpreter_defs.kmap_enter_type a b c d f j k.
Parameter klist_exit : ∀ {a b c d i j : Set},
Script_interpreter_defs.klist_exit_type a b c d i j.
Parameter klist_enter : ∀ {a b c d e j : Set},
Script_interpreter_defs.klist_enter_type a b c d e j.
Parameter kloop_in_left : ∀ {a b e f g : Set},
Script_interpreter_defs.kloop_in_left_type a b e f g.
Parameter kloop_in : ∀ {a f r s : Set},
Script_interpreter_defs.kloop_in_type a r f s.
Parameter kiter : ∀ {a b f r s : Set},
Script_interpreter_defs.kiter_type a b s r f.
Parameter next : ∀ {a f r s : Set},
Local_gas_counter.outdated_context × step_constants →
Local_gas_counter.local_gas_counter → Script_typed_ir.continuation →
a → s →
M?
(r × f × Local_gas_counter.outdated_context ×
Local_gas_counter.local_gas_counter).
Parameter ilist_map : ∀ {a b c d e : Set},
Script_interpreter_defs.ilist_map_type a b c d e.
Parameter ilist_iter : ∀ {a b c d e : Set},
Script_interpreter_defs.ilist_iter_type a b c d e.
Parameter iset_iter : ∀ {a b c d e : Set},
Script_interpreter_defs.iset_iter_type a b c d e.
Parameter imap_map : ∀ {a b c d e f : Set},
Script_interpreter_defs.imap_map_type a b c d e f.
Parameter imap_iter : ∀ {a b c d e f : Set},
Script_interpreter_defs.imap_iter_type a b c d e f.
Parameter imul_teznat : ∀ {b e f : Set},
Script_interpreter_defs.imul_teznat_type b e f.
Parameter imul_nattez : ∀ {b e f : Set},
Script_interpreter_defs.imul_nattez_type b e f.
Parameter ilsl_nat : ∀ {b e f : Set},
Script_interpreter_defs.ilsl_nat_type b e f.
Parameter ilsr_nat : ∀ {b e f : Set},
Script_interpreter_defs.ilsr_nat_type b e f.
Parameter ifailwith : Script_interpreter_defs.ifailwith_type.
Parameter iexec : ∀ {b e f g : Set},
Script_interpreter_defs.iexec_type b e f g.
Parameter iview : ∀ {a b e f i : Set},
Script_interpreter_defs.iview_type a b e f i.
Parameter step : ∀ {a f r s : Set}, Script_typed_ir.step_type a s r f.
End Raw.
End Internals.