🧠 Cache_memory_helpers.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.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.

Module SNodes.
  Record signature : Set := {
    t := int;
    zero : t;
    one : t;
    succ : t → t;
    add : t → t → t;
    to_int : t → int;
  }.
End SNodes.
Definition SNodes := SNodes.signature.

The [Nodes] module is used to count the number of computation steps performed when evaluating the size of the in-memory graph corresponding to an OCaml value.

In first approximation, the value of type [Nodes.t] threaded through {!expr_size} below and through the module {!Script_typed_ir_size} is meant to match the number of recursive calls in the [traverse] functions of {!Script_typed_ir} and in that of {!node_size}.

The assumption is that there's a bounded amount of work performed between two such recursive calls, hence that the total work is bounded above by something proportional to the [Nodes.t] accumulator.

Computations on values of type [Nodes.t] do not overflow, as they are bounded above by the number of nodes traversed when computing an OCaml value.

Module Nodes.
  Definition t : Set := int.

  Definition zero : int := 0.

  Definition one : int := 1.

  Definition succ (x_value : int) : int := x_value +i 1.

  Definition add (x_value : int) (y_value : int) : int := x_value +i y_value.

  Definition to_int {A : Set} (x_value : A) : A := x_value.

  (* Nodes *)
  Definition module :=
    {|
      SNodes.zero := zero;
      SNodes.one := one;
      SNodes.succ := succ;
      SNodes.add := add;
      SNodes.to_int := to_int
    |}.
End Nodes.
Definition Nodes : SNodes := Nodes.module.

Definition sint : Set := Saturation_repr.t.

Definition nodes_and_size : Set := int × sint.

Definition op_exclamationexclamation : int → Saturation_repr.t :=
  Saturation_repr.safe_int.

Definition op_plusexclamation
  : Saturation_repr.t → Saturation_repr.t → Saturation_repr.t :=
  Saturation_repr.add.

Definition op_plusquestion (s_value : Saturation_repr.t) (x_value : int)
  : Saturation_repr.t :=
  Saturation_repr.add s_value (op_exclamationexclamation x_value).

Definition op_starquestion (s_value : Saturation_repr.t) (x_value : int)
  : Saturation_repr.t :=
  Saturation_repr.mul s_value (op_exclamationexclamation x_value).

Definition op_divquestion (s_value : Saturation_repr.t) (x_value : int)
  : Saturation_repr.t :=
  Saturation_repr.ediv s_value (op_exclamationexclamation x_value).

Definition op_plusplus (function_parameter : int × Saturation_repr.t)
  : int × Saturation_repr.t → int × Saturation_repr.t :=
  let '(n1, s1) := function_parameter in
  fun (function_parameter : int × Saturation_repr.t) ⇒
    let '(n2, s2) := function_parameter in
    ((Nodes.(SNodes.add) n1 n2), (op_plusexclamation s1 s2)).

Definition zero : int × Saturation_repr.t :=
  (Nodes.(SNodes.zero), (op_exclamationexclamation 0)).

Definition word_size : Saturation_repr.t := op_exclamationexclamation 8.

Definition header_size : Saturation_repr.t := word_size.

Definition int32_size : Saturation_repr.t :=
  op_plusexclamation header_size word_size.

Definition int64_size : Saturation_repr.t :=
  op_plusexclamation header_size (op_starquestion word_size 2).

Definition h1w : Saturation_repr.t := op_plusexclamation header_size word_size.

Definition h2w : Saturation_repr.t :=
  op_plusexclamation header_size (op_starquestion word_size 2).

Definition h3w : Saturation_repr.t :=
  op_plusexclamation header_size (op_starquestion word_size 3).

Definition h4w : Saturation_repr.t :=
  op_plusexclamation header_size (op_starquestion word_size 4).

Definition h5w : Saturation_repr.t :=
  op_plusexclamation header_size (op_starquestion word_size 5).

Definition hh3w : Saturation_repr.t :=
  op_plusexclamation (op_starquestion word_size 3)
    (op_starquestion header_size 2).

Definition hh6w : Saturation_repr.t :=
  op_plusexclamation (op_starquestion word_size 6)
    (op_starquestion header_size 2).

Definition hh8w : Saturation_repr.t :=
  op_plusexclamation (op_starquestion word_size 8)
    (op_starquestion header_size 2).

Definition z_size (z_value : Z.t) : Saturation_repr.t :=
  let numbits := Z.numbits z_value in
  if numbits ≤i 62 then
    op_exclamationexclamation 0
  else
    op_plusquestion (op_starquestion word_size (Z.size_value z_value)) 32.

Definition string_size_gen (len : int) : Saturation_repr.t :=
  op_plusquestion header_size (len +i (8 -i (Pervasives._mod len 8))).

