Skip to main content

🍬 Script_cache.v

Translated OCaml

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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Cache_repr.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Script_ir_translator.

Definition identifier : Set := string.

Definition identifier_of_contract (addr : Alpha_context.Contract.contract)
  : string := Alpha_context.Contract.to_b58check addr.

Definition contract_of_identifier (identifier : string)
  : M? Alpha_context.Contract.contract :=
  Alpha_context.Contract.of_b58check identifier.

Definition cached_contract : Set :=
  Alpha_context.Script.t × Script_ir_translator.ex_script.

Definition load_and_elaborate
  (ctxt : Alpha_context.context) (addr : Alpha_context.Contract.contract)
  : M?
    (Alpha_context.context ×
      option (Alpha_context.Script.t × Script_ir_translator.ex_script × int)) :=
  let? '(ctxt, script) := Alpha_context.Contract.get_script ctxt addr in
  match script with
  | Nonereturn? (ctxt, None)
  | Some script
    let? '(ex_script, ctxt) :=
      Script_ir_translator.parse_script None ctxt true true script in
    let '(size_value, cost) := Script_ir_translator.script_size ex_script in
    let? ctxt := Alpha_context.Gas.consume ctxt cost in
    return? (ctxt, (Some (script, ex_script, size_value)))
  end.

Module Client.
  Definition cached_value : Set := cached_contract.

  Definition namespace_value : Alpha_context.Cache.namespace :=
    Alpha_context.Cache.create_namespace "contract".

  Definition cache_index : int := 0.

  Definition value_of_identifier
    (ctxt : Alpha_context.context) (identifier : string)
    : M? (Alpha_context.Script.t × Script_ir_translator.ex_script) :=
    let? addr := contract_of_identifier identifier in
    let? function_parameter := load_and_elaborate ctxt addr in
    match function_parameter with
    | (_, None)
      Pervasives.failwith "Script_cache: Inconsistent script cache."
    | (_, Some (unparsed_script, ir_script, _))
      return? (unparsed_script, ir_script)
    end.

  (* Client *)
  Definition module :=
    {|
      Cache_repr.CLIENT.namespace_value := namespace_value;
      Cache_repr.CLIENT.cache_index := cache_index;
      Cache_repr.CLIENT.value_of_identifier := value_of_identifier
    |}.
End Client.
Definition Client := Client.module.

Axiom Cache : Cache_repr.INTERFACE (cached_value := Client.cached_value).

Definition find
  (ctxt : Alpha_context.context) (addr : Alpha_context.Contract.contract)
  : M?
    (Alpha_context.context × string ×
      option (Alpha_context.Script.t × Script_ir_translator.ex_script)) :=
  let identifier := identifier_of_contract addr in
  let? function_parameter := Cache.(Cache_repr.INTERFACE.find) ctxt identifier
    in
  match function_parameter with
  | Some (unparsed_script, ex_script)
    return? (ctxt, identifier, (Some (unparsed_script, ex_script)))
  | None
    let? function_parameter := load_and_elaborate ctxt addr in
    match function_parameter with
    | (ctxt, None)return? (ctxt, identifier, None)
    | (ctxt, Some (unparsed_script, script_ir, size_value))
      let cached_value := (unparsed_script, script_ir) in
      let? ctxt :=
        Cache.(Cache_repr.INTERFACE.update) ctxt identifier
          (Some (cached_value, size_value)) in
      return? (ctxt, identifier, (Some (unparsed_script, script_ir)))
    end
  end.

Definition update
  (ctxt : Alpha_context.context) (identifier : Alpha_context.Cache.identifier)
  (updated_script : cached_contract) (approx_size : Alpha_context.Cache.size)
  : M? Alpha_context.context :=
  Cache.(Cache_repr.INTERFACE.update) ctxt identifier
    (Some (updated_script, approx_size)).

Definition entries (ctxt : Alpha_context.context)
  : M? (list (Alpha_context.Contract.contract × int)) :=
  List.map_e
    (fun (function_parameter : string × int) ⇒
      let '(identifier, age) := function_parameter in
      let? contract := contract_of_identifier identifier in
      return? (contract, age))
    (Cache.(Cache_repr.INTERFACE.list_identifiers) ctxt).

Definition contract_rank
  (ctxt : Alpha_context.context) (addr : Alpha_context.Contract.contract)
  : option int :=
  Cache.(Cache_repr.INTERFACE.identifier_rank) ctxt
    (identifier_of_contract addr).

Definition size_value : Alpha_context.context int :=
  Cache.(Cache_repr.INTERFACE.size_value).

Definition size_limit : Alpha_context.context int :=
  Cache.(Cache_repr.INTERFACE.size_limit).

Definition insert
  (ctxt : Alpha_context.context) (addr : Alpha_context.Contract.contract)
  (updated_script : cached_contract) (approx_size : Alpha_context.Cache.size)
  : M? Alpha_context.context :=
  let identifier := identifier_of_contract addr in
  Cache.(Cache_repr.INTERFACE.update) ctxt identifier
    (Some (updated_script, approx_size)).