Skip to main content

🐆 Tx_rollup_ticket.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.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.

Definition parse_ticket {a : Set}
  (consume_deserialization_gas :
    Alpha_context.Script.consume_deserialization_gas)
  (ticketer : Alpha_context.Contract.t)
  (contents : Alpha_context.Script.lazy_expr)
  (ty : Alpha_context.Script.lazy_expr) (ctxt : Alpha_context.context)
  : M? (Alpha_context.context × Ticket_token.ex_token) :=
  let? '(ty, ctxt) :=
    Alpha_context.Script.force_decode_in_context consume_deserialization_gas
      ctxt ty in
  let? '(contents, ctxt) :=
    Alpha_context.Script.force_decode_in_context consume_deserialization_gas
      ctxt contents in
  let? '(Script_ir_translator.Ex_comparable_ty contents_type, ctxt) :=
    Script_ir_translator.parse_comparable_ty ctxt (Micheline.root_value ty) in
  let? '(contents, ctxt) :=
    (Script_ir_translator.parse_comparable_data (a := a)) None ctxt
      contents_type (Micheline.root_value contents) in
  return?
    (ctxt,
      (Ticket_token.Ex_token
        {| Ticket_token.ex_token.Ex_token.ticketer := ticketer;
          Ticket_token.ex_token.Ex_token.contents_type := contents_type;
          Ticket_token.ex_token.Ex_token.contents := contents; |})).

Definition parse_ticket_and_operation {a : Set}
  (consume_deserialization_gas :
    Alpha_context.Script.consume_deserialization_gas)
  (ticketer : Alpha_context.Contract.t)
  (contents : Alpha_context.Script.lazy_expr)
  (ty : Alpha_context.Script.lazy_expr)
  (source : Alpha_context.Contract.contract)
  (destination : Alpha_context.Destination.t)
  (entrypoint : Alpha_context.Entrypoint.t) (amount : Z.t)
  (ctxt : Alpha_context.context)
  : M?
    (Alpha_context.context × Ticket_token.ex_token ×
      Script_typed_ir.packed_internal_operation) :=
  let? '(ty, ctxt) :=
    Alpha_context.Script.force_decode_in_context consume_deserialization_gas
      ctxt ty in
  let? '(contents, ctxt) :=
    Alpha_context.Script.force_decode_in_context consume_deserialization_gas
      ctxt contents in
  let? '(Script_ir_translator.Ex_comparable_ty contents_type, ctxt) :=
    Script_ir_translator.parse_comparable_ty ctxt (Micheline.root_value ty) in
  let? '(contents, ctxt) :=
    (Script_ir_translator.parse_comparable_data (a := a)) None ctxt
      contents_type (Micheline.root_value contents) in
  let ticket_token :=
    Ticket_token.Ex_token
      {| Ticket_token.ex_token.Ex_token.ticketer := ticketer;
        Ticket_token.ex_token.Ex_token.contents_type := contents_type;
        Ticket_token.ex_token.Ex_token.contents := contents; |} in
  let? amount_node :=
    Option.value_e
      (Alpha_context.Script_int.is_nat (Alpha_context.Script_int.of_zint amount))
      (Error_monad.trace_of_error
        (Build_extensible "Internal_error" string
          "Ticket quantity is negative, this can't happen because it comes from a qty."))
    in
  let? ticket_ty :=
    Script_typed_ir.ticket_t Micheline.dummy_location contents_type in
  let ticket :=
    {| Script_typed_ir.ticket.ticketer := ticketer;
      Script_typed_ir.ticket.contents := contents;
      Script_typed_ir.ticket.amount := amount_node; |} in
  let? '(parameters_expr, ctxt) :=
    Script_ir_translator.unparse_data ctxt Script_ir_translator.Optimized
      ticket_ty ticket in
  let? ctxt :=
    Alpha_context.Gas.consume ctxt
      (Alpha_context.Script.strip_locations_cost parameters_expr) in
  let parameters :=
    Alpha_context.Script.lazy_expr_value
      (Micheline.strip_locations parameters_expr) in
  let? '(ctxt, nonce_value) := Alpha_context.fresh_internal_nonce ctxt in
  let op :=
    Script_typed_ir.Internal_operation
      {| Script_typed_ir.internal_operation.source := source;
        Script_typed_ir.internal_operation.operation :=
          Script_typed_ir.Transaction
            {|
              Script_typed_ir.manager_operation.Transaction.transaction :=
                {| Alpha_context.transaction.amount := Alpha_context.Tez.zero;
                  Alpha_context.transaction.parameters := parameters;
                  Alpha_context.transaction.entrypoint := entrypoint;
                  Alpha_context.transaction.destination := destination; |};
              Script_typed_ir.manager_operation.Transaction.location :=
                Micheline.location parameters_expr;
              Script_typed_ir.manager_operation.Transaction.parameters_ty :=
                ticket_ty;
              Script_typed_ir.manager_operation.Transaction.parameters :=
                ticket; |};
        Script_typed_ir.internal_operation.nonce := nonce_value; |} in
  return? (ctxt, ticket_token, op).

Definition make_withdraw_order
  (ctxt : Alpha_context.context) (tx_rollup : Alpha_context.Tx_rollup.t)
  (ex_ticket : Ticket_token.ex_token) (claimer : Signature.public_key_hash)
  (amount : Tx_rollup_l2_qty.t)
  : M? (Alpha_context.context × Alpha_context.Tx_rollup_withdraw.order) :=
  let? '(tx_rollup_ticket_hash, ctxt) :=
    Ticket_balance_key.of_ex_token ctxt
      (Alpha_context.Destination.Tx_rollup tx_rollup) ex_ticket in
  let withdrawal :=
    {| Alpha_context.Tx_rollup_withdraw.order.claimer := claimer;
      Alpha_context.Tx_rollup_withdraw.order.ticket_hash :=
        tx_rollup_ticket_hash;
      Alpha_context.Tx_rollup_withdraw.order.amount := amount; |} in
  return? (ctxt, withdrawal).

Definition transfer_ticket_with_hashes
  (ctxt : Alpha_context.context) (src_hash : Alpha_context.Ticket_hash.t)
  (dst_hash : Alpha_context.Ticket_hash.t) (qty : Z.t)
  : M? (Alpha_context.context × Z.t) :=
  let? '(src_storage_diff, ctxt) :=
    Alpha_context.Ticket_balance.adjust_balance ctxt src_hash (Z.neg qty) in
  let? '(dst_storage_diff, ctxt) :=
    Alpha_context.Ticket_balance.adjust_balance ctxt dst_hash qty in
  let? '(diff_value, ctxt) :=
    Alpha_context.Ticket_balance.adjust_storage_space ctxt
      (src_storage_diff +Z dst_storage_diff) in
  return? (ctxt, diff_value).

Definition transfer_ticket
  (ctxt : Alpha_context.context) (src : Alpha_context.Destination.t)
  (dst : Alpha_context.Destination.t) (ex_token : Ticket_token.ex_token)
  (qty : Z.t) : M? (Alpha_context.context × Z.t) :=
  let? '(src_hash, ctxt) := Ticket_balance_key.of_ex_token ctxt src ex_token in
  let? '(dst_hash, ctxt) := Ticket_balance_key.of_ex_token ctxt dst ex_token in
  transfer_ticket_with_hashes ctxt src_hash dst_hash qty.