Skip to main content

🎫 Ticket_scanner.v

Translated OCaml

See proofs, 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 : 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 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 _ _
      has_tickets_of_ty_aux ty
        (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 _
      has_tickets_of_ty_aux ty
        (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 : 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) in
    let? ht := has_tickets_of_ty_aux ty 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.

  Axiom tickets_of_value_aux : {a ret : Set},
    bool Alpha_context.context Ticket_inspection.has_tickets
    Script_typed_ir.ty a accumulator continuation ret M? ret.

  Axiom tickets_of_list : {a ret : Set},
    Alpha_context.context bool Ticket_inspection.has_tickets
    Script_typed_ir.ty list a accumulator continuation ret M? ret.

  Axiom tickets_of_map : {k v ret : Set},
    bool Alpha_context.context Ticket_inspection.has_tickets
    Script_typed_ir.ty Script_typed_ir.map k v accumulator
    continuation ret M? ret.

  Axiom tickets_of_big_map : {ret : Set},
    Alpha_context.context Ticket_inspection.has_tickets
    Script_typed_ir.comparable_ty Script_typed_ir.big_map accumulator
    continuation ret M? ret.

  Definition tickets_of_value {A : Set}
    (ctxt : Alpha_context.context) (include_lazy : bool)
    (ht : Ticket_inspection.has_tickets) (ty : Script_typed_ir.ty) (x_value : A)
    : M? (accumulator × Alpha_context.context) :=
    tickets_of_value_aux include_lazy ctxt ht ty 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 : Script_typed_ir.ty)
  : M? (has_tickets × Alpha_context.context) :=
  let? '(has_tickets_value, ctxt) := Ticket_inspection.has_tickets_of_ty ctxt ty
    in
  return? ((Has_tickets has_tickets_value ty), 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 := function_parameter in
  Ticket_collection.tickets_of_value ctxt include_lazy ht ty.

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 := has_tickets_value in
  match ht with
  | Ticket_inspection.False_htreturn? (nil, ctxt)
  | _
    let? '(value_value, ctxt) :=
      (Script_ir_translator.parse_data (A := a)) None ctxt true true ty expr in
    tickets_of_value ctxt include_lazy has_tickets_value value_value
  end.