Definition bytes_size (b_value : bytes) : Saturation_repr.t :=
  string_size_gen (Bytes.length b_value).

Definition string_size (s_value : string) : Saturation_repr.t :=
  string_size_gen (String.length s_value).

Definition blake2b_hash_size : Saturation_repr.t :=
  op_plusexclamation h1w (string_size_gen 20).

Definition public_key_hash_in_memory_size : Saturation_repr.t :=
  op_plusexclamation h1w blake2b_hash_size.

Definition ret_adding {A : Set} (function_parameter : A × Saturation_repr.t)
  : Saturation_repr.t → A × Saturation_repr.t :=
  let '(nodes, size_value) := function_parameter in
  fun (added : Saturation_repr.t) ⇒
    (nodes, (op_plusexclamation size_value added)).

Definition ret_succ_adding (function_parameter : int × Saturation_repr.t)
  : Saturation_repr.t → int × Saturation_repr.t :=
  let '(nodes, size_value) := function_parameter in
  fun (added : Saturation_repr.t) ⇒
    ((Nodes.(SNodes.succ) nodes), (op_plusexclamation size_value added)).

Definition ret_succ {A : Set} (function_parameter : int × A) : int × A :=
  let '(nodes, size_value) := function_parameter in
  ((Nodes.(SNodes.succ) nodes), size_value).

Definition option_size {A : Set}
  (some : A → Saturation_repr.t) (x_value : option A) : Saturation_repr.t :=
  let some (x_value : A) : Saturation_repr.t :=
    op_plusexclamation h1w (some x_value) in
  Option.fold (op_exclamationexclamation 0) some x_value.

Definition option_size_vec {A : Set}
  (some : A → int × Saturation_repr.t) (x_value : option A)
  : int × Saturation_repr.t :=
  let some (x_value : A) : int × Saturation_repr.t :=
    ret_adding (some x_value) h1w in
  Option.fold zero some x_value.

Definition list_cell_size (elt_size : Saturation_repr.t) : Saturation_repr.t :=
  op_plusexclamation
    (op_plusexclamation (op_plusexclamation header_size word_size) word_size)
    elt_size.

Definition list_fold_size {A : Set}
  (elt_size : A → int × Saturation_repr.t) (list_value : list A)
  : int × Saturation_repr.t :=
  List.fold_left
    (fun (accu_value : int × Saturation_repr.t) ⇒
      fun (elt_value : A) ⇒
        ret_succ_adding (op_plusplus accu_value (elt_size elt_value)) h2w) zero
    list_value.

Definition boxed_tup2
  (x_value : Saturation_repr.t) (y_value : Saturation_repr.t)
  : Saturation_repr.t :=
  op_plusexclamation
    (op_plusexclamation
      (op_plusexclamation (op_plusexclamation header_size word_size) word_size)
      x_value) y_value.

Definition node_size {A B : Set}
  : Micheline.node A B → int × Saturation_repr.t :=
  let list_size {C : Set} (sns : list C) : Saturation_repr.t :=
    op_starquestion word_size ((List.length sns) ×i 3) in
  let annotation_size (a_value : list string) : int × Saturation_repr.t :=
    List.fold_left
      (fun (accu_value : int × Saturation_repr.t) ⇒
        fun (s_value : string) ⇒
          ret_succ_adding accu_value
            (op_plusexclamation h2w (string_size s_value))) zero a_value in
  let internal_node_size {C D : Set} (function_parameter : Micheline.node C D)
    : int × Saturation_repr.t :=
    match function_parameter with
    | Micheline.Int _ z_value ⇒
      (Nodes.(SNodes.one), (op_plusexclamation h2w (z_size z_value)))
    | Micheline.String _ s_value ⇒
      (Nodes.(SNodes.one), (op_plusexclamation h2w (string_size s_value)))
    | Micheline.Bytes _ s_value ⇒
      (Nodes.(SNodes.one), (op_plusexclamation h2w (bytes_size s_value)))
    | Micheline.Prim _ _ args a_value ⇒
      ret_succ_adding (annotation_size a_value)
        (op_plusexclamation (list_size args) h4w)
    | Micheline.Seq _ terms ⇒
      (Nodes.(SNodes.one), (op_plusexclamation (list_size terms) h2w))
    end in
  fun (node_value : Micheline.node A B) ⇒
    Script_repr.fold node_value zero
      (fun (accu_value : int × Saturation_repr.t) ⇒
        fun (node_value : Micheline.node A B) ⇒
          op_plusplus accu_value (internal_node_size node_value)).

Definition expr_size {A : Set} (expr : Micheline.canonical A)
  : int × Saturation_repr.t := node_size (Micheline.root_value expr).