Skip to main content

🔥 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
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].
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.