Skip to main content

💎 Nonce_storage.v

Proofs

See code, Gitlab , OCaml

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.
The function [record_hash] is valid.
The function [check_unrevealed] is valid.
The function [reveal] is valid.
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
Context contains an [Storage.Cycle.Unrevealed _] value
[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

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

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