🇿 Zk_rollup_operation_repr.v

Proofs

See code, Gitlab , OCaml

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.

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.

[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.