🇿 Zk_rollup_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Hex.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Module Address.
Import Zk_rollup_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Hex.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Module Address.
Import Zk_rollup_repr.
[Zk_rollup_repr.Address.encoding] is valid
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Address.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Address.
Data_encoding.Valid.t (fun _ ⇒ True) Address.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Address.
Validity predicate of [Zk_rollup_repr.pending_list]
Module pending_list.
Module Valid.
Import Zk_rollup_repr.
Import Zk_rollup_repr.ConstructorRecords_pending_list.pending_list.
Definition t (x : pending_list) : Prop :=
match x with
| Empty e ⇒ Int64.Valid.t e.(Empty.next_index)
| Pending p ⇒ Int64.Valid.t p.(Pending.next_index) ∧
Pervasives.UInt16.Valid.t p.(Pending.length)
end.
End Valid.
End pending_list.
Module Valid.
Import Zk_rollup_repr.
Import Zk_rollup_repr.ConstructorRecords_pending_list.pending_list.
Definition t (x : pending_list) : Prop :=
match x with
| Empty e ⇒ Int64.Valid.t e.(Empty.next_index)
| Pending p ⇒ Int64.Valid.t p.(Pending.next_index) ∧
Pervasives.UInt16.Valid.t p.(Pending.length)
end.
End Valid.
End pending_list.
[pending_list_encoding] is valid
Lemma pending_list_encoding_is_valid :
Data_encoding.Valid.t pending_list.Valid.t Zk_rollup_repr.pending_list_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto;
[|apply Data_encoding.Compact.Valid.make;
apply Data_encoding.Compact.Valid.int64_value..|].
{ unfold Data_encoding.Valid.Matching_function.t.
intros [[]|[]] H_valid;
match goal with
| |- context[Data_encoding.matched None ?tag ?encoding ?payload] ⇒
∃ (existT _ _ (tag, encoding, payload))
end;
repeat constructor.
}
{ hauto l: on. }
Qed.
#[global] Hint Resolve pending_list_encoding_is_valid : Data_encoding_db.
Module Index.
Data_encoding.Valid.t pending_list.Valid.t Zk_rollup_repr.pending_list_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto;
[|apply Data_encoding.Compact.Valid.make;
apply Data_encoding.Compact.Valid.int64_value..|].
{ unfold Data_encoding.Valid.Matching_function.t.
intros [[]|[]] H_valid;
match goal with
| |- context[Data_encoding.matched None ?tag ?encoding ?payload] ⇒
∃ (existT _ _ (tag, encoding, payload))
end;
repeat constructor.
}
{ hauto l: on. }
Qed.
#[global] Hint Resolve pending_list_encoding_is_valid : Data_encoding_db.
Module Index.
[to_path] and [of_path] are inverses
Lemma to_path_of_path_eq c :
Zk_rollup_repr.Index.of_path (Zk_rollup_repr.Index.to_path c []) =
return? (Some c).
Proof.
unfold Zk_rollup_repr.Index.to_path.
step. cbn. rewrite <- Heqt.
rewrite Hex.to_bytes_of_bytes; cbn.
pose proof Address.encoding_is_valid as H_Address.
destruct H_Address.
pose proof (Data_encoding.Valid.of_bytes_opt_to_bytes_exn_eq
(a := Zk_rollup_repr.Address.t) (fun _ ⇒ True)
Zk_rollup_repr.Address.encoding c)
as H_encoding.
match goal with
| |- context [@Binary.of_bytes_opt ?T _ _ ] ⇒
let t := type of H_encoding in
match t with
| context [@Data_encoding.Binary.of_bytes_opt ?T'] ⇒
change T with T' in ×
end
end.
now rewrite H_encoding.
Qed.
Zk_rollup_repr.Index.of_path (Zk_rollup_repr.Index.to_path c []) =
return? (Some c).
Proof.
unfold Zk_rollup_repr.Index.to_path.
step. cbn. rewrite <- Heqt.
rewrite Hex.to_bytes_of_bytes; cbn.
pose proof Address.encoding_is_valid as H_Address.
destruct H_Address.
pose proof (Data_encoding.Valid.of_bytes_opt_to_bytes_exn_eq
(a := Zk_rollup_repr.Address.t) (fun _ ⇒ True)
Zk_rollup_repr.Address.encoding c)
as H_encoding.
match goal with
| |- context [@Binary.of_bytes_opt ?T _ _ ] ⇒
let t := type of H_encoding in
match t with
| context [@Data_encoding.Binary.of_bytes_opt ?T'] ⇒
change T with T' in ×
end
end.
now rewrite H_encoding.
Qed.
[of_path] and [to_path] are inverses
Lemma of_path_to_path_eq path :
letP? ' p := Zk_rollup_repr.Index.of_path path in
match p with
| Some v ⇒ Zk_rollup_repr.Index.to_path v [] = path
| None ⇒ True
end.
Proof.
unfold Zk_rollup_repr.Index.to_path, Zk_rollup_repr.Index.of_path.
destruct path; simpl; [easy|].
destruct path; simpl; [|easy].
match goal with
| |- context[Hex.to_bytes ?h] ⇒
pose proof (Hex.of_bytes_to_bytes h)
end.
destruct Hex.to_bytes; simpl; [|easy].
destruct Address.encoding_is_valid.
match goal with
| |- context[Binary.of_bytes_opt _ ?bytes] ⇒
pose proof (to_bytes_opt_of_bytes_opt bytes)
end.
destruct Binary.of_bytes_opt; [|easy].
unfold Binary.to_bytes_exn.
hauto lq: on.
Qed.
letP? ' p := Zk_rollup_repr.Index.of_path path in
match p with
| Some v ⇒ Zk_rollup_repr.Index.to_path v [] = path
| None ⇒ True
end.
Proof.
unfold Zk_rollup_repr.Index.to_path, Zk_rollup_repr.Index.of_path.
destruct path; simpl; [easy|].
destruct path; simpl; [|easy].
match goal with
| |- context[Hex.to_bytes ?h] ⇒
pose proof (Hex.of_bytes_to_bytes h)
end.
destruct Hex.to_bytes; simpl; [|easy].
destruct Address.encoding_is_valid.
match goal with
| |- context[Binary.of_bytes_opt _ ?bytes] ⇒
pose proof (to_bytes_opt_of_bytes_opt bytes)
end.
destruct Binary.of_bytes_opt; [|easy].
unfold Binary.to_bytes_exn.
hauto lq: on.
Qed.
[rpc_arg] is valid
Lemma rpc_arg_is_valid :
RPC_arg.Valid.t (fun _ ⇒ True ) Zk_rollup_repr.Index.rpc_arg.
Proof.
apply Blake2B.Make_is_valid.
Qed.
RPC_arg.Valid.t (fun _ ⇒ True ) Zk_rollup_repr.Index.rpc_arg.
Proof.
apply Blake2B.Make_is_valid.
Qed.
[encoding] is valid
Lemma encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Zk_rollup_repr.Index.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t (fun _ ⇒ True) Zk_rollup_repr.Index.encoding.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
[compare] is valid
Lemma compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id Zk_rollup_repr.Index.compare.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End Index.
Compare.Valid.t (fun _ ⇒ True) id Zk_rollup_repr.Index.compare.
Proof.
apply Blake2B.Make_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.
End Index.
The index [Index] is valid.
Lemma Index_is_valid :
Storage_description.INDEX.Valid.t (fun _ ⇒ True) Zk_rollup_repr.Index.
Proof.
constructor; simpl.
{ constructor; simpl; intros.
{ reflexivity. }
{ apply Index.to_path_of_path_eq. }
{ apply Index.of_path_to_path_eq. }
{ reflexivity. }
}
{ apply Index.rpc_arg_is_valid. }
{ apply Index.encoding_is_valid. }
{ apply Index.compare_is_valid. }
Qed.
Storage_description.INDEX.Valid.t (fun _ ⇒ True) Zk_rollup_repr.Index.
Proof.
constructor; simpl.
{ constructor; simpl; intros.
{ reflexivity. }
{ apply Index.to_path_of_path_eq. }
{ apply Index.of_path_to_path_eq. }
{ reflexivity. }
}
{ apply Index.rpc_arg_is_valid. }
{ apply Index.encoding_is_valid. }
{ apply Index.compare_is_valid. }
Qed.