Skip to main content

🎫 Ticket_accounting.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "invalid_ticket_transfer" "Invalid ticket transfer"
    "Invalid ticket transfer detected in ticket balance update."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : string × Z.t) ⇒
          let '(ticketer, amount) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Attempted to send "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    " unit(s) of a ticket created by "
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      (CamlinternalFormatBasics.Char_literal "." % char
                        CamlinternalFormatBasics.End_of_format)))))
              "Attempted to send %a unit(s) of a ticket created by %s.")
            Z.pp_print amount ticketer))
    (Data_encoding.obj2
      (Data_encoding.req None None "ticketer" Data_encoding.string_value)
      (Data_encoding.req None None "amount" Data_encoding.z_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_ticket_transfer" then
          let '{|
            Invalid_ticket_transfer.ticketer := ticketer;
              Invalid_ticket_transfer.amount := amount
              |} := cast Invalid_ticket_transfer payload in
          Some (ticketer, amount)
        else None
      end)
    (fun (function_parameter : string × Z.t) ⇒
      let '(ticketer, amount) := function_parameter in
      Build_extensible "Invalid_ticket_transfer" Invalid_ticket_transfer
        {| Invalid_ticket_transfer.ticketer := ticketer;
          Invalid_ticket_transfer.amount := amount; |}).

Module Ticket_token_map.
  Include Proto_alpha.Ticket_token_map.

  Definition balance_diff
    (ctxt : Alpha_context.context) (token : Ticket_token.ex_token)
    (map : Ticket_token_map.t Z.t) : M? (Z.t × Alpha_context.context) :=
    let? '(amnt_opt, ctxt) := Ticket_token_map.find ctxt token map in
    return? ((Option.value_value amnt_opt Z.zero), ctxt).

  Definition merge_overlap (ctxt : Alpha_context.context) (b1 : Z.t) (b2 : Z.t)
    : M? (Z.t × Alpha_context.context) :=
    let? ctxt := Alpha_context.Gas.consume ctxt (Ticket_costs.add_z_cost b1 b2)
      in
    return? ((b1 +Z b2), ctxt).

  Definition of_list_with_merge
    (ctxt : Alpha_context.context)
    (token_amounts : list (Ticket_token.ex_token × Z.t))
    : M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
    Ticket_token_map.of_list ctxt merge_overlap token_amounts.

  Definition add (ctxt : Alpha_context.context)
    : Ticket_token_map.t Z.t Ticket_token_map.t Z.t
    M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
    Ticket_token_map.merge ctxt merge_overlap.

  Definition sub
    (ctxt : Alpha_context.context) (m1 : Ticket_token_map.t Z.t) (m2 : t Z.t)
    : M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
    let? '(m2, ctxt) :=
      map ctxt
        (fun (ctxt : Alpha_context.context) ⇒
          fun (function_parameter : Ticket_token.ex_token) ⇒
            let '_ := function_parameter in
            fun (amount : Z.t) ⇒
              let? ctxt :=
                Alpha_context.Gas.consume ctxt (Ticket_costs.negate_cost amount)
                in
              return? ((Z.neg amount), ctxt)) m2 in
    add ctxt m1 m2.
End Ticket_token_map.

Definition ticket_balances_of_value {A : Set}
  (ctxt : Alpha_context.context) (include_lazy : bool)
  (ty : Ticket_scanner.has_tickets) (value_value : A)
  : M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
  let? '(tickets, ctxt) :=
    Ticket_scanner.tickets_of_value ctxt include_lazy ty value_value in
  let? '(list_value, ctxt) :=
    List.fold_left_e
      (fun (function_parameter :
        list (Ticket_token.ex_token × Z.t) × Alpha_context.context) ⇒
        let '(acc_value, ctxt) := function_parameter in
        fun (ticket : Ticket_scanner.ex_ticket) ⇒
          let '(token, amount) :=
            Ticket_token.token_and_amount_of_ex_ticket ticket in
          let? ctxt :=
            Alpha_context.Gas.consume ctxt
              Ticket_costs.Constants.cost_collect_tickets_step in
          return?
            ((cons (token, (Alpha_context.Script_int.to_zint amount)) acc_value),
              ctxt)) (nil, ctxt) tickets in
  Ticket_token_map.of_list_with_merge ctxt list_value.

