🗳️ Voting_period_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Lemma string_of_kind_inj : ∀ x y,
Voting_period_repr.string_of_kind x = Voting_period_repr.string_of_kind y →
x = y.
intros x y; destruct x, y; easy.
Qed.
Lemma kind_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Voting_period_repr.kind_encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve kind_encoding_is_valid : Data_encoding_db.
Lemma succ_kind_inj : ∀ x y,
Voting_period_repr.succ_kind x = Voting_period_repr.succ_kind y →
x = y.
intros x y; destruct x, y; easy.
Qed.
Lemma succ_kind_diff : ∀ x, Voting_period_repr.succ_kind x ≠ x.
intro x; destruct x; easy.
Qed.
Module Valid.
Import Voting_period_repr.voting_period.
Record t (x : Voting_period_repr.voting_period) : Prop := {
index : Int32.Valid.t x.(index);
start_position : Int32.Valid.t x.(start_position);
}.
End Valid.
Module Info.
Module Valid.
Import Voting_period_repr.info.
Record t (x : Voting_period_repr.info) : Prop := {
voting_period : Valid.t x.(voting_period);
position : Int32.Valid.t x.(position);
remaining : Int32.Valid.t x.(remaining);
}.
End Valid.
End Info.
Lemma encoding_is_valid :
Data_encoding.Valid.t Valid.t Voting_period_repr.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma info_encoding_is_valid :
Data_encoding.Valid.t Info.Valid.t Voting_period_repr.info_encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve info_encoding_is_valid : Data_encoding_db.
Lemma compare_is_valid :
Compare.Valid.t
(fun _ ⇒ True)
(fun period ⇒ period.(Voting_period_repr.voting_period.index))
Voting_period_repr.compare.
Proof.
apply (Compare.equality (
let proj x := x.(Voting_period_repr.voting_period.index) in
Compare.projection proj Compare.Int32.(Compare.S.compare)
)); [sfirstorder|].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
apply Compare.int32_is_valid.
}
all: sfirstorder.
Qed.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Lemma string_of_kind_inj : ∀ x y,
Voting_period_repr.string_of_kind x = Voting_period_repr.string_of_kind y →
x = y.
intros x y; destruct x, y; easy.
Qed.
Lemma kind_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Voting_period_repr.kind_encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve kind_encoding_is_valid : Data_encoding_db.
Lemma succ_kind_inj : ∀ x y,
Voting_period_repr.succ_kind x = Voting_period_repr.succ_kind y →
x = y.
intros x y; destruct x, y; easy.
Qed.
Lemma succ_kind_diff : ∀ x, Voting_period_repr.succ_kind x ≠ x.
intro x; destruct x; easy.
Qed.
Module Valid.
Import Voting_period_repr.voting_period.
Record t (x : Voting_period_repr.voting_period) : Prop := {
index : Int32.Valid.t x.(index);
start_position : Int32.Valid.t x.(start_position);
}.
End Valid.
Module Info.
Module Valid.
Import Voting_period_repr.info.
Record t (x : Voting_period_repr.info) : Prop := {
voting_period : Valid.t x.(voting_period);
position : Int32.Valid.t x.(position);
remaining : Int32.Valid.t x.(remaining);
}.
End Valid.
End Info.
Lemma encoding_is_valid :
Data_encoding.Valid.t Valid.t Voting_period_repr.encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma info_encoding_is_valid :
Data_encoding.Valid.t Info.Valid.t Voting_period_repr.info_encoding.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve info_encoding_is_valid : Data_encoding_db.
Lemma compare_is_valid :
Compare.Valid.t
(fun _ ⇒ True)
(fun period ⇒ period.(Voting_period_repr.voting_period.index))
Voting_period_repr.compare.
Proof.
apply (Compare.equality (
let proj x := x.(Voting_period_repr.voting_period.index) in
Compare.projection proj Compare.Int32.(Compare.S.compare)
)); [sfirstorder|].
eapply Compare.implies.
{ eapply Compare.projection_is_valid.
apply Compare.int32_is_valid.
}
all: sfirstorder.
Qed.
The function [position_since] is valid.
Lemma position_since_is_valid level voting_period :
Int32.Valid.t (Voting_period_repr.position_since level voting_period).
Proof.
unfold Voting_period_repr.position_since.
lia.
Qed.
Int32.Valid.t (Voting_period_repr.position_since level voting_period).
Proof.
unfold Voting_period_repr.position_since.
lia.
Qed.
The function [remaining_blocks] is valid.
Lemma remaining_blocks_is_valid level voting_period blocks_per_voting_period :
Int32.Valid.t (
Voting_period_repr.remaining_blocks
level voting_period blocks_per_voting_period
).
Proof.
unfold Voting_period_repr.remaining_blocks.
lia.
Qed.
Int32.Valid.t (
Voting_period_repr.remaining_blocks
level voting_period blocks_per_voting_period
).
Proof.
unfold Voting_period_repr.remaining_blocks.
lia.
Qed.
The function [raw_reset] is valid
Lemma raw_reset_is_valid
(v : Voting_period_repr.voting_period)
(i : int32) :
Voting_period_repr.Valid.t v →
Int32.Valid.t i →
Voting_period_repr.Valid.t (Voting_period_repr.raw_reset v i).
Proof.
Admitted.
(v : Voting_period_repr.voting_period)
(i : int32) :
Voting_period_repr.Valid.t v →
Int32.Valid.t i →
Voting_period_repr.Valid.t (Voting_period_repr.raw_reset v i).
Proof.
Admitted.