Skip to main content

💾 Storage.v

Proofs

See code, Gitlab , OCaml

Proofs for all the encodings in Storage.v
Module Encoding.
The First 4 validations are focused on [UInt16], [Int32], [Int64] and [Z] all of them are related to some form of integer encoding
  Module UInt16.
    Lemma encoding_is_valid : Data_encoding.Valid.t Pervasives.UInt16.Valid.t
      Storage.Encoding.UInt16.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End UInt16.

  Module Int32.
    Lemma encoding_is_valid : Data_encoding.Valid.t Int32.Valid.t
      Storage.Encoding.Int32.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Int32.

  Module Int64.
    Lemma encoding_is_valid : Data_encoding.Valid.t Int32.Valid.t
      Storage.Encoding.Int32.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Int64.

  Module Z.
    Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True)
      Storage.Encoding.Z.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Z.

  Module Tenderbake.
    Module Branch.
The encoding [Storage.Tenderbake.Branch.encoding] is valid
      Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True)
        Storage.Tenderbake.Branch.encoding.
      Proof.
        Data_encoding.Valid.data_encoding_auto.
      Qed.
      #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
    End Branch.
  End Tenderbake.

  Module Deposits.
The encoding [Storage.Deposits.encoding] is valid
    Module Valid.
      Import TezosOfOCaml.Proto_alpha.Storage.deposits.

      Record t (x : Storage.deposits) : Prop := {
        initial_amount : Tez_repr.Valid.t x.(initial_amount);
        current_amount : Tez_repr.Valid.t x.(current_amount)
      }.
    End Valid.

    Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
      Storage.Deposits.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Deposits.

  Module Missed_endorsements_info.
The encoding [Storage.Missed_endorsements_info.encoding] is valid
    Module Valid.
      Import TezosOfOCaml.Proto_alpha.Storage.missed_endorsements_info.

      Record t (x : Storage.missed_endorsements_info) : Prop := {
        remaining_slots : Pervasives.Int31.Valid.t x.(remaining_slots);
        missed_levels : Pervasives.Int31.Valid.t x.(missed_levels)
      }.
    End Valid.

    Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
      Storage.Missed_endorsements_info.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Missed_endorsements_info.

  Module Slashed_level.
The encoding [Storage.Slashed_level.encoding] is valid
    Lemma encoding_is_valid : Data_encoding.Valid.t (fun _True)
      Storage.Slashed_level.encoding.
    Proof.
      Data_encoding.Valid.data_encoding_auto.
    Qed.
    #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
  End Slashed_level.

  Module Cycle.
    Module Public_key_with_ghost_hash.
The encoding [Storage.Cycle.public_key_with_ghost_encoding] is valid
      Module Valid.
        Definition t (x : Signature.public_key × Signature.public_key_hash) :=
          let '(public_key, public_key_hash) := x in
          public_key_hash =
          (Signature.Public_key.(SIGNATURE_PUBLIC_KEY.hash_value) public_key).
      End Valid.
    End Public_key_with_ghost_hash.

    Module Nonce_status.
The encoding [Storage.Cycle.nonce_status_encoding] is valid
      Module Valid.
        Definition t (x : Storage.Cycle.nonce_status) : Prop :=
          match x with
          | Storage.Cycle.Unrevealed _True
          | Storage.Cycle.Revealed vSeed_repr.Nonce.Valid.t v
          end.
      End Valid.

      Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
        Storage.Cycle.nonce_status_encoding.
      Proof.
        Data_encoding.Valid.data_encoding_auto.
      Qed.
      #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
    End Nonce_status.
  End Cycle.
End Encoding.

Module Cycle.
  Module Seed.
[update] is valid when the [cycle] key exists in the substore
    Lemma update_is_valid (ctxt : Proto_alpha.Raw_context.t)
      (cycle : Cycle_repr.t) (seed : Seed_repr.seed) :
      Raw_context.Valid.on
        (fun sim_ctxt
           Raw_context.Indexed_data_storage.key_exists
             cycle
             sim_ctxt
               .(Raw_context.Cycle_Seed))
        ctxt
      letP? ctxt' :=
        Storage.Cycle.Seed.(Storage_sigs.Indexed_data_storage_with_local_context.update)
          ctxt cycle seed in
      Raw_context.Valid.t ctxt'.
    Proof.
      intros H_valid_ctxt.
      Raw_context.Valid.destruct_rewrite H_valid_ctxt.
      rewrite_db storage_db.
      rewrite H_sim_ctxt_domain.
      cbn.
      unfold Storage_sigs.Indexed_map.Map; cbn.
      (* @TODO show that the added element 
         preserves the validity of the context *)

    Admitted.
  End Seed.

  Module Slashed_deposits.
The function [find_is_valid] is valid
    Lemma find_is_valid
      ctxt key subkey :
      Raw_context.Valid.t ctxt
      letP? x := Storage.Cycle.Slashed_deposits
        .(Storage_sigs.Indexed_data_storage.find)
           (ctxt, key) subkey in
      True.
    Proof.
      intros H_ctxt_valid.
      Raw_context.Valid.destruct_rewrite H_ctxt_valid.
      now rewrite_db storage_db.
    Qed.
  End Slashed_deposits.
