⚗️ Liquidity_baking_repr.v
Proofs
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.
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].
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.
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.