🎫 Ticket_operations_diff.v

Translated 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.Permanent "Failed_to_get_script"
      "Failed to get script for contract"
      "Failed to get script for contract when scanning operations for tickets"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (contract : Alpha_context.Contract.t) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Failed to get script for contract "
                  (CamlinternalFormatBasics.Alpha
                    CamlinternalFormatBasics.End_of_format))
                "Failed to get script for contract %a")
              Alpha_context.Contract.pp contract))
      (Data_encoding.obj1
        (Data_encoding.req None None "contract" Alpha_context.Contract.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Failed_to_get_script" then
            let c_value := cast Alpha_context.Contract.t payload in
            Some c_value
          else None
        end)
      (fun (c_value : Alpha_context.Contract.t) ⇒
        Build_extensible "Failed_to_get_script" Alpha_context.Contract.t c_value)
    in
  Error_monad.register_error_kind Error_monad.Permanent
    "contract_not_originated" "Contract not originated"
    "Non originated contract detected in ticket update."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Contract was not pre-originated"
                CamlinternalFormatBasics.End_of_format)
              "Contract was not pre-originated"))) Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Contract_not_originated" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Contract_not_originated" unit tt).

A carbonated map where the keys are destination (contract or tx_rollup).

Definition Destination_map :=
  Carbonated_map.Make
    (let context : Set := Alpha_context.context in
    let consume := Alpha_context.Gas.consume in
    {|
      Carbonated_map.GAS.consume := consume
    |})
    (let t : Set := Alpha_context.Destination.t in
    let compare := Alpha_context.Destination.compare in
    let compare_cost {A : Set} (function_parameter : A)
      : Alpha_context.Gas.cost :=
      let '_ := function_parameter in
      Ticket_costs.Constants.cost_compare_key_contract in
    {|
      Carbonated_map.COMPARABLE.compare := compare;
      Carbonated_map.COMPARABLE.compare_cost := compare_cost
    |}).

A module for mapping ticket-tokens to a map of contract destinations and amounts. The values specify how to distribute the spending of a ticket-token across different contracts.

In the example below, there is a total of 4 Token1 ticket-tokens transferred: three units are sent to contract K1 and one unit to K2. Additionally, there are 12 units of Token2 sent to K2, K7 and K8. And one unit of Token3 sent to K1. { Token1 -> { K1 -> 3, K2 -> 1 } Token2 -> { K2 -> 1, K7 -> 10, K8 -> 1} Token3 -> { K1 -> 1 } }

Module Ticket_token_map.
Include Proto_alpha.Ticket_token_map.

Adds a ticket-token with a destination and an amount to the map. The layout of the map parameter is as described above. Its type is:

(n num Destination_map.t) Ticket_token_map.t

As explained above, the inner map expresses a list of destination contracts and outgoing amount pairs.

Invariant: The internal contract-indexed map cannot be empty.

  Definition add
    (ctxt : Alpha_context.context) (ticket_token : Ticket_token.ex_token)
    (destination : Alpha_context.Destination.t) (amount : Ticket_amount.t)
    (map :
      Ticket_token_map.t (Destination_map.(Carbonated_map.S.t) Ticket_amount.t))
    : M ?
      (Ticket_token_map.t (Destination_map.(Carbonated_map.S.t) Ticket_amount.t)
        × Alpha_context.context ) :=
    Ticket_token_map.update ctxt ticket_token
      (fun (ctxt : Alpha_context.context) ⇒
        fun (old_val :
          option (Destination_map.(Carbonated_map.S.t) Ticket_amount.t)) ⇒
          match old_val with
          | None ⇒
            let map :=
              Destination_map.(Carbonated_map.S.singleton) destination amount in
            return ? ((Some map), ctxt)
          | Some destination_map ⇒
            let update
              (ctxt : Alpha_context.context)
              (prev_amt_opt : option Ticket_amount.t)
              : M ? (option Ticket_amount.t × Alpha_context.context ) :=
              match prev_amt_opt with
              | Some prev_amount ⇒
                let ? ctxt :=
                  Alpha_context.Gas.consume ctxt
                    (Ticket_costs.add_int_cost prev_amount amount) in
                return ? ((Some (Ticket_amount.add prev_amount amount)), ctxt)
              | None ⇒ return ? ((Some amount), ctxt)
              end in
            let ? '(destination_map , ctxt ) :=
              Destination_map.(Carbonated_map.S.update) ctxt destination update
                destination_map in
            return ? ((Some destination_map), ctxt)
          end) map.
End Ticket_token_map.

Definition tickets_of_transaction {A : Set}
  (ctxt : Alpha_context.context) (destination : Alpha_context.Destination.t)
  (parameters_ty : Script_typed_ir.ty) (parameters : A)
  : M ? (option ticket_transfer × Alpha_context.context ) :=
  let ? '(has_tickets_value , ctxt ) :=
    Ticket_scanner.type_has_tickets ctxt parameters_ty in
  let ? '(tickets , ctxt ) :=
    Ticket_scanner.tickets_of_value ctxt true has_tickets_value parameters in
  return ?
    ((Some
      {| ticket_transfer.destination := destination;
        ticket_transfer.tickets := tickets; |}), ctxt).

Extract tickets of an origination operation by scanning the storage.

Traverses a list of operations and scans for tickets.

Definition ticket_diffs_of_operations
  (ctxt : Alpha_context.context)
  (operations : list Script_typed_ir.packed_internal_operation)
  : M ? (list ticket_token_diff × Alpha_context.context ) :=
  let ? '(token_map , ctxt ) := ticket_token_map_of_operations ctxt operations in
  Ticket_token_map.fold_e ctxt
    (fun (ctxt : Alpha_context.context) ⇒
      fun (acc_value : list ticket_token_diff) ⇒
        fun (ticket_token : Ticket_token.ex_token) ⇒
          fun (destination_map :
            Destination_map.(Carbonated_map.S.t) Ticket_amount.t) ⇒
            let ? '(total_amount , ctxt ) :=
              Destination_map.(Carbonated_map.S.fold_e) ctxt
                (fun (ctxt : Alpha_context.t) ⇒
                  fun (total_amount : Script_int.num) ⇒
                    fun (_destination : Alpha_context.Destination.t) ⇒
                      fun (amount : Ticket_amount.t) ⇒
                        let ? ctxt :=
                          Alpha_context.Gas.consume ctxt
                            (Ticket_costs.add_int_cost total_amount amount) in
                        return ? ((Script_int.add_n total_amount amount), ctxt))
                Script_int.zero_n destination_map in
            let ? '(destinations , ctxt ) :=
              Destination_map.(Carbonated_map.S.to_list) ctxt destination_map in
            return ?
              ((cons
                {| ticket_token_diff.ticket_token := ticket_token;
                  ticket_token_diff.total_amount := total_amount;
                  ticket_token_diff.destinations := destinations; |} acc_value),
                ctxt)) nil token_map.