Skip to main content

🎫 Ticket_operations_diff.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Carbonated_map.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Gas_monad.
Require TezosOfOCaml.Proto_alpha.Script_cache.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_tc_errors.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_parameters.

Module ticket_transfer.
  Record record : Set := Build {
    destination : Alpha_context.Destination.t;
    tickets : list Ticket_scanner.ex_ticket;
  }.
  Definition with_destination destination (r : record) :=
    Build destination r.(tickets).
  Definition with_tickets tickets (r : record) :=
    Build r.(destination) tickets.
End ticket_transfer.
Definition ticket_transfer := ticket_transfer.record.

Module ticket_token_diff.
  Record record : Set := Build {
    ticket_token : Ticket_token.ex_token;
    total_amount : Alpha_context.Script_int.num;
    destinations :
      list (Alpha_context.Destination.t × Alpha_context.Script_int.num);
  }.
  Definition with_ticket_token ticket_token (r : record) :=
    Build ticket_token r.(total_amount) r.(destinations).
  Definition with_total_amount total_amount (r : record) :=
    Build r.(ticket_token) total_amount r.(destinations).
  Definition with_destinations destinations (r : record) :=
    Build r.(ticket_token) r.(total_amount) destinations.
End ticket_token_diff.
Definition ticket_token_diff := ticket_token_diff.record.

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 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 } }
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 : Alpha_context.Script_int.num)
    (map :
      Ticket_token_map.t
        (Destination_map.(Carbonated_map.S.t) Alpha_context.Script_int.num))
    : M?
      (Ticket_token_map.t
        (Destination_map.(Carbonated_map.S.t) Alpha_context.Script_int.num) ×
        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) Alpha_context.Script_int.num))
          ⇒
          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 Alpha_context.Script_int.num)
              : M? (option Alpha_context.Script_int.num × 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 (Alpha_context.Script_int.add_n prev_amount amount)),
                    ctxt)
              | Nonereturn? ((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 parse_and_cache_script
  (ctxt : Alpha_context.context) (destination : Alpha_context.Contract.t)
  (get_non_cached_script :
    Alpha_context.context M? (Alpha_context.Script.t × Alpha_context.context))
  : M? (Script_ir_translator.ex_script × Alpha_context.context) :=
  let? '(ctxt, _cache_key, cached) := Script_cache.find ctxt destination in
  match cached with
  | Some (_script, ex_script)return? (ex_script, ctxt)
  | None
    let? '(script, ctxt) := get_non_cached_script ctxt in
    let? '(ex_script, ctxt) :=
      Script_ir_translator.parse_script None ctxt true true script in
    let '(size_value, cost) := Script_ir_translator.script_size ex_script in
    let? ctxt := Alpha_context.Gas.consume ctxt cost in
    let? ctxt :=
      Script_cache.insert ctxt destination (script, ex_script) size_value in
    return? (ex_script, ctxt)
  end.

Definition cast_transaction_parameter {b a : Set}
  (ctxt : Alpha_context.context) (location : Alpha_context.Script.location)
  (entry_arg_ty : Script_typed_ir.ty) (parameters_ty : Script_typed_ir.ty)
  (parameters : b) : M? (a × Alpha_context.context) :=
  let? '(res, ctxt) :=
    Gas_monad.run ctxt
      (Script_ir_translator.ty_eq Script_tc_errors.Informative location
        entry_arg_ty parameters_ty) in
  let? 'Script_ir_translator.Eq := res in
  return? ((cast a parameters), ctxt).

Definition tickets_of_transaction {A : Set}
  (ctxt : Alpha_context.context) (destination : Alpha_context.Contract.contract)
  (entrypoint : Alpha_context.Entrypoint.t)
  (location : Alpha_context.Script.location)
  (parameters_ty : Script_typed_ir.ty) (parameters : A)
  : M? (option ticket_transfer × Alpha_context.context) :=
  match Alpha_context.Contract.is_implicit destination with
  | Some _return? (None, ctxt)
  | None
    let?
      '(Script_ir_translator.Ex_script
        (Script_typed_ir.Script {|
          Script_typed_ir.script.Script.arg_type := arg_type;
            Script_typed_ir.script.Script.entrypoints := entrypoints
            |}), ctxt) :=
      parse_and_cache_script ctxt destination
        (fun (ctxt : Alpha_context.context) ⇒
          let? '(ctxt, script_opt) :=
            Alpha_context.Contract.get_script ctxt destination in
          match script_opt with
          | None
            Error_monad.fail
              (Build_extensible "Failed_to_get_script"
                Alpha_context.Contract.contract destination)
          | Some scriptreturn? (script, ctxt)
          end) in
    let 'existT _ __Ex_script_'a [ctxt, entrypoints, arg_type] :=
      cast_exists (Es := Set)
        (fun __Ex_script_'a
          [Alpha_context.context ** Script_typed_ir.entrypoints **
            Script_typed_ir.ty]) [ctxt, entrypoints, arg_type] in
    let? '(res, ctxt) :=
      ((Gas_monad.run ctxt
        (Script_ir_translator.find_entrypoint Script_tc_errors.Informative
          arg_type entrypoints entrypoint)) :
        M?
          (M? (Script_ir_translator.ex_ty_cstr __Ex_script_'a) ×
            Alpha_context.context)) in
    let?
      'Script_ir_translator.Ex_ty_cstr {|
        Script_ir_translator.ex_ty_cstr.Ex_ty_cstr.ty := entry_arg_ty |} :=
      res in
    let 'existT _ __Ex_ty_cstr_'b entry_arg_ty :=
      cast_exists (Es := Set) (fun __Ex_ty_cstr_'bScript_typed_ir.ty)
        entry_arg_ty in
    let? '(has_tickets_value, ctxt) :=
      Ticket_scanner.type_has_tickets ctxt entry_arg_ty in
    let? '(parameters, ctxt) :=
      cast_transaction_parameter ctxt location entry_arg_ty parameters_ty
        parameters in
    let? '(tickets, ctxt) :=
      Ticket_scanner.tickets_of_value ctxt true has_tickets_value
        (parameters : __Ex_ty_cstr_'b) in
    return?
      ((Some
        {|
          ticket_transfer.destination :=
            Alpha_context.Destination.Contract destination;
          ticket_transfer.tickets := tickets; |}), ctxt)
  end.

Extract tickets of an origination operation by scanning the storage.
Definition tickets_of_origination {A : Set}
  (ctxt : Alpha_context.context) (preorigination : Alpha_context.Contract.t)
  (storage_type : Script_typed_ir.ty) (storage_value : A)
  : M? (option ticket_transfer × Alpha_context.context) :=
  let? '(has_tickets_value, ctxt) :=
    Ticket_scanner.type_has_tickets ctxt storage_type in
  let? '(tickets, ctxt) :=
    Ticket_scanner.tickets_of_value ctxt true has_tickets_value storage_value in
  return?
    ((Some
      {|
        ticket_transfer.destination :=
          Alpha_context.Destination.Contract preorigination;
        ticket_transfer.tickets := tickets; |}), ctxt).

Definition tickets_of_operation
  (ctxt : Alpha_context.context)
  (function_parameter : Script_typed_ir.packed_internal_operation)
  : M? (option ticket_transfer × Alpha_context.context) :=
  let
    'Script_typed_ir.Internal_operation {|
      Script_typed_ir.internal_operation.source := _;
        Script_typed_ir.internal_operation.operation := operation;
        Script_typed_ir.internal_operation.nonce := _
        |} := function_parameter in
  match operation with
  |
    Script_typed_ir.Transaction {|
      Script_typed_ir.manager_operation.Transaction.transaction := {|
        Alpha_context.transaction.amount := _;
          Alpha_context.transaction.parameters := _;
          Alpha_context.transaction.entrypoint := entrypoint;
          Alpha_context.transaction.destination :=
            Alpha_context.Destination.Contract destination
          |};
        Script_typed_ir.manager_operation.Transaction.location := location;
        Script_typed_ir.manager_operation.Transaction.parameters_ty :=
          parameters_ty;
        Script_typed_ir.manager_operation.Transaction.parameters := parameters
        |} ⇒
    tickets_of_transaction ctxt destination entrypoint location parameters_ty
      parameters
  |
    Script_typed_ir.Transaction {|
      Script_typed_ir.manager_operation.Transaction.transaction := {|
        Alpha_context.transaction.amount := _;
          Alpha_context.transaction.parameters := _;
          Alpha_context.transaction.entrypoint := entrypoint;
          Alpha_context.transaction.destination :=
            Alpha_context.Destination.Tx_rollup tx_rollup_dest
          |};
        Script_typed_ir.manager_operation.Transaction.location := _;
        Script_typed_ir.manager_operation.Transaction.parameters_ty :=
          parameters_ty;
        Script_typed_ir.manager_operation.Transaction.parameters := parameters
        |} ⇒
    if
      Alpha_context.Entrypoint.op_eq entrypoint
        Alpha_context.Tx_rollup.deposit_entrypoint
    then
      let? '{|
        Tx_rollup_parameters.deposit_parameters.ex_ticket := ex_ticket;
          Tx_rollup_parameters.deposit_parameters.l2_destination := _
          |} :=
        Tx_rollup_parameters.get_deposit_parameters parameters_ty parameters in
      return?
        ((Some
          {|
            ticket_transfer.destination :=
              Alpha_context.Destination.Tx_rollup tx_rollup_dest;
            ticket_transfer.tickets := [ ex_ticket ]; |}), ctxt)
    else
      return? (None, ctxt)
  |
    Script_typed_ir.Origination {|
      Script_typed_ir.manager_operation.Origination.origination := {|
        Alpha_context.origination.delegate := _;
          Alpha_context.origination.script := _;
          Alpha_context.origination.credit := _
          |};
        Script_typed_ir.manager_operation.Origination.preorigination :=
          preorigination;
        Script_typed_ir.manager_operation.Origination.storage_type :=
          storage_type;
        Script_typed_ir.manager_operation.Origination.storage := storage_value
        |} ⇒
    tickets_of_origination ctxt preorigination storage_type storage_value
  | Script_typed_ir.Delegation _return? (None, ctxt)
  end.

Definition add_transfer_to_token_map
  (ctxt : Alpha_context.context)
  (token_map :
    Ticket_token_map.t
      (Destination_map.(Carbonated_map.S.t) Alpha_context.Script_int.num))
  (function_parameter : ticket_transfer)
  : M?
    (Ticket_token_map.t
      (Destination_map.(Carbonated_map.S.t) Alpha_context.Script_int.num) ×
      Alpha_context.context) :=
  let '{|
    ticket_transfer.destination := destination;
      ticket_transfer.tickets := tickets
      |} := function_parameter in
  List.fold_left_es
    (fun (function_parameter :
      Ticket_token_map.t
        (Destination_map.(Carbonated_map.S.t) Alpha_context.Script_int.num) ×
        Alpha_context.context) ⇒
      let '(token_map, ctxt) := function_parameter in
      fun (ticket : Ticket_scanner.ex_ticket) ⇒
        let '(ticket_token, amount) :=
          Ticket_token.token_and_amount_of_ex_ticket ticket in
        Ticket_token_map.add ctxt ticket_token destination amount token_map)
    (token_map, ctxt) tickets.

