Skip to main content

🧠 Cache_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Constants_repr.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Voting_period_storage.

Module Cache_costs.
  Module S := Saturation_repr.

  Definition minimal_size_of_typed_contract_in_bytes : int := 688.

  Definition approximate_cardinal (bytes_value : int) : S.t :=
    S.safe_int (bytes_value /i minimal_size_of_typed_contract_in_bytes).

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

  Definition cache_update_constant : S.t := S.safe_int 600.

  Definition cache_update_coeff : S.t := S.safe_int 57.

  Definition cache_update (cache_size_in_bytes : int) : Gas_limit_repr.cost :=
    let approx_card := approximate_cardinal cache_size_in_bytes in
    Gas_limit_repr.atomic_step_cost
      (S.add cache_update_constant (S.mul cache_update_coeff (log2 approx_card))).

  Definition cache_find : int Gas_limit_repr.cost := cache_update.
End Cache_costs.

Definition index : Set := int.

Definition size : Set := int.

Definition identifier : Set := string.

Definition namespace : Set := string.

Definition compare_namespace : string string int :=
  Compare.String.(Compare.S.compare).

Module internal_identifier.
  Record record : Set := Build {
    namespace : namespace;
    id : identifier;
  }.
  Definition with_namespace namespace (r : record) :=
    Build namespace r.(id).
  Definition with_id id (r : record) :=
    Build r.(namespace) id.
End internal_identifier.
Definition internal_identifier := internal_identifier.record.

Definition separator : ascii := "@" % char.

Definition sanitize (namespace_value : string) : string :=
  if String.contains namespace_value separator then
    Pervasives.invalid_arg
      (Format.asprintf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "Invalid cache namespace: '"
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              (CamlinternalFormatBasics.String_literal "'. Character "
                (CamlinternalFormatBasics.Char
                  (CamlinternalFormatBasics.String_literal " is forbidden."
                    CamlinternalFormatBasics.End_of_format)))))
          "Invalid cache namespace: '%s'. Character %c is forbidden.")
        namespace_value separator)
  else
    namespace_value.

Definition create_namespace : string string := sanitize.

Definition string_of_internal_identifier
  (function_parameter : internal_identifier) : string :=
  let '{|
    internal_identifier.namespace := namespace_value;
      internal_identifier.id := id
      |} := function_parameter in
  Pervasives.op_caret namespace_value
    (Pervasives.op_caret (String.make 1 separator) id).

Definition internal_identifier_of_string (raw_value : string)
  : internal_identifier :=
  match String.index_opt raw_value separator with
  | None
    (* ❌ Assert instruction is not handled. *)
    assert internal_identifier false
  | Some index_value
    {| internal_identifier.namespace := String.sub raw_value 0 index_value;
      internal_identifier.id :=
        let delim_idx := index_value +i 1 in
        String.sub raw_value delim_idx ((String.length raw_value) -i delim_idx);
      |}
  end.

Definition internal_identifier_of_key (key_value : Context.cache_key)
  : internal_identifier :=
  let raw_value := Raw_context.Cache.(Context.CACHE.identifier_of_key) key_value
    in
  internal_identifier_of_string raw_value.

Definition key_of_internal_identifier
  (cache_index : int) (identifier : internal_identifier) : Context.cache_key :=
  let raw_value := string_of_internal_identifier identifier in
  Raw_context.Cache.(Context.CACHE.key_of_identifier) cache_index raw_value.

Definition make_key : int String.t identifier Context.cache_key :=
  let namespaces := Pervasives.ref_value nil in
  fun (cache_index : int) ⇒
    fun (namespace_value : String.t) ⇒
      if
        List.mem String.equal namespace_value
          (Pervasives.op_exclamation namespaces)
      then
        Pervasives.invalid_arg
          (Format.sprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Cache key namespace "
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal " already exist."
                    CamlinternalFormatBasics.End_of_format)))
              "Cache key namespace %s already exist.") namespace_value)
      else
        let '_ :=
          Pervasives.op_coloneq namespaces
            (cons namespace_value (Pervasives.op_exclamation namespaces)) in
        fun (id : identifier) ⇒
          let identifier :=
            {| internal_identifier.namespace := namespace_value;
              internal_identifier.id := id; |} in
          key_of_internal_identifier cache_index identifier.

