Skip to main content

🧠 Cache_repr.v

Proofs

See code, Gitlab , OCaml

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 iCache_repr.string_of_internal_identifier
                  (Cache_repr.internal_identifier_of_string s) = s
    | NoneTrue
    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.