Definition ticket_token_map_of_operations
  (ctxt : Alpha_context.context)
  (ops : list Script_typed_ir.packed_internal_operation)
  : M?
    (Ticket_token_map.t
      (Destination_map.(Carbonated_map.S.t) Alpha_context.Script_int.num) ×
      Alpha_context.context) :=
  List.fold_left_es
    (fun (function_parameter :
      Ticket_token_map.t
        (Destination_map.(Carbonated_map.S.t) Alpha_context.Script_int.num) ×
        Alpha_context.context) ⇒
      let '(token_map, ctxt) := function_parameter in
      fun (op : Script_typed_ir.packed_internal_operation) ⇒
        let? '(res, ctxt) := tickets_of_operation ctxt op in
        match res with
        | Some ticket_trans
          add_transfer_to_token_map ctxt token_map ticket_trans
        | Nonereturn? (token_map, ctxt)
        end) (Ticket_token_map.empty, ctxt) ops.

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 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) Alpha_context.Script_int.num)
            ⇒
            let? '(total_amount, ctxt) :=
              Destination_map.(Carbonated_map.S.fold) ctxt
                (fun (ctxt : Alpha_context.context) ⇒
                  fun (total_amount : Alpha_context.Script_int.num) ⇒
                    fun (_destination : Alpha_context.Destination.t) ⇒
                      fun (amount : Alpha_context.Script_int.num) ⇒
                        let? ctxt :=
                          Alpha_context.Gas.consume ctxt
                            (Ticket_costs.add_int_cost total_amount amount) in
                        return?
                          ((Alpha_context.Script_int.add_n total_amount amount),
                            ctxt)) Alpha_context.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.