Skip to main content

💎 Nonce_storage.v

Proofs

See code, Gitlab , OCaml

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 : Raw_context.t) (level : Level_repr.t)
      (status : Storage.Cycle.unrevealed_nonce) :
  Context_contains_unrevealed.t ctxt level status
  Nonce_is_revealable.t ctxt level
  Nonce_storage.get_unrevealed ctxt level = Pervasives.Ok status.
Proof.
  intros.
  unfold Nonce_storage.get_unrevealed.
  set (i := _.(Level_repr.t.cycle)).
  unfold Nonce_is_revealable.t in H0.
  assert (H1 : Cycle_repr.pred i = Some (Int32.pred i)).
  { unfold Cycle_repr.pred.
    unfold Int32.Valid.positive in H0.
    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 H0; 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.
  now rewrite H, H2, H3.
Qed.

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

[find . add] identity.

Fetching an added item on a context returns the same item

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 : 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
  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.
  rewrite (reveal_eq ctxt level status nonce_bytes); try assumption.
  unfold bind_prop.
  rewrite (Storage.Eq.Seeds.Nonce.eq)
    .(Non_iterable_indexed_data_storage.Eq.update).
  simpl.
  destruct Non_iterable_indexed_data_storage.Op.update eqn:?; [|easy].
  simpl.
  unfold Non_iterable_indexed_data_storage.Op.update in Heqt.
  assert (Non_iterable_indexed_data_storage.Op.mem
           (Storage.Eq.Seeds.Nonce.parse ctxt) level = true) by scrush.
  rewrite H2 in Heqt.
  injection Heqt as Heqt.
  rewrite <- Heqt.
  rewrite (Storage.Eq.Seeds.Nonce.eq)
    .(Non_iterable_indexed_data_storage.Eq.get).
  simpl.
  unfold Storage.Eq.Seeds.Nonce.parse;
  unfold Storage.Eq.Seeds.Nonce.apply.
  rewrite Storage.parse_apply.
  unfold Non_iterable_indexed_data_storage.Op.get.
  unfold Non_iterable_indexed_data_storage.Op.find.
  unfold Indexed_data_storage.State.Map.
  now rewrite (find_apply_add_eq ctxt level
                                 (Storage.Cycle.Revealed nonce_bytes)).
Qed.

[Non_iterable_indexed_data_storage.find] success implies

[check] success

Lemma find_ok_implies_check_ok (ctxt : Raw_context.t)
      (level : Level_repr.t)
  (x : option Nonce_storage.status) :
  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 : Raw_context.t) (level : Level_repr.t) :
  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 : 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.

If contect does not contains the [unrevealed] nonce.

[record_hash] followed by [get] returns the same

[unrevealed]

Lemma record_hash_get_eq
      (ctxt : Raw_context.t)
      (nonce : Storage.Cycle.unrevealed_nonce) :
  let level := Level_storage.current ctxt in
  Non_iterable_indexed_data_storage.Op.mem
    (Storage.Eq.Seeds.Nonce.parse ctxt)
    level = false
  match Nonce_storage.record_hash ctxt nonce with
  | Pervasives.Ok ctxt'
      Nonce_storage.get ctxt' (Level_storage.current ctxt) =
        Pervasives.Ok (Storage.Cycle.Unrevealed nonce)
  | Pervasives.Error eTrue
  end.
Proof.
  intros.
  unfold Nonce_storage.record_hash.
  rewrite (Storage.Eq.Seeds.Nonce.eq)
    .(Non_iterable_indexed_data_storage.Eq.init_value).
  simpl.
  unfold Non_iterable_indexed_data_storage.Op.init_value.
  subst level.
  rewrite H.
  simpl.
  unfold Nonce_storage.get.
  rewrite (Storage.Eq.Seeds.Nonce.eq)
    .(Non_iterable_indexed_data_storage.Eq.get).
  simpl.
  unfold Non_iterable_indexed_data_storage.Op.get.
  unfold Non_iterable_indexed_data_storage.Op.find.
  unfold Indexed_data_storage.State.Map.
  unfold Storage.Eq.Seeds.Nonce.parse.
  unfold Storage.Eq.Seeds.Nonce.apply.
  rewrite Storage.parse_apply.
  set (level := Level_storage.current _).
  now rewrite (find_apply_add_eq ctxt level
                             (Storage.Cycle.Unrevealed nonce)).
Qed.