🇿 Zk_rollup_repr.v

Proofs

[Zk_rollup_repr.Address.encoding] is valid

  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Address.encoding.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
  #[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 e ⇒ Int64.Valid.t e.(Empty.next_index)
      | Pending p ⇒ Int64.Valid.t p.(Pending.next_index) ∧
         Pervasives.UInt16.Valid.t p.(Pending.length)
      end.
  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.
Proof.
  Data_encoding.Valid.data_encoding_auto;
   [|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))
      end;
      repeat constructor.
  }
  { hauto l: on. }
Qed.
#[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 ).
  Proof.
    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 ×
        end
    end.
    now rewrite H_encoding.
  Qed.

[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 v ⇒ Zk_rollup_repr.Index.to_path v [] = path
    | None ⇒ True
    end.
  Proof.
    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)
    end.
    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)
    end.
    destruct Binary.of_bytes_opt; [|easy].
    unfold Binary.to_bytes_exn.
    hauto lq: on.
  Qed.

[rpc_arg] is valid

  Lemma rpc_arg_is_valid :
    RPC_arg.Valid.t (fun _ ⇒ True ) Zk_rollup_repr.Index.rpc_arg.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.

[encoding] is valid

  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True) Zk_rollup_repr.Index.encoding.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.

[compare] is valid

  Lemma compare_is_valid :
    Compare.Valid.t (fun _ ⇒ True) id Zk_rollup_repr.Index.compare.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
  #[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.
Proof.
  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. }
Qed.