💾 Storage_sigs.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage.
Require Import TezosOfOCaml.Proto_alpha.Storage_sigs.
Require Import TezosOfOCaml.Proto_alpha.Storage_functors.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Context.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Error_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
#[local] Open Scope list.
Module Single_data_storage.
Module Eq.
Import Proto_alpha.Storage_sigs.Single_data_storage.
Record t {t value : Set}
{S1 S2 : Single_data_storage (t := t) (value := value)}
: Prop := {
mem ctxt : S1.(mem) ctxt = S2.(mem) ctxt;
get ctxt : S1.(get) ctxt = S2.(get) ctxt;
find ctxt : S1.(find) ctxt = S2.(find) ctxt;
init_value ctxt value :
S1.(init_value) ctxt value = S2.(init_value) ctxt value;
update ctxt value :
S1.(update) ctxt value = S2.(update) ctxt value;
add ctxt value :
S1.(add) ctxt value = S2.(add) ctxt value;
add_or_remove ctxt value :
S1.(add_or_remove) ctxt value = S2.(add_or_remove) ctxt value;
remove_existing ctxt :
S1.(remove_existing) ctxt = S2.(remove_existing) ctxt;
remove ctxt : S1.(remove) ctxt = S2.(remove) ctxt;
}.
Arguments t {_ _ }.
End Eq.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage.
Require Import TezosOfOCaml.Proto_alpha.Storage_sigs.
Require Import TezosOfOCaml.Proto_alpha.Storage_functors.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Context.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Error_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
#[local] Open Scope list.
Module Single_data_storage.
Module Eq.
Import Proto_alpha.Storage_sigs.Single_data_storage.
Record t {t value : Set}
{S1 S2 : Single_data_storage (t := t) (value := value)}
: Prop := {
mem ctxt : S1.(mem) ctxt = S2.(mem) ctxt;
get ctxt : S1.(get) ctxt = S2.(get) ctxt;
find ctxt : S1.(find) ctxt = S2.(find) ctxt;
init_value ctxt value :
S1.(init_value) ctxt value = S2.(init_value) ctxt value;
update ctxt value :
S1.(update) ctxt value = S2.(update) ctxt value;
add ctxt value :
S1.(add) ctxt value = S2.(add) ctxt value;
add_or_remove ctxt value :
S1.(add_or_remove) ctxt value = S2.(add_or_remove) ctxt value;
remove_existing ctxt :
S1.(remove_existing) ctxt = S2.(remove_existing) ctxt;
remove ctxt : S1.(remove) ctxt = S2.(remove) ctxt;
}.
Arguments t {_ _ }.
End Eq.
The type of a simple store. We add a special case for a state with
an invalid encoding. It should not be possible to create such a state,
but we may not control what is already in the input store.
Module State.
Inductive t (a : Set) : Set :=
| Empty : t a
| Invalid_encoding : t a
| Value : a → t a.
Arguments Empty {_}.
Arguments Invalid_encoding {_}.
Arguments Value {_}.
Definition parse {a : Set} (encoding : Data_encoding.t a)
(value : option Context.value) : State.t a :=
match value with
| Some bytes ⇒
match Data_encoding.Binary.of_bytes_opt encoding bytes with
| Some value ⇒ State.Value value
| None ⇒ State.Invalid_encoding
end
| None ⇒ State.Empty
end.
End State.
Module Change.
Inductive t (a : Set) : Set :=
| Empty : t a
| Value : a → t a.
Arguments Empty {_}.
Arguments Value {_}.
Definition apply {a : Set} (ctxt : Raw_context.t) (path : Context.key)
(encoding : Data_encoding.t a) (change : t a) : Raw_context.t :=
match change with
| Empty ⇒ Raw_context.remove ctxt path
| Value value ⇒
let bytes :=
match Data_encoding.Binary.to_bytes_opt None encoding value with
| Some bytes ⇒ bytes
| None ⇒ Bytes.empty
end in
Raw_context.add ctxt path bytes
end.
End Change.
Definition reduce {a : Set} (_ : State.t a) (change : Change.t a)
: State.t a :=
match change with
| Change.Empty ⇒ State.Empty
| Change.Value value ⇒ State.Value value
end.
Module Op.
Definition mem {a : Set} (state : State.t a) : bool :=
match state with
| State.Empty ⇒ false
| State.Invalid_encoding | State.Value _ ⇒ true
end.
Definition get {a : Set} (absolute_key : key) (state : State.t a) : M? a :=
match state with
| State.Empty ⇒
let error := Raw_context.Missing_key absolute_key Raw_context.Get in
Raw_context.storage_error_value error
| State.Invalid_encoding ⇒
let error :=
Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data absolute_key) in
Error_monad.error_value error
| State.Value value ⇒ return? value
end.
Definition find {a : Set} (absolute_key : key) (state : State.t a)
: M? (option a) :=
match state with
| State.Empty ⇒ return? None
| State.Invalid_encoding ⇒
let error :=
Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data absolute_key) in
Error_monad.error_value error
| State.Value value ⇒ return? Some value
end.
Definition init_value {a : Set} (absolute_key : key) (state : State.t a)
(value : a) : M? (Change.t a) :=
match state with
| State.Empty ⇒ return? Change.Value value
| State.Invalid_encoding | State.Value _ ⇒
Raw_context.storage_error_value (Raw_context.Existing_key absolute_key)
end.
Definition update {a : Set} (absolute_key : key) (state : State.t a)
(value : a) : M? (Change.t a) :=
match state with
| State.Empty ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key absolute_key Raw_context._Set)
| State.Invalid_encoding | State.Value _ ⇒ return? Change.Value value
end.
Definition add {a : Set} (state : State.t a)
(value : a) : Change.t a :=
Change.Value value.
Definition add_or_remove {a : Set} (state : State.t a) (ovalue : option a)
: Change.t a :=
match ovalue with
| Some value ⇒ Change.Value value
| None ⇒ Change.Empty
end.
Definition remove_existing {a : Set} (absolute_key : key) (state : State.t a)
: M? (Change.t a) :=
match state with
| State.Empty ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key absolute_key Raw_context.Del)
| State.Invalid_encoding | State.Value _ ⇒
return? Change.Empty
end.
Definition remove {a : Set} (state : State.t a) : Change.t a :=
Change.Empty.
Ltac unfold_all :=
unfold
mem, get, find,
init_value, update, add, add_or_remove, remove_existing.
End Op.
Definition Make {C_t V_t : Set}
(parse : C_t → State.t V_t)
(apply : C_t → Change.t V_t → Raw_context.t)
(absolute_key : key)
: Single_data_storage (t := C_t) (value := V_t) :=
let apply_e ctxt change :=
let? change := change in
return? apply ctxt change in
{|
Single_data_storage.mem ctxt :=
Op.mem (parse ctxt);
Single_data_storage.get ctxt :=
Op.get absolute_key (parse ctxt);
Single_data_storage.find ctxt :=
Op.find absolute_key (parse ctxt);
Single_data_storage.init_value ctxt value :=
apply_e ctxt
(Op.init_value absolute_key (parse ctxt) value);
Single_data_storage.update ctxt value :=
apply_e ctxt
(Op.update absolute_key (parse ctxt) value);
Single_data_storage.add ctxt value :=
let change := Op.add (parse ctxt) value in
apply ctxt change;
Single_data_storage.add_or_remove ctxt ovalue :=
let change := Op.add_or_remove (parse ctxt) ovalue in
apply ctxt change;
Single_data_storage.remove_existing ctxt :=
apply_e ctxt
(Op.remove_existing absolute_key (parse ctxt));
Single_data_storage.remove ctxt :=
apply ctxt (Op.remove (parse ctxt));
|}.
End Single_data_storage.
Module Non_iterable_indexed_carbonated_data_storage_with_values.
Module Eq.
Parameter t : ∀ {t key value : Set},
Non_iterable_indexed_carbonated_data_storage_with_values
(t := t) (key := key) (value := value) →
Non_iterable_indexed_carbonated_data_storage_with_values
(t := t) (key := key) (value := value) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (key value : Set), Set.
End State.
Module Change.
Parameter t : ∀ (key value : Set), Set.
End Change.
Parameter reduce : ∀ {key value},
State.t key value → Change.t key value → State.t key value.
Parameter Make : ∀ {key value : Set}
(parse : Raw_context.t → State.t key value)
(apply : Raw_context.t → Change.t key value → Raw_context.t),
Non_iterable_indexed_carbonated_data_storage_with_values
(t := Raw_context.t) (key := key) (value := value).
End Non_iterable_indexed_carbonated_data_storage_with_values.
Inductive t (a : Set) : Set :=
| Empty : t a
| Invalid_encoding : t a
| Value : a → t a.
Arguments Empty {_}.
Arguments Invalid_encoding {_}.
Arguments Value {_}.
Definition parse {a : Set} (encoding : Data_encoding.t a)
(value : option Context.value) : State.t a :=
match value with
| Some bytes ⇒
match Data_encoding.Binary.of_bytes_opt encoding bytes with
| Some value ⇒ State.Value value
| None ⇒ State.Invalid_encoding
end
| None ⇒ State.Empty
end.
End State.
Module Change.
Inductive t (a : Set) : Set :=
| Empty : t a
| Value : a → t a.
Arguments Empty {_}.
Arguments Value {_}.
Definition apply {a : Set} (ctxt : Raw_context.t) (path : Context.key)
(encoding : Data_encoding.t a) (change : t a) : Raw_context.t :=
match change with
| Empty ⇒ Raw_context.remove ctxt path
| Value value ⇒
let bytes :=
match Data_encoding.Binary.to_bytes_opt None encoding value with
| Some bytes ⇒ bytes
| None ⇒ Bytes.empty
end in
Raw_context.add ctxt path bytes
end.
End Change.
Definition reduce {a : Set} (_ : State.t a) (change : Change.t a)
: State.t a :=
match change with
| Change.Empty ⇒ State.Empty
| Change.Value value ⇒ State.Value value
end.
Module Op.
Definition mem {a : Set} (state : State.t a) : bool :=
match state with
| State.Empty ⇒ false
| State.Invalid_encoding | State.Value _ ⇒ true
end.
Definition get {a : Set} (absolute_key : key) (state : State.t a) : M? a :=
match state with
| State.Empty ⇒
let error := Raw_context.Missing_key absolute_key Raw_context.Get in
Raw_context.storage_error_value error
| State.Invalid_encoding ⇒
let error :=
Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data absolute_key) in
Error_monad.error_value error
| State.Value value ⇒ return? value
end.
Definition find {a : Set} (absolute_key : key) (state : State.t a)
: M? (option a) :=
match state with
| State.Empty ⇒ return? None
| State.Invalid_encoding ⇒
let error :=
Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data absolute_key) in
Error_monad.error_value error
| State.Value value ⇒ return? Some value
end.
Definition init_value {a : Set} (absolute_key : key) (state : State.t a)
(value : a) : M? (Change.t a) :=
match state with
| State.Empty ⇒ return? Change.Value value
| State.Invalid_encoding | State.Value _ ⇒
Raw_context.storage_error_value (Raw_context.Existing_key absolute_key)
end.
Definition update {a : Set} (absolute_key : key) (state : State.t a)
(value : a) : M? (Change.t a) :=
match state with
| State.Empty ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key absolute_key Raw_context._Set)
| State.Invalid_encoding | State.Value _ ⇒ return? Change.Value value
end.
Definition add {a : Set} (state : State.t a)
(value : a) : Change.t a :=
Change.Value value.
Definition add_or_remove {a : Set} (state : State.t a) (ovalue : option a)
: Change.t a :=
match ovalue with
| Some value ⇒ Change.Value value
| None ⇒ Change.Empty
end.
Definition remove_existing {a : Set} (absolute_key : key) (state : State.t a)
: M? (Change.t a) :=
match state with
| State.Empty ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key absolute_key Raw_context.Del)
| State.Invalid_encoding | State.Value _ ⇒
return? Change.Empty
end.
Definition remove {a : Set} (state : State.t a) : Change.t a :=
Change.Empty.
Ltac unfold_all :=
unfold
mem, get, find,
init_value, update, add, add_or_remove, remove_existing.
End Op.
Definition Make {C_t V_t : Set}
(parse : C_t → State.t V_t)
(apply : C_t → Change.t V_t → Raw_context.t)
(absolute_key : key)
: Single_data_storage (t := C_t) (value := V_t) :=
let apply_e ctxt change :=
let? change := change in
return? apply ctxt change in
{|
Single_data_storage.mem ctxt :=
Op.mem (parse ctxt);
Single_data_storage.get ctxt :=
Op.get absolute_key (parse ctxt);
Single_data_storage.find ctxt :=
Op.find absolute_key (parse ctxt);
Single_data_storage.init_value ctxt value :=
apply_e ctxt
(Op.init_value absolute_key (parse ctxt) value);
Single_data_storage.update ctxt value :=
apply_e ctxt
(Op.update absolute_key (parse ctxt) value);
Single_data_storage.add ctxt value :=
let change := Op.add (parse ctxt) value in
apply ctxt change;
Single_data_storage.add_or_remove ctxt ovalue :=
let change := Op.add_or_remove (parse ctxt) ovalue in
apply ctxt change;
Single_data_storage.remove_existing ctxt :=
apply_e ctxt
(Op.remove_existing absolute_key (parse ctxt));
Single_data_storage.remove ctxt :=
apply ctxt (Op.remove (parse ctxt));
|}.
End Single_data_storage.
Module Non_iterable_indexed_carbonated_data_storage_with_values.
Module Eq.
Parameter t : ∀ {t key value : Set},
Non_iterable_indexed_carbonated_data_storage_with_values
(t := t) (key := key) (value := value) →
Non_iterable_indexed_carbonated_data_storage_with_values
(t := t) (key := key) (value := value) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (key value : Set), Set.
End State.
Module Change.
Parameter t : ∀ (key value : Set), Set.
End Change.
Parameter reduce : ∀ {key value},
State.t key value → Change.t key value → State.t key value.
Parameter Make : ∀ {key value : Set}
(parse : Raw_context.t → State.t key value)
(apply : Raw_context.t → Change.t key value → Raw_context.t),
Non_iterable_indexed_carbonated_data_storage_with_values
(t := Raw_context.t) (key := key) (value := value).
End Non_iterable_indexed_carbonated_data_storage_with_values.
Properties about the [Indexed_data_storage] signature.
The validity predicate states that we can conclude to the equality of the
result of folds operations given the equality of the parameters. We
consider a pointwise equality for the parameter which is a function. We
could also use the "functional extensionality axiom" but we prefer to
avoid it.
Module Valid.
Import Proto_alpha.Storage_sigs.Indexed_data_storage.
Record t {C_t I_t V_t : Set}
{S : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)} :
Prop := {
fold {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k v acc, f1 k v acc = f2 k v acc) →
S.(fold) ctxt order acc f1 = S.(fold) ctxt order acc f2;
fold_keys {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k acc, f1 k acc = f2 k acc) →
S.(fold_keys) ctxt order acc f1 = S.(fold_keys) ctxt order acc f2;
}.
Arguments t {_ _ _}.
End Valid.
Import Proto_alpha.Storage_sigs.Indexed_data_storage.
Record t {C_t I_t V_t : Set}
{S : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)} :
Prop := {
fold {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k v acc, f1 k v acc = f2 k v acc) →
S.(fold) ctxt order acc f1 = S.(fold) ctxt order acc f2;
fold_keys {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k acc, f1 k acc = f2 k acc) →
S.(fold_keys) ctxt order acc f1 = S.(fold_keys) ctxt order acc f2;
}.
Arguments t {_ _ _}.
End Valid.
The equality between two [Indexed_data_storage].
Module Eq.
Import Proto_alpha.Storage_sigs.Indexed_data_storage.
Record t {C_t I_t V_t : Set}
{S1 S2 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)} :
Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
clear ctxt : S1.(clear) ctxt = S2.(clear) ctxt;
keys ctxt : S1.(keys) ctxt = S2.(keys) ctxt;
bindings ctxt : S1.(bindings) ctxt = S2.(bindings) ctxt;
(* We only consider the "Sorted" order for the fold operations. *)
fold {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k v acc, f1 k v acc = f2 k v acc) →
S1.(fold) ctxt order acc f1 = S2.(fold) ctxt order acc f2;
fold_keys {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k acc, f1 k acc = f2 k acc) →
S1.(fold_keys) ctxt order acc f1 = S2.(fold_keys) ctxt order acc f2;
}.
Arguments t {_ _ _}.
Import Proto_alpha.Storage_sigs.Indexed_data_storage.
Record t {C_t I_t V_t : Set}
{S1 S2 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)} :
Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
clear ctxt : S1.(clear) ctxt = S2.(clear) ctxt;
keys ctxt : S1.(keys) ctxt = S2.(keys) ctxt;
bindings ctxt : S1.(bindings) ctxt = S2.(bindings) ctxt;
(* We only consider the "Sorted" order for the fold operations. *)
fold {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k v acc, f1 k v acc = f2 k v acc) →
S1.(fold) ctxt order acc f1 = S2.(fold) ctxt order acc f2;
fold_keys {a : Set} ctxt (acc : a) f1 f2 :
let order := Variant.Build "Sorted" unit tt in
(∀ k acc, f1 k acc = f2 k acc) →
S1.(fold_keys) ctxt order acc f1 = S2.(fold_keys) ctxt order acc f2;
}.
Arguments t {_ _ _}.
Our equality is reflexive.
Lemma refl {C_t I_t V_t : Set}
(S : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
Valid.t S →
t S S.
Proof.
sfirstorder.
Qed.
(S : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
Valid.t S →
t S S.
Proof.
sfirstorder.
Qed.
Our equality is symmetric.
Lemma sym {C_t I_t V_t : Set}
(S1 S2 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
Valid.t S1 → Valid.t S2 →
t S1 S2 → t S2 S1.
Proof.
intros [] [] []; constructor; intros;
repeat match goal with
| H : _ |- _ ⇒ rewrite H
end;
try reflexivity;
sauto dep: on.
Qed.
(S1 S2 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
Valid.t S1 → Valid.t S2 →
t S1 S2 → t S2 S1.
Proof.
intros [] [] []; constructor; intros;
repeat match goal with
| H : _ |- _ ⇒ rewrite H
end;
try reflexivity;
sauto dep: on.
Qed.
Our equality is transitive.
Lemma trans {C_t I_t V_t : Set}
(S1 S2 S3 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
Valid.t S1 → Valid.t S2 → Valid.t S3 →
t S1 S2 → t S2 S3 → t S1 S3.
Proof.
intros [] [] [] [] []; constructor; intros;
repeat match goal with
| H : _ |- _ ⇒ rewrite H
end;
try reflexivity;
sauto dep: on.
Qed.
End Eq.
(S1 S2 S3 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
Valid.t S1 → Valid.t S2 → Valid.t S3 →
t S1 S2 → t S2 S3 → t S1 S3.
Proof.
intros [] [] [] [] []; constructor; intros;
repeat match goal with
| H : _ |- _ ⇒ rewrite H
end;
try reflexivity;
sauto dep: on.
Qed.
End Eq.
A [Kernel] from which we can express all the other operations. This is
useful to simplify the proofs on the storage simulations.
Module Kernel.
Record signature {t key value : Set} : Set := {
t := t;
context := t;
key := key;
value := value;
mem : context → key → bool;
find : context → key → M? (option value);
add_or_remove : context → key → option value → Raw_context.t;
clear : context → Raw_context.t;
keys : context → list key;
bindings : context → list (key × value);
}.
End Kernel.
Definition Kernel := @Kernel.signature.
Arguments Kernel {_ _ _}.
Record signature {t key value : Set} : Set := {
t := t;
context := t;
key := key;
value := value;
mem : context → key → bool;
find : context → key → M? (option value);
add_or_remove : context → key → option value → Raw_context.t;
clear : context → Raw_context.t;
keys : context → list key;
bindings : context → list (key × value);
}.
End Kernel.
Definition Kernel := @Kernel.signature.
Arguments Kernel {_ _ _}.
The equality between two [Kernel].
Module Kernel_eq.
Import Kernel.
Record t {t key value : Set}
{K1 K2 : Kernel (t := t) (key := key) (value := value)}
: Prop := {
mem ctxt path : K1.(mem) ctxt path = K2.(mem) ctxt path;
find ctxt path : K1.(find) ctxt path = K2.(find) ctxt path;
add_or_remove ctxt path v :
K1.(add_or_remove) ctxt path v = K2.(add_or_remove) ctxt path v;
clear ctxt : K1.(clear) ctxt = K2.(clear) ctxt;
keys ctxt : K1.(keys) ctxt = K2.(keys) ctxt;
bindings ctxt : K1.(bindings) ctxt = K2.(bindings) ctxt;
}.
Arguments t {_ _ _}.
End Kernel_eq.
Import Kernel.
Record t {t key value : Set}
{K1 K2 : Kernel (t := t) (key := key) (value := value)}
: Prop := {
mem ctxt path : K1.(mem) ctxt path = K2.(mem) ctxt path;
find ctxt path : K1.(find) ctxt path = K2.(find) ctxt path;
add_or_remove ctxt path v :
K1.(add_or_remove) ctxt path v = K2.(add_or_remove) ctxt path v;
clear ctxt : K1.(clear) ctxt = K2.(clear) ctxt;
keys ctxt : K1.(keys) ctxt = K2.(keys) ctxt;
bindings ctxt : K1.(bindings) ctxt = K2.(bindings) ctxt;
}.
Arguments t {_ _ _}.
End Kernel_eq.
Projection to a [Kernel].
Definition to_kernel {t key value : Set}
(S : Indexed_data_storage (t := t) (key := key) (value := value)) :
Kernel (t := t) (key := key) (value := value) :=
{|
Kernel.mem := S.(Indexed_data_storage.mem);
Kernel.find := S.(Indexed_data_storage.find);
Kernel.add_or_remove := S.(Indexed_data_storage.add_or_remove);
Kernel.clear := S.(Indexed_data_storage.clear);
Kernel.keys := S.(Indexed_data_storage.keys);
Kernel.bindings := S.(Indexed_data_storage.bindings);
|}.
(S : Indexed_data_storage (t := t) (key := key) (value := value)) :
Kernel (t := t) (key := key) (value := value) :=
{|
Kernel.mem := S.(Indexed_data_storage.mem);
Kernel.find := S.(Indexed_data_storage.find);
Kernel.add_or_remove := S.(Indexed_data_storage.add_or_remove);
Kernel.clear := S.(Indexed_data_storage.clear);
Kernel.keys := S.(Indexed_data_storage.keys);
Kernel.bindings := S.(Indexed_data_storage.bindings);
|}.
Re-definition from a [Kernel].
Definition of_kernel {t key value : Set}
(P : Path_encoding.S (t := key))
(absolute_key : t → Context.key) (sub_path : Context.key)
(K : Kernel (t := t) (key := key) (value := value)) :
Indexed_data_storage (t := t) (key := key) (value := value) :=
let to_key (ctxt : t) (i : key) : Context.key :=
(absolute_key ctxt ++ P.(Path_encoding.S.to_path) i []) ++ sub_path in
{|
Indexed_data_storage.mem := K.(Kernel.mem);
Indexed_data_storage.get ctxt i :=
let? value := K.(Kernel.find) ctxt i in
match value with
| Some value ⇒ return? value
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key (to_key ctxt i) Raw_context.Get)
end;
Indexed_data_storage.find := K.(Kernel.find);
Indexed_data_storage.update ctxt i v :=
if K.(Kernel.mem) ctxt i then
return? K.(Kernel.add_or_remove) ctxt i (Some v)
else
Raw_context.storage_error_value
(Raw_context.Missing_key (to_key ctxt i) Raw_context._Set);
Indexed_data_storage.init_value ctxt i v :=
if K.(Kernel.mem) ctxt i then
Raw_context.storage_error_value
(Raw_context.Existing_key (to_key ctxt i))
else
return? K.(Kernel.add_or_remove) ctxt i (Some v);
Indexed_data_storage.add ctxt i v :=
K.(Kernel.add_or_remove) ctxt i (Some v);
Indexed_data_storage.add_or_remove := K.(Kernel.add_or_remove);
Indexed_data_storage.remove_existing ctxt i :=
if K.(Kernel.mem) ctxt i then
return? K.(Kernel.add_or_remove) ctxt i None
else
Raw_context.storage_error_value
(Raw_context.Missing_key (to_key ctxt i) Raw_context.Del);
Indexed_data_storage.remove ctxt i :=
K.(Kernel.add_or_remove) ctxt i None;
Indexed_data_storage.clear := K.(Kernel.clear);
Indexed_data_storage.keys := K.(Kernel.keys);
Indexed_data_storage.bindings := K.(Kernel.bindings);
Indexed_data_storage.fold _ ctxt order acc f :=
List.fold_right (fun '(k, v) acc ⇒ f k v acc)
(K.(Kernel.bindings) ctxt) acc;
Indexed_data_storage.fold_keys _ ctxt order acc f :=
List.fold_right f (K.(Kernel.keys) ctxt) acc;
|}.
(P : Path_encoding.S (t := key))
(absolute_key : t → Context.key) (sub_path : Context.key)
(K : Kernel (t := t) (key := key) (value := value)) :
Indexed_data_storage (t := t) (key := key) (value := value) :=
let to_key (ctxt : t) (i : key) : Context.key :=
(absolute_key ctxt ++ P.(Path_encoding.S.to_path) i []) ++ sub_path in
{|
Indexed_data_storage.mem := K.(Kernel.mem);
Indexed_data_storage.get ctxt i :=
let? value := K.(Kernel.find) ctxt i in
match value with
| Some value ⇒ return? value
| None ⇒
Raw_context.storage_error_value
(Raw_context.Missing_key (to_key ctxt i) Raw_context.Get)
end;
Indexed_data_storage.find := K.(Kernel.find);
Indexed_data_storage.update ctxt i v :=
if K.(Kernel.mem) ctxt i then
return? K.(Kernel.add_or_remove) ctxt i (Some v)
else
Raw_context.storage_error_value
(Raw_context.Missing_key (to_key ctxt i) Raw_context._Set);
Indexed_data_storage.init_value ctxt i v :=
if K.(Kernel.mem) ctxt i then
Raw_context.storage_error_value
(Raw_context.Existing_key (to_key ctxt i))
else
return? K.(Kernel.add_or_remove) ctxt i (Some v);
Indexed_data_storage.add ctxt i v :=
K.(Kernel.add_or_remove) ctxt i (Some v);
Indexed_data_storage.add_or_remove := K.(Kernel.add_or_remove);
Indexed_data_storage.remove_existing ctxt i :=
if K.(Kernel.mem) ctxt i then
return? K.(Kernel.add_or_remove) ctxt i None
else
Raw_context.storage_error_value
(Raw_context.Missing_key (to_key ctxt i) Raw_context.Del);
Indexed_data_storage.remove ctxt i :=
K.(Kernel.add_or_remove) ctxt i None;
Indexed_data_storage.clear := K.(Kernel.clear);
Indexed_data_storage.keys := K.(Kernel.keys);
Indexed_data_storage.bindings := K.(Kernel.bindings);
Indexed_data_storage.fold _ ctxt order acc f :=
List.fold_right (fun '(k, v) acc ⇒ f k v acc)
(K.(Kernel.bindings) ctxt) acc;
Indexed_data_storage.fold_keys _ ctxt order acc f :=
List.fold_right f (K.(Kernel.keys) ctxt) acc;
|}.
Going from and then to a kernel does not change anything (this way is not
really interesting).
Lemma to_kernel_of_kernel {t key value : Set}
(P : Path_encoding.S (t := key))
(absolute_key : t → Context.key) (sub_path : Context.key)
(K : Kernel (t := t) (key := key) (value := value)) :
to_kernel (of_kernel P absolute_key sub_path K) = K.
Proof.
reflexivity.
Qed.
(P : Path_encoding.S (t := key))
(absolute_key : t → Context.key) (sub_path : Context.key)
(K : Kernel (t := t) (key := key) (value := value)) :
to_kernel (of_kernel P absolute_key sub_path K) = K.
Proof.
reflexivity.
Qed.
From the equality on the kernel we can conclude the equality on the whole
definition.
Lemma of_kernel_implies_eq {t key value : Set}
(P : Path_encoding.S (t := key))
(absolute_key : t → Context.key) (sub_path : Context.key)
(K1 K2 : Kernel (t := t) (key := key) (value := value)) :
Kernel_eq.t K1 K2 →
Eq.t
(of_kernel P absolute_key sub_path K1)
(of_kernel P absolute_key sub_path K2).
Proof.
assert (∀ {a b : Set} (f1 f2 : a → b → b) l acc,
(∀ x acc, f1 x acc = f2 x acc) →
List.fold_right f1 l acc = List.fold_right f2 l acc
) by (induction l; hauto q: on).
intros []; constructor; hauto l: on.
Qed.
(P : Path_encoding.S (t := key))
(absolute_key : t → Context.key) (sub_path : Context.key)
(K1 K2 : Kernel (t := t) (key := key) (value := value)) :
Kernel_eq.t K1 K2 →
Eq.t
(of_kernel P absolute_key sub_path K1)
(of_kernel P absolute_key sub_path K2).
Proof.
assert (∀ {a b : Set} (f1 f2 : a → b → b) l acc,
(∀ x acc, f1 x acc = f2 x acc) →
List.fold_right f1 l acc = List.fold_right f2 l acc
) by (induction l; hauto q: on).
intros []; constructor; hauto l: on.
Qed.
The simulation state.
Module State.
Definition compare {I_t : Set} (P : Path_encoding.S (t := I_t))
(x1 x2 : I_t) : int :=
let path1 := P.(Path_encoding.S.to_path) x1 [] in
let path2 := P.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
Definition Ord {I_t : Set} (P : Path_encoding.S (t := I_t)) :
Compare.COMPARABLE (t := I_t) :=
{| Compare.COMPARABLE.compare := compare P |}.
Definition Map {I_t : Set} (P : Path_encoding.S (t := I_t)) :
Map.S (key := I_t) (t := _) :=
Map.Make (Ord P).
Definition compare {I_t : Set} (P : Path_encoding.S (t := I_t))
(x1 x2 : I_t) : int :=
let path1 := P.(Path_encoding.S.to_path) x1 [] in
let path2 := P.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
Definition Ord {I_t : Set} (P : Path_encoding.S (t := I_t)) :
Compare.COMPARABLE (t := I_t) :=
{| Compare.COMPARABLE.compare := compare P |}.
Definition Map {I_t : Set} (P : Path_encoding.S (t := I_t)) :
Map.S (key := I_t) (t := _) :=
Map.Make (Ord P).
The simulation state is a map to optional values. We keep the values
optional to represent values with an incorrect encoding.
Definition t {I_t : Set} (P : Path_encoding.S (t := I_t)) (V_t : Set)
: Set :=
(Map P).(Map.S.t) (option V_t).
End State.
: Set :=
(Map P).(Map.S.t) (option V_t).
End State.
An exmplicit change on the simutation state.
Module Change.
Inductive t (I_t V_t : Set) : Set :=
| Add : I_t → V_t → t I_t V_t
| Remove : I_t → t I_t V_t
| Clear : t I_t V_t.
Arguments Add {_ _}.
Arguments Remove {_ _}.
Arguments Clear {_ _}.
End Change.
Inductive t (I_t V_t : Set) : Set :=
| Add : I_t → V_t → t I_t V_t
| Remove : I_t → t I_t V_t
| Clear : t I_t V_t.
Arguments Add {_ _}.
Arguments Remove {_ _}.
Arguments Clear {_ _}.
End Change.
How to apply a change on the simulation state.
Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) (change : Change.t I_t V_t)
: State.t P V_t :=
match change with
| Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
| Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
| Change.Clear ⇒ (State.Map P).(Map.S.empty)
end.
(state : State.t P V_t) (change : Change.t I_t V_t)
: State.t P V_t :=
match change with
| Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
| Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
| Change.Clear ⇒ (State.Map P).(Map.S.empty)
end.
Primitive operations defined on the simulation state.
Module Op.
Definition mem {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) (k : I_t) : bool :=
(State.Map P).(Map.S.mem) k state.
Definition find {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t) (k : I_t) : M? (option V_t) :=
match (State.Map P).(Map.S.find) k state with
| Some (Some v) ⇒ return? Some v
| Some None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data (absolute_key ++ path)))
| None ⇒ return? None
end.
Definition get {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t) (k : I_t)
: M? V_t :=
match find absolute_key state k with
| Pervasives.Error e ⇒ Pervasives.Error e
| Pervasives.Ok None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Missing_key (absolute_key ++ path) Raw_context.Get))
| Pervasives.Ok (Some v) ⇒ return? v
end.
Definition add {I_t V_t : Set} (k : I_t) (v : V_t) : Change.t I_t V_t :=
Change.Add k v.
Definition add_or_remove {I_t V_t : Set} (k : I_t) (v : option V_t)
: Change.t I_t V_t :=
match v with
| Some v ⇒ Change.Add k v
| None ⇒ Change.Remove k
end.
Definition update {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t)
(k : I_t) (v : V_t) : M? Change.t I_t V_t :=
if mem state k
then return? (add k v)
else let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Missing_key (absolute_key ++ path) Raw_context._Set)).
Definition init_value {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t) (k : I_t) (v : V_t) : M? (Change.t I_t V_t) :=
if mem state k
then let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Existing_key (absolute_key ++ path)))
else return? (add k v).
Definition remove {I_t V_t : Set} (k : I_t) : Change.t I_t V_t :=
Change.Remove k.
Definition remove_existing {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key) (state : State.t P V_t) (k : I_t) :
M? Change.t I_t V_t :=
if Op.mem state k then
return? Op.remove k
else
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Missing_key (absolute_key ++ path) Raw_context.Del)).
Definition clear {I_t V_t : Set} : Change.t I_t V_t :=
Change.Clear.
Definition keys {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) : list I_t :=
List.filter_map
(fun '(k, v) ⇒
let× '_ := v in
Some k
)
((State.Map P).(Map.S.bindings) state).
Definition bindings {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) : list (I_t × V_t) :=
List.filter_map
(fun '(k, v) ⇒
let× v := v in
Some (k, v)
)
((State.Map P).(Map.S.bindings) state).
Definition mem {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) (k : I_t) : bool :=
(State.Map P).(Map.S.mem) k state.
Definition find {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t) (k : I_t) : M? (option V_t) :=
match (State.Map P).(Map.S.find) k state with
| Some (Some v) ⇒ return? Some v
| Some None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data (absolute_key ++ path)))
| None ⇒ return? None
end.
Definition get {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t) (k : I_t)
: M? V_t :=
match find absolute_key state k with
| Pervasives.Error e ⇒ Pervasives.Error e
| Pervasives.Ok None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Missing_key (absolute_key ++ path) Raw_context.Get))
| Pervasives.Ok (Some v) ⇒ return? v
end.
Definition add {I_t V_t : Set} (k : I_t) (v : V_t) : Change.t I_t V_t :=
Change.Add k v.
Definition add_or_remove {I_t V_t : Set} (k : I_t) (v : option V_t)
: Change.t I_t V_t :=
match v with
| Some v ⇒ Change.Add k v
| None ⇒ Change.Remove k
end.
Definition update {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t)
(k : I_t) (v : V_t) : M? Change.t I_t V_t :=
if mem state k
then return? (add k v)
else let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Missing_key (absolute_key ++ path) Raw_context._Set)).
Definition init_value {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(state : State.t P V_t) (k : I_t) (v : V_t) : M? (Change.t I_t V_t) :=
if mem state k
then let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Existing_key (absolute_key ++ path)))
else return? (add k v).
Definition remove {I_t V_t : Set} (k : I_t) : Change.t I_t V_t :=
Change.Remove k.
Definition remove_existing {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key) (state : State.t P V_t) (k : I_t) :
M? Change.t I_t V_t :=
if Op.mem state k then
return? Op.remove k
else
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Missing_key (absolute_key ++ path) Raw_context.Del)).
Definition clear {I_t V_t : Set} : Change.t I_t V_t :=
Change.Clear.
Definition keys {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) : list I_t :=
List.filter_map
(fun '(k, v) ⇒
let× '_ := v in
Some k
)
((State.Map P).(Map.S.bindings) state).
Definition bindings {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) : list (I_t × V_t) :=
List.filter_map
(fun '(k, v) ⇒
let× v := v in
Some (k, v)
)
((State.Map P).(Map.S.bindings) state).
Helper to unfold all the simulation operators.
Module Unfold.
Ltac all :=
repeat unfold mem, find, get,
add, add_or_remove, update, init_value,
remove, remove_existing,
clear, keys, bindings,
State.Map.
End Unfold.
End Op.
Ltac all :=
repeat unfold mem, find, get,
add, add_or_remove, update, init_value,
remove, remove_existing,
clear, keys, bindings,
State.Map.
End Unfold.
End Op.
Build a simulation store given two functions [parse] and [apply] to
communicate with the actual key-value store.
Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t) :
Indexed_data_storage (t := C_t) (key := I_t) (value := V_t) :=
{|
Indexed_data_storage.mem ctxt k :=
Op.mem (parse ctxt) k;
Indexed_data_storage.get ctxt k :=
Op.get (absolute_key ctxt) (parse ctxt) k;
Indexed_data_storage.find ctxt k :=
Op.find (absolute_key ctxt) (parse ctxt) k;
Indexed_data_storage.update ctxt k v:=
let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
return? apply ctxt change;
Indexed_data_storage.init_value ctxt k v :=
let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
return? apply ctxt change;
Indexed_data_storage.add ctxt k v :=
apply ctxt (Op.add k v);
Indexed_data_storage.add_or_remove ctxt k v :=
let change := Op.add_or_remove k v in
apply ctxt change;
Indexed_data_storage.remove_existing ctxt k :=
let state := parse ctxt in
let? change := Op.remove_existing (absolute_key ctxt) state k in
return? apply ctxt change;
Indexed_data_storage.remove ctxt k :=
let change := Op.remove k in
apply ctxt change;
Indexed_data_storage.clear ctxt :=
let change := Op.clear in
apply ctxt change;
Indexed_data_storage.keys ctxt := Op.keys (parse ctxt);
Indexed_data_storage.bindings ctxt := Op.bindings (parse ctxt);
Indexed_data_storage.fold _ ctxt _ acc f :=
List.fold_right
(fun '(k, v) acc ⇒ f k v acc) (Op.bindings (parse ctxt)) acc;
Indexed_data_storage.fold_keys _ ctxt _ acc f :=
List.fold_right f (Op.keys (parse ctxt)) acc;
|}.
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t) :
Indexed_data_storage (t := C_t) (key := I_t) (value := V_t) :=
{|
Indexed_data_storage.mem ctxt k :=
Op.mem (parse ctxt) k;
Indexed_data_storage.get ctxt k :=
Op.get (absolute_key ctxt) (parse ctxt) k;
Indexed_data_storage.find ctxt k :=
Op.find (absolute_key ctxt) (parse ctxt) k;
Indexed_data_storage.update ctxt k v:=
let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
return? apply ctxt change;
Indexed_data_storage.init_value ctxt k v :=
let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
return? apply ctxt change;
Indexed_data_storage.add ctxt k v :=
apply ctxt (Op.add k v);
Indexed_data_storage.add_or_remove ctxt k v :=
let change := Op.add_or_remove k v in
apply ctxt change;
Indexed_data_storage.remove_existing ctxt k :=
let state := parse ctxt in
let? change := Op.remove_existing (absolute_key ctxt) state k in
return? apply ctxt change;
Indexed_data_storage.remove ctxt k :=
let change := Op.remove k in
apply ctxt change;
Indexed_data_storage.clear ctxt :=
let change := Op.clear in
apply ctxt change;
Indexed_data_storage.keys ctxt := Op.keys (parse ctxt);
Indexed_data_storage.bindings ctxt := Op.bindings (parse ctxt);
Indexed_data_storage.fold _ ctxt _ acc f :=
List.fold_right
(fun '(k, v) acc ⇒ f k v acc) (Op.bindings (parse ctxt)) acc;
Indexed_data_storage.fold_keys _ ctxt _ acc f :=
List.fold_right f (Op.keys (parse ctxt)) acc;
|}.
The simulation store can be expressed from its kernel. This will be useful
to show the equality to other stores.
Lemma expressed_from_kernel {C_t I_t V_t : Set}
{P : Path_encoding.S (t := I_t)}
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t) :
let Store := Make absolute_key parse apply in
Eq.t Store (of_kernel P absolute_key [] (to_kernel Store)).
Proof.
constructor; intros; simpl; try reflexivity;
repeat Op.Unfold.all;
try (step; simpl; try rewrite List.app_nil_r; reflexivity);
try (apply List.fold_right_f_eq; hauto lq: on).
Qed.
End Indexed_data_storage.
Module Non_iterable_indexed_data_storage.
Module Eq.
Import Proto_alpha.Storage_sigs.Non_iterable_indexed_data_storage.
Record t {t key value : Set}
{S1 S2 : Non_iterable_indexed_data_storage (t := t) (key := key) (value := value)}
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
}.
Arguments t {_ _ _}.
End Eq.
Module State := Indexed_data_storage.State.
Module Change := Indexed_data_storage.Change.
Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)} :=
@Indexed_data_storage.reduce I_t V_t P.
Module Op := Indexed_data_storage.Op.
Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t)
: Non_iterable_indexed_data_storage (t := C_t) (key := I_t) :=
{|
Non_iterable_indexed_data_storage.mem ctxt k :=
Op.mem (parse ctxt) k;
Non_iterable_indexed_data_storage.get ctxt k :=
Op.get absolute_key (parse ctxt) k;
Non_iterable_indexed_data_storage.find ctxt k :=
Op.find absolute_key (parse ctxt) k;
Non_iterable_indexed_data_storage.update ctxt k v :=
let? change := Op.update absolute_key (parse ctxt) k v in
return? apply ctxt change;
Non_iterable_indexed_data_storage.init_value ctxt k v :=
let? change := Op.init_value absolute_key (parse ctxt) k v in
return? apply ctxt change;
Non_iterable_indexed_data_storage.add ctxt k v :=
apply ctxt (Op.add k v);
Non_iterable_indexed_data_storage.add_or_remove := axiom;
Non_iterable_indexed_data_storage.remove_existing := axiom;
Non_iterable_indexed_data_storage.remove := axiom;
|}.
End Non_iterable_indexed_data_storage.
Module Non_iterable_indexed_carbonated_data_storage_INTERNAL.
Import Proto_alpha.Storage_sigs.Non_iterable_indexed_carbonated_data_storage_INTERNAL.
Module Eq.
Record t {t key value : Set}
(S1 S2 : Non_iterable_indexed_carbonated_data_storage_INTERNAL (t := t) (key := key) (value := value))
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
}.
Arguments t {_ _ _}.
End Eq.
Module State := Indexed_data_storage.State.
Module Op := Indexed_data_storage.Op.
(* Module Change := Indexed_data_storage.Change. *)
Module Change.
Inductive t (I_t V_t : Set) : Set :=
| Add : I_t → V_t → t I_t V_t
| Remove : I_t → t I_t V_t
| Clear : t I_t V_t
| Consume_read_gas : int → I_t → t I_t V_t.
Arguments Add {_ _}.
Arguments Remove {_ _}.
Arguments Clear {_ _}.
Arguments Consume_read_gas {_ _}.
(* Send [Indexed_data_storage.Change.t] to [t] *)
Definition of_idx {I_t V_t : Set}
(change : Indexed_data_storage.Change.t I_t V_t)
: Change.t I_t V_t :=
match change with
| Indexed_data_storage.Change.Add k v ⇒ Change.Add k v
| Indexed_data_storage.Change.Remove k ⇒ Change.Remove k
| Indexed_data_storage.Change.Clear ⇒ Change.Clear
end.
End Change.
(* @TODO consume changes are identities by now, fix this later *)
Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) (change : Change.t I_t V_t)
: State.t P V_t :=
match change with
| Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
| Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
| Change.Clear ⇒ (State.Map P).(Map.S.empty)
| Change.Consume_read_gas gas key ⇒ state
end.
{P : Path_encoding.S (t := I_t)}
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t) :
let Store := Make absolute_key parse apply in
Eq.t Store (of_kernel P absolute_key [] (to_kernel Store)).
Proof.
constructor; intros; simpl; try reflexivity;
repeat Op.Unfold.all;
try (step; simpl; try rewrite List.app_nil_r; reflexivity);
try (apply List.fold_right_f_eq; hauto lq: on).
Qed.
End Indexed_data_storage.
Module Non_iterable_indexed_data_storage.
Module Eq.
Import Proto_alpha.Storage_sigs.Non_iterable_indexed_data_storage.
Record t {t key value : Set}
{S1 S2 : Non_iterable_indexed_data_storage (t := t) (key := key) (value := value)}
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
}.
Arguments t {_ _ _}.
End Eq.
Module State := Indexed_data_storage.State.
Module Change := Indexed_data_storage.Change.
Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)} :=
@Indexed_data_storage.reduce I_t V_t P.
Module Op := Indexed_data_storage.Op.
Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t)
: Non_iterable_indexed_data_storage (t := C_t) (key := I_t) :=
{|
Non_iterable_indexed_data_storage.mem ctxt k :=
Op.mem (parse ctxt) k;
Non_iterable_indexed_data_storage.get ctxt k :=
Op.get absolute_key (parse ctxt) k;
Non_iterable_indexed_data_storage.find ctxt k :=
Op.find absolute_key (parse ctxt) k;
Non_iterable_indexed_data_storage.update ctxt k v :=
let? change := Op.update absolute_key (parse ctxt) k v in
return? apply ctxt change;
Non_iterable_indexed_data_storage.init_value ctxt k v :=
let? change := Op.init_value absolute_key (parse ctxt) k v in
return? apply ctxt change;
Non_iterable_indexed_data_storage.add ctxt k v :=
apply ctxt (Op.add k v);
Non_iterable_indexed_data_storage.add_or_remove := axiom;
Non_iterable_indexed_data_storage.remove_existing := axiom;
Non_iterable_indexed_data_storage.remove := axiom;
|}.
End Non_iterable_indexed_data_storage.
Module Non_iterable_indexed_carbonated_data_storage_INTERNAL.
Import Proto_alpha.Storage_sigs.Non_iterable_indexed_carbonated_data_storage_INTERNAL.
Module Eq.
Record t {t key value : Set}
(S1 S2 : Non_iterable_indexed_carbonated_data_storage_INTERNAL (t := t) (key := key) (value := value))
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
}.
Arguments t {_ _ _}.
End Eq.
Module State := Indexed_data_storage.State.
Module Op := Indexed_data_storage.Op.
(* Module Change := Indexed_data_storage.Change. *)
Module Change.
Inductive t (I_t V_t : Set) : Set :=
| Add : I_t → V_t → t I_t V_t
| Remove : I_t → t I_t V_t
| Clear : t I_t V_t
| Consume_read_gas : int → I_t → t I_t V_t.
Arguments Add {_ _}.
Arguments Remove {_ _}.
Arguments Clear {_ _}.
Arguments Consume_read_gas {_ _}.
(* Send [Indexed_data_storage.Change.t] to [t] *)
Definition of_idx {I_t V_t : Set}
(change : Indexed_data_storage.Change.t I_t V_t)
: Change.t I_t V_t :=
match change with
| Indexed_data_storage.Change.Add k v ⇒ Change.Add k v
| Indexed_data_storage.Change.Remove k ⇒ Change.Remove k
| Indexed_data_storage.Change.Clear ⇒ Change.Clear
end.
End Change.
(* @TODO consume changes are identities by now, fix this later *)
Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(state : State.t P V_t) (change : Change.t I_t V_t)
: State.t P V_t :=
match change with
| Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
| Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
| Change.Clear ⇒ (State.Map P).(Map.S.empty)
| Change.Consume_read_gas gas key ⇒ state
end.
Gas consumption functions
(* @TODO make these functions return a value of gas (int)
instead of tweaking on the context. The reason is because
after the generalization of Make function these functions
will not have access to [Raw_context.t] anymore *)
Module Gas.
Definition len_key
{I_t : Set} {P : Path_encoding.S (t := I_t)}
(i_value : I_t) : list string :=
P.(Path_encoding.S.to_path) i_value [Storage_functors.len_name].
Definition consume_mem_gas
(c_value : Raw_context.t) (key_value : Context.key)
: M? Raw_context.t :=
Raw_context.consume_gas c_value
(Storage_costs.read_access (List.length key_value) 0).
Definition consume_read_gas
{I_t : Set} (P : Path_encoding.S (t := I_t))
(get : Raw_context.t → Context.key → M? bytes)
(c_value : Raw_context.t) (i_value : I_t)
: M? Raw_context.t :=
let len_key := len_key (P := P) i_value in
let? len := get c_value len_key in
let? read_bytes := decode_len_value len_key len in
let cost := Storage_costs.read_access (List.length len_key)
read_bytes in
Raw_context.consume_gas c_value cost.
(* @TODO This (V : VALUE) dependence is leaking up to Make
call, maybe we should define this as a [Parameter]? *)
Definition to_bytes {V_t : Set}
{V : VALUE (t := V_t)} (v : V.(VALUE.t)) : bytes :=
(@Storage_functors.Make_encoder V_t V).(
Storage_functors.ENCODER.to_bytes) v.
Definition consume_serialize_write_gas
{A I_t V_t : Set} (P : Path_encoding.S (t := I_t))
(V : VALUE (t := V_t))
(set : Raw_context.t → list string → bytes → M? A)
(c_value : Raw_context.t) (i_value : I_t)
(v_value : V.(VALUE.t)) : M? (A × bytes) :=
let bytes_value := to_bytes v_value in
let len := Bytes.length bytes_value in
let? c_value := Raw_context.consume_gas c_value
(Gas_limit_repr.alloc_mbytes_cost len) in
let cost := Storage_costs.write_access len in
let? c_value := Raw_context.consume_gas c_value cost in
let? c_value := set c_value (len_key (P := P) i_value)
(encode_len_value bytes_value) in
return? (c_value, bytes_value).
Definition consume_remove_gas {A I_t : Set} {ipath : Set → Set}
{P : Path_encoding.S (t := I_t)}
{I : INDEX (t := I_t) (ipath := ipath)}
(del : Raw_context.t → list string → M? A)
(c_value : Raw_context.t) (i_value : I.(INDEX.t)) : M? A :=
let? c_value :=
Raw_context.consume_gas c_value (Storage_costs.write_access 0)
in
del c_value (len_key (P := P) i_value).
Definition data_key {I_t : Set} (P : Path_encoding.S (t := I_t))
(i_value : I_t)
: list string :=
P.(Path_encoding.S.to_path) i_value [ data_name].
End Gas.
(* @TODO How to take gas in account in these ops *)
Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t)
: Non_iterable_indexed_carbonated_data_storage_INTERNAL
(t := C_t) (key := I_t) (value := V_t) :=
{|
Non_iterable_indexed_carbonated_data_storage_INTERNAL.mem ctxt k :=
return? (apply ctxt (Change.Consume_read_gas axiom k),
Op.mem (parse ctxt) k);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.get
ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.get (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.find
ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.find (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.update ctxt k v :=
let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.init_value ctxt k v :=
let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.add
ctxt k v :=
let change := Change.of_idx (Op.add k v) in
return? (apply ctxt change, 0, true);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.add_or_remove := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.remove_existing := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.remove := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.list_values := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.fold_keys_unaccounted := axiom;
|}.
End Non_iterable_indexed_carbonated_data_storage_INTERNAL.
Module Non_iterable_indexed_carbonated_data_storage.
Import Proto_alpha.Storage_sigs.Non_iterable_indexed_carbonated_data_storage.
Module Eq.
Record t {t key value : Set}
{S1 S2 : Non_iterable_indexed_carbonated_data_storage (t := t) (key := key) (value := value)}
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
}.
Arguments t {_ _ _}.
End Eq.
Module State := Non_iterable_indexed_carbonated_data_storage_INTERNAL.State.
Module Change := Non_iterable_indexed_carbonated_data_storage_INTERNAL.Change.
Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)} := @Non_iterable_indexed_carbonated_data_storage_INTERNAL.reduce I_t V_t P.
Module Op := Non_iterable_indexed_carbonated_data_storage_INTERNAL.Op.
(* @TODO How to take gas in account in these ops *)
Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t)
: Non_iterable_indexed_carbonated_data_storage (t := C_t) (key := I_t) :=
{|
Non_iterable_indexed_carbonated_data_storage.mem ctxt k :=
return? (apply ctxt (Change.Consume_read_gas axiom k),
Op.mem (parse ctxt) k);
Non_iterable_indexed_carbonated_data_storage.get ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.get (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage.find ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.find (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage.update ctxt k v :=
let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage.init_value ctxt k v :=
let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage.add ctxt k v :=
let change := Change.of_idx (Op.add k v) in
return? (apply ctxt change, 0, true);
Non_iterable_indexed_carbonated_data_storage.add_or_remove := axiom;
Non_iterable_indexed_carbonated_data_storage.remove_existing := axiom;
Non_iterable_indexed_carbonated_data_storage.remove := axiom;
|}.
End Non_iterable_indexed_carbonated_data_storage.
Module Indexed_data_snapshotable_storage.
Module Eq.
Parameter t : ∀ {t snapshot key value : Set},
Indexed_data_snapshotable_storage
(t := t) (snapshot := snapshot) (key := key) (value := value) →
Indexed_data_snapshotable_storage
(t := t) (snapshot := snapshot) (key := key) (value := value) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (snapshot key value : Set), Set.
End State.
Module Change.
Parameter t : ∀ (snapshot key value : Set), Set.
End Change.
Parameter reduce : ∀ {snapshot key value},
State.t snapshot key value →
Change.t snapshot key value →
State.t snapshot key value.
Parameter Make : ∀ {snapshot key value : Set}
(parse : Raw_context.t → State.t snapshot key value)
(apply : Raw_context.t → Change.t snapshot key value → Raw_context.t),
Indexed_data_snapshotable_storage
(t := Raw_context.t) (snapshot := snapshot) (key := key) (value := value).
End Indexed_data_snapshotable_storage.
Module Data_set_storage.
Module Eq.
Import Proto_alpha.Storage_sigs.Data_set_storage.
Record t {t elt : Set}
{S1 S2 : Data_set_storage (t := t) (elt := elt)}
: Prop := {
mem ctxt value : S1.(mem) ctxt value = S2.(mem) ctxt value;
add ctxt value : S1.(add) ctxt value = S2.(add) ctxt value;
remove ctxt value : S1.(remove) ctxt value = S2.(remove) ctxt value;
elements ctxt : S1.(elements) ctxt = S2.(elements) ctxt;
clear ctxt : S1.(clear) ctxt = S2.(clear) ctxt;
}.
Arguments t {_ _}.
End Eq.
Module State.
Definition compare {elt : Set} (P : Path_encoding.S (t := elt))
(x1 x2 : elt) : int :=
let path1 := P.(Path_encoding.S.to_path) x1 [] in
let path2 := P.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
Definition Ord {elt : Set} (P : Path_encoding.S (t := elt)) :
Compare.COMPARABLE (t := elt) :=
{| Compare.COMPARABLE.compare := compare P |}.
Definition _Set {elt : Set} (P : Path_encoding.S (t := elt))
: _Set.S (elt := elt) (t := _) :=
_Set.Make (Ord P).
Definition t {elt : Set} (P : Path_encoding.S (t := elt)) : Set :=
(_Set P).(_Set.S.t).
End State.
Module Change.
Inductive t (elt : Set) : Set :=
| Add : elt → t elt
| Clear : t elt
| Remove : elt → t elt.
Arguments Add {_}.
Arguments Clear {_}.
Arguments Remove {_}.
End Change.
Definition reduce {elt : Set} {P : Path_encoding.S (t := elt)}
(state : State.t P) (change : Change.t elt) : State.t P :=
match change with
| Change.Add value ⇒ (State._Set P).(_Set.S.add) value state
| Change.Clear ⇒ (State._Set P).(_Set.S.empty)
| Change.Remove value ⇒ (State._Set P).(_Set.S.remove) value state
end.
Module Op.
Definition mem {elt : Set} {P : Path_encoding.S (t := elt)}
(state : State.t P) (value : elt) : bool :=
(State._Set P).(_Set.S.mem) value state.
Definition add {elt : Set} (value : elt) : Change.t elt :=
Change.Add value.
Definition remove {elt : Set} (value : elt) : Change.t elt :=
Change.Remove value.
Definition elements {elt : Set} {P : Path_encoding.S (t := elt)}
(state : State.t P) : list elt :=
(State._Set P).(_Set.S.elements) state.
Definition clear {elt : Set} : Change.t elt :=
Change.Clear.
Definition fold {elt : Set} {P : Path_encoding.S (t := elt)} {a : Set}
(state : State.t P) (x : a) (f : elt → a → a) : a :=
(State._Set P).(_Set.S.fold) f state x.
Ltac unfold_all :=
repeat unfold mem, add, remove, elements,
clear, fold, State._Set.
End Op.
Definition Make {elt : Set} {P : Path_encoding.S (t := elt)}
(parse : Raw_context.t → State.t P)
(apply : Raw_context.t → Change.t elt → Raw_context.t)
: Data_set_storage (t := Raw_context.t) (elt := elt) :=
{|
Data_set_storage.mem ctxt value :=
Op.mem (parse ctxt) value;
Data_set_storage.add ctxt value :=
apply ctxt (Op.add value);
Data_set_storage.remove ctxt value :=
apply ctxt (Op.remove value);
Data_set_storage.elements ctxt :=
Op.elements (parse ctxt);
Data_set_storage.fold a ctxt order x f :=
Op.fold (parse ctxt) x f;
Data_set_storage.clear ctxt :=
apply ctxt Op.clear;
|}.
End Data_set_storage.
Module Carbonated_data_set_storage.
Module Eq.
Parameter t : ∀ {t elt : Set},
Carbonated_data_set_storage (t := t) (elt := elt) →
Carbonated_data_set_storage (t := t) (elt := elt) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (elt : Set), Set.
End State.
Module Change.
Parameter t : ∀ (elt : Set), Set.
End Change.
Parameter reduce : ∀ {elt},
State.t elt → Change.t elt → State.t elt.
Parameter Make : ∀ {elt : Set}
(parse : Raw_context.t → State.t elt)
(apply : Raw_context.t → Change.t elt → Raw_context.t),
Carbonated_data_set_storage
(t := Raw_context.t) (elt := elt).
End Carbonated_data_set_storage.
Module Simple_single_data_storage.
Module Eq.
Parameter t : ∀ {value : Set},
Storage.Simple_single_data_storage (value := value) →
Storage.Simple_single_data_storage (value := value) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (value : Set), Set.
End State.
Module Change.
Parameter t : ∀ (value : Set), Set.
End Change.
Parameter reduce : ∀ {value},
State.t value → Change.t value → State.t value.
Parameter Make : ∀ {value : Set}
(parse : Raw_context.t → State.t value)
(apply : Raw_context.t → Change.t value → Raw_context.t),
Storage.Simple_single_data_storage (value := value).
End Simple_single_data_storage.
Module For_cycle.
Module Eq.
Import Proto_alpha.Storage.FOR_CYCLE.
Record t
{S1 S2 : Storage.FOR_CYCLE}
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
}.
End Eq.
instead of tweaking on the context. The reason is because
after the generalization of Make function these functions
will not have access to [Raw_context.t] anymore *)
Module Gas.
Definition len_key
{I_t : Set} {P : Path_encoding.S (t := I_t)}
(i_value : I_t) : list string :=
P.(Path_encoding.S.to_path) i_value [Storage_functors.len_name].
Definition consume_mem_gas
(c_value : Raw_context.t) (key_value : Context.key)
: M? Raw_context.t :=
Raw_context.consume_gas c_value
(Storage_costs.read_access (List.length key_value) 0).
Definition consume_read_gas
{I_t : Set} (P : Path_encoding.S (t := I_t))
(get : Raw_context.t → Context.key → M? bytes)
(c_value : Raw_context.t) (i_value : I_t)
: M? Raw_context.t :=
let len_key := len_key (P := P) i_value in
let? len := get c_value len_key in
let? read_bytes := decode_len_value len_key len in
let cost := Storage_costs.read_access (List.length len_key)
read_bytes in
Raw_context.consume_gas c_value cost.
(* @TODO This (V : VALUE) dependence is leaking up to Make
call, maybe we should define this as a [Parameter]? *)
Definition to_bytes {V_t : Set}
{V : VALUE (t := V_t)} (v : V.(VALUE.t)) : bytes :=
(@Storage_functors.Make_encoder V_t V).(
Storage_functors.ENCODER.to_bytes) v.
Definition consume_serialize_write_gas
{A I_t V_t : Set} (P : Path_encoding.S (t := I_t))
(V : VALUE (t := V_t))
(set : Raw_context.t → list string → bytes → M? A)
(c_value : Raw_context.t) (i_value : I_t)
(v_value : V.(VALUE.t)) : M? (A × bytes) :=
let bytes_value := to_bytes v_value in
let len := Bytes.length bytes_value in
let? c_value := Raw_context.consume_gas c_value
(Gas_limit_repr.alloc_mbytes_cost len) in
let cost := Storage_costs.write_access len in
let? c_value := Raw_context.consume_gas c_value cost in
let? c_value := set c_value (len_key (P := P) i_value)
(encode_len_value bytes_value) in
return? (c_value, bytes_value).
Definition consume_remove_gas {A I_t : Set} {ipath : Set → Set}
{P : Path_encoding.S (t := I_t)}
{I : INDEX (t := I_t) (ipath := ipath)}
(del : Raw_context.t → list string → M? A)
(c_value : Raw_context.t) (i_value : I.(INDEX.t)) : M? A :=
let? c_value :=
Raw_context.consume_gas c_value (Storage_costs.write_access 0)
in
del c_value (len_key (P := P) i_value).
Definition data_key {I_t : Set} (P : Path_encoding.S (t := I_t))
(i_value : I_t)
: list string :=
P.(Path_encoding.S.to_path) i_value [ data_name].
End Gas.
(* @TODO How to take gas in account in these ops *)
Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t)
: Non_iterable_indexed_carbonated_data_storage_INTERNAL
(t := C_t) (key := I_t) (value := V_t) :=
{|
Non_iterable_indexed_carbonated_data_storage_INTERNAL.mem ctxt k :=
return? (apply ctxt (Change.Consume_read_gas axiom k),
Op.mem (parse ctxt) k);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.get
ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.get (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.find
ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.find (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.update ctxt k v :=
let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.init_value ctxt k v :=
let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.add
ctxt k v :=
let change := Change.of_idx (Op.add k v) in
return? (apply ctxt change, 0, true);
Non_iterable_indexed_carbonated_data_storage_INTERNAL.add_or_remove := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.remove_existing := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.remove := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.list_values := axiom;
Non_iterable_indexed_carbonated_data_storage_INTERNAL.fold_keys_unaccounted := axiom;
|}.
End Non_iterable_indexed_carbonated_data_storage_INTERNAL.
Module Non_iterable_indexed_carbonated_data_storage.
Import Proto_alpha.Storage_sigs.Non_iterable_indexed_carbonated_data_storage.
Module Eq.
Record t {t key value : Set}
{S1 S2 : Non_iterable_indexed_carbonated_data_storage (t := t) (key := key) (value := value)}
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
update ctxt path value :
S1.(update) ctxt path value = S2.(update) ctxt path value;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
add_or_remove ctxt path value :
S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
}.
Arguments t {_ _ _}.
End Eq.
Module State := Non_iterable_indexed_carbonated_data_storage_INTERNAL.State.
Module Change := Non_iterable_indexed_carbonated_data_storage_INTERNAL.Change.
Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)} := @Non_iterable_indexed_carbonated_data_storage_INTERNAL.reduce I_t V_t P.
Module Op := Non_iterable_indexed_carbonated_data_storage_INTERNAL.Op.
(* @TODO How to take gas in account in these ops *)
Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
(absolute_key : C_t → Context.key)
(parse : C_t → State.t P V_t)
(apply : C_t → Change.t I_t V_t → Raw_context.t)
: Non_iterable_indexed_carbonated_data_storage (t := C_t) (key := I_t) :=
{|
Non_iterable_indexed_carbonated_data_storage.mem ctxt k :=
return? (apply ctxt (Change.Consume_read_gas axiom k),
Op.mem (parse ctxt) k);
Non_iterable_indexed_carbonated_data_storage.get ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.get (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage.find ctxt k :=
let change := (Change.Consume_read_gas axiom k) in
let? value := Op.find (absolute_key ctxt) (parse ctxt) k in
return? (apply ctxt change, value);
Non_iterable_indexed_carbonated_data_storage.update ctxt k v :=
let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage.init_value ctxt k v :=
let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
return? (apply ctxt (Change.of_idx change), 0);
Non_iterable_indexed_carbonated_data_storage.add ctxt k v :=
let change := Change.of_idx (Op.add k v) in
return? (apply ctxt change, 0, true);
Non_iterable_indexed_carbonated_data_storage.add_or_remove := axiom;
Non_iterable_indexed_carbonated_data_storage.remove_existing := axiom;
Non_iterable_indexed_carbonated_data_storage.remove := axiom;
|}.
End Non_iterable_indexed_carbonated_data_storage.
Module Indexed_data_snapshotable_storage.
Module Eq.
Parameter t : ∀ {t snapshot key value : Set},
Indexed_data_snapshotable_storage
(t := t) (snapshot := snapshot) (key := key) (value := value) →
Indexed_data_snapshotable_storage
(t := t) (snapshot := snapshot) (key := key) (value := value) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (snapshot key value : Set), Set.
End State.
Module Change.
Parameter t : ∀ (snapshot key value : Set), Set.
End Change.
Parameter reduce : ∀ {snapshot key value},
State.t snapshot key value →
Change.t snapshot key value →
State.t snapshot key value.
Parameter Make : ∀ {snapshot key value : Set}
(parse : Raw_context.t → State.t snapshot key value)
(apply : Raw_context.t → Change.t snapshot key value → Raw_context.t),
Indexed_data_snapshotable_storage
(t := Raw_context.t) (snapshot := snapshot) (key := key) (value := value).
End Indexed_data_snapshotable_storage.
Module Data_set_storage.
Module Eq.
Import Proto_alpha.Storage_sigs.Data_set_storage.
Record t {t elt : Set}
{S1 S2 : Data_set_storage (t := t) (elt := elt)}
: Prop := {
mem ctxt value : S1.(mem) ctxt value = S2.(mem) ctxt value;
add ctxt value : S1.(add) ctxt value = S2.(add) ctxt value;
remove ctxt value : S1.(remove) ctxt value = S2.(remove) ctxt value;
elements ctxt : S1.(elements) ctxt = S2.(elements) ctxt;
clear ctxt : S1.(clear) ctxt = S2.(clear) ctxt;
}.
Arguments t {_ _}.
End Eq.
Module State.
Definition compare {elt : Set} (P : Path_encoding.S (t := elt))
(x1 x2 : elt) : int :=
let path1 := P.(Path_encoding.S.to_path) x1 [] in
let path2 := P.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
Definition Ord {elt : Set} (P : Path_encoding.S (t := elt)) :
Compare.COMPARABLE (t := elt) :=
{| Compare.COMPARABLE.compare := compare P |}.
Definition _Set {elt : Set} (P : Path_encoding.S (t := elt))
: _Set.S (elt := elt) (t := _) :=
_Set.Make (Ord P).
Definition t {elt : Set} (P : Path_encoding.S (t := elt)) : Set :=
(_Set P).(_Set.S.t).
End State.
Module Change.
Inductive t (elt : Set) : Set :=
| Add : elt → t elt
| Clear : t elt
| Remove : elt → t elt.
Arguments Add {_}.
Arguments Clear {_}.
Arguments Remove {_}.
End Change.
Definition reduce {elt : Set} {P : Path_encoding.S (t := elt)}
(state : State.t P) (change : Change.t elt) : State.t P :=
match change with
| Change.Add value ⇒ (State._Set P).(_Set.S.add) value state
| Change.Clear ⇒ (State._Set P).(_Set.S.empty)
| Change.Remove value ⇒ (State._Set P).(_Set.S.remove) value state
end.
Module Op.
Definition mem {elt : Set} {P : Path_encoding.S (t := elt)}
(state : State.t P) (value : elt) : bool :=
(State._Set P).(_Set.S.mem) value state.
Definition add {elt : Set} (value : elt) : Change.t elt :=
Change.Add value.
Definition remove {elt : Set} (value : elt) : Change.t elt :=
Change.Remove value.
Definition elements {elt : Set} {P : Path_encoding.S (t := elt)}
(state : State.t P) : list elt :=
(State._Set P).(_Set.S.elements) state.
Definition clear {elt : Set} : Change.t elt :=
Change.Clear.
Definition fold {elt : Set} {P : Path_encoding.S (t := elt)} {a : Set}
(state : State.t P) (x : a) (f : elt → a → a) : a :=
(State._Set P).(_Set.S.fold) f state x.
Ltac unfold_all :=
repeat unfold mem, add, remove, elements,
clear, fold, State._Set.
End Op.
Definition Make {elt : Set} {P : Path_encoding.S (t := elt)}
(parse : Raw_context.t → State.t P)
(apply : Raw_context.t → Change.t elt → Raw_context.t)
: Data_set_storage (t := Raw_context.t) (elt := elt) :=
{|
Data_set_storage.mem ctxt value :=
Op.mem (parse ctxt) value;
Data_set_storage.add ctxt value :=
apply ctxt (Op.add value);
Data_set_storage.remove ctxt value :=
apply ctxt (Op.remove value);
Data_set_storage.elements ctxt :=
Op.elements (parse ctxt);
Data_set_storage.fold a ctxt order x f :=
Op.fold (parse ctxt) x f;
Data_set_storage.clear ctxt :=
apply ctxt Op.clear;
|}.
End Data_set_storage.
Module Carbonated_data_set_storage.
Module Eq.
Parameter t : ∀ {t elt : Set},
Carbonated_data_set_storage (t := t) (elt := elt) →
Carbonated_data_set_storage (t := t) (elt := elt) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (elt : Set), Set.
End State.
Module Change.
Parameter t : ∀ (elt : Set), Set.
End Change.
Parameter reduce : ∀ {elt},
State.t elt → Change.t elt → State.t elt.
Parameter Make : ∀ {elt : Set}
(parse : Raw_context.t → State.t elt)
(apply : Raw_context.t → Change.t elt → Raw_context.t),
Carbonated_data_set_storage
(t := Raw_context.t) (elt := elt).
End Carbonated_data_set_storage.
Module Simple_single_data_storage.
Module Eq.
Parameter t : ∀ {value : Set},
Storage.Simple_single_data_storage (value := value) →
Storage.Simple_single_data_storage (value := value) →
Prop.
End Eq.
Module State.
Parameter t : ∀ (value : Set), Set.
End State.
Module Change.
Parameter t : ∀ (value : Set), Set.
End Change.
Parameter reduce : ∀ {value},
State.t value → Change.t value → State.t value.
Parameter Make : ∀ {value : Set}
(parse : Raw_context.t → State.t value)
(apply : Raw_context.t → Change.t value → Raw_context.t),
Storage.Simple_single_data_storage (value := value).
End Simple_single_data_storage.
Module For_cycle.
Module Eq.
Import Proto_alpha.Storage.FOR_CYCLE.
Record t
{S1 S2 : Storage.FOR_CYCLE}
: Prop := {
mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
init_value ctxt path value :
S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
remove_existing ctxt path :
S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
}.
End Eq.
The simulation state.
Module State.
Definition compare (P : Path_encoding.S (t := Cycle_repr.t))
(x1 x2 : Cycle_repr.t) : int :=
let path1 := P.(Path_encoding.S.to_path) x1 [] in
let path2 := P.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
Definition Ord (P : Path_encoding.S (t := Cycle_repr.t)) :
Compare.COMPARABLE :=
{| Compare.COMPARABLE.compare := compare P |}.
Definition Map (P : Path_encoding.S (t := Cycle_repr.t)) :
Map.S (key := Cycle_repr.t) (t := _) :=
Map.Make (Ord P).
Definition t (P : Path_encoding.S (t := Cycle_repr.t))
: Set :=
(Map P).(Map.S.t) (option Seed_repr.seed).
End State.
Module Change.
Inductive t : Set :=
| Add : Cycle_repr.t → Seed_repr.seed → t
| Remove : Cycle_repr.t → t.
End Change.
Definition reduce {P : Path_encoding.S (t := Cycle_repr.t)}
(state : State.t P) (change : Change.t)
: State.t P :=
match change with
| Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
| Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
end.
Module Op.
Definition mem {P : Path_encoding.S (t := Cycle_repr.t)}
(state : State.t P) (k : Cycle_repr.t) : bool :=
(State.Map P).(Map.S.mem) k state.
Definition init_value {P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(state : State.t P) (k : Cycle_repr.t) (v : Seed_repr.seed) : M? (Change.t) :=
if mem state k
then let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Existing_key (absolute_key ++ path)))
else return? Change.Add k v.
Definition get {P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(state : State.t P) (k : Cycle_repr.t)
: M? Seed_repr.seed :=
match (State.Map P).(Map.S.find) k state with
| Some (Some v) ⇒ return? v
| Some None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data (absolute_key ++ path)))
| None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error"
Raw_context.storage_error
(Raw_context.Missing_key
(absolute_key ++ path)
Raw_context.Get))
end.
Definition remove_existing
{P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(state : State.t P) (k : Cycle_repr.t)
: M? Change.t :=
if Op.mem state k
then return? (Change.Remove k)
else let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error"
Raw_context.storage_error
(Raw_context.Missing_key
(absolute_key ++ path)
Raw_context.Del)).
Module Unfold.
Ltac all :=
repeat unfold mem, init_value, get, remove_existing, State.Map.
End Unfold.
End Op.
Definition Make {P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(parse : Raw_context.t → State.t P)
(apply : Raw_context.t → Change.t → Raw_context.t)
: Storage.FOR_CYCLE :=
{|
Storage.FOR_CYCLE.mem ctxt k :=
Op.mem (parse ctxt) k;
Storage.FOR_CYCLE.get ctxt k :=
Op.get absolute_key (parse ctxt) k;
Storage.FOR_CYCLE.init_value ctxt k v :=
let? change := Op.init_value absolute_key (parse ctxt) k v in
return? apply ctxt change;
Storage.FOR_CYCLE.remove_existing ctxt k :=
let state := parse ctxt in
let? change := Op.remove_existing absolute_key state k in
return? apply ctxt change;
|}.
End For_cycle.
Definition compare (P : Path_encoding.S (t := Cycle_repr.t))
(x1 x2 : Cycle_repr.t) : int :=
let path1 := P.(Path_encoding.S.to_path) x1 [] in
let path2 := P.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
Definition Ord (P : Path_encoding.S (t := Cycle_repr.t)) :
Compare.COMPARABLE :=
{| Compare.COMPARABLE.compare := compare P |}.
Definition Map (P : Path_encoding.S (t := Cycle_repr.t)) :
Map.S (key := Cycle_repr.t) (t := _) :=
Map.Make (Ord P).
Definition t (P : Path_encoding.S (t := Cycle_repr.t))
: Set :=
(Map P).(Map.S.t) (option Seed_repr.seed).
End State.
Module Change.
Inductive t : Set :=
| Add : Cycle_repr.t → Seed_repr.seed → t
| Remove : Cycle_repr.t → t.
End Change.
Definition reduce {P : Path_encoding.S (t := Cycle_repr.t)}
(state : State.t P) (change : Change.t)
: State.t P :=
match change with
| Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
| Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
end.
Module Op.
Definition mem {P : Path_encoding.S (t := Cycle_repr.t)}
(state : State.t P) (k : Cycle_repr.t) : bool :=
(State.Map P).(Map.S.mem) k state.
Definition init_value {P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(state : State.t P) (k : Cycle_repr.t) (v : Seed_repr.seed) : M? (Change.t) :=
if mem state k
then let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Existing_key (absolute_key ++ path)))
else return? Change.Add k v.
Definition get {P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(state : State.t P) (k : Cycle_repr.t)
: M? Seed_repr.seed :=
match (State.Map P).(Map.S.find) k state with
| Some (Some v) ⇒ return? v
| Some None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error" Raw_context.storage_error
(Raw_context.Corrupted_data (absolute_key ++ path)))
| None ⇒
let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error"
Raw_context.storage_error
(Raw_context.Missing_key
(absolute_key ++ path)
Raw_context.Get))
end.
Definition remove_existing
{P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(state : State.t P) (k : Cycle_repr.t)
: M? Change.t :=
if Op.mem state k
then return? (Change.Remove k)
else let path := P.(Path_encoding.S.to_path) k [] in
Error_monad.error_value
(Build_extensible "Storage_error"
Raw_context.storage_error
(Raw_context.Missing_key
(absolute_key ++ path)
Raw_context.Del)).
Module Unfold.
Ltac all :=
repeat unfold mem, init_value, get, remove_existing, State.Map.
End Unfold.
End Op.
Definition Make {P : Path_encoding.S (t := Cycle_repr.t)}
(absolute_key : Context.key)
(parse : Raw_context.t → State.t P)
(apply : Raw_context.t → Change.t → Raw_context.t)
: Storage.FOR_CYCLE :=
{|
Storage.FOR_CYCLE.mem ctxt k :=
Op.mem (parse ctxt) k;
Storage.FOR_CYCLE.get ctxt k :=
Op.get absolute_key (parse ctxt) k;
Storage.FOR_CYCLE.init_value ctxt k v :=
let? change := Op.init_value absolute_key (parse ctxt) k v in
return? apply ctxt change;
Storage.FOR_CYCLE.remove_existing ctxt k :=
let state := parse ctxt in
let? change := Op.remove_existing absolute_key state k in
return? apply ctxt change;
|}.
End For_cycle.