🎫 Ticket_transfer.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Definition parse_ticket
(consume_deserialization_gas :
Alpha_context.Script.consume_deserialization_gas)
(ticketer : Alpha_context.Contract.t)
(contents : Alpha_context.Script.lazy_expr)
(ty_value : Alpha_context.Script.lazy_expr) (ctxt : Alpha_context.context)
: M? (Alpha_context.context × Ticket_token.ex_token) :=
let? '(ty_value, ctxt) :=
Alpha_context.Script.force_decode_in_context consume_deserialization_gas
ctxt ty_value 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_value) in
let 'existT _ __Ex_comparable_ty_'a [ctxt, contents_type] :=
cast_exists (Es := Set)
(fun __Ex_comparable_ty_'a ⇒
[Alpha_context.context ** Script_typed_ir.comparable_ty])
[ctxt, contents_type] in
let? '(contents, ctxt) :=
((Script_ir_translator.parse_comparable_data None ctxt contents_type
(Micheline.root_value contents)) :
M? (__Ex_comparable_ty_'a × Alpha_context.context)) in
let token :=
Ticket_token.Ex_token
{| Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents; |} in
return? (ctxt, token).
Definition parse_ticket_and_operation
(consume_deserialization_gas :
Alpha_context.Script.consume_deserialization_gas)
(ticketer : Alpha_context.Contract.t)
(contents : Alpha_context.Script.lazy_expr)
(ty_value : Alpha_context.Script.lazy_expr)
(source : Alpha_context.Contract.t) (destination : Contract_hash.t)
(entrypoint : Alpha_context.Entrypoint.t)
(amount : Script_typed_ir.ticket_amount) (ctxt : Alpha_context.context)
: M?
(Alpha_context.context × Ticket_token.ex_token ×
Script_typed_ir.packed_internal_operation) :=
let?
'(ctxt,
(Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents
|}) as token) :=
parse_ticket consume_deserialization_gas ticketer contents ty_value ctxt 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; |} in
let? '(unparsed_parameters, ctxt) :=
Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
ticket_ty ticket 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_to_smart_contract
{|
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
:= destination;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
:= Alpha_context.Tez.zero;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
:= entrypoint;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.location
:= Micheline.dummy_location;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters_ty
:= ticket_ty;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters
:= ticket;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
:= unparsed_parameters; |};
Script_typed_ir.internal_operation.nonce := nonce_value; |} in
return? (ctxt, token, op).
Definition transfer_ticket_with_hashes
(ctxt : Alpha_context.context) (src_hash : Alpha_context.Ticket_hash.t)
(dst_hash : Alpha_context.Ticket_hash.t) (qty : Ticket_amount.t)
: M? (Alpha_context.context × Z.t) :=
let qty := Script_int.to_zint qty in
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 : Ticket_amount.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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.
Require TezosOfOCaml.Proto_alpha.Script_ir_unparser.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_amount.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Definition parse_ticket
(consume_deserialization_gas :
Alpha_context.Script.consume_deserialization_gas)
(ticketer : Alpha_context.Contract.t)
(contents : Alpha_context.Script.lazy_expr)
(ty_value : Alpha_context.Script.lazy_expr) (ctxt : Alpha_context.context)
: M? (Alpha_context.context × Ticket_token.ex_token) :=
let? '(ty_value, ctxt) :=
Alpha_context.Script.force_decode_in_context consume_deserialization_gas
ctxt ty_value 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_value) in
let 'existT _ __Ex_comparable_ty_'a [ctxt, contents_type] :=
cast_exists (Es := Set)
(fun __Ex_comparable_ty_'a ⇒
[Alpha_context.context ** Script_typed_ir.comparable_ty])
[ctxt, contents_type] in
let? '(contents, ctxt) :=
((Script_ir_translator.parse_comparable_data None ctxt contents_type
(Micheline.root_value contents)) :
M? (__Ex_comparable_ty_'a × Alpha_context.context)) in
let token :=
Ticket_token.Ex_token
{| Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents; |} in
return? (ctxt, token).
Definition parse_ticket_and_operation
(consume_deserialization_gas :
Alpha_context.Script.consume_deserialization_gas)
(ticketer : Alpha_context.Contract.t)
(contents : Alpha_context.Script.lazy_expr)
(ty_value : Alpha_context.Script.lazy_expr)
(source : Alpha_context.Contract.t) (destination : Contract_hash.t)
(entrypoint : Alpha_context.Entrypoint.t)
(amount : Script_typed_ir.ticket_amount) (ctxt : Alpha_context.context)
: M?
(Alpha_context.context × Ticket_token.ex_token ×
Script_typed_ir.packed_internal_operation) :=
let?
'(ctxt,
(Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := contents_type;
Ticket_token.parsed_token.contents := contents
|}) as token) :=
parse_ticket consume_deserialization_gas ticketer contents ty_value ctxt 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; |} in
let? '(unparsed_parameters, ctxt) :=
Script_ir_translator.unparse_data ctxt Script_ir_unparser.Optimized
ticket_ty ticket 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_to_smart_contract
{|
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.destination
:= destination;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.amount
:= Alpha_context.Tez.zero;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.entrypoint
:= entrypoint;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.location
:= Micheline.dummy_location;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters_ty
:= ticket_ty;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.parameters
:= ticket;
Script_typed_ir.internal_operation_contents.Transaction_to_smart_contract.unparsed_parameters
:= unparsed_parameters; |};
Script_typed_ir.internal_operation.nonce := nonce_value; |} in
return? (ctxt, token, op).
Definition transfer_ticket_with_hashes
(ctxt : Alpha_context.context) (src_hash : Alpha_context.Ticket_hash.t)
(dst_hash : Alpha_context.Ticket_hash.t) (qty : Ticket_amount.t)
: M? (Alpha_context.context × Z.t) :=
let qty := Script_int.to_zint qty in
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 : Ticket_amount.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.