🧾 Receipt_repr.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.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Inductive balance : Set :=
| Contract : Contract_repr.t → balance
| Block_fees : balance
| Deposits : Signature.public_key_hash → balance
| Nonce_revelation_rewards : balance
| Double_signing_evidence_rewards : balance
| Endorsing_rewards : balance
| Baking_rewards : balance
| Baking_bonuses : balance
| Storage_fees : balance
| Double_signing_punishments : balance
| Lost_endorsing_rewards : Signature.public_key_hash → bool → bool → balance
| Liquidity_baking_subsidies : balance
| Burned : balance
| Commitments : Blinded_public_key_hash.t → balance
| Bootstrap : balance
| Invoice : balance
| Initial_commitments : balance
| Minted : balance
| Frozen_bonds : Contract_repr.t → Bond_id_repr.t → balance
| Tx_rollup_rejection_punishments : balance
| Tx_rollup_rejection_rewards : balance
| Sc_rollup_refutation_punishments : balance
| Sc_rollup_refutation_rewards : balance.
Definition balance_encoding : Data_encoding.encoding balance :=
Data_encoding.def "operation_metadata.alpha.balance" None None
(Data_encoding.union None
[
Data_encoding.case_value "Contract" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "contract"))
(Data_encoding.req None None "contract"
Contract_repr.encoding))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Contract c_value ⇒ Some (tt, c_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × Contract_repr.t) ⇒
let '(_, c_value) := function_parameter in
Contract c_value);
Data_encoding.case_value "Block_fees" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "accumulator"))
(Data_encoding.req None None "category"
(Data_encoding.constant "block fees")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Block_fees ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Block_fees);
Data_encoding.case_value "Deposits" None (Data_encoding.Tag 4)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "freezer"))
(Data_encoding.req None None "category"
(Data_encoding.constant "deposits"))
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Deposits d_value ⇒ Some (tt, tt, d_value)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Signature.public_key_hash) ⇒
let '(_, _, d_value) := function_parameter in
Deposits d_value);
Data_encoding.case_value "Nonce_revelation_rewards" None
(Data_encoding.Tag 5)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "nonce revelation rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Nonce_revelation_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Nonce_revelation_rewards);
Data_encoding.case_value "Double_signing_evidence_rewards" None
(Data_encoding.Tag 6)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant
"double signing evidence rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Double_signing_evidence_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Double_signing_evidence_rewards);
Data_encoding.case_value "Endorsing_rewards" None (Data_encoding.Tag 7)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "endorsing rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Endorsing_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Endorsing_rewards);
Data_encoding.case_value "Baking_rewards" None (Data_encoding.Tag 8)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "baking rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Baking_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Baking_rewards);
Data_encoding.case_value "Baking_bonuses" None (Data_encoding.Tag 9)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "baking bonuses")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Baking_bonuses ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Baking_bonuses);
Data_encoding.case_value "Storage_fees" None (Data_encoding.Tag 11)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "storage fees")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Storage_fees ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Storage_fees);
Data_encoding.case_value "Double_signing_punishments" None
(Data_encoding.Tag 12)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "punishments")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Double_signing_punishments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Double_signing_punishments);
Data_encoding.case_value "Lost_endorsing_rewards" None
(Data_encoding.Tag 13)
(Data_encoding.obj5
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "lost endorsing rewards"))
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "participation"
Data_encoding.bool_value)
(Data_encoding.req None None "revelation"
Data_encoding.bool_value))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Lost_endorsing_rewards d_value p_value r_value ⇒
Some (tt, tt, d_value, p_value, r_value)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Signature.public_key_hash × bool × bool) ⇒
let '(_, _, d_value, p_value, r_value) := function_parameter
in
Lost_endorsing_rewards d_value p_value r_value);
Data_encoding.case_value "Liquidity_baking_subsidies" None
(Data_encoding.Tag 14)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "subsidy")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Liquidity_baking_subsidies ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Liquidity_baking_subsidies);
Data_encoding.case_value "Burned" None (Data_encoding.Tag 15)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "burned")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Burned ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Burned);
Data_encoding.case_value "Commitments" None (Data_encoding.Tag 16)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "commitment"))
(Data_encoding.req None None "category"
(Data_encoding.constant "commitment"))
(Data_encoding.req None None "committer"
Blinded_public_key_hash.encoding))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Commitments bpkh ⇒ Some (tt, tt, bpkh)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Blinded_public_key_hash.t) ⇒
let '(_, _, bpkh) := function_parameter in
Commitments bpkh);
Data_encoding.case_value "Bootstrap" None (Data_encoding.Tag 17)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "bootstrap")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Bootstrap ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Bootstrap);
Data_encoding.case_value "Invoice" None (Data_encoding.Tag 18)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "invoice")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Invoice ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Invoice);
Data_encoding.case_value "Initial_commitments" None
(Data_encoding.Tag 19)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "commitment")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Initial_commitments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Initial_commitments);
Data_encoding.case_value "Minted" None (Data_encoding.Tag 20)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "minted")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Minted ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Minted);
Data_encoding.case_value "Frozen_bonds" None (Data_encoding.Tag 21)
(Data_encoding.obj4
(Data_encoding.req None None "kind"
(Data_encoding.constant "freezer"))
(Data_encoding.req None None "category"
(Data_encoding.constant "bonds"))
(Data_encoding.req None None "contract"
Contract_repr.encoding)
(Data_encoding.req None None "bond_id" Bond_id_repr.encoding))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Frozen_bonds c_value r_value ⇒
Some (tt, tt, c_value, r_value)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Contract_repr.t × Bond_id_repr.t) ⇒
let '(_, _, c_value, r_value) := function_parameter in
Frozen_bonds c_value r_value);
Data_encoding.case_value "Tx_rollup_rejection_rewards" None
(Data_encoding.Tag 22)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "tx_rollup_rejection_rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Tx_rollup_rejection_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Tx_rollup_rejection_rewards);
Data_encoding.case_value "Tx_rollup_rejection_punishments" None
(Data_encoding.Tag 23)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant
"tx_rollup_rejection_punishments")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Tx_rollup_rejection_punishments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Tx_rollup_rejection_punishments);
Data_encoding.case_value "Sc_rollup_refutation_punishments" None
(Data_encoding.Tag 24)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant
"sc_rollup_refutation_punishments")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Sc_rollup_refutation_punishments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Sc_rollup_refutation_punishments);
Data_encoding.case_value "Sc_rollup_refutation_rewards" None
(Data_encoding.Tag 25)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "sc_rollup_refutation_rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Sc_rollup_refutation_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Sc_rollup_refutation_rewards)
]).
Definition is_not_zero (c_value : int) : bool :=
Pervasives.not (Compare.Int.equal c_value 0).
Definition compare_balance (ba : balance) (bb : balance) : int :=
match (ba, bb) with
| (Contract ca, Contract cb) ⇒ Contract_repr.compare ca cb
| (Deposits pkha, Deposits pkhb) ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb
| (Lost_endorsing_rewards pkha pa ra, Lost_endorsing_rewards pkhb pb rb) ⇒
let c_value :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb
in
if is_not_zero c_value then
c_value
else
let c_value := Compare.Bool.(Compare.S.compare) pa pb in
if is_not_zero c_value then
c_value
else
Compare.Bool.(Compare.S.compare) ra rb
| (Commitments bpkha, Commitments bpkhb) ⇒
Blinded_public_key_hash.compare bpkha bpkhb
| (Frozen_bonds ca ra, Frozen_bonds cb rb) ⇒
let c_value := Contract_repr.compare ca cb in
if is_not_zero c_value then
c_value
else
Bond_id_repr.compare ra rb
| (_, _) ⇒
let index_value (b_value : balance) : int :=
match b_value with
| Contract _ ⇒ 0
| Block_fees ⇒ 1
| Deposits _ ⇒ 2
| Nonce_revelation_rewards ⇒ 3
| Double_signing_evidence_rewards ⇒ 4
| Endorsing_rewards ⇒ 5
| Baking_rewards ⇒ 6
| Baking_bonuses ⇒ 7
| Storage_fees ⇒ 8
| Double_signing_punishments ⇒ 9
| Lost_endorsing_rewards _ _ _ ⇒ 10
| Liquidity_baking_subsidies ⇒ 11
| Burned ⇒ 12
| Commitments _ ⇒ 13
| Bootstrap ⇒ 14
| Invoice ⇒ 15
| Initial_commitments ⇒ 16
| Minted ⇒ 17
| Frozen_bonds _ _ ⇒ 18
| Tx_rollup_rejection_punishments ⇒ 19
| Tx_rollup_rejection_rewards ⇒ 20
| Sc_rollup_refutation_punishments ⇒ 21
| Sc_rollup_refutation_rewards ⇒ 22
end in
Compare.Int.compare (index_value ba) (index_value bb)
end.
Inductive balance_update : Set :=
| Debited : Tez_repr.t → balance_update
| Credited : Tez_repr.t → balance_update.
Definition is_zero_update (function_parameter : balance_update) : bool :=
match function_parameter with
| (Debited t_value | Credited t_value) ⇒ Tez_repr.op_eq t_value Tez_repr.zero
end.
Definition balance_update_encoding : Data_encoding.encoding balance_update :=
Data_encoding.def "operation_metadata.alpha.balance_update" None None
(Data_encoding.obj1
(Data_encoding.req None None "change"
(Data_encoding.conv
(fun (function_parameter : balance_update) ⇒
match function_parameter with
| Credited v_value ⇒ Tez_repr.to_mutez v_value
| Debited v_value ⇒ Int64.neg (Tez_repr.to_mutez v_value)
end)
(Data_encoding.Json.wrap_error
(fun (v_value : int64) ⇒
if v_value <i64 0 then
match Tez_repr.of_mutez (Int64.neg v_value) with
| Some v_value ⇒ Debited v_value
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert balance_update false
end
else
match Tez_repr.of_mutez v_value with
| Some v_value ⇒ Credited v_value
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert balance_update false
end)) None Data_encoding.int64_value))).
Inductive update_origin : Set :=
| Block_application : update_origin
| Protocol_migration : update_origin
| Subsidy : update_origin
| Simulation : update_origin.
Definition compare_update_origin (oa : update_origin) (ob : update_origin)
: int :=
let index_value (o_value : update_origin) : int :=
match o_value with
| Block_application ⇒ 0
| Protocol_migration ⇒ 1
| Subsidy ⇒ 2
| Simulation ⇒ 3
end in
Compare.Int.compare (index_value oa) (index_value ob).
Definition update_origin_encoding : Data_encoding.encoding update_origin :=
Data_encoding.def "operation_metadata.alpha.update_origin" None None
(Data_encoding.obj1
(Data_encoding.req None None "origin"
(Data_encoding.union None
[
Data_encoding.case_value "Block_application" None
(Data_encoding.Tag 0) (Data_encoding.constant "block")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Block_application ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Block_application);
Data_encoding.case_value "Protocol_migration" None
(Data_encoding.Tag 1) (Data_encoding.constant "migration")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Protocol_migration ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Protocol_migration);
Data_encoding.case_value "Subsidy" None (Data_encoding.Tag 2)
(Data_encoding.constant "subsidy")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Subsidy ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Subsidy);
Data_encoding.case_value "Simulation" None (Data_encoding.Tag 3)
(Data_encoding.constant "simulation")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Simulation ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Simulation)
]))).
Definition balance_updates : Set :=
list (balance × balance_update × update_origin).
Definition balance_updates_encoding
: Data_encoding.encoding (list (balance × balance_update × update_origin)) :=
Data_encoding.def "operation_metadata.alpha.balance_updates" None None
(Data_encoding.list_value None
(Data_encoding.conv
(fun (function_parameter : balance × balance_update × update_origin) ⇒
let '(balance, balance_update, update_origin) := function_parameter in
((balance, balance_update), update_origin))
(fun (function_parameter : (balance × balance_update) × update_origin)
⇒
let '((balance, balance_update), update_origin) := function_parameter
in
(balance, balance_update, update_origin)) None
(Data_encoding.merge_objs
(Data_encoding.merge_objs balance_encoding balance_update_encoding)
update_origin_encoding))).
Module BalanceMap.
Definition Map_Make_include :=
Map.Make
(let t : Set := balance × update_origin in
let compare (function_parameter : balance × update_origin)
: balance × update_origin → int :=
let '(ba, ua) := function_parameter in
fun (function_parameter : balance × update_origin) ⇒
let '(bb, ub) := function_parameter in
let c_value := compare_balance ba bb in
if is_not_zero c_value then
c_value
else
compare_update_origin ua ub in
{|
Compare.COMPARABLE.compare := compare
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Bond_id_repr.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Tez_repr.
Inductive balance : Set :=
| Contract : Contract_repr.t → balance
| Block_fees : balance
| Deposits : Signature.public_key_hash → balance
| Nonce_revelation_rewards : balance
| Double_signing_evidence_rewards : balance
| Endorsing_rewards : balance
| Baking_rewards : balance
| Baking_bonuses : balance
| Storage_fees : balance
| Double_signing_punishments : balance
| Lost_endorsing_rewards : Signature.public_key_hash → bool → bool → balance
| Liquidity_baking_subsidies : balance
| Burned : balance
| Commitments : Blinded_public_key_hash.t → balance
| Bootstrap : balance
| Invoice : balance
| Initial_commitments : balance
| Minted : balance
| Frozen_bonds : Contract_repr.t → Bond_id_repr.t → balance
| Tx_rollup_rejection_punishments : balance
| Tx_rollup_rejection_rewards : balance
| Sc_rollup_refutation_punishments : balance
| Sc_rollup_refutation_rewards : balance.
Definition balance_encoding : Data_encoding.encoding balance :=
Data_encoding.def "operation_metadata.alpha.balance" None None
(Data_encoding.union None
[
Data_encoding.case_value "Contract" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "contract"))
(Data_encoding.req None None "contract"
Contract_repr.encoding))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Contract c_value ⇒ Some (tt, c_value)
| _ ⇒ None
end)
(fun (function_parameter : unit × Contract_repr.t) ⇒
let '(_, c_value) := function_parameter in
Contract c_value);
Data_encoding.case_value "Block_fees" None (Data_encoding.Tag 2)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "accumulator"))
(Data_encoding.req None None "category"
(Data_encoding.constant "block fees")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Block_fees ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Block_fees);
Data_encoding.case_value "Deposits" None (Data_encoding.Tag 4)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "freezer"))
(Data_encoding.req None None "category"
(Data_encoding.constant "deposits"))
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Deposits d_value ⇒ Some (tt, tt, d_value)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Signature.public_key_hash) ⇒
let '(_, _, d_value) := function_parameter in
Deposits d_value);
Data_encoding.case_value "Nonce_revelation_rewards" None
(Data_encoding.Tag 5)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "nonce revelation rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Nonce_revelation_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Nonce_revelation_rewards);
Data_encoding.case_value "Double_signing_evidence_rewards" None
(Data_encoding.Tag 6)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant
"double signing evidence rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Double_signing_evidence_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Double_signing_evidence_rewards);
Data_encoding.case_value "Endorsing_rewards" None (Data_encoding.Tag 7)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "endorsing rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Endorsing_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Endorsing_rewards);
Data_encoding.case_value "Baking_rewards" None (Data_encoding.Tag 8)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "baking rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Baking_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Baking_rewards);
Data_encoding.case_value "Baking_bonuses" None (Data_encoding.Tag 9)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "baking bonuses")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Baking_bonuses ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Baking_bonuses);
Data_encoding.case_value "Storage_fees" None (Data_encoding.Tag 11)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "storage fees")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Storage_fees ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Storage_fees);
Data_encoding.case_value "Double_signing_punishments" None
(Data_encoding.Tag 12)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "punishments")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Double_signing_punishments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Double_signing_punishments);
Data_encoding.case_value "Lost_endorsing_rewards" None
(Data_encoding.Tag 13)
(Data_encoding.obj5
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "lost endorsing rewards"))
(Data_encoding.req None None "delegate"
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
(Data_encoding.req None None "participation"
Data_encoding.bool_value)
(Data_encoding.req None None "revelation"
Data_encoding.bool_value))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Lost_endorsing_rewards d_value p_value r_value ⇒
Some (tt, tt, d_value, p_value, r_value)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Signature.public_key_hash × bool × bool) ⇒
let '(_, _, d_value, p_value, r_value) := function_parameter
in
Lost_endorsing_rewards d_value p_value r_value);
Data_encoding.case_value "Liquidity_baking_subsidies" None
(Data_encoding.Tag 14)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "subsidy")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Liquidity_baking_subsidies ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Liquidity_baking_subsidies);
Data_encoding.case_value "Burned" None (Data_encoding.Tag 15)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant "burned")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Burned ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Burned);
Data_encoding.case_value "Commitments" None (Data_encoding.Tag 16)
(Data_encoding.obj3
(Data_encoding.req None None "kind"
(Data_encoding.constant "commitment"))
(Data_encoding.req None None "category"
(Data_encoding.constant "commitment"))
(Data_encoding.req None None "committer"
Blinded_public_key_hash.encoding))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Commitments bpkh ⇒ Some (tt, tt, bpkh)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Blinded_public_key_hash.t) ⇒
let '(_, _, bpkh) := function_parameter in
Commitments bpkh);
Data_encoding.case_value "Bootstrap" None (Data_encoding.Tag 17)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "bootstrap")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Bootstrap ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Bootstrap);
Data_encoding.case_value "Invoice" None (Data_encoding.Tag 18)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "invoice")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Invoice ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Invoice);
Data_encoding.case_value "Initial_commitments" None
(Data_encoding.Tag 19)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "commitment")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Initial_commitments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Initial_commitments);
Data_encoding.case_value "Minted" None (Data_encoding.Tag 20)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "minted")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Minted ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Minted);
Data_encoding.case_value "Frozen_bonds" None (Data_encoding.Tag 21)
(Data_encoding.obj4
(Data_encoding.req None None "kind"
(Data_encoding.constant "freezer"))
(Data_encoding.req None None "category"
(Data_encoding.constant "bonds"))
(Data_encoding.req None None "contract"
Contract_repr.encoding)
(Data_encoding.req None None "bond_id" Bond_id_repr.encoding))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Frozen_bonds c_value r_value ⇒
Some (tt, tt, c_value, r_value)
| _ ⇒ None
end)
(fun (function_parameter :
unit × unit × Contract_repr.t × Bond_id_repr.t) ⇒
let '(_, _, c_value, r_value) := function_parameter in
Frozen_bonds c_value r_value);
Data_encoding.case_value "Tx_rollup_rejection_rewards" None
(Data_encoding.Tag 22)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "tx_rollup_rejection_rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Tx_rollup_rejection_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Tx_rollup_rejection_rewards);
Data_encoding.case_value "Tx_rollup_rejection_punishments" None
(Data_encoding.Tag 23)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant
"tx_rollup_rejection_punishments")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Tx_rollup_rejection_punishments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Tx_rollup_rejection_punishments);
Data_encoding.case_value "Sc_rollup_refutation_punishments" None
(Data_encoding.Tag 24)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "burned"))
(Data_encoding.req None None "category"
(Data_encoding.constant
"sc_rollup_refutation_punishments")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Sc_rollup_refutation_punishments ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Sc_rollup_refutation_punishments);
Data_encoding.case_value "Sc_rollup_refutation_rewards" None
(Data_encoding.Tag 25)
(Data_encoding.obj2
(Data_encoding.req None None "kind"
(Data_encoding.constant "minted"))
(Data_encoding.req None None "category"
(Data_encoding.constant "sc_rollup_refutation_rewards")))
(fun (function_parameter : balance) ⇒
match function_parameter with
| Sc_rollup_refutation_rewards ⇒ Some (tt, tt)
| _ ⇒ None
end)
(fun (function_parameter : unit × unit) ⇒
let '(_, _) := function_parameter in
Sc_rollup_refutation_rewards)
]).
Definition is_not_zero (c_value : int) : bool :=
Pervasives.not (Compare.Int.equal c_value 0).
Definition compare_balance (ba : balance) (bb : balance) : int :=
match (ba, bb) with
| (Contract ca, Contract cb) ⇒ Contract_repr.compare ca cb
| (Deposits pkha, Deposits pkhb) ⇒
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb
| (Lost_endorsing_rewards pkha pa ra, Lost_endorsing_rewards pkhb pb rb) ⇒
let c_value :=
Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) pkha pkhb
in
if is_not_zero c_value then
c_value
else
let c_value := Compare.Bool.(Compare.S.compare) pa pb in
if is_not_zero c_value then
c_value
else
Compare.Bool.(Compare.S.compare) ra rb
| (Commitments bpkha, Commitments bpkhb) ⇒
Blinded_public_key_hash.compare bpkha bpkhb
| (Frozen_bonds ca ra, Frozen_bonds cb rb) ⇒
let c_value := Contract_repr.compare ca cb in
if is_not_zero c_value then
c_value
else
Bond_id_repr.compare ra rb
| (_, _) ⇒
let index_value (b_value : balance) : int :=
match b_value with
| Contract _ ⇒ 0
| Block_fees ⇒ 1
| Deposits _ ⇒ 2
| Nonce_revelation_rewards ⇒ 3
| Double_signing_evidence_rewards ⇒ 4
| Endorsing_rewards ⇒ 5
| Baking_rewards ⇒ 6
| Baking_bonuses ⇒ 7
| Storage_fees ⇒ 8
| Double_signing_punishments ⇒ 9
| Lost_endorsing_rewards _ _ _ ⇒ 10
| Liquidity_baking_subsidies ⇒ 11
| Burned ⇒ 12
| Commitments _ ⇒ 13
| Bootstrap ⇒ 14
| Invoice ⇒ 15
| Initial_commitments ⇒ 16
| Minted ⇒ 17
| Frozen_bonds _ _ ⇒ 18
| Tx_rollup_rejection_punishments ⇒ 19
| Tx_rollup_rejection_rewards ⇒ 20
| Sc_rollup_refutation_punishments ⇒ 21
| Sc_rollup_refutation_rewards ⇒ 22
end in
Compare.Int.compare (index_value ba) (index_value bb)
end.
Inductive balance_update : Set :=
| Debited : Tez_repr.t → balance_update
| Credited : Tez_repr.t → balance_update.
Definition is_zero_update (function_parameter : balance_update) : bool :=
match function_parameter with
| (Debited t_value | Credited t_value) ⇒ Tez_repr.op_eq t_value Tez_repr.zero
end.
Definition balance_update_encoding : Data_encoding.encoding balance_update :=
Data_encoding.def "operation_metadata.alpha.balance_update" None None
(Data_encoding.obj1
(Data_encoding.req None None "change"
(Data_encoding.conv
(fun (function_parameter : balance_update) ⇒
match function_parameter with
| Credited v_value ⇒ Tez_repr.to_mutez v_value
| Debited v_value ⇒ Int64.neg (Tez_repr.to_mutez v_value)
end)
(Data_encoding.Json.wrap_error
(fun (v_value : int64) ⇒
if v_value <i64 0 then
match Tez_repr.of_mutez (Int64.neg v_value) with
| Some v_value ⇒ Debited v_value
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert balance_update false
end
else
match Tez_repr.of_mutez v_value with
| Some v_value ⇒ Credited v_value
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert balance_update false
end)) None Data_encoding.int64_value))).
Inductive update_origin : Set :=
| Block_application : update_origin
| Protocol_migration : update_origin
| Subsidy : update_origin
| Simulation : update_origin.
Definition compare_update_origin (oa : update_origin) (ob : update_origin)
: int :=
let index_value (o_value : update_origin) : int :=
match o_value with
| Block_application ⇒ 0
| Protocol_migration ⇒ 1
| Subsidy ⇒ 2
| Simulation ⇒ 3
end in
Compare.Int.compare (index_value oa) (index_value ob).
Definition update_origin_encoding : Data_encoding.encoding update_origin :=
Data_encoding.def "operation_metadata.alpha.update_origin" None None
(Data_encoding.obj1
(Data_encoding.req None None "origin"
(Data_encoding.union None
[
Data_encoding.case_value "Block_application" None
(Data_encoding.Tag 0) (Data_encoding.constant "block")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Block_application ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Block_application);
Data_encoding.case_value "Protocol_migration" None
(Data_encoding.Tag 1) (Data_encoding.constant "migration")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Protocol_migration ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Protocol_migration);
Data_encoding.case_value "Subsidy" None (Data_encoding.Tag 2)
(Data_encoding.constant "subsidy")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Subsidy ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Subsidy);
Data_encoding.case_value "Simulation" None (Data_encoding.Tag 3)
(Data_encoding.constant "simulation")
(fun (function_parameter : update_origin) ⇒
match function_parameter with
| Simulation ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Simulation)
]))).
Definition balance_updates : Set :=
list (balance × balance_update × update_origin).
Definition balance_updates_encoding
: Data_encoding.encoding (list (balance × balance_update × update_origin)) :=
Data_encoding.def "operation_metadata.alpha.balance_updates" None None
(Data_encoding.list_value None
(Data_encoding.conv
(fun (function_parameter : balance × balance_update × update_origin) ⇒
let '(balance, balance_update, update_origin) := function_parameter in
((balance, balance_update), update_origin))
(fun (function_parameter : (balance × balance_update) × update_origin)
⇒
let '((balance, balance_update), update_origin) := function_parameter
in
(balance, balance_update, update_origin)) None
(Data_encoding.merge_objs
(Data_encoding.merge_objs balance_encoding balance_update_encoding)
update_origin_encoding))).
Module BalanceMap.
Definition Map_Make_include :=
Map.Make
(let t : Set := balance × update_origin in
let compare (function_parameter : balance × update_origin)
: balance × update_origin → int :=
let '(ba, ua) := function_parameter in
fun (function_parameter : balance × update_origin) ⇒
let '(bb, ub) := function_parameter in
let c_value := compare_balance ba bb in
if is_not_zero c_value then
c_value
else
compare_update_origin ua ub in
{|
Compare.COMPARABLE.compare := compare
|}).
Inclusion of the module [Map_Make_include]
Definition key := Map_Make_include.(Map.S.key).
Definition t := Map_Make_include.(Map.S.t).
Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).
Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).
Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).
Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).
Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).
Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).
Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).
Definition merge {a b c : Set} :=
Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).
Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).
Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).
Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).
Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).
Definition iter_e {a trace : Set} :=
Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).
Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).
Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).
Definition iter_es {a trace : Set} :=
Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).
Definition fold {a b : Set} :=
Map_Make_include.(Map.S.fold) (a := a) (b := b).
Definition fold_e {a b trace : Set} :=
Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).
Definition fold_s {a b : Set} :=
Map_Make_include.(Map.S.fold_s) (a := a) (b := b).
Definition fold_es {a b trace : Set} :=
Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).
Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).
Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).
Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).
Definition filter_map {a b : Set} :=
Map_Make_include.(Map.S.filter_map) (a := a) (b := b).
Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).
Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).
Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).
Definition min_binding {a : Set} :=
Map_Make_include.(Map.S.min_binding) (a := a).
Definition min_binding_opt {a : Set} :=
Map_Make_include.(Map.S.min_binding_opt) (a := a).
Definition max_binding {a : Set} :=
Map_Make_include.(Map.S.max_binding) (a := a).
Definition max_binding_opt {a : Set} :=
Map_Make_include.(Map.S.max_binding_opt) (a := a).
Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).
Definition choose_opt {a : Set} :=
Map_Make_include.(Map.S.choose_opt) (a := a).
Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).
Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).
Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).
Definition find_first {a : Set} :=
Map_Make_include.(Map.S.find_first) (a := a).
Definition find_first_opt {a : Set} :=
Map_Make_include.(Map.S.find_first_opt) (a := a).
Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).
Definition find_last_opt {a : Set} :=
Map_Make_include.(Map.S.find_last_opt) (a := a).
Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).
Definition mapi {a b : Set} :=
Map_Make_include.(Map.S.mapi) (a := a) (b := b).
Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).
Definition to_rev_seq {a : Set} :=
Map_Make_include.(Map.S.to_rev_seq) (a := a).
Definition to_seq_from {a : Set} :=
Map_Make_include.(Map.S.to_seq_from) (a := a).
Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).
Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).
Definition iter_ep {a _error : Set} :=
Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).
Definition update_r {b : Set}
(key_value : key) (f_value : option b → M? (option b)) (map : t b)
: M? (t b) :=
let? function_parameter := f_value (find key_value map) in
match function_parameter with
| Some v_value ⇒ return? (add key_value v_value map)
| None ⇒ return? (remove key_value map)
end.
End BalanceMap.
Definition group_balance_updates
(balance_updates : list (balance × balance_update × update_origin))
: M? (list (balance × balance_update × update_origin)) :=
let? map :=
List.fold_left_e
(fun (acc_value : BalanceMap.t balance_update) ⇒
fun (function_parameter : balance × balance_update × update_origin) ⇒
let '(b_value, update, o_value) := function_parameter in
if is_zero_update update then
return? acc_value
else
BalanceMap.update_r (b_value, o_value)
(fun (function_parameter : option balance_update) ⇒
match function_parameter with
| None ⇒ return? (Some update)
| Some balance ⇒
match (balance, update) with
|
((Credited a_value, Debited b_value) |
(Debited b_value, Credited a_value)) ⇒
if Tez_repr.op_eq a_value b_value then
return? None
else
if Tez_repr.op_gt a_value b_value then
let? update := Tez_repr.op_minusquestion a_value b_value
in
return? (Some (Credited update))
else
let? update := Tez_repr.op_minusquestion b_value a_value
in
return? (Some (Debited update))
| (Credited a_value, Credited b_value) ⇒
let? update := Tez_repr.op_plusquestion a_value b_value in
return? (Some (Credited update))
| (Debited a_value, Debited b_value) ⇒
let? update := Tez_repr.op_plusquestion a_value b_value in
return? (Some (Debited update))
end
end) acc_value) BalanceMap.empty balance_updates in
return?
(BalanceMap.fold
(fun (function_parameter : balance × update_origin) ⇒
let '(b_value, o_value) := function_parameter in
fun (u_value : balance_update) ⇒
fun (acc_value : list (balance × balance_update × update_origin)) ⇒
cons (b_value, u_value, o_value) acc_value) map nil).
Definition t := Map_Make_include.(Map.S.t).
Definition empty {a : Set} := Map_Make_include.(Map.S.empty) (a := a).
Definition is_empty {a : Set} := Map_Make_include.(Map.S.is_empty) (a := a).
Definition mem {a : Set} := Map_Make_include.(Map.S.mem) (a := a).
Definition add {a : Set} := Map_Make_include.(Map.S.add) (a := a).
Definition update {a : Set} := Map_Make_include.(Map.S.update) (a := a).
Definition singleton {a : Set} := Map_Make_include.(Map.S.singleton) (a := a).
Definition remove {a : Set} := Map_Make_include.(Map.S.remove) (a := a).
Definition merge {a b c : Set} :=
Map_Make_include.(Map.S.merge) (a := a) (b := b) (c := c).
Definition union {a : Set} := Map_Make_include.(Map.S.union) (a := a).
Definition compare {a : Set} := Map_Make_include.(Map.S.compare) (a := a).
Definition equal {a : Set} := Map_Make_include.(Map.S.equal) (a := a).
Definition iter {a : Set} := Map_Make_include.(Map.S.iter) (a := a).
Definition iter_e {a trace : Set} :=
Map_Make_include.(Map.S.iter_e) (a := a) (trace := trace).
Definition iter_s {a : Set} := Map_Make_include.(Map.S.iter_s) (a := a).
Definition iter_p {a : Set} := Map_Make_include.(Map.S.iter_p) (a := a).
Definition iter_es {a trace : Set} :=
Map_Make_include.(Map.S.iter_es) (a := a) (trace := trace).
Definition fold {a b : Set} :=
Map_Make_include.(Map.S.fold) (a := a) (b := b).
Definition fold_e {a b trace : Set} :=
Map_Make_include.(Map.S.fold_e) (a := a) (b := b) (trace := trace).
Definition fold_s {a b : Set} :=
Map_Make_include.(Map.S.fold_s) (a := a) (b := b).
Definition fold_es {a b trace : Set} :=
Map_Make_include.(Map.S.fold_es) (a := a) (b := b) (trace := trace).
Definition for_all {a : Set} := Map_Make_include.(Map.S.for_all) (a := a).
Definition _exists {a : Set} := Map_Make_include.(Map.S._exists) (a := a).
Definition filter {a : Set} := Map_Make_include.(Map.S.filter) (a := a).
Definition filter_map {a b : Set} :=
Map_Make_include.(Map.S.filter_map) (a := a) (b := b).
Definition partition {a : Set} := Map_Make_include.(Map.S.partition) (a := a).
Definition cardinal {a : Set} := Map_Make_include.(Map.S.cardinal) (a := a).
Definition bindings {a : Set} := Map_Make_include.(Map.S.bindings) (a := a).
Definition min_binding {a : Set} :=
Map_Make_include.(Map.S.min_binding) (a := a).
Definition min_binding_opt {a : Set} :=
Map_Make_include.(Map.S.min_binding_opt) (a := a).
Definition max_binding {a : Set} :=
Map_Make_include.(Map.S.max_binding) (a := a).
Definition max_binding_opt {a : Set} :=
Map_Make_include.(Map.S.max_binding_opt) (a := a).
Definition choose {a : Set} := Map_Make_include.(Map.S.choose) (a := a).
Definition choose_opt {a : Set} :=
Map_Make_include.(Map.S.choose_opt) (a := a).
Definition split {a : Set} := Map_Make_include.(Map.S.split) (a := a).
Definition find {a : Set} := Map_Make_include.(Map.S.find) (a := a).
Definition find_opt {a : Set} := Map_Make_include.(Map.S.find_opt) (a := a).
Definition find_first {a : Set} :=
Map_Make_include.(Map.S.find_first) (a := a).
Definition find_first_opt {a : Set} :=
Map_Make_include.(Map.S.find_first_opt) (a := a).
Definition find_last {a : Set} := Map_Make_include.(Map.S.find_last) (a := a).
Definition find_last_opt {a : Set} :=
Map_Make_include.(Map.S.find_last_opt) (a := a).
Definition map {a b : Set} := Map_Make_include.(Map.S.map) (a := a) (b := b).
Definition mapi {a b : Set} :=
Map_Make_include.(Map.S.mapi) (a := a) (b := b).
Definition to_seq {a : Set} := Map_Make_include.(Map.S.to_seq) (a := a).
Definition to_rev_seq {a : Set} :=
Map_Make_include.(Map.S.to_rev_seq) (a := a).
Definition to_seq_from {a : Set} :=
Map_Make_include.(Map.S.to_seq_from) (a := a).
Definition add_seq {a : Set} := Map_Make_include.(Map.S.add_seq) (a := a).
Definition of_seq {a : Set} := Map_Make_include.(Map.S.of_seq) (a := a).
Definition iter_ep {a _error : Set} :=
Map_Make_include.(Map.S.iter_ep) (a := a) (_error := _error).
Definition update_r {b : Set}
(key_value : key) (f_value : option b → M? (option b)) (map : t b)
: M? (t b) :=
let? function_parameter := f_value (find key_value map) in
match function_parameter with
| Some v_value ⇒ return? (add key_value v_value map)
| None ⇒ return? (remove key_value map)
end.
End BalanceMap.
Definition group_balance_updates
(balance_updates : list (balance × balance_update × update_origin))
: M? (list (balance × balance_update × update_origin)) :=
let? map :=
List.fold_left_e
(fun (acc_value : BalanceMap.t balance_update) ⇒
fun (function_parameter : balance × balance_update × update_origin) ⇒
let '(b_value, update, o_value) := function_parameter in
if is_zero_update update then
return? acc_value
else
BalanceMap.update_r (b_value, o_value)
(fun (function_parameter : option balance_update) ⇒
match function_parameter with
| None ⇒ return? (Some update)
| Some balance ⇒
match (balance, update) with
|
((Credited a_value, Debited b_value) |
(Debited b_value, Credited a_value)) ⇒
if Tez_repr.op_eq a_value b_value then
return? None
else
if Tez_repr.op_gt a_value b_value then
let? update := Tez_repr.op_minusquestion a_value b_value
in
return? (Some (Credited update))
else
let? update := Tez_repr.op_minusquestion b_value a_value
in
return? (Some (Debited update))
| (Credited a_value, Credited b_value) ⇒
let? update := Tez_repr.op_plusquestion a_value b_value in
return? (Some (Credited update))
| (Debited a_value, Debited b_value) ⇒
let? update := Tez_repr.op_plusquestion a_value b_value in
return? (Some (Debited update))
end
end) acc_value) BalanceMap.empty balance_updates in
return?
(BalanceMap.fold
(fun (function_parameter : balance × update_origin) ⇒
let '(b_value, o_value) := function_parameter in
fun (u_value : balance_update) ⇒
fun (acc_value : list (balance × balance_update × update_origin)) ⇒
cons (b_value, u_value, o_value) acc_value) map nil).