Skip to main content

🎫 Ticket_scanner.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
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.
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_tk_value False_ht
    | Script_typed_ir.Never_tk_value False_ht
    | Script_typed_ir.Int_tk_value False_ht
    | Script_typed_ir.Nat_tk_value False_ht
    | Script_typed_ir.Signature_tk_value False_ht
    | Script_typed_ir.String_tk_value False_ht
    | Script_typed_ir.Bytes_tk_value False_ht
    | Script_typed_ir.Mutez_tk_value False_ht
    | Script_typed_ir.Bool_tk_value False_ht
    | Script_typed_ir.Key_hash_tk_value False_ht
    | Script_typed_ir.Key_tk_value False_ht
    | Script_typed_ir.Timestamp_tk_value False_ht
    | Script_typed_ir.Chain_id_tk_value False_ht
    | Script_typed_ir.Address_tk_value False_ht
    | Script_typed_ir.Tx_rollup_l2_address_tk_value False_ht
    | Script_typed_ir.Pair_t _ _ _ Dependent_bool.YesYesk_value False_ht
    | Script_typed_ir.Union_t _ _ _ Dependent_bool.YesYesk_value False_ht
    | Script_typed_ir.Option_t _ _ Dependent_bool.Yesk_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_htFalse_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_tk_value False_ht
    | Script_typed_ir.Int_tk_value False_ht
    | Script_typed_ir.Nat_tk_value False_ht
    | Script_typed_ir.Signature_tk_value False_ht
    | Script_typed_ir.String_tk_value False_ht
    | Script_typed_ir.Bytes_tk_value False_ht
    | Script_typed_ir.Mutez_tk_value False_ht
    | Script_typed_ir.Key_hash_tk_value False_ht
    | Script_typed_ir.Key_tk_value False_ht
    | Script_typed_ir.Timestamp_tk_value False_ht
    | Script_typed_ir.Address_tk_value False_ht
    | Script_typed_ir.Tx_rollup_l2_address_tk_value False_ht
    | Script_typed_ir.Bool_tk_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_tk_value False_ht
    | Script_typed_ir.Never_tk_value False_ht
    | Script_typed_ir.Bls12_381_g1_tk_value False_ht
    | Script_typed_ir.Bls12_381_g2_tk_value False_ht
    | Script_typed_ir.Bls12_381_fr_tk_value False_ht
    | Script_typed_ir.Chest_tk_value False_ht
    | Script_typed_ir.Chest_key_tk_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_tk_value ctxt acc_value
    | Script_typed_ir.Never_tk_value ctxt acc_value
    | Script_typed_ir.Int_tk_value ctxt acc_value
    | Script_typed_ir.Nat_tk_value ctxt acc_value
    | Script_typed_ir.Signature_tk_value ctxt acc_value
    | Script_typed_ir.String_tk_value ctxt acc_value
    | Script_typed_ir.Bytes_tk_value ctxt acc_value
    | Script_typed_ir.Mutez_tk_value ctxt acc_value
    | Script_typed_ir.Bool_tk_value ctxt acc_value
    | Script_typed_ir.Key_hash_tk_value ctxt acc_value
    | Script_typed_ir.Key_tk_value ctxt acc_value
    | Script_typed_ir.Timestamp_tk_value ctxt acc_value
    | Script_typed_ir.Chain_id_tk_value ctxt acc_value
    | Script_typed_ir.Address_tk_value ctxt acc_value
    | Script_typed_ir.Tx_rollup_l2_address_tk_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.Yesk_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
      | Nonek_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_typed_ir.boxed_list __5 ** Script_typed_ir.ty **
              Ticket_inspection.has_tickets]) [x_value, el_ty, el_hty] in
      let '{| Script_typed_ir.boxed_list.elements := elements |} := 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.fail
              (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
                  | Nonek_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_htfalse
  | _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_htreturn? (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? (int × 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 Micheline.dummy_location ctxt ty_value in
  let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in
  let ty_size := Saturation_repr.to_int ty_size 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 := Saturation_repr.to_int val_size 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? ((ty_size +i val_size), ctxt).