🎫 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 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 : 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)
              | 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 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 script ⇒ return ? (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_'b ⇒ Script_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.

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.