🦥 Lazy_storage_diff.v
Translated 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.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Next.
Record signature {id : Set} : Set := {
id := id;
init_value : Raw_context.t → M? Raw_context.t;
incr : Raw_context.t → M? (Raw_context.t × id);
}.
End Next.
Definition Next := @Next.signature.
Arguments Next {_}.
Module Total_bytes.
Record signature {id : Set} : Set := {
id := id;
init_value : Raw_context.t → id → Z.t → M? Raw_context.t;
get : Raw_context.t → id → M? Z.t;
update : Raw_context.t → id → Z.t → M? Raw_context.t;
}.
End Total_bytes.
Definition Total_bytes := @Total_bytes.signature.
Arguments Total_bytes {_}.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Lazy_storage_kind.
Require TezosOfOCaml.Proto_alpha.Michelson_v1_primitives.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Sapling_repr.
Require TezosOfOCaml.Proto_alpha.Sapling_storage.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Next.
Record signature {id : Set} : Set := {
id := id;
init_value : Raw_context.t → M? Raw_context.t;
incr : Raw_context.t → M? (Raw_context.t × id);
}.
End Next.
Definition Next := @Next.signature.
Arguments Next {_}.
Module Total_bytes.
Record signature {id : Set} : Set := {
id := id;
init_value : Raw_context.t → id → Z.t → M? Raw_context.t;
get : Raw_context.t → id → M? Z.t;
update : Raw_context.t → id → Z.t → M? Raw_context.t;
}.
End Total_bytes.
Definition Total_bytes := @Total_bytes.signature.
Arguments Total_bytes {_}.
Operations to be defined on a lazy storage type.
Module OPS.
Record signature {Id_t alloc updates : Set} : Set := {
Id : Lazy_storage_kind.ID (t := Id_t);
alloc := alloc;
updates := updates;
title : string;
alloc_encoding : Data_encoding.t alloc;
updates_encoding : Data_encoding.t updates;
alloc_in_memory_size : alloc → Cache_memory_helpers.nodes_and_size;
updates_in_memory_size : updates → Cache_memory_helpers.nodes_and_size;
bytes_size_for_empty : Z.t;
alloc_value :
Raw_context.t → Id.(Lazy_storage_kind.ID.t) → alloc → M? Raw_context.t;
apply_updates :
Raw_context.t → Id.(Lazy_storage_kind.ID.t) → updates →
M? (Raw_context.t × Z.t);
Next : Next (id := Id.(Lazy_storage_kind.ID.t));
Total_bytes : Total_bytes (id := Id.(Lazy_storage_kind.ID.t));
Record signature {Id_t alloc updates : Set} : Set := {
Id : Lazy_storage_kind.ID (t := Id_t);
alloc := alloc;
updates := updates;
title : string;
alloc_encoding : Data_encoding.t alloc;
updates_encoding : Data_encoding.t updates;
alloc_in_memory_size : alloc → Cache_memory_helpers.nodes_and_size;
updates_in_memory_size : updates → Cache_memory_helpers.nodes_and_size;
bytes_size_for_empty : Z.t;
alloc_value :
Raw_context.t → Id.(Lazy_storage_kind.ID.t) → alloc → M? Raw_context.t;
apply_updates :
Raw_context.t → Id.(Lazy_storage_kind.ID.t) → updates →
M? (Raw_context.t × Z.t);
Next : Next (id := Id.(Lazy_storage_kind.ID.t));
Total_bytes : Total_bytes (id := Id.(Lazy_storage_kind.ID.t));
Deep copy.
copy :
Raw_context.t → Id.(Lazy_storage_kind.ID.t) →
Id.(Lazy_storage_kind.ID.t) → M? Raw_context.t;
Raw_context.t → Id.(Lazy_storage_kind.ID.t) →
Id.(Lazy_storage_kind.ID.t) → M? Raw_context.t;
Deep deletion.
remove : Raw_context.t → Id.(Lazy_storage_kind.ID.t) → Raw_context.t;
}.
End OPS.
Definition OPS := @OPS.signature.
Arguments OPS {_ _ _}.
Module Big_map.
Include Lazy_storage_kind.Big_map.
Definition alloc_in_memory_size (function_parameter : alloc)
: int × Saturation_repr.t :=
let '{|
Lazy_storage_kind.Big_map.alloc.key_type := key_type;
Lazy_storage_kind.Big_map.alloc.value_type := value_type
|} := function_parameter in
Cache_memory_helpers.ret_adding
(Cache_memory_helpers.op_plusplus
(Cache_memory_helpers.expr_size key_type)
(Cache_memory_helpers.expr_size value_type))
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
(Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size 2)).
Definition updates_in_memory_size (updates : list update)
: int × Saturation_repr.t :=
let update_size (function_parameter : update) : int × Saturation_repr.t :=
let '{|
Lazy_storage_kind.Big_map.update.key := key_value;
Lazy_storage_kind.Big_map.update.key_hash := _;
Lazy_storage_kind.Big_map.update.value := value_value
|} := function_parameter in
Cache_memory_helpers.ret_adding
(Cache_memory_helpers.op_plusplus
(Cache_memory_helpers.expr_size key_value)
(Cache_memory_helpers.option_size_vec Cache_memory_helpers.expr_size
value_value))
(Cache_memory_helpers.op_plusquestion
(Cache_memory_helpers.op_plusexclamation
Cache_memory_helpers.header_size
(Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size
3)) Script_expr_hash.size_value) in
Cache_memory_helpers.list_fold_size update_size updates.
Definition bytes_size_for_big_map_key : int := 65.
Definition bytes_size_for_empty : Z.t :=
let bytes_size_for_big_map := 33 in
Z.of_int bytes_size_for_big_map.
Definition alloc_value
(ctxt : Raw_context.t)
(id : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
(function_parameter : alloc) : M? Raw_context.t :=
let '{|
Lazy_storage_kind.Big_map.alloc.key_type := key_type;
Lazy_storage_kind.Big_map.alloc.value_type := value_type
|} := function_parameter in
let key_type :=
Micheline.strip_locations
(Script_repr.strip_annotations (Micheline.root_value key_type)) in
let value_type :=
Micheline.strip_locations
(Script_repr.strip_annotations (Micheline.root_value value_type)) in
let? ctxt :=
Storage.Big_map.Key_type.(Storage_sigs.Indexed_data_storage.init_value)
ctxt id key_type in
Storage.Big_map.Value_type.(Storage_sigs.Indexed_data_storage.init_value)
ctxt id value_type.
Definition apply_update
(ctxt : Raw_context.t) (id : Storage.Big_map.id)
(function_parameter : update) : M? (Raw_context.t × Z.t) :=
let '{|
Lazy_storage_kind.Big_map.update.key :=
_key_is_shown_only_on_the_receipt_in_print_big_map_diff;
Lazy_storage_kind.Big_map.update.key_hash := key_hash;
Lazy_storage_kind.Big_map.update.value := value_value
|} := function_parameter in
match value_value with
| None ⇒
let? '(ctxt, freed, existed) :=
Storage.Big_map.Contents.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage_with_values.remove)
(ctxt, id) key_hash in
let freed :=
if existed then
freed +i bytes_size_for_big_map_key
else
freed in
return? (ctxt, (Z.of_int (Pervasives.op_tildeminus freed)))
| Some v_value ⇒
let? '(ctxt, size_diff, existed) :=
Storage.Big_map.Contents.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage_with_values.add)
(ctxt, id) key_hash v_value in
let size_diff :=
if existed then
size_diff
else
size_diff +i bytes_size_for_big_map_key in
return? (ctxt, (Z.of_int size_diff))
end.
Definition apply_updates
(ctxt : Raw_context.t) (id : Storage.Big_map.id) (updates : list update)
: M? (Raw_context.t × Z.t) :=
List.fold_left_es
(fun (function_parameter : Raw_context.t × Z.t) ⇒
let '(ctxt, size_value) := function_parameter in
fun (update : update) ⇒
let? '(ctxt, added_size) := apply_update ctxt id update in
return? (ctxt, (size_value +Z added_size))) (ctxt, Z.zero) updates.
Include Storage.Big_map.
End Big_map.
Definition ops (id alloc updates : Set) : Set :=
{_ : unit @ OPS (Id_t := id) (alloc := alloc) (updates := updates)}.
Module Sapling_state.
Include Lazy_storage_kind.Sapling_state.
Definition alloc_in_memory_size (function_parameter : alloc)
: int × Saturation_repr.t :=
let '{| Lazy_storage_kind.Sapling_state.alloc.memo_size := _ |} :=
function_parameter in
(Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size)).
Definition updates_in_memory_size (update : Sapling_repr.diff)
: int × Saturation_repr.t :=
(Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
(Sapling_repr.diff_in_memory_size update)).
Definition bytes_size_for_empty : Z.t := Z.of_int 33.
Definition alloc_value
(ctxt : Raw_context.t) (id : Storage.Sapling.id)
(function_parameter : alloc) : M? Raw_context.t :=
let '{| Lazy_storage_kind.Sapling_state.alloc.memo_size := memo_size |} :=
function_parameter in
Sapling_storage.init_value ctxt id memo_size.
Definition apply_updates
(ctxt : Raw_context.t) (id : Storage.Sapling.id)
(updates : Sapling_repr.diff) : M? (Raw_context.t × Z.t) :=
Sapling_storage.apply_diff ctxt id updates.
Include Storage.Sapling.
End Sapling_state.
Axiom get_ops : ∀ {i a u : Set}, Lazy_storage_kind.t → ops i a u.
}.
End OPS.
Definition OPS := @OPS.signature.
Arguments OPS {_ _ _}.
Module Big_map.
Include Lazy_storage_kind.Big_map.
Definition alloc_in_memory_size (function_parameter : alloc)
: int × Saturation_repr.t :=
let '{|
Lazy_storage_kind.Big_map.alloc.key_type := key_type;
Lazy_storage_kind.Big_map.alloc.value_type := value_type
|} := function_parameter in
Cache_memory_helpers.ret_adding
(Cache_memory_helpers.op_plusplus
(Cache_memory_helpers.expr_size key_type)
(Cache_memory_helpers.expr_size value_type))
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
(Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size 2)).
Definition updates_in_memory_size (updates : list update)
: int × Saturation_repr.t :=
let update_size (function_parameter : update) : int × Saturation_repr.t :=
let '{|
Lazy_storage_kind.Big_map.update.key := key_value;
Lazy_storage_kind.Big_map.update.key_hash := _;
Lazy_storage_kind.Big_map.update.value := value_value
|} := function_parameter in
Cache_memory_helpers.ret_adding
(Cache_memory_helpers.op_plusplus
(Cache_memory_helpers.expr_size key_value)
(Cache_memory_helpers.option_size_vec Cache_memory_helpers.expr_size
value_value))
(Cache_memory_helpers.op_plusquestion
(Cache_memory_helpers.op_plusexclamation
Cache_memory_helpers.header_size
(Cache_memory_helpers.op_starquestion Cache_memory_helpers.word_size
3)) Script_expr_hash.size_value) in
Cache_memory_helpers.list_fold_size update_size updates.
Definition bytes_size_for_big_map_key : int := 65.
Definition bytes_size_for_empty : Z.t :=
let bytes_size_for_big_map := 33 in
Z.of_int bytes_size_for_big_map.
Definition alloc_value
(ctxt : Raw_context.t)
(id : Lazy_storage_kind.Big_map.Id.(Lazy_storage_kind.ID.t))
(function_parameter : alloc) : M? Raw_context.t :=
let '{|
Lazy_storage_kind.Big_map.alloc.key_type := key_type;
Lazy_storage_kind.Big_map.alloc.value_type := value_type
|} := function_parameter in
let key_type :=
Micheline.strip_locations
(Script_repr.strip_annotations (Micheline.root_value key_type)) in
let value_type :=
Micheline.strip_locations
(Script_repr.strip_annotations (Micheline.root_value value_type)) in
let? ctxt :=
Storage.Big_map.Key_type.(Storage_sigs.Indexed_data_storage.init_value)
ctxt id key_type in
Storage.Big_map.Value_type.(Storage_sigs.Indexed_data_storage.init_value)
ctxt id value_type.
Definition apply_update
(ctxt : Raw_context.t) (id : Storage.Big_map.id)
(function_parameter : update) : M? (Raw_context.t × Z.t) :=
let '{|
Lazy_storage_kind.Big_map.update.key :=
_key_is_shown_only_on_the_receipt_in_print_big_map_diff;
Lazy_storage_kind.Big_map.update.key_hash := key_hash;
Lazy_storage_kind.Big_map.update.value := value_value
|} := function_parameter in
match value_value with
| None ⇒
let? '(ctxt, freed, existed) :=
Storage.Big_map.Contents.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage_with_values.remove)
(ctxt, id) key_hash in
let freed :=
if existed then
freed +i bytes_size_for_big_map_key
else
freed in
return? (ctxt, (Z.of_int (Pervasives.op_tildeminus freed)))
| Some v_value ⇒
let? '(ctxt, size_diff, existed) :=
Storage.Big_map.Contents.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage_with_values.add)
(ctxt, id) key_hash v_value in
let size_diff :=
if existed then
size_diff
else
size_diff +i bytes_size_for_big_map_key in
return? (ctxt, (Z.of_int size_diff))
end.
Definition apply_updates
(ctxt : Raw_context.t) (id : Storage.Big_map.id) (updates : list update)
: M? (Raw_context.t × Z.t) :=
List.fold_left_es
(fun (function_parameter : Raw_context.t × Z.t) ⇒
let '(ctxt, size_value) := function_parameter in
fun (update : update) ⇒
let? '(ctxt, added_size) := apply_update ctxt id update in
return? (ctxt, (size_value +Z added_size))) (ctxt, Z.zero) updates.
Include Storage.Big_map.
End Big_map.
Definition ops (id alloc updates : Set) : Set :=
{_ : unit @ OPS (Id_t := id) (alloc := alloc) (updates := updates)}.
Module Sapling_state.
Include Lazy_storage_kind.Sapling_state.
Definition alloc_in_memory_size (function_parameter : alloc)
: int × Saturation_repr.t :=
let '{| Lazy_storage_kind.Sapling_state.alloc.memo_size := _ |} :=
function_parameter in
(Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
(Cache_memory_helpers.op_plusexclamation Cache_memory_helpers.header_size
Cache_memory_helpers.word_size)).
Definition updates_in_memory_size (update : Sapling_repr.diff)
: int × Saturation_repr.t :=
(Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
(Sapling_repr.diff_in_memory_size update)).
Definition bytes_size_for_empty : Z.t := Z.of_int 33.
Definition alloc_value
(ctxt : Raw_context.t) (id : Storage.Sapling.id)
(function_parameter : alloc) : M? Raw_context.t :=
let '{| Lazy_storage_kind.Sapling_state.alloc.memo_size := memo_size |} :=
function_parameter in
Sapling_storage.init_value ctxt id memo_size.
Definition apply_updates
(ctxt : Raw_context.t) (id : Storage.Sapling.id)
(updates : Sapling_repr.diff) : M? (Raw_context.t × Z.t) :=
Sapling_storage.apply_diff ctxt id updates.
Include Storage.Sapling.
End Sapling_state.
Axiom get_ops : ∀ {i a u : Set}, Lazy_storage_kind.t → ops i a u.
Records for the constructor parameters
Module ConstructorRecords_init.
Module init.
Module Copy.
Record record {src : Set} : Set := Build {
src : src;
}.
Arguments record : clear implicits.
Definition with_src {t_src} src (r : record t_src) :=
Build t_src src.
End Copy.
Definition Copy_skeleton := Copy.record.
End init.
End ConstructorRecords_init.
Import ConstructorRecords_init.
Reserved Notation "'init.Copy".
Inductive init (id alloc : Set) : Set :=
| Existing : init id alloc
| Copy : 'init.Copy id → init id alloc
| Alloc : alloc → init id alloc
where "'init.Copy" := (fun (t_id : Set) ⇒ init.Copy_skeleton t_id).
Module init.
Include ConstructorRecords_init.init.
Definition Copy := 'init.Copy.
End init.
Arguments Existing {_ _}.
Arguments Copy {_ _}.
Arguments Alloc {_ _}.
Module init.
Module Copy.
Record record {src : Set} : Set := Build {
src : src;
}.
Arguments record : clear implicits.
Definition with_src {t_src} src (r : record t_src) :=
Build t_src src.
End Copy.
Definition Copy_skeleton := Copy.record.
End init.
End ConstructorRecords_init.
Import ConstructorRecords_init.
Reserved Notation "'init.Copy".
Inductive init (id alloc : Set) : Set :=
| Existing : init id alloc
| Copy : 'init.Copy id → init id alloc
| Alloc : alloc → init id alloc
where "'init.Copy" := (fun (t_id : Set) ⇒ init.Copy_skeleton t_id).
Module init.
Include ConstructorRecords_init.init.
Definition Copy := 'init.Copy.
End init.
Arguments Existing {_ _}.
Arguments Copy {_ _}.
Arguments Alloc {_ _}.
Records for the constructor parameters
Module ConstructorRecords_diff.
Module diff.
Module Update.
Record record {init updates : Set} : Set := Build {
init : init;
updates : updates;
}.
Arguments record : clear implicits.
Definition with_init {t_init t_updates} init
(r : record t_init t_updates) :=
Build t_init t_updates init r.(updates).
Definition with_updates {t_init t_updates} updates
(r : record t_init t_updates) :=
Build t_init t_updates r.(init) updates.
End Update.
Definition Update_skeleton := Update.record.
End diff.
End ConstructorRecords_diff.
Import ConstructorRecords_diff.
Reserved Notation "'diff.Update".
Inductive diff (id alloc updates : Set) : Set :=
| Remove : diff id alloc updates
| Update : 'diff.Update alloc id updates → diff id alloc updates
where "'diff.Update" :=
(fun (t_alloc t_id t_updates : Set) ⇒ diff.Update_skeleton
(init t_id t_alloc) t_updates).
Module diff.
Include ConstructorRecords_diff.diff.
Definition Update := 'diff.Update.
End diff.
Arguments Remove {_ _ _}.
Arguments Update {_ _ _}.
Definition diff_encoding {i a u : Set} (OPS : ops i a u)
: Data_encoding.t (diff i a u) :=
let 'existS _ _ OPS := OPS in
Data_encoding.union None
[
Data_encoding.case_value "update" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "action"
(Data_encoding.constant "update"))
(Data_encoding.req None None "updates" OPS.(OPS.updates_encoding)))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
|
Update {|
diff.Update.init := Existing;
diff.Update.updates := updates
|} ⇒ Some (tt, updates)
| _ ⇒ None
end)
(fun (function_parameter : unit × u) ⇒
let '(_, updates) := function_parameter in
Update
{| diff.Update.init := Existing;
diff.Update.updates := updates; |});
Data_encoding.case_value "remove" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "action"
(Data_encoding.constant "remove")))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
| Remove ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Remove);
Data_encoding.case_value "copy" None (Data_encoding.Tag 2)
(Data_encoding.obj3
(Data_encoding.req None None "action"
(Data_encoding.constant "copy"))
(Data_encoding.req None None "source"
OPS.(OPS.Id).(Lazy_storage_kind.ID.encoding))
(Data_encoding.req None None "updates" OPS.(OPS.updates_encoding)))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
|
Update {|
diff.Update.init := Copy {| init.Copy.src := src |};
diff.Update.updates := updates
|} ⇒ Some (tt, src, updates)
| _ ⇒ None
end)
(fun (function_parameter : unit × i × u) ⇒
let '(_, src, updates) := function_parameter in
Update
{| diff.Update.init := Copy {| init.Copy.src := src; |};
diff.Update.updates := updates; |});
Data_encoding.case_value "alloc" None (Data_encoding.Tag 3)
(Data_encoding.merge_objs
(Data_encoding.obj2
(Data_encoding.req None None "action"
(Data_encoding.constant "alloc"))
(Data_encoding.req None None "updates"
OPS.(OPS.updates_encoding))) OPS.(OPS.alloc_encoding))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
|
Update {|
diff.Update.init := Alloc alloc_value;
diff.Update.updates := updates
|} ⇒ Some ((tt, updates), alloc_value)
| _ ⇒ None
end)
(fun (function_parameter : (unit × u) × a) ⇒
let '((_, updates), alloc_value) := function_parameter in
Update
{| diff.Update.init := Alloc alloc_value;
diff.Update.updates := updates; |})
].
Definition init_size {i a u : Set} (OPS : ops i a u)
: init i a → Cache_memory_helpers.nodes_and_size :=
let 'existS _ _ OPS := OPS in
fun (init_value : init i a) ⇒
match init_value with
| Existing ⇒ Cache_memory_helpers.zero
| Copy {| init.Copy.src := _id_is_a_Z_fitting_in_an_int_for_a_long_time |}
⇒
(Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
(Cache_memory_helpers.op_plusexclamation
Cache_memory_helpers.header_size Cache_memory_helpers.word_size))
| Alloc alloc_value ⇒
Cache_memory_helpers.ret_adding
(OPS.(OPS.alloc_in_memory_size) alloc_value)
(Cache_memory_helpers.op_plusexclamation
Cache_memory_helpers.header_size Cache_memory_helpers.word_size)
end.
Definition updates_size {i a u : Set} (OPS : ops i a u)
: u → Cache_memory_helpers.nodes_and_size :=
let 'existS _ _ OPS := OPS in
fun (updates : u) ⇒ OPS.(OPS.updates_in_memory_size) updates.
Definition diff_in_memory_size {A B C : Set}
(kind_value : Lazy_storage_kind.t) (diff_value : diff A B C)
: int × Saturation_repr.t :=
match diff_value with
| Remove ⇒ Cache_memory_helpers.zero
| Update {| diff.Update.init := init_value; diff.Update.updates := updates |}
⇒
let ops := get_ops kind_value in
Cache_memory_helpers.ret_adding
(Cache_memory_helpers.op_plusplus (init_size ops init_value)
(updates_size ops updates)) Cache_memory_helpers.h2w
end.
Module diff.
Module Update.
Record record {init updates : Set} : Set := Build {
init : init;
updates : updates;
}.
Arguments record : clear implicits.
Definition with_init {t_init t_updates} init
(r : record t_init t_updates) :=
Build t_init t_updates init r.(updates).
Definition with_updates {t_init t_updates} updates
(r : record t_init t_updates) :=
Build t_init t_updates r.(init) updates.
End Update.
Definition Update_skeleton := Update.record.
End diff.
End ConstructorRecords_diff.
Import ConstructorRecords_diff.
Reserved Notation "'diff.Update".
Inductive diff (id alloc updates : Set) : Set :=
| Remove : diff id alloc updates
| Update : 'diff.Update alloc id updates → diff id alloc updates
where "'diff.Update" :=
(fun (t_alloc t_id t_updates : Set) ⇒ diff.Update_skeleton
(init t_id t_alloc) t_updates).
Module diff.
Include ConstructorRecords_diff.diff.
Definition Update := 'diff.Update.
End diff.
Arguments Remove {_ _ _}.
Arguments Update {_ _ _}.
Definition diff_encoding {i a u : Set} (OPS : ops i a u)
: Data_encoding.t (diff i a u) :=
let 'existS _ _ OPS := OPS in
Data_encoding.union None
[
Data_encoding.case_value "update" None (Data_encoding.Tag 0)
(Data_encoding.obj2
(Data_encoding.req None None "action"
(Data_encoding.constant "update"))
(Data_encoding.req None None "updates" OPS.(OPS.updates_encoding)))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
|
Update {|
diff.Update.init := Existing;
diff.Update.updates := updates
|} ⇒ Some (tt, updates)
| _ ⇒ None
end)
(fun (function_parameter : unit × u) ⇒
let '(_, updates) := function_parameter in
Update
{| diff.Update.init := Existing;
diff.Update.updates := updates; |});
Data_encoding.case_value "remove" None (Data_encoding.Tag 1)
(Data_encoding.obj1
(Data_encoding.req None None "action"
(Data_encoding.constant "remove")))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
| Remove ⇒ Some tt
| _ ⇒ None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Remove);
Data_encoding.case_value "copy" None (Data_encoding.Tag 2)
(Data_encoding.obj3
(Data_encoding.req None None "action"
(Data_encoding.constant "copy"))
(Data_encoding.req None None "source"
OPS.(OPS.Id).(Lazy_storage_kind.ID.encoding))
(Data_encoding.req None None "updates" OPS.(OPS.updates_encoding)))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
|
Update {|
diff.Update.init := Copy {| init.Copy.src := src |};
diff.Update.updates := updates
|} ⇒ Some (tt, src, updates)
| _ ⇒ None
end)
(fun (function_parameter : unit × i × u) ⇒
let '(_, src, updates) := function_parameter in
Update
{| diff.Update.init := Copy {| init.Copy.src := src; |};
diff.Update.updates := updates; |});
Data_encoding.case_value "alloc" None (Data_encoding.Tag 3)
(Data_encoding.merge_objs
(Data_encoding.obj2
(Data_encoding.req None None "action"
(Data_encoding.constant "alloc"))
(Data_encoding.req None None "updates"
OPS.(OPS.updates_encoding))) OPS.(OPS.alloc_encoding))
(fun (function_parameter : diff i a u) ⇒
match function_parameter with
|
Update {|
diff.Update.init := Alloc alloc_value;
diff.Update.updates := updates
|} ⇒ Some ((tt, updates), alloc_value)
| _ ⇒ None
end)
(fun (function_parameter : (unit × u) × a) ⇒
let '((_, updates), alloc_value) := function_parameter in
Update
{| diff.Update.init := Alloc alloc_value;
diff.Update.updates := updates; |})
].
Definition init_size {i a u : Set} (OPS : ops i a u)
: init i a → Cache_memory_helpers.nodes_and_size :=
let 'existS _ _ OPS := OPS in
fun (init_value : init i a) ⇒
match init_value with
| Existing ⇒ Cache_memory_helpers.zero
| Copy {| init.Copy.src := _id_is_a_Z_fitting_in_an_int_for_a_long_time |}
⇒
(Cache_memory_helpers.Nodes.(Cache_memory_helpers.SNodes.zero),
(Cache_memory_helpers.op_plusexclamation
Cache_memory_helpers.header_size Cache_memory_helpers.word_size))
| Alloc alloc_value ⇒
Cache_memory_helpers.ret_adding
(OPS.(OPS.alloc_in_memory_size) alloc_value)
(Cache_memory_helpers.op_plusexclamation
Cache_memory_helpers.header_size Cache_memory_helpers.word_size)
end.
Definition updates_size {i a u : Set} (OPS : ops i a u)
: u → Cache_memory_helpers.nodes_and_size :=
let 'existS _ _ OPS := OPS in
fun (updates : u) ⇒ OPS.(OPS.updates_in_memory_size) updates.
Definition diff_in_memory_size {A B C : Set}
(kind_value : Lazy_storage_kind.t) (diff_value : diff A B C)
: int × Saturation_repr.t :=
match diff_value with
| Remove ⇒ Cache_memory_helpers.zero
| Update {| diff.Update.init := init_value; diff.Update.updates := updates |}
⇒
let ops := get_ops kind_value in
Cache_memory_helpers.ret_adding
(Cache_memory_helpers.op_plusplus (init_size ops init_value)
(updates_size ops updates)) Cache_memory_helpers.h2w
end.
[apply_updates ctxt ops ~id init] applies the updates [updates] on lazy
storage [id] on storage context [ctxt] using operations [ops] and returns the
updated storage context and the added size in bytes (may be negative).
Definition apply_updates {i a u : Set} (ctxt : Raw_context.t) (OPS : ops i a u)
: i → u → M? (Raw_context.t × Z.t) :=
let 'existS _ _ OPS := OPS in
fun (id : i) ⇒
fun (updates : u) ⇒
let? '(ctxt, updates_size) := OPS.(OPS.apply_updates) ctxt id updates in
if Z.equal updates_size Z.zero then
return? (ctxt, updates_size)
else
let? size_value := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt id in
let? ctxt :=
OPS.(OPS.Total_bytes).(Total_bytes.update) ctxt id
(size_value +Z updates_size) in
return? (ctxt, updates_size).
: i → u → M? (Raw_context.t × Z.t) :=
let 'existS _ _ OPS := OPS in
fun (id : i) ⇒
fun (updates : u) ⇒
let? '(ctxt, updates_size) := OPS.(OPS.apply_updates) ctxt id updates in
if Z.equal updates_size Z.zero then
return? (ctxt, updates_size)
else
let? size_value := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt id in
let? ctxt :=
OPS.(OPS.Total_bytes).(Total_bytes.update) ctxt id
(size_value +Z updates_size) in
return? (ctxt, updates_size).
[apply_init ctxt ops ~id init] applies the initialization [init] on lazy
storage [id] on storage context [ctxt] using operations [ops] and returns the
updated storage context and the added size in bytes (may be negative).
If [id] represents a temporary lazy storage, the added size may be wrong.
Definition apply_init {i a u : Set} (ctxt : Raw_context.t) (OPS : ops i a u)
: i → init i a → M? (Raw_context.t × Z.t) :=
let 'existS _ _ OPS := OPS in
fun (id : i) ⇒
fun (init_value : init i a) ⇒
match init_value with
| Existing ⇒ return? (ctxt, Z.zero)
| Copy {| init.Copy.src := src |} ⇒
let? ctxt := OPS.(OPS.copy) ctxt src id in
if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
return? (ctxt, Z.zero)
else
let? copy_size := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt src in
return? (ctxt, (copy_size +Z OPS.(OPS.bytes_size_for_empty)))
| Alloc alloc_value ⇒
let? ctxt :=
OPS.(OPS.Total_bytes).(Total_bytes.init_value) ctxt id Z.zero in
let? ctxt := OPS.(OPS.alloc_value) ctxt id alloc_value in
return? (ctxt, OPS.(OPS.bytes_size_for_empty))
end.
: i → init i a → M? (Raw_context.t × Z.t) :=
let 'existS _ _ OPS := OPS in
fun (id : i) ⇒
fun (init_value : init i a) ⇒
match init_value with
| Existing ⇒ return? (ctxt, Z.zero)
| Copy {| init.Copy.src := src |} ⇒
let? ctxt := OPS.(OPS.copy) ctxt src id in
if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
return? (ctxt, Z.zero)
else
let? copy_size := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt src in
return? (ctxt, (copy_size +Z OPS.(OPS.bytes_size_for_empty)))
| Alloc alloc_value ⇒
let? ctxt :=
OPS.(OPS.Total_bytes).(Total_bytes.init_value) ctxt id Z.zero in
let? ctxt := OPS.(OPS.alloc_value) ctxt id alloc_value in
return? (ctxt, OPS.(OPS.bytes_size_for_empty))
end.
[apply_diff ctxt ops ~id diff] applies the diff [diff] on lazy storage [id]
on storage context [ctxt] using operations [ops] and returns the updated
storage context and the added size in bytes (may be negative).
If [id] represents a temporary lazy storage, the added size may be wrong.
Definition apply_diff {i a u : Set}
(ctxt : Raw_context.t) (function_parameter : ops i a u)
: i → diff i a u → M? (Raw_context.t × Z.t) :=
let 'OPS as ops := function_parameter in
let 'existS _ _ OPS := OPS in
fun (id : i) ⇒
fun (diff_value : diff i a u) ⇒
match diff_value with
| Remove ⇒
if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
let ctxt := OPS.(OPS.remove) ctxt id in
return? (ctxt, Z.zero)
else
let? size_value := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt id in
let ctxt := OPS.(OPS.remove) ctxt id in
return? (ctxt, (Z.neg (size_value +Z OPS.(OPS.bytes_size_for_empty))))
|
Update {|
diff.Update.init := init_value; diff.Update.updates := updates |}
⇒
let? '(ctxt, init_size) := apply_init ctxt ops id init_value in
let? '(ctxt, updates_size) := apply_updates ctxt ops id updates in
return? (ctxt, (init_size +Z updates_size))
end.
Inductive diffs_item : Set :=
| Item : ∀ {i a u : Set},
Lazy_storage_kind.t → i → diff i a u → diffs_item.
Definition make {i a u : Set}
(k_value : Lazy_storage_kind.t) (id : i) (diff_value : diff i a u)
: diffs_item := Item k_value id diff_value.
Axiom item_encoding : Data_encoding.encoding diffs_item.
Definition item_in_memory_size (function_parameter : diffs_item)
: int × Saturation_repr.t :=
let
'Item kind_value _id_is_a_Z_fitting_in_an_int_for_a_long_time diff_value :=
function_parameter in
Cache_memory_helpers.ret_adding (diff_in_memory_size kind_value diff_value)
Cache_memory_helpers.h3w.
Definition diffs : Set := list diffs_item.
Definition diffs_in_memory_size (diffs : list diffs_item)
: int × Saturation_repr.t :=
Cache_memory_helpers.list_fold_size item_in_memory_size diffs.
Definition encoding : Data_encoding.encoding (list diffs_item) :=
(let arg := Data_encoding.def "lazy_storage_diff" in
fun (eta : Data_encoding.encoding (list diffs_item)) ⇒ arg None None eta)
(Data_encoding.list_value None item_encoding).
Definition apply (ctxt : Raw_context.t) (diffs : list diffs_item)
: M? (Raw_context.t × Z.t) :=
List.fold_left_es
(fun (function_parameter : Raw_context.t × Z.t) ⇒
let '(ctxt, total_size) := function_parameter in
fun (function_parameter : diffs_item) ⇒
let 'Item k_value id diff_value := function_parameter in
let ops := get_ops k_value in
let? '(ctxt, added_size) := apply_diff ctxt ops id diff_value in
let OPS := ops in
return?
(let 'existS _ _ OPS := OPS in
(ctxt,
(if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
total_size
else
total_size +Z added_size)))) (ctxt, Z.zero) diffs.
Axiom fresh : ∀ {i : Set},
Lazy_storage_kind.t → bool → Raw_context.t → M? (Raw_context.t × i).
Axiom init_value : Raw_context.t → M? Raw_context.t.
Axiom cleanup_temporaries : Raw_context.t → Raw_context.t.
(ctxt : Raw_context.t) (function_parameter : ops i a u)
: i → diff i a u → M? (Raw_context.t × Z.t) :=
let 'OPS as ops := function_parameter in
let 'existS _ _ OPS := OPS in
fun (id : i) ⇒
fun (diff_value : diff i a u) ⇒
match diff_value with
| Remove ⇒
if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
let ctxt := OPS.(OPS.remove) ctxt id in
return? (ctxt, Z.zero)
else
let? size_value := OPS.(OPS.Total_bytes).(Total_bytes.get) ctxt id in
let ctxt := OPS.(OPS.remove) ctxt id in
return? (ctxt, (Z.neg (size_value +Z OPS.(OPS.bytes_size_for_empty))))
|
Update {|
diff.Update.init := init_value; diff.Update.updates := updates |}
⇒
let? '(ctxt, init_size) := apply_init ctxt ops id init_value in
let? '(ctxt, updates_size) := apply_updates ctxt ops id updates in
return? (ctxt, (init_size +Z updates_size))
end.
Inductive diffs_item : Set :=
| Item : ∀ {i a u : Set},
Lazy_storage_kind.t → i → diff i a u → diffs_item.
Definition make {i a u : Set}
(k_value : Lazy_storage_kind.t) (id : i) (diff_value : diff i a u)
: diffs_item := Item k_value id diff_value.
Axiom item_encoding : Data_encoding.encoding diffs_item.
Definition item_in_memory_size (function_parameter : diffs_item)
: int × Saturation_repr.t :=
let
'Item kind_value _id_is_a_Z_fitting_in_an_int_for_a_long_time diff_value :=
function_parameter in
Cache_memory_helpers.ret_adding (diff_in_memory_size kind_value diff_value)
Cache_memory_helpers.h3w.
Definition diffs : Set := list diffs_item.
Definition diffs_in_memory_size (diffs : list diffs_item)
: int × Saturation_repr.t :=
Cache_memory_helpers.list_fold_size item_in_memory_size diffs.
Definition encoding : Data_encoding.encoding (list diffs_item) :=
(let arg := Data_encoding.def "lazy_storage_diff" in
fun (eta : Data_encoding.encoding (list diffs_item)) ⇒ arg None None eta)
(Data_encoding.list_value None item_encoding).
Definition apply (ctxt : Raw_context.t) (diffs : list diffs_item)
: M? (Raw_context.t × Z.t) :=
List.fold_left_es
(fun (function_parameter : Raw_context.t × Z.t) ⇒
let '(ctxt, total_size) := function_parameter in
fun (function_parameter : diffs_item) ⇒
let 'Item k_value id diff_value := function_parameter in
let ops := get_ops k_value in
let? '(ctxt, added_size) := apply_diff ctxt ops id diff_value in
let OPS := ops in
return?
(let 'existS _ _ OPS := OPS in
(ctxt,
(if OPS.(OPS.Id).(Lazy_storage_kind.ID.is_temp) id then
total_size
else
total_size +Z added_size)))) (ctxt, Z.zero) diffs.
Axiom fresh : ∀ {i : Set},
Lazy_storage_kind.t → bool → Raw_context.t → M? (Raw_context.t × i).
Axiom init_value : Raw_context.t → M? Raw_context.t.
Axiom cleanup_temporaries : Raw_context.t → Raw_context.t.