⚗️ Liquidity_baking_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Liquidity_baking_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.

Lemma liquidity_baking_toggle_vote_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True)
    Liquidity_baking_repr.liquidity_baking_toggle_vote_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  ecrush.
Qed.
#[global] Hint Resolve liquidity_baking_toggle_vote_encoding_is_valid :
  Data_encoding_db.

Module Toggle_EMA.
  Import Liquidity_baking_repr.

  (* Property about the [Toggle_EMA.of_int32), [Toggle_EMA.to_int32] *)
  Lemma of_int32_to_int32 : ∀ (x : int32),
    Toggle_EMA.check_bounds x = true →
    match Toggle_EMA.of_int32 x with
    | Pervasives.Ok y ⇒ Toggle_EMA.to_int32 y = x
    | Pervasives.Error e ⇒ True
    end.
  Proof.
    intros x H. destruct (Toggle_EMA.of_int32 x) eqn:Y; [|trivial].
    unfold Toggle_EMA.of_int32 in ×. sauto q: on.
  Qed.

  (* Property about the [Toggle_EMA.of_int32], [Toggle_EMA.to_int32] *)
  Lemma of_int32_for_encoding_to_int32 : ∀ x,
    Toggle_EMA.check_bounds x = true →
    Toggle_EMA.of_int32_for_encoding (Toggle_EMA.to_int32 x) =
      Pervasives.Ok x.
  Proof.
    intros x H; unfold Toggle_EMA.of_int32_for_encoding, Toggle_EMA.to_int32;
      hauto lq: on.
  Qed.

The validity predicate for [encoding_is_valid].

  Module Valid.
    Definition t (x : int32) : Prop := 0 ≤ x ≤ 2000000000.
  End Valid.

Encoding [encoding] is valid.

  Lemma encoding_is_valid :
    Data_encoding.Valid.t Valid.t
      Toggle_EMA.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto.
    intros x [].
    unfold
      Toggle_EMA.of_int32_for_encoding,
      Toggle_EMA.to_int32,
      Toggle_EMA.check_bounds.
    split; [|destruct (_ && _)%bool eqn:D]; lia.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Toggle_EMA.