🐆 Tx_rollup_l2_context.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context.
Require TezosOfOCaml.Environment.V8.Proofs.Bls.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_storage_sig.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context.
Require TezosOfOCaml.Environment.V8.Proofs.Bls.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_l2_storage_sig.
The encoding [metadata_encoding] is valid.
Lemma metadata_encoding_is_valid :
Data_encoding.Valid.t Tx_rollup_l2_context_sig.metadata.Valid.t
Tx_rollup_l2_context.metadata_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Admitted.
#[global] Hint Resolve metadata_encoding_is_valid : Data_encoding_db.
Module key.
Module Valid.
Data_encoding.Valid.t Tx_rollup_l2_context_sig.metadata.Valid.t
Tx_rollup_l2_context.metadata_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Admitted.
#[global] Hint Resolve metadata_encoding_is_valid : Data_encoding_db.
Module key.
Module Valid.
Validity predicate for [key].
Definition t (x : Tx_rollup_l2_context.key) : Prop :=
match x with
| Tx_rollup_l2_context.Address_metadata address ⇒
Tx_rollup_l2_context_sig.address_index.Valid.t address
| Tx_rollup_l2_context.Address_count ⇒ True
| Tx_rollup_l2_context.Address_index _ ⇒ True
| Tx_rollup_l2_context.Ticket_count ⇒ True
| Tx_rollup_l2_context.Ticket_index _ ⇒ True
| Tx_rollup_l2_context.Ticket_ledger ticket address ⇒
Tx_rollup_l2_context_sig.ticket_index.Valid.t ticket ∧
Tx_rollup_l2_context_sig.address_index.Valid.t address
end.
End Valid.
End key.
Module packed_key.
Module Valid.
match x with
| Tx_rollup_l2_context.Address_metadata address ⇒
Tx_rollup_l2_context_sig.address_index.Valid.t address
| Tx_rollup_l2_context.Address_count ⇒ True
| Tx_rollup_l2_context.Address_index _ ⇒ True
| Tx_rollup_l2_context.Ticket_count ⇒ True
| Tx_rollup_l2_context.Ticket_index _ ⇒ True
| Tx_rollup_l2_context.Ticket_ledger ticket address ⇒
Tx_rollup_l2_context_sig.ticket_index.Valid.t ticket ∧
Tx_rollup_l2_context_sig.address_index.Valid.t address
end.
End Valid.
End key.
Module packed_key.
Module Valid.
Validity predicate for [packed_key].
Definition t (x : Tx_rollup_l2_context.packed_key) : Prop :=
match x with
| Tx_rollup_l2_context.Key key ⇒ key.Valid.t key
end.
End Valid.
End packed_key.
match x with
| Tx_rollup_l2_context.Key key ⇒ key.Valid.t key
end.
End Valid.
End packed_key.
The encoding [packed_key_encoding] is valid.
Lemma packed_key_encoding_is_valid :
Data_encoding.Valid.t packed_key.Valid.t
Tx_rollup_l2_context.packed_key_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [[]] ?; simpl in *; try easy.
destruct_all Tx_rollup_l2_context_sig.ticket_index; simpl in *; try easy.
repeat split; try lia.
easy.
Qed.
#[global] Hint Resolve packed_key_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t packed_key.Valid.t
Tx_rollup_l2_context.packed_key_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros [[]] ?; simpl in *; try easy.
destruct_all Tx_rollup_l2_context_sig.ticket_index; simpl in *; try easy.
repeat split; try lia.
easy.
Qed.
#[global] Hint Resolve packed_key_encoding_is_valid : Data_encoding_db.
Type corresponding to a [key].
Definition key_to_Set (x : Tx_rollup_l2_context.key) : Set :=
match x with
| Tx_rollup_l2_context.Address_metadata _ ⇒ Tx_rollup_l2_context_sig.metadata
| Tx_rollup_l2_context.Address_count ⇒ int32
| Tx_rollup_l2_context.Address_index _ ⇒ Tx_rollup_l2_address.Indexable.t
| Tx_rollup_l2_context.Ticket_count ⇒ int32
| Tx_rollup_l2_context.Ticket_index _ ⇒
Indexable.t Ticket_hash_repr.t
| Tx_rollup_l2_context.Ticket_ledger _ _ ⇒ Tx_rollup_l2_qty.t
end.
Module key_to_Set.
Module Valid.
match x with
| Tx_rollup_l2_context.Address_metadata _ ⇒ Tx_rollup_l2_context_sig.metadata
| Tx_rollup_l2_context.Address_count ⇒ int32
| Tx_rollup_l2_context.Address_index _ ⇒ Tx_rollup_l2_address.Indexable.t
| Tx_rollup_l2_context.Ticket_count ⇒ int32
| Tx_rollup_l2_context.Ticket_index _ ⇒
Indexable.t Ticket_hash_repr.t
| Tx_rollup_l2_context.Ticket_ledger _ _ ⇒ Tx_rollup_l2_qty.t
end.
Module key_to_Set.
Module Valid.
Validity predicate for the type corresponding to a [key].
Definition t (key : Tx_rollup_l2_context.key) : key_to_Set key → Prop :=
match key with
| Tx_rollup_l2_context.Address_metadata _ ⇒
Tx_rollup_l2_context_sig.metadata.Valid.t
| Tx_rollup_l2_context.Address_count ⇒ Int32.Valid.non_negative
| Tx_rollup_l2_context.Address_index _ ⇒ Indexable.Index.Valid.t
| Tx_rollup_l2_context.Ticket_count ⇒ Int32.Valid.non_negative
| Tx_rollup_l2_context.Ticket_index _ ⇒ Indexable.Index.Valid.t
| Tx_rollup_l2_context.Ticket_ledger _ _ ⇒ Tx_rollup_l2_qty.Valid.t
end.
End Valid.
End key_to_Set.
match key with
| Tx_rollup_l2_context.Address_metadata _ ⇒
Tx_rollup_l2_context_sig.metadata.Valid.t
| Tx_rollup_l2_context.Address_count ⇒ Int32.Valid.non_negative
| Tx_rollup_l2_context.Address_index _ ⇒ Indexable.Index.Valid.t
| Tx_rollup_l2_context.Ticket_count ⇒ Int32.Valid.non_negative
| Tx_rollup_l2_context.Ticket_index _ ⇒ Indexable.Index.Valid.t
| Tx_rollup_l2_context.Ticket_ledger _ _ ⇒ Tx_rollup_l2_qty.Valid.t
end.
End Valid.
End key_to_Set.
The generator of encodings [value_encoding] is valid.
Lemma value_encoding_is_valid key :
Data_encoding.Valid.t (key_to_Set.Valid.t key)
(Tx_rollup_l2_context.value_encoding (a := key_to_Set key) key).
Proof.
destruct key; simpl; rewrite cast_eval;
Data_encoding.Valid.data_encoding_auto.
{ lia. }
{ lia. }
{ intros [] ?; simpl in *; try easy.
split; lia.
}
Qed.
#[global] Hint Resolve value_encoding_is_valid : Data_encoding_db.
Module Make.
Import Proto_alpha.Tx_rollup_l2_context.Make.
Section Make.
Context `{FArgs}
(P_t : S_t → Prop)
(with_post : ∀ {a : Set}, (a → Prop) → S_m a → Prop)
(H_S : Tx_rollup_l2_storage_sig.STORAGE.Valid.t P_t (@with_post) S).
Arguments with_post {_}.
Data_encoding.Valid.t (key_to_Set.Valid.t key)
(Tx_rollup_l2_context.value_encoding (a := key_to_Set key) key).
Proof.
destruct key; simpl; rewrite cast_eval;
Data_encoding.Valid.data_encoding_auto.
{ lia. }
{ lia. }
{ intros [] ?; simpl in *; try easy.
split; lia.
}
Qed.
#[global] Hint Resolve value_encoding_is_valid : Data_encoding_db.
Module Make.
Import Proto_alpha.Tx_rollup_l2_context.Make.
Section Make.
Context `{FArgs}
(P_t : S_t → Prop)
(with_post : ∀ {a : Set}, (a → Prop) → S_m a → Prop)
(H_S : Tx_rollup_l2_storage_sig.STORAGE.Valid.t P_t (@with_post) S).
Arguments with_post {_}.
The module [Syntax] is valid.
Lemma Syntax_is_valid :
Tx_rollup_l2_context_sig.SYNTAX.Valid.t (@with_post) Syntax.
Proof.
sfirstorder.
Qed.
Tx_rollup_l2_context_sig.SYNTAX.Valid.t (@with_post) Syntax.
Proof.
sfirstorder.
Qed.
The function [bls_verify] is valid.
Lemma bls_verify_is_valid l signature :
with_post (fun _ ⇒ True) (bls_verify l signature).
Proof.
sfirstorder.
Qed.
with_post (fun _ ⇒ True) (bls_verify l signature).
Proof.
sfirstorder.
Qed.
The function [unwrap_or] is valid.
Lemma unwrap_or_is_valid {a : Set} (P : a → Prop) (opt : option a) err
(H_opt : Option.Forall P opt)
(H_err : Error.not_internal [err]) :
with_post P (unwrap_or opt err).
Proof.
destruct opt; simpl in *; now apply Syntax_is_valid.
Qed.
(H_opt : Option.Forall P opt)
(H_err : Error.not_internal [err]) :
with_post P (unwrap_or opt err).
Proof.
destruct opt; simpl in *; now apply Syntax_is_valid.
Qed.
The function [serialize_key] is valid.
Lemma serialize_key_is_valid key_value
(H_key_value : key.Valid.t key_value) :
with_post (fun _ ⇒ True) (serialize_key key_value).
Proof.
unfold serialize_key, unwrap_or.
destruct packed_key_encoding_is_valid.
pose proof (of_bytes_opt_to_bytes_opt
(Tx_rollup_l2_context.Key key_value) H_key_value
).
destruct Data_encoding.Binary.to_bytes_opt; [|contradiction].
now apply Syntax_is_valid.
Qed.
(H_key_value : key.Valid.t key_value) :
with_post (fun _ ⇒ True) (serialize_key key_value).
Proof.
unfold serialize_key, unwrap_or.
destruct packed_key_encoding_is_valid.
pose proof (of_bytes_opt_to_bytes_opt
(Tx_rollup_l2_context.Key key_value) H_key_value
).
destruct Data_encoding.Binary.to_bytes_opt; [|contradiction].
now apply Syntax_is_valid.
Qed.
The function [serialize_value] is valid.
Lemma serialize_value_is_valid {a : Set} (P : a → Prop) encoding value
(H_encoding : Data_encoding.Valid.t P encoding)
(H_value : P value) :
with_post (fun _ ⇒ True) (serialize_value encoding value).
Proof.
unfold serialize_value, unwrap_or.
destruct H_encoding.
pose proof (of_bytes_opt_to_bytes_opt value H_value).
destruct Data_encoding.Binary.to_bytes_opt; now apply Syntax_is_valid.
Qed.
(H_encoding : Data_encoding.Valid.t P encoding)
(H_value : P value) :
with_post (fun _ ⇒ True) (serialize_value encoding value).
Proof.
unfold serialize_value, unwrap_or.
destruct H_encoding.
pose proof (of_bytes_opt_to_bytes_opt value H_value).
destruct Data_encoding.Binary.to_bytes_opt; now apply Syntax_is_valid.
Qed.
The function [deserialize_value] is valid.
Lemma deserialize_value_is_valid {a : Set} (P : a → Prop) encoding value
(H_encoding : Data_encoding.Valid.t P encoding) :
with_post P (deserialize_value encoding value).
Proof.
unfold deserialize_value, unwrap_or.
destruct H_encoding.
pose proof (to_bytes_opt_of_bytes_opt value).
destruct Data_encoding.Binary.of_bytes_opt; now apply Syntax_is_valid.
Qed.
(H_encoding : Data_encoding.Valid.t P encoding) :
with_post P (deserialize_value encoding value).
Proof.
unfold deserialize_value, unwrap_or.
destruct H_encoding.
pose proof (to_bytes_opt_of_bytes_opt value).
destruct Data_encoding.Binary.of_bytes_opt; now apply Syntax_is_valid.
Qed.
The function [get] is valid.
Lemma get_is_valid ctxt key_value
(H_ctxt : P_t ctxt)
(H_key_value : key.Valid.t key_value) :
with_post (Option.Forall (key_to_Set.Valid.t key_value))
(get ctxt key_value).
Proof.
unfold get.
eapply Syntax_is_valid. {
now apply serialize_key_is_valid.
}
intros.
eapply Syntax_is_valid. {
now apply H_S.
}
intros [] ?.
{ eapply Syntax_is_valid. {
apply deserialize_value_is_valid.
apply value_encoding_is_valid.
}
intros.
now apply Syntax_is_valid.
}
{ now apply Syntax_is_valid. }
Qed.
(H_ctxt : P_t ctxt)
(H_key_value : key.Valid.t key_value) :
with_post (Option.Forall (key_to_Set.Valid.t key_value))
(get ctxt key_value).
Proof.
unfold get.
eapply Syntax_is_valid. {
now apply serialize_key_is_valid.
}
intros.
eapply Syntax_is_valid. {
now apply H_S.
}
intros [] ?.
{ eapply Syntax_is_valid. {
apply deserialize_value_is_valid.
apply value_encoding_is_valid.
}
intros.
now apply Syntax_is_valid.
}
{ now apply Syntax_is_valid. }
Qed.
The function [set] is valid.
Lemma set_is_valid ctxt key_value value
(H_ctxt : P_t ctxt)
(H_key_value : key.Valid.t key_value)
(H_value : key_to_Set.Valid.t key_value value) :
with_post P_t (set ctxt key_value value).
Proof.
unfold set.
eapply Syntax_is_valid. {
now apply serialize_key_is_valid.
}
intros.
eapply Syntax_is_valid. {
apply serialize_value_is_valid with (P := key_to_Set.Valid.t key_value);
try easy.
apply value_encoding_is_valid.
}
intros.
now apply H_S.
Qed.
(H_ctxt : P_t ctxt)
(H_key_value : key.Valid.t key_value)
(H_value : key_to_Set.Valid.t key_value value) :
with_post P_t (set ctxt key_value value).
Proof.
unfold set.
eapply Syntax_is_valid. {
now apply serialize_key_is_valid.
}
intros.
eapply Syntax_is_valid. {
apply serialize_value_is_valid with (P := key_to_Set.Valid.t key_value);
try easy.
apply value_encoding_is_valid.
}
intros.
now apply H_S.
Qed.
The function [remove] is valid.
Lemma remove_is_valid ctxt key_value
(H_ctxt : P_t ctxt)
(H_key_value : key.Valid.t key_value) :
with_post P_t (remove ctxt key_value).
Proof.
unfold remove.
eapply Syntax_is_valid. {
now apply serialize_key_is_valid.
}
intros.
now apply H_S.
Qed.
(H_ctxt : P_t ctxt)
(H_key_value : key.Valid.t key_value) :
with_post P_t (remove ctxt key_value).
Proof.
unfold remove.
eapply Syntax_is_valid. {
now apply serialize_key_is_valid.
}
intros.
now apply H_S.
Qed.
The function [Address_metadata.get] is valid.
Lemma Address_metadata_get_is_valid ctxt index
(H_ctxt : P_t ctxt)
(H_index : Tx_rollup_l2_context_sig.address_index.Valid.t index) :
with_post (Option.Forall Tx_rollup_l2_context_sig.metadata.Valid.t)
(Address_metadata.get ctxt index).
Proof.
unfold Address_metadata.get.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Address_metadata index).
Qed.
(H_ctxt : P_t ctxt)
(H_index : Tx_rollup_l2_context_sig.address_index.Valid.t index) :
with_post (Option.Forall Tx_rollup_l2_context_sig.metadata.Valid.t)
(Address_metadata.get ctxt index).
Proof.
unfold Address_metadata.get.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Address_metadata index).
Qed.
The module [Address_metadata] is valid.
Lemma Address_metadata_is_valid :
Tx_rollup_l2_context_sig.ADDRESS_METADATA.Valid.t P_t (@with_post)
Address_metadata.
Proof.
constructor; intros; simpl.
{ grep Address_metadata.get.
now apply Address_metadata_get_is_valid.
}
{ grep Address_metadata.incr_counter.
unfold Address_metadata.incr_counter.
eapply Syntax_is_valid. {
now apply Address_metadata_get_is_valid.
}
intros [] ?; simpl in ×.
{ eapply Syntax_is_valid with (P := fun _ ⇒ True). {
destruct (_ >=? _); simpl; now apply Syntax_is_valid.
}
intros.
apply set_is_valid; simpl; try easy.
constructor; simpl.
lia.
}
{ now apply Syntax_is_valid. }
}
{ grep Address_metadata.init_with_public_key.
unfold Address_metadata.init_with_public_key.
eapply Syntax_is_valid. {
now apply Address_metadata_get_is_valid.
}
intros [] ?; simpl in ×.
{ now apply Syntax_is_valid. }
{ now apply set_is_valid. }
}
Qed.
Tx_rollup_l2_context_sig.ADDRESS_METADATA.Valid.t P_t (@with_post)
Address_metadata.
Proof.
constructor; intros; simpl.
{ grep Address_metadata.get.
now apply Address_metadata_get_is_valid.
}
{ grep Address_metadata.incr_counter.
unfold Address_metadata.incr_counter.
eapply Syntax_is_valid. {
now apply Address_metadata_get_is_valid.
}
intros [] ?; simpl in ×.
{ eapply Syntax_is_valid with (P := fun _ ⇒ True). {
destruct (_ >=? _); simpl; now apply Syntax_is_valid.
}
intros.
apply set_is_valid; simpl; try easy.
constructor; simpl.
lia.
}
{ now apply Syntax_is_valid. }
}
{ grep Address_metadata.init_with_public_key.
unfold Address_metadata.init_with_public_key.
eapply Syntax_is_valid. {
now apply Address_metadata_get_is_valid.
}
intros [] ?; simpl in ×.
{ now apply Syntax_is_valid. }
{ now apply set_is_valid. }
}
Qed.
The function [Address_index.count] is valid.
Lemma Address_index_count_is_valid ctxt
(H_ctxt : P_t ctxt) :
with_post Int32.Valid.non_negative (Address_index.count ctxt).
Proof.
eapply Syntax_is_valid. {
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Address_count).
}
now intros [] ?.
Qed.
(H_ctxt : P_t ctxt) :
with_post Int32.Valid.non_negative (Address_index.count ctxt).
Proof.
eapply Syntax_is_valid. {
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Address_count).
}
now intros [] ?.
Qed.
The function [Address_index.associate_index] is valid.
Lemma Address_index_associate_index_is_valid ctxt addr
(H_ctxt : P_t ctxt) :
with_post
(fun '(ctxt, index) ⇒
P_t ctxt ∧
Tx_rollup_l2_context_sig.address_index.Valid.t index
)
(Address_index.associate_index ctxt addr).
Proof.
unfold Address_index.associate_index.
eapply Syntax_is_valid. {
now apply Address_index_count_is_valid.
}
intros i_value H_i_value.
eapply Syntax_is_valid with
(P := fun _ ⇒ Int32.succ i_value ≥ i_value). {
destruct (_ ≥i32 _) eqn:?; simpl; apply Syntax_is_valid; [lia|easy].
}
intros.
unfold Indexable.index_exn, Indexable.index_value.
eapply Syntax_is_valid. {
apply set_is_valid; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
}
intros.
eapply Syntax_is_valid. {
apply set_is_valid; simpl; try easy.
lia.
}
intros.
split; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
Qed.
(H_ctxt : P_t ctxt) :
with_post
(fun '(ctxt, index) ⇒
P_t ctxt ∧
Tx_rollup_l2_context_sig.address_index.Valid.t index
)
(Address_index.associate_index ctxt addr).
Proof.
unfold Address_index.associate_index.
eapply Syntax_is_valid. {
now apply Address_index_count_is_valid.
}
intros i_value H_i_value.
eapply Syntax_is_valid with
(P := fun _ ⇒ Int32.succ i_value ≥ i_value). {
destruct (_ ≥i32 _) eqn:?; simpl; apply Syntax_is_valid; [lia|easy].
}
intros.
unfold Indexable.index_exn, Indexable.index_value.
eapply Syntax_is_valid. {
apply set_is_valid; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
}
intros.
eapply Syntax_is_valid. {
apply set_is_valid; simpl; try easy.
lia.
}
intros.
split; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
Qed.
The function [Address_index.get] is valid.
Lemma Address_index_get_is_valid ctxt addr
(H_ctxt : P_t ctxt) :
with_post (Option.Forall Tx_rollup_l2_context_sig.address_index.Valid.t)
(Address_index.get ctxt addr).
Proof.
unfold Address_index.get.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Address_index addr).
Qed.
(H_ctxt : P_t ctxt) :
with_post (Option.Forall Tx_rollup_l2_context_sig.address_index.Valid.t)
(Address_index.get ctxt addr).
Proof.
unfold Address_index.get.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Address_index addr).
Qed.
The module [Address_index] is valid.
Lemma Address_index_is_valid :
Tx_rollup_l2_context_sig.INDEX.Valid.t
P_t (@with_post)
Tx_rollup_l2_context_sig.address_index.Valid.t
Address_index.
Proof.
constructor; intros; simpl.
{ grep Address_index.init_counter.
unfold Address_index.init_counter.
now apply set_is_valid.
}
{ grep Address_index.get.
now apply Address_index_get_is_valid.
}
{ grep Address_index.get_or_associate_index.
unfold Address_index.get_or_associate_index.
eapply Syntax_is_valid. {
now apply Address_index_get_is_valid.
}
intros [] ?; simpl in ×.
{ now apply Syntax_is_valid. }
{ eapply Syntax_is_valid. {
now apply Address_index_associate_index_is_valid.
}
now intros; Tactics.destruct_pairs.
}
}
{ grep Address_index.count.
now apply Address_index_count_is_valid.
}
Qed.
Tx_rollup_l2_context_sig.INDEX.Valid.t
P_t (@with_post)
Tx_rollup_l2_context_sig.address_index.Valid.t
Address_index.
Proof.
constructor; intros; simpl.
{ grep Address_index.init_counter.
unfold Address_index.init_counter.
now apply set_is_valid.
}
{ grep Address_index.get.
now apply Address_index_get_is_valid.
}
{ grep Address_index.get_or_associate_index.
unfold Address_index.get_or_associate_index.
eapply Syntax_is_valid. {
now apply Address_index_get_is_valid.
}
intros [] ?; simpl in ×.
{ now apply Syntax_is_valid. }
{ eapply Syntax_is_valid. {
now apply Address_index_associate_index_is_valid.
}
now intros; Tactics.destruct_pairs.
}
}
{ grep Address_index.count.
now apply Address_index_count_is_valid.
}
Qed.
The function [Ticket_index.count] is valid.
Lemma Ticket_index_count_is_valid ctxt
(H_ctxt : P_t ctxt) :
with_post Int32.Valid.non_negative (Ticket_index.count ctxt).
Proof.
eapply Syntax_is_valid. {
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Ticket_count).
}
now intros [] ?.
Qed.
(H_ctxt : P_t ctxt) :
with_post Int32.Valid.non_negative (Ticket_index.count ctxt).
Proof.
eapply Syntax_is_valid. {
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Ticket_count).
}
now intros [] ?.
Qed.
The function [Ticket_index.associate_index] is valid.
Lemma Ticket_index_associate_index_is_valid ctxt addr
(H_ctxt : P_t ctxt) :
with_post
(fun '(ctxt, index) ⇒
P_t ctxt ∧
Tx_rollup_l2_context_sig.ticket_index.Valid.t index
)
(Ticket_index.associate_index ctxt addr).
Proof.
unfold Ticket_index.associate_index.
eapply Syntax_is_valid. {
now apply Ticket_index_count_is_valid.
}
intros i_value H_i_value.
eapply Syntax_is_valid with
(P := fun _ ⇒ Int32.succ i_value ≥ i_value). {
destruct (_ ≥i32 _) eqn:?; simpl; apply Syntax_is_valid; [lia|easy].
}
intros.
unfold Indexable.index_exn, Indexable.index_value.
eapply Syntax_is_valid. {
apply set_is_valid; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
}
intros.
eapply Syntax_is_valid. {
apply set_is_valid; simpl; try easy.
lia.
}
intros.
split; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
Qed.
(H_ctxt : P_t ctxt) :
with_post
(fun '(ctxt, index) ⇒
P_t ctxt ∧
Tx_rollup_l2_context_sig.ticket_index.Valid.t index
)
(Ticket_index.associate_index ctxt addr).
Proof.
unfold Ticket_index.associate_index.
eapply Syntax_is_valid. {
now apply Ticket_index_count_is_valid.
}
intros i_value H_i_value.
eapply Syntax_is_valid with
(P := fun _ ⇒ Int32.succ i_value ≥ i_value). {
destruct (_ ≥i32 _) eqn:?; simpl; apply Syntax_is_valid; [lia|easy].
}
intros.
unfold Indexable.index_exn, Indexable.index_value.
eapply Syntax_is_valid. {
apply set_is_valid; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
}
intros.
eapply Syntax_is_valid. {
apply set_is_valid; simpl; try easy.
lia.
}
intros.
split; try easy.
destruct (_ ≤i32 _) eqn:?; simpl; lia.
Qed.
The function [Ticket_index.get] is valid.
Lemma Ticket_index_get_is_valid ctxt addr
(H_ctxt : P_t ctxt) :
with_post (Option.Forall Tx_rollup_l2_context_sig.ticket_index.Valid.t)
(Ticket_index.get ctxt addr).
Proof.
unfold Ticket_index.get.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Ticket_index addr).
Qed.
(H_ctxt : P_t ctxt) :
with_post (Option.Forall Tx_rollup_l2_context_sig.ticket_index.Valid.t)
(Ticket_index.get ctxt addr).
Proof.
unfold Ticket_index.get.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Ticket_index addr).
Qed.
The module [Ticket_index] is valid.
Lemma Ticket_index_is_valid :
Tx_rollup_l2_context_sig.INDEX.Valid.t
P_t (@with_post)
Tx_rollup_l2_context_sig.ticket_index.Valid.t
Ticket_index.
Proof.
constructor; intros; simpl.
{ grep Ticket_index.init_counter.
unfold Ticket_index.init_counter.
now apply set_is_valid.
}
{ grep Ticket_index.get.
now apply Ticket_index_get_is_valid.
}
{ grep Ticket_index.get_or_associate_index.
unfold Ticket_index.get_or_associate_index.
eapply Syntax_is_valid. {
now apply Ticket_index_get_is_valid.
}
intros [] ?; simpl in ×.
{ now apply Syntax_is_valid. }
{ eapply Syntax_is_valid. {
now apply Ticket_index_associate_index_is_valid.
}
now intros; Tactics.destruct_pairs.
}
}
{ grep Ticket_index.count.
now apply Ticket_index_count_is_valid.
}
Qed.
Tx_rollup_l2_context_sig.INDEX.Valid.t
P_t (@with_post)
Tx_rollup_l2_context_sig.ticket_index.Valid.t
Ticket_index.
Proof.
constructor; intros; simpl.
{ grep Ticket_index.init_counter.
unfold Ticket_index.init_counter.
now apply set_is_valid.
}
{ grep Ticket_index.get.
now apply Ticket_index_get_is_valid.
}
{ grep Ticket_index.get_or_associate_index.
unfold Ticket_index.get_or_associate_index.
eapply Syntax_is_valid. {
now apply Ticket_index_get_is_valid.
}
intros [] ?; simpl in ×.
{ now apply Syntax_is_valid. }
{ eapply Syntax_is_valid. {
now apply Ticket_index_associate_index_is_valid.
}
now intros; Tactics.destruct_pairs.
}
}
{ grep Ticket_index.count.
now apply Ticket_index_count_is_valid.
}
Qed.
The function [Ticket_ledger.get_opt] is valid.
Lemma Ticket_ledger_get_opt_is_valid ctxt tidx aidx
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
with_post (Option.Forall Tx_rollup_l2_qty.Valid.t)
(Ticket_ledger.get_opt ctxt tidx aidx).
Proof.
unfold Ticket_ledger.get_opt.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Ticket_ledger tidx aidx).
Qed.
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
with_post (Option.Forall Tx_rollup_l2_qty.Valid.t)
(Ticket_ledger.get_opt ctxt tidx aidx).
Proof.
unfold Ticket_ledger.get_opt.
now apply get_is_valid with
(key_value := Tx_rollup_l2_context.Ticket_ledger tidx aidx).
Qed.
The function [Ticket_ledger.get] is valid.
Lemma Ticket_ledger_get_is_valid ctxt tidx aidx
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
with_post Tx_rollup_l2_qty.Valid.t (Ticket_ledger.get ctxt tidx aidx).
Proof.
unfold Ticket_ledger.get.
eapply Syntax_is_valid. {
now apply Ticket_ledger_get_opt_is_valid.
}
now intros [] ?; simpl in ×.
Qed.
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
with_post Tx_rollup_l2_qty.Valid.t (Ticket_ledger.get ctxt tidx aidx).
Proof.
unfold Ticket_ledger.get.
eapply Syntax_is_valid. {
now apply Ticket_ledger_get_opt_is_valid.
}
now intros [] ?; simpl in ×.
Qed.
The function [Ticket_ledger.set] is valid.
Lemma Ticket_ledger_set_is_valid ctxt tidx aidx qty
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx)
(H_qty : Tx_rollup_l2_qty.Valid.t qty) :
with_post P_t (Ticket_ledger.set ctxt tidx aidx qty).
Proof.
unfold Ticket_ledger.set.
now apply set_is_valid.
Qed.
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx)
(H_qty : Tx_rollup_l2_qty.Valid.t qty) :
with_post P_t (Ticket_ledger.set ctxt tidx aidx qty).
Proof.
unfold Ticket_ledger.set.
now apply set_is_valid.
Qed.
The function [Ticket_ledger.remove] is valid.
Lemma Ticket_ledger_remove_is_valid ctxt tidx aidx
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
with_post P_t (Ticket_ledger.remove ctxt tidx aidx).
Proof.
unfold Ticket_ledger.remove.
now apply remove_is_valid.
Qed.
(H_ctxt : P_t ctxt)
(H_tidx : Tx_rollup_l2_context_sig.ticket_index.Valid.t tidx)
(H_aidx : Tx_rollup_l2_context_sig.address_index.Valid.t aidx) :
with_post P_t (Ticket_ledger.remove ctxt tidx aidx).
Proof.
unfold Ticket_ledger.remove.
now apply remove_is_valid.
Qed.
The module [Ticket_ledger] is valid.
Lemma Ticket_ledger_is_valid :
Tx_rollup_l2_context_sig.TICKET_LEDGER.Valid.t
P_t (@with_post)
Ticket_ledger.
Proof.
constructor; intros; simpl.
{ grep Ticket_ledger.get.
now apply Ticket_ledger_get_is_valid.
}
{ grep Ticket_ledger.credit.
eapply Syntax_is_valid. {
now apply Ticket_ledger_get_is_valid.
}
intros.
step.
{ apply Ticket_ledger_set_is_valid; try easy.
hauto l: on use: Tx_rollup_l2_qty.add_is_valid.
}
{ now apply Syntax_is_valid. }
}
{ grep Ticket_ledger.spend.
eapply Syntax_is_valid. {
now apply Ticket_ledger_get_is_valid.
}
intros.
step.
{ step; [
apply Ticket_ledger_set_is_valid |
apply Ticket_ledger_remove_is_valid
]; try easy.
hauto l: on use: Tx_rollup_l2_qty.sub_is_valid.
}
{ now apply Syntax_is_valid. }
}
Qed.
Tx_rollup_l2_context_sig.TICKET_LEDGER.Valid.t
P_t (@with_post)
Ticket_ledger.
Proof.
constructor; intros; simpl.
{ grep Ticket_ledger.get.
now apply Ticket_ledger_get_is_valid.
}
{ grep Ticket_ledger.credit.
eapply Syntax_is_valid. {
now apply Ticket_ledger_get_is_valid.
}
intros.
step.
{ apply Ticket_ledger_set_is_valid; try easy.
hauto l: on use: Tx_rollup_l2_qty.add_is_valid.
}
{ now apply Syntax_is_valid. }
}
{ grep Ticket_ledger.spend.
eapply Syntax_is_valid. {
now apply Ticket_ledger_get_is_valid.
}
intros.
step.
{ step; [
apply Ticket_ledger_set_is_valid |
apply Ticket_ledger_remove_is_valid
]; try easy.
hauto l: on use: Tx_rollup_l2_qty.sub_is_valid.
}
{ now apply Syntax_is_valid. }
}
Qed.
The functor [functor] is valid.
Lemma functor_is_valid :
Tx_rollup_l2_context_sig.CONTEXT.Valid.t P_t (@with_post) functor.
Proof.
constructor; simpl.
{ apply Syntax_is_valid. }
{ apply bls_verify_is_valid. }
{ apply Address_metadata_is_valid. }
{ apply Address_index_is_valid. }
{ apply Ticket_index_is_valid. }
{ apply Ticket_ledger_is_valid. }
Qed.
End Make.
End Make.
Tx_rollup_l2_context_sig.CONTEXT.Valid.t P_t (@with_post) functor.
Proof.
constructor; simpl.
{ apply Syntax_is_valid. }
{ apply bls_verify_is_valid. }
{ apply Address_metadata_is_valid. }
{ apply Address_index_is_valid. }
{ apply Ticket_index_is_valid. }
{ apply Ticket_ledger_is_valid. }
Qed.
End Make.
End Make.
The functor [Make] is valid.
Lemma Make_is_valid {S_t : Set} {S_m : Set → Set}
(P_t : S_t → Prop)
(with_post : ∀ {a : Set}, (a → Prop) → S_m a → Prop)
(S : Tx_rollup_l2_storage_sig.STORAGE (t := S_t) (m := S_m))
(H_S : Tx_rollup_l2_storage_sig.STORAGE.Valid.t P_t (@with_post) S) :
Tx_rollup_l2_context_sig.CONTEXT.Valid.t P_t (@with_post)
(Tx_rollup_l2_context.Make S).
Proof.
now apply Make.functor_is_valid.
Qed.
(P_t : S_t → Prop)
(with_post : ∀ {a : Set}, (a → Prop) → S_m a → Prop)
(S : Tx_rollup_l2_storage_sig.STORAGE (t := S_t) (m := S_m))
(H_S : Tx_rollup_l2_storage_sig.STORAGE.Valid.t P_t (@with_post) S) :
Tx_rollup_l2_context_sig.CONTEXT.Valid.t P_t (@with_post)
(Tx_rollup_l2_context.Make S).
Proof.
now apply Make.functor_is_valid.
Qed.