🔥 Carbonated_map_costs.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.

Module S := Saturation_repr.

Definition cost : Set := Saturation_repr.t.

This is a good enough approximation

Definition log2 (x_value : S.t) : S.t := S.safe_int (1 +i (S.numbits x_value)).

Collect benchmark from [Carbonated_map_benchmarks.Find_benchmark].

The model is similar to the gas model as from [Michelson_v1_gas.map_get]. The user is responsible for providing the [compare_key_cost] which depends on the size of the [key]. See [Carbonated_map_benchmarks.Find_benchmark] for an example. The rational for the model is: [intercept] is for paying a fixed cost regardless of size. [compare_key_cost] is for the log2 of steps comparing keys [traversal_overhead] is for the overhead of log2 steps walking the tree

Definition find_cost (compare_key_cost : Gas_limit_repr.cost) (size_value : int)
  : Gas_limit_repr.cost :=
  let intercept := S.safe_int 50 in
  let size_value := S.safe_int size_value in
  let compare_cost :=
    Gas_limit_repr.op_starat (log2 size_value) compare_key_cost in
  let traversal_overhead :=
    Gas_limit_repr.op_starat (log2 size_value) (S.safe_int 2) in
  Gas_limit_repr.op_plusat (Gas_limit_repr.op_plusat intercept compare_cost)
    traversal_overhead.

Modelling the precise overhead of update compared with [find] is tricky. The cost of [find] depends on the cost of comparing keys. When the tree is recreated, after looking up the element, this cost is no longer a factor. On the other hand, if the old map is no longer used, some nodes are going to be garbage collected at a later stage which incurs an extra cost.

We here use the same model as in [Michelson_v1_gas.map_update]. That is providing an overestimate by doubling the cost of [find].

Definition update_cost
  (compare_key_cost : Gas_limit_repr.cost) (size_value : int)
  : Gas_limit_repr.cost :=
  Gas_limit_repr.op_starat (S.safe_int 2)
    (find_cost compare_key_cost size_value).

Collect benchmark from [Carbonated_map_benchmarks.Fold_benchmark].

The cost of producing a list of elements is linear in the size of the map and does not depend on the size of the elements nor keys.

Definition fold_cost (size_value : int) : Gas_limit_repr.cost :=
  Gas_limit_repr.op_plusat (S.safe_int 50)
    (Gas_limit_repr.op_starat (S.safe_int 24) (S.safe_int size_value)).