Skip to main content

🪅 Token.v

Translated OCaml

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.Commitment_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Frozen_deposits_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.

Inductive container : Set :=
| Contract : Contract_repr.t container
| Collected_commitments : Blinded_public_key_hash.t container
| Delegate_balance : Signature.public_key_hash container
| Frozen_deposits : Signature.public_key_hash container
| Block_fees : container
| Frozen_bonds : Contract_repr.t Bond_id_repr.t container.

Inductive infinite_source : Set :=
| Invoice : infinite_source
| Bootstrap : infinite_source
| Initial_commitments : infinite_source
| Revelation_rewards : infinite_source
| Double_signing_evidence_rewards : infinite_source
| Endorsing_rewards : infinite_source
| Baking_rewards : infinite_source
| Baking_bonuses : infinite_source
| Minted : infinite_source
| Liquidity_baking_subsidies : infinite_source
| Tx_rollup_rejection_rewards : infinite_source.

Inductive source : Set :=
| Source_infinite : infinite_source source
| Source_container : container source.

Inductive infinite_sink : Set :=
| Storage_fees : infinite_sink
| Double_signing_punishments : infinite_sink
| Lost_endorsing_rewards :
  Signature.public_key_hash bool bool infinite_sink
| Burned : infinite_sink
| Tx_rollup_rejection_punishments : infinite_sink.

Inductive sink : Set :=
| Sink_infinite : infinite_sink sink
| Sink_container : container sink.

Definition allocated (ctxt : Raw_context.t) (stored : container)
  : M? (Raw_context.t × bool) :=
  match stored with
  | Contract contract
    let? allocated := Contract_storage.allocated ctxt contract in
    return? (ctxt, allocated)
  | Collected_commitments bpkh
    let? allocated :=
      Error_monad.op_gtpipeeq (Commitment_storage._exists ctxt bpkh)
        Error_monad.ok in
    return? (ctxt, allocated)
  | Delegate_balance delegate
    let contract := Contract_repr.implicit_contract delegate in
    let? allocated := Contract_storage.allocated ctxt contract in
    return? (ctxt, allocated)
  | Frozen_deposits delegate
    let contract := Contract_repr.implicit_contract delegate in
    let allocated := Frozen_deposits_storage.allocated ctxt contract in
    return? (ctxt, allocated)
  | Block_feesreturn? (ctxt, true)
  | Frozen_bonds contract bond_id
    Contract_storage.bond_allocated ctxt contract bond_id
  end.

Definition balance (ctxt : Raw_context.t) (stored : container)
  : M? (Raw_context.t × Tez_repr.t) :=
  match stored with
  | Contract contract
    let? balance := Contract_storage.get_balance ctxt contract in
    return? (ctxt, balance)
  | Collected_commitments bpkh
    let? balance := Commitment_storage.committed_amount ctxt bpkh in
    return? (ctxt, balance)
  | Delegate_balance delegate
    let contract := Contract_repr.implicit_contract delegate in
    let? balance :=
      Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage.get)
        ctxt contract in
    return? (ctxt, balance)
  | Frozen_deposits delegate
    let contract := Contract_repr.implicit_contract delegate in
    let? frozen_deposits := Frozen_deposits_storage.find ctxt contract in
    let balance :=
      match frozen_deposits with
      | NoneTez_repr.zero
      | Some frozen_deposits
        frozen_deposits.(Storage.deposits.current_amount)
      end in
    return? (ctxt, balance)
  | Block_feesreturn? (ctxt, (Raw_context.get_collected_fees ctxt))
  | Frozen_bonds contract bond_id
    let? '(ctxt, balance_opt) :=
      Contract_storage.find_bond ctxt contract bond_id in
    return? (ctxt, (Option.value_value balance_opt Tez_repr.zero))
  end.

Definition credit {A : Set}
  (ctxt : Raw_context.t) (dest : sink) (amount : Tez_repr.t) (origin : A)
  : M?
    (Raw_context.t × (Receipt_repr.balance × Receipt_repr.balance_update × A)) :=
  let? '(ctxt, balance) :=
    match dest with
    | Sink_infinite infinite_sink
      let sink :=
        match infinite_sink with
        | Storage_feesReceipt_repr.Storage_fees
        | Double_signing_punishmentsReceipt_repr.Double_signing_punishments
        | Lost_endorsing_rewards d_value p_value r_value
          Receipt_repr.Lost_endorsing_rewards d_value p_value r_value
        | Tx_rollup_rejection_punishments
          Receipt_repr.Tx_rollup_rejection_punishments
        | BurnedReceipt_repr.Burned
        end in
      return? (ctxt, sink)
    | Sink_container container
      match container with
      | Contract dest
        let? ctxt :=
          Contract_storage.credit_only_call_from_token ctxt dest amount in
        return? (ctxt, (Receipt_repr.Contract dest))
      | Collected_commitments bpkh
        let? ctxt :=
          Commitment_storage.increase_commitment_only_call_from_token ctxt bpkh
            amount in
        return? (ctxt, (Receipt_repr.Commitments bpkh))
      | Delegate_balance delegate
        let contract := Contract_repr.implicit_contract delegate in
        let? ctxt :=
          Contract_storage.increase_balance_only_call_from_token ctxt contract
            amount in
        return? (ctxt, (Receipt_repr.Contract contract))
      | (Frozen_deposits delegate) as dest
        let? '(ctxt, allocated) := allocated ctxt dest in
        let? ctxt :=
          if Pervasives.not allocated then
            Frozen_deposits_storage.init_value ctxt delegate
          else
            return? ctxt in
        let? ctxt :=
          Frozen_deposits_storage.credit_only_call_from_token ctxt delegate
            amount in
        return? (ctxt, (Receipt_repr.Deposits delegate))
      | Block_fees
        let? ctxt :=
          Raw_context.credit_collected_fees_only_call_from_token ctxt amount in
        return? (ctxt, Receipt_repr.Block_fees)
      | Frozen_bonds contract bond_id
        let? ctxt :=
          Contract_storage.credit_bond_only_call_from_token ctxt contract
            bond_id amount in
        return? (ctxt, (Receipt_repr.Frozen_bonds contract bond_id))
      end
    end in
  return? (ctxt, (balance, (Receipt_repr.Credited amount), origin)).

