💎 Nonce_storage.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Nonce_storage.
Require TezosOfOCaml.Proto_alpha.Storage.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Int32.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.

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.

Condition on a [Raw_context.t] and a [Level_repr.t] for a nonce to be revealable

Module Nonce_is_revealable.
  Definition t (ctxt : 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 : 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 : 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

Lemma 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 →
  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.
  rewrite (get_unrevealed_eq ctxt level status); try assumption.
  simpl.
  now rewrite H1.
Qed.

(* @TODO *)

[find . add] identity.

Fetching an added item on a context returns the same item

Axiom find_apply_add_eq
  : ∀ (ctxt : Raw_context.t)
      (level : Level_repr.t)
      (nonce_status : Storage.Seed.nonce_status),
  (Map.Make
    (Indexed_data_storage.State.Ord Storage.generic_Path_encoding))
  .(S.find) level
  (Storage.Simulation.reduce (Storage.parse ctxt)
     (Storage.Simulation.Seeds
        (Storage.Simulation.Seeds.Nonce
           (Non_iterable_indexed_data_storage.Op.add
              level nonce_status))))
  .(Storage.Simulation.seeds).(Storage.Simulation.Seeds.nonce) =
  Some (Some nonce_status).

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 e ⇒ True
  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.