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

Definition init_value
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? Raw_context.t :=
  Storage.Contract.Frozen_deposits.(Storage_sigs.Indexed_data_storage.init_value)
    ctxt (Contract_repr.Implicit delegate)
    {| Storage.deposits.initial_amount := Tez_repr.zero;
      Storage.deposits.current_amount := Tez_repr.zero; |}.

Definition allocated : Raw_context.t → Contract_repr.t → bool :=
  Storage.Contract.Frozen_deposits.(Storage_sigs.Indexed_data_storage.mem).

Definition get : Raw_context.t → Contract_repr.t → M? Storage.deposits :=
  Storage.Contract.Frozen_deposits.(Storage_sigs.Indexed_data_storage.get).

Definition find
  : Raw_context.t → Contract_repr.t → M? (option Storage.deposits) :=
  Storage.Contract.Frozen_deposits.(Storage_sigs.Indexed_data_storage.find).

Definition update_balance {A : Set}
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (f_value : Tez_repr.t → A → M? Tez_repr.t) (amount : A)
  : M? Raw_context.t :=
  let delegate_contract := Contract_repr.Implicit delegate in
  let? frozen_deposits := get ctxt delegate_contract in
  let? new_amount :=
    f_value frozen_deposits.(Storage.deposits.current_amount) amount in
  Storage.Contract.Frozen_deposits.(Storage_sigs.Indexed_data_storage.update)
    ctxt delegate_contract
    (Storage.deposits.with_current_amount new_amount frozen_deposits).

Definition credit_only_call_from_token
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (amount : Tez_repr.t) : M? Raw_context.t :=
  update_balance ctxt delegate Tez_repr.op_plusquestion amount.

Definition spend_only_call_from_token
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (amount : Tez_repr.t) : M? Raw_context.t :=
  update_balance ctxt delegate Tez_repr.op_minusquestion amount.

Definition update_initial_amount
  (ctxt : Raw_context.t) (delegate_contract : Contract_repr.t)
  (deposits_cap : Tez_repr.t) : M? Raw_context.t :=
  let? frozen_deposits := get ctxt delegate_contract in
  Storage.Contract.Frozen_deposits.(Storage_sigs.Indexed_data_storage.update)
    ctxt delegate_contract
    (Storage.deposits.with_initial_amount deposits_cap frozen_deposits).