🎫 Ticket_scanner.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.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator_config.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_list.
Require TezosOfOCaml.Proto_alpha.Script_map.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir_size_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"Unsupported_non_empty_overlay" "Unsupported non empty overlay"
"Unsupported big-map value with non-empty overlay"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unsupported big-map value with non-empty overlay"
CamlinternalFormatBasics.End_of_format)
"Unsupported big-map value with non-empty overlay")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unsupported_non_empty_overlay" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unsupported_non_empty_overlay" unit tt) in
Error_monad.register_error_kind Error_monad.Branch
"Unsupported_type_operation" "Unsupported type operation"
"Types embedding operations are not supported"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Types embedding operations are not supported"
CamlinternalFormatBasics.End_of_format)
"Types embedding operations are not supported")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unsupported_type_operation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unsupported_type_operation" unit tt).
Inductive ex_ticket : Set :=
| Ex_ticket : ∀ {a : Set},
Script_typed_ir.comparable_ty → Script_typed_ir.ticket a → ex_ticket.
Module Ticket_inspection.
let '_ :=
Error_monad.register_error_kind Error_monad.Branch
"Unsupported_non_empty_overlay" "Unsupported non empty overlay"
"Unsupported big-map value with non-empty overlay"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Unsupported big-map value with non-empty overlay"
CamlinternalFormatBasics.End_of_format)
"Unsupported big-map value with non-empty overlay")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unsupported_non_empty_overlay" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unsupported_non_empty_overlay" unit tt) in
Error_monad.register_error_kind Error_monad.Branch
"Unsupported_type_operation" "Unsupported type operation"
"Types embedding operations are not supported"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal
"Types embedding operations are not supported"
CamlinternalFormatBasics.End_of_format)
"Types embedding operations are not supported")))
Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unsupported_type_operation" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Unsupported_type_operation" unit tt).
Inductive ex_ticket : Set :=
| Ex_ticket : ∀ {a : Set},
Script_typed_ir.comparable_ty → Script_typed_ir.ticket a → ex_ticket.
Module Ticket_inspection.
Witness flag for whether a type can be populated by a value containing a
ticket. [False_ht] must be used only when a value of the type cannot
contain a ticket.
This flag is necessary for avoiding ticket collection (see below) to have
quadratic complexity in the order of: size-of-the-type * size-of-value.
This type is local to the [Ticket_scanner] module and should not be
exported.
Inductive has_tickets : Set :=
| True_ht : has_tickets
| False_ht : has_tickets
| Pair_ht : has_tickets → has_tickets → has_tickets
| Union_ht : has_tickets → has_tickets → has_tickets
| Option_ht : has_tickets → has_tickets
| List_ht : has_tickets → has_tickets
| Set_ht : has_tickets → has_tickets
| Map_ht : has_tickets → has_tickets → has_tickets
| Big_map_ht : has_tickets → has_tickets → has_tickets.
Definition has_tickets_of_comparable {ret : Set}
(key_ty : Script_typed_ir.comparable_ty) (k_value : has_tickets → ret)
: ret :=
match key_ty with
| Script_typed_ir.Unit_t ⇒ k_value False_ht
| Script_typed_ir.Never_t ⇒ k_value False_ht
| Script_typed_ir.Int_t ⇒ k_value False_ht
| Script_typed_ir.Nat_t ⇒ k_value False_ht
| Script_typed_ir.Signature_t ⇒ k_value False_ht
| Script_typed_ir.String_t ⇒ k_value False_ht
| Script_typed_ir.Bytes_t ⇒ k_value False_ht
| Script_typed_ir.Mutez_t ⇒ k_value False_ht
| Script_typed_ir.Bool_t ⇒ k_value False_ht
| Script_typed_ir.Key_hash_t ⇒ k_value False_ht
| Script_typed_ir.Key_t ⇒ k_value False_ht
| Script_typed_ir.Timestamp_t ⇒ k_value False_ht
| Script_typed_ir.Chain_id_t ⇒ k_value False_ht
| Script_typed_ir.Address_t ⇒ k_value False_ht
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value False_ht
| Script_typed_ir.Pair_t _ _ _ Dependent_bool.YesYes ⇒ k_value False_ht
| Script_typed_ir.Union_t _ _ _ Dependent_bool.YesYes ⇒ k_value False_ht
| Script_typed_ir.Option_t _ _ Dependent_bool.Yes ⇒ k_value False_ht
| _ ⇒ unreachable_gadt_branch
end.
Definition pair_has_tickets
(pair_value : has_tickets → has_tickets → has_tickets) (ht1 : has_tickets)
(ht2 : has_tickets) : has_tickets :=
match (ht1, ht2) with
| (False_ht, False_ht) ⇒ False_ht
| _ ⇒ pair_value ht1 ht2
end.
Definition map_has_tickets
(map : has_tickets → has_tickets) (ht : has_tickets) : has_tickets :=
match ht with
| False_ht ⇒ False_ht
| _ ⇒ map ht
end.
Definition continuation (r : Set) : Set := has_tickets → M? r.
Reserved Notation "'has_tickets_of_pair".
Reserved Notation "'has_tickets_of_key_and_value".
Fixpoint has_tickets_of_ty_aux {ret : Set}
(ty_value : Script_typed_ir.ty) (k_value : continuation ret) : M? ret :=
let has_tickets_of_pair {ret} := 'has_tickets_of_pair ret in
let has_tickets_of_key_and_value {ret} := 'has_tickets_of_key_and_value ret
in
match ty_value with
| Script_typed_ir.Ticket_t _ _ ⇒ k_value True_ht
| Script_typed_ir.Unit_t ⇒ k_value False_ht
| Script_typed_ir.Int_t ⇒ k_value False_ht
| Script_typed_ir.Nat_t ⇒ k_value False_ht
| Script_typed_ir.Signature_t ⇒ k_value False_ht
| Script_typed_ir.String_t ⇒ k_value False_ht
| Script_typed_ir.Bytes_t ⇒ k_value False_ht
| Script_typed_ir.Mutez_t ⇒ k_value False_ht
| Script_typed_ir.Key_hash_t ⇒ k_value False_ht
| Script_typed_ir.Key_t ⇒ k_value False_ht
| Script_typed_ir.Timestamp_t ⇒ k_value False_ht
| Script_typed_ir.Address_t ⇒ k_value False_ht
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value False_ht
| Script_typed_ir.Bool_t ⇒ k_value False_ht
| Script_typed_ir.Pair_t ty1 ty2 _ _ ⇒
has_tickets_of_pair ty1 ty2
(fun (ht1 : has_tickets) ⇒ fun (ht2 : has_tickets) ⇒ Pair_ht ht1 ht2)
k_value
| Script_typed_ir.Union_t ty1 ty2 _ _ ⇒
has_tickets_of_pair ty1 ty2
(fun (ht1 : has_tickets) ⇒ fun (ht2 : has_tickets) ⇒ Union_ht ht1 ht2)
k_value
| Script_typed_ir.Lambda_t _ _ _ ⇒ k_value False_ht
| Script_typed_ir.Option_t ty_value _ _ ⇒
has_tickets_of_ty_aux ty_value
(fun (ht : has_tickets) ⇒
let opt_hty :=
map_has_tickets (fun (ht : has_tickets) ⇒ Option_ht ht) ht in
k_value opt_hty)
| Script_typed_ir.List_t ty_value _ ⇒
has_tickets_of_ty_aux ty_value
(fun (ht : has_tickets) ⇒
let list_hty :=
map_has_tickets (fun (ht : has_tickets) ⇒ List_ht ht) ht in
k_value list_hty)
| Script_typed_ir.Set_t key_ty _ ⇒
has_tickets_of_comparable key_ty
(fun (ht : has_tickets) ⇒
let set_hty :=
map_has_tickets (fun (ht : has_tickets) ⇒ Set_ht ht) ht in
k_value set_hty)
| Script_typed_ir.Map_t key_ty val_ty _ ⇒
has_tickets_of_key_and_value key_ty val_ty
(fun (ht1 : has_tickets) ⇒ fun (ht2 : has_tickets) ⇒ Map_ht ht1 ht2)
k_value
| Script_typed_ir.Big_map_t key_ty val_ty _ ⇒
has_tickets_of_key_and_value key_ty val_ty
(fun (ht1 : has_tickets) ⇒
fun (ht2 : has_tickets) ⇒ Big_map_ht ht1 ht2) k_value
| Script_typed_ir.Contract_t _ _ ⇒ k_value False_ht
| Script_typed_ir.Sapling_transaction_t _ ⇒ k_value False_ht
| Script_typed_ir.Sapling_transaction_deprecated_t _ ⇒ k_value False_ht
| Script_typed_ir.Sapling_state_t _ ⇒ k_value False_ht
| Script_typed_ir.Operation_t ⇒
Error_monad.error_value
(Build_extensible "Unsupported_type_operation" unit tt)
| Script_typed_ir.Chain_id_t ⇒ k_value False_ht
| Script_typed_ir.Never_t ⇒ k_value False_ht
| Script_typed_ir.Bls12_381_g1_t ⇒ k_value False_ht
| Script_typed_ir.Bls12_381_g2_t ⇒ k_value False_ht
| Script_typed_ir.Bls12_381_fr_t ⇒ k_value False_ht
| Script_typed_ir.Chest_t ⇒ k_value False_ht
| Script_typed_ir.Chest_key_t ⇒ k_value False_ht
end
where "'has_tickets_of_pair" :=
(fun (ret : Set) ⇒ fun
(ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.ty)
(pair_value : has_tickets → has_tickets → has_tickets)
(k_value : continuation ret) ⇒
has_tickets_of_ty_aux ty1
(fun (ht1 : has_tickets) ⇒
has_tickets_of_ty_aux ty2
(fun (ht2 : has_tickets) ⇒
k_value (pair_has_tickets pair_value ht1 ht2))))
and "'has_tickets_of_key_and_value" :=
(fun (ret : Set) ⇒ fun
(key_ty : Script_typed_ir.comparable_ty) (val_ty : Script_typed_ir.ty)
(pair_value : has_tickets → has_tickets → has_tickets)
(k_value : continuation ret) ⇒
has_tickets_of_comparable key_ty
(fun (ht1 : has_tickets) ⇒
has_tickets_of_ty_aux val_ty
(fun (ht2 : has_tickets) ⇒
k_value (pair_has_tickets pair_value ht1 ht2)))).
Definition has_tickets_of_pair {ret : Set} := 'has_tickets_of_pair ret.
Definition has_tickets_of_key_and_value {ret : Set} :=
'has_tickets_of_key_and_value ret.
Definition has_tickets_of_ty
(ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty)
: M? (has_tickets × Alpha_context.context) :=
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Ticket_costs.has_tickets_of_ty_cost ty_value) in
let? ht := has_tickets_of_ty_aux ty_value Error_monad.ok in
return? (ht, ctxt).
End Ticket_inspection.
Module Ticket_collection.
Definition consume_gas_steps : Alpha_context.t → int → M? Alpha_context.t :=
fun x_1 ⇒
Ticket_costs.consume_gas_steps x_1
Ticket_costs.Constants.cost_collect_tickets_step.
Definition accumulator : Set := list ex_ticket.
Definition continuation (a : Set) : Set :=
Alpha_context.context → accumulator → M? a.
Definition tickets_of_comparable {ret : Set}
(ctxt : Alpha_context.context) (comp_ty : Script_typed_ir.comparable_ty)
(acc_value : accumulator) (k_value : continuation ret) : M? ret :=
match comp_ty with
| Script_typed_ir.Unit_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Never_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Int_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Nat_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Signature_t ⇒ k_value ctxt acc_value
| Script_typed_ir.String_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Bytes_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Mutez_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Bool_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Key_hash_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Key_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Timestamp_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Chain_id_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Address_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Pair_t _ _ _ Dependent_bool.YesYes ⇒
k_value ctxt acc_value
| Script_typed_ir.Union_t _ _ _ Dependent_bool.YesYes ⇒
k_value ctxt acc_value
| Script_typed_ir.Option_t _ _ Dependent_bool.Yes ⇒ k_value ctxt acc_value
| _ ⇒ unreachable_gadt_branch
end.
Definition tickets_of_set {a ret : Set}
(ctxt : Alpha_context.context) (key_ty : Script_typed_ir.comparable_ty)
(_set : Script_typed_ir.set a) (acc_value : accumulator)
(k_value : continuation ret) : M? ret :=
let? ctxt := consume_gas_steps ctxt 1 in
tickets_of_comparable ctxt key_ty acc_value k_value.
Reserved Notation "'tickets_of_map".
Reserved Notation "'tickets_of_big_map".
#[bypass_check(guard)]
Fixpoint tickets_of_value_aux {a ret : Set}
(include_lazy : bool) (ctxt : Alpha_context.context)
(hty : Ticket_inspection.has_tickets) (ty_value : Script_typed_ir.ty)
(x_value : a) (acc_value : accumulator) (k_value : continuation ret)
{struct hty} : M? ret :=
let tickets_of_map {k v ret} := 'tickets_of_map k v ret in
let tickets_of_big_map {v ret} := 'tickets_of_big_map v ret in
let? ctxt := consume_gas_steps ctxt 1 in
match (hty, ty_value, x_value) with
| (Ticket_inspection.False_ht, _, _) ⇒ k_value ctxt acc_value
|
(Ticket_inspection.Pair_ht hty1 hty2, Script_typed_ir.Pair_t ty1 ty2 _ _,
x_value) ⇒
let 'existT _ [__0, __1] [x_value, ty2, ty1, hty2, hty1] :=
cast_exists (Es := [Set ** Set])
(fun '[__0, __1] ⇒
[__0 × __1 ** Script_typed_ir.ty ** Script_typed_ir.ty **
Ticket_inspection.has_tickets ** Ticket_inspection.has_tickets])
[x_value, ty2, ty1, hty2, hty1] in
let '(l_value, r_value) := x_value in
tickets_of_value_aux include_lazy ctxt hty1 ty1 l_value acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
tickets_of_value_aux include_lazy ctxt hty2 ty2 r_value acc_value
k_value)
|
(Ticket_inspection.Union_ht htyl htyr,
Script_typed_ir.Union_t tyl tyr _ _, x_value) ⇒
let 'existT _ [__2, __3] [x_value, tyr, tyl, htyr, htyl] :=
cast_exists (Es := [Set ** Set])
(fun '[__2, __3] ⇒
[Script_typed_ir.union __2 __3 ** Script_typed_ir.ty **
Script_typed_ir.ty ** Ticket_inspection.has_tickets **
Ticket_inspection.has_tickets]) [x_value, tyr, tyl, htyr, htyl] in
match x_value with
| Script_typed_ir.L v_value ⇒
tickets_of_value_aux include_lazy ctxt htyl tyl v_value acc_value
k_value
| Script_typed_ir.R v_value ⇒
tickets_of_value_aux include_lazy ctxt htyr tyr v_value acc_value
k_value
end
|
(Ticket_inspection.Option_ht el_hty, Script_typed_ir.Option_t el_ty _ _,
x_value) ⇒
let 'existT _ __4 [x_value, el_ty, el_hty] :=
cast_exists (Es := Set)
(fun __4 ⇒
[option __4 ** Script_typed_ir.ty ** Ticket_inspection.has_tickets])
[x_value, el_ty, el_hty] in
match x_value with
| Some x_value ⇒
tickets_of_value_aux include_lazy ctxt el_hty el_ty x_value acc_value
k_value
| None ⇒ k_value ctxt acc_value
end
|
(Ticket_inspection.List_ht el_hty, Script_typed_ir.List_t el_ty _, x_value)
⇒
let 'existT _ __5 [x_value, el_ty, el_hty] :=
cast_exists (Es := Set)
(fun __5 ⇒
[Script_list.t __5 ** Script_typed_ir.ty **
Ticket_inspection.has_tickets]) [x_value, el_ty, el_hty] in
let elements := Script_list.to_list x_value in
tickets_of_list ctxt include_lazy el_hty el_ty elements acc_value k_value
| (Ticket_inspection.Set_ht _, Script_typed_ir.Set_t key_ty _, x_value) ⇒
let 'existT _ __6 [x_value, key_ty] :=
cast_exists (Es := Set)
(fun __6 ⇒ [Script_typed_ir.set __6 ** Script_typed_ir.comparable_ty])
[x_value, key_ty] in
tickets_of_set ctxt key_ty x_value acc_value k_value
|
(Ticket_inspection.Map_ht _ val_hty,
Script_typed_ir.Map_t key_ty val_ty _, x_value) ⇒
let 'existT _ [__7, __8] [x_value, val_ty, key_ty, val_hty] :=
cast_exists (Es := [Set ** Set])
(fun '[__7, __8] ⇒
[Script_typed_ir.map __7 __8 ** Script_typed_ir.ty **
Script_typed_ir.comparable_ty ** Ticket_inspection.has_tickets])
[x_value, val_ty, key_ty, val_hty] in
tickets_of_comparable ctxt key_ty acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
tickets_of_map include_lazy ctxt val_hty val_ty x_value acc_value
k_value)
|
(Ticket_inspection.Big_map_ht _ val_hty,
Script_typed_ir.Big_map_t key_ty _ _, x_value) ⇒
let 'existT _ __10 [x_value, key_ty, val_hty] :=
cast_exists (Es := Set)
(fun __10 ⇒
[Script_typed_ir.big_map ** Script_typed_ir.comparable_ty **
Ticket_inspection.has_tickets]) [x_value, key_ty, val_hty] in
if include_lazy then
(tickets_of_big_map (v := __10)) ctxt val_hty key_ty x_value acc_value
k_value
else
k_value ctxt acc_value
| (Ticket_inspection.True_ht, Script_typed_ir.Ticket_t comp_ty _, x_value)
⇒
let 'existT _ __11 [x_value, comp_ty] :=
cast_exists (Es := Set)
(fun __11 ⇒
[Script_typed_ir.ticket __11 ** Script_typed_ir.comparable_ty])
[x_value, comp_ty] in
k_value ctxt (cons (Ex_ticket comp_ty x_value) acc_value)
| _ ⇒ unreachable_gadt_branch
end
with tickets_of_list {a ret : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(el_hty : Ticket_inspection.has_tickets) (el_ty : Script_typed_ir.ty)
(elements : list a) (acc_value : accumulator) (k_value : continuation ret)
{struct elements} : M? ret :=
let? ctxt := consume_gas_steps ctxt 1 in
match elements with
| cons elem elems ⇒
tickets_of_value_aux include_lazy ctxt el_hty el_ty elem acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
tickets_of_list ctxt include_lazy el_hty el_ty elems acc_value
k_value)
| [] ⇒ k_value ctxt acc_value
end
where "'tickets_of_map" :=
(fun (k v ret : Set) ⇒ fun
(include_lazy : bool) (ctxt : Alpha_context.context)
(val_hty : Ticket_inspection.has_tickets) (val_ty : Script_typed_ir.ty)
(map : Script_typed_ir.map k v) (acc_value : accumulator)
(k_value : continuation ret) ⇒
let M := Script_map.get_module map in
let 'existS _ _ M := M in
let? ctxt := consume_gas_steps ctxt 1 in
let? ctxt :=
consume_gas_steps ctxt M.(Script_typed_ir.Boxed_map.size_value) in
let values :=
M.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.fold)
(fun (function_parameter : k) ⇒
let '_ := function_parameter in
fun (v_value : v) ⇒ fun (vs : list v) ⇒ cons v_value vs)
M.(Script_typed_ir.Boxed_map.boxed) nil in
tickets_of_list ctxt include_lazy val_hty val_ty values acc_value k_value)
and "'tickets_of_big_map" :=
(fun (v ret : Set) ⇒ fun
(ctxt : Alpha_context.context) (val_hty : Ticket_inspection.has_tickets)
(key_ty : Script_typed_ir.comparable_ty)
(function_parameter : Script_typed_ir.big_map) ⇒
let
'Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.id := id;
Script_typed_ir.big_map.Big_map.diff := {|
Script_typed_ir.big_map_overlay.map := _;
Script_typed_ir.big_map_overlay.size :=
size_value
|};
Script_typed_ir.big_map.Big_map.key_type := _;
Script_typed_ir.big_map.Big_map.value_type := value_type
|} := function_parameter in
fun (acc_value : accumulator) ⇒
fun (k_value : continuation ret) ⇒
let? ctxt := consume_gas_steps ctxt 1 in
if size_value >i 0 then
Error_monad.tzfail
(Build_extensible "Unsupported_non_empty_overlay" unit tt)
else
tickets_of_comparable ctxt key_ty acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
match id with
| Some id ⇒
let accum {B : Set}
(function_parameter : list v × Alpha_context.context)
: B × Micheline.canonical Alpha_context.Script.prim →
M? (list v × Alpha_context.context) :=
let '(values, ctxt) := function_parameter in
fun (function_parameter :
B × Micheline.canonical Alpha_context.Script.prim) ⇒
let '(_key_hash, exp) := function_parameter in
let? '(v_value, ctxt) :=
Script_ir_translator.parse_data
(Script_ir_translator_config.make None None true tt)
ctxt true value_type (Micheline.root_value exp) in
return? ((cons v_value values), ctxt) in
let? '(ctxt, exps) :=
Alpha_context.Big_map.list_key_values None None ctxt id in
let? '(values, ctxt) :=
List.fold_left_es accum (nil, ctxt) exps in
tickets_of_list ctxt true val_hty value_type values
acc_value k_value
| None ⇒ k_value ctxt acc_value
end)).
Definition tickets_of_map {k v ret : Set} := 'tickets_of_map k v ret.
Definition tickets_of_big_map {ret : Set} := 'tickets_of_big_map ret.
Definition tickets_of_value {A : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(ht : Ticket_inspection.has_tickets) (ty_value : Script_typed_ir.ty)
(x_value : A) : M? (accumulator × Alpha_context.context) :=
tickets_of_value_aux include_lazy ctxt ht ty_value x_value nil
(fun (ctxt : Alpha_context.context) ⇒
fun (ex_tickets : accumulator) ⇒ return? (ex_tickets, ctxt)).
End Ticket_collection.
Inductive has_tickets : Set :=
| Has_tickets :
Ticket_inspection.has_tickets → Script_typed_ir.ty → has_tickets.
Definition type_has_tickets
(ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty)
: M? (has_tickets × Alpha_context.context) :=
let? '(has_tickets_value, ctxt) :=
Ticket_inspection.has_tickets_of_ty ctxt ty_value in
return? ((Has_tickets has_tickets_value ty_value), ctxt).
Definition tickets_of_value {A : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(function_parameter : has_tickets)
: A → M? (Ticket_collection.accumulator × Alpha_context.context) :=
let 'Has_tickets ht ty_value := function_parameter in
Ticket_collection.tickets_of_value ctxt include_lazy ht ty_value.
Definition has_tickets_value (function_parameter : has_tickets) : bool :=
let 'Has_tickets ht _ := function_parameter in
match ht with
| Ticket_inspection.False_ht ⇒ false
| _ ⇒ true
end.
Definition tickets_of_node {a : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(has_tickets_value : has_tickets) (expr : Alpha_context.Script.node)
: M? (Ticket_collection.accumulator × Alpha_context.context) :=
let 'Has_tickets ht ty_value := has_tickets_value in
match ht with
| Ticket_inspection.False_ht ⇒ return? (nil, ctxt)
| _ ⇒
let? '(value_value, ctxt) :=
(Script_ir_translator.parse_data (A := a))
(Script_ir_translator_config.make None None true tt) ctxt true ty_value
expr in
tickets_of_value ctxt include_lazy has_tickets_value value_value
end.
Definition ex_ticket_size
(ctxt : Alpha_context.context) (function_parameter : ex_ticket)
: M? (Saturation_repr.t × Alpha_context.context) :=
let 'Ex_ticket ty_value ticket := function_parameter in
let? ty_value := Script_typed_ir.ticket_t Micheline.dummy_location ty_value in
let? '(ty', ctxt) := Script_ir_unparser.unparse_ty tt ctxt ty_value in
let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in
let ty_size_cost := Script_typed_ir_size_costs.nodes_cost ty_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt ty_size_cost in
let '(val_nodes, val_size) := Script_typed_ir_size.value_size ty_value ticket
in
let val_size_cost := Script_typed_ir_size_costs.nodes_cost val_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt val_size_cost in
return? ((Saturation_repr.add ty_size val_size), ctxt).
Definition ex_token_and_amount_of_ex_ticket (function_parameter : ex_ticket)
: Ticket_token.ex_token × Script_typed_ir.ticket_amount :=
let
'Ex_ticket contents_type {|
Script_typed_ir.ticket.ticketer := ticketer;
Script_typed_ir.ticket.contents := contents;
Script_typed_ir.ticket.amount := amount
|} := function_parameter in
((Ticket_token.Ex_token
{| Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents; |}), amount).
| True_ht : has_tickets
| False_ht : has_tickets
| Pair_ht : has_tickets → has_tickets → has_tickets
| Union_ht : has_tickets → has_tickets → has_tickets
| Option_ht : has_tickets → has_tickets
| List_ht : has_tickets → has_tickets
| Set_ht : has_tickets → has_tickets
| Map_ht : has_tickets → has_tickets → has_tickets
| Big_map_ht : has_tickets → has_tickets → has_tickets.
Definition has_tickets_of_comparable {ret : Set}
(key_ty : Script_typed_ir.comparable_ty) (k_value : has_tickets → ret)
: ret :=
match key_ty with
| Script_typed_ir.Unit_t ⇒ k_value False_ht
| Script_typed_ir.Never_t ⇒ k_value False_ht
| Script_typed_ir.Int_t ⇒ k_value False_ht
| Script_typed_ir.Nat_t ⇒ k_value False_ht
| Script_typed_ir.Signature_t ⇒ k_value False_ht
| Script_typed_ir.String_t ⇒ k_value False_ht
| Script_typed_ir.Bytes_t ⇒ k_value False_ht
| Script_typed_ir.Mutez_t ⇒ k_value False_ht
| Script_typed_ir.Bool_t ⇒ k_value False_ht
| Script_typed_ir.Key_hash_t ⇒ k_value False_ht
| Script_typed_ir.Key_t ⇒ k_value False_ht
| Script_typed_ir.Timestamp_t ⇒ k_value False_ht
| Script_typed_ir.Chain_id_t ⇒ k_value False_ht
| Script_typed_ir.Address_t ⇒ k_value False_ht
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value False_ht
| Script_typed_ir.Pair_t _ _ _ Dependent_bool.YesYes ⇒ k_value False_ht
| Script_typed_ir.Union_t _ _ _ Dependent_bool.YesYes ⇒ k_value False_ht
| Script_typed_ir.Option_t _ _ Dependent_bool.Yes ⇒ k_value False_ht
| _ ⇒ unreachable_gadt_branch
end.
Definition pair_has_tickets
(pair_value : has_tickets → has_tickets → has_tickets) (ht1 : has_tickets)
(ht2 : has_tickets) : has_tickets :=
match (ht1, ht2) with
| (False_ht, False_ht) ⇒ False_ht
| _ ⇒ pair_value ht1 ht2
end.
Definition map_has_tickets
(map : has_tickets → has_tickets) (ht : has_tickets) : has_tickets :=
match ht with
| False_ht ⇒ False_ht
| _ ⇒ map ht
end.
Definition continuation (r : Set) : Set := has_tickets → M? r.
Reserved Notation "'has_tickets_of_pair".
Reserved Notation "'has_tickets_of_key_and_value".
Fixpoint has_tickets_of_ty_aux {ret : Set}
(ty_value : Script_typed_ir.ty) (k_value : continuation ret) : M? ret :=
let has_tickets_of_pair {ret} := 'has_tickets_of_pair ret in
let has_tickets_of_key_and_value {ret} := 'has_tickets_of_key_and_value ret
in
match ty_value with
| Script_typed_ir.Ticket_t _ _ ⇒ k_value True_ht
| Script_typed_ir.Unit_t ⇒ k_value False_ht
| Script_typed_ir.Int_t ⇒ k_value False_ht
| Script_typed_ir.Nat_t ⇒ k_value False_ht
| Script_typed_ir.Signature_t ⇒ k_value False_ht
| Script_typed_ir.String_t ⇒ k_value False_ht
| Script_typed_ir.Bytes_t ⇒ k_value False_ht
| Script_typed_ir.Mutez_t ⇒ k_value False_ht
| Script_typed_ir.Key_hash_t ⇒ k_value False_ht
| Script_typed_ir.Key_t ⇒ k_value False_ht
| Script_typed_ir.Timestamp_t ⇒ k_value False_ht
| Script_typed_ir.Address_t ⇒ k_value False_ht
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value False_ht
| Script_typed_ir.Bool_t ⇒ k_value False_ht
| Script_typed_ir.Pair_t ty1 ty2 _ _ ⇒
has_tickets_of_pair ty1 ty2
(fun (ht1 : has_tickets) ⇒ fun (ht2 : has_tickets) ⇒ Pair_ht ht1 ht2)
k_value
| Script_typed_ir.Union_t ty1 ty2 _ _ ⇒
has_tickets_of_pair ty1 ty2
(fun (ht1 : has_tickets) ⇒ fun (ht2 : has_tickets) ⇒ Union_ht ht1 ht2)
k_value
| Script_typed_ir.Lambda_t _ _ _ ⇒ k_value False_ht
| Script_typed_ir.Option_t ty_value _ _ ⇒
has_tickets_of_ty_aux ty_value
(fun (ht : has_tickets) ⇒
let opt_hty :=
map_has_tickets (fun (ht : has_tickets) ⇒ Option_ht ht) ht in
k_value opt_hty)
| Script_typed_ir.List_t ty_value _ ⇒
has_tickets_of_ty_aux ty_value
(fun (ht : has_tickets) ⇒
let list_hty :=
map_has_tickets (fun (ht : has_tickets) ⇒ List_ht ht) ht in
k_value list_hty)
| Script_typed_ir.Set_t key_ty _ ⇒
has_tickets_of_comparable key_ty
(fun (ht : has_tickets) ⇒
let set_hty :=
map_has_tickets (fun (ht : has_tickets) ⇒ Set_ht ht) ht in
k_value set_hty)
| Script_typed_ir.Map_t key_ty val_ty _ ⇒
has_tickets_of_key_and_value key_ty val_ty
(fun (ht1 : has_tickets) ⇒ fun (ht2 : has_tickets) ⇒ Map_ht ht1 ht2)
k_value
| Script_typed_ir.Big_map_t key_ty val_ty _ ⇒
has_tickets_of_key_and_value key_ty val_ty
(fun (ht1 : has_tickets) ⇒
fun (ht2 : has_tickets) ⇒ Big_map_ht ht1 ht2) k_value
| Script_typed_ir.Contract_t _ _ ⇒ k_value False_ht
| Script_typed_ir.Sapling_transaction_t _ ⇒ k_value False_ht
| Script_typed_ir.Sapling_transaction_deprecated_t _ ⇒ k_value False_ht
| Script_typed_ir.Sapling_state_t _ ⇒ k_value False_ht
| Script_typed_ir.Operation_t ⇒
Error_monad.error_value
(Build_extensible "Unsupported_type_operation" unit tt)
| Script_typed_ir.Chain_id_t ⇒ k_value False_ht
| Script_typed_ir.Never_t ⇒ k_value False_ht
| Script_typed_ir.Bls12_381_g1_t ⇒ k_value False_ht
| Script_typed_ir.Bls12_381_g2_t ⇒ k_value False_ht
| Script_typed_ir.Bls12_381_fr_t ⇒ k_value False_ht
| Script_typed_ir.Chest_t ⇒ k_value False_ht
| Script_typed_ir.Chest_key_t ⇒ k_value False_ht
end
where "'has_tickets_of_pair" :=
(fun (ret : Set) ⇒ fun
(ty1 : Script_typed_ir.ty) (ty2 : Script_typed_ir.ty)
(pair_value : has_tickets → has_tickets → has_tickets)
(k_value : continuation ret) ⇒
has_tickets_of_ty_aux ty1
(fun (ht1 : has_tickets) ⇒
has_tickets_of_ty_aux ty2
(fun (ht2 : has_tickets) ⇒
k_value (pair_has_tickets pair_value ht1 ht2))))
and "'has_tickets_of_key_and_value" :=
(fun (ret : Set) ⇒ fun
(key_ty : Script_typed_ir.comparable_ty) (val_ty : Script_typed_ir.ty)
(pair_value : has_tickets → has_tickets → has_tickets)
(k_value : continuation ret) ⇒
has_tickets_of_comparable key_ty
(fun (ht1 : has_tickets) ⇒
has_tickets_of_ty_aux val_ty
(fun (ht2 : has_tickets) ⇒
k_value (pair_has_tickets pair_value ht1 ht2)))).
Definition has_tickets_of_pair {ret : Set} := 'has_tickets_of_pair ret.
Definition has_tickets_of_key_and_value {ret : Set} :=
'has_tickets_of_key_and_value ret.
Definition has_tickets_of_ty
(ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty)
: M? (has_tickets × Alpha_context.context) :=
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Ticket_costs.has_tickets_of_ty_cost ty_value) in
let? ht := has_tickets_of_ty_aux ty_value Error_monad.ok in
return? (ht, ctxt).
End Ticket_inspection.
Module Ticket_collection.
Definition consume_gas_steps : Alpha_context.t → int → M? Alpha_context.t :=
fun x_1 ⇒
Ticket_costs.consume_gas_steps x_1
Ticket_costs.Constants.cost_collect_tickets_step.
Definition accumulator : Set := list ex_ticket.
Definition continuation (a : Set) : Set :=
Alpha_context.context → accumulator → M? a.
Definition tickets_of_comparable {ret : Set}
(ctxt : Alpha_context.context) (comp_ty : Script_typed_ir.comparable_ty)
(acc_value : accumulator) (k_value : continuation ret) : M? ret :=
match comp_ty with
| Script_typed_ir.Unit_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Never_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Int_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Nat_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Signature_t ⇒ k_value ctxt acc_value
| Script_typed_ir.String_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Bytes_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Mutez_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Bool_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Key_hash_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Key_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Timestamp_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Chain_id_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Address_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Tx_rollup_l2_address_t ⇒ k_value ctxt acc_value
| Script_typed_ir.Pair_t _ _ _ Dependent_bool.YesYes ⇒
k_value ctxt acc_value
| Script_typed_ir.Union_t _ _ _ Dependent_bool.YesYes ⇒
k_value ctxt acc_value
| Script_typed_ir.Option_t _ _ Dependent_bool.Yes ⇒ k_value ctxt acc_value
| _ ⇒ unreachable_gadt_branch
end.
Definition tickets_of_set {a ret : Set}
(ctxt : Alpha_context.context) (key_ty : Script_typed_ir.comparable_ty)
(_set : Script_typed_ir.set a) (acc_value : accumulator)
(k_value : continuation ret) : M? ret :=
let? ctxt := consume_gas_steps ctxt 1 in
tickets_of_comparable ctxt key_ty acc_value k_value.
Reserved Notation "'tickets_of_map".
Reserved Notation "'tickets_of_big_map".
#[bypass_check(guard)]
Fixpoint tickets_of_value_aux {a ret : Set}
(include_lazy : bool) (ctxt : Alpha_context.context)
(hty : Ticket_inspection.has_tickets) (ty_value : Script_typed_ir.ty)
(x_value : a) (acc_value : accumulator) (k_value : continuation ret)
{struct hty} : M? ret :=
let tickets_of_map {k v ret} := 'tickets_of_map k v ret in
let tickets_of_big_map {v ret} := 'tickets_of_big_map v ret in
let? ctxt := consume_gas_steps ctxt 1 in
match (hty, ty_value, x_value) with
| (Ticket_inspection.False_ht, _, _) ⇒ k_value ctxt acc_value
|
(Ticket_inspection.Pair_ht hty1 hty2, Script_typed_ir.Pair_t ty1 ty2 _ _,
x_value) ⇒
let 'existT _ [__0, __1] [x_value, ty2, ty1, hty2, hty1] :=
cast_exists (Es := [Set ** Set])
(fun '[__0, __1] ⇒
[__0 × __1 ** Script_typed_ir.ty ** Script_typed_ir.ty **
Ticket_inspection.has_tickets ** Ticket_inspection.has_tickets])
[x_value, ty2, ty1, hty2, hty1] in
let '(l_value, r_value) := x_value in
tickets_of_value_aux include_lazy ctxt hty1 ty1 l_value acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
tickets_of_value_aux include_lazy ctxt hty2 ty2 r_value acc_value
k_value)
|
(Ticket_inspection.Union_ht htyl htyr,
Script_typed_ir.Union_t tyl tyr _ _, x_value) ⇒
let 'existT _ [__2, __3] [x_value, tyr, tyl, htyr, htyl] :=
cast_exists (Es := [Set ** Set])
(fun '[__2, __3] ⇒
[Script_typed_ir.union __2 __3 ** Script_typed_ir.ty **
Script_typed_ir.ty ** Ticket_inspection.has_tickets **
Ticket_inspection.has_tickets]) [x_value, tyr, tyl, htyr, htyl] in
match x_value with
| Script_typed_ir.L v_value ⇒
tickets_of_value_aux include_lazy ctxt htyl tyl v_value acc_value
k_value
| Script_typed_ir.R v_value ⇒
tickets_of_value_aux include_lazy ctxt htyr tyr v_value acc_value
k_value
end
|
(Ticket_inspection.Option_ht el_hty, Script_typed_ir.Option_t el_ty _ _,
x_value) ⇒
let 'existT _ __4 [x_value, el_ty, el_hty] :=
cast_exists (Es := Set)
(fun __4 ⇒
[option __4 ** Script_typed_ir.ty ** Ticket_inspection.has_tickets])
[x_value, el_ty, el_hty] in
match x_value with
| Some x_value ⇒
tickets_of_value_aux include_lazy ctxt el_hty el_ty x_value acc_value
k_value
| None ⇒ k_value ctxt acc_value
end
|
(Ticket_inspection.List_ht el_hty, Script_typed_ir.List_t el_ty _, x_value)
⇒
let 'existT _ __5 [x_value, el_ty, el_hty] :=
cast_exists (Es := Set)
(fun __5 ⇒
[Script_list.t __5 ** Script_typed_ir.ty **
Ticket_inspection.has_tickets]) [x_value, el_ty, el_hty] in
let elements := Script_list.to_list x_value in
tickets_of_list ctxt include_lazy el_hty el_ty elements acc_value k_value
| (Ticket_inspection.Set_ht _, Script_typed_ir.Set_t key_ty _, x_value) ⇒
let 'existT _ __6 [x_value, key_ty] :=
cast_exists (Es := Set)
(fun __6 ⇒ [Script_typed_ir.set __6 ** Script_typed_ir.comparable_ty])
[x_value, key_ty] in
tickets_of_set ctxt key_ty x_value acc_value k_value
|
(Ticket_inspection.Map_ht _ val_hty,
Script_typed_ir.Map_t key_ty val_ty _, x_value) ⇒
let 'existT _ [__7, __8] [x_value, val_ty, key_ty, val_hty] :=
cast_exists (Es := [Set ** Set])
(fun '[__7, __8] ⇒
[Script_typed_ir.map __7 __8 ** Script_typed_ir.ty **
Script_typed_ir.comparable_ty ** Ticket_inspection.has_tickets])
[x_value, val_ty, key_ty, val_hty] in
tickets_of_comparable ctxt key_ty acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
tickets_of_map include_lazy ctxt val_hty val_ty x_value acc_value
k_value)
|
(Ticket_inspection.Big_map_ht _ val_hty,
Script_typed_ir.Big_map_t key_ty _ _, x_value) ⇒
let 'existT _ __10 [x_value, key_ty, val_hty] :=
cast_exists (Es := Set)
(fun __10 ⇒
[Script_typed_ir.big_map ** Script_typed_ir.comparable_ty **
Ticket_inspection.has_tickets]) [x_value, key_ty, val_hty] in
if include_lazy then
(tickets_of_big_map (v := __10)) ctxt val_hty key_ty x_value acc_value
k_value
else
k_value ctxt acc_value
| (Ticket_inspection.True_ht, Script_typed_ir.Ticket_t comp_ty _, x_value)
⇒
let 'existT _ __11 [x_value, comp_ty] :=
cast_exists (Es := Set)
(fun __11 ⇒
[Script_typed_ir.ticket __11 ** Script_typed_ir.comparable_ty])
[x_value, comp_ty] in
k_value ctxt (cons (Ex_ticket comp_ty x_value) acc_value)
| _ ⇒ unreachable_gadt_branch
end
with tickets_of_list {a ret : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(el_hty : Ticket_inspection.has_tickets) (el_ty : Script_typed_ir.ty)
(elements : list a) (acc_value : accumulator) (k_value : continuation ret)
{struct elements} : M? ret :=
let? ctxt := consume_gas_steps ctxt 1 in
match elements with
| cons elem elems ⇒
tickets_of_value_aux include_lazy ctxt el_hty el_ty elem acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
tickets_of_list ctxt include_lazy el_hty el_ty elems acc_value
k_value)
| [] ⇒ k_value ctxt acc_value
end
where "'tickets_of_map" :=
(fun (k v ret : Set) ⇒ fun
(include_lazy : bool) (ctxt : Alpha_context.context)
(val_hty : Ticket_inspection.has_tickets) (val_ty : Script_typed_ir.ty)
(map : Script_typed_ir.map k v) (acc_value : accumulator)
(k_value : continuation ret) ⇒
let M := Script_map.get_module map in
let 'existS _ _ M := M in
let? ctxt := consume_gas_steps ctxt 1 in
let? ctxt :=
consume_gas_steps ctxt M.(Script_typed_ir.Boxed_map.size_value) in
let values :=
M.(Script_typed_ir.Boxed_map.OPS).(Script_typed_ir.Boxed_map_OPS.fold)
(fun (function_parameter : k) ⇒
let '_ := function_parameter in
fun (v_value : v) ⇒ fun (vs : list v) ⇒ cons v_value vs)
M.(Script_typed_ir.Boxed_map.boxed) nil in
tickets_of_list ctxt include_lazy val_hty val_ty values acc_value k_value)
and "'tickets_of_big_map" :=
(fun (v ret : Set) ⇒ fun
(ctxt : Alpha_context.context) (val_hty : Ticket_inspection.has_tickets)
(key_ty : Script_typed_ir.comparable_ty)
(function_parameter : Script_typed_ir.big_map) ⇒
let
'Script_typed_ir.Big_map {|
Script_typed_ir.big_map.Big_map.id := id;
Script_typed_ir.big_map.Big_map.diff := {|
Script_typed_ir.big_map_overlay.map := _;
Script_typed_ir.big_map_overlay.size :=
size_value
|};
Script_typed_ir.big_map.Big_map.key_type := _;
Script_typed_ir.big_map.Big_map.value_type := value_type
|} := function_parameter in
fun (acc_value : accumulator) ⇒
fun (k_value : continuation ret) ⇒
let? ctxt := consume_gas_steps ctxt 1 in
if size_value >i 0 then
Error_monad.tzfail
(Build_extensible "Unsupported_non_empty_overlay" unit tt)
else
tickets_of_comparable ctxt key_ty acc_value
(fun (ctxt : Alpha_context.context) ⇒
fun (acc_value : accumulator) ⇒
match id with
| Some id ⇒
let accum {B : Set}
(function_parameter : list v × Alpha_context.context)
: B × Micheline.canonical Alpha_context.Script.prim →
M? (list v × Alpha_context.context) :=
let '(values, ctxt) := function_parameter in
fun (function_parameter :
B × Micheline.canonical Alpha_context.Script.prim) ⇒
let '(_key_hash, exp) := function_parameter in
let? '(v_value, ctxt) :=
Script_ir_translator.parse_data
(Script_ir_translator_config.make None None true tt)
ctxt true value_type (Micheline.root_value exp) in
return? ((cons v_value values), ctxt) in
let? '(ctxt, exps) :=
Alpha_context.Big_map.list_key_values None None ctxt id in
let? '(values, ctxt) :=
List.fold_left_es accum (nil, ctxt) exps in
tickets_of_list ctxt true val_hty value_type values
acc_value k_value
| None ⇒ k_value ctxt acc_value
end)).
Definition tickets_of_map {k v ret : Set} := 'tickets_of_map k v ret.
Definition tickets_of_big_map {ret : Set} := 'tickets_of_big_map ret.
Definition tickets_of_value {A : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(ht : Ticket_inspection.has_tickets) (ty_value : Script_typed_ir.ty)
(x_value : A) : M? (accumulator × Alpha_context.context) :=
tickets_of_value_aux include_lazy ctxt ht ty_value x_value nil
(fun (ctxt : Alpha_context.context) ⇒
fun (ex_tickets : accumulator) ⇒ return? (ex_tickets, ctxt)).
End Ticket_collection.
Inductive has_tickets : Set :=
| Has_tickets :
Ticket_inspection.has_tickets → Script_typed_ir.ty → has_tickets.
Definition type_has_tickets
(ctxt : Alpha_context.context) (ty_value : Script_typed_ir.ty)
: M? (has_tickets × Alpha_context.context) :=
let? '(has_tickets_value, ctxt) :=
Ticket_inspection.has_tickets_of_ty ctxt ty_value in
return? ((Has_tickets has_tickets_value ty_value), ctxt).
Definition tickets_of_value {A : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(function_parameter : has_tickets)
: A → M? (Ticket_collection.accumulator × Alpha_context.context) :=
let 'Has_tickets ht ty_value := function_parameter in
Ticket_collection.tickets_of_value ctxt include_lazy ht ty_value.
Definition has_tickets_value (function_parameter : has_tickets) : bool :=
let 'Has_tickets ht _ := function_parameter in
match ht with
| Ticket_inspection.False_ht ⇒ false
| _ ⇒ true
end.
Definition tickets_of_node {a : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(has_tickets_value : has_tickets) (expr : Alpha_context.Script.node)
: M? (Ticket_collection.accumulator × Alpha_context.context) :=
let 'Has_tickets ht ty_value := has_tickets_value in
match ht with
| Ticket_inspection.False_ht ⇒ return? (nil, ctxt)
| _ ⇒
let? '(value_value, ctxt) :=
(Script_ir_translator.parse_data (A := a))
(Script_ir_translator_config.make None None true tt) ctxt true ty_value
expr in
tickets_of_value ctxt include_lazy has_tickets_value value_value
end.
Definition ex_ticket_size
(ctxt : Alpha_context.context) (function_parameter : ex_ticket)
: M? (Saturation_repr.t × Alpha_context.context) :=
let 'Ex_ticket ty_value ticket := function_parameter in
let? ty_value := Script_typed_ir.ticket_t Micheline.dummy_location ty_value in
let? '(ty', ctxt) := Script_ir_unparser.unparse_ty tt ctxt ty_value in
let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in
let ty_size_cost := Script_typed_ir_size_costs.nodes_cost ty_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt ty_size_cost in
let '(val_nodes, val_size) := Script_typed_ir_size.value_size ty_value ticket
in
let val_size_cost := Script_typed_ir_size_costs.nodes_cost val_nodes in
let? ctxt := Alpha_context.Gas.consume ctxt val_size_cost in
return? ((Saturation_repr.add ty_size val_size), ctxt).
Definition ex_token_and_amount_of_ex_ticket (function_parameter : ex_ticket)
: Ticket_token.ex_token × Script_typed_ir.ticket_amount :=
let
'Ex_ticket contents_type {|
Script_typed_ir.ticket.ticketer := ticketer;
Script_typed_ir.ticket.contents := contents;
Script_typed_ir.ticket.amount := amount
|} := function_parameter in
((Ticket_token.Ex_token
{| Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents; |}), amount).