Definition NamespaceMap :=
  Map.Make
    (let t : Set := namespace in
    let compare := compare_namespace in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Definition partial_key_handler : Set :=
  Raw_context.t string M? Context.cache_value.

Definition value_of_key_handlers
  : Pervasives.ref (NamespaceMap.(Map.S.t) partial_key_handler) :=
  Pervasives.ref_value NamespaceMap.(Map.S.empty).

Module Admin.
Inclusion of the module [Raw_context.Cache]
  Definition key := Raw_context.Cache.(Context.CACHE.key).

  Definition value := Raw_context.Cache.(Context.CACHE.value).

  Definition key_of_identifier :=
    Raw_context.Cache.(Context.CACHE.key_of_identifier).

  Definition identifier_of_key :=
    Raw_context.Cache.(Context.CACHE.identifier_of_key).

  Definition pp := Raw_context.Cache.(Context.CACHE.pp).

  Definition find := Raw_context.Cache.(Context.CACHE.find).

  Definition set_cache_layout :=
    Raw_context.Cache.(Context.CACHE.set_cache_layout).

  Definition update := Raw_context.Cache.(Context.CACHE.update).

  Definition sync := Raw_context.Cache.(Context.CACHE.sync).

  Definition clear := Raw_context.Cache.(Context.CACHE.clear).

  (* Definition future_cache_expectation :=
    Raw_context.Cache.(Context.CACHE.future_cache_expectation). *)


  Definition cache_size := Raw_context.Cache.(Context.CACHE.cache_size).

  Definition cache_size_limit :=
    Raw_context.Cache.(Context.CACHE.cache_size_limit).

  Definition future_cache_expectation
    (blocks_before_activation : option int32) (ctxt : Raw_context.t)
    (time_in_blocks : int) : M? Raw_context.t :=
    let time_in_blocks' := Int32.of_int time_in_blocks in
    let blocks_per_voting_period :=
      (Constants_storage.cycles_per_voting_period ctxt) ×i32
      (Constants_storage.blocks_per_cycle ctxt) in
    let? function_parameter :=
      match blocks_before_activation with
      | NoneVoting_period_storage.blocks_before_activation ctxt
      | Some blockError_monad.return_some block
      end in
    match
      (function_parameter,
        match function_parameter with
        | Some block
          ((block i32 0) && (block i32 time_in_blocks')) ||
          (blocks_per_voting_period <i32 time_in_blocks')
        | _false
        end) with
    | (Some block, true)
      return? (Raw_context.Cache.(Context.CACHE.clear) ctxt)
    | (_, _)
      return?
        (Raw_context.Cache.(Context.CACHE.future_cache_expectation) ctxt
          time_in_blocks)
    end.

  Definition list_keys (context_value : Raw_context.t) (cache_index : int)
    : option (list (Context.cache_key × int)) :=
    Raw_context.Cache.(Context.CACHE.list_keys) context_value cache_index.

  Definition key_rank
    (context_value : Raw_context.t) (key_value : Context.cache_key)
    : option int :=
    Raw_context.Cache.(Context.CACHE.key_rank) context_value key_value.

  Definition value_of_key (ctxt : Raw_context.t) (key_value : Context.cache_key)
    : M? Context.cache_value :=
    let ctxt := Raw_context.set_gas_unlimited ctxt in
    let '{|
      internal_identifier.namespace := namespace_value;
        internal_identifier.id := id
        |} := internal_identifier_of_key key_value in
    match
      NamespaceMap.(Map.S.find) namespace_value
        (Pervasives.op_exclamation value_of_key_handlers) with
    | Some value_of_keyvalue_of_key ctxt id
    | None
      Pervasives.failwith
        (Format.sprintf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.String_literal "No handler for key `"
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                (CamlinternalFormatBasics.Char
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    (CamlinternalFormatBasics.Char_literal "'" % char
                      CamlinternalFormatBasics.End_of_format)))))
            "No handler for key `%s%c%s'") namespace_value separator id)
    end.
End Admin.

Module CLIENT.
  Record signature {cached_value : Set} : Set := {
    cache_index : int;
    namespace_value : namespace;
    cached_value := cached_value;
    value_of_identifier : Raw_context.t identifier M? cached_value;
  }.
