Skip to main content

🧠 Cache_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Cache_repr.

Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V7.Proofs.Compare.
Require TezosOfOCaml.Environment.V7.Proofs.String.
Require TezosOfOCaml.Proto_alpha.Proofs.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_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_is_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.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.String Cache_repr.separator ident)) =
    Pervasives.Ok ({| 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].
    now rewrite String.substr_r_eq, String.substring_l_eq.
  Qed.

  Lemma string_of_internal_identifier_inverse : {s : string},
    match String.index_opt s Cache_repr.separator with
    | Some i
        match Cache_repr.internal_identifier_of_string s with
        | Pervasives.Ok ii
            Cache_repr.string_of_internal_identifier ii = s
        | Pervasives.Error _False
        end
    | NoneTrue
    end.
  Proof.
    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.

Module Admin.
The function [value_of_key] is valid.
  Lemma value_of_key_is_valid ctxt key_value :
    Raw_context.Valid.t ctxt
    letP? _ := Cache_repr.Admin.value_of_key ctxt key_value in
    True.
  Proof.
  Admitted.
End Admin.