🇿 Zk_rollup_operation_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Environment.V8.Proofs.Plonk.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Zk_rollup_repr.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_operation_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Environment.V8.Proofs.Plonk.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Ticket_hash_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Zk_rollup_repr.
Validity predicate for [Zk_rollup_operation_repr.t]
Module Valid.
Import Zk_rollup_operation_repr.t.
Record t (x : _) : Prop := {
op_code : Pervasives.Int31.Valid.t x.(op_code);
}.
End Valid.
Import Zk_rollup_operation_repr.t.
Record t (x : _) : Prop := {
op_code : Pervasives.Int31.Valid.t x.(op_code);
}.
End Valid.
[Zk_rollup_operation_repr.encoding] is valid
Lemma encoding_is_valid :
Data_encoding.Valid.t Valid.t Zk_rollup_operation_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
admit.
intros [x] []; cbn in ×.
repeat match goal with
| |- _ ∧ _ ⇒ split
end; try step; try easy; try apply H_Valid.
admit.
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t Valid.t Zk_rollup_operation_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
admit.
intros [x] []; cbn in ×.
repeat match goal with
| |- _ ∧ _ ⇒ split
end; try step; try easy; try apply H_Valid.
admit.
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.