Skip to main content

⚗️ Liquidity_baking_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.

Inductive liquidity_baking_toggle_vote : Set :=
| LB_on : liquidity_baking_toggle_vote
| LB_off : liquidity_baking_toggle_vote
| LB_pass : liquidity_baking_toggle_vote.

Definition liquidity_baking_toggle_vote_encoding
  : Data_encoding.encoding liquidity_baking_toggle_vote :=
  let of_int8 (function_parameter : int)
    : Pervasives.result liquidity_baking_toggle_vote string :=
    match function_parameter with
    | 0 ⇒ Pervasives.Ok LB_on
    | 1 ⇒ Pervasives.Ok LB_off
    | 2 ⇒ Pervasives.Ok LB_pass
    | _Pervasives.Error "liquidity_baking_toggle_vote_of_int8"
    end in
  let to_int8 (function_parameter : liquidity_baking_toggle_vote) : int :=
    match function_parameter with
    | LB_on ⇒ 0
    | LB_off ⇒ 1
    | LB_pass ⇒ 2
    end in
  (let arg := Data_encoding.def "liquidity_baking_toggle_vote" in
  fun (eta : Data_encoding.encoding liquidity_baking_toggle_vote) ⇒
    arg None None eta)
    (Data_encoding.splitted
      (Data_encoding.string_enum
        [ ("on", LB_on); ("off", LB_off); ("pass", LB_pass) ])
      (Data_encoding.conv_with_guard to_int8 of_int8 None Data_encoding.int8)).

Module Toggle_EMA.
  Definition t : Set := Int32.t.

  Definition check_bounds (x_value : int32) : bool :=
    (0 i32 x_value) && (x_value i32 2000000000).

  Definition of_int32 (x_value : int32) : M? int32 :=
    if check_bounds x_value then
      return? x_value
    else
      Error_monad.fail
        (Build_extensible "Liquidity_baking_toggle_ema_out_of_bound" int32
          x_value).

  Definition zero : int32 := Int32.zero.

  Definition of_int32_for_encoding (x_value : int32)
    : Pervasives.result int32 string :=
    if check_bounds x_value then
      Pervasives.Ok x_value
    else
      Pervasives.Error "out of bounds".

  Definition to_int32 {A : Set} (ema : A) : A := ema.

  Definition z_1999 : Z.t := Z.of_int 1999.

  Definition z_2000 : Z.t := Z.of_int 2000.

  Definition attenuate (z_value : Z.t) : Z.t := (z_1999 ×Z z_value) /Z z_2000.

  Definition z_1_000_000_000 : Z.t := Z.of_int 1000000000.

  Definition recenter (f_value : Z.t Z.t) (ema : Z.t) : Z.t :=
    z_1_000_000_000 +Z (f_value (ema -Z z_1_000_000_000)).

  Definition z_500_000 : Z.t := Z.of_int 500000.

  Definition update_ema_off (ema : int32) : int32 :=
    let ema := Z.of_int32 ema in
    Z.to_int32 (recenter (fun (ema : Z.t) ⇒ (attenuate ema) +Z z_500_000) ema).

  Definition update_ema_on (ema : int32) : int32 :=
    let ema := Z.of_int32 ema in
    Z.to_int32 (recenter (fun (ema : Z.t) ⇒ (attenuate ema) -Z z_500_000) ema).

  Definition op_lt : int32 int32 bool := Compare.Int32.(Compare.S.op_lt).

  Definition encoding : Data_encoding.encoding int32 :=
    Data_encoding.conv_with_guard to_int32 of_int32_for_encoding None
      Data_encoding.int32_value.
End Toggle_EMA.

Definition compute_new_ema
  (toggle_vote : liquidity_baking_toggle_vote) (ema : Toggle_EMA.t)
  : Toggle_EMA.t :=
  match toggle_vote with
  | LB_passema
  | LB_offToggle_EMA.update_ema_off ema
  | LB_onToggle_EMA.update_ema_on ema
  end.