🖼️ Raw_context.v
Proofs
See code, See simulations, Gitlab , OCaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Error_monad.
Require TezosOfOCaml.Environment.V8.Proofs.Time.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context_intf.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Simulations.Raw_context.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Error_monad.
Require TezosOfOCaml.Environment.V8.Proofs.Time.
Require TezosOfOCaml.Proto_alpha.Proofs.Constants_parametric_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_attestation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Error.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Parameters_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Origination_nonce.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context_intf.
Require TezosOfOCaml.Proto_alpha.Proofs.Round_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Seed_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Voting_period_repr.
Require TezosOfOCaml.Proto_alpha.Simulations.Raw_context.
Predicates for a [Single_data_storage.t _] type
The store is empty
Definition empty {a : Set}
(store : Storage_sigs.Single_data_storage.t a) : Prop :=
store = None.
Arguments empty _ /.
End Single_data_storage.
(store : Storage_sigs.Single_data_storage.t a) : Prop :=
store = None.
Arguments empty _ /.
End Single_data_storage.
Predicates for a [Indexed_data_storage _ _] type
The key exists in the context
Definition key_exists {k v : Set}
{index : Path_encoding.S}
(key : k)
(map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
: Prop :=
(Storage_sigs.Indexed_map.Map index).(Map.S.mem) key map = true.
Arguments key_exists _ _ _ /.
{index : Path_encoding.S}
(key : k)
(map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
: Prop :=
(Storage_sigs.Indexed_map.Map index).(Map.S.mem) key map = true.
Arguments key_exists _ _ _ /.
The value [value] with key [key] exists in the map and satisfies the
given property [P].
Definition value_exists {k v : Set}
{index : Path_encoding.S}
(P : v → Prop)
(key : k)
(map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
: Prop :=
match (Storage_sigs.Indexed_map.Map index).(Map.S.find) key map with
| Some value ⇒ P value
| None ⇒ False
end.
Arguments value_exists _ _ _ /.
{index : Path_encoding.S}
(P : v → Prop)
(key : k)
(map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
: Prop :=
match (Storage_sigs.Indexed_map.Map index).(Map.S.find) key map with
| Some value ⇒ P value
| None ⇒ False
end.
Arguments value_exists _ _ _ /.
If value [value] with key [key] exists in the map,
then it satisfies the given the property [P].
Definition if_value_exists {k v : Set}
{index : Path_encoding.S}
(P : v → Prop)
(key : k)
(map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
: Prop :=
match (Storage_sigs.Indexed_map.Map index).(Map.S.find) key map with
| Some value ⇒ P value
| None ⇒ True
end.
Arguments if_value_exists _ _ _ /.
{index : Path_encoding.S}
(P : v → Prop)
(key : k)
(map : Map.Make_t (Storage_sigs.Indexed_map.Ord index) v)
: Prop :=
match (Storage_sigs.Indexed_map.Map index).(Map.S.find) key map with
| Some value ⇒ P value
| None ⇒ True
end.
Arguments if_value_exists _ _ _ /.
[value_exists] implies [if_value_exits]
Lemma exists_impl_if_exists {k v : Set}
{index : Path_encoding.S (t := k)}
(P : v → Prop)
(key : k)
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index) v) :
value_exists P key map →
if_value_exists P key map.
Proof.
simpl in ×.
now match goal with
| |- match ?a with _ ⇒ _ end → match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end.
Qed.
End Indexed_data_storage.
Module Nested_indexed_data_storage.
{index : Path_encoding.S (t := k)}
(P : v → Prop)
(key : k)
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index) v) :
value_exists P key map →
if_value_exists P key map.
Proof.
simpl in ×.
now match goal with
| |- match ?a with _ ⇒ _ end → match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end.
Qed.
End Indexed_data_storage.
Module Nested_indexed_data_storage.
The key and subkey exists in the context
Definition key_exists {k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
: Prop :=
Indexed_data_storage.value_exists
(fun submap ⇒
Indexed_data_storage.key_exists subkey submap)
key map.
Arguments key_exists _ _ _ /.
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
: Prop :=
Indexed_data_storage.value_exists
(fun submap ⇒
Indexed_data_storage.key_exists subkey submap)
key map.
Arguments key_exists _ _ _ /.
This is like [Indexed_data_storage.value_exists] but for nested
maps. A value of type [v] exists with [key] and [subkey], and
satisfies the given property [P]
Definition value_exists {k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
: Prop :=
Raw_context.Indexed_data_storage.value_exists
(fun submap ⇒
Raw_context.Indexed_data_storage.value_exists
(fun value ⇒ P value) subkey submap)
key map.
Arguments value_exists _ _ _ _ /.
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
: Prop :=
Raw_context.Indexed_data_storage.value_exists
(fun submap ⇒
Raw_context.Indexed_data_storage.value_exists
(fun value ⇒ P value) subkey submap)
key map.
Arguments value_exists _ _ _ _ /.
If the value [value] with key [key] and subkey [subkey] exists
in the map and submap, then it satisfies the given the
property [P].
Definition if_value_exists {k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
: Prop :=
Raw_context.Indexed_data_storage.if_value_exists
(fun submap ⇒
Raw_context.Indexed_data_storage.if_value_exists
(fun value ⇒ P value) subkey submap)
key map.
Arguments if_value_exists _ _ _ _ /.
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v))
: Prop :=
Raw_context.Indexed_data_storage.if_value_exists
(fun submap ⇒
Raw_context.Indexed_data_storage.if_value_exists
(fun value ⇒ P value) subkey submap)
key map.
Arguments if_value_exists _ _ _ _ /.
If a value exists, then a key also exists
Lemma value_exists_impl_key_exists {k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
value_exists P key subkey map →
key_exists key subkey map.
Proof.
simpl.
match goal with
| |- match ?a with _ ⇒ _ end → match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end.
step; [|easy].
apply Map.find_mem_eq in Heqo.
intros _. easy.
Qed.
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
value_exists P key subkey map →
key_exists key subkey map.
Proof.
simpl.
match goal with
| |- match ?a with _ ⇒ _ end → match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end.
step; [|easy].
apply Map.find_mem_eq in Heqo.
intros _. easy.
Qed.
If key exists then a value exists and it satisfies some
unspecified property [P]
Lemma key_exists_impl_value_exists {k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
key_exists key subkey map →
∃ P, value_exists P key subkey map.
Proof.
simpl. intros H. eexists.
match type of H with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end
end.
step.
{ instantiate (1 := fun _ ⇒ True). simpl. trivial. }
{ apply Map.find_eq_none_implies_mem_eq_false in Heqo.
match goal with
| H : ?a subkey m = true,
H' : ?b subkey m = false |- _ ⇒
change b with a in H'; rewrite H' in H;
discriminate
end.
}
Qed.
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
key_exists key subkey map →
∃ P, value_exists P key subkey map.
Proof.
simpl. intros H. eexists.
match type of H with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end
end.
step.
{ instantiate (1 := fun _ ⇒ True). simpl. trivial. }
{ apply Map.find_eq_none_implies_mem_eq_false in Heqo.
match goal with
| H : ?a subkey m = true,
H' : ?b subkey m = false |- _ ⇒
change b with a in H'; rewrite H' in H;
discriminate
end.
}
Qed.
If you have a [key_exists k k' m] and a [if_value_exists P k k' m] you
can deduce [value_exists P k k' m]
Lemma key_exists_and_if_value_exists_impl_value_exists {k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(key : k) (subkey : k') (P : v → Prop)
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
key_exists key subkey map →
if_value_exists P key subkey map →
value_exists P key subkey map.
Proof.
simpl.
step; cbn; [|easy].
intros H_mem.
step; cbn; [easy|].
apply Map.find_eq_none_implies_mem_eq_false in Heqo0.
match type of H_mem with
| ?a subkey m = true ⇒
match type of Heqo0 with
| ?b subkey m = false ⇒
change b with a in *;
now rewrite H_mem in Heqo0
end
end.
Qed.
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(key : k) (subkey : k') (P : v → Prop)
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
key_exists key subkey map →
if_value_exists P key subkey map →
value_exists P key subkey map.
Proof.
simpl.
step; cbn; [|easy].
intros H_mem.
step; cbn; [easy|].
apply Map.find_eq_none_implies_mem_eq_false in Heqo0.
match type of H_mem with
| ?a subkey m = true ⇒
match type of Heqo0 with
| ?b subkey m = false ⇒
change b with a in *;
now rewrite H_mem in Heqo0
end
end.
Qed.
[value_exists] implies [if_value_exists]
Lemma exists_impl_if_exists {k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
value_exists P key subkey map →
if_value_exists P key subkey map.
Proof.
simpl in ×.
match goal with
| |- match ?a with _ ⇒ _ end → match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end.
now step.
Qed.
End Nested_indexed_data_storage.
Module Tenderbake.
Import Raw_context.
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
(P : v → Prop)
(key : k) (subkey : k')
(map :
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)) :
value_exists P key subkey map →
if_value_exists P key subkey map.
Proof.
simpl in ×.
match goal with
| |- match ?a with _ ⇒ _ end → match ?b with _ ⇒ _ end ⇒
change b with a; destruct a; simpl; [|contradiction]
end.
now step.
Qed.
End Nested_indexed_data_storage.
Module Tenderbake.
Import Raw_context.
Validity for the [Tenderbake] sub-store.
Module Valid.
Record t (x : Raw_context.t) : Prop := {
First_level_of_protocol : x.(Tenderbake_First_level_of_protocol) ≠ None;
}.
End Valid.
End Tenderbake.
Module Vote.
Import Raw_context.
Record t (x : Raw_context.t) : Prop := {
First_level_of_protocol : x.(Tenderbake_First_level_of_protocol) ≠ None;
}.
End Valid.
End Tenderbake.
Module Vote.
Import Raw_context.
Validity for the [Vote] sub-store.
Module Valid.
Record t (x : Raw_context.t) : Prop := {
Current_period :
match x.(Vote_Current_period) with
| Some period ⇒ Voting_period_repr.Valid.t period
| None ⇒ False
end;
Pred_period_kind : x.(Vote_Pred_period_kind) ≠ None;
}.
End Valid.
End Vote.
Module Sc_rollup_Commitment_added.
Import Raw_context_generated.
Record t (x : Raw_context.t) : Prop := {
Current_period :
match x.(Vote_Current_period) with
| Some period ⇒ Voting_period_repr.Valid.t period
| None ⇒ False
end;
Pred_period_kind : x.(Vote_Pred_period_kind) ≠ None;
}.
End Valid.
End Vote.
Module Sc_rollup_Commitment_added.
Import Raw_context_generated.
If a [commitment : Sc_rollup_commitment_repr.V1.t] exists in
the context, then it is valid
Module Valid.
Definition t
(commitment_added_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
Sc_rollup_commitment_repr.Hash.Path_encoding_Make_hex_include
Raw_level_repr.t))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Raw_level_repr.Valid.t rollup index
commitment_added_projection.
End Valid.
End Sc_rollup_Commitment_added.
Module Sc_rollup_Commitments.
Import Raw_context_generated.
Definition t
(commitment_added_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
Sc_rollup_commitment_repr.Hash.Path_encoding_Make_hex_include
Raw_level_repr.t))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Raw_level_repr.Valid.t rollup index
commitment_added_projection.
End Valid.
End Sc_rollup_Commitment_added.
Module Sc_rollup_Commitments.
Import Raw_context_generated.
If a [commitment : Sc_rollup_commitment_repr.V1.t] exists in the
context, then it is valid
Module Valid.
Definition t
(commitment_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
Sc_rollup_commitment_repr.Hash.Path_encoding_Make_hex_include
Sc_rollup_commitment_repr.t))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Sc_rollup_commitment_repr.V1.Valid.t rollup index
commitment_projection.
End Valid.
End Sc_rollup_Commitments.
Module Sc_rollup_Game.
Import Raw_context_generated.
Definition t
(commitment_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
Sc_rollup_commitment_repr.Hash.Path_encoding_Make_hex_include
Sc_rollup_commitment_repr.t))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Sc_rollup_commitment_repr.V1.Valid.t rollup index
commitment_projection.
End Valid.
End Sc_rollup_Commitments.
Module Sc_rollup_Game.
Import Raw_context_generated.
If a [game : Sc_rollup_game_repr.t] exists in the context,
then it is valid
Module Valid.
Definition t
(game_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
(of_functors_index
Sc_rollup_Game_versioned_and_timeout_Index)
Sc_rollup_game_repr.t))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup
index
game_projection.
End Valid.
End Sc_rollup_Game.
Module Sc_rollup_Game_timeout.
Import Raw_context_generated.
Definition t
(game_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
(of_functors_index
Sc_rollup_Game_versioned_and_timeout_Index)
Sc_rollup_game_repr.t))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup
index
game_projection.
End Valid.
End Sc_rollup_Game.
Module Sc_rollup_Game_timeout.
Import Raw_context_generated.
If [game_timeout : Sc_rollup_game_repr.timeout] exists in the
context, then it valid
Module Valid.
Definition t
(game_timeout_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
(of_functors_index
Sc_rollup_Game_versioned_and_timeout_Index)
Sc_rollup_game_repr.timeout))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Sc_rollup_game_repr.timeout.Valid.t
rollup
index
game_timeout_projection.
End Valid.
End Sc_rollup_Game_timeout.
Definition t
(game_timeout_projection : Storage_sigs.Indexed_map.t
(of_description_index Sc_rollup_repr.Index)
(Storage_sigs.Indexed_data_storage.t
(of_functors_index
Sc_rollup_Game_versioned_and_timeout_Index)
Sc_rollup_game_repr.timeout))
: Prop :=
∀ rollup index,
Nested_indexed_data_storage.if_value_exists
Sc_rollup_game_repr.timeout.Valid.t
rollup
index
game_timeout_projection.
End Valid.
End Sc_rollup_Game_timeout.
Reading a value from the empty context always return [None].
Axiom find_empty_context : ∀ (k : key),
Context.find Raw_context.empty_context k = None.
#[local] Open Scope list.
Module consensus_pk.
Module Valid.
Import Proto_alpha.Raw_context.consensus_pk.
Context.find Raw_context.empty_context k = None.
#[local] Open Scope list.
Module consensus_pk.
Module Valid.
Import Proto_alpha.Raw_context.consensus_pk.
Validity predicate for [consensus_pk].
Record t (x : Raw_context.consensus_pk) : Prop := {
consensus_pkh :
x.(consensus_pkh) =
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
x.(consensus_pk);
}.
End Valid.
End consensus_pk.
consensus_pkh :
x.(consensus_pkh) =
Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value)
x.(consensus_pk);
}.
End Valid.
End consensus_pk.
The encoding [consensus_pk_encoding] is valid.
Lemma consensus_pk_encoding_is_valid :
Data_encoding.Valid.t consensus_pk.Valid.t Raw_context.consensus_pk_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; simpl in ×.
step.
{ assert (consensus_pkh = delegate). {
destruct Signature.Included_SIGNATURE_is_valid.
destruct Public_key_hash.
destruct Compare_S0.
destruct is_Make.
rewrite equal in Heqb; simpl in Heqb.
apply Signature.Included_SIGNATURE_is_valid; trivial; simpl.
lia.
}
sfirstorder.
}
{ sfirstorder. }
Qed.
#[global] Hint Resolve consensus_pk_encoding_is_valid : Data_encoding_db.
Module Raw_consensus.
Data_encoding.Valid.t consensus_pk.Valid.t Raw_context.consensus_pk_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [] []; simpl in ×.
step.
{ assert (consensus_pkh = delegate). {
destruct Signature.Included_SIGNATURE_is_valid.
destruct Public_key_hash.
destruct Compare_S0.
destruct is_Make.
rewrite equal in Heqb; simpl in Heqb.
apply Signature.Included_SIGNATURE_is_valid; trivial; simpl.
lia.
}
sfirstorder.
}
{ sfirstorder. }
Qed.
#[global] Hint Resolve consensus_pk_encoding_is_valid : Data_encoding_db.
Module Raw_consensus.
Validity predicate for [Raw_consensus.t].
Module Valid.
Import Raw_context.Raw_consensus.t.
Record t (x : Raw_context.Raw_consensus.t) : Prop := {
current_endorsement_power :
Pervasives.Int.Valid.t x.(current_endorsement_power);
locked_round_evidence :
Option.Forall
(fun '(round, power) ⇒
Round_repr.Valid.t round ∧ Pervasives.Int.Valid.t power
)
x.(locked_round_evidence);
preendorsements_quorum_round :
Option.Forall Round_repr.Valid.t x.(preendorsements_quorum_round);
}.
End Valid.
Import Raw_context.Raw_consensus.t.
Record t (x : Raw_context.Raw_consensus.t) : Prop := {
current_endorsement_power :
Pervasives.Int.Valid.t x.(current_endorsement_power);
locked_round_evidence :
Option.Forall
(fun '(round, power) ⇒
Round_repr.Valid.t round ∧ Pervasives.Int.Valid.t power
)
x.(locked_round_evidence);
preendorsements_quorum_round :
Option.Forall Round_repr.Valid.t x.(preendorsements_quorum_round);
}.
End Valid.
The function [initialize_with_endorsements_and_preendorsements] is
valid.
Lemma initialize_with_endorsements_and_preendorsements_is_valid
allowed_endorsements allowed_preendorsements t_value
(H_t_value : Valid.t t_value) :
Valid.t (
Raw_context.Raw_consensus.initialize_with_endorsements_and_preendorsements
allowed_endorsements allowed_preendorsements t_value
).
Proof.
sauto lq: on.
Qed.
End Raw_consensus.
Module config.
Module Valid.
Import Simulations.Raw_context_aux.config.
allowed_endorsements allowed_preendorsements t_value
(H_t_value : Valid.t t_value) :
Valid.t (
Raw_context.Raw_consensus.initialize_with_endorsements_and_preendorsements
allowed_endorsements allowed_preendorsements t_value
).
Proof.
sauto lq: on.
Qed.
End Raw_consensus.
Module config.
Module Valid.
Import Simulations.Raw_context_aux.config.
Validity predicate for the simulation of [Raw_context.back].
Record simulation (x : Simulations.Raw_context_aux.config) : Prop := {
constants :
Constants_parametric_repr.Valid.t x.(constants);
round_durations : Round_repr.Durations.Valid.t x.(round_durations);
cycle_eras : Level_repr.Cycle_eras.Valid.t x.(cycle_eras);
level : Level_repr.Valid.t x.(level);
predecessor_timestamp : Time.Valid.t x.(predecessor_timestamp);
timestamp : Time.Valid.t x.(timestamp);
fees : Tez_repr.Valid.t x.(fees);
origination_nonce :
Option.Forall Origination_nonce.Valid.t x.(origination_nonce);
internal_nonce : Pervasives.Int.Valid.t x.(internal_nonce);
internal_nonces_used :
List.Forall Pervasives.Int.Valid.t (
Raw_context.Int_set.(_Set.S.elements)
x.(internal_nonces_used)
);
remaining_block_gas :
Saturation_repr.Valid.t x.(remaining_block_gas);
consensus : Raw_consensus.Valid.t x.(consensus);
stake_distribution_for_current_cycle :
x.(stake_distribution_for_current_cycle) ≠ None;
dal_attestation_slot_accountability :
Dal_attestation_repr.Accountability.Valid.t
x.(dal_attestation_slot_accountability);
}.
End Valid.
End config.
Module standalone.
constants :
Constants_parametric_repr.Valid.t x.(constants);
round_durations : Round_repr.Durations.Valid.t x.(round_durations);
cycle_eras : Level_repr.Cycle_eras.Valid.t x.(cycle_eras);
level : Level_repr.Valid.t x.(level);
predecessor_timestamp : Time.Valid.t x.(predecessor_timestamp);
timestamp : Time.Valid.t x.(timestamp);
fees : Tez_repr.Valid.t x.(fees);
origination_nonce :
Option.Forall Origination_nonce.Valid.t x.(origination_nonce);
internal_nonce : Pervasives.Int.Valid.t x.(internal_nonce);
internal_nonces_used :
List.Forall Pervasives.Int.Valid.t (
Raw_context.Int_set.(_Set.S.elements)
x.(internal_nonces_used)
);
remaining_block_gas :
Saturation_repr.Valid.t x.(remaining_block_gas);
consensus : Raw_consensus.Valid.t x.(consensus);
stake_distribution_for_current_cycle :
x.(stake_distribution_for_current_cycle) ≠ None;
dal_attestation_slot_accountability :
Dal_attestation_repr.Accountability.Valid.t
x.(dal_attestation_slot_accountability);
}.
End Valid.
End config.
Module standalone.
The validity predicate for the
[Simulations.Raw_context.standalone] type
Module Valid.
Import Simulations.Raw_context_aux.standalone.
Record simulation (x : Simulations.Raw_context_aux.standalone) : Prop := {
cycle_eras : Level_repr.Cycle_eras.Valid.t x.(cycle_eras);
constants : Constants_parametric_repr.Valid.t x.(constants);
protocol_param :
Option.Forall Parameters_repr.Valid.t x.(protocol_param);
}.
End Valid.
End standalone.
Import Simulations.Raw_context_aux.standalone.
Record simulation (x : Simulations.Raw_context_aux.standalone) : Prop := {
cycle_eras : Level_repr.Cycle_eras.Valid.t x.(cycle_eras);
constants : Constants_parametric_repr.Valid.t x.(constants);
protocol_param :
Option.Forall Parameters_repr.Valid.t x.(protocol_param);
}.
End Valid.
End standalone.
The validity predicate for the [Simulations.Raw_context.t] type
Module Valid.
Import Simulations.Raw_context.
Record simulation (x : Simulations.Raw_context.t) : Prop := {
config : config.Valid.simulation x.(config);
standalone : standalone.Valid.simulation x.(standalone);
Tenderbake : Tenderbake.Valid.t x;
Vote : Vote.Valid.t x;
Sc_rollup_Commitment_added :
Sc_rollup_Commitment_added.Valid.t
x.(Sc_rollup_Commitment_added);
Sc_rollup_Commitments :
Sc_rollup_Commitments.Valid.t x.(Sc_rollup_Commitments);
Sc_rollup_Game : Sc_rollup_Game.Valid.t x.(Sc_rollup_Game);
Sc_rollup_Game_timeout :
Sc_rollup_Game_timeout.Valid.t x.(Sc_rollup_Game_timeout);
}.
Import Simulations.Raw_context.
Record simulation (x : Simulations.Raw_context.t) : Prop := {
config : config.Valid.simulation x.(config);
standalone : standalone.Valid.simulation x.(standalone);
Tenderbake : Tenderbake.Valid.t x;
Vote : Vote.Valid.t x;
Sc_rollup_Commitment_added :
Sc_rollup_Commitment_added.Valid.t
x.(Sc_rollup_Commitment_added);
Sc_rollup_Commitments :
Sc_rollup_Commitments.Valid.t x.(Sc_rollup_Commitments);
Sc_rollup_Game : Sc_rollup_Game.Valid.t x.(Sc_rollup_Game);
Sc_rollup_Game_timeout :
Sc_rollup_Game_timeout.Valid.t x.(Sc_rollup_Game_timeout);
}.
Validity predicate for [Raw_context.t] with a specific domain.
Definition on (domain : Simulations.Raw_context.t → Prop)
(ctxt : Proto_alpha.Raw_context.t) : Prop :=
∃ sim_ctxt : Simulations.Raw_context.t,
ctxt = Raw_context.to_t sim_ctxt ∧
simulation sim_ctxt ∧
domain sim_ctxt.
(ctxt : Proto_alpha.Raw_context.t) : Prop :=
∃ sim_ctxt : Simulations.Raw_context.t,
ctxt = Raw_context.to_t sim_ctxt ∧
simulation sim_ctxt ∧
domain sim_ctxt.
Validity predicate for [Raw_context.t].
Open the validity hypothesis about a context and do some rewrites.
Ltac destruct_rewrite H :=
let sim_ctxt := fresh "sim_ctxt" in
let H_sim_ctxt_eq := fresh "H_sim_ctxt_eq" in
let H_sim_ctxt := fresh "H_sim_ctxt" in
let H_sim_ctxt_domain := fresh "H_sim_ctxt_domain" in
let H_eq := fresh "H_eq" in
(* We use [eqn:] to keep the hypothesis [H] alive *)
destruct H
as [sim_ctxt [H_sim_ctxt_eq [H_sim_ctxt H_sim_ctxt_domain]]] eqn:H_eq;
clear H_eq;
rewrite H_sim_ctxt_eq in ×.
End Valid.
let sim_ctxt := fresh "sim_ctxt" in
let H_sim_ctxt_eq := fresh "H_sim_ctxt_eq" in
let H_sim_ctxt := fresh "H_sim_ctxt" in
let H_sim_ctxt_domain := fresh "H_sim_ctxt_domain" in
let H_eq := fresh "H_eq" in
(* We use [eqn:] to keep the hypothesis [H] alive *)
destruct H
as [sim_ctxt [H_sim_ctxt_eq [H_sim_ctxt H_sim_ctxt_domain]]] eqn:H_eq;
clear H_eq;
rewrite H_sim_ctxt_eq in ×.
End Valid.
A lemma to help find a simulation from a raw context.
Lemma to_t_inversion
remaining_operation_gas standalone constants round_durations
cycle_eras level predecessor_timestamp timestamp fees origination_nonce
temporary_lazy_storage_ids internal_nonce internal_nonces_used
remaining_block_gas unlimited_operation_gas consensus
non_consensus_operations_rev dictator_proposal_seen sampler_state
stake_distribution_for_current_cycle tx_rollup_current_messages
sc_rollup_current_messages dal_slot_fee_market dal_attestation_slot_accountability
dal_committee sim_ctxt :
{|
Proto_alpha.Raw_context.t.remaining_operation_gas :=
remaining_operation_gas;
Proto_alpha.Raw_context.t.back :=
{|
Proto_alpha.Raw_context.back.context := Raw_context.to_context standalone;
Proto_alpha.Raw_context.back.constants := constants;
Proto_alpha.Raw_context.back.round_durations := round_durations;
Proto_alpha.Raw_context.back.cycle_eras := cycle_eras;
Proto_alpha.Raw_context.back.level := level;
Proto_alpha.Raw_context.back.predecessor_timestamp :=
predecessor_timestamp;
Proto_alpha.Raw_context.back.timestamp := timestamp;
Proto_alpha.Raw_context.back.fees := fees;
Proto_alpha.Raw_context.back.origination_nonce := origination_nonce;
Proto_alpha.Raw_context.back.temporary_lazy_storage_ids :=
temporary_lazy_storage_ids;
Proto_alpha.Raw_context.back.internal_nonce := internal_nonce;
Proto_alpha.Raw_context.back.internal_nonces_used :=
internal_nonces_used;
Proto_alpha.Raw_context.back.remaining_block_gas := remaining_block_gas;
Proto_alpha.Raw_context.back.unlimited_operation_gas :=
unlimited_operation_gas;
Proto_alpha.Raw_context.back.consensus := consensus;
Proto_alpha.Raw_context.back.non_consensus_operations_rev :=
non_consensus_operations_rev;
Proto_alpha.Raw_context.back.dictator_proposal_seen :=
dictator_proposal_seen;
Proto_alpha.Raw_context.back.sampler_state := sampler_state;
Proto_alpha.Raw_context.back.stake_distribution_for_current_cycle :=
stake_distribution_for_current_cycle;
Proto_alpha.Raw_context.back.tx_rollup_current_messages :=
tx_rollup_current_messages;
Proto_alpha.Raw_context.back.sc_rollup_current_messages :=
sc_rollup_current_messages;
Proto_alpha.Raw_context.back.dal_slot_fee_market := dal_slot_fee_market;
Proto_alpha.Raw_context.back.dal_attestation_slot_accountability :=
dal_attestation_slot_accountability;
Proto_alpha.Raw_context.back.dal_committee := dal_committee;
|}
|} =
Raw_context.to_t {|
Raw_context.config := {|
Raw_context_aux.config.remaining_operation_gas :=
remaining_operation_gas;
Raw_context_aux.config.constants := constants;
Raw_context_aux.config.round_durations := round_durations;
Raw_context_aux.config.cycle_eras := cycle_eras;
Raw_context_aux.config.level := level;
Raw_context_aux.config.predecessor_timestamp :=
predecessor_timestamp;
Raw_context_aux.config.timestamp := timestamp;
Raw_context_aux.config.fees := fees;
Raw_context_aux.config.origination_nonce := origination_nonce;
Raw_context_aux.config.temporary_lazy_storage_ids :=
temporary_lazy_storage_ids;
Raw_context_aux.config.internal_nonce := internal_nonce;
Raw_context_aux.config.internal_nonces_used :=
internal_nonces_used;
Raw_context_aux.config.remaining_block_gas := remaining_block_gas;
Raw_context_aux.config.unlimited_operation_gas :=
unlimited_operation_gas;
Raw_context_aux.config.consensus := consensus;
Raw_context_aux.config.non_consensus_operations_rev :=
non_consensus_operations_rev;
Raw_context_aux.config.dictator_proposal_seen :=
dictator_proposal_seen;
Raw_context_aux.config.sampler_state := sampler_state;
Raw_context_aux.config.stake_distribution_for_current_cycle :=
stake_distribution_for_current_cycle;
Raw_context_aux.config.tx_rollup_current_messages :=
tx_rollup_current_messages;
Raw_context_aux.config.sc_rollup_current_messages :=
sc_rollup_current_messages;
Raw_context_aux.config.dal_slot_fee_market :=
dal_slot_fee_market;
Raw_context_aux.config.dal_attestation_slot_accountability :=
dal_attestation_slot_accountability;
Raw_context_aux.config.dal_committee :=
dal_committee;
|};
Raw_context.standalone := standalone;
Raw_context.Block_round := sim_ctxt.(Raw_context.Block_round);
Raw_context.Tenderbake_First_level_of_protocol :=
sim_ctxt.(Raw_context.Tenderbake_First_level_of_protocol);
Raw_context.Tenderbake_Endorsement_branch :=
sim_ctxt.(Raw_context.Tenderbake_Endorsement_branch);
Raw_context.Tenderbake_Grand_parent_branch :=
sim_ctxt.(Raw_context.Tenderbake_Grand_parent_branch);
Raw_context.Contract_Global_counter :=
sim_ctxt.(Raw_context.Contract_Global_counter);
Raw_context.Contract_Spendable_balance :=
sim_ctxt.(Raw_context.Contract_Spendable_balance);
Raw_context.Contract_Missed_endorsements :=
sim_ctxt.(Raw_context.Contract_Missed_endorsements);
Raw_context.Contract_Manager :=
sim_ctxt.(Raw_context.Contract_Manager);
Raw_context.Contract_Consensus_key :=
sim_ctxt.(Raw_context.Contract_Consensus_key);
Raw_context.Contract_Pending_consensus_keys :=
sim_ctxt.(Raw_context.Contract_Pending_consensus_keys);
Raw_context.Contract_Delegate :=
sim_ctxt.(Raw_context.Contract_Delegate);
Raw_context.Contract_Inactive_delegate :=
sim_ctxt.(Raw_context.Contract_Inactive_delegate);
Raw_context.Contract_Delegate_last_cycle_before_deactivation :=
sim_ctxt
.(Raw_context.Contract_Delegate_last_cycle_before_deactivation);
Raw_context.Contract_Delegated :=
sim_ctxt.(Raw_context.Contract_Delegated);
Raw_context.Contract_Counter :=
sim_ctxt.(Raw_context.Contract_Counter);
Raw_context.Contract_Code :=
sim_ctxt.(Raw_context.Contract_Code);
Raw_context.Contract_Storage :=
sim_ctxt.(Raw_context.Contract_Storage);
Raw_context.Contract_Paid_storage_space :=
sim_ctxt.(Raw_context.Contract_Paid_storage_space);
Raw_context.Contract_Used_storage_space :=
sim_ctxt.(Raw_context.Contract_Used_storage_space);
Raw_context.Contract_Frozen_deposits :=
sim_ctxt.(Raw_context.Contract_Frozen_deposits);
Raw_context.Contract_Frozen_bonds :=
sim_ctxt.(Raw_context.Contract_Frozen_bonds);
Raw_context.Contract_Total_frozen_bonds :=
sim_ctxt.(Raw_context.Contract_Total_frozen_bonds);
Raw_context.Global_constants_Map :=
sim_ctxt.(Raw_context.Global_constants_Map);
Raw_context.Big_map_Next_Storage :=
sim_ctxt.(Raw_context.Big_map_Next_Storage);
Raw_context.Big_map_Total_bytes :=
sim_ctxt.(Raw_context.Big_map_Total_bytes);
Raw_context.Big_map_Key_type :=
sim_ctxt.(Raw_context.Big_map_Key_type);
Raw_context.Big_map_Value_type :=
sim_ctxt.(Raw_context.Big_map_Value_type);
Raw_context.Big_map_Contents :=
sim_ctxt.(Raw_context.Big_map_Contents);
Raw_context.Sapling_Next_Storage :=
sim_ctxt.(Raw_context.Sapling_Next_Storage);
Raw_context.Sapling_Total_bytes :=
sim_ctxt.(Raw_context.Sapling_Total_bytes);
Raw_context.Sapling_Commitments_size :=
sim_ctxt.(Raw_context.Sapling_Commitments_size);
Raw_context.Sapling_Memo_size :=
sim_ctxt.(Raw_context.Sapling_Memo_size);
Raw_context.Sapling_Commitments :=
sim_ctxt.(Raw_context.Sapling_Commitments);
Raw_context.Sapling_Ciphertexts :=
sim_ctxt.(Raw_context.Sapling_Ciphertexts);
Raw_context.Sapling_Nullifiers_size :=
sim_ctxt.(Raw_context.Sapling_Nullifiers_size);
Raw_context.Sapling_Nullifiers_ordered :=
sim_ctxt.(Raw_context.Sapling_Nullifiers_ordered);
Raw_context.Sapling_Nullifiers_hashed :=
sim_ctxt.(Raw_context.Sapling_Nullifiers_hashed);
Raw_context.Sapling_Roots :=
sim_ctxt.(Raw_context.Sapling_Roots);
Raw_context.Sapling_Roots_pos :=
sim_ctxt.(Raw_context.Sapling_Roots_pos);
Raw_context.Sapling_Roots_level :=
sim_ctxt.(Raw_context.Sapling_Roots_level);
Raw_context.Delegates :=
sim_ctxt.(Raw_context.Delegates);
Raw_context.Consensus_keys :=
sim_ctxt.(Raw_context.Consensus_keys);
Raw_context.Cycle_Slashed_deposits :=
sim_ctxt.(Raw_context.Cycle_Slashed_deposits);
Raw_context.Cycle_Selected_stake_distribution :=
sim_ctxt.(Raw_context.Cycle_Selected_stake_distribution);
Raw_context.Cycle_Total_active_stake :=
sim_ctxt.(Raw_context.Cycle_Total_active_stake);
Raw_context.Cycle_Delegate_sampler_state :=
sim_ctxt.(Raw_context.Cycle_Delegate_sampler_state);
Raw_context.Cycle_Nonce :=
sim_ctxt.(Raw_context.Cycle_Nonce);
Raw_context.Cycle_Seed :=
sim_ctxt.(Raw_context.Cycle_Seed);
Raw_context.Stake_Staking_balance :=
sim_ctxt.(Raw_context.Stake_Staking_balance);
Raw_context.Stake_Active_delegates_with_minimal_stake :=
sim_ctxt.(Raw_context.Stake_Active_delegates_with_minimal_stake);
Raw_context.Stake_Last_snapshot :=
sim_ctxt.(Raw_context.Stake_Last_snapshot);
Raw_context.Vote_Pred_period_kind :=
sim_ctxt.(Raw_context.Vote_Pred_period_kind);
Raw_context.Vote_Current_period :=
sim_ctxt.(Raw_context.Vote_Current_period);
Raw_context.Vote_Participation_ema :=
sim_ctxt.(Raw_context.Vote_Participation_ema);
Raw_context.Vote_Current_proposal :=
sim_ctxt.(Raw_context.Vote_Current_proposal);
Raw_context.Vote_Voting_power_in_listings :=
sim_ctxt.(Raw_context.Vote_Voting_power_in_listings);
Raw_context.Vote_Listings :=
sim_ctxt.(Raw_context.Vote_Listings);
Raw_context.Vote_Proposals :=
sim_ctxt.(Raw_context.Vote_Proposals);
Raw_context.Vote_Proposals_count :=
sim_ctxt.(Raw_context.Vote_Proposals_count);
Raw_context.Vote_Ballots :=
sim_ctxt.(Raw_context.Vote_Ballots);
Raw_context.Seed_status :=
sim_ctxt.(Raw_context.Seed_status);
Raw_context.Seed_VDF_setup :=
sim_ctxt.(Raw_context.Seed_VDF_setup);
Raw_context.Commitments :=
sim_ctxt.(Raw_context.Commitments);
Raw_context.Ramp_up_Rewards :=
sim_ctxt.(Raw_context.Ramp_up_Rewards);
Raw_context.Pending_migration_Balance_updates :=
sim_ctxt.(Raw_context.Pending_migration_Balance_updates);
Raw_context.Pending_migration_Operation_results :=
sim_ctxt.(Raw_context.Pending_migration_Operation_results);
Raw_context.Liquidity_baking_Toggle_ema :=
sim_ctxt.(Raw_context.Liquidity_baking_Toggle_ema);
Raw_context.Liquidity_baking_Cpmm_address :=
sim_ctxt.(Raw_context.Liquidity_baking_Cpmm_address);
Raw_context.Ticket_balance_Paid_storage_space :=
sim_ctxt.(Raw_context.Ticket_balance_Paid_storage_space);
Raw_context.Ticket_balance_Used_storage_space :=
sim_ctxt.(Raw_context.Ticket_balance_Used_storage_space);
Raw_context.Ticket_balance_Table :=
sim_ctxt.(Raw_context.Ticket_balance_Table);
Raw_context.Tx_rollup_State :=
sim_ctxt.(Raw_context.Tx_rollup_State);
Raw_context.Tx_rollup_Inbox :=
sim_ctxt.(Raw_context.Tx_rollup_Inbox);
Raw_context.Tx_rollup_Revealed_withdrawals :=
sim_ctxt.(Raw_context.Tx_rollup_Revealed_withdrawals);
Raw_context.Tx_rollup_Commitment :=
sim_ctxt.(Raw_context.Tx_rollup_Commitment);
Raw_context.Tx_rollup_Commitment_bond :=
sim_ctxt.(Raw_context.Tx_rollup_Commitment_bond);
Raw_context.Sc_rollup_PVM_kind :=
sim_ctxt.(Raw_context.Sc_rollup_PVM_kind);
Raw_context.Sc_rollup_Parameters_type :=
sim_ctxt.(Raw_context.Sc_rollup_Parameters_type);
Raw_context.Sc_rollup_Genesis_info :=
sim_ctxt.(Raw_context.Sc_rollup_Genesis_info);
Raw_context.Sc_rollup_Inbox :=
sim_ctxt.(Raw_context.Sc_rollup_Inbox);
Raw_context.Sc_rollup_Last_cemented_commitment :=
sim_ctxt.(Raw_context.Sc_rollup_Last_cemented_commitment);
Raw_context.Sc_rollup_Stakers :=
sim_ctxt.(Raw_context.Sc_rollup_Stakers);
Raw_context.Sc_rollup_Staker_count :=
sim_ctxt.(Raw_context.Sc_rollup_Staker_count);
Raw_context.Sc_rollup_Commitments :=
sim_ctxt.(Raw_context.Sc_rollup_Commitments);
Raw_context.Sc_rollup_Commitment_stake_count :=
sim_ctxt.(Raw_context.Sc_rollup_Commitment_stake_count);
Raw_context.Sc_rollup_Commitment_first_publication_level :=
sim_ctxt.(Raw_context.Sc_rollup_Commitment_first_publication_level);
Raw_context.Sc_rollup_Commitment_added :=
sim_ctxt.(Raw_context.Sc_rollup_Commitment_added);
Raw_context.Sc_rollup_Game_versioned :=
sim_ctxt.(Raw_context.Sc_rollup_Game_versioned);
Raw_context.Sc_rollup_Game :=
sim_ctxt.(Raw_context.Sc_rollup_Game);
Raw_context.Sc_rollup_Game_timeout :=
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout);
Raw_context.Sc_rollup_Opponent :=
sim_ctxt.(Raw_context.Sc_rollup_Opponent);
Raw_context.Sc_rollup_Applied_outbox_messages :=
sim_ctxt.(Raw_context.Sc_rollup_Applied_outbox_messages);
Raw_context.Dal_Slot_Headers :=
sim_ctxt.(Raw_context.Dal_Slot_Headers);
Raw_context.Dal_Slot_History :=
sim_ctxt.(Raw_context.Dal_Slot_History);
Raw_context.Zk_rollup_Account :=
sim_ctxt.(Raw_context.Zk_rollup_Account);
Raw_context.Zk_rollup_Pending_list :=
sim_ctxt.(Raw_context.Zk_rollup_Pending_list);
Raw_context.Zk_rollup_Pending_operation :=
sim_ctxt.(Raw_context.Zk_rollup_Pending_operation);
|}.
Proof.
reflexivity.
Qed.
remaining_operation_gas standalone constants round_durations
cycle_eras level predecessor_timestamp timestamp fees origination_nonce
temporary_lazy_storage_ids internal_nonce internal_nonces_used
remaining_block_gas unlimited_operation_gas consensus
non_consensus_operations_rev dictator_proposal_seen sampler_state
stake_distribution_for_current_cycle tx_rollup_current_messages
sc_rollup_current_messages dal_slot_fee_market dal_attestation_slot_accountability
dal_committee sim_ctxt :
{|
Proto_alpha.Raw_context.t.remaining_operation_gas :=
remaining_operation_gas;
Proto_alpha.Raw_context.t.back :=
{|
Proto_alpha.Raw_context.back.context := Raw_context.to_context standalone;
Proto_alpha.Raw_context.back.constants := constants;
Proto_alpha.Raw_context.back.round_durations := round_durations;
Proto_alpha.Raw_context.back.cycle_eras := cycle_eras;
Proto_alpha.Raw_context.back.level := level;
Proto_alpha.Raw_context.back.predecessor_timestamp :=
predecessor_timestamp;
Proto_alpha.Raw_context.back.timestamp := timestamp;
Proto_alpha.Raw_context.back.fees := fees;
Proto_alpha.Raw_context.back.origination_nonce := origination_nonce;
Proto_alpha.Raw_context.back.temporary_lazy_storage_ids :=
temporary_lazy_storage_ids;
Proto_alpha.Raw_context.back.internal_nonce := internal_nonce;
Proto_alpha.Raw_context.back.internal_nonces_used :=
internal_nonces_used;
Proto_alpha.Raw_context.back.remaining_block_gas := remaining_block_gas;
Proto_alpha.Raw_context.back.unlimited_operation_gas :=
unlimited_operation_gas;
Proto_alpha.Raw_context.back.consensus := consensus;
Proto_alpha.Raw_context.back.non_consensus_operations_rev :=
non_consensus_operations_rev;
Proto_alpha.Raw_context.back.dictator_proposal_seen :=
dictator_proposal_seen;
Proto_alpha.Raw_context.back.sampler_state := sampler_state;
Proto_alpha.Raw_context.back.stake_distribution_for_current_cycle :=
stake_distribution_for_current_cycle;
Proto_alpha.Raw_context.back.tx_rollup_current_messages :=
tx_rollup_current_messages;
Proto_alpha.Raw_context.back.sc_rollup_current_messages :=
sc_rollup_current_messages;
Proto_alpha.Raw_context.back.dal_slot_fee_market := dal_slot_fee_market;
Proto_alpha.Raw_context.back.dal_attestation_slot_accountability :=
dal_attestation_slot_accountability;
Proto_alpha.Raw_context.back.dal_committee := dal_committee;
|}
|} =
Raw_context.to_t {|
Raw_context.config := {|
Raw_context_aux.config.remaining_operation_gas :=
remaining_operation_gas;
Raw_context_aux.config.constants := constants;
Raw_context_aux.config.round_durations := round_durations;
Raw_context_aux.config.cycle_eras := cycle_eras;
Raw_context_aux.config.level := level;
Raw_context_aux.config.predecessor_timestamp :=
predecessor_timestamp;
Raw_context_aux.config.timestamp := timestamp;
Raw_context_aux.config.fees := fees;
Raw_context_aux.config.origination_nonce := origination_nonce;
Raw_context_aux.config.temporary_lazy_storage_ids :=
temporary_lazy_storage_ids;
Raw_context_aux.config.internal_nonce := internal_nonce;
Raw_context_aux.config.internal_nonces_used :=
internal_nonces_used;
Raw_context_aux.config.remaining_block_gas := remaining_block_gas;
Raw_context_aux.config.unlimited_operation_gas :=
unlimited_operation_gas;
Raw_context_aux.config.consensus := consensus;
Raw_context_aux.config.non_consensus_operations_rev :=
non_consensus_operations_rev;
Raw_context_aux.config.dictator_proposal_seen :=
dictator_proposal_seen;
Raw_context_aux.config.sampler_state := sampler_state;
Raw_context_aux.config.stake_distribution_for_current_cycle :=
stake_distribution_for_current_cycle;
Raw_context_aux.config.tx_rollup_current_messages :=
tx_rollup_current_messages;
Raw_context_aux.config.sc_rollup_current_messages :=
sc_rollup_current_messages;
Raw_context_aux.config.dal_slot_fee_market :=
dal_slot_fee_market;
Raw_context_aux.config.dal_attestation_slot_accountability :=
dal_attestation_slot_accountability;
Raw_context_aux.config.dal_committee :=
dal_committee;
|};
Raw_context.standalone := standalone;
Raw_context.Block_round := sim_ctxt.(Raw_context.Block_round);
Raw_context.Tenderbake_First_level_of_protocol :=
sim_ctxt.(Raw_context.Tenderbake_First_level_of_protocol);
Raw_context.Tenderbake_Endorsement_branch :=
sim_ctxt.(Raw_context.Tenderbake_Endorsement_branch);
Raw_context.Tenderbake_Grand_parent_branch :=
sim_ctxt.(Raw_context.Tenderbake_Grand_parent_branch);
Raw_context.Contract_Global_counter :=
sim_ctxt.(Raw_context.Contract_Global_counter);
Raw_context.Contract_Spendable_balance :=
sim_ctxt.(Raw_context.Contract_Spendable_balance);
Raw_context.Contract_Missed_endorsements :=
sim_ctxt.(Raw_context.Contract_Missed_endorsements);
Raw_context.Contract_Manager :=
sim_ctxt.(Raw_context.Contract_Manager);
Raw_context.Contract_Consensus_key :=
sim_ctxt.(Raw_context.Contract_Consensus_key);
Raw_context.Contract_Pending_consensus_keys :=
sim_ctxt.(Raw_context.Contract_Pending_consensus_keys);
Raw_context.Contract_Delegate :=
sim_ctxt.(Raw_context.Contract_Delegate);
Raw_context.Contract_Inactive_delegate :=
sim_ctxt.(Raw_context.Contract_Inactive_delegate);
Raw_context.Contract_Delegate_last_cycle_before_deactivation :=
sim_ctxt
.(Raw_context.Contract_Delegate_last_cycle_before_deactivation);
Raw_context.Contract_Delegated :=
sim_ctxt.(Raw_context.Contract_Delegated);
Raw_context.Contract_Counter :=
sim_ctxt.(Raw_context.Contract_Counter);
Raw_context.Contract_Code :=
sim_ctxt.(Raw_context.Contract_Code);
Raw_context.Contract_Storage :=
sim_ctxt.(Raw_context.Contract_Storage);
Raw_context.Contract_Paid_storage_space :=
sim_ctxt.(Raw_context.Contract_Paid_storage_space);
Raw_context.Contract_Used_storage_space :=
sim_ctxt.(Raw_context.Contract_Used_storage_space);
Raw_context.Contract_Frozen_deposits :=
sim_ctxt.(Raw_context.Contract_Frozen_deposits);
Raw_context.Contract_Frozen_bonds :=
sim_ctxt.(Raw_context.Contract_Frozen_bonds);
Raw_context.Contract_Total_frozen_bonds :=
sim_ctxt.(Raw_context.Contract_Total_frozen_bonds);
Raw_context.Global_constants_Map :=
sim_ctxt.(Raw_context.Global_constants_Map);
Raw_context.Big_map_Next_Storage :=
sim_ctxt.(Raw_context.Big_map_Next_Storage);
Raw_context.Big_map_Total_bytes :=
sim_ctxt.(Raw_context.Big_map_Total_bytes);
Raw_context.Big_map_Key_type :=
sim_ctxt.(Raw_context.Big_map_Key_type);
Raw_context.Big_map_Value_type :=
sim_ctxt.(Raw_context.Big_map_Value_type);
Raw_context.Big_map_Contents :=
sim_ctxt.(Raw_context.Big_map_Contents);
Raw_context.Sapling_Next_Storage :=
sim_ctxt.(Raw_context.Sapling_Next_Storage);
Raw_context.Sapling_Total_bytes :=
sim_ctxt.(Raw_context.Sapling_Total_bytes);
Raw_context.Sapling_Commitments_size :=
sim_ctxt.(Raw_context.Sapling_Commitments_size);
Raw_context.Sapling_Memo_size :=
sim_ctxt.(Raw_context.Sapling_Memo_size);
Raw_context.Sapling_Commitments :=
sim_ctxt.(Raw_context.Sapling_Commitments);
Raw_context.Sapling_Ciphertexts :=
sim_ctxt.(Raw_context.Sapling_Ciphertexts);
Raw_context.Sapling_Nullifiers_size :=
sim_ctxt.(Raw_context.Sapling_Nullifiers_size);
Raw_context.Sapling_Nullifiers_ordered :=
sim_ctxt.(Raw_context.Sapling_Nullifiers_ordered);
Raw_context.Sapling_Nullifiers_hashed :=
sim_ctxt.(Raw_context.Sapling_Nullifiers_hashed);
Raw_context.Sapling_Roots :=
sim_ctxt.(Raw_context.Sapling_Roots);
Raw_context.Sapling_Roots_pos :=
sim_ctxt.(Raw_context.Sapling_Roots_pos);
Raw_context.Sapling_Roots_level :=
sim_ctxt.(Raw_context.Sapling_Roots_level);
Raw_context.Delegates :=
sim_ctxt.(Raw_context.Delegates);
Raw_context.Consensus_keys :=
sim_ctxt.(Raw_context.Consensus_keys);
Raw_context.Cycle_Slashed_deposits :=
sim_ctxt.(Raw_context.Cycle_Slashed_deposits);
Raw_context.Cycle_Selected_stake_distribution :=
sim_ctxt.(Raw_context.Cycle_Selected_stake_distribution);
Raw_context.Cycle_Total_active_stake :=
sim_ctxt.(Raw_context.Cycle_Total_active_stake);
Raw_context.Cycle_Delegate_sampler_state :=
sim_ctxt.(Raw_context.Cycle_Delegate_sampler_state);
Raw_context.Cycle_Nonce :=
sim_ctxt.(Raw_context.Cycle_Nonce);
Raw_context.Cycle_Seed :=
sim_ctxt.(Raw_context.Cycle_Seed);
Raw_context.Stake_Staking_balance :=
sim_ctxt.(Raw_context.Stake_Staking_balance);
Raw_context.Stake_Active_delegates_with_minimal_stake :=
sim_ctxt.(Raw_context.Stake_Active_delegates_with_minimal_stake);
Raw_context.Stake_Last_snapshot :=
sim_ctxt.(Raw_context.Stake_Last_snapshot);
Raw_context.Vote_Pred_period_kind :=
sim_ctxt.(Raw_context.Vote_Pred_period_kind);
Raw_context.Vote_Current_period :=
sim_ctxt.(Raw_context.Vote_Current_period);
Raw_context.Vote_Participation_ema :=
sim_ctxt.(Raw_context.Vote_Participation_ema);
Raw_context.Vote_Current_proposal :=
sim_ctxt.(Raw_context.Vote_Current_proposal);
Raw_context.Vote_Voting_power_in_listings :=
sim_ctxt.(Raw_context.Vote_Voting_power_in_listings);
Raw_context.Vote_Listings :=
sim_ctxt.(Raw_context.Vote_Listings);
Raw_context.Vote_Proposals :=
sim_ctxt.(Raw_context.Vote_Proposals);
Raw_context.Vote_Proposals_count :=
sim_ctxt.(Raw_context.Vote_Proposals_count);
Raw_context.Vote_Ballots :=
sim_ctxt.(Raw_context.Vote_Ballots);
Raw_context.Seed_status :=
sim_ctxt.(Raw_context.Seed_status);
Raw_context.Seed_VDF_setup :=
sim_ctxt.(Raw_context.Seed_VDF_setup);
Raw_context.Commitments :=
sim_ctxt.(Raw_context.Commitments);
Raw_context.Ramp_up_Rewards :=
sim_ctxt.(Raw_context.Ramp_up_Rewards);
Raw_context.Pending_migration_Balance_updates :=
sim_ctxt.(Raw_context.Pending_migration_Balance_updates);
Raw_context.Pending_migration_Operation_results :=
sim_ctxt.(Raw_context.Pending_migration_Operation_results);
Raw_context.Liquidity_baking_Toggle_ema :=
sim_ctxt.(Raw_context.Liquidity_baking_Toggle_ema);
Raw_context.Liquidity_baking_Cpmm_address :=
sim_ctxt.(Raw_context.Liquidity_baking_Cpmm_address);
Raw_context.Ticket_balance_Paid_storage_space :=
sim_ctxt.(Raw_context.Ticket_balance_Paid_storage_space);
Raw_context.Ticket_balance_Used_storage_space :=
sim_ctxt.(Raw_context.Ticket_balance_Used_storage_space);
Raw_context.Ticket_balance_Table :=
sim_ctxt.(Raw_context.Ticket_balance_Table);
Raw_context.Tx_rollup_State :=
sim_ctxt.(Raw_context.Tx_rollup_State);
Raw_context.Tx_rollup_Inbox :=
sim_ctxt.(Raw_context.Tx_rollup_Inbox);
Raw_context.Tx_rollup_Revealed_withdrawals :=
sim_ctxt.(Raw_context.Tx_rollup_Revealed_withdrawals);
Raw_context.Tx_rollup_Commitment :=
sim_ctxt.(Raw_context.Tx_rollup_Commitment);
Raw_context.Tx_rollup_Commitment_bond :=
sim_ctxt.(Raw_context.Tx_rollup_Commitment_bond);
Raw_context.Sc_rollup_PVM_kind :=
sim_ctxt.(Raw_context.Sc_rollup_PVM_kind);
Raw_context.Sc_rollup_Parameters_type :=
sim_ctxt.(Raw_context.Sc_rollup_Parameters_type);
Raw_context.Sc_rollup_Genesis_info :=
sim_ctxt.(Raw_context.Sc_rollup_Genesis_info);
Raw_context.Sc_rollup_Inbox :=
sim_ctxt.(Raw_context.Sc_rollup_Inbox);
Raw_context.Sc_rollup_Last_cemented_commitment :=
sim_ctxt.(Raw_context.Sc_rollup_Last_cemented_commitment);
Raw_context.Sc_rollup_Stakers :=
sim_ctxt.(Raw_context.Sc_rollup_Stakers);
Raw_context.Sc_rollup_Staker_count :=
sim_ctxt.(Raw_context.Sc_rollup_Staker_count);
Raw_context.Sc_rollup_Commitments :=
sim_ctxt.(Raw_context.Sc_rollup_Commitments);
Raw_context.Sc_rollup_Commitment_stake_count :=
sim_ctxt.(Raw_context.Sc_rollup_Commitment_stake_count);
Raw_context.Sc_rollup_Commitment_first_publication_level :=
sim_ctxt.(Raw_context.Sc_rollup_Commitment_first_publication_level);
Raw_context.Sc_rollup_Commitment_added :=
sim_ctxt.(Raw_context.Sc_rollup_Commitment_added);
Raw_context.Sc_rollup_Game_versioned :=
sim_ctxt.(Raw_context.Sc_rollup_Game_versioned);
Raw_context.Sc_rollup_Game :=
sim_ctxt.(Raw_context.Sc_rollup_Game);
Raw_context.Sc_rollup_Game_timeout :=
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout);
Raw_context.Sc_rollup_Opponent :=
sim_ctxt.(Raw_context.Sc_rollup_Opponent);
Raw_context.Sc_rollup_Applied_outbox_messages :=
sim_ctxt.(Raw_context.Sc_rollup_Applied_outbox_messages);
Raw_context.Dal_Slot_Headers :=
sim_ctxt.(Raw_context.Dal_Slot_Headers);
Raw_context.Dal_Slot_History :=
sim_ctxt.(Raw_context.Dal_Slot_History);
Raw_context.Zk_rollup_Account :=
sim_ctxt.(Raw_context.Zk_rollup_Account);
Raw_context.Zk_rollup_Pending_list :=
sim_ctxt.(Raw_context.Zk_rollup_Pending_list);
Raw_context.Zk_rollup_Pending_operation :=
sim_ctxt.(Raw_context.Zk_rollup_Pending_operation);
|}.
Proof.
reflexivity.
Qed.
Properties on the [Raw_context.T] signature.
Helper to unfold [Raw_context] primitives on the storage.
Module Unfold.
Import Proto_alpha.Raw_context.
Ltac all :=
unfold
mem, mem_tree,
get, get_tree,
find, find_tree,
add, add_tree,
init_value, init_tree,
update, update_tree,
remove_existing, remove_existing_tree,
remove,
add_or_remove, add_or_remove_tree,
list_value, fold,
project, absolute_key.
End Unfold.
Import Proto_alpha.Raw_context.
Ltac all :=
unfold
mem, mem_tree,
get, get_tree,
find, find_tree,
add, add_tree,
init_value, init_tree,
update, update_tree,
remove_existing, remove_existing_tree,
remove,
add_or_remove, add_or_remove_tree,
list_value, fold,
project, absolute_key.
End Unfold.
A [Raw_context] is valid when the fold operator respect the functional
extentionality axiom.
Module Valid.
Import Raw_context_intf.T.
Record t {t local_context} {C : Raw_context.T (t :=
t) (local_context := local_context)} : Prop := {
fold {a : Set} depth ctxt k order (acc : a) f1 f2 :
(∀ k v acc, f1 k v acc = f2 k v acc) →
C.(fold) depth ctxt k order acc f1 =
C.(fold) depth ctxt k order acc f2;
}.
Arguments t {_}.
End Valid.
Import Raw_context_intf.T.
Record t {t local_context} {C : Raw_context.T (t :=
t) (local_context := local_context)} : Prop := {
fold {a : Set} depth ctxt k order (acc : a) f1 f2 :
(∀ k v acc, f1 k v acc = f2 k v acc) →
C.(fold) depth ctxt k order acc f1 =
C.(fold) depth ctxt k order acc f2;
}.
Arguments t {_}.
End Valid.
The equality between two [Raw_context.T].
Module Eq.
Import Raw_context_intf.T.
Record t {t local_context : Set} {C1 C2 : Raw_context.T (t :=
t) (local_context := local_context)} : Prop := {
mem ctxt k : C1.(mem) ctxt k = C2.(mem) ctxt k;
mem_tree ctxt k : C1.(mem_tree) ctxt k = C2.(mem_tree) ctxt k;
get ctxt k : C1.(get) ctxt k = C2.(get) ctxt k;
get_tree ctxt k : C1.(get_tree) ctxt k = C2.(get_tree) ctxt k;
find ctxt k : C1.(find) ctxt k = C2.(find) ctxt k;
find_tree ctxt k : C1.(find_tree) ctxt k = C2.(find_tree) ctxt k;
list_value ctxt offset length k :
C1.(list_value) ctxt offset length k =
C2.(list_value) ctxt offset length k;
init_value ctxt k v : C1.(init_value) ctxt k v = C2.(init_value) ctxt k v;
init_tree ctxt k v : C1.(init_tree) ctxt k v = C2.(init_tree) ctxt k v;
update ctxt k v : C1.(update) ctxt k v = C2.(update) ctxt k v;
update_tree ctxt k v : C1.(update_tree) ctxt k v = C2.(update_tree) ctxt k v;
add ctxt k v : C1.(add) ctxt k v = C2.(add) ctxt k v;
add_tree ctxt k v : C1.(add_tree) ctxt k v = C2.(add_tree) ctxt k v;
remove ctxt k : C1.(remove) ctxt k = C2.(remove) ctxt k;
remove_existing ctxt k :
C1.(remove_existing) ctxt k = C2.(remove_existing) ctxt k;
remove_existing_tree ctxt k :
C1.(remove_existing_tree) ctxt k = C2.(remove_existing_tree) ctxt k;
add_or_remove ctxt k v :
C1.(add_or_remove) ctxt k v = C2.(add_or_remove) ctxt k v;
add_or_remove_tree ctxt k v :
C1.(add_or_remove_tree) ctxt k v = C2.(add_or_remove_tree) ctxt k v;
fold {a : Set} depth ctxt k order (acc : a) f :
C1.(fold) depth ctxt k order acc f =
C2.(fold) depth ctxt k order acc f;
Tree : Raw_context_intf.TREE.Eq.t C1.(Tree) C2.(Tree);
project ctxt : C1.(project) ctxt = C2.(project) ctxt;
absolute_key ctxt k : C1.(absolute_key) ctxt k = C2.(absolute_key) ctxt k;
(* We do not check [consume_gas], [check_enough_gas] and [description]. *)
}.
Arguments t {_ _}.
End Eq.
Import Raw_context_intf.T.
Record t {t local_context : Set} {C1 C2 : Raw_context.T (t :=
t) (local_context := local_context)} : Prop := {
mem ctxt k : C1.(mem) ctxt k = C2.(mem) ctxt k;
mem_tree ctxt k : C1.(mem_tree) ctxt k = C2.(mem_tree) ctxt k;
get ctxt k : C1.(get) ctxt k = C2.(get) ctxt k;
get_tree ctxt k : C1.(get_tree) ctxt k = C2.(get_tree) ctxt k;
find ctxt k : C1.(find) ctxt k = C2.(find) ctxt k;
find_tree ctxt k : C1.(find_tree) ctxt k = C2.(find_tree) ctxt k;
list_value ctxt offset length k :
C1.(list_value) ctxt offset length k =
C2.(list_value) ctxt offset length k;
init_value ctxt k v : C1.(init_value) ctxt k v = C2.(init_value) ctxt k v;
init_tree ctxt k v : C1.(init_tree) ctxt k v = C2.(init_tree) ctxt k v;
update ctxt k v : C1.(update) ctxt k v = C2.(update) ctxt k v;
update_tree ctxt k v : C1.(update_tree) ctxt k v = C2.(update_tree) ctxt k v;
add ctxt k v : C1.(add) ctxt k v = C2.(add) ctxt k v;
add_tree ctxt k v : C1.(add_tree) ctxt k v = C2.(add_tree) ctxt k v;
remove ctxt k : C1.(remove) ctxt k = C2.(remove) ctxt k;
remove_existing ctxt k :
C1.(remove_existing) ctxt k = C2.(remove_existing) ctxt k;
remove_existing_tree ctxt k :
C1.(remove_existing_tree) ctxt k = C2.(remove_existing_tree) ctxt k;
add_or_remove ctxt k v :
C1.(add_or_remove) ctxt k v = C2.(add_or_remove) ctxt k v;
add_or_remove_tree ctxt k v :
C1.(add_or_remove_tree) ctxt k v = C2.(add_or_remove_tree) ctxt k v;
fold {a : Set} depth ctxt k order (acc : a) f :
C1.(fold) depth ctxt k order acc f =
C2.(fold) depth ctxt k order acc f;
Tree : Raw_context_intf.TREE.Eq.t C1.(Tree) C2.(Tree);
project ctxt : C1.(project) ctxt = C2.(project) ctxt;
absolute_key ctxt k : C1.(absolute_key) ctxt k = C2.(absolute_key) ctxt k;
(* We do not check [consume_gas], [check_enough_gas] and [description]. *)
}.
Arguments t {_ _}.
End Eq.
A [Kernel] of primitive operations which are enough to describe a
whole [Raw_context.T].
The path from the root of the context store. It may depend on the
value of the context for indexed raw contexts.
Extract the root raw context.
Update the root raw context part of the context, and keep everything
else (typically, keeps the index for indexed raw contexts).
update : t → Proto_alpha.Raw_context.t → t;
}.
End Kernel.
Definition Kernel :=
@Kernel.signature.
Arguments Kernel {_}.
}.
End Kernel.
Definition Kernel :=
@Kernel.signature.
Arguments Kernel {_}.
The equality between two raw kernels.
Module Kernel_eq.
Import Kernel.
Record t {t} {K1 K2 : Kernel (t :=
t)} : Prop := {
absolute_key ctxt : K1.(absolute_key) ctxt = K2.(absolute_key) ctxt;
project ctxt : K1.(project) ctxt = K2.(project) ctxt;
update ctxt root_ctxt :
K1.(update) ctxt root_ctxt = K2.(update) ctxt root_ctxt;
}.
Arguments t {_}.
End Kernel_eq.
Import Kernel.
Record t {t} {K1 K2 : Kernel (t :=
t)} : Prop := {
absolute_key ctxt : K1.(absolute_key) ctxt = K2.(absolute_key) ctxt;
project ctxt : K1.(project) ctxt = K2.(project) ctxt;
update ctxt root_ctxt :
K1.(update) ctxt root_ctxt = K2.(update) ctxt root_ctxt;
}.
Arguments t {_}.
End Kernel_eq.
Define a whole raw context from its kernel.
Definition of_kernel {t local_context} (K : Kernel (t :=
t)) : Raw_context.T (t := t) (local_context := local_context) :=
let '{|
Kernel.absolute_key :=
absolute_key;
Kernel.project :=
project;
Kernel.update :=
update
|} :=
K in
let to_key ctxt k :=
absolute_key ctxt ++ k in
{|
Raw_context_intf.T.mem ctxt k :=
Raw_context.mem (project ctxt) (to_key ctxt k);
Raw_context_intf.T.mem_tree ctxt k :=
Raw_context.mem_tree (project ctxt) (to_key ctxt k);
Raw_context_intf.T.get ctxt k :=
Raw_context.get (project ctxt) (to_key ctxt k);
Raw_context_intf.T.get_tree ctxt k :=
Raw_context.get_tree (project ctxt) (to_key ctxt k);
Raw_context_intf.T.find ctxt k :=
Raw_context.find (project ctxt) (to_key ctxt k);
Raw_context_intf.T.find_tree ctxt k :=
Raw_context.find_tree (project ctxt) (to_key ctxt k);
Raw_context_intf.T.list_value ctxt offset length k :=
Raw_context.list_value (project ctxt) offset length (to_key ctxt k);
Raw_context_intf.T.init_value ctxt k v :=
let? root := Raw_context.init_value (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.init_tree ctxt k v :=
let? root := Raw_context.init_tree (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.update ctxt k v :=
let? root := Raw_context.update (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.update_tree ctxt k v :=
let? root := Raw_context.update_tree (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.add ctxt k v :=
let root := Raw_context.add (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.add_tree ctxt k v :=
let root := Raw_context.add_tree (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.remove ctxt k :=
let root := Raw_context.remove (project ctxt) (to_key ctxt k) in
update ctxt root;
Raw_context_intf.T.remove_existing ctxt k :=
let? root :=
Raw_context.remove_existing (project ctxt) (to_key ctxt k) in
return? update ctxt root;
Raw_context_intf.T.remove_existing_tree ctxt k :=
let? root :=
Raw_context.remove_existing_tree (project ctxt) (to_key ctxt k) in
return? update ctxt root;
Raw_context_intf.T.add_or_remove ctxt k v :=
let root :=
Raw_context.add_or_remove (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.add_or_remove_tree ctxt k v :=
let root :=
Raw_context.add_or_remove_tree (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.fold _ depth ctxt k order acc f :=
Raw_context.fold depth (project ctxt) (to_key ctxt k) order acc f;
Raw_context_intf.T.config_value :=
axiom "config_value";
Raw_context_intf.T.length :=
axiom "length";
Raw_context_intf.T.Tree :=
{|
Raw_context_intf.TREE.mem :=
Raw_context.Tree.(Raw_context_intf.TREE.mem);
Raw_context_intf.TREE.mem_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.mem_tree);
Raw_context_intf.TREE.get :=
Raw_context.Tree.(Raw_context_intf.TREE.get);
Raw_context_intf.TREE.get_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.get_tree);
Raw_context_intf.TREE.find :=
Raw_context.Tree.(Raw_context_intf.TREE.find);
Raw_context_intf.TREE.find_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.find_tree);
Raw_context_intf.TREE.list_value :=
Raw_context.Tree.(Raw_context_intf.TREE.list_value);
Raw_context_intf.TREE.init_value :=
Raw_context.Tree.(Raw_context_intf.TREE.init_value);
Raw_context_intf.TREE.init_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.init_tree);
Raw_context_intf.TREE.update :=
Raw_context.Tree.(Raw_context_intf.TREE.update);
Raw_context_intf.TREE.update_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.update_tree);
Raw_context_intf.TREE.add :=
Raw_context.Tree.(Raw_context_intf.TREE.add);
Raw_context_intf.TREE.add_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.add_tree);
Raw_context_intf.TREE.remove :=
Raw_context.Tree.(Raw_context_intf.TREE.remove);
Raw_context_intf.TREE.remove_existing :=
Raw_context.Tree.(Raw_context_intf.TREE.remove_existing);
Raw_context_intf.TREE.remove_existing_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.remove_existing_tree);
Raw_context_intf.TREE.add_or_remove :=
Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove);
Raw_context_intf.TREE.add_or_remove_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove_tree);
Raw_context_intf.TREE.fold _ :=
Raw_context.Tree.(Raw_context_intf.TREE.fold);
Raw_context_intf.TREE.config_value :=
Raw_context.Tree.(Raw_context_intf.TREE.config_value);
Raw_context_intf.TREE.length :=
Raw_context.Tree.(Raw_context_intf.TREE.length);
(* The definition of the [Tree] is very long and differs only on this
field. *)
Raw_context_intf.TREE.empty ctxt :=
Raw_context.Tree.empty (project ctxt);
Raw_context_intf.TREE.is_empty :=
Raw_context.Tree.(Raw_context_intf.TREE.is_empty);
Raw_context_intf.TREE.kind_value :=
Raw_context.Tree.(Raw_context_intf.TREE.kind_value);
Raw_context_intf.TREE.to_value :=
Raw_context.Tree.(Raw_context_intf.TREE.to_value);
Raw_context_intf.TREE.hash_value :=
Raw_context.Tree.(Raw_context_intf.TREE.hash_value);
Raw_context_intf.TREE.equal :=
Raw_context.Tree.(Raw_context_intf.TREE.equal);
Raw_context_intf.TREE.clear :=
Raw_context.Tree.(Raw_context_intf.TREE.clear);
|};
Raw_context_intf.T.verify_tree_proof ctxt :=
axiom "verify_tree_proof";
Raw_context_intf.T.verify_stream_proof ctxt :=
axiom "verify_stream_proof";
Raw_context_intf.T.equal_config :=
axiom "equal_config";
Raw_context_intf.T.project ctxt :=
project ctxt;
Raw_context_intf.T.absolute_key ctxt k :=
to_key ctxt k;
Raw_context_intf.T.consume_gas :=
axiom "consume_gas";
Raw_context_intf.T.check_enough_gas :=
axiom "check_enough_gas";
Raw_context_intf.T.description :=
axiom "description";
Raw_context_intf.T.with_local_context := axiom "with_local_context";
Raw_context_intf.T.Local_context := axiom "Local_context";
|}.
t)) : Raw_context.T (t := t) (local_context := local_context) :=
let '{|
Kernel.absolute_key :=
absolute_key;
Kernel.project :=
project;
Kernel.update :=
update
|} :=
K in
let to_key ctxt k :=
absolute_key ctxt ++ k in
{|
Raw_context_intf.T.mem ctxt k :=
Raw_context.mem (project ctxt) (to_key ctxt k);
Raw_context_intf.T.mem_tree ctxt k :=
Raw_context.mem_tree (project ctxt) (to_key ctxt k);
Raw_context_intf.T.get ctxt k :=
Raw_context.get (project ctxt) (to_key ctxt k);
Raw_context_intf.T.get_tree ctxt k :=
Raw_context.get_tree (project ctxt) (to_key ctxt k);
Raw_context_intf.T.find ctxt k :=
Raw_context.find (project ctxt) (to_key ctxt k);
Raw_context_intf.T.find_tree ctxt k :=
Raw_context.find_tree (project ctxt) (to_key ctxt k);
Raw_context_intf.T.list_value ctxt offset length k :=
Raw_context.list_value (project ctxt) offset length (to_key ctxt k);
Raw_context_intf.T.init_value ctxt k v :=
let? root := Raw_context.init_value (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.init_tree ctxt k v :=
let? root := Raw_context.init_tree (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.update ctxt k v :=
let? root := Raw_context.update (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.update_tree ctxt k v :=
let? root := Raw_context.update_tree (project ctxt) (to_key ctxt k) v in
return? update ctxt root;
Raw_context_intf.T.add ctxt k v :=
let root := Raw_context.add (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.add_tree ctxt k v :=
let root := Raw_context.add_tree (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.remove ctxt k :=
let root := Raw_context.remove (project ctxt) (to_key ctxt k) in
update ctxt root;
Raw_context_intf.T.remove_existing ctxt k :=
let? root :=
Raw_context.remove_existing (project ctxt) (to_key ctxt k) in
return? update ctxt root;
Raw_context_intf.T.remove_existing_tree ctxt k :=
let? root :=
Raw_context.remove_existing_tree (project ctxt) (to_key ctxt k) in
return? update ctxt root;
Raw_context_intf.T.add_or_remove ctxt k v :=
let root :=
Raw_context.add_or_remove (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.add_or_remove_tree ctxt k v :=
let root :=
Raw_context.add_or_remove_tree (project ctxt) (to_key ctxt k) v in
update ctxt root;
Raw_context_intf.T.fold _ depth ctxt k order acc f :=
Raw_context.fold depth (project ctxt) (to_key ctxt k) order acc f;
Raw_context_intf.T.config_value :=
axiom "config_value";
Raw_context_intf.T.length :=
axiom "length";
Raw_context_intf.T.Tree :=
{|
Raw_context_intf.TREE.mem :=
Raw_context.Tree.(Raw_context_intf.TREE.mem);
Raw_context_intf.TREE.mem_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.mem_tree);
Raw_context_intf.TREE.get :=
Raw_context.Tree.(Raw_context_intf.TREE.get);
Raw_context_intf.TREE.get_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.get_tree);
Raw_context_intf.TREE.find :=
Raw_context.Tree.(Raw_context_intf.TREE.find);
Raw_context_intf.TREE.find_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.find_tree);
Raw_context_intf.TREE.list_value :=
Raw_context.Tree.(Raw_context_intf.TREE.list_value);
Raw_context_intf.TREE.init_value :=
Raw_context.Tree.(Raw_context_intf.TREE.init_value);
Raw_context_intf.TREE.init_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.init_tree);
Raw_context_intf.TREE.update :=
Raw_context.Tree.(Raw_context_intf.TREE.update);
Raw_context_intf.TREE.update_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.update_tree);
Raw_context_intf.TREE.add :=
Raw_context.Tree.(Raw_context_intf.TREE.add);
Raw_context_intf.TREE.add_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.add_tree);
Raw_context_intf.TREE.remove :=
Raw_context.Tree.(Raw_context_intf.TREE.remove);
Raw_context_intf.TREE.remove_existing :=
Raw_context.Tree.(Raw_context_intf.TREE.remove_existing);
Raw_context_intf.TREE.remove_existing_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.remove_existing_tree);
Raw_context_intf.TREE.add_or_remove :=
Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove);
Raw_context_intf.TREE.add_or_remove_tree :=
Raw_context.Tree.(Raw_context_intf.TREE.add_or_remove_tree);
Raw_context_intf.TREE.fold _ :=
Raw_context.Tree.(Raw_context_intf.TREE.fold);
Raw_context_intf.TREE.config_value :=
Raw_context.Tree.(Raw_context_intf.TREE.config_value);
Raw_context_intf.TREE.length :=
Raw_context.Tree.(Raw_context_intf.TREE.length);
(* The definition of the [Tree] is very long and differs only on this
field. *)
Raw_context_intf.TREE.empty ctxt :=
Raw_context.Tree.empty (project ctxt);
Raw_context_intf.TREE.is_empty :=
Raw_context.Tree.(Raw_context_intf.TREE.is_empty);
Raw_context_intf.TREE.kind_value :=
Raw_context.Tree.(Raw_context_intf.TREE.kind_value);
Raw_context_intf.TREE.to_value :=
Raw_context.Tree.(Raw_context_intf.TREE.to_value);
Raw_context_intf.TREE.hash_value :=
Raw_context.Tree.(Raw_context_intf.TREE.hash_value);
Raw_context_intf.TREE.equal :=
Raw_context.Tree.(Raw_context_intf.TREE.equal);
Raw_context_intf.TREE.clear :=
Raw_context.Tree.(Raw_context_intf.TREE.clear);
|};
Raw_context_intf.T.verify_tree_proof ctxt :=
axiom "verify_tree_proof";
Raw_context_intf.T.verify_stream_proof ctxt :=
axiom "verify_stream_proof";
Raw_context_intf.T.equal_config :=
axiom "equal_config";
Raw_context_intf.T.project ctxt :=
project ctxt;
Raw_context_intf.T.absolute_key ctxt k :=
to_key ctxt k;
Raw_context_intf.T.consume_gas :=
axiom "consume_gas";
Raw_context_intf.T.check_enough_gas :=
axiom "check_enough_gas";
Raw_context_intf.T.description :=
axiom "description";
Raw_context_intf.T.with_local_context := axiom "with_local_context";
Raw_context_intf.T.Local_context := axiom "Local_context";
|}.
Generating contexts from two equal kernels yields two equal raw
contexts.
Lemma from_kernel_implies_eq {t local_context : Set} (K1 K2 : Kernel (t := t)) :
Kernel_eq.t K1 K2 →
Eq.t (local_context := local_context) (of_kernel K1) (of_kernel K2).
Proof.
intros []; repeat constructor; intros; simpl;
repeat match goal with
| |- context [let? _ := ?e in _] ⇒
destruct e eqn:?;
simpl
end;
repeat match goal with
| H : _ |- _ ⇒ rewrite H in ×
end;
congruence.
Qed.
Kernel_eq.t K1 K2 →
Eq.t (local_context := local_context) (of_kernel K1) (of_kernel K2).
Proof.
intros []; repeat constructor; intros; simpl;
repeat match goal with
| |- context [let? _ := ?e in _] ⇒
destruct e eqn:?;
simpl
end;
repeat match goal with
| H : _ |- _ ⇒ rewrite H in ×
end;
congruence.
Qed.
If a raw context is described by a given kernel.
Definition is_from_kernel {t local_context} (C : Raw_context.T (t := t) (local_context := local_context))
(K : Kernel (t := t)) : Prop :=
Eq.t C (of_kernel K).
(K : Kernel (t := t)) : Prop :=
Eq.t C (of_kernel K).
The kernel of the root raw context.
Definition M_kernel : Kernel (t := Proto_alpha.Raw_context.t) := {|
Kernel.absolute_key _ := [];
Kernel.project ctxt := ctxt;
Kernel.update _ root := root;
|}.
Kernel.absolute_key _ := [];
Kernel.project ctxt := ctxt;
Kernel.update _ root := root;
|}.
The main raw context can be expressed from a kernel.
Lemma M_is_from_kernel : is_from_kernel Raw_context.M M_kernel.
Proof.
repeat constructor; intros; simpl; try reflexivity;
match goal with
| |- context [let? _ := ?e in _] ⇒
destruct e eqn:?;
simpl
end;
sfirstorder.
Qed.
End T.
Proof.
repeat constructor; intros; simpl; try reflexivity;
match goal with
| |- context [let? _ := ?e in _] ⇒
destruct e eqn:?;
simpl
end;
sfirstorder.
Qed.
End T.
The value of [get_constants] for a valid context.
Lemma get_constants_eq {A : Set} standalone :
standalone.Valid.simulation standalone →
Raw_context.get_constants (A := A) (Raw_context.to_context standalone) =
return? standalone.(Raw_context_aux.standalone.constants).
Proof.
intros [].
unfold Raw_context.get_constants, Raw_context.to_context;
repeat destruct Binary.to_bytes_opt eqn:? in |- *;
repeat Context.rewrite_find_add;
repeat rewrite Raw_context.find_empty_context;
destruct Constants_parametric_repr.encoding_is_valid as [H_of_to H_to_of];
pose proof (H_of_to standalone.(Raw_context_aux.standalone.constants)) as H_encoding;
hauto l: on.
Qed.
standalone.Valid.simulation standalone →
Raw_context.get_constants (A := A) (Raw_context.to_context standalone) =
return? standalone.(Raw_context_aux.standalone.constants).
Proof.
intros [].
unfold Raw_context.get_constants, Raw_context.to_context;
repeat destruct Binary.to_bytes_opt eqn:? in |- *;
repeat Context.rewrite_find_add;
repeat rewrite Raw_context.find_empty_context;
destruct Constants_parametric_repr.encoding_is_valid as [H_of_to H_to_of];
pose proof (H_of_to standalone.(Raw_context_aux.standalone.constants)) as H_encoding;
hauto l: on.
Qed.
The function [check_inited] always succeeds on the simulated context.
Lemma check_inited_eq (standalone : Raw_context_aux.standalone) :
Raw_context.check_inited (Raw_context.to_context standalone) = return? tt.
Proof.
unfold Raw_context.check_inited, Raw_context.to_context;
repeat destruct Binary.to_bytes_opt eqn:? in |- *;
repeat Context.rewrite_find_add;
reflexivity.
Qed.
Raw_context.check_inited (Raw_context.to_context standalone) = return? tt.
Proof.
unfold Raw_context.check_inited, Raw_context.to_context;
repeat destruct Binary.to_bytes_opt eqn:? in |- *;
repeat Context.rewrite_find_add;
reflexivity.
Qed.
@TODO fix proof
Lemma check_cycle_eras_eq standalone :
standalone.Valid.simulation standalone →
Raw_context.check_cycle_eras
standalone.(Raw_context_aux.standalone.cycle_eras)
standalone.(Raw_context_aux.standalone.constants) =
return? tt.
Proof.
intros [].
unfold Raw_context.check_cycle_eras, Level_repr.current_era.
step; simpl.
{ inversion cycle_eras. cbn in ×. contradiction. }
{ (* TODO add this to the Level_repr.current_era_is_valid *)
assert (H : c.(Level_repr.cycle_era.blocks_per_cycle) =
standalone.(Raw_context_aux.standalone.constants)
.(Constants_parametric_repr.t.blocks_per_cycle) ∧
c.(Level_repr.cycle_era.blocks_per_commitment) =
standalone.(Raw_context_aux.standalone.constants)
.(Constants_parametric_repr.t.blocks_per_commitment))
by admit.
destruct H as [H H'].
step.
{ step; cbn; [reflexivity|].
rewrite Z.eqb_neq in Heqb0.
contradiction Heqb0.
}
{ rewrite Z.eqb_neq in Heqb.
contradiction H.
}
Admitted.
standalone.Valid.simulation standalone →
Raw_context.check_cycle_eras
standalone.(Raw_context_aux.standalone.cycle_eras)
standalone.(Raw_context_aux.standalone.constants) =
return? tt.
Proof.
intros [].
unfold Raw_context.check_cycle_eras, Level_repr.current_era.
step; simpl.
{ inversion cycle_eras. cbn in ×. contradiction. }
{ (* TODO add this to the Level_repr.current_era_is_valid *)
assert (H : c.(Level_repr.cycle_era.blocks_per_cycle) =
standalone.(Raw_context_aux.standalone.constants)
.(Constants_parametric_repr.t.blocks_per_cycle) ∧
c.(Level_repr.cycle_era.blocks_per_commitment) =
standalone.(Raw_context_aux.standalone.constants)
.(Constants_parametric_repr.t.blocks_per_commitment))
by admit.
destruct H as [H H'].
step.
{ step; cbn; [reflexivity|].
rewrite Z.eqb_neq in Heqb0.
contradiction Heqb0.
}
{ rewrite Z.eqb_neq in Heqb.
contradiction H.
}
Admitted.
Context contains an origination nonce
Module contains_origination_nonce.
Definition t (ctxt : Proto_alpha.Raw_context.t) : Prop :=
∃ origination_nonce,
Raw_context.origination_nonce ctxt = Some origination_nonce.
End contains_origination_nonce.
Definition t (ctxt : Proto_alpha.Raw_context.t) : Prop :=
∃ origination_nonce,
Raw_context.origination_nonce ctxt = Some origination_nonce.
End contains_origination_nonce.
The context has one [Level_repr.cycle_era] and
[level] is greather than this era
Module Has_one_era.
Definition t (ctxt : Proto_alpha.Raw_context.t)
(era : Level_repr.cycle_era) : Prop :=
Raw_context.cycle_eras ctxt = [era].
End Has_one_era.
Definition t (ctxt : Proto_alpha.Raw_context.t)
(era : Level_repr.cycle_era) : Prop :=
Raw_context.cycle_eras ctxt = [era].
End Has_one_era.
The encoding [storage_error_encoding] is valid.
Lemma storage_error_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Raw_context.storage_error_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
sauto l: on.
Qed.
#[global] Hint Resolve storage_error_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t (fun _ ⇒ True)
Raw_context.storage_error_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
sauto l: on.
Qed.
#[global] Hint Resolve storage_error_encoding_is_valid : Data_encoding_db.
[check_inited] never returns an internal error
Lemma check_inited_is_valid standalone :
letP? _ := Raw_context.check_inited (Raw_context.to_context standalone) in True.
Proof.
now rewrite Raw_context.check_inited_eq.
Qed.
Module ToMove.
letP? _ := Raw_context.check_inited (Raw_context.to_context standalone) in True.
Proof.
now rewrite Raw_context.check_inited_eq.
Qed.
Module ToMove.
ensures that [level] is greater than the levels inside [ctxt]
@TODO This predicate can probably be simplified when [ctxt] is valid
because level decrease.
Definition level_valid_for_context standalone
(level : Raw_level_repr.t) : Prop :=
letP? _ := Level_repr.level_from_raw
standalone.(Raw_context_aux.standalone.cycle_eras) level
in True.
End ToMove.
(* @TODO? should we also check that predecessor_timestamp
is less than timestamp in the input of prepare?*)
(level : Raw_level_repr.t) : Prop :=
letP? _ := Level_repr.level_from_raw
standalone.(Raw_context_aux.standalone.cycle_eras) level
in True.
End ToMove.
(* @TODO? should we also check that predecessor_timestamp
is less than timestamp in the input of prepare?*)
under the expected validity conditions, [prepare] never returns an internal
error, provided that [level] (aka [Int32.succ pred_level]) is greater
than the first level of [ctxt].
Note: this hypothesis can probably be simplified, since the validity of
[ctxt] ensures that the levels of ctxt are decreasing.
@TODO fix proof
Lemma prepare_is_valid (pred_level : Raw_level_repr.t)
(predecessor_timestamp timestamp : Time.t) (standalone : Raw_context_aux.standalone) :
Raw_level_repr.Valid.t pred_level →
pred_level ≠ Int32.max_int →
standalone.Valid.simulation standalone →
ToMove.level_valid_for_context standalone (Int32.succ pred_level) →
letP? _ :=
Raw_context.prepare
(Int32.succ pred_level)
predecessor_timestamp
timestamp
(Raw_context.to_context standalone)
in True.
Proof.
intros.
unfold Raw_context.prepare.
rewrite Raw_level_repr.of_int32_eq by lia; simpl.
rewrite Raw_context.check_inited_eq; simpl.
rewrite Raw_context.get_constants_eq by assumption; simpl.
rewrite Round_repr.Durations.create_eq by dtauto; simpl.
(predecessor_timestamp timestamp : Time.t) (standalone : Raw_context_aux.standalone) :
Raw_level_repr.Valid.t pred_level →
pred_level ≠ Int32.max_int →
standalone.Valid.simulation standalone →
ToMove.level_valid_for_context standalone (Int32.succ pred_level) →
letP? _ :=
Raw_context.prepare
(Int32.succ pred_level)
predecessor_timestamp
timestamp
(Raw_context.to_context standalone)
in True.
Proof.
intros.
unfold Raw_context.prepare.
rewrite Raw_level_repr.of_int32_eq by lia; simpl.
rewrite Raw_context.check_inited_eq; simpl.
rewrite Raw_context.get_constants_eq by assumption; simpl.
rewrite Round_repr.Durations.create_eq by dtauto; simpl.
rewrite Raw_context.get_cycle_eras_eq by assumption; simpl.
rewrite Raw_context.check_cycle_eras_eq by assumption; simpl.
apply no_internal_errors_let.
(** Note: the tactic no_internal_errors_lets
would create three non-trivial subgoals, including the first one here *)
assumption. intro. exact I. Qed.
would create three non-trivial subgoals, including the first one here *)
assumption. intro. exact I. Qed.
Admitted.
[Raw_context.sampler] is valid
Lemma sampler_for_cycle_is_valid
(f
: Proto_alpha.Raw_context.t →
tzresult (Seed_repr.seed × Sampler.t Raw_context.consensus_pk))
(ctxt : Proto_alpha.Raw_context.t)
(cycle : Cycle_repr.t)
: (∀ ctxt, letP? _ := (f ctxt) in True) →
letP? _ := Raw_context.sampler_for_cycle f ctxt cycle in True.
Proof. Admitted.
(f
: Proto_alpha.Raw_context.t →
tzresult (Seed_repr.seed × Sampler.t Raw_context.consensus_pk))
(ctxt : Proto_alpha.Raw_context.t)
(cycle : Cycle_repr.t)
: (∀ ctxt, letP? _ := (f ctxt) in True) →
letP? _ := Raw_context.sampler_for_cycle f ctxt cycle in True.
Proof. Admitted.
Simulation [to_t] is injective
Lemma to_t_is_injective c1 c2 :
Raw_context.to_t c1 = Raw_context.to_t c2 → c1 = c2.
Proof.
Admitted.
Raw_context.to_t c1 = Raw_context.to_t c2 → c1 = c2.
Proof.
Admitted.
[fees] is valid
Lemma fees_is_valid ctxt :
Valid.t ctxt →
Tez_repr.Valid.t (Raw_context.fees ctxt).
Proof.
intro Hv.
unfold Raw_context.fees.
destruct ctxt; simpl.
unfold Valid.t in Hv.
unfold Valid.on in Hv.
destruct Hv as [sc Hsc].
destruct Hsc as [Heq [Hv _]].
unfold Raw_context.to_t in Heq.
inversion Heq.
destruct Hv.
unfold Raw_context.to_back; simpl.
destruct config.
exact fees.
Qed.
Valid.t ctxt →
Tez_repr.Valid.t (Raw_context.fees ctxt).
Proof.
intro Hv.
unfold Raw_context.fees.
destruct ctxt; simpl.
unfold Valid.t in Hv.
unfold Valid.on in Hv.
destruct Hv as [sc Hsc].
destruct Hsc as [Heq [Hv _]].
unfold Raw_context.to_t in Heq.
inversion Heq.
destruct Hv.
unfold Raw_context.to_back; simpl.
destruct config.
exact fees.
Qed.
[update_back] is valid
Lemma update_back_is_valid ctxt back :
Valid.t ctxt →
Valid.t (Raw_context.update_back ctxt back).
Proof.
Admitted.
Valid.t ctxt →
Valid.t (Raw_context.update_back ctxt back).
Proof.
Admitted.
[get_collected_fees_only_call_from_token] is valid
Lemma get_collected_fees_is_valid ctxt :
Valid.t ctxt →
Tez_repr.Valid.t (Raw_context.get_collected_fees ctxt).
Proof.
apply fees_is_valid.
Qed.
Valid.t ctxt →
Tez_repr.Valid.t (Raw_context.get_collected_fees ctxt).
Proof.
apply fees_is_valid.
Qed.
[update_fees] is valid
Lemma update_fees_is_valid ctxt t :
Valid.t ctxt →
Tez_repr.Valid.t t →
Valid.t (Raw_context.update_fees ctxt t).
Proof.
Admitted.
Valid.t ctxt →
Tez_repr.Valid.t t →
Valid.t (Raw_context.update_fees ctxt t).
Proof.
Admitted.
[credit_collected_fees_only_call_from_token] is valid
Lemma credit_collected_fees_only_call_from_token_is_valid ctxt fees' :
Valid.t ctxt →
letP? t1 := Raw_context.credit_collected_fees_only_call_from_token
ctxt fees' in Valid.t t1.
Proof.
intro.
unfold Raw_context.credit_collected_fees_only_call_from_token.
eapply Error.split_letP.
{ apply Tez_repr.op_plusquestion_is_valid.
now apply get_collected_fees_is_valid.
}
intros; simpl.
now apply update_fees_is_valid.
Qed.
Valid.t ctxt →
letP? t1 := Raw_context.credit_collected_fees_only_call_from_token
ctxt fees' in Valid.t t1.
Proof.
intro.
unfold Raw_context.credit_collected_fees_only_call_from_token.
eapply Error.split_letP.
{ apply Tez_repr.op_plusquestion_is_valid.
now apply get_collected_fees_is_valid.
}
intros; simpl.
now apply update_fees_is_valid.
Qed.
[spend_collected_fees_only_call_from_token] is valid
Lemma spend_collected_fees_only_call_from_token_is_valid ctxt fees :
Valid.t ctxt →
Tez_repr.Valid.t fees →
letP? t1 := Raw_context.spend_collected_fees_only_call_from_token
ctxt fees in Valid.t t1.
Proof.
intros Hctxt Hfees.
unfold Raw_context.spend_collected_fees_only_call_from_token.
eapply Error.split_letP.
2:{ intros.
simpl.
apply update_fees_is_valid; eauto.
}
epose proof (Tez_repr.op_minusquestion_is_valid
(get_collected_fees_is_valid _ Hctxt)
Hfees).
destruct Raw_context.get_collected_fees.
destruct fees.
destruct Tez_repr.op_minusquestion eqn:Hminus.
{ destruct t; tauto. }
{ unfold Tez_repr.op_minusquestion in Hminus.
destruct (_ ≤i64 _); [discriminate|].
simpl in ×.
now inversion Hminus.
}
Qed.
Valid.t ctxt →
Tez_repr.Valid.t fees →
letP? t1 := Raw_context.spend_collected_fees_only_call_from_token
ctxt fees in Valid.t t1.
Proof.
intros Hctxt Hfees.
unfold Raw_context.spend_collected_fees_only_call_from_token.
eapply Error.split_letP.
2:{ intros.
simpl.
apply update_fees_is_valid; eauto.
}
epose proof (Tez_repr.op_minusquestion_is_valid
(get_collected_fees_is_valid _ Hctxt)
Hfees).
destruct Raw_context.get_collected_fees.
destruct fees.
destruct Tez_repr.op_minusquestion eqn:Hminus.
{ destruct t; tauto. }
{ unfold Tez_repr.op_minusquestion in Hminus.
destruct (_ ≤i64 _); [discriminate|].
simpl in ×.
now inversion Hminus.
}
Qed.
[init_origination_nonce] is valid
Lemma init_origination_nonce_is_valid ctxt operation_hash :
Valid.t ctxt →
let ctxt :=
Raw_context.init_origination_nonce ctxt operation_hash in
Valid.t ctxt.
Proof.
intro.
now apply update_back_is_valid.
Qed.
Valid.t ctxt →
let ctxt :=
Raw_context.init_origination_nonce ctxt operation_hash in
Valid.t ctxt.
Proof.
intro.
now apply update_back_is_valid.
Qed.
[increment_origination_nonce] is valid
Lemma increment_origination_nonce_is_valid ctxt :
Valid.t ctxt →
letP? ' (ctxt, _) := Raw_context.increment_origination_nonce
ctxt in Valid.t ctxt.
Proof.
intro.
unfold Raw_context.increment_origination_nonce.
destruct Raw_context.origination_nonce; [|reflexivity].
now apply update_back_is_valid.
Qed.
Valid.t ctxt →
letP? ' (ctxt, _) := Raw_context.increment_origination_nonce
ctxt in Valid.t ctxt.
Proof.
intro.
unfold Raw_context.increment_origination_nonce.
destruct Raw_context.origination_nonce; [|reflexivity].
now apply update_back_is_valid.
Qed.
[origination_nonce] is valid
Lemma origination_nonce_is_valid ctxt o :
Valid.t ctxt →
Raw_context.origination_nonce ctxt = Some o →
Origination_nonce.Valid.t o.
Proof.
Admitted.
Valid.t ctxt →
Raw_context.origination_nonce ctxt = Some o →
Origination_nonce.Valid.t o.
Proof.
Admitted.
[get_origination_nonce] is valid
Lemma get_origination_nonce_is_valid ctxt :
Valid.t ctxt →
letP? 'o := Raw_context.get_origination_nonce
ctxt in
Origination_nonce.Valid.t o.
Proof.
intro.
unfold Raw_context.get_origination_nonce.
destruct Raw_context.origination_nonce eqn:?; [|reflexivity].
eapply origination_nonce_is_valid; eauto.
Qed.
Valid.t ctxt →
letP? 'o := Raw_context.get_origination_nonce
ctxt in
Origination_nonce.Valid.t o.
Proof.
intro.
unfold Raw_context.get_origination_nonce.
destruct Raw_context.origination_nonce eqn:?; [|reflexivity].
eapply origination_nonce_is_valid; eauto.
Qed.
The function [unset_origination_nonce] is valid.
Lemma unset_origination_nonce_is_valid ctxt :
Valid.t ctxt →
let ctxt := Raw_context.unset_origination_nonce ctxt in
Raw_context.Valid.t ctxt.
Proof.
intro.
unfold Raw_context.unset_origination_nonce.
unfold Raw_context.update_origination_nonce.
now apply update_back_is_valid.
Qed.
Valid.t ctxt →
let ctxt := Raw_context.unset_origination_nonce ctxt in
Raw_context.Valid.t ctxt.
Proof.
intro.
unfold Raw_context.unset_origination_nonce.
unfold Raw_context.update_origination_nonce.
now apply update_back_is_valid.
Qed.
The function [remaining_operation_gas] is valid.
Lemma remaining_operation_gas_is_valid ctxt :
Valid.t ctxt →
Saturation_repr.Strictly_valid.t
(Raw_context.remaining_operation_gas ctxt).
Proof.
Admitted.
Valid.t ctxt →
Saturation_repr.Strictly_valid.t
(Raw_context.remaining_operation_gas ctxt).
Proof.
Admitted.
The function [gas_level] is valid.
Lemma gas_level_is_valid ctxt :
Valid.t ctxt →
let gas := Raw_context.gas_level ctxt in
Gas_limit_repr.Valid.t gas.
Proof.
intro.
unfold Raw_context.gas_level.
destruct Raw_context.unlimited_operation_gas eqn:?; [exact I|].
now apply remaining_operation_gas_is_valid.
Qed.
Valid.t ctxt →
let gas := Raw_context.gas_level ctxt in
Gas_limit_repr.Valid.t gas.
Proof.
intro.
unfold Raw_context.gas_level.
destruct Raw_context.unlimited_operation_gas eqn:?; [exact I|].
now apply remaining_operation_gas_is_valid.
Qed.
The function [remaining_block_gas] is valid.
Lemma remaining_block_gas_is_valid ctxt :
Valid.t ctxt →
Saturation_repr.Valid.t
(Raw_context.remaining_block_gas ctxt).
Proof.
Admitted.
Valid.t ctxt →
Saturation_repr.Valid.t
(Raw_context.remaining_block_gas ctxt).
Proof.
Admitted.
The function [block_gas_level] is valid.
Lemma block_gas_level_is_valid ctxt :
Valid.t ctxt →
let gas := Raw_context.block_gas_level ctxt in
Saturation_repr.Valid.t gas.
Proof.
intro.
now apply remaining_block_gas_is_valid.
Qed.
Valid.t ctxt →
let gas := Raw_context.block_gas_level ctxt in
Saturation_repr.Valid.t gas.
Proof.
intro.
now apply remaining_block_gas_is_valid.
Qed.
The function [consume_gas_limit_in_block] is valid.
Lemma consume_gas_limit_in_block_is_valid ctxt gas_limit :
Valid.t ctxt →
Gas_limit_repr.Arith.Integral.Valid.t gas_limit →
letP? ctxt := Raw_context.consume_gas_limit_in_block ctxt gas_limit in
Raw_context.Valid.t ctxt.
Proof.
intros.
unfold Raw_context.consume_gas_limit_in_block.
eapply Error.split_letP.
{ apply Gas_limit_repr.check_gas_limit_is_valid.
{ admit. }
{ auto. }
}
{ intros _ _.
destruct (Gas_limit_repr.Arith.op_gt).
{ reflexivity. }
{ now apply update_back_is_valid. }
}
Admitted.
Valid.t ctxt →
Gas_limit_repr.Arith.Integral.Valid.t gas_limit →
letP? ctxt := Raw_context.consume_gas_limit_in_block ctxt gas_limit in
Raw_context.Valid.t ctxt.
Proof.
intros.
unfold Raw_context.consume_gas_limit_in_block.
eapply Error.split_letP.
{ apply Gas_limit_repr.check_gas_limit_is_valid.
{ admit. }
{ auto. }
}
{ intros _ _.
destruct (Gas_limit_repr.Arith.op_gt).
{ reflexivity. }
{ now apply update_back_is_valid. }
}
Admitted.
The function [with_remaining_operation_gas] is valid.
Lemma with_remaining_operation_gas_is_valid ctxt remaining :
Valid.t ctxt →
Saturation_repr.Valid.t remaining →
Valid.t
(Raw_context.t.with_remaining_operation_gas remaining ctxt).
Proof.
Admitted.
Valid.t ctxt →
Saturation_repr.Valid.t remaining →
Valid.t
(Raw_context.t.with_remaining_operation_gas remaining ctxt).
Proof.
Admitted.
The function [set_gas_limit] is valid.
Lemma set_gas_limit_is_valid ctxt remaining :
Valid.t ctxt →
Saturation_repr.Valid.t remaining →
let ctxt := Raw_context.set_gas_limit ctxt remaining in
Raw_context.Valid.t ctxt.
Proof.
simpl; intros.
unfold Raw_context.set_gas_limit.
apply with_remaining_operation_gas_is_valid; [|auto].
now apply update_back_is_valid.
Qed.
Valid.t ctxt →
Saturation_repr.Valid.t remaining →
let ctxt := Raw_context.set_gas_limit ctxt remaining in
Raw_context.Valid.t ctxt.
Proof.
simpl; intros.
unfold Raw_context.set_gas_limit.
apply with_remaining_operation_gas_is_valid; [|auto].
now apply update_back_is_valid.
Qed.
The function [set_gas_unlimited] is valid.
Lemma set_gas_unlimited_is_valid ctxt :
Valid.t ctxt →
let ctxt := Raw_context.set_gas_unlimited ctxt in
Raw_context.Valid.t ctxt.
Proof.
simpl; intro.
now apply update_back_is_valid.
Qed.
Valid.t ctxt →
let ctxt := Raw_context.set_gas_unlimited ctxt in
Raw_context.Valid.t ctxt.
Proof.
simpl; intro.
now apply update_back_is_valid.
Qed.
The function [raw_consume] is valid.
Lemma raw_consume_is_valid amount cost amount' :
Saturation_repr.Valid.t amount →
Saturation_repr.Valid.t cost →
Gas_limit_repr.raw_consume amount cost = Some amount' →
Saturation_repr.Valid.t amount'.
Proof.
Admitted.
Saturation_repr.Valid.t amount →
Saturation_repr.Valid.t cost →
Gas_limit_repr.raw_consume amount cost = Some amount' →
Saturation_repr.Valid.t amount'.
Proof.
Admitted.
The function [consume_gas] is valid.
Lemma consume_gas_is_valid ctxt cost :
Valid.t ctxt →
Saturation_repr.Valid.t cost →
letP? ctxt := Raw_context.consume_gas ctxt cost in
Raw_context.Valid.t ctxt.
Proof.
intros Hctxt Hcost.
unfold Raw_context.consume_gas.
destruct Gas_limit_repr.raw_consume eqn:Heq.
{ simpl.
unfold Raw_context.update_remaining_operation_gas.
apply with_remaining_operation_gas_is_valid; [auto|].
apply (raw_consume_is_valid
(Raw_context.remaining_operation_gas ctxt)
cost); auto.
pose (remaining_operation_gas_is_valid _ Hctxt).
unfold Saturation_repr.Strictly_valid.t in ×.
unfold Saturation_repr.Valid.t; lia.
}
{ destruct Raw_context.unlimited_operation_gas; [auto|].
reflexivity.
}
Qed.
Valid.t ctxt →
Saturation_repr.Valid.t cost →
letP? ctxt := Raw_context.consume_gas ctxt cost in
Raw_context.Valid.t ctxt.
Proof.
intros Hctxt Hcost.
unfold Raw_context.consume_gas.
destruct Gas_limit_repr.raw_consume eqn:Heq.
{ simpl.
unfold Raw_context.update_remaining_operation_gas.
apply with_remaining_operation_gas_is_valid; [auto|].
apply (raw_consume_is_valid
(Raw_context.remaining_operation_gas ctxt)
cost); auto.
pose (remaining_operation_gas_is_valid _ Hctxt).
unfold Saturation_repr.Strictly_valid.t in ×.
unfold Saturation_repr.Valid.t; lia.
}
{ destruct Raw_context.unlimited_operation_gas; [auto|].
reflexivity.
}
Qed.
The function [activate] is valid
Lemma activate_is_valid ctxt h :
Raw_context.Valid.t ctxt →
Raw_context.Valid.t (Raw_context.activate ctxt h).
Proof.
intro.
now apply update_back_is_valid.
Qed.
Module Cache.
Raw_context.Valid.t ctxt →
Raw_context.Valid.t (Raw_context.activate ctxt h).
Proof.
intro.
now apply update_back_is_valid.
Qed.
Module Cache.
The function [sync] is valid.
Lemma sync_is_valid c_value cache_nonce :
Raw_context.Valid.t c_value →
Raw_context.Valid.t (Raw_context.Cache.sync c_value cache_nonce).
Proof.
Admitted.
End Cache.
Module Consensus.
Raw_context.Valid.t c_value →
Raw_context.Valid.t (Raw_context.Cache.sync c_value cache_nonce).
Proof.
Admitted.
End Cache.
Module Consensus.
The function [update_consensus_with] is valid.
Lemma update_consensus_with_is_valid ctxt f
(H_ctxt : Raw_context.Valid.t ctxt)
(H_f : ∀ consensus,
Raw_consensus.Valid.t consensus →
Raw_consensus.Valid.t (f consensus)
) :
let ctxt := Raw_context.Consensus.update_consensus_with ctxt f in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt)
(H_f : ∀ consensus,
Raw_consensus.Valid.t consensus →
Raw_consensus.Valid.t (f consensus)
) :
let ctxt := Raw_context.Consensus.update_consensus_with ctxt f in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
The function [initialize_consensus_operation] is valid.
Lemma initialize_consensus_operation_is_valid
ctxt allowed_endorsements allowed_preendorsements
(H_ctxt : Raw_context.Valid.t ctxt) :
let ctxt :=
Raw_context.Consensus.initialize_consensus_operation
ctxt allowed_endorsements allowed_preendorsements in
Raw_context.Valid.t ctxt.
Proof.
unfold Raw_context.Consensus.initialize_consensus_operation.
apply update_consensus_with_is_valid; trivial.
apply
Raw_context.Raw_consensus.initialize_with_endorsements_and_preendorsements_is_valid.
Qed.
End Consensus.
Module Tx_rollup.
ctxt allowed_endorsements allowed_preendorsements
(H_ctxt : Raw_context.Valid.t ctxt) :
let ctxt :=
Raw_context.Consensus.initialize_consensus_operation
ctxt allowed_endorsements allowed_preendorsements in
Raw_context.Valid.t ctxt.
Proof.
unfold Raw_context.Consensus.initialize_consensus_operation.
apply update_consensus_with_is_valid; trivial.
apply
Raw_context.Raw_consensus.initialize_with_endorsements_and_preendorsements_is_valid.
Qed.
End Consensus.
Module Tx_rollup.
The function [add_message] is valid.
Lemma add_message_is_valid ctxt rollup message :
Raw_context.Valid.t ctxt →
let '(ctxt, _) := Raw_context.Tx_rollup.add_message ctxt rollup message in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
End Tx_rollup.
Module Sc_rollup_in_memory_inbox.
Raw_context.Valid.t ctxt →
let '(ctxt, _) := Raw_context.Tx_rollup.add_message ctxt rollup message in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
End Tx_rollup.
Module Sc_rollup_in_memory_inbox.
The function [current_messages] is valid.
(*
Lemma current_messages ctxt rollup :
Raw_context.Valid.t ctxt ->
letP? '(_, ctxt) :=
Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt rollup in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(** The function [set_current_messages] is valid. *)
Lemma set_current_messages ctxt rollup tree_value :
Raw_context.Valid.t ctxt ->
letP? ctxt :=
Raw_context.Sc_rollup_in_memory_inbox.set_current_messages
ctxt rollup tree_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted. *)
End Sc_rollup_in_memory_inbox.
Module Dal.
Lemma current_messages ctxt rollup :
Raw_context.Valid.t ctxt ->
letP? '(_, ctxt) :=
Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt rollup in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(** The function [set_current_messages] is valid. *)
Lemma set_current_messages ctxt rollup tree_value :
Raw_context.Valid.t ctxt ->
letP? ctxt :=
Raw_context.Sc_rollup_in_memory_inbox.set_current_messages
ctxt rollup tree_value in
Raw_context.Valid.t ctxt.
Proof.
Admitted. *)
End Sc_rollup_in_memory_inbox.
Module Dal.
The function [record_available_shards] is valid.
(*
Lemma record_available_shards_is_valid ctxt slots shards
(H_ctxt : Raw_context.Valid.t ctxt)
(H_slots : Dal_endorsement_repr.Valid.t slots)
(H_shards :
List.Forall Dal_endorsement_repr.Accountability.shard.Valid.t shards) :
let ctxt := Raw_context.Dal.record_available_shards ctxt slots shards in
Raw_context.Valid.t ctxt.
Proof.
unfold Raw_context.Dal.record_available_shards.
destruct H_ctxt as [sim_ctxt [H_sim_ctxt_eq [H_sim_ctxt]]].
rewrite H_sim_ctxt_eq; simpl.
destruct sim_ctxt; simpl.
destruct config; simpl.
unfold Raw_context.to_t,
Raw_context.to_back,
Proto_alpha.Raw_context.t.with_back,
Raw_context.back.with_dal_endorsement_slot_accountability;
simpl.
cbn.
eexists.
split; [|split; trivial].
{ apply to_t_inversion. }
{
destruct H_sim_ctxt, config, standalone0. simpl in *.
match type of H_sim_ctxt_eq with
| _ = Raw_context.to_t ?sim_ctxt' =>
instantiate (1 := sim_ctxt')
end.
constructor; simpl; try (constructor; simpl); trivial;
destruct Tenderbake, Vote; [|easy..].
now apply
Dal_endorsement_repr.Accountability
.record_shards_availability_is_valid.
}
Qed.
(** The function [register_slot] is valid. *)
Lemma register_slot_is_valid ctxt slot
(H_ctxt : Raw_context.Valid.t ctxt)
(H_slot : Dal_slot_repr.Valid.t slot) :
letP? '(ctxt, _) := Raw_context.Dal.register_slot ctxt slot in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(** The function [candidates] is valid. *)
Lemma candidates_is_valid ctxt
(H_ctxt : Raw_context.Valid.t ctxt) :
let slots := Raw_context.Dal.candidates ctxt in
List.Forall Dal_slot_repr.Valid.t slots.
Proof.
Admitted.
(** The function [shards] is valid. *)
Lemma shards_is_valid ctxt endorser
(H_ctxt : Raw_context.Valid.t ctxt) :
let slots := Raw_context.Dal.shards ctxt endorser in
List.Forall
Dal_endorsement_repr.Accountability.shard.Valid.t
(Raw_context.Dal.shards ctxt endorser).
Proof.
Admitted.
*)
End Dal.
Lemma record_available_shards_is_valid ctxt slots shards
(H_ctxt : Raw_context.Valid.t ctxt)
(H_slots : Dal_endorsement_repr.Valid.t slots)
(H_shards :
List.Forall Dal_endorsement_repr.Accountability.shard.Valid.t shards) :
let ctxt := Raw_context.Dal.record_available_shards ctxt slots shards in
Raw_context.Valid.t ctxt.
Proof.
unfold Raw_context.Dal.record_available_shards.
destruct H_ctxt as [sim_ctxt [H_sim_ctxt_eq [H_sim_ctxt]]].
rewrite H_sim_ctxt_eq; simpl.
destruct sim_ctxt; simpl.
destruct config; simpl.
unfold Raw_context.to_t,
Raw_context.to_back,
Proto_alpha.Raw_context.t.with_back,
Raw_context.back.with_dal_endorsement_slot_accountability;
simpl.
cbn.
eexists.
split; [|split; trivial].
{ apply to_t_inversion. }
{
destruct H_sim_ctxt, config, standalone0. simpl in *.
match type of H_sim_ctxt_eq with
| _ = Raw_context.to_t ?sim_ctxt' =>
instantiate (1 := sim_ctxt')
end.
constructor; simpl; try (constructor; simpl); trivial;
destruct Tenderbake, Vote; [|easy..].
now apply
Dal_endorsement_repr.Accountability
.record_shards_availability_is_valid.
}
Qed.
(** The function [register_slot] is valid. *)
Lemma register_slot_is_valid ctxt slot
(H_ctxt : Raw_context.Valid.t ctxt)
(H_slot : Dal_slot_repr.Valid.t slot) :
letP? '(ctxt, _) := Raw_context.Dal.register_slot ctxt slot in
Raw_context.Valid.t ctxt.
Proof.
Admitted.
(** The function [candidates] is valid. *)
Lemma candidates_is_valid ctxt
(H_ctxt : Raw_context.Valid.t ctxt) :
let slots := Raw_context.Dal.candidates ctxt in
List.Forall Dal_slot_repr.Valid.t slots.
Proof.
Admitted.
(** The function [shards] is valid. *)
Lemma shards_is_valid ctxt endorser
(H_ctxt : Raw_context.Valid.t ctxt) :
let slots := Raw_context.Dal.shards ctxt endorser in
List.Forall
Dal_endorsement_repr.Accountability.shard.Valid.t
(Raw_context.Dal.shards ctxt endorser).
Proof.
Admitted.
*)
End Dal.
[on domain ctxt] implies [t ctxt]
Lemma on_impl_t ctxt domain :
Raw_context.Valid.on domain ctxt →
Raw_context.Valid.t ctxt.
Proof.
unfold Raw_context.Valid.t. intros H_ctxt.
unfold Raw_context.Valid.on in ×.
destruct H_ctxt as [ctxt'].
∃ ctxt'.
Tactics.destruct_conjs.
now split_conj.
Qed.
Raw_context.Valid.on domain ctxt →
Raw_context.Valid.t ctxt.
Proof.
unfold Raw_context.Valid.t. intros H_ctxt.
unfold Raw_context.Valid.on in ×.
destruct H_ctxt as [ctxt'].
∃ ctxt'.
Tactics.destruct_conjs.
now split_conj.
Qed.
If a context simulation [sim_ctxt] is valid in the trivial
domain [fun _ => True], then for every projection [p] and every
function [f], [sim_ctxt <| p := f sim_ctxt.(p) |>] is also valid.
[record <| projection := value |>] is the update notation for
records.
Lemma f_preserves_context_trivial_validity `{FArgs : Make.FArgs}
{a : Set} (sim_ctxt : Raw_context.t)
(projection : Raw_context.t → Make.t a) (f : Make.t a → Make.t a) :
Raw_context.Valid.t (Raw_context.to_t sim_ctxt) →
Raw_context.Valid.t (Raw_context.to_t
sim_ctxt <| projection := f sim_ctxt.(projection) |>).
Proof.
eauto.
Qed.
{a : Set} (sim_ctxt : Raw_context.t)
(projection : Raw_context.t → Make.t a) (f : Make.t a → Make.t a) :
Raw_context.Valid.t (Raw_context.to_t sim_ctxt) →
Raw_context.Valid.t (Raw_context.to_t
sim_ctxt <| projection := f sim_ctxt.(projection) |>).
Proof.
eauto.
Qed.
If [domain1] implies [domain2] for every simulated context
[sim_ctxt], then [Raw_context.Valid.on domain1 ctxt] implies
[Raw_context.Valid.on domain2 ctxt]
Lemma domain_impl_ctxt (domain1 domain2 : Raw_context.t → Prop)
ctxt :
(∀ sim_ctxt, domain1 sim_ctxt → domain2 sim_ctxt) →
Raw_context.Valid.on domain1 ctxt →
Raw_context.Valid.on domain2 ctxt.
Proof.
intros H_domain H_ctxt.
Raw_context.Valid.destruct_rewrite H_ctxt.
specialize (H_domain sim_ctxt).
unfold Raw_context.Valid.on in ×.
eauto.
Qed.
ctxt :
(∀ sim_ctxt, domain1 sim_ctxt → domain2 sim_ctxt) →
Raw_context.Valid.on domain1 ctxt →
Raw_context.Valid.on domain2 ctxt.
Proof.
intros H_domain H_ctxt.
Raw_context.Valid.destruct_rewrite H_ctxt.
specialize (H_domain sim_ctxt).
unfold Raw_context.Valid.on in ×.
eauto.
Qed.
If [domain1] implies [domain2] for the specific simulated
context [sim_ctxt], then [Raw_context.Valid.on domain1 ctxt] implies
[Raw_context.Valid.on domain2 ctxt]
Lemma domain_impl_sim_ctxt (domain1 domain2 : Raw_context.t → Prop)
sim_ctxt :
(domain1 sim_ctxt → domain2 sim_ctxt) →
Raw_context.Valid.on domain1 (Raw_context.to_t sim_ctxt) →
Raw_context.Valid.on domain2 (Raw_context.to_t sim_ctxt).
Proof.
intros H_domain H_ctxt.
unfold Raw_context.Valid.on in ×.
Raw_context.Valid.destruct_rewrite H_ctxt.
destruct H_ctxt as [sim_ctxt' H_ctxt'].
destruct H_ctxt' as [H_sim_ctxt_eq' ?].
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq'.
subst sim_ctxt0.
∃ sim_ctxt'.
split_conj; [reflexivity|assumption|].
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq.
subst sim_ctxt'.
now apply H_domain.
Qed.
sim_ctxt :
(domain1 sim_ctxt → domain2 sim_ctxt) →
Raw_context.Valid.on domain1 (Raw_context.to_t sim_ctxt) →
Raw_context.Valid.on domain2 (Raw_context.to_t sim_ctxt).
Proof.
intros H_domain H_ctxt.
unfold Raw_context.Valid.on in ×.
Raw_context.Valid.destruct_rewrite H_ctxt.
destruct H_ctxt as [sim_ctxt' H_ctxt'].
destruct H_ctxt' as [H_sim_ctxt_eq' ?].
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq'.
subst sim_ctxt0.
∃ sim_ctxt'.
split_conj; [reflexivity|assumption|].
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq.
subst sim_ctxt'.
now apply H_domain.
Qed.
This tactic makes it easier to apply the lemma
[domain_impl_sim_ctxt] by searching the domains in
the proof context and the current goal. It expects
a goal in the form [Raw_context.Valid.on domain2
(Raw_context.to_t sim_ctxt)] and [H_ctxt] should
also have the same form.
Ltac apply_domain_impl_sim_ctxt H_ctxt :=
match type of H_ctxt with
| Raw_context.Valid.on ?domain1 (Raw_context.to_t ?sim_ctxt) ⇒
match goal with
| |- Raw_context.Valid.on
?domain2 (Raw_context.to_t ?sim_ctxt) ⇒
apply (Raw_context.domain_impl_sim_ctxt domain1 domain2
sim_ctxt); [|assumption]
end
end.
match type of H_ctxt with
| Raw_context.Valid.on ?domain1 (Raw_context.to_t ?sim_ctxt) ⇒
match goal with
| |- Raw_context.Valid.on
?domain2 (Raw_context.to_t ?sim_ctxt) ⇒
apply (Raw_context.domain_impl_sim_ctxt domain1 domain2
sim_ctxt); [|assumption]
end
end.
If you have two domains [domain1] and [domain2], you can glue
them together into a conjunction
[fun sim_ctxt => domain1 sim_ctxt /\ domain2 sim_ctxt]
Lemma domain_conj {ctxt domain1 domain2} :
Raw_context.Valid.on domain1 ctxt →
Raw_context.Valid.on domain2 ctxt →
Raw_context.Valid.on
(fun sim_ctxt ⇒ domain1 sim_ctxt ∧ domain2 sim_ctxt) ctxt.
Proof.
intros H1 H2.
Raw_context.Valid.destruct_rewrite H1.
unfold Raw_context.Valid.on.
∃ sim_ctxt; split_conj; try easy.
Raw_context.Valid.destruct_rewrite H2.
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq0.
subst sim_ctxt. easy.
Qed.
Raw_context.Valid.on domain1 ctxt →
Raw_context.Valid.on domain2 ctxt →
Raw_context.Valid.on
(fun sim_ctxt ⇒ domain1 sim_ctxt ∧ domain2 sim_ctxt) ctxt.
Proof.
intros H1 H2.
Raw_context.Valid.destruct_rewrite H1.
unfold Raw_context.Valid.on.
∃ sim_ctxt; split_conj; try easy.
Raw_context.Valid.destruct_rewrite H2.
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq0.
subst sim_ctxt. easy.
Qed.
If `sim_ctxt` is in the domains
[fun sim_ctxt => key_exists key subkey sim_ctxt.(projection)] and
[fun sim_ctxt => if_value_exists P key subkey sim_ctxt.(projection)]
then `sim_ctxt` is also in the domain
[fun sim_ctxt => value_exists P key subkey sim_ctxt.(projection)]
Lemma key_exists_impl_value_exists
{k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
{proj1 :
Raw_context.t →
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)}
(key : k) (subkey : k')
(ctxt : Proto_alpha.Raw_context.t)
(P : v → Prop) :
Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.key_exists
key subkey sim_ctxt.(proj1)) ctxt →
Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.if_value_exists P
key subkey sim_ctxt.(proj1)) ctxt →
Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.value_exists
P key subkey sim_ctxt.(proj1))
ctxt.
Proof.
intros H_ctxt1 H_ctxt2.
Raw_context.Valid.destruct_rewrite H_ctxt1.
Raw_context.Valid.destruct_rewrite H_ctxt2.
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq0.
subst sim_ctxt0.
∃ sim_ctxt; split_conj; try easy.
now apply Raw_context.Nested_indexed_data_storage
.key_exists_and_if_value_exists_impl_value_exists.
Qed.
{k k' v : Set}
{index : Path_encoding.S (t := k)}
{index' : Path_encoding.S (t := k')}
{proj1 :
Raw_context.t →
Map.Make_t (Storage_sigs.Indexed_map.Ord index)
(Map.Make_t (Storage_sigs.Indexed_map.Ord index') v)}
(key : k) (subkey : k')
(ctxt : Proto_alpha.Raw_context.t)
(P : v → Prop) :
Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.key_exists
key subkey sim_ctxt.(proj1)) ctxt →
Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.if_value_exists P
key subkey sim_ctxt.(proj1)) ctxt →
Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.value_exists
P key subkey sim_ctxt.(proj1))
ctxt.
Proof.
intros H_ctxt1 H_ctxt2.
Raw_context.Valid.destruct_rewrite H_ctxt1.
Raw_context.Valid.destruct_rewrite H_ctxt2.
apply Raw_context.to_t_is_injective in H_sim_ctxt_eq0.
subst sim_ctxt0.
∃ sim_ctxt; split_conj; try easy.
now apply Raw_context.Nested_indexed_data_storage
.key_exists_and_if_value_exists_impl_value_exists.
Qed.