🎫 Ticket_accounting.v
Translated 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_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_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.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
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_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) :=
let? '(amnt_opt, ctxt) := Ticket_token_map.find ctxt token map in
return? ((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) :=
let? ctxt := Alpha_context.Gas.consume ctxt (Ticket_costs.add_z_cost b1 b2)
in
return? ((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 ctxt
(fun (ctxt : Alpha_context.context) ⇒
fun (function_parameter : Ticket_token.ex_token) ⇒
let '_ := function_parameter in
fun (amount : Z.t) ⇒
let? ctxt :=
Alpha_context.Gas.consume ctxt (Ticket_costs.negate_cost amount)
in
return? ((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 : 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 in
let? '(list_value, ctxt) :=
List.fold_left_e
(fun (function_parameter :
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_token.token_and_amount_of_ex_ticket ticket in
let? ctxt :=
Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step in
return?
((cons (token, (Alpha_context.Script_int.to_zint amount)) acc_value),
ctxt)) (nil, ctxt) tickets in
Ticket_token_map.of_list_with_merge ctxt list_value.
Definition update_ticket_balances_raw
(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.ex_token.Ex_token.ticketer := ticketer;
Ticket_token.ex_token.Ex_token.contents_type := _;
Ticket_token.ex_token.Ex_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 : 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.ex_token.Ex_token.ticketer := ticketer |} :=
ticket_token in
(amount ≤Z Z.zero) || (Alpha_context.Contract.equal ticketer self) in
let? '_ :=
Error_monad.error_unless is_valid_balance_update
(invalid_ticket_transfer_error ticket_token amount) in
update_ticket_balances_raw ctxt total_storage_diff ticket_token
[ ((Alpha_context.Destination.Contract self), 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) :=
let? '(amnt_opt, ctxt) := Ticket_token_map.find ctxt token map in
return? ((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) :=
let? ctxt := Alpha_context.Gas.consume ctxt (Ticket_costs.add_z_cost b1 b2)
in
return? ((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 ctxt
(fun (ctxt : Alpha_context.context) ⇒
fun (function_parameter : Ticket_token.ex_token) ⇒
let '_ := function_parameter in
fun (amount : Z.t) ⇒
let? ctxt :=
Alpha_context.Gas.consume ctxt (Ticket_costs.negate_cost amount)
in
return? ((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 : 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 in
let? '(list_value, ctxt) :=
List.fold_left_e
(fun (function_parameter :
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_token.token_and_amount_of_ex_ticket ticket in
let? ctxt :=
Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step in
return?
((cons (token, (Alpha_context.Script_int.to_zint amount)) acc_value),
ctxt)) (nil, ctxt) tickets in
Ticket_token_map.of_list_with_merge ctxt list_value.
Definition update_ticket_balances_raw
(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.ex_token.Ex_token.ticketer := ticketer;
Ticket_token.ex_token.Ex_token.contents_type := _;
Ticket_token.ex_token.Ex_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 : 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.ex_token.Ex_token.ticketer := ticketer |} :=
ticket_token in
(amount ≤Z Z.zero) || (Alpha_context.Contract.equal ticketer self) in
let? '_ :=
Error_monad.error_unless is_valid_balance_update
(invalid_ticket_transfer_error ticket_token amount) in
update_ticket_balances_raw ctxt total_storage_diff ticket_token
[ ((Alpha_context.Destination.Contract self), 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.
Calculating the spending budget:
additions = new_storage_strict + lazy_storage_diff
subtractions = old_storage_strict + arg_tickets
delta = additions - subtractions
Definition ticket_diffs {A B : Set}
(ctxt : Alpha_context.context)
(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 × 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? '(subtractions, ctxt) :=
Ticket_token_map.add ctxt old_storage_strict arg_tickets in
let? '(additions, ctxt) :=
Ticket_token_map.add ctxt new_storage_strict lazy_storage_diff in
Ticket_token_map.sub ctxt additions subtractions.
Definition update_ticket_balances
(ctxt : Alpha_context.context) (self : 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)
: Alpha_context.Script_int.num → M? (bool × Alpha_context.context) :=
let
'(Ticket_token.Ex_token {|
Ticket_token.ex_token.Ex_token.ticketer := ticketer |}) as
ticket_token := function_parameter in
fun (amount : Alpha_context.Script_int.num) ⇒
if Alpha_context.Contract.equal ticketer self then
return? (true, ctxt)
else
let? '(balance_diff, ctxt) :=
Ticket_token_map.balance_diff ctxt ticket_token ticket_diffs in
return?
(((Alpha_context.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 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
(Alpha_context.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 × Alpha_context.Script_int.num) ⇒
let '(token, amount) := function_parameter in
let? ctxt :=
Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step in
return?
((cons (token, (Alpha_context.Script_int.to_zint amount))
acc_value), ctxt)) (nil, ctxt) destinations in
update_ticket_balances_raw ctxt total_storage_diff ticket_token
destinations) (total_storage_diff, ctxt) ticket_op_diffs.
(ctxt : Alpha_context.context)
(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 × 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? '(subtractions, ctxt) :=
Ticket_token_map.add ctxt old_storage_strict arg_tickets in
let? '(additions, ctxt) :=
Ticket_token_map.add ctxt new_storage_strict lazy_storage_diff in
Ticket_token_map.sub ctxt additions subtractions.
Definition update_ticket_balances
(ctxt : Alpha_context.context) (self : 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)
: Alpha_context.Script_int.num → M? (bool × Alpha_context.context) :=
let
'(Ticket_token.Ex_token {|
Ticket_token.ex_token.Ex_token.ticketer := ticketer |}) as
ticket_token := function_parameter in
fun (amount : Alpha_context.Script_int.num) ⇒
if Alpha_context.Contract.equal ticketer self then
return? (true, ctxt)
else
let? '(balance_diff, ctxt) :=
Ticket_token_map.balance_diff ctxt ticket_token ticket_diffs in
return?
(((Alpha_context.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 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
(Alpha_context.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 × Alpha_context.Script_int.num) ⇒
let '(token, amount) := function_parameter in
let? ctxt :=
Alpha_context.Gas.consume ctxt
Ticket_costs.Constants.cost_collect_tickets_step in
return?
((cons (token, (Alpha_context.Script_int.to_zint amount))
acc_value), ctxt)) (nil, ctxt) destinations in
update_ticket_balances_raw ctxt total_storage_diff ticket_token
destinations) (total_storage_diff, ctxt) ticket_op_diffs.