Skip to main content

🇿 Zk_rollup_repr.v


See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Zk_rollup_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Hex.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.

Module Address.
  Import Zk_rollup_repr.
[Zk_rollup_repr.Address.encoding] is valid
  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _True) Address.encoding.
    apply Blake2B.Make_is_valid.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Address.

Validity predicate of [Zk_rollup_repr.pending_list]
Module pending_list.
  Module Valid.
    Import Zk_rollup_repr.
    Import Zk_rollup_repr.ConstructorRecords_pending_list.pending_list.
    Definition t (x : pending_list) : Prop :=
      match x with
      | Empty eInt64.Valid.t e.(Empty.next_index)
      | Pending pInt64.Valid.t p.(Pending.next_index)
         Pervasives.UInt16.Valid.t p.(Pending.length)
  End Valid.
End pending_list.

[pending_list_encoding] is valid
Lemma pending_list_encoding_is_valid :
  Data_encoding.Valid.t pending_list.Valid.t Zk_rollup_repr.pending_list_encoding.
   [|apply Data_encoding.Compact.Valid.make;
    apply Data_encoding.Compact.Valid.int64_value..|].
  { unfold Data_encoding.Valid.Matching_function.t.
    intros [[]|[]] H_valid;
      match goal with
      | |- context[Data_encoding.matched None ?tag ?encoding ?payload] ⇒
         (existT _ _ (tag, encoding, payload))
      repeat constructor.
  { hauto l: on. }
#[global] Hint Resolve pending_list_encoding_is_valid : Data_encoding_db.

Module Index.
[to_path] and [of_path] are inverses
  Lemma to_path_of_path_eq c :
    Zk_rollup_repr.Index.of_path (Zk_rollup_repr.Index.to_path c []) =
    return? (Some c).
    unfold Zk_rollup_repr.Index.to_path.
    step. cbn. rewrite <- Heqt.
    rewrite Hex.to_bytes_of_bytes; cbn.
    pose proof Address.encoding_is_valid as H_Address.
    destruct H_Address.
    pose proof (Data_encoding.Valid.of_bytes_opt_to_bytes_exn_eq
      (a := Zk_rollup_repr.Address.t) (fun _True)
      Zk_rollup_repr.Address.encoding c)
      as H_encoding.
    match goal with
    | |- context [@Binary.of_bytes_opt ?T _ _ ] ⇒
        let t := type of H_encoding in
        match t with
        | context [@Data_encoding.Binary.of_bytes_opt ?T'] ⇒
            change T with T' in ×
    now rewrite H_encoding.

[of_path] and [to_path] are inverses
  Lemma of_path_to_path_eq path :
    letP? ' p := Zk_rollup_repr.Index.of_path path in
    match p with
    | Some vZk_rollup_repr.Index.to_path v [] = path
    | NoneTrue
    unfold Zk_rollup_repr.Index.to_path, Zk_rollup_repr.Index.of_path.
    destruct path; simpl; [easy|].
    destruct path; simpl; [|easy].
    match goal with
    | |- context[Hex.to_bytes ?h] ⇒
      pose proof (Hex.of_bytes_to_bytes h)
    destruct Hex.to_bytes; simpl; [|easy].
    destruct Address.encoding_is_valid.
    match goal with
    | |- context[Binary.of_bytes_opt _ ?bytes] ⇒
      pose proof (to_bytes_opt_of_bytes_opt bytes)
    destruct Binary.of_bytes_opt; [|easy].
    unfold Binary.to_bytes_exn.
    hauto lq: on.

[rpc_arg] is valid
  Lemma rpc_arg_is_valid :
    RPC_arg.Valid.t (fun _True ) Zk_rollup_repr.Index.rpc_arg.
    apply Blake2B.Make_is_valid.

[encoding] is valid
  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _True) Zk_rollup_repr.Index.encoding.
    apply Blake2B.Make_is_valid.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[compare] is valid
  Lemma compare_is_valid :
    Compare.Valid.t (fun _True) id
    apply Blake2B.Make_is_valid.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End Index.

The index [Index] is valid.
Lemma Index_is_valid :
  Storage_description.INDEX.Valid.t (fun _True) Zk_rollup_repr.Index.
  constructor; simpl.
  { constructor; simpl; intros.
    { reflexivity. }
    { apply Index.to_path_of_path_eq. }
    { apply Index.of_path_to_path_eq. }
    { reflexivity. }
  { apply Index.rpc_arg_is_valid. }
  { apply Index.encoding_is_valid. }
  { apply Index.compare_is_valid. }