🪜 Level_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Lemma compare_is_valid : Compare.Valid.t
(fun _ ⇒ True)
(fun '{| Level_repr.t.level := level |} ⇒ level)
Level_repr.compare.
Proof.
apply
(Compare.projection_is_valid
(fun pat : Level_repr.t.record ⇒ pat.(Level_repr.t.level))
Compare.int32_is_valid).
Qed.
Module level_from_raw_with_era_invariants.
Import Level_repr.t.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Z.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Lemma compare_is_valid : Compare.Valid.t
(fun _ ⇒ True)
(fun '{| Level_repr.t.level := level |} ⇒ level)
Level_repr.compare.
Proof.
apply
(Compare.projection_is_valid
(fun pat : Level_repr.t.record ⇒ pat.(Level_repr.t.level))
Compare.int32_is_valid).
Qed.
Module level_from_raw_with_era_invariants.
Import Level_repr.t.
These conditions are used on the
[Level_repr.level_from_raw_with_era] to build a level
from an [int] and a [Level_repr.cycle_era] @TODO eliminate the output as a field of the record and
prove suitable computation lemma @TODO put outside the Valid module
Record t (era : Level_repr.cycle_era) (first_level_in_alpha_family level0 :
Raw_level_repr.raw_level) (output_level : Level_repr.t): Prop := {
level : Int32.Valid.t level0 ∧ output_level.(Level_repr.t.level) = level0 ;
level_position_in_era : Int32.Valid.non_negative (
level0 -Z era.(Level_repr.cycle_era.first_level));
level_position: (level0 -Z first_level_in_alpha_family) =
output_level.(level_position) ∧
Int32.Valid.non_negative ( level0 -Z first_level_in_alpha_family);
cycle : (output_level.(cycle) = era.(Level_repr.cycle_era.first_cycle) +Z
(level0 -Z era.(Level_repr.cycle_era.first_level)) /Z
era.(Level_repr.cycle_era.blocks_per_cycle)) ∧
Int32.Valid.t (level0 -Z era.(Level_repr.cycle_era.first_level)) ∧
Int32.Valid.non_negative ((level0 -Z era.(Level_repr.cycle_era.first_level))
/Z era.(Level_repr.cycle_era.blocks_per_cycle)) ∧
Int32.Valid.non_negative (era.(Level_repr.cycle_era.first_cycle) +Z
(level0 -Z era.(Level_repr.cycle_era.first_level)) /Z
era.(Level_repr.cycle_era.blocks_per_cycle));
cycle_position : (output_level.(cycle_position) =
rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle)) ∧
Int32.Valid.t (rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle));
expected_commitment :
(output_level.(expected_commitment) =
(rem
(rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle))
era.(Level_repr.cycle_era.blocks_per_commitment) =?
era.(Level_repr.cycle_era.blocks_per_commitment) -Z 1)) ∧
Int32.Valid.t
(era.(Level_repr.cycle_era.blocks_per_commitment) -Z 1) ∧
Int32.Valid.t
(rem
(rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle))
era.(Level_repr.cycle_era.blocks_per_commitment));
}.
End level_from_raw_with_era_invariants.
Module Valid.
Import Level_repr.t.
Record t (l : Level_repr.t) : Prop := {
Raw_level_repr.raw_level) (output_level : Level_repr.t): Prop := {
level : Int32.Valid.t level0 ∧ output_level.(Level_repr.t.level) = level0 ;
level_position_in_era : Int32.Valid.non_negative (
level0 -Z era.(Level_repr.cycle_era.first_level));
level_position: (level0 -Z first_level_in_alpha_family) =
output_level.(level_position) ∧
Int32.Valid.non_negative ( level0 -Z first_level_in_alpha_family);
cycle : (output_level.(cycle) = era.(Level_repr.cycle_era.first_cycle) +Z
(level0 -Z era.(Level_repr.cycle_era.first_level)) /Z
era.(Level_repr.cycle_era.blocks_per_cycle)) ∧
Int32.Valid.t (level0 -Z era.(Level_repr.cycle_era.first_level)) ∧
Int32.Valid.non_negative ((level0 -Z era.(Level_repr.cycle_era.first_level))
/Z era.(Level_repr.cycle_era.blocks_per_cycle)) ∧
Int32.Valid.non_negative (era.(Level_repr.cycle_era.first_cycle) +Z
(level0 -Z era.(Level_repr.cycle_era.first_level)) /Z
era.(Level_repr.cycle_era.blocks_per_cycle));
cycle_position : (output_level.(cycle_position) =
rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle)) ∧
Int32.Valid.t (rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle));
expected_commitment :
(output_level.(expected_commitment) =
(rem
(rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle))
era.(Level_repr.cycle_era.blocks_per_commitment) =?
era.(Level_repr.cycle_era.blocks_per_commitment) -Z 1)) ∧
Int32.Valid.t
(era.(Level_repr.cycle_era.blocks_per_commitment) -Z 1) ∧
Int32.Valid.t
(rem
(rem (level0 -Z era.(Level_repr.cycle_era.first_level))
era.(Level_repr.cycle_era.blocks_per_cycle))
era.(Level_repr.cycle_era.blocks_per_commitment));
}.
End level_from_raw_with_era_invariants.
Module Valid.
Import Level_repr.t.
Record t (l : Level_repr.t) : Prop := {
@Q what the use of this record?
level : Raw_level_repr.Valid.t l.(level);
level_position : Int32.Valid.t l.(level_position);
cycle : Cycle_repr.Valid.t l.(cycle);
cycle_position : Int32.Valid.t l.(cycle_position);
}.
End Valid.
level_position : Int32.Valid.t l.(level_position);
cycle : Cycle_repr.Valid.t l.(cycle);
cycle_position : Int32.Valid.t l.(cycle_position);
}.
End Valid.
The encoding [encoding] is valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t Level_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] H;
repeat split; cbn; try apply H.
destruct H; cbn in ×. clear - cycle0. lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma diff_value_eq_zero : ∀ l, Level_repr.diff_value l l = 0.
Proof.
intro l; unfold Level_repr.diff_value, Raw_level_repr.to_int32.
autounfold with tezos_z.
now rewrite Z.sub_diag.
Qed.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] H;
repeat split; cbn; try apply H.
destruct H; cbn in ×. clear - cycle0. lia.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Lemma diff_value_eq_zero : ∀ l, Level_repr.diff_value l l = 0.
Proof.
intro l; unfold Level_repr.diff_value, Raw_level_repr.to_int32.
autounfold with tezos_z.
now rewrite Z.sub_diag.
Qed.
Given the [Level_repr.Valid.invariants],
[level_from_raw_with_era] reconstruct the
same level @TODO without the forall for uniformity
Lemma level_from_raw_with_era_id :
∀ (era : _) (level_in_alpha_family level : Raw_level_repr.raw_level)
(output : Level_repr.t),
level_from_raw_with_era_invariants.t era
level_in_alpha_family level output →
Level_repr.level_from_raw_with_era era level_in_alpha_family
level = return? output.
Proof.
intros [] level_in_alpha_family level [] [].
unfold
Level_repr.level_from_raw_with_era,
Raw_level_repr.diff_value;
autounfold with tezos_z; cbn in × ;
rewrite Int32.normalize_identity by lia.
step; [|lia].
unfold Cycle_repr.add;
autounfold with tezos_z; cbn in ×.
rewrite !Int32.normalize_identity by lia.
step; [|lia]; cbn.
now repeat f_equal.
Qed.
(* @Proto_alpha: [level_from_raw_level_from_raw] is an alias of [..._aux_exn] *)
Lemma level_from_raw_level_from_raw_aux_exn_eq :
Level_repr.level_from_raw_aux_exn = Level_repr.level_from_raw.
Proof.
unfold Level_repr.level_from_raw. reflexivity.
Qed.
Module Cycle_era.
Module Valid.
Import Level_repr.cycle_era.
Record t (cycle : Level_repr.cycle_era) : Prop := {
first_level : Raw_level_repr.Valid.t cycle.(first_level);
first_cycle : Int32.Valid.t cycle.(first_cycle);
blocks_per_cycle : Int32.Valid.t cycle.(blocks_per_cycle);
blocks_per_commitment : Int32.Valid.t cycle.(blocks_per_commitment);
}.
End Valid.
End Cycle_era.
Lemma cycle_era_encoding_is_valid :
Data_encoding.Valid.t Cycle_era.Valid.t Level_repr.cycle_era_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
Module Cycle_eras.
Module Valid.
∀ (era : _) (level_in_alpha_family level : Raw_level_repr.raw_level)
(output : Level_repr.t),
level_from_raw_with_era_invariants.t era
level_in_alpha_family level output →
Level_repr.level_from_raw_with_era era level_in_alpha_family
level = return? output.
Proof.
intros [] level_in_alpha_family level [] [].
unfold
Level_repr.level_from_raw_with_era,
Raw_level_repr.diff_value;
autounfold with tezos_z; cbn in × ;
rewrite Int32.normalize_identity by lia.
step; [|lia].
unfold Cycle_repr.add;
autounfold with tezos_z; cbn in ×.
rewrite !Int32.normalize_identity by lia.
step; [|lia]; cbn.
now repeat f_equal.
Qed.
(* @Proto_alpha: [level_from_raw_level_from_raw] is an alias of [..._aux_exn] *)
Lemma level_from_raw_level_from_raw_aux_exn_eq :
Level_repr.level_from_raw_aux_exn = Level_repr.level_from_raw.
Proof.
unfold Level_repr.level_from_raw. reflexivity.
Qed.
Module Cycle_era.
Module Valid.
Import Level_repr.cycle_era.
Record t (cycle : Level_repr.cycle_era) : Prop := {
first_level : Raw_level_repr.Valid.t cycle.(first_level);
first_cycle : Int32.Valid.t cycle.(first_cycle);
blocks_per_cycle : Int32.Valid.t cycle.(blocks_per_cycle);
blocks_per_commitment : Int32.Valid.t cycle.(blocks_per_commitment);
}.
End Valid.
End Cycle_era.
Lemma cycle_era_encoding_is_valid :
Data_encoding.Valid.t Cycle_era.Valid.t Level_repr.cycle_era_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
Module Cycle_eras.
Module Valid.
@TODO @Q write one's own [isSorted] predicates?
(* @Q @TODO should we go tack to output [cycles = cycle_eras']
in the second case? *)
Record t (cycle_eras : list Level_repr.cycle_era) : Prop := {
can_create :
match Level_repr.create_cycle_eras cycle_eras with
| Pervasives.Ok cycle_eras' ⇒ cycle_eras' = cycle_eras
| Pervasives.Error _ ⇒ False
end;
each_cycle_era_valid : List.Forall Cycle_era.Valid.t cycle_eras;
}.
End Valid.
in the second case? *)
Record t (cycle_eras : list Level_repr.cycle_era) : Prop := {
can_create :
match Level_repr.create_cycle_eras cycle_eras with
| Pervasives.Ok cycle_eras' ⇒ cycle_eras' = cycle_eras
| Pervasives.Error _ ⇒ False
end;
each_cycle_era_valid : List.Forall Cycle_era.Valid.t cycle_eras;
}.
End Valid.
[get_first_levels (cycle_eras)] outputs the lists of the [first_level]s
of the [era]s in [cycle_eras] @TODO to be used with a predicate [is_sorted]
Fixpoint get_first_levels (cycle_eras : list Level_repr.cycle_era)
: list Raw_level_repr.t :=
match cycle_eras with
| [] ⇒ []
| era :: cycle_eras0 ⇒ era.(Level_repr.cycle_era.first_level)
:: get_first_levels cycle_eras0
end.
: list Raw_level_repr.t :=
match cycle_eras with
| [] ⇒ []
| era :: cycle_eras0 ⇒ era.(Level_repr.cycle_era.first_level)
:: get_first_levels cycle_eras0
end.
[get_first_levels (cycle_ers)] outputs the lists of the [first_cycle]s
of the [era]s in [cycle_eras] @TODO to be used with a predicate [is_sorted]
Fixpoint get_first_cycles (cycle_eras : list Level_repr.cycle_era)
: list Cycle_repr.t :=
match cycle_eras with
| [] ⇒ []
| era :: cycle_eras0 ⇒ era.(Level_repr.cycle_era.first_cycle)
:: get_first_cycles cycle_eras0
end.
: list Cycle_repr.t :=
match cycle_eras with
| [] ⇒ []
| era :: cycle_eras0 ⇒ era.(Level_repr.cycle_era.first_cycle)
:: get_first_cycles cycle_eras0
end.
[ce_aux] is the internal fixpoint of create_cycle_eras] in @Proto_alpha
Fixpoint ce_aux (era0 : Level_repr.cycle_era)
(cycle_eras0 : list Level_repr.cycle_era) : M? unit :=
let '{| Level_repr.cycle_era.first_level := first_level;
Level_repr.cycle_era.first_cycle := first_cycle |} := era0 in
match cycle_eras0 with
| ({| Level_repr.cycle_era.first_level := first_level_of_previous_era;
Level_repr.cycle_era.first_cycle := first_cycle_of_previous_era
|} as previous_era) :: even_older_eras ⇒
if (Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
(Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
then ce_aux previous_era even_older_eras
else
Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
| [] ⇒ return? tt
end.
Lemma unfold_ce_aux (era0 : Level_repr.cycle_era)
(cycle_eras0 : list Level_repr.cycle_era) :
ce_aux era0 cycle_eras0 =
let '{| Level_repr.cycle_era.first_level := first_level;
Level_repr.cycle_era.first_cycle := first_cycle |} := era0 in
match cycle_eras0 with
| ({| Level_repr.cycle_era.first_level := first_level_of_previous_era;
Level_repr.cycle_era.first_cycle := first_cycle_of_previous_era
|} as previous_era) :: even_older_eras ⇒
if (Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
(Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
then ce_aux previous_era even_older_eras
else
Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
| [] ⇒ return? tt
end.
Proof. intros.
destruct cycle_eras0.
{ reflexivity. }
{ unfold ce_aux. destruct (_ && _); reflexivity. }
Qed.
(cycle_eras0 : list Level_repr.cycle_era) : M? unit :=
let '{| Level_repr.cycle_era.first_level := first_level;
Level_repr.cycle_era.first_cycle := first_cycle |} := era0 in
match cycle_eras0 with
| ({| Level_repr.cycle_era.first_level := first_level_of_previous_era;
Level_repr.cycle_era.first_cycle := first_cycle_of_previous_era
|} as previous_era) :: even_older_eras ⇒
if (Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
(Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
then ce_aux previous_era even_older_eras
else
Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
| [] ⇒ return? tt
end.
Lemma unfold_ce_aux (era0 : Level_repr.cycle_era)
(cycle_eras0 : list Level_repr.cycle_era) :
ce_aux era0 cycle_eras0 =
let '{| Level_repr.cycle_era.first_level := first_level;
Level_repr.cycle_era.first_cycle := first_cycle |} := era0 in
match cycle_eras0 with
| ({| Level_repr.cycle_era.first_level := first_level_of_previous_era;
Level_repr.cycle_era.first_cycle := first_cycle_of_previous_era
|} as previous_era) :: even_older_eras ⇒
if (Raw_level_repr.op_gt first_level first_level_of_previous_era) &&
(Cycle_repr.op_gt first_cycle first_cycle_of_previous_era)
then ce_aux previous_era even_older_eras
else
Error_monad.error_value (Build_extensible "Invalid_cycle_eras" unit tt)
| [] ⇒ return? tt
end.
Proof. intros.
destruct cycle_eras0.
{ reflexivity. }
{ unfold ce_aux. destruct (_ && _); reflexivity. }
Qed.
Helps unfold [create_cycle_era] *without* using an anonymous fixpoint
Lemma unfold_create_cycle_era (era0 : Level_repr.cycle_era)
(cycle_eras0 : list Level_repr.cycle_era) :
Level_repr.create_cycle_eras (era0 :: cycle_eras0) =
let? '_ := ce_aux era0 cycle_eras0 in
return? (era0 :: cycle_eras0).
Proof.
intros.
reflexivity.
Qed.
(cycle_eras0 : list Level_repr.cycle_era) :
Level_repr.create_cycle_eras (era0 :: cycle_eras0) =
let? '_ := ce_aux era0 cycle_eras0 in
return? (era0 :: cycle_eras0).
Proof.
intros.
reflexivity.
Qed.
When [ce_aux era cycle_eras] is valid, then so is
[create_cycle_eras (era :: cycle_eras)] and it [return?]s
[(era :: cycle_eras)]
Lemma ce_aux_valid_implies_create_valid
(era : Level_repr.cycle_era) (cycle_eras : list Level_repr.cycle_era) :
letP?relaxed _ := ce_aux era cycle_eras
in Level_repr.create_cycle_eras (era :: cycle_eras)
= return? (era :: cycle_eras).
Proof.
intros. destruct (ce_aux era cycle_eras) eqn:res0 ; hnf ;
[rewrite unfold_create_cycle_era ; rewrite res0; reflexivity |
constructor].
Qed.
(era : Level_repr.cycle_era) (cycle_eras : list Level_repr.cycle_era) :
letP?relaxed _ := ce_aux era cycle_eras
in Level_repr.create_cycle_eras (era :: cycle_eras)
= return? (era :: cycle_eras).
Proof.
intros. destruct (ce_aux era cycle_eras) eqn:res0 ; hnf ;
[rewrite unfold_create_cycle_era ; rewrite res0; reflexivity |
constructor].
Qed.
When [Level_repr.create_cycle_eras] is valid, so is
[ce_aux] and it [return?]s [tt]
Lemma create_valid_implies_ce_aux_valid (era : Level_repr.cycle_era)
(cycle_eras : list Level_repr.cycle_era) :
letP?relaxed _ := Level_repr.create_cycle_eras (era :: cycle_eras)
in ce_aux era cycle_eras = return? tt.
Proof.
intros.
destruct (ce_aux era cycle_eras) eqn:res0 ; hnf;
rewrite unfold_create_cycle_era; rewrite res0 ; hnf;
[apply f_equal ; destruct u ; reflexivity| constructor ].
Qed.
(* When [create_cycles_eras] is valid, it outputs its parameter *)
Lemma valid_create_cycle_era_outputs_input
(cycle_eras l : list Level_repr.cycle_era) :
Level_repr.create_cycle_eras (cycle_eras) = V0.Pervasives.Ok l
→ l = cycle_eras.
Proof.
intros.
destruct cycle_eras as [ | era0 ce0].
{ inversion H. }
{ specialize (create_valid_implies_ce_aux_valid era0 ce0) as H1.
rewrite H in H1. hnf in H1.
specialize (ce_aux_valid_implies_create_valid era0 ce0) as H2.
rewrite H1 in H2. hnf in H2. unfold "return?" in H2.
rewrite H in H2. inversion H2. reflexivity. }
Qed.
(cycle_eras : list Level_repr.cycle_era) :
letP?relaxed _ := Level_repr.create_cycle_eras (era :: cycle_eras)
in ce_aux era cycle_eras = return? tt.
Proof.
intros.
destruct (ce_aux era cycle_eras) eqn:res0 ; hnf;
rewrite unfold_create_cycle_era; rewrite res0 ; hnf;
[apply f_equal ; destruct u ; reflexivity| constructor ].
Qed.
(* When [create_cycles_eras] is valid, it outputs its parameter *)
Lemma valid_create_cycle_era_outputs_input
(cycle_eras l : list Level_repr.cycle_era) :
Level_repr.create_cycle_eras (cycle_eras) = V0.Pervasives.Ok l
→ l = cycle_eras.
Proof.
intros.
destruct cycle_eras as [ | era0 ce0].
{ inversion H. }
{ specialize (create_valid_implies_ce_aux_valid era0 ce0) as H1.
rewrite H in H1. hnf in H1.
specialize (ce_aux_valid_implies_create_valid era0 ce0) as H2.
rewrite H1 in H2. hnf in H2. unfold "return?" in H2.
rewrite H in H2. inversion H2. reflexivity. }
Qed.
When [cycle_eras] is valid then
[Level_repr.create_cycle_eras cycle_eras] [return?]s [cycle_eras]
Lemma valid_cycle_eras_implies_valid_cycle_create
(cycle_eras : list Level_repr.cycle_era): Valid.t cycle_eras
→ Level_repr.create_cycle_eras cycle_eras = V0.Pervasives.Ok cycle_eras.
Proof.
intros. destruct H.
destruct (Level_repr.create_cycle_eras cycle_eras) eqn:res.
{ apply valid_create_cycle_era_outputs_input in res. apply f_equal.
assumption. }
{ contradiction. }
Qed.
(cycle_eras : list Level_repr.cycle_era): Valid.t cycle_eras
→ Level_repr.create_cycle_eras cycle_eras = V0.Pervasives.Ok cycle_eras.
Proof.
intros. destruct H.
destruct (Level_repr.create_cycle_eras cycle_eras) eqn:res.
{ apply valid_create_cycle_era_outputs_input in res. apply f_equal.
assumption. }
{ contradiction. }
Qed.
When [cycle_eras] is valid then
[Level_repr.create_cycle_eras cycle_eras] [return?]s [cycle_eras]
Lemma valid_cycle_eras_implies_valid_ce_aux (era : Level_repr.cycle_era)
(ce : list Level_repr.cycle_era): Valid.t (era :: ce)
→ ce_aux era ce = V0.Pervasives.Ok tt.
Proof.
intros. destruct H.
destruct (Level_repr.create_cycle_eras (era :: ce)) eqn:res0.
{ specialize (create_valid_implies_ce_aux_valid era ce) as res1.
rewrite res0 in res1; hnf in res1. assumption. }
{ contradiction. }
Qed.
(* @TODO :
1. rename
2. spec *)
Lemma valid_inductive_step_aux1 : ∀ (era0 era1 : Level_repr.cycle_era)
(cycle_eras : list Level_repr.cycle_era),
letP?relaxed _ := Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)
in (Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level)
era1.(Level_repr.cycle_era.first_level) = true) ∧
Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle)
era1.(Level_repr.cycle_era.first_cycle) = true.
Proof.
intros.
destruct (Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras))
eqn:res ; simpl.
{ unfold Level_repr.create_cycle_eras in res.
destruct (_ && _) eqn:cond_val in res.
{ rewrite Bool.andb_true_iff in cond_val. tauto. }
{ inversion res. } }
{ constructor. }
Qed.
(* @TODO :
1. rename
2. spec *)
Lemma valid_inductive_step_aux2 : ∀ (era0 era1 : Level_repr.cycle_era)
(cycle_eras : list Level_repr.cycle_era),
letP?relaxed _ := Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)
in Level_repr.create_cycle_eras (era1 :: cycle_eras) =
V0.Pervasives.Ok (era1 :: cycle_eras) .
Proof.
intros.
destruct (Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)) eqn:res.
{ hnf. destruct (ce_aux era1 cycle_eras) eqn:ce_aux0.
{ rewrite unfold_create_cycle_era. hnf. rewrite ce_aux0. simpl.
unfold "return?". reflexivity. }
{ rewrite unfold_create_cycle_era. rewrite ce_aux0. simpl.
specialize (create_valid_implies_ce_aux_valid era0 (era1 :: cycle_eras))
as H2 ; rewrite res in H2 ; hnf in H2.
assert (H3: ce_aux era1 cycle_eras = V0.Pervasives.Ok tt).
{ inversion H2. destruct ( _ && _ ) eqn:bool_cond in H0.
{ assumption. } { inversion H0. } }
rewrite H3 in ce_aux0. inversion ce_aux0. } }
{ constructor. }
Qed.
Lemma valid_inductive_step : ∀ (cycle_eras : list Level_repr.cycle_era),
match cycle_eras with
| era0 :: era1 :: cycle_eras1 ⇒
Valid.t cycle_eras ↔
(Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level)
era1.(Level_repr.cycle_era.first_level) = true ∧
Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle)
era1.(Level_repr.cycle_era.first_cycle) = true ∧
Cycle_era.Valid.t era0
∧ Valid.t (era1 :: cycle_eras1) )
| [era] ⇒ Cycle_era.Valid.t era ↔ Valid.t [era]
| [] ⇒ Valid.t cycle_eras ↔ False
end.
Proof.
(* destruct cycle_eras as [ | era0 ce0 ]. *)
destruct cycle_eras as [ | era0 [ | era1 ce1 ]].
{ split ; intro H. { inversion H; compute in *; assumption. } { exfalso ;
assumption. }}
{ split ; intro H.
{ constructor ; constructor. {apply H. } {constructor. } }
{ destruct H eqn:H0. inversion each_cycle_era_valid. assumption. } }
{ split ; intro H.
{ specialize (valid_inductive_step_aux1 era0 era1 ce1) as bool_cond.
specialize (valid_inductive_step_aux2 era0 era1 ce1) as val_cond.
destruct H.
destruct (Level_repr.create_cycle_eras (era0 :: era1 :: ce1))
eqn:res_create. destruct bool_cond as [level_cond cycle_cond].
{ assert (era0_valid : Cycle_era.Valid.t era0).
{ inversion each_cycle_era_valid. assumption. }
destruct era0_valid as
[era0_f_level era0_f_cycle era0_b_p_cycles era0_b_p_commit].
destruct era0_f_level as [era0_fl1 era0_fl2].
destruct era0_f_cycle as [era0_fc1 era0_fc2].
destruct era0_b_p_cycles as [era0_bpcy1 era0_bpcy2].
destruct era0_b_p_commit as [era0_bpco1 era0_bpco2].
repeat split; try assumption.
{ hnf in val_cond. rewrite val_cond. constructor. }
{ inversion each_cycle_era_valid. assumption. }
}
{ contradiction. } }
{ destruct H as [H1 [H2 [H3 H4]]].
constructor.
{ rewrite unfold_create_cycle_era.
apply valid_cycle_eras_implies_valid_ce_aux in H4.
assert (H5: ce_aux era0 (era1 :: ce1) = V0.Pervasives.Ok tt).
{ rewrite unfold_ce_aux. cbn. destruct ( _ && _ ) eqn:H6.
{ assumption. }
{ exfalso. assert (H7: era0.(Level_repr.cycle_era.first_level) >?
era1.(Level_repr.cycle_era.first_level)= true). { assumption. }
assert (H8: era0.(Level_repr.cycle_era.first_cycle) >?
era1.(Level_repr.cycle_era.first_cycle) = true). { assumption. }
destruct era0. destruct era1. simpl in ×.
rewrite H7 in H6. rewrite H8 in H6. inversion H6.
} } (*** @TODO assert H5 should probably be a lemma *)
rewrite H5; constructor. }
{ constructor; [ assumption |destruct H4 ; assumption ].
}
}
}
Qed.
(ce : list Level_repr.cycle_era): Valid.t (era :: ce)
→ ce_aux era ce = V0.Pervasives.Ok tt.
Proof.
intros. destruct H.
destruct (Level_repr.create_cycle_eras (era :: ce)) eqn:res0.
{ specialize (create_valid_implies_ce_aux_valid era ce) as res1.
rewrite res0 in res1; hnf in res1. assumption. }
{ contradiction. }
Qed.
(* @TODO :
1. rename
2. spec *)
Lemma valid_inductive_step_aux1 : ∀ (era0 era1 : Level_repr.cycle_era)
(cycle_eras : list Level_repr.cycle_era),
letP?relaxed _ := Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)
in (Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level)
era1.(Level_repr.cycle_era.first_level) = true) ∧
Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle)
era1.(Level_repr.cycle_era.first_cycle) = true.
Proof.
intros.
destruct (Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras))
eqn:res ; simpl.
{ unfold Level_repr.create_cycle_eras in res.
destruct (_ && _) eqn:cond_val in res.
{ rewrite Bool.andb_true_iff in cond_val. tauto. }
{ inversion res. } }
{ constructor. }
Qed.
(* @TODO :
1. rename
2. spec *)
Lemma valid_inductive_step_aux2 : ∀ (era0 era1 : Level_repr.cycle_era)
(cycle_eras : list Level_repr.cycle_era),
letP?relaxed _ := Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)
in Level_repr.create_cycle_eras (era1 :: cycle_eras) =
V0.Pervasives.Ok (era1 :: cycle_eras) .
Proof.
intros.
destruct (Level_repr.create_cycle_eras (era0 :: era1 :: cycle_eras)) eqn:res.
{ hnf. destruct (ce_aux era1 cycle_eras) eqn:ce_aux0.
{ rewrite unfold_create_cycle_era. hnf. rewrite ce_aux0. simpl.
unfold "return?". reflexivity. }
{ rewrite unfold_create_cycle_era. rewrite ce_aux0. simpl.
specialize (create_valid_implies_ce_aux_valid era0 (era1 :: cycle_eras))
as H2 ; rewrite res in H2 ; hnf in H2.
assert (H3: ce_aux era1 cycle_eras = V0.Pervasives.Ok tt).
{ inversion H2. destruct ( _ && _ ) eqn:bool_cond in H0.
{ assumption. } { inversion H0. } }
rewrite H3 in ce_aux0. inversion ce_aux0. } }
{ constructor. }
Qed.
Lemma valid_inductive_step : ∀ (cycle_eras : list Level_repr.cycle_era),
match cycle_eras with
| era0 :: era1 :: cycle_eras1 ⇒
Valid.t cycle_eras ↔
(Raw_level_repr.op_gt era0.(Level_repr.cycle_era.first_level)
era1.(Level_repr.cycle_era.first_level) = true ∧
Cycle_repr.op_gt era0.(Level_repr.cycle_era.first_cycle)
era1.(Level_repr.cycle_era.first_cycle) = true ∧
Cycle_era.Valid.t era0
∧ Valid.t (era1 :: cycle_eras1) )
| [era] ⇒ Cycle_era.Valid.t era ↔ Valid.t [era]
| [] ⇒ Valid.t cycle_eras ↔ False
end.
Proof.
(* destruct cycle_eras as [ | era0 ce0 ]. *)
destruct cycle_eras as [ | era0 [ | era1 ce1 ]].
{ split ; intro H. { inversion H; compute in *; assumption. } { exfalso ;
assumption. }}
{ split ; intro H.
{ constructor ; constructor. {apply H. } {constructor. } }
{ destruct H eqn:H0. inversion each_cycle_era_valid. assumption. } }
{ split ; intro H.
{ specialize (valid_inductive_step_aux1 era0 era1 ce1) as bool_cond.
specialize (valid_inductive_step_aux2 era0 era1 ce1) as val_cond.
destruct H.
destruct (Level_repr.create_cycle_eras (era0 :: era1 :: ce1))
eqn:res_create. destruct bool_cond as [level_cond cycle_cond].
{ assert (era0_valid : Cycle_era.Valid.t era0).
{ inversion each_cycle_era_valid. assumption. }
destruct era0_valid as
[era0_f_level era0_f_cycle era0_b_p_cycles era0_b_p_commit].
destruct era0_f_level as [era0_fl1 era0_fl2].
destruct era0_f_cycle as [era0_fc1 era0_fc2].
destruct era0_b_p_cycles as [era0_bpcy1 era0_bpcy2].
destruct era0_b_p_commit as [era0_bpco1 era0_bpco2].
repeat split; try assumption.
{ hnf in val_cond. rewrite val_cond. constructor. }
{ inversion each_cycle_era_valid. assumption. }
}
{ contradiction. } }
{ destruct H as [H1 [H2 [H3 H4]]].
constructor.
{ rewrite unfold_create_cycle_era.
apply valid_cycle_eras_implies_valid_ce_aux in H4.
assert (H5: ce_aux era0 (era1 :: ce1) = V0.Pervasives.Ok tt).
{ rewrite unfold_ce_aux. cbn. destruct ( _ && _ ) eqn:H6.
{ assumption. }
{ exfalso. assert (H7: era0.(Level_repr.cycle_era.first_level) >?
era1.(Level_repr.cycle_era.first_level)= true). { assumption. }
assert (H8: era0.(Level_repr.cycle_era.first_cycle) >?
era1.(Level_repr.cycle_era.first_cycle) = true). { assumption. }
destruct era0. destruct era1. simpl in ×.
rewrite H7 in H6. rewrite H8 in H6. inversion H6.
} } (*** @TODO assert H5 should probably be a lemma *)
rewrite H5; constructor. }
{ constructor; [ assumption |destruct H4 ; assumption ].
}
}
}
Qed.
a valid [cycle_eras] is non-empty.
Lemma valid_cycle_eras_non_empty : ∀ (cycle_eras : list
Level_repr.cycle_era), Valid.t cycle_eras → cycle_eras ≠ [].
Proof.
unfold "~". intros. rewrite H0 in H. assert
(H1 := (valid_inductive_step [])) ; simpl in H1.
apply H1. apply H.
Qed.
Level_repr.cycle_era), Valid.t cycle_eras → cycle_eras ≠ [].
Proof.
unfold "~". intros. rewrite H0 in H. assert
(H1 := (valid_inductive_step [])) ; simpl in H1.
apply H1. apply H.
Qed.
if [cycle_eras] is valid, then the [first_level] and [first_cycle] of
its first [era] are greater than those of its last one, meaning
than the last [era] is more ancient than the first one.
Lemma valid_implies_first_gt_last : ∀ (cycle_eras : list
Level_repr.cycle_era), let rev_c_e := rev cycle_eras in
Valid.t cycle_eras → match cycle_eras with
| era0 :: _ ⇒ match rev_c_e with
| last_era :: _ ⇒
Raw_level_repr.op_gteq
era0.(Level_repr.cycle_era.first_level)
last_era.(Level_repr.cycle_era.first_level) = true ∧
Cycle_repr.op_gteq
era0.(Level_repr.cycle_era.first_cycle)
last_era.(Level_repr.cycle_era.first_cycle) = true
| [] ⇒ False
end
| [] ⇒ False
end.
Proof.
induction cycle_eras as [ | era0 ce0 H].
{ simpl. intro H. apply valid_cycle_eras_non_empty in H. apply H.
reflexivity. }
{ simpl in H. destruct ce0 as [ | era1 ce1].
{ simpl. intro. split ; lia. }
{ specialize (valid_inductive_step (era0 :: era1 ::ce1)) as ind_step ;
hnf in ind_step.
simpl. intro val_cond. apply ind_step in
val_cond. clear ind_step.
unfold rev, rev' in *; simpl in ×.
destruct val_cond as [H1 [H2 [H3 H4]]].
apply H in H4. clear H.
simpl.
destruct (Lists.List.rev_append ce1 [era1]) eqn:rev_ce0.
{ contradiction. }
{ destruct (Lists.List.rev_append ce1 [era1; era0]) eqn:rev_ce.
specialize (List.rev_append_not_empty2 ce1 [era1; era0]) as contrad.
apply contrad. { intro. inversion H. } { assumption. }
assert (H5 : c0 = c).
{ specialize (@List.same_last_element_rev_append Level_repr.cycle_era
era1 [ ] [era0] ce1)
as H6.
rewrite rev_ce0 in H6. rewrite rev_ce in H6.
inversion H6. reflexivity.
}
subst. lia.
}
}
}
Qed.
Level_repr.cycle_era), let rev_c_e := rev cycle_eras in
Valid.t cycle_eras → match cycle_eras with
| era0 :: _ ⇒ match rev_c_e with
| last_era :: _ ⇒
Raw_level_repr.op_gteq
era0.(Level_repr.cycle_era.first_level)
last_era.(Level_repr.cycle_era.first_level) = true ∧
Cycle_repr.op_gteq
era0.(Level_repr.cycle_era.first_cycle)
last_era.(Level_repr.cycle_era.first_cycle) = true
| [] ⇒ False
end
| [] ⇒ False
end.
Proof.
induction cycle_eras as [ | era0 ce0 H].
{ simpl. intro H. apply valid_cycle_eras_non_empty in H. apply H.
reflexivity. }
{ simpl in H. destruct ce0 as [ | era1 ce1].
{ simpl. intro. split ; lia. }
{ specialize (valid_inductive_step (era0 :: era1 ::ce1)) as ind_step ;
hnf in ind_step.
simpl. intro val_cond. apply ind_step in
val_cond. clear ind_step.
unfold rev, rev' in *; simpl in ×.
destruct val_cond as [H1 [H2 [H3 H4]]].
apply H in H4. clear H.
simpl.
destruct (Lists.List.rev_append ce1 [era1]) eqn:rev_ce0.
{ contradiction. }
{ destruct (Lists.List.rev_append ce1 [era1; era0]) eqn:rev_ce.
specialize (List.rev_append_not_empty2 ce1 [era1; era0]) as contrad.
apply contrad. { intro. inversion H. } { assumption. }
assert (H5 : c0 = c).
{ specialize (@List.same_last_element_rev_append Level_repr.cycle_era
era1 [ ] [era0] ce1)
as H6.
rewrite rev_ce0 in H6. rewrite rev_ce in H6.
inversion H6. reflexivity.
}
subst. lia.
}
}
}
Qed.
@TODO : prove the full decreasing pre-condition of valid [cycle_eras]
(* Lemma valid_implies_sorted_levels_and_cyles : forall (cycle_eras
: list Level_repr.cycle_era),
Valid.t cycle_eras <-> list Level_repr.cycle_era
(Sorted.Sorted (fun l1 l2 =>
(Raw_level_repr.op_gt
l1 l2 = true))). *)
End Cycle_eras.
: list Level_repr.cycle_era),
Valid.t cycle_eras <-> list Level_repr.cycle_era
(Sorted.Sorted (fun l1 l2 =>
(Raw_level_repr.op_gt
l1 l2 = true))). *)
End Cycle_eras.
[level] is greater than the [cycle_era.first_level]
Module Level_in_era.
Definition t (level : Level_repr.t) (era : Level_repr.cycle_era)
: Prop :=
let raw_level := level.(Level_repr.t.level) in
raw_level ≥ era.(Level_repr.cycle_era.first_level).
End Level_in_era.
Definition t (level : Level_repr.t) (era : Level_repr.cycle_era)
: Prop :=
let raw_level := level.(Level_repr.t.level) in
raw_level ≥ era.(Level_repr.cycle_era.first_level).
End Level_in_era.
[cycle] is greater than [cycle_era.first_cycle]
Module Cycle_in_era.
Definition t
(cycle : Cycle_repr.t)
(era : Level_repr.cycle_era)
: Prop :=
cycle ≥ era.(Level_repr.cycle_era.first_cycle).
End Cycle_in_era.
Lemma cycle_eras_encoding_is_valid :
Data_encoding.Valid.t Cycle_eras.Valid.t Level_repr.cycle_eras_encoding.
Data_encoding.Valid.data_encoding_auto.
Proof.
apply cycle_era_encoding_is_valid.
intros x H; split.
- apply H.
- destruct H.
destruct (Level_repr.create_cycle_eras _); [
congruence | tauto ].
Qed.
Definition t
(cycle : Cycle_repr.t)
(era : Level_repr.cycle_era)
: Prop :=
cycle ≥ era.(Level_repr.cycle_era.first_cycle).
End Cycle_in_era.
Lemma cycle_eras_encoding_is_valid :
Data_encoding.Valid.t Cycle_eras.Valid.t Level_repr.cycle_eras_encoding.
Data_encoding.Valid.data_encoding_auto.
Proof.
apply cycle_era_encoding_is_valid.
intros x H; split.
- apply H.
- destruct H.
destruct (Level_repr.create_cycle_eras _); [
congruence | tauto ].
Qed.
The function [first_level_in_cycle_from_eras] is valid.
Lemma first_level_in_cycle_from_eras_is_valid cycle_eras cycle :
Cycle_eras.Valid.t cycle_eras →
Cycle_repr.Valid.t cycle →
letP? level := Level_repr.first_level_in_cycle_from_eras cycle_eras cycle in
Valid.t level.
Proof.
(* intros.
destruct (Level_repr.first_level_in_cycle_from_eras cycle_eras cycle) eqn:res.
{ unfold Level_repr.first_level_in_cycle_from_eras in res. admit. }
{ admit. } *)
Admitted.
Cycle_eras.Valid.t cycle_eras →
Cycle_repr.Valid.t cycle →
letP? level := Level_repr.first_level_in_cycle_from_eras cycle_eras cycle in
Valid.t level.
Proof.
(* intros.
destruct (Level_repr.first_level_in_cycle_from_eras cycle_eras cycle) eqn:res.
{ unfold Level_repr.first_level_in_cycle_from_eras in res. admit. }
{ admit. } *)
Admitted.
The function [create_cycle_eras] is valid
Lemma create_cycle_eras_is_valid cs :
cs ≠ [] →
letP? cs' := Level_repr.create_cycle_eras cs in
cs' = cs.
Proof.
intros.
induction cs; cbn.
{ contradiction. }
{ destruct cs; cbn; [easy|].
step; cbn; [|reflexivity].
match goal with
| |- context [
let? ' _ := ?f' _ _ in _] ⇒
set (aux := f')
end.
intros.
destruct (aux c cs) eqn:?; cbn; [easy|].
assert (H_aux_is_valid : ∀ e c cs, aux c cs =
Pervasives.Error e →
Error.not_internal e).
{ clear.
intros ? ? ?.
subst aux.
generalize c.
induction cs; [discriminate|].
intros ?.
step; cbn.
{ apply IHcs. }
{ inj. subst e. reflexivity. }
}
now apply H_aux_is_valid in Heqt.
}
Qed.
cs ≠ [] →
letP? cs' := Level_repr.create_cycle_eras cs in
cs' = cs.
Proof.
intros.
induction cs; cbn.
{ contradiction. }
{ destruct cs; cbn; [easy|].
step; cbn; [|reflexivity].
match goal with
| |- context [
let? ' _ := ?f' _ _ in _] ⇒
set (aux := f')
end.
intros.
destruct (aux c cs) eqn:?; cbn; [easy|].
assert (H_aux_is_valid : ∀ e c cs, aux c cs =
Pervasives.Error e →
Error.not_internal e).
{ clear.
intros ? ? ?.
subst aux.
generalize c.
induction cs; [discriminate|].
intros ?.
step; cbn.
{ apply IHcs. }
{ inj. subst e. reflexivity. }
}
now apply H_aux_is_valid in Heqt.
}
Qed.
Predicate stating that [level] belongs to [cycle_eras]
Module level_belongs_to_cycle_eras.
Module Valid.
Fixpoint t (cycle_eras : list Level_repr.cycle_era)
(raw_level : Z.t) : Prop :=
match cycle_eras with
| [] ⇒ False
| cycle_era :: cycle_eras ⇒
raw_level ≥ cycle_era.(Level_repr.cycle_era.first_level) ∨
t cycle_eras raw_level
end.
End Valid.
End level_belongs_to_cycle_eras.
Module Valid.
Fixpoint t (cycle_eras : list Level_repr.cycle_era)
(raw_level : Z.t) : Prop :=
match cycle_eras with
| [] ⇒ False
| cycle_era :: cycle_eras ⇒
raw_level ≥ cycle_era.(Level_repr.cycle_era.first_level) ∨
t cycle_eras raw_level
end.
End Valid.
End level_belongs_to_cycle_eras.
The function [era_of_level] is valid
Lemma era_of_level_is_valid cycle_eras raw_level :
List.Forall Level_repr.Cycle_era.Valid.t cycle_eras →
level_belongs_to_cycle_eras.Valid.t cycle_eras raw_level →
Raw_level_repr.Valid.t raw_level →
letP? era := Level_repr.era_of_level cycle_eras raw_level in
Level_repr.Cycle_era.Valid.t era ∧
era.(Level_repr.cycle_era.first_level) ≤ raw_level.
Proof.
intros H_cycle_eras' H_cycle_eras H_level.
red in H_cycle_eras.
induction cycle_eras.
{ contradiction. }
{ destruct H_cycle_eras.
{ cbn.
replace (_ >=? _) with true
by (destruct a; cbn in *; lia).
cbn. split_conj.
{ now inversion H_cycle_eras'. }
{ lia. }
}
{ cbn.
step.
{ cbn. split.
{ now inversion H_cycle_eras'. }
{ destruct a; cbn in ×.
{ lia. }
}
}
{ apply IHcycle_eras.
{ now inversion H_cycle_eras'. }
{ easy. }
}
}
}
Qed.
List.Forall Level_repr.Cycle_era.Valid.t cycle_eras →
level_belongs_to_cycle_eras.Valid.t cycle_eras raw_level →
Raw_level_repr.Valid.t raw_level →
letP? era := Level_repr.era_of_level cycle_eras raw_level in
Level_repr.Cycle_era.Valid.t era ∧
era.(Level_repr.cycle_era.first_level) ≤ raw_level.
Proof.
intros H_cycle_eras' H_cycle_eras H_level.
red in H_cycle_eras.
induction cycle_eras.
{ contradiction. }
{ destruct H_cycle_eras.
{ cbn.
replace (_ >=? _) with true
by (destruct a; cbn in *; lia).
cbn. split_conj.
{ now inversion H_cycle_eras'. }
{ lia. }
}
{ cbn.
step.
{ cbn. split.
{ now inversion H_cycle_eras'. }
{ destruct a; cbn in ×.
{ lia. }
}
}
{ apply IHcycle_eras.
{ now inversion H_cycle_eras'. }
{ easy. }
}
}
}
Qed.
The function [level_from_raw_with_era] is valid
Lemma level_from_raw_with_era_is_valid cycle_era
first_level_in_alpha_family level output_level :
Level_repr.level_from_raw_with_era_invariants.t cycle_era
first_level_in_alpha_family level output_level →
Level_repr.Cycle_era.Valid.t cycle_era →
Raw_level_repr.Valid.t first_level_in_alpha_family →
Raw_level_repr.Valid.t level →
cycle_era.(Level_repr.cycle_era.first_level) ≤ level →
letP? ' y := Level_repr.level_from_raw_with_era
cycle_era first_level_in_alpha_family level in
Level_repr.Valid.t y.
Proof.
intros.
unfold Level_repr.level_from_raw_with_era.
rewrite Raw_level_repr.diff_value_is_non_negative;
[|try easy || apply H..].
eapply Error.split_letP with (P := Cycle_repr.Valid.t); [|intros]. {
unfold Int32.to_int.
unfold Raw_level_repr.diff_value, "/i32", "-i32".
destruct H.
unfold Cycle_repr.add; cbn.
repeat rewrite Int32.normalize_identity;
Tactics.destruct_conjs.
{ red in H10. unfold "-Z", "/Z" in H10.
match goal with
| |- context [if ?e then _ else _] ⇒
set (cond := e)
end.
assert (H_cond_pos : cond = true) by
(subst cond; destruct cycle_era; cbn in *; lia).
rewrite H_cond_pos.
cbn.
unfold "+i32".
rewrite Int32.normalize_identity.
{ lia. }
{ clear - H11.
unfold "-Z", "/Z", "+Z" in H11.
revert H11.
apply Int32.non_negative_impl_t.
}
}
{ unfold "-Z", "/Z", "+Z" in ×.
revert H10.
apply Int32.non_negative_impl_t.
}
{ easy. }
{ unfold "-Z", "/Z" in H10.
clear - H10. revert H10.
apply Int32.non_negative_impl_t.
}
{ easy. }
}
{ destruct H. cbn.
split; cbn; try easy; unfold Raw_level_repr.diff_value; lia.
}
{ destruct H0. easy. }
Qed.
first_level_in_alpha_family level output_level :
Level_repr.level_from_raw_with_era_invariants.t cycle_era
first_level_in_alpha_family level output_level →
Level_repr.Cycle_era.Valid.t cycle_era →
Raw_level_repr.Valid.t first_level_in_alpha_family →
Raw_level_repr.Valid.t level →
cycle_era.(Level_repr.cycle_era.first_level) ≤ level →
letP? ' y := Level_repr.level_from_raw_with_era
cycle_era first_level_in_alpha_family level in
Level_repr.Valid.t y.
Proof.
intros.
unfold Level_repr.level_from_raw_with_era.
rewrite Raw_level_repr.diff_value_is_non_negative;
[|try easy || apply H..].
eapply Error.split_letP with (P := Cycle_repr.Valid.t); [|intros]. {
unfold Int32.to_int.
unfold Raw_level_repr.diff_value, "/i32", "-i32".
destruct H.
unfold Cycle_repr.add; cbn.
repeat rewrite Int32.normalize_identity;
Tactics.destruct_conjs.
{ red in H10. unfold "-Z", "/Z" in H10.
match goal with
| |- context [if ?e then _ else _] ⇒
set (cond := e)
end.
assert (H_cond_pos : cond = true) by
(subst cond; destruct cycle_era; cbn in *; lia).
rewrite H_cond_pos.
cbn.
unfold "+i32".
rewrite Int32.normalize_identity.
{ lia. }
{ clear - H11.
unfold "-Z", "/Z", "+Z" in H11.
revert H11.
apply Int32.non_negative_impl_t.
}
}
{ unfold "-Z", "/Z", "+Z" in ×.
revert H10.
apply Int32.non_negative_impl_t.
}
{ easy. }
{ unfold "-Z", "/Z" in H10.
clear - H10. revert H10.
apply Int32.non_negative_impl_t.
}
{ easy. }
}
{ destruct H. cbn.
split; cbn; try easy; unfold Raw_level_repr.diff_value; lia.
}
{ destruct H0. easy. }
Qed.
The function [level_from_raw] is valid
Lemma level_from_raw_is_valid cycle_eras raw_level
(output_level : Level_repr.t) :
List.Forall Level_repr.Cycle_era.Valid.t cycle_eras →
level_belongs_to_cycle_eras.Valid.t cycle_eras raw_level →
Raw_level_repr.Valid.t raw_level →
letP? level := Level_repr.level_from_raw cycle_eras raw_level in
Level_repr.Valid.t level.
Proof.
intros H_Forall H_cycle_eras H_raw_level **.
unfold Level_repr.level_from_raw,
Level_repr.level_from_raw_aux_exn.
induction cycle_eras as [|cycle_era cycle_eras IHcycle_eras]
using rev_ind; [contradiction|].
rewrite List.rev_eq.
rewrite rev_unit.
cbn.
eapply Error.split_letP. {
now apply Level_repr.era_of_level_is_valid.
}
intros era_of_level [H H']. cbn in ×.
pose proof Level_repr.level_from_raw_with_era_is_valid era_of_level
cycle_era.(Level_repr.cycle_era.first_level) raw_level
output_level as H_from_raw.
destruct (Level_repr.level_from_raw_with_era _ _ _) eqn:?; cbn in ×.
{ apply H_from_raw; try easy.
{ (* @TODO
Level_repr.level_from_raw_with_era_invariants.t era_of_level
cycle_era.(Level_repr.cycle_era.first_level) raw_level
output_level
*)
admit.
}
{ apply List.Forall_app in H_Forall.
destruct H_Forall as [_ H_Forall].
inversion H_Forall as [].
destruct_by_type (Level_repr.Cycle_era.Valid.t _);
cbn in ×.
easy.
}
}
{ eapply Error.is_valid_impl_not_internal; [|solve [eauto]].
apply Level_repr.level_from_raw_with_era_is_valid
with (output_level := output_level); try easy.
{ (* @TODO Level_repr.level_from_raw_with_era_invariants.t
era_of_level cycle_era.(Level_repr.cycle_era.first_level)
raw_level output_level *)
admit.
}
{ apply List.Forall_app in H_Forall.
destruct H_Forall as [_ H_Forall].
inversion H_Forall as [].
destruct_by_type (Level_repr.Cycle_era.Valid.t _);
cbn in ×. easy.
}
}
Admitted.
(output_level : Level_repr.t) :
List.Forall Level_repr.Cycle_era.Valid.t cycle_eras →
level_belongs_to_cycle_eras.Valid.t cycle_eras raw_level →
Raw_level_repr.Valid.t raw_level →
letP? level := Level_repr.level_from_raw cycle_eras raw_level in
Level_repr.Valid.t level.
Proof.
intros H_Forall H_cycle_eras H_raw_level **.
unfold Level_repr.level_from_raw,
Level_repr.level_from_raw_aux_exn.
induction cycle_eras as [|cycle_era cycle_eras IHcycle_eras]
using rev_ind; [contradiction|].
rewrite List.rev_eq.
rewrite rev_unit.
cbn.
eapply Error.split_letP. {
now apply Level_repr.era_of_level_is_valid.
}
intros era_of_level [H H']. cbn in ×.
pose proof Level_repr.level_from_raw_with_era_is_valid era_of_level
cycle_era.(Level_repr.cycle_era.first_level) raw_level
output_level as H_from_raw.
destruct (Level_repr.level_from_raw_with_era _ _ _) eqn:?; cbn in ×.
{ apply H_from_raw; try easy.
{ (* @TODO
Level_repr.level_from_raw_with_era_invariants.t era_of_level
cycle_era.(Level_repr.cycle_era.first_level) raw_level
output_level
*)
admit.
}
{ apply List.Forall_app in H_Forall.
destruct H_Forall as [_ H_Forall].
inversion H_Forall as [].
destruct_by_type (Level_repr.Cycle_era.Valid.t _);
cbn in ×.
easy.
}
}
{ eapply Error.is_valid_impl_not_internal; [|solve [eauto]].
apply Level_repr.level_from_raw_with_era_is_valid
with (output_level := output_level); try easy.
{ (* @TODO Level_repr.level_from_raw_with_era_invariants.t
era_of_level cycle_era.(Level_repr.cycle_era.first_level)
raw_level output_level *)
admit.
}
{ apply List.Forall_app in H_Forall.
destruct H_Forall as [_ H_Forall].
inversion H_Forall as [].
destruct_by_type (Level_repr.Cycle_era.Valid.t _);
cbn in ×. easy.
}
}
Admitted.
The function [root_level] is valid
Lemma root_level_is_valid cycle_eras :
Level_repr.Cycle_eras.Valid.t cycle_eras →
letP? ' x := Level_repr.root_level cycle_eras in
Level_repr.Valid.t x.
Proof.
Admitted.
Level_repr.Cycle_eras.Valid.t cycle_eras →
letP? ' x := Level_repr.root_level cycle_eras in
Level_repr.Valid.t x.
Proof.
Admitted.
The function [last_of_cycle] is valid
Lemma last_of_cycle_is_valid cycle_eras level :
letP? ' _ := Level_repr.last_of_cycle cycle_eras level in True.
Proof.
Admitted.
letP? ' _ := Level_repr.last_of_cycle cycle_eras level in True.
Proof.
Admitted.
The [raw_level] passed to [level_from_raw] is
present in the returned level
Lemma level_from_raw_eq cycle_eras raw_level :
Cycle_eras.Valid.t cycle_eras →
Raw_level_repr.Valid.t raw_level →
letP? ' level :=
Level_repr.level_from_raw cycle_eras raw_level
in level.(Level_repr.t.level) = raw_level.
Proof.
Admitted.
Cycle_eras.Valid.t cycle_eras →
Raw_level_repr.Valid.t raw_level →
letP? ' level :=
Level_repr.level_from_raw cycle_eras raw_level
in level.(Level_repr.t.level) = raw_level.
Proof.
Admitted.