Skip to main content

✒️ Contract_repr.v

Proofs

See code, Gitlab , OCaml

[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 blake2b_hash_size_is_valid
  : Saturation_repr.Valid.t Contract_repr.blake2b_hash_size.
  now apply Saturation_repr.Valid.decide.
Qed.

Lemma public_key_hash_in_memory_size_is_valid
  : Saturation_repr.Valid.t Contract_repr.public_key_hash_in_memory_size.
  now apply Saturation_repr.Valid.decide.
Qed.

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 contractContract_repr.to_b58check contract = b58
  | Pervasives.Error _True
  end.

Lemma implicit_contract_is_implicit : id,
  Contract_repr.is_implicit (Contract_repr.implicit_contract id) = Some id.
  reflexivity.
Qed.

Lemma implicit_contract_is_not_originated : id,
  Contract_repr.is_originated (Contract_repr.implicit_contract id) = None.
  reflexivity.
Qed.

Axiom originated_contracts_length : first_nonce last_nonce,
  List.length (Contract_repr.originated_contracts first_nonce last_nonce) =
  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.

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.

Lemma index_path_encoding_is_valid
  : Path_encoding.S.Valid.t
    (Storage_description.INDEX.to_Path Contract_repr.Index).
  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[]]; trivial.
    destruct (Hex.to_bytes (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.
    rewrite H_encoding_to_of.
    eassert (H_hex_of_to := Hex.of_bytes_to_bytes _).
    rewrite H_s in H_hex_of_to.
    now rewrite H_hex_of_to.
  - 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.