🍬 Script_cache.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.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)).
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)).