💍 Commitment_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.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tez_repr.

Definition _exists : Raw_context.t → Blinded_public_key_hash.t → bool :=
  Storage.Commitments.(Storage_sigs.Indexed_data_storage.mem).

Definition committed_amount
  (ctxt : Raw_context.t) (bpkh : Blinded_public_key_hash.t) : M? Tez_repr.t :=
  let? balance :=
    Storage.Commitments.(Storage_sigs.Indexed_data_storage.find) ctxt bpkh in
  return? (Option.value_value balance Tez_repr.zero).

Definition increase_commitment_only_call_from_token
  (ctxt : Raw_context.t) (bpkh : Blinded_public_key_hash.t)
  (amount : Tez_repr.t) : M? Raw_context.t :=
  if Tez_repr.op_eq amount Tez_repr.zero then
    return? ctxt
  else
    let? balance := committed_amount ctxt bpkh in
    let? new_balance := Tez_repr.op_plusquestion amount balance in
    Error_monad.op_gtpipeeq
      (Storage.Commitments.(Storage_sigs.Indexed_data_storage.add) ctxt bpkh
        new_balance) Error_monad.ok.

Definition decrease_commitment_only_call_from_token
  (ctxt : Raw_context.t) (bpkh : Blinded_public_key_hash.t)
  (amount : Tez_repr.t) : M? Raw_context.t :=
  let? balance := committed_amount ctxt bpkh in
  let? new_balance := Tez_repr.op_minusquestion balance amount in
  if Tez_repr.op_eq new_balance Tez_repr.zero then
    Error_monad.op_gtpipeeq
      (Storage.Commitments.(Storage_sigs.Indexed_data_storage.remove) ctxt bpkh)
      Error_monad.ok
  else
    Error_monad.op_gtpipeeq
      (Storage.Commitments.(Storage_sigs.Indexed_data_storage.add) ctxt bpkh
        new_balance) Error_monad.ok.