⚗️ Liquidity_baking_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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Definition get_cpmm_address : Raw_context.t → M? Contract_hash.t :=
  Storage.Liquidity_baking.Cpmm_address.(Storage_sigs.Single_data_storage.get).

Definition get_toggle_ema (ctxt : Raw_context.t)
  : M? Liquidity_baking_repr.Toggle_EMA.t :=
  let? ema :=
    Storage.Liquidity_baking.Toggle_ema.(Storage_sigs.Single_data_storage.get)
      ctxt in
  Liquidity_baking_repr.Toggle_EMA.of_int32 ema.

Definition on_cpmm_exists {A : Set}
  (ctxt : Raw_context.t)
  (f_value : Raw_context.t → Contract_hash.t → M? (Raw_context.t × list A))
  : M? (Raw_context.t × list A) :=
  let? cpmm_contract := get_cpmm_address ctxt in
  let function_parameter :=
    Contract_storage._exists ctxt (Contract_repr.Originated cpmm_contract) in
  match function_parameter with
  | false ⇒ return? (ctxt, nil)
  | true ⇒ f_value ctxt cpmm_contract
  end.

Definition update_toggle_ema
  (ctxt : Raw_context.t)
  (toggle_vote : Liquidity_baking_repr.liquidity_baking_toggle_vote)
  : M? (Raw_context.t × Liquidity_baking_repr.Toggle_EMA.t) :=
  let? old_ema := get_toggle_ema ctxt in
  let new_ema := Liquidity_baking_repr.compute_new_ema toggle_vote old_ema in
  let? ctxt :=
    Storage.Liquidity_baking.Toggle_ema.(Storage_sigs.Single_data_storage.update)
      ctxt (Liquidity_baking_repr.Toggle_EMA.to_int32 new_ema) in
  return? (ctxt, new_ema).

Definition check_ema_below_threshold
  (ctxt : Raw_context.t) (ema : Liquidity_baking_repr.Toggle_EMA.t) : bool :=
  Liquidity_baking_repr.Toggle_EMA.op_lt ema
    (Constants_storage.liquidity_baking_toggle_ema_threshold ctxt).

Definition on_subsidy_allowed {A : Set}
  (ctxt : Raw_context.t)
  (toggle_vote : Liquidity_baking_repr.liquidity_baking_toggle_vote)
  (f_value : Raw_context.t → Contract_hash.t → M? (Raw_context.t × list A))
  : M? (Raw_context.t × list A × Liquidity_baking_repr.Toggle_EMA.t) :=
  let? '(ctxt, toggle_ema) := update_toggle_ema ctxt toggle_vote in
  if check_ema_below_threshold ctxt toggle_ema then
    let? '(ctxt, operation_results) := on_cpmm_exists ctxt f_value in
    return? (ctxt, operation_results, toggle_ema)
  else
    return? (ctxt, nil, toggle_ema).