🦏 Sc_rollup_commitment_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Import Error.Tactics_letP.
#[local] Ltac destruct_match :=
match goal with
| H : match ?a with _ ⇒ _ end |-
context [match ?b with _ ⇒ _ end] ⇒
change b with a; destruct a eqn:?
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Import Error.Tactics_letP.
#[local] Ltac destruct_match :=
match goal with
| H : match ?a with _ ⇒ _ end |-
context [match ?b with _ ⇒ _ end] ⇒
change b with a; destruct a eqn:?
end.
The function [get_commitment_opt_unsafe] is valid.
Lemma get_commitment_opt_unsafe_is_valid ctxt rollup commitment
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(commitment, ctxt) :=
Sc_rollup_commitment_storage.get_commitment_opt_unsafe
ctxt rollup commitment in
Option.Forall Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_commitment_opt_unsafe.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db.
destruct H_sim_ctxt. red in Sc_rollup_Commitments.
specialize (Sc_rollup_Commitments rollup commitment).
simpl in ×.
unfold Option.bind.
do 2 (destruct_match; [|split; easy]).
now split.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(commitment, ctxt) :=
Sc_rollup_commitment_storage.get_commitment_opt_unsafe
ctxt rollup commitment in
Option.Forall Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_commitment_opt_unsafe.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db.
destruct H_sim_ctxt. red in Sc_rollup_Commitments.
specialize (Sc_rollup_Commitments rollup commitment).
simpl in ×.
unfold Option.bind.
do 2 (destruct_match; [|split; easy]).
now split.
Qed.
The function [get_commitment_unsafe] is valid
Lemma get_commitment_unsafe_is_valid ctxt rollup commitment :
Raw_context.Valid.t ctxt →
letP? '(commitment, ctxt) :=
Sc_rollup_commitment_storage.get_commitment_unsafe
ctxt rollup commitment in
Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
Raw_context.Valid.t ctxt .
Proof.
intros.
unfold Sc_rollup_commitment_storage.get_commitment_unsafe.
esplit_letP. {
now apply get_commitment_opt_unsafe_is_valid.
}
i_des_pairs.
step; simpl in *; [|reflexivity]. now split.
Qed.
Raw_context.Valid.t ctxt →
letP? '(commitment, ctxt) :=
Sc_rollup_commitment_storage.get_commitment_unsafe
ctxt rollup commitment in
Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
Raw_context.Valid.t ctxt .
Proof.
intros.
unfold Sc_rollup_commitment_storage.get_commitment_unsafe.
esplit_letP. {
now apply get_commitment_opt_unsafe_is_valid.
}
i_des_pairs.
step; simpl in *; [|reflexivity]. now split.
Qed.
The function [last_cemented_commitment] is valid.
Lemma last_cemented_commitment_is_valid ctxt rollup
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_commitment_storage.last_cemented_commitment
ctxt rollup in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.last_cemented_commitment.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db; simpl.
now step.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_commitment_storage.last_cemented_commitment
ctxt rollup in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.last_cemented_commitment.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db; simpl.
now step.
Qed.
The function [get_commitment] is valid.
Lemma get_commitment_is_valid ctxt rollup commitment
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(commitment, ctxt) :=
Sc_rollup_commitment_storage.get_commitment
ctxt rollup commitment in
Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_commitment.
esplit_letP. {
now apply last_cemented_commitment_is_valid.
}
i_des_pairs.
now apply get_commitment_unsafe_is_valid.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(commitment, ctxt) :=
Sc_rollup_commitment_storage.get_commitment
ctxt rollup commitment in
Sc_rollup_commitment_repr.V1.Valid.t commitment ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_commitment.
esplit_letP. {
now apply last_cemented_commitment_is_valid.
}
i_des_pairs.
now apply get_commitment_unsafe_is_valid.
Qed.
The function [last_cemented_commitment_hash_with_level] is
valid.
Lemma last_cemented_commitment_hash_with_level_is_valid ctxt rollup
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, level, ctxt) :=
Sc_rollup_commitment_storage
.last_cemented_commitment_hash_with_level
ctxt rollup in
Raw_level_repr.Valid.t level ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage
.last_cemented_commitment_hash_with_level.
esplit_letP. {
now apply last_cemented_commitment_is_valid.
}
i_des_pairs.
unfold Lwt_result_syntax.op_letplus.
esplit_letP. {
now apply get_commitment_unsafe_is_valid.
}
intros [? ?] [? ?].
simpl.
split; [|easy].
apply_by_type (Sc_rollup_commitment_repr.V1.Valid.t _).
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, level, ctxt) :=
Sc_rollup_commitment_storage
.last_cemented_commitment_hash_with_level
ctxt rollup in
Raw_level_repr.Valid.t level ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage
.last_cemented_commitment_hash_with_level.
esplit_letP. {
now apply last_cemented_commitment_is_valid.
}
i_des_pairs.
unfold Lwt_result_syntax.op_letplus.
esplit_letP. {
now apply get_commitment_unsafe_is_valid.
}
intros [? ?] [? ?].
simpl.
split; [|easy].
apply_by_type (Sc_rollup_commitment_repr.V1.Valid.t _).
Qed.
The function [set_commitment_added] is valid.
Lemma set_commitment_added_is_valid ctxt rollup node_value new_value
(H_ctxt : Raw_context.Valid.t ctxt)
(H_new_value : Raw_level_repr.Valid.t new_value) :
letP? '(size_diff, new_value, ctxt) :=
Sc_rollup_commitment_storage.set_commitment_added
ctxt rollup node_value new_value in
Pervasives.Int.Valid.t size_diff ∧
Raw_level_repr.Valid.t new_value ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.set_commitment_added.
esplit_letP. {
Raw_context.Valid.destruct_rewrite H_ctxt.
simpl. destruct H_sim_ctxt.
rewrite Storage_generated.Sc_rollup.Commitment_added.find.
simpl.
unshelve instantiate (1 := fun '(ctxt, opt_raw_level) ⇒
Raw_context.Valid.t ctxt ∧
Option.Forall Raw_level_repr.Valid.t opt_raw_level
). simpl.
split; [easy|].
unfold Option.bind.
specialize (Sc_rollup_Commitment_added rollup node_value).
simpl in ×.
now do 2 (destruct_match; [|easy]).
}
i_des_pairs.
step; simpl; [now split_conj|].
esplit_letP. {
select (Raw_context.Valid.t _) Raw_context.Valid.destruct_rewrite.
rewrite Storage_generated.Sc_rollup.Commitment_added.add
with (size := 0); simpl.
destruct H_sim_ctxt.
specialize (Sc_rollup_Commitment_added ltac:(assumption)
ltac:(assumption)).
unshelve instantiate (1 := fun '(ctxt, i, b) ⇒
Raw_context.Valid.t ctxt ∧ Pervasives.Int.Valid.t i); simpl.
simpl in ×.
destruct_match; simpl; split; [|easy| |easy];
apply (Raw_context.f_preserves_context_trivial_validity
_ Raw_context.Sc_rollup_Commitment_added
ltac:(eauto) H).
}
i_des_pairs.
simpl. split_conj; easy.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt)
(H_new_value : Raw_level_repr.Valid.t new_value) :
letP? '(size_diff, new_value, ctxt) :=
Sc_rollup_commitment_storage.set_commitment_added
ctxt rollup node_value new_value in
Pervasives.Int.Valid.t size_diff ∧
Raw_level_repr.Valid.t new_value ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.set_commitment_added.
esplit_letP. {
Raw_context.Valid.destruct_rewrite H_ctxt.
simpl. destruct H_sim_ctxt.
rewrite Storage_generated.Sc_rollup.Commitment_added.find.
simpl.
unshelve instantiate (1 := fun '(ctxt, opt_raw_level) ⇒
Raw_context.Valid.t ctxt ∧
Option.Forall Raw_level_repr.Valid.t opt_raw_level
). simpl.
split; [easy|].
unfold Option.bind.
specialize (Sc_rollup_Commitment_added rollup node_value).
simpl in ×.
now do 2 (destruct_match; [|easy]).
}
i_des_pairs.
step; simpl; [now split_conj|].
esplit_letP. {
select (Raw_context.Valid.t _) Raw_context.Valid.destruct_rewrite.
rewrite Storage_generated.Sc_rollup.Commitment_added.add
with (size := 0); simpl.
destruct H_sim_ctxt.
specialize (Sc_rollup_Commitment_added ltac:(assumption)
ltac:(assumption)).
unshelve instantiate (1 := fun '(ctxt, i, b) ⇒
Raw_context.Valid.t ctxt ∧ Pervasives.Int.Valid.t i); simpl.
simpl in ×.
destruct_match; simpl; split; [|easy| |easy];
apply (Raw_context.f_preserves_context_trivial_validity
_ Raw_context.Sc_rollup_Commitment_added
ltac:(eauto) H).
}
i_des_pairs.
simpl. split_conj; easy.
Qed.
The function [get_predecessor_opt_unsafe] is valid.
Lemma get_predecessor_opt_unsafe_is_valid ctxt rollup node_value
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_commitment_storage.get_predecessor_opt_unsafe
ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_predecessor_opt_unsafe.
esplit_letP. {
now apply get_commitment_opt_unsafe_is_valid.
}
now intros [? ?] [? ?].
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_commitment_storage.get_predecessor_opt_unsafe
ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_predecessor_opt_unsafe.
esplit_letP. {
now apply get_commitment_opt_unsafe_is_valid.
}
now intros [? ?] [? ?].
Qed.
The function [get_predecessor_unsafe] is valid.
Lemma get_predecessor_unsafe_is_valid ctxt rollup node_value
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_commitment_storage.get_predecessor_unsafe
ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_predecessor_unsafe.
esplit_letP. {
now apply get_commitment_unsafe_is_valid.
}
now intros [? ?] [? ?].
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(_, ctxt) :=
Sc_rollup_commitment_storage.get_predecessor_unsafe
ctxt rollup node_value in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.get_predecessor_unsafe.
esplit_letP. {
now apply get_commitment_unsafe_is_valid.
}
now intros [? ?] [? ?].
Qed.
The function [hash_value] is valid.
Lemma hash_value_is_valid ctxt commitment
(H_ctxt : Raw_context.Valid.t ctxt)
(H_commitment : Sc_rollup_commitment_repr.V1.Valid.t commitment) :
letP? '(ctxt, _) :=
Sc_rollup_commitment_storage.hash_value ctxt commitment in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.hash_value.
esplit_letP. {
apply Raw_context.consume_gas_is_valid; [easy|].
Raw_context.Valid.destruct_rewrite H_ctxt.
apply Sc_rollup_costs.Constants.cost_serialize_commitment_is_valid.
}
intros.
unfold to_result.
step; simpl; [|reflexivity].
esplit_letP. {
apply Raw_context.consume_gas_is_valid; [easy|].
apply Sc_rollup_costs.Constants.cost_hash_bytes_is_valid.
}
now intros.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt)
(H_commitment : Sc_rollup_commitment_repr.V1.Valid.t commitment) :
letP? '(ctxt, _) :=
Sc_rollup_commitment_storage.hash_value ctxt commitment in
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_commitment_storage.hash_value.
esplit_letP. {
apply Raw_context.consume_gas_is_valid; [easy|].
Raw_context.Valid.destruct_rewrite H_ctxt.
apply Sc_rollup_costs.Constants.cost_serialize_commitment_is_valid.
}
intros.
unfold to_result.
step; simpl; [|reflexivity].
esplit_letP. {
apply Raw_context.consume_gas_is_valid; [easy|].
apply Sc_rollup_costs.Constants.cost_hash_bytes_is_valid.
}
now intros.
Qed.