🪅 Token.v

Translated OCaml

See proofs, Gitlab , 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.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
| Sc_rollup_refutation_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
| Tx_rollup_rejection_punishments : infinite_sink
| Sc_rollup_refutation_punishments : infinite_sink
| Burned : 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 := Commitment_storage._exists ctxt bpkh in
    return? (ctxt, allocated)
  | Delegate_balance delegate ⇒
    let contract := Contract_repr.Implicit delegate in
    let allocated := Contract_storage.allocated ctxt contract in
    return? (ctxt, allocated)
  | Frozen_deposits delegate ⇒
    let contract := Contract_repr.Implicit delegate in
    let allocated := Frozen_deposits_storage.allocated ctxt contract in
    return? (ctxt, allocated)
  | Block_fees ⇒ return? (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 delegate in
    let? balance :=
      Storage.Contract.Spendable_balance.(Storage_sigs.Indexed_data_storage_with_local_context.get)
        ctxt contract in
    return? (ctxt, balance)
  | Frozen_deposits delegate ⇒
    let contract := Contract_repr.Implicit delegate in
    let? frozen_deposits := Frozen_deposits_storage.find ctxt contract in
    let balance :=
      match frozen_deposits with
      | None ⇒ Tez_repr.zero
      | Some frozen_deposits ⇒
        frozen_deposits.(Storage.deposits.current_amount)
      end in
    return? (ctxt, balance)
  | Block_fees ⇒ return? (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_fees ⇒ Receipt_repr.Storage_fees
        | Double_signing_punishments ⇒ Receipt_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
        | Sc_rollup_refutation_punishments ⇒
          Receipt_repr.Sc_rollup_refutation_punishments
        | Burned ⇒ Receipt_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 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
        | Bootstrap ⇒ Receipt_repr.Bootstrap
        | Invoice ⇒ Receipt_repr.Invoice
        | Initial_commitments ⇒ Receipt_repr.Initial_commitments
        | Minted ⇒ Receipt_repr.Minted
        | Liquidity_baking_subsidies ⇒ Receipt_repr.Liquidity_baking_subsidies
        | Revelation_rewards ⇒ Receipt_repr.Nonce_revelation_rewards
        | Double_signing_evidence_rewards ⇒
          Receipt_repr.Double_signing_evidence_rewards
        | Endorsing_rewards ⇒ Receipt_repr.Endorsing_rewards
        | Baking_rewards ⇒ Receipt_repr.Baking_rewards
        | Baking_bonuses ⇒ Receipt_repr.Baking_bonuses
        | Tx_rollup_rejection_rewards ⇒
          Receipt_repr.Tx_rollup_rejection_rewards
        | Sc_rollup_refutation_rewards ⇒
          Receipt_repr.Sc_rollup_refutation_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 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_starsthstar ⇒ op_starsthstar
    | None ⇒ Receipt_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_starsthstar ⇒ op_starsthstar
    | None ⇒ Receipt_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.