🎫 Ticket_accounting.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.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Ticket_operations_diff.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Module Invalid_ticket_transfer.
Record record : Set := Build {
ticketer : string;
amount : Z.t;
}.
Definition with_ticketer ticketer (r : record) :=
Build ticketer r.(amount).
Definition with_amount amount (r : record) :=
Build r.(ticketer) amount.
End Invalid_ticket_transfer.
Definition Invalid_ticket_transfer := Invalid_ticket_transfer.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Ticket_balance_key.
Require TezosOfOCaml.Proto_alpha.Ticket_costs.
Require TezosOfOCaml.Proto_alpha.Ticket_lazy_storage_diff.
Require TezosOfOCaml.Proto_alpha.Ticket_operations_diff.
Require TezosOfOCaml.Proto_alpha.Ticket_receipt.
Require TezosOfOCaml.Proto_alpha.Ticket_scanner.
Require TezosOfOCaml.Proto_alpha.Ticket_token.
Require TezosOfOCaml.Proto_alpha.Ticket_token_map.
Module Invalid_ticket_transfer.
Record record : Set := Build {
ticketer : string;
amount : Z.t;
}.
Definition with_ticketer ticketer (r : record) :=
Build ticketer r.(amount).
Definition with_amount amount (r : record) :=
Build r.(ticketer) amount.
End Invalid_ticket_transfer.
Definition Invalid_ticket_transfer := Invalid_ticket_transfer.record.
Init function; without side-effects in Coq
Definition init_module : unit :=
Error_monad.register_error_kind Error_monad.Permanent
"invalid_ticket_transfer" "Invalid ticket transfer"
"Invalid ticket transfer detected in ticket balance update."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : string × Z.t) ⇒
let '(ticketer, amount) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Attempted to send "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" unit(s) of a ticket created by "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Attempted to send %a unit(s) of a ticket created by %s.")
Z.pp_print amount ticketer))
(Data_encoding.obj2
(Data_encoding.req None None "ticketer" Data_encoding.string_value)
(Data_encoding.req None None "amount" Data_encoding.z_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_ticket_transfer" then
let '{|
Invalid_ticket_transfer.ticketer := ticketer;
Invalid_ticket_transfer.amount := amount
|} := cast Invalid_ticket_transfer payload in
Some (ticketer, amount)
else None
end)
(fun (function_parameter : string × Z.t) ⇒
let '(ticketer, amount) := function_parameter in
Build_extensible "Invalid_ticket_transfer" Invalid_ticket_transfer
{| Invalid_ticket_transfer.ticketer := ticketer;
Invalid_ticket_transfer.amount := amount; |}).
Module Ticket_token_map.
Include Proto_alpha.Ticket_token_map.
Definition balance_diff
(ctxt : Alpha_context.context) (token : Ticket_token.ex_token)
(map : Ticket_token_map.t Z.t) : M? (Z.t × Alpha_context.context) :=
Error_monad.Lwt_result_syntax.op_letplus
(Ticket_token_map.find ctxt token map)
(fun function_parameter ⇒
let '(amnt_opt, ctxt) := function_parameter in
((Option.value_value amnt_opt Z.zero), ctxt)).
Definition merge_overlap (ctxt : Alpha_context.context) (b1 : Z.t) (b2 : Z.t)
: M? (Z.t × Alpha_context.context) :=
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt (Ticket_costs.add_z_cost b1 b2))
(fun ctxt ⇒ ((b1 +Z b2), ctxt)).
Definition of_list_with_merge
(ctxt : Alpha_context.context)
(token_amounts : list (Ticket_token.ex_token × Z.t))
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
Ticket_token_map.of_list ctxt merge_overlap token_amounts.
Definition add (ctxt : Alpha_context.context)
: Ticket_token_map.t Z.t → Ticket_token_map.t Z.t →
M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
Ticket_token_map.merge ctxt merge_overlap.
Definition sub
(ctxt : Alpha_context.context) (m1 : Ticket_token_map.t Z.t) (m2 : t Z.t)
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
let? '(m2, ctxt) :=
map_e ctxt
(fun (ctxt : Alpha_context.context) ⇒
fun (_ex_token : Ticket_token.ex_token) ⇒
fun (amount : Z.t) ⇒
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt
(Ticket_costs.negate_cost amount))
(fun ctxt ⇒ ((Z.neg amount), ctxt))) m2 in
add ctxt m1 m2.
End Ticket_token_map.
Definition ticket_balances_of_value {A : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(ty_value : Ticket_scanner.has_tickets) (value_value : A)
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
let? '(tickets, ctxt) :=
Ticket_scanner.tickets_of_value ctxt include_lazy ty_value value_value in
let accum_ticket_balances
(function_parameter :
list (Ticket_token.ex_token × Z.t) × Alpha_context.context)
: Ticket_scanner.ex_ticket →
M? (list (Ticket_token.ex_token × Z.t) × Alpha_context.context) :=
let '(acc_value, ctxt) := function_parameter in
fun (ticket : Ticket_scanner.ex_ticket) ⇒
let '(token, amount) :=
Ticket_scanner.ex_token_and_amount_of_ex_ticket ticket in
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step)
(fun ctxt ⇒
((cons (token, (Script_int.to_zint amount)) acc_value), ctxt)) in
let? '(token_amounts, ctxt) :=
List.fold_left_e accum_ticket_balances (nil, ctxt) tickets in
Ticket_token_map.of_list_with_merge ctxt token_amounts.
Definition update_ticket_balances_aux
(ctxt : Alpha_context.context) (total_storage_diff : Z.t)
(token : Ticket_token.ex_token)
(destinations : list (Alpha_context.Destination.t × Z.t))
: M? (Z.t × Alpha_context.context) :=
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(tot_storage_diff, ctxt) := function_parameter in
fun (function_parameter : Alpha_context.Destination.t × Z.t) ⇒
let '(owner, delta) := function_parameter in
let? '(key_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt owner token in
let? '(storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_balance ctxt key_hash delta in
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Ticket_costs.add_z_cost total_storage_diff storage_diff) in
return? ((tot_storage_diff +Z storage_diff), ctxt))
(total_storage_diff, ctxt) destinations.
Definition invalid_ticket_transfer_error
(function_parameter : Ticket_token.ex_token) : Z.t → Error_monad._error :=
let
'Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := _;
Ticket_token.parsed_token.contents := _
|} := function_parameter in
fun (amount : Z.t) ⇒
Build_extensible "Invalid_ticket_transfer" Invalid_ticket_transfer
{|
Invalid_ticket_transfer.ticketer :=
Alpha_context.Contract.to_b58check ticketer;
Invalid_ticket_transfer.amount := amount; |}.
Definition update_ticket_balances_for_self_contract
(ctxt : Alpha_context.context) (self_contract : Alpha_context.Contract.t)
(ticket_diffs : list (Ticket_token.ex_token × Z.t))
: M? (Z.t × Alpha_context.context) :=
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(total_storage_diff, ctxt) := function_parameter in
fun (function_parameter : Ticket_token.ex_token × Z.t) ⇒
let '(ticket_token, amount) := function_parameter in
let is_valid_balance_update :=
let
'Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer |} :=
ticket_token in
(amount ≤Z Z.zero) ||
(Alpha_context.Contract.equal ticketer self_contract) in
let? '_ :=
Error_monad.error_unless is_valid_balance_update
(invalid_ticket_transfer_error ticket_token amount) in
update_ticket_balances_aux ctxt total_storage_diff ticket_token
[ ((Alpha_context.Destination.Contract self_contract), amount) ])
(Z.zero, ctxt) ticket_diffs.
Definition ticket_diffs_of_lazy_storage_diff
(ctxt : Alpha_context.context)
(storage_type_has_tickets : Ticket_scanner.has_tickets)
(lazy_storage_diff : list Alpha_context.Lazy_storage.diffs_item)
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
if Ticket_scanner.has_tickets_value storage_type_has_tickets then
let? '(diffs, ctxt) :=
Ticket_lazy_storage_diff.ticket_diffs_of_lazy_storage_diff ctxt
lazy_storage_diff in
Ticket_token_map.of_list_with_merge ctxt diffs
else
return? (Ticket_token_map.empty, ctxt).
Error_monad.register_error_kind Error_monad.Permanent
"invalid_ticket_transfer" "Invalid ticket transfer"
"Invalid ticket transfer detected in ticket balance update."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : string × Z.t) ⇒
let '(ticketer, amount) := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Attempted to send "
(CamlinternalFormatBasics.Alpha
(CamlinternalFormatBasics.String_literal
" unit(s) of a ticket created by "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))))
"Attempted to send %a unit(s) of a ticket created by %s.")
Z.pp_print amount ticketer))
(Data_encoding.obj2
(Data_encoding.req None None "ticketer" Data_encoding.string_value)
(Data_encoding.req None None "amount" Data_encoding.z_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_ticket_transfer" then
let '{|
Invalid_ticket_transfer.ticketer := ticketer;
Invalid_ticket_transfer.amount := amount
|} := cast Invalid_ticket_transfer payload in
Some (ticketer, amount)
else None
end)
(fun (function_parameter : string × Z.t) ⇒
let '(ticketer, amount) := function_parameter in
Build_extensible "Invalid_ticket_transfer" Invalid_ticket_transfer
{| Invalid_ticket_transfer.ticketer := ticketer;
Invalid_ticket_transfer.amount := amount; |}).
Module Ticket_token_map.
Include Proto_alpha.Ticket_token_map.
Definition balance_diff
(ctxt : Alpha_context.context) (token : Ticket_token.ex_token)
(map : Ticket_token_map.t Z.t) : M? (Z.t × Alpha_context.context) :=
Error_monad.Lwt_result_syntax.op_letplus
(Ticket_token_map.find ctxt token map)
(fun function_parameter ⇒
let '(amnt_opt, ctxt) := function_parameter in
((Option.value_value amnt_opt Z.zero), ctxt)).
Definition merge_overlap (ctxt : Alpha_context.context) (b1 : Z.t) (b2 : Z.t)
: M? (Z.t × Alpha_context.context) :=
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt (Ticket_costs.add_z_cost b1 b2))
(fun ctxt ⇒ ((b1 +Z b2), ctxt)).
Definition of_list_with_merge
(ctxt : Alpha_context.context)
(token_amounts : list (Ticket_token.ex_token × Z.t))
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
Ticket_token_map.of_list ctxt merge_overlap token_amounts.
Definition add (ctxt : Alpha_context.context)
: Ticket_token_map.t Z.t → Ticket_token_map.t Z.t →
M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
Ticket_token_map.merge ctxt merge_overlap.
Definition sub
(ctxt : Alpha_context.context) (m1 : Ticket_token_map.t Z.t) (m2 : t Z.t)
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
let? '(m2, ctxt) :=
map_e ctxt
(fun (ctxt : Alpha_context.context) ⇒
fun (_ex_token : Ticket_token.ex_token) ⇒
fun (amount : Z.t) ⇒
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt
(Ticket_costs.negate_cost amount))
(fun ctxt ⇒ ((Z.neg amount), ctxt))) m2 in
add ctxt m1 m2.
End Ticket_token_map.
Definition ticket_balances_of_value {A : Set}
(ctxt : Alpha_context.context) (include_lazy : bool)
(ty_value : Ticket_scanner.has_tickets) (value_value : A)
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
let? '(tickets, ctxt) :=
Ticket_scanner.tickets_of_value ctxt include_lazy ty_value value_value in
let accum_ticket_balances
(function_parameter :
list (Ticket_token.ex_token × Z.t) × Alpha_context.context)
: Ticket_scanner.ex_ticket →
M? (list (Ticket_token.ex_token × Z.t) × Alpha_context.context) :=
let '(acc_value, ctxt) := function_parameter in
fun (ticket : Ticket_scanner.ex_ticket) ⇒
let '(token, amount) :=
Ticket_scanner.ex_token_and_amount_of_ex_ticket ticket in
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step)
(fun ctxt ⇒
((cons (token, (Script_int.to_zint amount)) acc_value), ctxt)) in
let? '(token_amounts, ctxt) :=
List.fold_left_e accum_ticket_balances (nil, ctxt) tickets in
Ticket_token_map.of_list_with_merge ctxt token_amounts.
Definition update_ticket_balances_aux
(ctxt : Alpha_context.context) (total_storage_diff : Z.t)
(token : Ticket_token.ex_token)
(destinations : list (Alpha_context.Destination.t × Z.t))
: M? (Z.t × Alpha_context.context) :=
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(tot_storage_diff, ctxt) := function_parameter in
fun (function_parameter : Alpha_context.Destination.t × Z.t) ⇒
let '(owner, delta) := function_parameter in
let? '(key_hash, ctxt) :=
Ticket_balance_key.of_ex_token ctxt owner token in
let? '(storage_diff, ctxt) :=
Alpha_context.Ticket_balance.adjust_balance ctxt key_hash delta in
let? ctxt :=
Alpha_context.Gas.consume ctxt
(Ticket_costs.add_z_cost total_storage_diff storage_diff) in
return? ((tot_storage_diff +Z storage_diff), ctxt))
(total_storage_diff, ctxt) destinations.
Definition invalid_ticket_transfer_error
(function_parameter : Ticket_token.ex_token) : Z.t → Error_monad._error :=
let
'Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer;
Ticket_token.parsed_token.contents_type := _;
Ticket_token.parsed_token.contents := _
|} := function_parameter in
fun (amount : Z.t) ⇒
Build_extensible "Invalid_ticket_transfer" Invalid_ticket_transfer
{|
Invalid_ticket_transfer.ticketer :=
Alpha_context.Contract.to_b58check ticketer;
Invalid_ticket_transfer.amount := amount; |}.
Definition update_ticket_balances_for_self_contract
(ctxt : Alpha_context.context) (self_contract : Alpha_context.Contract.t)
(ticket_diffs : list (Ticket_token.ex_token × Z.t))
: M? (Z.t × Alpha_context.context) :=
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(total_storage_diff, ctxt) := function_parameter in
fun (function_parameter : Ticket_token.ex_token × Z.t) ⇒
let '(ticket_token, amount) := function_parameter in
let is_valid_balance_update :=
let
'Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer |} :=
ticket_token in
(amount ≤Z Z.zero) ||
(Alpha_context.Contract.equal ticketer self_contract) in
let? '_ :=
Error_monad.error_unless is_valid_balance_update
(invalid_ticket_transfer_error ticket_token amount) in
update_ticket_balances_aux ctxt total_storage_diff ticket_token
[ ((Alpha_context.Destination.Contract self_contract), amount) ])
(Z.zero, ctxt) ticket_diffs.
Definition ticket_diffs_of_lazy_storage_diff
(ctxt : Alpha_context.context)
(storage_type_has_tickets : Ticket_scanner.has_tickets)
(lazy_storage_diff : list Alpha_context.Lazy_storage.diffs_item)
: M? (Ticket_token_map.t Z.t × Alpha_context.context) :=
if Ticket_scanner.has_tickets_value storage_type_has_tickets then
let? '(diffs, ctxt) :=
Ticket_lazy_storage_diff.ticket_diffs_of_lazy_storage_diff ctxt
lazy_storage_diff in
Ticket_token_map.of_list_with_merge ctxt diffs
else
return? (Ticket_token_map.empty, ctxt).
Description here:
https://hackmd.io/lutm_5JNRVW-nNFSFkCXLQ?view#Implementation
- [old_storage_strict] the amount S_1^{strict} of ticket-tokens in the strict part of
the old storage.
- [new_storage_strict] the amount S_2^{strict} of ticket-tokens in the strict part of the
new storage.
- [lazy_storage_diff] the amount S_{\delta}^{lazy} of ticket-tokens added to the lazy part of
the storage.
- [arg_tickets] the amount I of ticket-tokens contained in the incoming
arguments.
We calculate the ticket diff as the following:
[new_storage_strict] + [lazy_storage_diff] - ([old_storage_strict] + [arg_tickets])
Additionally, we calculate the ticket receipt as below.
We do not subtract the [arg_tickets] since we only want to display the tickets updated in storage for the receipt.
[new_storage_strict] + [lazy_storage_diff] - [storage_strict]
Definition ticket_diffs {A B : Set}
(ctxt : Alpha_context.context) (self_contract : Alpha_context.Contract.t)
(arg_type_has_tickets : Ticket_scanner.has_tickets)
(storage_type_has_tickets : Ticket_scanner.has_tickets) (arg : A)
(old_storage : B) (new_storage : B)
(lazy_storage_diff : list Alpha_context.Lazy_storage.diffs_item)
: M? (Ticket_token_map.t Z.t × Ticket_receipt.t × Alpha_context.context) :=
let? '(arg_tickets, ctxt) :=
ticket_balances_of_value ctxt true arg_type_has_tickets arg in
let? '(lazy_storage_diff, ctxt) :=
ticket_diffs_of_lazy_storage_diff ctxt storage_type_has_tickets
lazy_storage_diff in
let? '(old_storage_strict, ctxt) :=
ticket_balances_of_value ctxt false storage_type_has_tickets old_storage in
let? '(new_storage_strict, ctxt) :=
ticket_balances_of_value ctxt false storage_type_has_tickets new_storage in
let? '(additions, ctxt) :=
Ticket_token_map.add ctxt new_storage_strict lazy_storage_diff in
let? '(total_storage_diff, ctxt) :=
Ticket_token_map.sub ctxt additions old_storage_strict in
let? '(diff_value, ctxt) :=
Ticket_token_map.sub ctxt total_storage_diff arg_tickets in
let? '(ticket_receipt, ctxt) :=
Ticket_token_map.to_ticket_receipt ctxt
(Alpha_context.Destination.Contract self_contract) total_storage_diff in
return? (diff_value, ticket_receipt, ctxt).
Definition update_ticket_balances
(ctxt : Alpha_context.context) (self_contract : Alpha_context.Contract.t)
(ticket_diffs : Ticket_token_map.t Z.t)
(operations : list Script_typed_ir.packed_internal_operation)
: M? (Z.t × Alpha_context.context) :=
let validate_spending_budget
(ctxt : Alpha_context.context) (function_parameter : Ticket_token.ex_token)
: Script_int.num → M? (bool × Alpha_context.context) :=
let
'(Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer |}) as ticket_token :=
function_parameter in
fun (amount : Script_int.num) ⇒
if Alpha_context.Contract.equal ticketer self_contract then
return? (true, ctxt)
else
Error_monad.Lwt_result_syntax.op_letplus
(Ticket_token_map.balance_diff ctxt ticket_token ticket_diffs)
(fun function_parameter ⇒
let '(balance_diff, ctxt) := function_parameter in
(((Script_int.to_zint amount) ≤Z (Z.neg balance_diff)), ctxt)) in
let? '(ticket_op_diffs, ctxt) :=
Ticket_operations_diff.ticket_diffs_of_operations ctxt operations in
let? '(ticket_diffs, ctxt) := Ticket_token_map.to_list ctxt ticket_diffs in
let? '(total_storage_diff, ctxt) :=
update_ticket_balances_for_self_contract ctxt self_contract ticket_diffs in
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(total_storage_diff, ctxt) := function_parameter in
fun (function_parameter : Ticket_operations_diff.ticket_token_diff) ⇒
let '{|
Ticket_operations_diff.ticket_token_diff.ticket_token := ticket_token;
Ticket_operations_diff.ticket_token_diff.total_amount :=
total_amount;
Ticket_operations_diff.ticket_token_diff.destinations :=
destinations
|} := function_parameter in
let? '(is_valid_balance_update, ctxt) :=
validate_spending_budget ctxt ticket_token total_amount in
let? '_ :=
Error_monad.error_unless is_valid_balance_update
(invalid_ticket_transfer_error ticket_token
(Script_int.to_zint total_amount)) in
let? '(destinations, ctxt) :=
List.fold_left_e
(fun (function_parameter :
list (Alpha_context.Destination.t × Z.t) × Alpha_context.context)
⇒
let '(acc_value, ctxt) := function_parameter in
fun (function_parameter :
Alpha_context.Destination.t × Script_typed_ir.ticket_amount) ⇒
let '(token, amount) := function_parameter in
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step)
(fun ctxt ⇒
((cons (token, (Script_int.to_zint amount)) acc_value), ctxt)))
(nil, ctxt) destinations in
update_ticket_balances_aux ctxt total_storage_diff ticket_token
destinations) (total_storage_diff, ctxt) ticket_op_diffs.
(ctxt : Alpha_context.context) (self_contract : Alpha_context.Contract.t)
(arg_type_has_tickets : Ticket_scanner.has_tickets)
(storage_type_has_tickets : Ticket_scanner.has_tickets) (arg : A)
(old_storage : B) (new_storage : B)
(lazy_storage_diff : list Alpha_context.Lazy_storage.diffs_item)
: M? (Ticket_token_map.t Z.t × Ticket_receipt.t × Alpha_context.context) :=
let? '(arg_tickets, ctxt) :=
ticket_balances_of_value ctxt true arg_type_has_tickets arg in
let? '(lazy_storage_diff, ctxt) :=
ticket_diffs_of_lazy_storage_diff ctxt storage_type_has_tickets
lazy_storage_diff in
let? '(old_storage_strict, ctxt) :=
ticket_balances_of_value ctxt false storage_type_has_tickets old_storage in
let? '(new_storage_strict, ctxt) :=
ticket_balances_of_value ctxt false storage_type_has_tickets new_storage in
let? '(additions, ctxt) :=
Ticket_token_map.add ctxt new_storage_strict lazy_storage_diff in
let? '(total_storage_diff, ctxt) :=
Ticket_token_map.sub ctxt additions old_storage_strict in
let? '(diff_value, ctxt) :=
Ticket_token_map.sub ctxt total_storage_diff arg_tickets in
let? '(ticket_receipt, ctxt) :=
Ticket_token_map.to_ticket_receipt ctxt
(Alpha_context.Destination.Contract self_contract) total_storage_diff in
return? (diff_value, ticket_receipt, ctxt).
Definition update_ticket_balances
(ctxt : Alpha_context.context) (self_contract : Alpha_context.Contract.t)
(ticket_diffs : Ticket_token_map.t Z.t)
(operations : list Script_typed_ir.packed_internal_operation)
: M? (Z.t × Alpha_context.context) :=
let validate_spending_budget
(ctxt : Alpha_context.context) (function_parameter : Ticket_token.ex_token)
: Script_int.num → M? (bool × Alpha_context.context) :=
let
'(Ticket_token.Ex_token {|
Ticket_token.parsed_token.ticketer := ticketer |}) as ticket_token :=
function_parameter in
fun (amount : Script_int.num) ⇒
if Alpha_context.Contract.equal ticketer self_contract then
return? (true, ctxt)
else
Error_monad.Lwt_result_syntax.op_letplus
(Ticket_token_map.balance_diff ctxt ticket_token ticket_diffs)
(fun function_parameter ⇒
let '(balance_diff, ctxt) := function_parameter in
(((Script_int.to_zint amount) ≤Z (Z.neg balance_diff)), ctxt)) in
let? '(ticket_op_diffs, ctxt) :=
Ticket_operations_diff.ticket_diffs_of_operations ctxt operations in
let? '(ticket_diffs, ctxt) := Ticket_token_map.to_list ctxt ticket_diffs in
let? '(total_storage_diff, ctxt) :=
update_ticket_balances_for_self_contract ctxt self_contract ticket_diffs in
List.fold_left_es
(fun (function_parameter : Z.t × Alpha_context.context) ⇒
let '(total_storage_diff, ctxt) := function_parameter in
fun (function_parameter : Ticket_operations_diff.ticket_token_diff) ⇒
let '{|
Ticket_operations_diff.ticket_token_diff.ticket_token := ticket_token;
Ticket_operations_diff.ticket_token_diff.total_amount :=
total_amount;
Ticket_operations_diff.ticket_token_diff.destinations :=
destinations
|} := function_parameter in
let? '(is_valid_balance_update, ctxt) :=
validate_spending_budget ctxt ticket_token total_amount in
let? '_ :=
Error_monad.error_unless is_valid_balance_update
(invalid_ticket_transfer_error ticket_token
(Script_int.to_zint total_amount)) in
let? '(destinations, ctxt) :=
List.fold_left_e
(fun (function_parameter :
list (Alpha_context.Destination.t × Z.t) × Alpha_context.context)
⇒
let '(acc_value, ctxt) := function_parameter in
fun (function_parameter :
Alpha_context.Destination.t × Script_typed_ir.ticket_amount) ⇒
let '(token, amount) := function_parameter in
Error_monad.Result_syntax.op_letplus
(Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step)
(fun ctxt ⇒
((cons (token, (Script_int.to_zint amount)) acc_value), ctxt)))
(nil, ctxt) destinations in
update_ticket_balances_aux ctxt total_storage_diff ticket_token
destinations) (total_storage_diff, ctxt) ticket_op_diffs.