🧠 Cache_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Cache_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Pervasives.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.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.
∀ {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
| None ⇒ True
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.
∀ {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
| None ⇒ True
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.
Raw_context.Valid.t ctxt →
letP? _ := Cache_repr.Admin.value_of_key ctxt key_value in
True.
Proof.
Admitted.
End Admin.