🔥 Carbonated_map_costs.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Carbonated_map_costs.

Require TezosOfOCaml.Proto_alpha.Proofs.Saturation_repr.

The function [log2] is valid.

Lemma log2_is_valid x_value :
  Saturation_repr.Valid.t (Carbonated_map_costs.log2 x_value).
Proof.
  apply Saturation_repr.safe_int_is_valid.
Qed.

The function [find_cost] is valid.

Lemma find_cost_is_valid compare_key_cost size_value :
  Saturation_repr.Valid.t
    (Carbonated_map_costs.find_cost compare_key_cost size_value).
Proof.
  apply Saturation_repr.add_is_valid.
Qed.

The function [update_cost] is valid.

Lemma update_cost_is_valid compare_key_cost size_value :
  Saturation_repr.Valid.t
    (Carbonated_map_costs.update_cost compare_key_cost size_value).
Proof.
  apply Saturation_repr.mul_is_valid; [
    apply Saturation_repr.safe_int_is_valid |
    apply find_cost_is_valid
  ].
Qed.

The function [fold_cost] is valid.

Lemma fold_cost_is_valid size_value :
  Saturation_repr.Valid.t (Carbonated_map_costs.fold_cost size_value).
Proof.
  apply Saturation_repr.add_is_valid.
Qed.