Skip to main content

⚗️ Liquidity_baking_storage.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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Contract_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Definition get_cpmm_address : Raw_context.t M? Contract_repr.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_repr.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 cpmm_contract in
  match function_parameter with
  | falsereturn? (ctxt, nil)
  | truef_value ctxt cpmm_contract
  end.

Definition check_below_sunset (ctxt : Raw_context.t) : bool :=
  let sunset_level := Constants_storage.liquidity_baking_sunset_level ctxt in
  let level :=
    Raw_level_repr.to_int32 (Level_storage.current ctxt).(Level_repr.t.level) in
  level <i32 sunset_level.

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_repr.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) && (check_below_sunset ctxt)
  then
    let? '(ctxt, operation_results) := on_cpmm_exists ctxt f_value in
    return? (ctxt, operation_results, toggle_ema)
  else
    return? (ctxt, nil, toggle_ema).