Definition spend {A : Set}
  (ctxt : Raw_context.t) (src : source) (amount : Tez_repr.t) (origin : A)
  : M?
    (Raw_context.t × (Receipt_repr.balance × Receipt_repr.balance_update × A)) :=
  let? '(ctxt, balance) :=
    match src with
    | Source_infinite infinite_source
      let src :=
        match infinite_source with
        | BootstrapReceipt_repr.Bootstrap
        | InvoiceReceipt_repr.Invoice
        | Initial_commitmentsReceipt_repr.Initial_commitments
        | MintedReceipt_repr.Minted
        | Liquidity_baking_subsidiesReceipt_repr.Liquidity_baking_subsidies
        | Revelation_rewardsReceipt_repr.Nonce_revelation_rewards
        | Double_signing_evidence_rewards
          Receipt_repr.Double_signing_evidence_rewards
        | Endorsing_rewardsReceipt_repr.Endorsing_rewards
        | Baking_rewardsReceipt_repr.Baking_rewards
        | Baking_bonusesReceipt_repr.Baking_bonuses
        | Tx_rollup_rejection_rewards
          Receipt_repr.Tx_rollup_rejection_rewards
        end in
      return? (ctxt, src)
    | Source_container container
      match container with
      | Contract src
        let? ctxt := Contract_storage.spend_only_call_from_token ctxt src amount
          in
        return? (ctxt, (Receipt_repr.Contract src))
      | Collected_commitments bpkh
        let? ctxt :=
          Commitment_storage.decrease_commitment_only_call_from_token ctxt bpkh
            amount in
        return? (ctxt, (Receipt_repr.Commitments bpkh))
      | Delegate_balance delegate
        let contract := Contract_repr.implicit_contract delegate in
        let? ctxt :=
          Contract_storage.decrease_balance_only_call_from_token ctxt contract
            amount in
        return? (ctxt, (Receipt_repr.Contract contract))
      | Frozen_deposits delegate
        let? ctxt :=
          Frozen_deposits_storage.spend_only_call_from_token ctxt delegate
            amount in
        return? (ctxt, (Receipt_repr.Deposits delegate))
      | Block_fees
        let? ctxt :=
          Raw_context.spend_collected_fees_only_call_from_token ctxt amount in
        return? (ctxt, Receipt_repr.Block_fees)
      | Frozen_bonds contract bond_id
        let? ctxt :=
          Contract_storage.spend_bond_only_call_from_token ctxt contract bond_id
            amount in
        return? (ctxt, (Receipt_repr.Frozen_bonds contract bond_id))
      end
    end in
  return? (ctxt, (balance, (Receipt_repr.Debited amount), origin)).

Definition transfer_n (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t list (source × Tez_repr.t) sink
  M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (ctxt : Raw_context.t) ⇒
    fun (src : list (source × Tez_repr.t)) ⇒
      fun (dest : sink) ⇒
        let sources :=
          List.filter
            (fun (function_parameter : source × Tez_repr.t) ⇒
              let '(_, am) := function_parameter in
              Tez_repr.op_ltgt am Tez_repr.zero) src in
        match sources with
        | []return? (ctxt, nil)
        | cons _ _
          let? '(ctxt, amount, debit_logs) :=
            List.fold_left_es
              (fun (function_parameter :
                Raw_context.t × Tez_repr.t ×
                  list
                    (Receipt_repr.balance × Receipt_repr.balance_update ×
                      Receipt_repr.update_origin)) ⇒
                let '(ctxt, total, debit_logs) := function_parameter in
                fun (function_parameter : source × Tez_repr.t) ⇒
                  let '(source, amount) := function_parameter in
                  let? '(ctxt, debit_log) := spend ctxt source amount origin in
                  let? total := Tez_repr.op_plusquestion amount total in
                  return? (ctxt, total, (cons debit_log debit_logs)))
              (ctxt, Tez_repr.zero, nil) sources in
          let? '(ctxt, credit_log) := credit ctxt dest amount origin in
          let? ctxt :=
            List.fold_left_es
              (fun (ctxt : Raw_context.t) ⇒
                fun (function_parameter : source × Tez_repr.t) ⇒
                  let '(source, _amount) := function_parameter in
                  match source with
                  |
                    (Source_container (Contract contract) |
                    Source_container (Frozen_bonds contract _)) ⇒
                    Contract_storage.ensure_deallocated_if_empty ctxt contract
                  | _return? ctxt
                  end) ctxt sources in
          let balance_updates := List.rev (cons credit_log debit_logs) in
          return? (ctxt, balance_updates)
        end.

Definition transfer (op_staroptstar : option Receipt_repr.update_origin)
  : Raw_context.t source sink Tez_repr.t
  M?
    (Raw_context.t ×
      list
        (Receipt_repr.balance × Receipt_repr.balance_update ×
          Receipt_repr.update_origin)) :=
  let origin :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | NoneReceipt_repr.Block_application
    end in
  fun (ctxt : Raw_context.t) ⇒
    fun (src : source) ⇒
      fun (dest : sink) ⇒
        fun (amount : Tez_repr.t) ⇒
          transfer_n (Some origin) ctxt [ (src, amount) ] dest.