🇿 Zk_rollup_account_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Plonk.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Module static.
Module Valid.
Import Proto_alpha.Zk_rollup_account_repr.static.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Plonk.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_account_repr.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_state_repr.
Module static.
Module Valid.
Import Proto_alpha.Zk_rollup_account_repr.static.
The validity predicate for [Zk_rollup_account_repr.static]
Record t (x : Zk_rollup_account_repr.static) : Prop := {
state_length : Pervasives.Int31.Valid.t x.(state_length);
circuits_info : True; (* sorted x.(circuits_info *)
nb_ops : Pervasives.Int31.Valid.t x.(nb_ops);
}.
End Valid.
End static.
Module dynamic.
Module Valid.
Import Proto_alpha.Zk_rollup_account_repr.dynamic.
state_length : Pervasives.Int31.Valid.t x.(state_length);
circuits_info : True; (* sorted x.(circuits_info *)
nb_ops : Pervasives.Int31.Valid.t x.(nb_ops);
}.
End Valid.
End static.
Module dynamic.
Module Valid.
Import Proto_alpha.Zk_rollup_account_repr.dynamic.
The validity predicate for [Zk_rollup_account_repr.dynamic]
Record t (x : Zk_rollup_account_repr.dynamic) : Prop := {
dynamic_paid : 0 ≤ x.(paid_l2_operations_storage_space);
dynamic_used : 0 ≤ x.(used_l2_operations_storage_space);
}.
End Valid.
End dynamic.
Module Valid.
Import Zk_rollup_account_repr.t.
dynamic_paid : 0 ≤ x.(paid_l2_operations_storage_space);
dynamic_used : 0 ≤ x.(used_l2_operations_storage_space);
}.
End Valid.
End dynamic.
Module Valid.
Import Zk_rollup_account_repr.t.
Valid predicate for [Zk_rollup_account_repr.t]
Record t (x : Zk_rollup_account_repr.t) : Prop := {
static : static.Valid.t x.(static);
dynamic : dynamic.Valid.t x.(dynamic);
}.
End Valid.
static : static.Valid.t x.(static);
dynamic : dynamic.Valid.t x.(dynamic);
}.
End Valid.
The encoding [circuits_info_encoding] is valid
Lemma circuits_info_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True)
Zk_rollup_account_repr.circuits_info_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
(* TODO *)
(*
intros [x] H_Valid. destruct H_Valid, static.
repeat match goal with
| |- _ /\ _ => split
end; trivial; try assumption.
3, 4 : sauto lq: on.
{ destruct x.
match goal with
| |- Forall _ ?arg =>
generalize arg
end.
induction l; [easy|].
constructor; [now step|assumption].
}
{ unfold Zk_rollup_account_repr.SMap.
destruct x; cbn in *.
with_strategy transparent [Map.Make] unfold Map.Make; cbn.
unfold Make.bindings.
apply Map.of_seq_node_to_seq_node_eq.
}
*)
Admitted.
#[global] Hint Resolve circuits_info_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t (fun _ ⇒ True)
Zk_rollup_account_repr.circuits_info_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
(* TODO *)
(*
intros [x] H_Valid. destruct H_Valid, static.
repeat match goal with
| |- _ /\ _ => split
end; trivial; try assumption.
3, 4 : sauto lq: on.
{ destruct x.
match goal with
| |- Forall _ ?arg =>
generalize arg
end.
induction l; [easy|].
constructor; [now step|assumption].
}
{ unfold Zk_rollup_account_repr.SMap.
destruct x; cbn in *.
with_strategy transparent [Map.Make] unfold Map.Make; cbn.
unfold Make.bindings.
apply Map.of_seq_node_to_seq_node_eq.
}
*)
Admitted.
#[global] Hint Resolve circuits_info_encoding_is_valid : Data_encoding_db.
[Zk_rollup_account_repr.encoding] is valid
Lemma encoding_is_valid :
Data_encoding.Valid.t Valid.t Zk_rollup_account_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t Valid.t Zk_rollup_account_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.