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) :=
    Error_monad.Lwt_result_syntax.op_letplus
      (Ticket_token_map.find ctxt token map)
      (fun function_parameter
        let '(amnt_opt, ctxt) := function_parameter in
        ((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) :=
    Error_monad.Result_syntax.op_letplus
      (Alpha_context.Gas.consume ctxt (Ticket_costs.add_z_cost b1 b2))
      (fun ctxt((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_e ctxt
        (fun (ctxt : Alpha_context.context) ⇒
          fun (_ex_token : Ticket_token.ex_token) ⇒
            fun (amount : Z.t) ⇒
              Error_monad.Result_syntax.op_letplus
                (Alpha_context.Gas.consume ctxt
                  (Ticket_costs.negate_cost amount))
                (fun ctxt((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_value : 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_value in
  let accum_ticket_balances
    (function_parameter :
      list (Ticket_token.ex_token × Z.t) × Alpha_context.context)
    : Ticket_scanner.ex_ticket
    M? (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_scanner.ex_token_and_amount_of_ex_ticket ticket in
      Error_monad.Result_syntax.op_letplus
        (Alpha_context.Gas.consume ctxt
          Ticket_costs.Constants.cost_collect_tickets_step)
        (fun ctxt
          ((cons (token, (Script_int.to_zint amount)) acc_value), ctxt)) in
  let? '(token_amounts, ctxt) :=
    List.fold_left_e accum_ticket_balances (nil, ctxt) tickets in
  Ticket_token_map.of_list_with_merge ctxt token_amounts.

Definition update_ticket_balances_aux
  (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.parsed_token.ticketer := ticketer;
        Ticket_token.parsed_token.contents_type := _;
        Ticket_token.parsed_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_contract : 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.parsed_token.ticketer := ticketer |} :=
            ticket_token in
          (amount Z Z.zero) ||
          (Alpha_context.Contract.equal ticketer self_contract) in
        let? '_ :=
          Error_monad.error_unless is_valid_balance_update
            (invalid_ticket_transfer_error ticket_token amount) in
        update_ticket_balances_aux ctxt total_storage_diff ticket_token
          [ ((Alpha_context.Destination.Contract self_contract), 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.
We calculate the ticket diff as the following: [new_storage_strict] + [lazy_storage_diff] - ([old_storage_strict] + [arg_tickets])
Additionally, we calculate the ticket receipt as below. We do not subtract the [arg_tickets] since we only want to display the tickets updated in storage for the receipt. [new_storage_strict] + [lazy_storage_diff] - [storage_strict]
Definition ticket_diffs {A B : Set}
  (ctxt : Alpha_context.context) (self_contract : Alpha_context.Contract.t)
  (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 × Ticket_receipt.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? '(additions, ctxt) :=
    Ticket_token_map.add ctxt new_storage_strict lazy_storage_diff in
  let? '(total_storage_diff, ctxt) :=
    Ticket_token_map.sub ctxt additions old_storage_strict in
  let? '(diff_value, ctxt) :=
    Ticket_token_map.sub ctxt total_storage_diff arg_tickets in
  let? '(ticket_receipt, ctxt) :=
    Ticket_token_map.to_ticket_receipt ctxt
      (Alpha_context.Destination.Contract self_contract) total_storage_diff in
  return? (diff_value, ticket_receipt, ctxt).

Definition update_ticket_balances
  (ctxt : Alpha_context.context) (self_contract : 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)
    : Script_int.num M? (bool × Alpha_context.context) :=
    let
      '(Ticket_token.Ex_token {|
        Ticket_token.parsed_token.ticketer := ticketer |}) as ticket_token :=
      function_parameter in
    fun (amount : Script_int.num) ⇒
      if Alpha_context.Contract.equal ticketer self_contract then
        return? (true, ctxt)
      else
        Error_monad.Lwt_result_syntax.op_letplus
          (Ticket_token_map.balance_diff ctxt ticket_token ticket_diffs)
          (fun function_parameter
            let '(balance_diff, ctxt) := function_parameter in
            (((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_contract 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
              (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 × Script_typed_ir.ticket_amount) ⇒
                let '(token, amount) := function_parameter in
                Error_monad.Result_syntax.op_letplus
                  (Alpha_context.Gas.consume ctxt
                    Ticket_costs.Constants.cost_collect_tickets_step)
                  (fun ctxt
                    ((cons (token, (Script_int.to_zint amount)) acc_value), ctxt)))
            (nil, ctxt) destinations in
        update_ticket_balances_aux ctxt total_storage_diff ticket_token
          destinations) (total_storage_diff, ctxt) ticket_op_diffs.