End CLIENT.
Definition CLIENT := @CLIENT.signature.
Arguments CLIENT {_}.

Module INTERFACE.
  Record signature {cached_value : Set} : Set := {
    cached_value := cached_value;
    update :
      Raw_context.t identifier option (cached_value × int)
      M? Raw_context.t;
    find : Raw_context.t identifier M? (option cached_value);
    list_identifiers : Raw_context.t list (identifier × int);
    identifier_rank : Raw_context.t identifier option int;
    size_value : Raw_context.t size;
    size_limit : Raw_context.t size;
  }.
End INTERFACE.
Definition INTERFACE := @INTERFACE.signature.
Arguments INTERFACE {_}.

Definition register_exn {cvalue : Set}
  (C : {_ : unit @ CLIENT (cached_value := cvalue)})
  : {_ : unit @ INTERFACE (cached_value := cvalue)} :=
  let 'existS _ _ C := C in
  let '_ :=
    if
      (C.(CLIENT.cache_index) <i 0) ||
      (Constants_repr.cache_layout_size i C.(CLIENT.cache_index))
    then
      Pervasives.invalid_arg "Cache index is invalid"
    else
      tt in
  let mk := make_key C.(CLIENT.cache_index) C.(CLIENT.namespace_value) in
  existS (A := unit) (fun __) tt
    (let cached_value : Set := cvalue in
    (* ❌ top_level_evaluation *)
    let size_value (ctxt : Raw_context.t) : int :=
      (fun x_1Option.value_value x_1 Pervasives.max_int)
        (Admin.cache_size ctxt C.(CLIENT.cache_index)) in
    let size_limit (ctxt : Raw_context.t) : int :=
      (fun x_1Option.value_value x_1 0)
        (Admin.cache_size_limit ctxt C.(CLIENT.cache_index)) in
    let update
      (ctxt : Raw_context.t) (id : identifier)
      (v_value : option (cached_value × int)) : M? Raw_context.t :=
      let cache_size_in_bytes := size_value ctxt in
      let? ctxt :=
        Raw_context.consume_gas ctxt
          (Cache_costs.cache_update cache_size_in_bytes) in
      let v_value :=
        Option.map
          (fun (function_parameter : cached_value × int) ⇒
            let '(v_value, size_value) := function_parameter in
            ((Build_extensible "K" cached_value v_value), size_value)) v_value
        in
      return? (Admin.update ctxt (mk id) v_value) in
    let find (ctxt : Raw_context.t) (id : identifier)
      : M? (option cached_value) :=
      let cache_size_in_bytes := size_value ctxt in
      let? ctxt :=
        Raw_context.consume_gas ctxt
          (Cache_costs.cache_find cache_size_in_bytes) in
      let function_parameter := Admin.find ctxt (mk id) in
      match function_parameter with
      | Nonereturn? None
      | Some value_value
        match value_value with
        | Build_extensible tag _ payload
          if String.eqb tag "K" then
            let v_value := cast cached_value payload in
            return? (Some v_value)
          else
            (* ❌ Assert instruction is not handled. *)
            assert (M? (option cached_value)) false
        end
      end in
    let list_identifiers (ctxt : Raw_context.t) : list (identifier × int) :=
      (fun (function_parameter : option (list (Context.cache_key × int))) ⇒
        match function_parameter with
        | None
          (* ❌ Assert instruction is not handled. *)
          assert (list (identifier × int)) false
        | Some list_value
          List.filter_map
            (fun (function_parameter : Context.cache_key × int) ⇒
              let '(key_value, age) := function_parameter in
              let '{|
                internal_identifier.namespace := namespace_value;
                  internal_identifier.id := id
                  |} := internal_identifier_of_key key_value in
              if String.equal namespace_value C.(CLIENT.namespace_value) then
                Some (id, age)
              else
                None) list_value
        end) (Admin.list_keys ctxt C.(CLIENT.cache_index)) in
    let identifier_rank (ctxt : Raw_context.t) (id : identifier) : option int :=
      Admin.key_rank ctxt (mk id) in
    {|
      INTERFACE.update := update;
      INTERFACE.find := find;
      INTERFACE.list_identifiers := list_identifiers;
      INTERFACE.identifier_rank := identifier_rank;
      INTERFACE.size_value := size_value;
      INTERFACE.size_limit := size_limit
    |}).