End Cycle.

Module Seed.
[Storage.For_cycle] is a composition of [Storage.Cycle.Seed] and [Storage.Seed_status] substores.

  Module For_cycle.
[get ctxt cycle] is valid when the [cycle] key exists in the substore [Storage.Cycle.Seed]

    Lemma get_is_valid (ctxt : Proto_alpha.Raw_context.t)
      (cycle : Cycle_repr.t) :
      Raw_context.Valid.on
        (fun sim_ctxt
           Raw_context.Indexed_data_storage.key_exists
             cycle
             sim_ctxt
               .(Raw_context.Cycle_Seed))
        ctxt
      letP? _ := Storage.Seed.For_cycle.get ctxt cycle in
        True.
    Proof.
      intros H_valid_ctxt.
      unfold Storage.Seed.For_cycle.get. cbn.
      Raw_context.Valid.destruct_rewrite H_valid_ctxt.
      rewrite_db storage_db.
      red in H_sim_ctxt_domain.
      cbn in ×.
      apply Map.mem_find_not_eq_none in H_sim_ctxt_domain.
      now step.
    Qed.

[update] is valid when the [cycle] key exists in [Storage.Cycle.Seed] substore and the substore [Storage.Seed_status] is not empty
    Lemma update_is_valid (ctxt : Proto_alpha.Raw_context.t)
      (cycle : Cycle_repr.t) (seed : Seed_repr.seed)
      (seed_status : Seed_repr.seed_status) :
      Raw_context.Valid.on
        (fun sim_ctxt
           Raw_context.Indexed_data_storage.key_exists
             cycle
             sim_ctxt
               .(Raw_context.Cycle_Seed)
           ¬ Raw_context.Single_data_storage.empty
               sim_ctxt
                 .(Raw_context.Seed_status))
        ctxt
      letP? ctxt' :=
        Storage.Seed.For_cycle.update ctxt cycle seed seed_status in
      Raw_context.Valid.t ctxt'.
    Proof.
      intros H_valid_ctxt.
      Raw_context.Valid.destruct_rewrite H_valid_ctxt.
      unfold Storage.Seed.For_cycle.update.
      rewrite_db storage_db.
      destruct H_sim_ctxt_domain as [H_mem H_seed_status].
      rewrite H_mem; cbn.
      rewrite_db storage_db; cbn in ×.
      step; [|easy].
      cbn. (* show that the the updated context is valid *)
    Admitted.
  End For_cycle.

  Module VDF_Setup.
[find] is valid
    Lemma find_is_valid (ctxt : Proto_alpha.Raw_context.t) :
      Raw_context.Valid.t ctxt
      letP? x :=
         Storage.Seed.VDF_setup
           .(Storage_sigs.Single_data_storage.find) ctxt in
        True.
    Proof.
    Admitted.
  End VDF_Setup.

[get_status] is valid
  Lemma get_status_is_valid (ctxt : Proto_alpha.Raw_context.t) :
    Raw_context.Valid.t ctxt
    letP? seed_status := Storage.Seed.get_status ctxt in
    True.
  Proof.
  Admitted.
End Seed.

Module Seed_status.
[update] is valid when the substore is not empty
  Lemma update_is_valid (ctxt : Proto_alpha.Raw_context.t) value :
    Raw_context.Valid.on
      (fun sim_ctxt
         ¬ Raw_context.Single_data_storage.empty
             sim_ctxt
               .(Raw_context.Seed_status))
      ctxt
    letP? ctxt := Storage.Seed_status
       .(Storage_sigs.Single_data_storage.update) ctxt value in
    Raw_context.Valid.t ctxt.
  Proof.
    intros H_valid_ctxt.
    Raw_context.Valid.destruct_rewrite H_valid_ctxt.
    rewrite_db storage_db.
    cbn in ×.
    step; [|easy].
    cbn. (* @TODO show that the added value preserves the validity
            of the storage *)

  Admitted.
End Seed_status.

Module Slashed_deposits.
The function [find_is_valid] is valid
  Lemma find_is_valid
    ctxt key subkey :
    Raw_context.Valid.t ctxt
    letP? x := Storage.Slashed_deposits
      .(Storage_sigs.Indexed_data_storage.find)
         (ctxt, key) subkey in
    True.
  Proof.
    unfold Storage.Slashed_deposits.
    now apply Storage.Cycle.Slashed_deposits.find_is_valid.
  Qed.
End Slashed_deposits.

Module deposits.
  Module Valid.
    Import Proto_alpha.Storage.deposits.

Validity predicate for [Storage.deposits].
    Record t (x : Storage.deposits) : Prop := {
      initial_amount : Tez_repr.Valid.t x.(initial_amount);
      current_amount : Tez_repr.Valid.t x.(current_amount);
    }.
  End Valid.
End deposits.