🔥 Carbonated_map_costs.v
Translated 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.
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
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.
: 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).
(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)).
Gas_limit_repr.op_plusat (S.safe_int 50)
(Gas_limit_repr.op_starat (S.safe_int 24) (S.safe_int size_value)).