💎 Nonce_storage.v

Proofs

See code, Gitlab , OCaml

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

[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.

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 *)

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.

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.

[Non_iterable_indexed_data_storage.find] success implies

[check] success

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.

[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.

[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.