Definition update_ticket_balances_raw
  (ctxt : Alpha_context.context) (total_storage_diff : Z.t)
  (token : Ticket_token.ex_token)
  (destinations : list (Alpha_context.Destination.t × Z.t))
  : M? (Z.t × Alpha_context.context) :=
  List.fold_left_es
    (fun (function_parameter : Z.t × Alpha_context.context) ⇒
      let '(tot_storage_diff, ctxt) := function_parameter in
      fun (function_parameter : Alpha_context.Destination.t × Z.t) ⇒
        let '(owner, delta) := function_parameter in
        let? '(key_hash, ctxt) :=
          Ticket_balance_key.of_ex_token ctxt owner token in
        let? '(storage_diff, ctxt) :=
          Alpha_context.Ticket_balance.adjust_balance ctxt key_hash delta in
        let? ctxt :=
          Alpha_context.Gas.consume ctxt
            (Ticket_costs.add_z_cost total_storage_diff storage_diff) in
        return? ((tot_storage_diff +Z storage_diff), ctxt))
    (total_storage_diff, ctxt) destinations.

Definition invalid_ticket_transfer_error
  (function_parameter : Ticket_token.ex_token) : Z.t Error_monad._error :=
  let
    'Ticket_token.Ex_token {|
      Ticket_token.ex_token.Ex_token.ticketer := ticketer;
        Ticket_token.ex_token.Ex_token.contents_type := _;
        Ticket_token.ex_token.Ex_token.contents := _
        |} := function_parameter in
  fun (amount : Z.t) ⇒
    Build_extensible "Invalid_ticket_transfer" Invalid_ticket_transfer
      {|
        Invalid_ticket_transfer.ticketer :=
          Alpha_context.Contract.to_b58check ticketer;
        Invalid_ticket_transfer.amount := amount; |}.

Definition update_ticket_balances_for_self_contract
  (ctxt : Alpha_context.context) (self : Alpha_context.Contract.t)
  (ticket_diffs : list (Ticket_token.ex_token × Z.t))
  : M? (Z.t × Alpha_context.context) :=
  List.fold_left_es
    (fun (function_parameter : Z.t × Alpha_context.context) ⇒
      let '(total_storage_diff, ctxt) := function_parameter in
      fun (function_parameter : Ticket_token.ex_token × Z.t) ⇒
        let '(ticket_token, amount) := function_parameter in
        let is_valid_balance_update :=
          let
            'Ticket_token.Ex_token {|
              Ticket_token.ex_token.Ex_token.ticketer := ticketer |} :=
            ticket_token in
          (amount Z Z.zero) || (Alpha_context.Contract.equal ticketer self) in
        let? '_ :=
          Error_monad.error_unless is_valid_balance_update
            (invalid_ticket_transfer_error ticket_token amount) in
        update_ticket_balances_raw ctxt total_storage_diff ticket_token
          [ ((Alpha_context.Destination.Contract self), amount) ])
    (Z.zero, ctxt) ticket_diffs.

Definition ticket_diffs_of_lazy_storage_diff
  (ctxt : Alpha_context.context)
  (storage_type_has_tickets : Ticket_scanner.has_tickets)
  (lazy_storage_diff : list Alpha_context.Lazy_storage.diffs_item)
  : M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
  if Ticket_scanner.has_tickets_value storage_type_has_tickets then
    let? '(diffs, ctxt) :=
      Ticket_lazy_storage_diff.ticket_diffs_of_lazy_storage_diff ctxt
        lazy_storage_diff in
    Ticket_token_map.of_list_with_merge ctxt diffs
  else
    return? (Ticket_token_map.empty, ctxt).

