💾 Storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Environment.V8.Proofs.Block_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_generated.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Simulations.Raw_context.
Require TezosOfOCaml.Proto_alpha.Simulations.Storage_functors.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Environment.V8.Proofs.Block_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_generated.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Simulations.Raw_context.
Require TezosOfOCaml.Proto_alpha.Simulations.Storage_functors.
Proofs for all the encodings in Storage.v
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.
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.
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.
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.
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.
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.
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 v ⇒ Seed_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.
Definition t (x : Storage.Cycle.nonce_status) : Prop :=
match x with
| Storage.Cycle.Unrevealed _ ⇒ True
| Storage.Cycle.Revealed v ⇒ Seed_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.
(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.
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.
[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.
(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.
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.
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.
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.
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.
initial_amount : Tez_repr.Valid.t x.(initial_amount);
current_amount : Tez_repr.Valid.t x.(current_amount);
}.
End Valid.
End deposits.