Skip to main content

🧾 Receipt_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.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.

Definition balance_encoding : Data_encoding.encoding balance :=
  (let arg := Data_encoding.def "operation_metadata.alpha.balance" in
  fun (eta : Data_encoding.encoding balance) ⇒ arg None None eta)
    (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_valueSome (tt, c_value)
            | _None
            end)
          (fun (function_parameter : unit × Contract_repr.contract) ⇒
            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_feesSome (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_valueSome (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_rewardsSome (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_rewardsSome (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_rewardsSome (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_rewardsSome (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_bonusesSome (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_feesSome (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_punishmentsSome (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_subsidiesSome (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
            | BurnedSome (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 bpkhSome (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
            | BootstrapSome (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
            | InvoiceSome (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_commitmentsSome (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
            | MintedSome (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.contract × 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_rewardsSome (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_punishmentsSome (tt, tt)
            | _None
            end)
          (fun (function_parameter : unit × unit) ⇒
            let '(_, _) := function_parameter in
            Tx_rollup_rejection_punishments)
      ]).

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
      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 :=
  (let arg := Data_encoding.def "operation_metadata.alpha.balance_update" in
  fun (eta : Data_encoding.encoding balance_update) ⇒ arg None None eta)
    (Data_encoding.obj1
      (Data_encoding.req None None "change"
        (Data_encoding.conv
          (fun (function_parameter : balance_update) ⇒
            match function_parameter with
            | Credited v_valueTez_repr.to_mutez v_value
            | Debited v_valueInt64.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_valueDebited v_value
                | None
                  (* ❌ Assert instruction is not handled. *)
                  assert balance_update false
                end
              else
                match Tez_repr.of_mutez v_value with
                | Some v_valueCredited 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 :=
  (let arg := Data_encoding.def "operation_metadata.alpha.update_origin" in
  fun (eta : Data_encoding.encoding update_origin) ⇒ arg None None eta)
    (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_applicationSome 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_migrationSome 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
                | SubsidySome 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
                | SimulationSome 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)) :=
  (let arg := Data_encoding.def "operation_metadata.alpha.balance_updates" in
  fun (eta :
    Data_encoding.encoding (list (balance × balance_update × update_origin))) ⇒
    arg None None eta)
    (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_valuereturn? (add key_value v_value map)
    | Nonereturn? (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
                | Nonereturn? (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).