🧠 Cache_repr.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.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
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 43.
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 cache_nonce : Set := Bytes.t.
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)
: M? internal_identifier :=
match String.index_opt raw_value separator with
| None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some index_value ⇒
return?
{| 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)
: M? 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.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Block_header_repr.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
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 43.
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 cache_nonce : Set := Bytes.t.
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)
: M? internal_identifier :=
match String.index_opt raw_value separator with
| None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some index_value ⇒
return?
{| 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)
: M? 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 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 sync := Raw_context.Cache.(Context.CACHE.sync).
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
| None ⇒ Voting_period_storage.blocks_before_activation ctxt
| Some block ⇒ Error_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_key ⇒ value_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 → M? (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_1 ⇒ Option.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_1 ⇒ Option.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
| None ⇒ return? 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 Error_monad.error_value (Build_extensible "Asserted" unit tt)
end
end in
let list_identifiers (ctxt : Raw_context.t)
: M? (list (identifier × int)) :=
(fun (function_parameter : option (list (Context.cache_key × int))) ⇒
match function_parameter with
| None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some list_value ⇒
let? list_value :=
List.map_e
(fun (function_parameter : Context.cache_key × int) ⇒
let '(key_value, age) := function_parameter in
let? res := internal_identifier_of_key key_value in
return? (res, age)) list_value in
return?
(List.filter_map
(fun (function_parameter : internal_identifier × int) ⇒
let
'({|
internal_identifier.namespace := namespace_value;
internal_identifier.id := id
|}, age) := function_parameter 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
|}).
Definition cache_nonce_from_block_header
(shell : Block_header.shell_header) (contents : Block_header_repr.contents)
: cache_nonce :=
let shell :=
{| Block_header.shell_header.level := 0;
Block_header.shell_header.proto_level := 0;
Block_header.shell_header.predecessor :=
shell.(Block_header.shell_header.predecessor);
Block_header.shell_header.timestamp := Time.of_seconds 0;
Block_header.shell_header.validation_passes := 0;
Block_header.shell_header.operations_hash :=
shell.(Block_header.shell_header.operations_hash);
Block_header.shell_header.fitness := nil;
Block_header.shell_header.context := Context_hash.zero; |} in
let contents :=
Block_header_repr.contents.with_proof_of_work_nonce
(Bytes.make Constants_repr.proof_of_work_nonce_size "0" % char)
(Block_header_repr.contents.with_payload_hash Block_payload_hash.zero
contents) in
let protocol_data :=
{| Block_header_repr.protocol_data.contents := contents;
Block_header_repr.protocol_data.signature := Signature.zero; |} in
let x_value :=
{| Block_header_repr.t.shell := shell;
Block_header_repr.t.protocol_data := protocol_data; |} in
Block_hash.to_bytes (Block_header_repr.hash_value x_value).
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 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 sync := Raw_context.Cache.(Context.CACHE.sync).
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
| None ⇒ Voting_period_storage.blocks_before_activation ctxt
| Some block ⇒ Error_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_key ⇒ value_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 → M? (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_1 ⇒ Option.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_1 ⇒ Option.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
| None ⇒ return? 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 Error_monad.error_value (Build_extensible "Asserted" unit tt)
end
end in
let list_identifiers (ctxt : Raw_context.t)
: M? (list (identifier × int)) :=
(fun (function_parameter : option (list (Context.cache_key × int))) ⇒
match function_parameter with
| None ⇒ Error_monad.error_value (Build_extensible "Asserted" unit tt)
| Some list_value ⇒
let? list_value :=
List.map_e
(fun (function_parameter : Context.cache_key × int) ⇒
let '(key_value, age) := function_parameter in
let? res := internal_identifier_of_key key_value in
return? (res, age)) list_value in
return?
(List.filter_map
(fun (function_parameter : internal_identifier × int) ⇒
let
'({|
internal_identifier.namespace := namespace_value;
internal_identifier.id := id
|}, age) := function_parameter 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
|}).
Definition cache_nonce_from_block_header
(shell : Block_header.shell_header) (contents : Block_header_repr.contents)
: cache_nonce :=
let shell :=
{| Block_header.shell_header.level := 0;
Block_header.shell_header.proto_level := 0;
Block_header.shell_header.predecessor :=
shell.(Block_header.shell_header.predecessor);
Block_header.shell_header.timestamp := Time.of_seconds 0;
Block_header.shell_header.validation_passes := 0;
Block_header.shell_header.operations_hash :=
shell.(Block_header.shell_header.operations_hash);
Block_header.shell_header.fitness := nil;
Block_header.shell_header.context := Context_hash.zero; |} in
let contents :=
Block_header_repr.contents.with_proof_of_work_nonce
(Bytes.make Constants_repr.proof_of_work_nonce_size "0" % char)
(Block_header_repr.contents.with_payload_hash Block_payload_hash.zero
contents) in
let protocol_data :=
{| Block_header_repr.protocol_data.contents := contents;
Block_header_repr.protocol_data.signature := Signature.zero; |} in
let x_value :=
{| Block_header_repr.t.shell := shell;
Block_header_repr.t.protocol_data := protocol_data; |} in
Block_hash.to_bytes (Block_header_repr.hash_value x_value).