🪜 Level_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Level_storage.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Proofs.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Module Valid.
The [level] is in the context cycle_eras
Definition t (ctxt : Proto_alpha.Raw_context.t)
(raw_level : Raw_level_repr.t) :=
Raw_context.Valid.on
(fun sim_ctxt ⇒
Level_repr.level_belongs_to_cycle_eras.Valid.t
sim_ctxt.(Raw_context.config)
.(Raw_context_aux.config.cycle_eras)
raw_level)
ctxt.
(raw_level : Raw_level_repr.t) :=
Raw_context.Valid.on
(fun sim_ctxt ⇒
Level_repr.level_belongs_to_cycle_eras.Valid.t
sim_ctxt.(Raw_context.config)
.(Raw_context_aux.config.cycle_eras)
raw_level)
ctxt.
Given the context [cycle_eras], if [l] belongs to the [cycle_eras]
and [l <= l'], then [l'] belongs to the [cycle_era] too.
Lemma le_impl_t ctxt l l' :
l ≤ l' →
t ctxt l →
t ctxt l'.
Proof.
intros H_le H_ctxt. cbn in ×.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Raw_context.Valid.on.
∃ sim_ctxt. intros.
split_conj; [easy..|].
induction sim_ctxt.(Raw_context.config)
.(Raw_context_aux.config.cycle_eras)
as [|cycle_era cycle_eras IHcycle_eras].
{ contradiction. }
{ cbn in ×.
destruct H_sim_ctxt_domain.
{ left.
clear - H_le H.
destruct cycle_era; cbn in ×.
apply Z.le_ge.
apply Z.ge_le in H.
lia.
}
{ right.
now apply IHcycle_eras.
}
}
Qed.
End Valid.
l ≤ l' →
t ctxt l →
t ctxt l'.
Proof.
intros H_le H_ctxt. cbn in ×.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Raw_context.Valid.on.
∃ sim_ctxt. intros.
split_conj; [easy..|].
induction sim_ctxt.(Raw_context.config)
.(Raw_context_aux.config.cycle_eras)
as [|cycle_era cycle_eras IHcycle_eras].
{ contradiction. }
{ cbn in ×.
destruct H_sim_ctxt_domain.
{ left.
clear - H_le H.
destruct cycle_era; cbn in ×.
apply Z.le_ge.
apply Z.ge_le in H.
lia.
}
{ right.
now apply IHcycle_eras.
}
}
Qed.
End Valid.
The function [from_raw] is valid.
Lemma from_raw_is_valid ctxt level :
Valid.t ctxt level →
Raw_level_repr.Valid.t level →
letP? level := Level_storage.from_raw ctxt level in
Level_repr.Valid.t level.
Proof.
intros H_ctxt H_level.
unfold Level_storage.from_raw.
pose proof (Level_repr.level_from_raw_is_valid
(Raw_context.cycle_eras ctxt) level)
as H_from_raw.
destruct (Level_repr.level_from_raw _ _);
Raw_context.Valid.destruct_rewrite H_ctxt.
{ cbn in ×. apply H_from_raw.
{ hauto l: on. }
{ now destruct H_sim_ctxt, config, cycle_eras. }
{ easy. }
{ easy. }
}
{ cbn in ×. apply H_from_raw.
{ hauto l: on. }
{ now destruct H_sim_ctxt, config, cycle_eras. }
{ easy. }
{ easy. }
}
Qed.
Valid.t ctxt level →
Raw_level_repr.Valid.t level →
letP? level := Level_storage.from_raw ctxt level in
Level_repr.Valid.t level.
Proof.
intros H_ctxt H_level.
unfold Level_storage.from_raw.
pose proof (Level_repr.level_from_raw_is_valid
(Raw_context.cycle_eras ctxt) level)
as H_from_raw.
destruct (Level_repr.level_from_raw _ _);
Raw_context.Valid.destruct_rewrite H_ctxt.
{ cbn in ×. apply H_from_raw.
{ hauto l: on. }
{ now destruct H_sim_ctxt, config, cycle_eras. }
{ easy. }
{ easy. }
}
{ cbn in ×. apply H_from_raw.
{ hauto l: on. }
{ now destruct H_sim_ctxt, config, cycle_eras. }
{ easy. }
{ easy. }
}
Qed.
The raw level [from_raw] passed as argument to [from_raw] is
inside the returned level
Lemma from_raw_eq ctxt raw_level :
Valid.t ctxt raw_level →
Raw_level_repr.Valid.t raw_level →
letP? level := Level_storage.from_raw ctxt raw_level in
level.(Level_repr.t.level) = raw_level.
Proof.
intros H_ctxt H_raw_level.
unfold Level_storage.from_raw.
apply Level_repr.level_from_raw_eq; [|easy].
unfold Valid.t in ×.
Raw_context.Valid.destruct_rewrite H_ctxt.
now destruct H_sim_ctxt, config.
Qed.
Valid.t ctxt raw_level →
Raw_level_repr.Valid.t raw_level →
letP? level := Level_storage.from_raw ctxt raw_level in
level.(Level_repr.t.level) = raw_level.
Proof.
intros H_ctxt H_raw_level.
unfold Level_storage.from_raw.
apply Level_repr.level_from_raw_eq; [|easy].
unfold Valid.t in ×.
Raw_context.Valid.destruct_rewrite H_ctxt.
now destruct H_sim_ctxt, config.
Qed.
[from_raw_with_offset] returns a valid level
Lemma from_raw_with_offset_is_valid (ctxt : Proto_alpha.Raw_context.t)
(raw_level raw_level': Raw_level_repr.t)
(offset : Int32.t) (level : Level_repr.t) :
Level_repr.Valid.t level →
Level_repr.level_from_raw_aux (Raw_context.cycle_eras ctxt)
raw_level' = Pervasives.Ok level →
Raw_level_repr.of_int32
(Raw_level_repr.to_int32 raw_level +i32 offset) =
Pervasives.Ok raw_level' →
match Level_storage.from_raw_with_offset ctxt offset raw_level with
| Pervasives.Ok l ⇒ Level_repr.Valid.t l
| Pervasives.Error _ ⇒ True
end.
Proof.
intros.
unfold Level_storage.from_raw_with_offset.
unfold Level_repr.level_from_raw_with_offset.
remember (Raw_level_repr.of_int32 _) as i.
rewrite H1. unfold "let? ' _ := _ in _".
now rewrite H0.
Qed.
(raw_level raw_level': Raw_level_repr.t)
(offset : Int32.t) (level : Level_repr.t) :
Level_repr.Valid.t level →
Level_repr.level_from_raw_aux (Raw_context.cycle_eras ctxt)
raw_level' = Pervasives.Ok level →
Raw_level_repr.of_int32
(Raw_level_repr.to_int32 raw_level +i32 offset) =
Pervasives.Ok raw_level' →
match Level_storage.from_raw_with_offset ctxt offset raw_level with
| Pervasives.Ok l ⇒ Level_repr.Valid.t l
| Pervasives.Error _ ⇒ True
end.
Proof.
intros.
unfold Level_storage.from_raw_with_offset.
unfold Level_repr.level_from_raw_with_offset.
remember (Raw_level_repr.of_int32 _) as i.
rewrite H1. unfold "let? ' _ := _ in _".
now rewrite H0.
Qed.
[root_value] level is valid
Lemma root_value_is_valid : ∀ {ctxt} l,
Int32.Valid.t Cycle_repr.root_value →
Raw_level_repr.Valid.t l.(Level_repr.cycle_era.first_level) →
last_opt (Raw_context.cycle_eras ctxt) = Some l →
letP? lsrv := Level_storage.root_value ctxt in
Level_repr.Valid.t lsrv.
Proof.
intros.
unfold Level_storage.root_value.
unfold Level_repr.root_level.
unfold "letP? ' _ := _ in _".
unfold "let? ' _ := _ in _".
now rewrite H1.
Qed.
Int32.Valid.t Cycle_repr.root_value →
Raw_level_repr.Valid.t l.(Level_repr.cycle_era.first_level) →
last_opt (Raw_context.cycle_eras ctxt) = Some l →
letP? lsrv := Level_storage.root_value ctxt in
Level_repr.Valid.t lsrv.
Proof.
intros.
unfold Level_storage.root_value.
unfold Level_repr.root_level.
unfold "letP? ' _ := _ in _".
unfold "let? ' _ := _ in _".
now rewrite H1.
Qed.
The function [succ] is valid.
Lemma succ_is_valid ctxt level :
Valid.t ctxt level.(Level_repr.t.level) →
Level_repr.Valid.t level →
Raw_level_repr.Valid.t (level.(Level_repr.t.level) +Z 1) →
letP? level := Level_storage.succ ctxt level in
Level_repr.Valid.t level.
Proof.
intros H_ctxt H_level H_raw_level.
unfold Level_storage.succ.
apply Level_storage.from_raw_is_valid.
{ set (s := Raw_level_repr.succ _).
assert (H_lt : level.(Level_repr.t.level) < s).
{ subst s.
unfold Raw_level_repr.succ, Int32.succ. lia.
}
pose (level' := level.(Level_repr.t.level)).
pose proof Valid.le_impl_t ctxt level' s as H_ctxt'.
apply H_ctxt'.
{ lia. }
{ easy. }
}
{ apply Raw_level_repr.succ_is_valid.
apply H_level.
}
Qed.
Valid.t ctxt level.(Level_repr.t.level) →
Level_repr.Valid.t level →
Raw_level_repr.Valid.t (level.(Level_repr.t.level) +Z 1) →
letP? level := Level_storage.succ ctxt level in
Level_repr.Valid.t level.
Proof.
intros H_ctxt H_level H_raw_level.
unfold Level_storage.succ.
apply Level_storage.from_raw_is_valid.
{ set (s := Raw_level_repr.succ _).
assert (H_lt : level.(Level_repr.t.level) < s).
{ subst s.
unfold Raw_level_repr.succ, Int32.succ. lia.
}
pose (level' := level.(Level_repr.t.level)).
pose proof Valid.le_impl_t ctxt level' s as H_ctxt'.
apply H_ctxt'.
{ lia. }
{ easy. }
}
{ apply Raw_level_repr.succ_is_valid.
apply H_level.
}
Qed.
[succ] is equivalent to [Z.succ]
Lemma succ_eq (ctxt : Proto_alpha.Raw_context.t)
(level : Level_repr.t) :
Valid.t ctxt level.(Level_repr.t.level) →
Raw_level_repr.Valid.t (level.(Level_repr.t.level) +Z 1) →
Level_repr.Valid.t level →
letP? l' := Level_storage.succ ctxt level in
let raw_level1 := level.(Level_repr.t.level) in
let raw_level2 := l'.(Level_repr.t.level) in
raw_level2 = Z.succ raw_level1.
Proof.
intros H_ctxt H_int H_level.
unfold Level_storage.succ,
Raw_level_repr.succ,
Int32.succ,
"+i32" in ×.
rewrite Int32.normalize_identity; [|lia].
pose proof Level_storage.from_raw_eq ctxt
(level.(Level_repr.t.level) +Z 1)
as H_from_raw.
fold Z.add.
destruct (Level_storage.from_raw _ _) eqn:?;
apply H_from_raw; try easy;
apply (Valid.le_impl_t ctxt level.(Level_repr.t.level)
(level.(Level_repr.t.level) +Z 1) ltac:(lia) ltac:(assumption)).
Qed.
(level : Level_repr.t) :
Valid.t ctxt level.(Level_repr.t.level) →
Raw_level_repr.Valid.t (level.(Level_repr.t.level) +Z 1) →
Level_repr.Valid.t level →
letP? l' := Level_storage.succ ctxt level in
let raw_level1 := level.(Level_repr.t.level) in
let raw_level2 := l'.(Level_repr.t.level) in
raw_level2 = Z.succ raw_level1.
Proof.
intros H_ctxt H_int H_level.
unfold Level_storage.succ,
Raw_level_repr.succ,
Int32.succ,
"+i32" in ×.
rewrite Int32.normalize_identity; [|lia].
pose proof Level_storage.from_raw_eq ctxt
(level.(Level_repr.t.level) +Z 1)
as H_from_raw.
fold Z.add.
destruct (Level_storage.from_raw _ _) eqn:?;
apply H_from_raw; try easy;
apply (Valid.le_impl_t ctxt level.(Level_repr.t.level)
(level.(Level_repr.t.level) +Z 1) ltac:(lia) ltac:(assumption)).
Qed.
The function [pred] is valid.
Lemma pred_is_valid ctxt level :
Valid.t ctxt (level.(Level_repr.t.level) -Z 1) →
Level_repr.Valid.t level →
letP? level := Level_storage.pred ctxt level in
Option.Forall Level_repr.Valid.t level.
Proof.
intros ? H_level. unfold Level_storage.pred.
destruct H_level.
pose proof @Raw_level_repr.pred_is_valid level.(Level_repr.t.level)
ltac:(assumption) as H_pred.
destruct (Raw_level_repr.pred _) as [pred_level|]; [|easy].
Tactics.destruct_conjs.
subst pred_level.
eapply Error.split_letP with (P := Level_repr.Valid.t); [|intros]. {
now apply from_raw_is_valid.
}
easy.
Qed.
Valid.t ctxt (level.(Level_repr.t.level) -Z 1) →
Level_repr.Valid.t level →
letP? level := Level_storage.pred ctxt level in
Option.Forall Level_repr.Valid.t level.
Proof.
intros ? H_level. unfold Level_storage.pred.
destruct H_level.
pose proof @Raw_level_repr.pred_is_valid level.(Level_repr.t.level)
ltac:(assumption) as H_pred.
destruct (Raw_level_repr.pred _) as [pred_level|]; [|easy].
Tactics.destruct_conjs.
subst pred_level.
eapply Error.split_letP with (P := Level_repr.Valid.t); [|intros]. {
now apply from_raw_is_valid.
}
easy.
Qed.
[preq] is equivalent to [Z.pred] on positives
Lemma pred_eq
(ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t) :
Int32.Valid.t (level.(Level_repr.t.level) - 1) →
Valid.t ctxt (level.(Level_repr.t.level) - 1) →
Level_repr.Valid.t level →
letP? lsc := Level_storage.pred ctxt level in
match lsc with
| Some l ⇒
let raw_level1 := level.(Level_repr.t.level) in
let raw_level2 := l.(Level_repr.t.level) in
raw_level2 = Int32.pred raw_level1
| None ⇒ True
end.
Proof.
intros ? H_ctxt H_level.
unfold Level_storage.pred.
unfold Raw_level_repr.pred.
destruct (Raw_level_repr.op_eq _ _) eqn:?; [easy|].
assert (H_pos : Raw_level_repr.Valid.t
(level.(Level_repr.t.level) - 1)).
{ destruct level, H_level; cbn in ×.
lia.
}
unfold Int32.pred, "-i32".
rewrite Int32.normalize_identity by assumption.
pose proof Level_storage.from_raw_eq ctxt
(level.(Level_repr.t.level) - 1) H_ctxt H_pos
as H_from_raw.
now destruct (Level_storage.from_raw _ _).
Qed.
(ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t) :
Int32.Valid.t (level.(Level_repr.t.level) - 1) →
Valid.t ctxt (level.(Level_repr.t.level) - 1) →
Level_repr.Valid.t level →
letP? lsc := Level_storage.pred ctxt level in
match lsc with
| Some l ⇒
let raw_level1 := level.(Level_repr.t.level) in
let raw_level2 := l.(Level_repr.t.level) in
raw_level2 = Int32.pred raw_level1
| None ⇒ True
end.
Proof.
intros ? H_ctxt H_level.
unfold Level_storage.pred.
unfold Raw_level_repr.pred.
destruct (Raw_level_repr.op_eq _ _) eqn:?; [easy|].
assert (H_pos : Raw_level_repr.Valid.t
(level.(Level_repr.t.level) - 1)).
{ destruct level, H_level; cbn in ×.
lia.
}
unfold Int32.pred, "-i32".
rewrite Int32.normalize_identity by assumption.
pose proof Level_storage.from_raw_eq ctxt
(level.(Level_repr.t.level) - 1) H_ctxt H_pos
as H_from_raw.
now destruct (Level_storage.from_raw _ _).
Qed.
[current] level is valid
Lemma current_is_valid ctxt :
Raw_context.Valid.t ctxt →
Level_repr.Valid.t (Level_storage.current ctxt).
Proof.
intros H.
Raw_context.Valid.destruct_rewrite H.
dtauto.
Qed.
Raw_context.Valid.t ctxt →
Level_repr.Valid.t (Level_storage.current ctxt).
Proof.
intros H.
Raw_context.Valid.destruct_rewrite H.
dtauto.
Qed.
The function [add] is valid.
Lemma add_is_valid ctxt level n :
Valid.t ctxt level.(Level_repr.t.level) →
Level_repr.Valid.t level →
Pervasives.Int.Valid.positive n →
letP? level := Level_storage.add ctxt level n in
Level_repr.Valid.t level.
Proof.
intros H_ctxt H_level H_n.
unfold Level_storage.add.
destruct H_level.
pose proof Raw_level_repr.add_eq level.(Level_repr.t.level) n
as H_add.
repeat specialize (H_add ltac:(assumption || lia)).
pose proof Raw_level_repr.add_is_valid level.(Level_repr.t.level) n
as H_add'.
repeat specialize (H_add' ltac:(assumption || lia)).
step; cbn in *; [|easy]. subst i.
apply from_raw_is_valid; [|easy].
apply (Valid.le_impl_t ctxt level.(Level_repr.t.level)
(level.(Level_repr.t.level) +Z n)); [lia|easy].
Qed.
Valid.t ctxt level.(Level_repr.t.level) →
Level_repr.Valid.t level →
Pervasives.Int.Valid.positive n →
letP? level := Level_storage.add ctxt level n in
Level_repr.Valid.t level.
Proof.
intros H_ctxt H_level H_n.
unfold Level_storage.add.
destruct H_level.
pose proof Raw_level_repr.add_eq level.(Level_repr.t.level) n
as H_add.
repeat specialize (H_add ltac:(assumption || lia)).
pose proof Raw_level_repr.add_is_valid level.(Level_repr.t.level) n
as H_add'.
repeat specialize (H_add' ltac:(assumption || lia)).
step; cbn in *; [|easy]. subst i.
apply from_raw_is_valid; [|easy].
apply (Valid.le_impl_t ctxt level.(Level_repr.t.level)
(level.(Level_repr.t.level) +Z n)); [lia|easy].
Qed.
[add] is equivalent to [+Z]
Lemma add_eq (ctxt : Proto_alpha.Raw_context.t) (l : Level_repr.t)
(i : Int32.t) :
Valid.t ctxt l.(Level_repr.t.level) →
Int32.Valid.positive i →
Level_repr.Valid.t l →
Raw_level_repr.Valid.t (l.(Level_repr.t.level) +Z i) →
letP? l' := Level_storage.add ctxt l i in
let raw_level1 := l.(Level_repr.t.level) in
let raw_level2 := l'.(Level_repr.t.level) in
raw_level2 = raw_level1 +Z i.
Proof.
intros H_ctxt Hint Hlevel Hint_level.
unfold Level_storage.add.
eapply Error.split_letP. {
apply Raw_level_repr.add_eq.
{ apply Hlevel. }
{ lia. }
}
intros raw_level H_raw_level. cbn in ×.
subst raw_level.
pose proof (Level_storage.from_raw_eq ctxt
(l.(Level_repr.t.level) +Z i)) as H_from_raw.
pose proof (Level_storage.from_raw_is_valid ctxt
(l.(Level_repr.t.level) +Z i)) as H_from_raw'.
destruct (Level_storage.from_raw _ _).
{ apply H_from_raw; [|assumption].
apply (Valid.le_impl_t ctxt l.(Level_repr.t.level)
(l.(Level_repr.t.level) +Z i) ltac:(lia) ltac:(assumption)).
}
{ cbn in ×. apply H_from_raw'; try easy.
apply (Valid.le_impl_t ctxt l.(Level_repr.t.level)
(l.(Level_repr.t.level) +Z i) ltac:(lia) ltac:(assumption)).
}
Qed.
(i : Int32.t) :
Valid.t ctxt l.(Level_repr.t.level) →
Int32.Valid.positive i →
Level_repr.Valid.t l →
Raw_level_repr.Valid.t (l.(Level_repr.t.level) +Z i) →
letP? l' := Level_storage.add ctxt l i in
let raw_level1 := l.(Level_repr.t.level) in
let raw_level2 := l'.(Level_repr.t.level) in
raw_level2 = raw_level1 +Z i.
Proof.
intros H_ctxt Hint Hlevel Hint_level.
unfold Level_storage.add.
eapply Error.split_letP. {
apply Raw_level_repr.add_eq.
{ apply Hlevel. }
{ lia. }
}
intros raw_level H_raw_level. cbn in ×.
subst raw_level.
pose proof (Level_storage.from_raw_eq ctxt
(l.(Level_repr.t.level) +Z i)) as H_from_raw.
pose proof (Level_storage.from_raw_is_valid ctxt
(l.(Level_repr.t.level) +Z i)) as H_from_raw'.
destruct (Level_storage.from_raw _ _).
{ apply H_from_raw; [|assumption].
apply (Valid.le_impl_t ctxt l.(Level_repr.t.level)
(l.(Level_repr.t.level) +Z i) ltac:(lia) ltac:(assumption)).
}
{ cbn in ×. apply H_from_raw'; try easy.
apply (Valid.le_impl_t ctxt l.(Level_repr.t.level)
(l.(Level_repr.t.level) +Z i) ltac:(lia) ltac:(assumption)).
}
Qed.
The function [sub] is valid.
Lemma sub_is_valid ctxt level n :
Pervasives.Int.Valid.t n →
Raw_level_repr.Valid.t (level.(Level_repr.t.level)) →
Raw_level_repr.Valid.t (level.(Level_repr.t.level) -Z n) →
Valid.t ctxt (level.(Level_repr.t.level) -Z n) →
letP? level := Level_storage.sub ctxt level n in
Option.Forall Level_repr.Valid.t level.
Proof.
intros H_n H_level H_level' H_ctxt.
unfold Level_storage.sub.
eapply Error.split_letP. {
apply Raw_level_repr.sub_eq; [|easy].
apply H_level.
}
intros opti32 H_opt; cbn in ×.
step; [|easy].
injection H_opt as H_i. subst i.
eapply Error.split_letP. {
apply Level_repr.root_level_is_valid.
Raw_context.Valid.destruct_rewrite H_ctxt.
cbn in ×.
now destruct H_sim_ctxt, config.
}
intros level'' H_level''.
step; [|easy].
eapply Error.split_letP. {
now apply from_raw_is_valid.
} easy.
Qed.
Pervasives.Int.Valid.t n →
Raw_level_repr.Valid.t (level.(Level_repr.t.level)) →
Raw_level_repr.Valid.t (level.(Level_repr.t.level) -Z n) →
Valid.t ctxt (level.(Level_repr.t.level) -Z n) →
letP? level := Level_storage.sub ctxt level n in
Option.Forall Level_repr.Valid.t level.
Proof.
intros H_n H_level H_level' H_ctxt.
unfold Level_storage.sub.
eapply Error.split_letP. {
apply Raw_level_repr.sub_eq; [|easy].
apply H_level.
}
intros opti32 H_opt; cbn in ×.
step; [|easy].
injection H_opt as H_i. subst i.
eapply Error.split_letP. {
apply Level_repr.root_level_is_valid.
Raw_context.Valid.destruct_rewrite H_ctxt.
cbn in ×.
now destruct H_sim_ctxt, config.
}
intros level'' H_level''.
step; [|easy].
eapply Error.split_letP. {
now apply from_raw_is_valid.
} easy.
Qed.
[sub] is equivalent to [-Z]
Lemma sub_eq (ctxt : Proto_alpha.Raw_context.t)
(l : Level_repr.t) (i : Int32.t) :
Pervasives.Int.Valid.t i →
Valid.t ctxt (l.(Level_repr.t.level) -Z i) →
Int32.Valid.t (l.(Level_repr.t.level) -Z i) →
Level_repr.Valid.t l →
letP? res := Level_storage.sub ctxt l i in
match res with
| Some l' ⇒
let raw_level1 := l.(Level_repr.t.level) in
let raw_level2 := l'.(Level_repr.t.level) in
raw_level2 = raw_level1 -Z i
| None ⇒ True
end.
Proof.
intros H_int H_ctxt H_int32 H_level.
unfold Level_storage.sub.
destruct H_level.
pose proof (Raw_level_repr.sub_eq l.(Level_repr.t.level) i
level ltac:(assumption)) as H_sub.
pose proof (Raw_level_repr.sub_is_valid l.(Level_repr.t.level) i
level ltac:(assumption)) as H_sub'.
destruct (Raw_level_repr.sub _ _) as [opt|]; cbn in *; [|easy].
subst opt. cbn in ×.
eapply Error.split_letP. {
apply Level_repr.root_level_is_valid.
Raw_context.Valid.destruct_rewrite H_ctxt.
cbn in ×.
now destruct H_sim_ctxt, config.
} intros level' H_level'.
step; [|easy].
eapply Error.split_letP. {
now apply from_raw_eq.
}
easy.
Qed.
(l : Level_repr.t) (i : Int32.t) :
Pervasives.Int.Valid.t i →
Valid.t ctxt (l.(Level_repr.t.level) -Z i) →
Int32.Valid.t (l.(Level_repr.t.level) -Z i) →
Level_repr.Valid.t l →
letP? res := Level_storage.sub ctxt l i in
match res with
| Some l' ⇒
let raw_level1 := l.(Level_repr.t.level) in
let raw_level2 := l'.(Level_repr.t.level) in
raw_level2 = raw_level1 -Z i
| None ⇒ True
end.
Proof.
intros H_int H_ctxt H_int32 H_level.
unfold Level_storage.sub.
destruct H_level.
pose proof (Raw_level_repr.sub_eq l.(Level_repr.t.level) i
level ltac:(assumption)) as H_sub.
pose proof (Raw_level_repr.sub_is_valid l.(Level_repr.t.level) i
level ltac:(assumption)) as H_sub'.
destruct (Raw_level_repr.sub _ _) as [opt|]; cbn in *; [|easy].
subst opt. cbn in ×.
eapply Error.split_letP. {
apply Level_repr.root_level_is_valid.
Raw_context.Valid.destruct_rewrite H_ctxt.
cbn in ×.
now destruct H_sim_ctxt, config.
} intros level' H_level'.
step; [|easy].
eapply Error.split_letP. {
now apply from_raw_eq.
}
easy.
Qed.
[previous] level is valid
Lemma previous_is_valid ctxt :
Valid.t ctxt
((Level_storage.current ctxt).(Level_repr.t.level) -Z 1) →
(letP? pred :=
Level_storage.pred ctxt (Level_storage.current ctxt) in
pred ≠ None) →
letP? lsp := Level_storage.previous ctxt in
Level_repr.Valid.t lsp.
Proof.
intros H_ctxt H_pred.
unfold Level_storage.previous.
eapply Error.split_letP. {
assert (H_ctxt' : Raw_context.Valid.t ctxt).
{ unfold Valid.t in H_ctxt.
now apply Raw_context.on_impl_t in H_ctxt.
}
let current := constr:(Level_storage.current ctxt) in
pose proof pred_is_valid ctxt current
H_ctxt (current_is_valid ctxt H_ctxt')
as H_pred'.
destruct (Level_storage.pred _ _); [|easy].
cbn in ×.
instantiate (1 := fun x ⇒
x ≠ None ∧ Option.Forall Level_repr.Valid.t x).
easy.
}
intros opt_level H_opt_level; cbn in ×. destruct H_opt_level as
[H_opt_neq H_opt_valid].
step; cbn; [|contradiction].
easy.
Qed.
Valid.t ctxt
((Level_storage.current ctxt).(Level_repr.t.level) -Z 1) →
(letP? pred :=
Level_storage.pred ctxt (Level_storage.current ctxt) in
pred ≠ None) →
letP? lsp := Level_storage.previous ctxt in
Level_repr.Valid.t lsp.
Proof.
intros H_ctxt H_pred.
unfold Level_storage.previous.
eapply Error.split_letP. {
assert (H_ctxt' : Raw_context.Valid.t ctxt).
{ unfold Valid.t in H_ctxt.
now apply Raw_context.on_impl_t in H_ctxt.
}
let current := constr:(Level_storage.current ctxt) in
pose proof pred_is_valid ctxt current
H_ctxt (current_is_valid ctxt H_ctxt')
as H_pred'.
destruct (Level_storage.pred _ _); [|easy].
cbn in ×.
instantiate (1 := fun x ⇒
x ≠ None ∧ Option.Forall Level_repr.Valid.t x).
easy.
}
intros opt_level H_opt_level; cbn in ×. destruct H_opt_level as
[H_opt_neq H_opt_valid].
step; cbn; [|contradiction].
easy.
Qed.
[pred] do not return none on positive input
Lemma pred_not_none ctxt x :
Valid.t ctxt (x.(Level_repr.t.level) -i32 1) →
Int32.Valid.positive x.(Level_repr.t.level) →
letP? x' := Level_storage.pred ctxt x in
x' ≠ None.
Proof.
intros.
unfold Level_storage.pred, Raw_level_repr.pred.
destruct x; cbn in ×.
replace (_ =? 0) with false by lia.
unfold Int32.pred in ×.
pose proof (from_raw_is_valid ctxt (Int32.pred level)
ltac:(assumption)) as H_from_raw.
destruct (Level_storage.from_raw _ _); [
|apply H_from_raw; lia].
cbn.
discriminate.
Qed.
Valid.t ctxt (x.(Level_repr.t.level) -i32 1) →
Int32.Valid.positive x.(Level_repr.t.level) →
letP? x' := Level_storage.pred ctxt x in
x' ≠ None.
Proof.
intros.
unfold Level_storage.pred, Raw_level_repr.pred.
destruct x; cbn in ×.
replace (_ =? 0) with false by lia.
unfold Int32.pred in ×.
pose proof (from_raw_is_valid ctxt (Int32.pred level)
ltac:(assumption)) as H_from_raw.
destruct (Level_storage.from_raw _ _); [
|apply H_from_raw; lia].
cbn.
discriminate.
Qed.
[previous] is equal to [pred (current ctxt)]
Lemma pred_current_eq_previous (ctxt : Proto_alpha.Raw_context.t) :
letP?relaxed res :=
Level_storage.pred ctxt (Level_storage.current ctxt) in
letP?relaxed res' := Level_storage.previous ctxt in
match res with
| Some prev ⇒ prev = res'
| None ⇒ True
end.
Proof.
intros; unfold Level_storage.previous.
do 2 (step; cbn; [|try easy]).
reflexivity.
Qed.
letP?relaxed res :=
Level_storage.pred ctxt (Level_storage.current ctxt) in
letP?relaxed res' := Level_storage.previous ctxt in
match res with
| Some prev ⇒ prev = res'
| None ⇒ True
end.
Proof.
intros; unfold Level_storage.previous.
do 2 (step; cbn; [|try easy]).
reflexivity.
Qed.
The function [first_level_in_cycle] is valid.
Lemma first_level_in_cycle_is_valid ctxt cycle :
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t cycle →
letP? level :=
Level_storage.first_level_in_cycle ctxt cycle in
Level_repr.Valid.t level.
Proof.
intros H.
unfold Level_storage.first_level_in_cycle; cbn.
Raw_context.Valid.destruct_rewrite H.
apply Level_repr.first_level_in_cycle_from_eras_is_valid; dtauto.
Qed.
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t cycle →
letP? level :=
Level_storage.first_level_in_cycle ctxt cycle in
Level_repr.Valid.t level.
Proof.
intros H.
unfold Level_storage.first_level_in_cycle; cbn.
Raw_context.Valid.destruct_rewrite H.
apply Level_repr.first_level_in_cycle_from_eras_is_valid; dtauto.
Qed.
The function [last_level_in_cycle] is valid.
Lemma last_level_in_cycle_is_valid ctxt cycle :
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t (cycle +Z 1) →
letP? first_level_in_next_cycle :=
Level_storage.first_level_in_cycle ctxt (cycle +Z 1) in
Raw_level_repr.Valid.t
(first_level_in_next_cycle.(Level_repr.t.level) - 1) →
Valid.t ctxt (first_level_in_next_cycle.(Level_repr.t.level) - 1) →
letP? last_level_in_cycle :=
Level_storage.last_level_in_cycle ctxt cycle in
Level_repr.Valid.t last_level_in_cycle.
Proof.
intros.
unfold Level_storage.last_level_in_cycle in ×.
unfold Cycle_repr.succ, Int32.succ, "+i32". fold Z.add in ×.
rewrite Int32.normalize_identity by lia.
pose proof (first_level_in_cycle_is_valid ctxt (cycle +Z 1)
ltac:(assumption) ltac:(assumption)) as H_first.
destruct (Level_storage.first_level_in_cycle ctxt (cycle +Z 1))
as [first_level_in_next_cycle|]; cbn in *; [|easy].
intros H_raw_level H_ctxt.
pose proof (pred_not_none ctxt first_level_in_next_cycle)
as H_pred_not_none.
unfold "-i32" in ×. rewrite Int32.normalize_identity in × by lia.
specialize (H_pred_not_none H_ctxt ltac:(destruct H_first; cbn in *;
lia)).
pose proof (pred_eq ctxt first_level_in_next_cycle ltac:(lia)
H_ctxt H_first) as H_pred.
pose proof (pred_is_valid ctxt first_level_in_next_cycle ltac:(lia)
H_first) as H_pred_valid.
destruct (Level_storage.pred _ _) as [opt_pred|]; cbn in *; [|easy].
destruct opt_pred as [last_level_in_cycle|]; [|easy]. cbn.
easy.
Qed.
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t (cycle +Z 1) →
letP? first_level_in_next_cycle :=
Level_storage.first_level_in_cycle ctxt (cycle +Z 1) in
Raw_level_repr.Valid.t
(first_level_in_next_cycle.(Level_repr.t.level) - 1) →
Valid.t ctxt (first_level_in_next_cycle.(Level_repr.t.level) - 1) →
letP? last_level_in_cycle :=
Level_storage.last_level_in_cycle ctxt cycle in
Level_repr.Valid.t last_level_in_cycle.
Proof.
intros.
unfold Level_storage.last_level_in_cycle in ×.
unfold Cycle_repr.succ, Int32.succ, "+i32". fold Z.add in ×.
rewrite Int32.normalize_identity by lia.
pose proof (first_level_in_cycle_is_valid ctxt (cycle +Z 1)
ltac:(assumption) ltac:(assumption)) as H_first.
destruct (Level_storage.first_level_in_cycle ctxt (cycle +Z 1))
as [first_level_in_next_cycle|]; cbn in *; [|easy].
intros H_raw_level H_ctxt.
pose proof (pred_not_none ctxt first_level_in_next_cycle)
as H_pred_not_none.
unfold "-i32" in ×. rewrite Int32.normalize_identity in × by lia.
specialize (H_pred_not_none H_ctxt ltac:(destruct H_first; cbn in *;
lia)).
pose proof (pred_eq ctxt first_level_in_next_cycle ltac:(lia)
H_ctxt H_first) as H_pred.
pose proof (pred_is_valid ctxt first_level_in_next_cycle ltac:(lia)
H_first) as H_pred_valid.
destruct (Level_storage.pred _ _) as [opt_pred|]; cbn in *; [|easy].
destruct opt_pred as [last_level_in_cycle|]; [|easy]. cbn.
easy.
Qed.
The function [levels_in_cycle] is valid.
Lemma levels_in_cycle_is_valid ctxt cycle :
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t cycle →
letP? levels := Level_storage.levels_in_cycle ctxt cycle in
List.Forall Level_repr.Valid.t levels.
Proof.
intros.
unfold Level_storage.levels_in_cycle.
eapply Error.split_letP. {
now apply first_level_in_cycle_is_valid.
}
intros first_level_in_cycle' H_first.
cbn.
(* @TODO : This involves a loop function that recurses
over the levels, the levels are ints so Coq cannot
check that it ends
*)
Admitted.
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t cycle →
letP? levels := Level_storage.levels_in_cycle ctxt cycle in
List.Forall Level_repr.Valid.t levels.
Proof.
intros.
unfold Level_storage.levels_in_cycle.
eapply Error.split_letP. {
now apply first_level_in_cycle_is_valid.
}
intros first_level_in_cycle' H_first.
cbn.
(* @TODO : This involves a loop function that recurses
over the levels, the levels are ints so Coq cannot
check that it ends
*)
Admitted.
The function [levels_in_current_cycle] is valid.
Lemma levels_in_current_cycle_is_valid ctxt offset :
Raw_context.Valid.t ctxt →
Option.Forall (fun offset : int32 ⇒
let current :=
(Level_storage.current ctxt).(Level_repr.t.level) in
Cycle_repr.Valid.t (current +Z offset))
offset →
letP? levels :=
Level_storage.levels_in_current_cycle ctxt offset tt in
List.Forall Level_repr.Valid.t levels.
Proof.
intros H_ctxt **.
unfold Level_storage.levels_in_current_cycle.
unfold Cycle_repr.to_int32.
destruct offset as [offset|].
{ cbn in ×. step; cbn.
{ constructor. }
{ apply levels_in_cycle_is_valid; [easy|].
unfold Cycle_repr.of_int32_exn.
step; [|lia].
pose proof current_is_valid as H_current.
repeat specialize (H_current ltac:(assumption)).
destruct (Level_storage.current ctxt); cbn.
destruct H_current; cbn in ×.
lia.
}
}
{ cbn in ×. step; cbn; [constructor|].
apply levels_in_cycle_is_valid; [easy|].
unfold Cycle_repr.of_int32_exn.
step; lia.
}
Qed.
Raw_context.Valid.t ctxt →
Option.Forall (fun offset : int32 ⇒
let current :=
(Level_storage.current ctxt).(Level_repr.t.level) in
Cycle_repr.Valid.t (current +Z offset))
offset →
letP? levels :=
Level_storage.levels_in_current_cycle ctxt offset tt in
List.Forall Level_repr.Valid.t levels.
Proof.
intros H_ctxt **.
unfold Level_storage.levels_in_current_cycle.
unfold Cycle_repr.to_int32.
destruct offset as [offset|].
{ cbn in ×. step; cbn.
{ constructor. }
{ apply levels_in_cycle_is_valid; [easy|].
unfold Cycle_repr.of_int32_exn.
step; [|lia].
pose proof current_is_valid as H_current.
repeat specialize (H_current ltac:(assumption)).
destruct (Level_storage.current ctxt); cbn.
destruct H_current; cbn in ×.
lia.
}
}
{ cbn in ×. step; cbn; [constructor|].
apply levels_in_cycle_is_valid; [easy|].
unfold Cycle_repr.of_int32_exn.
step; lia.
}
Qed.
The function [levels_with_commitments_in_cycle] is valid.
Lemma levels_with_commitments_in_cycle_is_valid ctxt cycle :
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t cycle →
letP? levels :=
Level_storage.levels_with_commitments_in_cycle ctxt cycle in
List.Forall Level_repr.Valid.t levels.
Proof.
intros.
unfold Level_storage.levels_with_commitments_in_cycle.
Raw_context.Valid.t ctxt →
Cycle_repr.Valid.t cycle →
letP? levels :=
Level_storage.levels_with_commitments_in_cycle ctxt cycle in
List.Forall Level_repr.Valid.t levels.
Proof.
intros.
unfold Level_storage.levels_with_commitments_in_cycle.
This involves a loop function that recurses over the
levels. Coq can't check that it finishes
Admitted.
The function [last_allowed_fork_level] is valid.
Lemma last_allowed_fork_level_is_valid ctxt :
Raw_context.Valid.t ctxt →
letP? level :=
Level_storage.last_allowed_fork_level ctxt in
Raw_level_repr.Valid.t level.
Proof.
intros H.
unfold Level_storage.last_allowed_fork_level.
Raw_context.Valid.destruct_rewrite H.
eapply Error.split_letP.
{ apply Cycle_repr.sub_is_valid.
unfold Constants_storage.preserved_cycles; cbn.
destruct H_sim_ctxt, config, constants.
lia.
}
{ intros [cycle|] ?; simpl in *;
[|apply Raw_level_repr.root_value_is_valid].
eapply Error.split_letP; [
now apply first_level_in_cycle_is_valid |
sauto l: on
].
}
Qed.
Raw_context.Valid.t ctxt →
letP? level :=
Level_storage.last_allowed_fork_level ctxt in
Raw_level_repr.Valid.t level.
Proof.
intros H.
unfold Level_storage.last_allowed_fork_level.
Raw_context.Valid.destruct_rewrite H.
eapply Error.split_letP.
{ apply Cycle_repr.sub_is_valid.
unfold Constants_storage.preserved_cycles; cbn.
destruct H_sim_ctxt, config, constants.
lia.
}
{ intros [cycle|] ?; simpl in *;
[|apply Raw_level_repr.root_value_is_valid].
eapply Error.split_letP; [
now apply first_level_in_cycle_is_valid |
sauto l: on
].
}
Qed.
The function [last_of_a_cycle] is valid.
Lemma last_of_a_cycle_is_valid ctxt level :
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Level_storage.last_of_a_cycle ctxt level in
True.
Proof.
intros.
unfold Level_storage.last_of_a_cycle.
apply Level_repr.last_of_cycle_is_valid.
Qed.
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Level_storage.last_of_a_cycle ctxt level in
True.
Proof.
intros.
unfold Level_storage.last_of_a_cycle.
apply Level_repr.last_of_cycle_is_valid.
Qed.
Given a context with at last one era, with a level on it,
[dawn_of_a_new_cycle] is when the next [cycle_position]
is equal to the [cycle_era.blocks_per_cycle] for that era
Lemma dawn_of_a_new_cycle_eq (ctxt : Proto_alpha.Raw_context.t)
(era : Level_repr.cycle_era) :
Raw_context.Has_one_era.t ctxt era →
Level_repr.Level_in_era.t (Level_storage.current ctxt) era →
Int32.succ
(Level_storage.current ctxt).(Level_repr.t.cycle_position) =?
era.(Level_repr.cycle_era.blocks_per_cycle) = true →
letP? res := Level_storage.dawn_of_a_new_cycle ctxt in
match res with
| Some l ⇒ l = (Level_storage.current ctxt).(Level_repr.t.cycle)
| None ⇒ True
end.
Proof.
intros.
unfold Level_storage.dawn_of_a_new_cycle.
unfold Level_storage.last_of_a_cycle.
unfold Level_repr.last_of_cycle. simpl.
unfold Level_repr.era_of_level.
rewrite H.
unfold Raw_level_repr.op_gteq. simpl.
unfold Level_repr.Level_in_era.t in H0.
rewrite <- Reflect.Z_geb_ge in H0; unfold is_true in H0.
remember (_ >=? _) as cond. rewrite H0.
hauto lq: on.
Qed.
(era : Level_repr.cycle_era) :
Raw_context.Has_one_era.t ctxt era →
Level_repr.Level_in_era.t (Level_storage.current ctxt) era →
Int32.succ
(Level_storage.current ctxt).(Level_repr.t.cycle_position) =?
era.(Level_repr.cycle_era.blocks_per_cycle) = true →
letP? res := Level_storage.dawn_of_a_new_cycle ctxt in
match res with
| Some l ⇒ l = (Level_storage.current ctxt).(Level_repr.t.cycle)
| None ⇒ True
end.
Proof.
intros.
unfold Level_storage.dawn_of_a_new_cycle.
unfold Level_storage.last_of_a_cycle.
unfold Level_repr.last_of_cycle. simpl.
unfold Level_repr.era_of_level.
rewrite H.
unfold Raw_level_repr.op_gteq. simpl.
unfold Level_repr.Level_in_era.t in H0.
rewrite <- Reflect.Z_geb_ge in H0; unfold is_true in H0.
remember (_ >=? _) as cond. rewrite H0.
hauto lq: on.
Qed.