🦏 Sc_rollup_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Blake2B.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Bounded.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.

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

[compare] function is valid

  Lemma compare_is_valid :
    Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.Address.compare.
  Proof. apply Blake2B.Make_is_valid. Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.

Propositional equality and [equal] are equivalent on [Address.t].

  Lemma equal_is_valid :
    Compare.Equal.Valid.t (fun _ ⇒ True) Sc_rollup_repr.Address.equal.
  Proof.
    apply Blake2B.Make_equal_is_valid.
  Qed.

  Lemma of_b58_opt_to_b58_eq v :
    Sc_rollup_repr.Address.of_b58check_opt
      (Sc_rollup_repr.Address.to_b58check v) = return× v.
  Proof.
    unfold Make_t.
    match goal with
    | [v : Make_t ?R0 ?N0 |- _] ⇒ pose R0 as R ; pose N0 as N ;
      destruct (Blake2B.Make_is_valid R N) as [ _ _ B58_DATA _]
    end.
    destruct B58_DATA. rewrite of_to_b58_check. reflexivity.
  Qed.

  Lemma to_b58_opt_of_b58_eq b58 :
  match Sc_rollup_repr.Address.of_b58check_opt b58 with
  | Some v ⇒ Sc_rollup_repr.Address.to_b58check v = b58
  | None ⇒ True
  end.
  Proof.
    unfold Sc_rollup_repr.Address.of_b58check_opt.
    unfold Sc_rollup_repr.Address.H.

Now that [Sc_rollup_repr.Address.H.] has been unfolded *once*, we can read the parameters of [Make_t] and fold them to clean the proof.

    match goal with
    | |- context [Make_t ?R0 ?N0] ⇒ pose R0 as R ; pose N0 as N ;
      destruct (Blake2B.Make_is_valid R N) as [ _ _ B58_DATA _]
    end.
    destruct B58_DATA.
    unfold Sc_rollup_repr.Address.to_b58check.
    unfold Sc_rollup_repr.Address.H.
    fold R. fold N.
    apply to_of_b58_check.
  Qed.

  Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True)
                          Sc_rollup_repr.Address.rpc_arg.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.
End Address.

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

[compare] function is valid

  Lemma compare_is_valid :
    Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.State_hash.compare.
  Proof. apply Blake2B.Make_is_valid. Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End State_hash.

Axiom of_b58_to_b58_eq : ∀ s,
    Sc_rollup_repr.of_b58check
      (Sc_rollup_repr.Address.to_b58check s) = return? s.

Axiom to_b58_of_b58_eq : ∀ b58,
  match Sc_rollup_repr.of_b58check b58 with
  | Pervasives.Ok v ⇒ Sc_rollup_repr.Address.to_b58check v = b58
  | Pervasives.Error _ ⇒ True
  end.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros; split; trivial.
  apply of_b58_to_b58_eq.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True) Sc_rollup_repr.rpc_arg.
Proof.
  constructor; intros; simpl.
  { rewrite of_b58_to_b58_eq; reflexivity. }
  { destruct (Sc_rollup_repr.of_b58check s) eqn:E; simpl; trivial.
    specialize (to_b58_of_b58_eq s); rewrite E; trivial. }
Qed.

Lemma index_path_encoding_is_valid :
  Path_encoding.S.Valid.t
    (Storage_description.INDEX.to_Path Sc_rollup_repr.Index).
Proof.
  constructor;
    unfold
      Sc_rollup_repr.Index,
      Sc_rollup_repr.Index.module,
      Sc_rollup_repr.Index.to_path,
      Sc_rollup_repr.Index.of_path,
      Binary.to_bytes_exn,
      Sc_rollup_repr.Index.path_length; simpl.
  { intros; destruct (Hex.of_bytes _ _); reflexivity. }
  { intro v; destruct (Hex.of_bytes _ _) eqn:E;
      rewrite <- E, Hex.to_bytes_of_bytes; clear E; simpl.
    specialize
      (Data_encoding.Valid.of_bytes_opt_to_bytes_opt encoding_is_valid v I).
    destruct (Binary.to_bytes_opt _ _ _) eqn:E; [|contradiction];
      intro Epath; rewrite Epath; reflexivity.
  }
  { intro path; destruct path; simpl; trivial; destruct path; simpl; trivial.
    destruct (Hex.to_bytes _) eqn:E; simpl; trivial;
    specialize (Hex.of_bytes_to_bytes (Hex.Hex s)); rewrite E; intro;
      specialize
        (Data_encoding.Valid.to_bytes_opt_of_bytes_opt encoding_is_valid b);
    destruct (Binary.of_bytes_opt _ _) eqn:E1; simpl; trivial.
    hauto lq: on.
  }
  { intros; destruct (Hex.of_bytes None _); reflexivity. }
Qed.

Module Index.

[compare] function is valid

  Lemma compare_is_valid :
    Compare.Valid.t (fun _ ⇒ True) id Sc_rollup_repr.Index.compare.
  Proof. apply Blake2B.Make_is_valid. Qed.
  #[global] Hint Resolve compare_is_valid : Compare_db.
End Index.

Module Number_of_ticks.

The bounds [Number_of_ticks] are valid.

  Lemma is_valid :
    Bounded.S.Valid.t Int64.Valid.t
      Sc_rollup_repr.Number_of_ticks.Bounded_Int64_include.
  Proof.
    apply Bounded.Int64_is_Valid.
    constructor; simpl; lia.
  Qed.

The corresponding encoding is valid.

  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True)
      Sc_rollup_repr.Number_of_ticks.Bounded_Int64_include.(S.encoding).
  Proof.
    apply is_valid.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Number_of_ticks.

(* TODO: missing module Sc_rollup_repr.Kind
Module Kind.
  Lemma encoding_is_valid
    : Data_encoding.Valid.t (fun _ => True) Sc_rollup_repr.Kind.encoding.
    Data_encoding.Valid.data_encoding_auto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Kind.
*)