✒️ Contract_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Contract_repr.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Operation_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.

[compare] function is valid

Lemma compare_is_valid
  : Compare.Valid.t (fun _ ⇒ True) id Contract_repr.compare.
Proof.
  constructor; unfold Contract_repr.compare; simpl;
    unfold id; change (_.(Compare.COMPARABLE.t)) with Contract_repr.t;
    intros;
    try match goal with
    | [H : _ = _ |- _] ⇒ now rewrite H
    end;
    destruct_all Contract_repr.t; simpl in *; try easy;
    try f_equal;
    sfirstorder use:
      Signature.Public_key_hash_compare_is_valid,
      Contract_hash.compare_is_valid.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Lemma in_memory_size_is_valid : ∀ contract,
  Saturation_repr.Valid.t (Contract_repr.in_memory_size contract).
  intros.
  destruct contract; simpl; now apply Saturation_repr.Valid.decide.
Qed.

Axiom of_b58_to_b58_eq : ∀ contract,
  Contract_repr.of_b58check (Contract_repr.to_b58check contract) =
    return? contract.

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

of_b58check_gen implicit_of_b58data (to_b58check x) = x we need this to prove the encoding validity below @TODO: https://gitlab.com/formal-land/coq-tezos-of-ocaml/-/issues/376

Axiom of_b58check_implicit_to_b58check_eq
  : ∀ x,
    Contract_repr.of_b58check_gen
      Contract_repr.implicit_of_b58data
      (Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.to_b58check) x) = return? x.

of_b58check_gen originated_of_b58data (to_b58check x) = x we need this to prove the encoding validity below @TODO: https://gitlab.com/formal-land/coq-tezos-of-ocaml/-/issues/376

Axiom of_b58check_originated_to_b58check_eq
  : ∀ x,
    Contract_repr.of_b58check_gen
      Contract_repr.originated_of_b58data
      (Contract_hash.to_b58check x) = return? x.

Axiom originated_contracts_length :
  ∀ first_nonce last_nonce,
    letP? l := (Contract_repr.originated_contracts first_nonce last_nonce) in
    List.length l
    = Compare.Int.(Compare.S.max) 0 (
        last_nonce.(Origination_nonce.t.origination_index) -
        first_nonce.(Origination_nonce.t.origination_index)).

Lemma rpc_arg_valid : RPC_arg.Valid.t (fun _ ⇒ True) Contract_repr.rpc_arg.
  constructor; intros; simpl.
  { rewrite of_b58_to_b58_eq.
    simpl.
    reflexivity.
  }
  { assert (H := to_b58_of_b58_eq s).
    now destruct (Contract_repr.of_b58check _).
  }
Qed.

Encoding [Contract_repr.implicit_encoding] is valid.

Lemma originated_encoding_is_valid
  : Data_encoding.Valid.t (fun _ ⇒ True) Contract_repr.originated_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros;
    now rewrite of_b58check_originated_to_b58check_eq.
Qed.
#[global] Hint Resolve originated_encoding_is_valid : Data_encoding_db.

Encoding [Contract_repr.encoding] is valid.

Lemma encoding_is_valid : Data_encoding.Valid.t (fun _ ⇒ True) Contract_repr.encoding.
  Data_encoding.Valid.data_encoding_auto;
    try now intros [].
  intros [] ?; try (repeat apply conj; try tauto);
    try rewrite of_b58_to_b58_eq; reflexivity.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Encoding [Contract_repr.implicit_encoding] is valid.

Lemma implicit_encoding_is_valid
  : Data_encoding.Valid.t (fun _ ⇒ True) Contract_repr.implicit_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros;
    now rewrite of_b58check_implicit_to_b58check_eq.
Qed.
#[global] Hint Resolve implicit_encoding_is_valid : Data_encoding_db.

Lemma index_path_encoding_is_valid
  : Path_encoding.S.Valid.t
    (Storage_description.INDEX.to_Path Contract_repr.Index).
Proof.
  constructor; intros; simpl;
    unfold Contract_repr.Index.to_path, Contract_repr.Index.of_path.
  { destruct Hex.of_bytes. reflexivity. }
  { destruct Hex.of_bytes eqn:H0.
    rewrite <- H0.
    rewrite Hex.to_bytes_of_bytes; simpl.
    unfold Binary.to_bytes_exn.
    destruct Binary.to_bytes_opt; apply axiom.
  }
  { destruct path as [|s[]]; simpl; trivial.
    destruct (Hex.to_bytes (Hex.Hex s)) eqn:H_s; simpl; trivial.
    destruct (Binary.of_bytes_opt _ _) eqn:H_b; trivial.
    eassert (H_encoding_to_of :=
      encoding_is_valid.(Data_encoding.Valid.to_bytes_opt_of_bytes_opt) _).
    rewrite H_b in H_encoding_to_of.
    unfold Binary.to_bytes_exn.
    eassert (H_hex_of_to := Hex.of_bytes_to_bytes _).
    rewrite H_s in H_hex_of_to.
    hauto lq: on.
  }
  { now destruct (Hex.of_bytes _ _). }
Qed.

Lemma index_is_valid :
  Storage_description.INDEX.Valid.t (fun _ ⇒ True) Contract_repr.Index.
  constructor;
    try apply index_path_encoding_is_valid;
    try apply encoding_is_valid;
    try apply rpc_arg_valid;
    try apply compare_is_valid.
Qed.

Module Index.

[compare] function is valid

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