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

Definition identifier : Set := string.

Definition identifier_of_contract (addr : Contract_hash.t) : string :=
  Contract_hash.to_b58check addr.

Definition contract_of_identifier (identifier : string) : M? Contract_hash.t :=
  match Contract_hash.of_b58check_opt identifier with
  | Some addr ⇒ Pervasives.Ok addr
  | None ⇒
    Error_monad.error_value
      (Build_extensible "Invalid_contract_notation" string identifier)
  end.

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

Definition load_and_elaborate
  (ctxt : Alpha_context.context) (addr : Contract_hash.t)
  : 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
  | None ⇒ return? (ctxt, None)
  | Some script ⇒
    let? '(ex_script, ctxt) :=
      Script_ir_translator.parse_script
        (Script_ir_translator_config.make None None true tt) ctxt 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 : Contract_hash.t)
  : 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 (Contract_hash.t × int)) :=
  let? identifiers := Cache.(Cache_repr.INTERFACE.list_identifiers) ctxt in
  List.map_e
    (fun (function_parameter : string × int) ⇒
      let '(identifier, age) := function_parameter in
      let? contract := contract_of_identifier identifier in
      return? (contract, age)) identifiers.

Definition contract_rank (ctxt : Alpha_context.context) (addr : Contract_hash.t)
  : 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 : Contract_hash.t)
  (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)).