🧠 Cache_repr.v

Proofs

See code, Gitlab , OCaml

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

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Pervasives.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.String.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Cache_repr.

Module Cache_costs.
  Lemma minimal_size_of_typed_contract_in_bytes_is_valid :
    ∀ {i : int},
    Pervasives.Int.Valid.t i →
    Saturation_repr.Valid.t
      (Cache_repr.Cache_costs.approximate_cardinal i).
    intros. unfold Cache_repr.Cache_costs.approximate_cardinal.
    apply Saturation_repr.safe_int_is_valid.
  Qed.

  Lemma log2_is_valid :
    ∀ {x : Cache_repr.Cache_costs.S.t},
    Pervasives.Int.Valid.t x →
    Saturation_repr.Valid.t
      (Cache_repr.Cache_costs.log2 x).
    intros.
    unfold Cache_repr.Cache_costs.log2.
    apply Saturation_repr.safe_int_is_valid.
  Qed.

  Lemma cache_update_constant_is_valid :
    Saturation_repr.Valid.t
      Cache_repr.Cache_costs.cache_update_constant.
    apply Saturation_repr.safe_int_is_valid.
  Qed.

  Lemma cache_update_coeff_is_valid :
    Saturation_repr.Valid.t
      Cache_repr.Cache_costs.cache_update_coeff.
    apply Saturation_repr.safe_int_is_valid.
  Qed.

This function is only valid if input is positive

  Lemma cache_update_is_valid :
    ∀ {i : int},
    Saturation_repr.Valid.t i →
    Saturation_repr.Valid.t
      (Cache_repr.Cache_costs.cache_update i).
    intros.
    unfold Cache_repr.Cache_costs.cache_update.
    apply Gas_limit_repr.atomic_step_cost_valid.
    apply Saturation_repr.add_is_valid.
  Qed.

cache_find is an alias to cache_update

  Lemma cache_find_is_valid :
    ∀ {i : int},
    Saturation_repr.Valid.t i →
    Saturation_repr.Valid.t
      (Cache_repr.Cache_costs.cache_find i).
    intros. now apply cache_update_is_valid.
  Qed.
End Cache_costs.

Module Namespace.
  Module Valid.
    Definition t (s : string) : Prop :=
      String.contains s Cache_repr.separator = false.
  End Valid.
End Namespace.

Lemma sanitize_eq : ∀ {s : string},
  Namespace.Valid.t s →
  Cache_repr.sanitize s = s.
  unfold Cache_repr.sanitize, Namespace.Valid.t.
  intros.
  match goal with
  |[|- context [if ?e then _ else _]] ⇒ destruct e eqn:?
  end; [inversion H|reflexivity].
Qed.

Lemma create_namespace_eq : ∀ {s : string},
  Namespace.Valid.t s →
  Cache_repr.create_namespace s = s.
  intros. now apply sanitize_eq.
Qed.

Lemma compare_namespace_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Cache_repr.compare_namespace.
Proof.
  apply Compare.string_is_valid.
Qed.
#[global] Hint Resolve compare_namespace_is_valid : Compare_db.

Module InternalIdentifier.
  Import Cache_repr.internal_identifier.

  Lemma string_of_internal_identifier_eq : ∀ {i : Cache_repr.internal_identifier},
    Cache_repr.string_of_internal_identifier i =
      i.(namespace) ++ (String Cache_repr.separator i.(id)).
    intros i.
    unfold Cache_repr.string_of_internal_identifier.
    simpl. reflexivity.
  Qed.

  Lemma internal_identifier_of_string_eq : ∀ {ns ident : string},
    Namespace.Valid.t ns →
    Cache_repr.internal_identifier_of_string (ns ++ (String Cache_repr.separator ident)) =
    {| namespace := ns; id := ident |}.
    unfold Namespace.Valid.t.
    intros ns ident H.
    unfold Cache_repr.internal_identifier_of_string.
    rewrite String.index_opt_eq; [|assumption].
    f_equal; [now rewrite String.substring_l_eq|now rewrite String.substr_r_eq].
  Qed.

  Lemma string_of_internal_identifier_inverse : ∀ {s : string},
    match String.index_opt s Cache_repr.separator with
    | Some i ⇒ Cache_repr.string_of_internal_identifier
                  (Cache_repr.internal_identifier_of_string s) = s
    | None ⇒ True
    end.
    intros s.
    destruct (String.index_opt _ _) eqn:Eq_index; [|easy].
    unfold Cache_repr.internal_identifier_of_string.
    rewrite Eq_index.
    unfold Cache_repr.string_of_internal_identifier.
    simpl in ×.
    unfold Pervasives.op_caret.
    rewrite String.substr_concat_eq; easy.
  Qed.
End InternalIdentifier.

Ltac remove_assert e default :=
  match eval hnf in e with
  | context f [assert _ false] ⇒
    let x := context f [default] in
    exact x
  end.

Lemma without_assert s (default : Cache_repr.internal_identifier) :
  String.index_opt s Cache_repr.separator ≠ None →
  Cache_repr.internal_identifier_of_string s =
  ltac:(remove_assert (Cache_repr.internal_identifier_of_string s) default).
Proof.
  unfold Cache_repr.internal_identifier_of_string.
  destruct String.index_opt eqn:?; [|easy].
  intros _.
  f_equal.
Qed.