💎 Nonce_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Nonce_storage.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Nonce_storage.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Int32.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
The encoding [encoding] is valid.
Lemma encoding_is_valid :
Data_encoding.Valid.t Seed_repr.Nonce.Valid.t Nonce_storage.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t Seed_repr.Nonce.Valid.t Nonce_storage.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
The function [get_unrevealed] is valid.
Lemma get_unrevealed_is_valid ctxt level :
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.get_unrevealed ctxt level in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.get_unrevealed ctxt level in
True.
Proof.
Admitted.
The function [record_hash] is valid.
Lemma record_hash_is_valid ctxt unrevealed :
Raw_context.Valid.t ctxt →
letP? ctxt := Nonce_storage.record_hash ctxt unrevealed in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
letP? ctxt := Nonce_storage.record_hash ctxt unrevealed in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [check_unrevealed] is valid.
Lemma check_unrevealed_is_valid ctxt level nonce_value :
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.check_unrevealed ctxt level nonce_value in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.check_unrevealed ctxt level nonce_value in
True.
Proof.
Admitted.
The function [reveal] is valid.
Lemma reveal_is_valid ctxt level nonce_value :
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? ctxt := Nonce_storage.reveal ctxt level nonce_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? ctxt := Nonce_storage.reveal ctxt level nonce_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [get] is valid.
Lemma get_is_valid ctxt level :
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.get ctxt level in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.get ctxt level in
True.
Proof.
Admitted.
The function [check] is valid.
Lemma check_is_valid ctxt level :
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.check ctxt level in
True.
Proof.
Admitted.
Raw_context.Valid.t ctxt →
Level_repr.Valid.t level →
letP? _ := Nonce_storage.check ctxt level in
True.
Proof.
Admitted.
Condition on a [Raw_context.t] and a [Level_repr.t] for a nonce to be
revealable
Module Nonce_is_revealable.
Definition t (ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t) :
Prop :=
let cur_level := Level_storage.current ctxt in
let cur_level' := cur_level.(Level_repr.t.cycle) in
Int32.Valid.positive cur_level' ∧
(cur_level' - 1) = level.(Level_repr.t.cycle).
End Nonce_is_revealable.
Definition t (ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t) :
Prop :=
let cur_level := Level_storage.current ctxt in
let cur_level' := cur_level.(Level_repr.t.cycle) in
Int32.Valid.positive cur_level' ∧
(cur_level' - 1) = level.(Level_repr.t.cycle).
End Nonce_is_revealable.
Context contains an [Storage.Cycle.Unrevealed _] value
Module Context_contains_unrevealed.
Definition t
(ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t)
(status : Storage.Cycle.unrevealed_nonce): Prop :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
ctxt level = return? Storage.Cycle.Unrevealed status.
End Context_contains_unrevealed.
Definition t
(ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t)
(status : Storage.Cycle.unrevealed_nonce): Prop :=
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.get)
ctxt level = return? Storage.Cycle.Unrevealed status.
End Context_contains_unrevealed.
[status.nonce_hash] is valid regarding [Seed_repr.check_hash] function
Module Seed_repr_valid_hash.
Definition t
(nonce_bytes : bytes)
(status : Storage.Cycle.unrevealed_nonce) :=
(Seed_repr.check_hash nonce_bytes
status.(Storage.Cycle.unrevealed_nonce.nonce_hash)) = true.
End Seed_repr_valid_hash.
Definition t
(nonce_bytes : bytes)
(status : Storage.Cycle.unrevealed_nonce) :=
(Seed_repr.check_hash nonce_bytes
status.(Storage.Cycle.unrevealed_nonce.nonce_hash)) = true.
End Seed_repr_valid_hash.
Given a context with an unrevealed nonce
that is revealable, regariding [ContextCurrentLevelCycle]
[get_unrevealed] returns the unrealed nonce
Lemma get_unrevealed_eq ctxt level status :
Context_contains_unrevealed.t ctxt level status →
Nonce_is_revealable.t ctxt level →
(Level_storage.current ctxt).(Level_repr.t.cycle_position) <
Constants_storage.nonce_revelation_threshold ctxt →
Nonce_storage.get_unrevealed ctxt level = Pervasives.Ok status.
Proof.
intros H_unrevealed H_revealable H_threshold.
unfold Nonce_storage.get_unrevealed.
set (i := _.(Level_repr.t.cycle)).
unfold Nonce_is_revealable.t in H_revealable.
assert (H1 : Cycle_repr.pred i = Some (Int32.pred i)).
{ unfold Cycle_repr.pred.
unfold Int32.Valid.positive in H_revealable.
match goal with
| |- match ?e with _ ⇒ _ end = _ ⇒ destruct e eqn:?
end; [lia|easy|lia]. }
rewrite H1.
autounfold with tezos_z.
rewrite Int32.normalize_identity;
[|unfold Int32.Valid.positive in H_revealable; lia].
unfold Cycle_repr.op_lt. simpl.
assert (H2 : i - 1 <? level.(Level_repr.t.cycle) = false) by lia.
assert (H3 : level.(Level_repr.t.cycle) <? i - 1 = false) by lia.
rewrite H_unrevealed, H2, H3; simpl.
step; lia.
Qed.
(* @TODO *)
Context_contains_unrevealed.t ctxt level status →
Nonce_is_revealable.t ctxt level →
(Level_storage.current ctxt).(Level_repr.t.cycle_position) <
Constants_storage.nonce_revelation_threshold ctxt →
Nonce_storage.get_unrevealed ctxt level = Pervasives.Ok status.
Proof.
intros H_unrevealed H_revealable H_threshold.
unfold Nonce_storage.get_unrevealed.
set (i := _.(Level_repr.t.cycle)).
unfold Nonce_is_revealable.t in H_revealable.
assert (H1 : Cycle_repr.pred i = Some (Int32.pred i)).
{ unfold Cycle_repr.pred.
unfold Int32.Valid.positive in H_revealable.
match goal with
| |- match ?e with _ ⇒ _ end = _ ⇒ destruct e eqn:?
end; [lia|easy|lia]. }
rewrite H1.
autounfold with tezos_z.
rewrite Int32.normalize_identity;
[|unfold Int32.Valid.positive in H_revealable; lia].
unfold Cycle_repr.op_lt. simpl.
assert (H2 : i - 1 <? level.(Level_repr.t.cycle) = false) by lia.
assert (H3 : level.(Level_repr.t.cycle) <? i - 1 = false) by lia.
rewrite H_unrevealed, H2, H3; simpl.
step; lia.
Qed.
(* @TODO *)
Given a context with an unrevealed nonce and not in the first level cycle
[reveal] is equivalent to [Non_iterable_indexed_data_storage.update] the
unrevealed nonce with a revealed nonce
Lemma reveal_eq ctxt level status nonce_bytes :
Context_contains_unrevealed.t ctxt level status →
Nonce_is_revealable.t ctxt level →
(Level_storage.current ctxt).(Level_repr.t.cycle_position) <
Constants_storage.nonce_revelation_threshold ctxt →
Seed_repr_valid_hash.t nonce_bytes status →
Nonce_storage.reveal ctxt level nonce_bytes =
Storage.Seed.Nonce.(
Storage_sigs.Non_iterable_indexed_data_storage.update)
ctxt level (Storage.Cycle.Revealed nonce_bytes).
Proof.
intros. unfold Nonce_storage.reveal.
Admitted.
Context_contains_unrevealed.t ctxt level status →
Nonce_is_revealable.t ctxt level →
(Level_storage.current ctxt).(Level_repr.t.cycle_position) <
Constants_storage.nonce_revelation_threshold ctxt →
Seed_repr_valid_hash.t nonce_bytes status →
Nonce_storage.reveal ctxt level nonce_bytes =
Storage.Seed.Nonce.(
Storage_sigs.Non_iterable_indexed_data_storage.update)
ctxt level (Storage.Cycle.Revealed nonce_bytes).
Proof.
intros. unfold Nonce_storage.reveal.
Admitted.
Given a context with an unrevealed nonce that is revealable,
regarging [ContextCurrentLevelCycle] and given a valid status
apply [reveal] to that nonce, followed by [get], returns the
revealed nonce
Lemma get_reveal_eq
(ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t)
(status : Storage.Cycle.unrevealed_nonce) (nonce_bytes : bytes) :
Context_contains_unrevealed.t ctxt level status →
Nonce_is_revealable.t ctxt level →
Seed_repr_valid_hash.t nonce_bytes status →
(Level_storage.current ctxt).(Level_repr.t.cycle_position) <
Constants_storage.nonce_revelation_threshold ctxt →
letP? ctxt' := Nonce_storage.reveal ctxt level nonce_bytes in
letP? x := Nonce_storage.get ctxt' level in
x = (Storage.Cycle.Revealed nonce_bytes).
Proof.
intros H_unrevealed H_revealable H_hash H_threshold.
rewrite (reveal_eq ctxt level status nonce_bytes); try assumption.
unfold bind_prop.
Admitted.
(ctxt : Proto_alpha.Raw_context.t) (level : Level_repr.t)
(status : Storage.Cycle.unrevealed_nonce) (nonce_bytes : bytes) :
Context_contains_unrevealed.t ctxt level status →
Nonce_is_revealable.t ctxt level →
Seed_repr_valid_hash.t nonce_bytes status →
(Level_storage.current ctxt).(Level_repr.t.cycle_position) <
Constants_storage.nonce_revelation_threshold ctxt →
letP? ctxt' := Nonce_storage.reveal ctxt level nonce_bytes in
letP? x := Nonce_storage.get ctxt' level in
x = (Storage.Cycle.Revealed nonce_bytes).
Proof.
intros H_unrevealed H_revealable H_hash H_threshold.
rewrite (reveal_eq ctxt level status nonce_bytes); try assumption.
unfold bind_prop.
Admitted.
Lemma find_ok_implies_check_ok ctxt level x :
Storage.Seed.Nonce.(
Storage_sigs.Non_iterable_indexed_data_storage.find) ctxt level =
Pervasives.Ok x →
match Nonce_storage.check ctxt level with
| Pervasives.Ok _ ⇒ True
| Pervasives.Error _ ⇒ False
end.
Proof.
intro H.
unfold Nonce_storage.check.
destruct (_ ctxt level); simpl; [|discriminate H].
now destruct o.
Qed.
Storage.Seed.Nonce.(
Storage_sigs.Non_iterable_indexed_data_storage.find) ctxt level =
Pervasives.Ok x →
match Nonce_storage.check ctxt level with
| Pervasives.Ok _ ⇒ True
| Pervasives.Error _ ⇒ False
end.
Proof.
intro H.
unfold Nonce_storage.check.
destruct (_ ctxt level); simpl; [|discriminate H].
now destruct o.
Qed.
[Non_iterable_indexed_data_storage.find ... = Pervasives.Ok None]
implies [check ... = Pervasives.Ok No_nonce_expected]
Lemma check_no_nonce_expected_eq ctxt level :
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.find)
ctxt level = Pervasives.Ok None →
Nonce_storage.check ctxt level = Pervasives.Ok
Nonce_storage.No_nonce_expected.
Proof.
intros.
unfold Nonce_storage.check.
now rewrite H.
Qed.
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.find)
ctxt level = Pervasives.Ok None →
Nonce_storage.check ctxt level = Pervasives.Ok
Nonce_storage.No_nonce_expected.
Proof.
intros.
unfold Nonce_storage.check.
now rewrite H.
Qed.
[Non_iterable_indexed_data_storage.find ... = Pervasives.Ok (Some status)]
implies [check ... = Pervasives.Ok (Nonce_expected status)]
Lemma check_nonce_expected_eq
(ctxt : Proto_alpha.Raw_context.t)
(level : Level_repr.t)
(status : Storage.Seed.nonce_status) :
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.find)
ctxt level
= Pervasives.Ok (Some status) →
Nonce_storage.check ctxt level =
Pervasives.Ok (Nonce_storage.Nonce_expected status).
Proof.
intros.
unfold Nonce_storage.check.
now rewrite H.
Qed.
(ctxt : Proto_alpha.Raw_context.t)
(level : Level_repr.t)
(status : Storage.Seed.nonce_status) :
Storage.Seed.Nonce.(Storage_sigs.Non_iterable_indexed_data_storage.find)
ctxt level
= Pervasives.Ok (Some status) →
Nonce_storage.check ctxt level =
Pervasives.Ok (Nonce_storage.Nonce_expected status).
Proof.
intros.
unfold Nonce_storage.check.
now rewrite H.
Qed.