Description here: https://hackmd.io/lutm_5JNRVW-nNFSFkCXLQ?view#Implementation - [old_storage_strict] the amount S_1^{strict} of ticket-tokens in the strict part of the old storage. - [new_storage_strict] the amount S_2^{strict} of ticket-tokens in the strict part of the new storage. - [lazy_storage_diff] the amount S_{\delta}^{lazy} of ticket-tokens added to the lazy part of the storage. - [arg_tickets] the amount I of ticket-tokens contained in the incoming arguments.
Calculating the spending budget: additions = new_storage_strict + lazy_storage_diff subtractions = old_storage_strict + arg_tickets delta = additions - subtractions
Definition ticket_diffs {A B : Set}
  (ctxt : Alpha_context.context)
  (arg_type_has_tickets : Ticket_scanner.has_tickets)
  (storage_type_has_tickets : Ticket_scanner.has_tickets) (arg : A)
  (old_storage : B) (new_storage : B)
  (lazy_storage_diff : list Alpha_context.Lazy_storage.diffs_item)
  : M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
  let? '(arg_tickets, ctxt) :=
    ticket_balances_of_value ctxt true arg_type_has_tickets arg in
  let? '(lazy_storage_diff, ctxt) :=
    ticket_diffs_of_lazy_storage_diff ctxt storage_type_has_tickets
      lazy_storage_diff in
  let? '(old_storage_strict, ctxt) :=
    ticket_balances_of_value ctxt false storage_type_has_tickets old_storage in
  let? '(new_storage_strict, ctxt) :=
    ticket_balances_of_value ctxt false storage_type_has_tickets new_storage in
  let? '(subtractions, ctxt) :=
    Ticket_token_map.add ctxt old_storage_strict arg_tickets in
  let? '(additions, ctxt) :=
    Ticket_token_map.add ctxt new_storage_strict lazy_storage_diff in
  Ticket_token_map.sub ctxt additions subtractions.

Definition update_ticket_balances
  (ctxt : Alpha_context.context) (self : Alpha_context.Contract.t)
  (ticket_diffs : Ticket_token_map.t Z.t)
  (operations : list Script_typed_ir.packed_internal_operation)
  : M? (Z.t × Alpha_context.context) :=
  let validate_spending_budget
    (ctxt : Alpha_context.context) (function_parameter : Ticket_token.ex_token)
    : Alpha_context.Script_int.num M? (bool × Alpha_context.context) :=
    let
      '(Ticket_token.Ex_token {|
        Ticket_token.ex_token.Ex_token.ticketer := ticketer |}) as
        ticket_token := function_parameter in
    fun (amount : Alpha_context.Script_int.num) ⇒
      if Alpha_context.Contract.equal ticketer self then
        return? (true, ctxt)
      else
        let? '(balance_diff, ctxt) :=
          Ticket_token_map.balance_diff ctxt ticket_token ticket_diffs in
        return?
          (((Alpha_context.Script_int.to_zint amount) Z (Z.neg balance_diff)),
            ctxt) in
  let? '(ticket_op_diffs, ctxt) :=
    Ticket_operations_diff.ticket_diffs_of_operations ctxt operations in
  let? '(ticket_diffs, ctxt) := Ticket_token_map.to_list ctxt ticket_diffs in
  let? '(total_storage_diff, ctxt) :=
    update_ticket_balances_for_self_contract ctxt self ticket_diffs in
  List.fold_left_es
    (fun (function_parameter : Z.t × Alpha_context.context) ⇒
      let '(total_storage_diff, ctxt) := function_parameter in
      fun (function_parameter : Ticket_operations_diff.ticket_token_diff) ⇒
        let '{|
          Ticket_operations_diff.ticket_token_diff.ticket_token := ticket_token;
            Ticket_operations_diff.ticket_token_diff.total_amount :=
              total_amount;
            Ticket_operations_diff.ticket_token_diff.destinations :=
              destinations
            |} := function_parameter in
        let? '(is_valid_balance_update, ctxt) :=
          validate_spending_budget ctxt ticket_token total_amount in
        let? '_ :=
          Error_monad.error_unless is_valid_balance_update
            (invalid_ticket_transfer_error ticket_token
              (Alpha_context.Script_int.to_zint total_amount)) in
        let? '(destinations, ctxt) :=
          List.fold_left_e
            (fun (function_parameter :
              list (Alpha_context.Destination.t × Z.t) × Alpha_context.context)
              ⇒
              let '(acc_value, ctxt) := function_parameter in
              fun (function_parameter :
                Alpha_context.Destination.t × Alpha_context.Script_int.num) ⇒
                let '(token, amount) := function_parameter in
                let? ctxt :=
                  Alpha_context.Gas.consume ctxt
                    Ticket_costs.Constants.cost_collect_tickets_step in
                return?
                  ((cons (token, (Alpha_context.Script_int.to_zint amount))
                    acc_value), ctxt)) (nil, ctxt) destinations in
        update_ticket_balances_raw ctxt total_storage_diff ticket_token
          destinations) (total_storage_diff, ctxt) ticket_op_diffs.