Skip to main content

🇿 Zk_rollup_operation_repr.v

Proofs

See code, Gitlab , OCaml

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.