Skip to main content

🇿 Zk_rollup_account_repr.v

Proofs

See code, Gitlab , OCaml

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.

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.

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.

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.

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.

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