💾 Storage_sigs.v
Simulations
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Context.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Single_data_storage.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Context.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Module Single_data_storage.
Simulation state for a [Single_data_storage].
Conversion back to a value in [Context].
Definition to_context {a : Set} (encoding : Data_encoding.t a)
(state : t a) : option Context.value :=
match state with
| None ⇒ None
| Some value ⇒
match Data_encoding.Binary.to_bytes_opt None encoding value with
| None ⇒ None (* We will expect this case not to happen in the proofs *)
| Some bytes ⇒ Some bytes
end
end.
End Single_data_storage.
Module Indexed_map.
(state : t a) : option Context.value :=
match state with
| None ⇒ None
| Some value ⇒
match Data_encoding.Binary.to_bytes_opt None encoding value with
| None ⇒ None (* We will expect this case not to happen in the proofs *)
| Some bytes ⇒ Some bytes
end
end.
End Single_data_storage.
Module Indexed_map.
The comparison function extracted from an index.
Definition compare {I_t : Set} (I : Path_encoding.S (t := I_t))
(x1 x2 : I_t) : int :=
let path1 := I.(Path_encoding.S.to_path) x1 [] in
let path2 := I.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
(x1 x2 : I_t) : int :=
let path1 := I.(Path_encoding.S.to_path) x1 [] in
let path2 := I.(Path_encoding.S.to_path) x2 [] in
Context.Key.compare path1 path2.
The comparable module extracted from an index.
Definition Ord {I_t : Set} (I : Path_encoding.S (t := I_t)) :
Compare.COMPARABLE (t := I_t) :=
{| Compare.COMPARABLE.compare := compare I |}.
Compare.COMPARABLE (t := I_t) :=
{| Compare.COMPARABLE.compare := compare I |}.
The [Map] functor instanciated for a particular index.
Definition Map {I_t : Set} (I : Path_encoding.S (t := I_t)) :
Map.S (key := I_t) (t := _) :=
Map.Make (Ord I).
Map.S (key := I_t) (t := _) :=
Map.Make (Ord I).
The type of maps indexed by a [Path_encoding.S].
Definition t {I_t : Set} (I : Path_encoding.S (t := I_t))
(V_t : Set) : Set :=
(Map I).(Map.S.t) V_t.
End Indexed_map.
Module Indexed_set.
Definition _Set {I_t : Set} (I : Path_encoding.S (t := I_t)) :
_Set.S (elt := I_t) (t := _) :=
_Set.Make (Indexed_map.Ord I).
(V_t : Set) : Set :=
(Map I).(Map.S.t) V_t.
End Indexed_map.
Module Indexed_set.
Definition _Set {I_t : Set} (I : Path_encoding.S (t := I_t)) :
_Set.S (elt := I_t) (t := _) :=
_Set.Make (Indexed_map.Ord I).
The type of sets indexed by a [Path_encoding.S].
Definition t {I_t : Set} (I : Path_encoding.S (t := I_t)) : Set :=
(_Set I).(_Set.S.t).
End Indexed_set.
Module Indexed_data_storage.
Definition t {I_t : Set} (I : Path_encoding.S (t := I_t))
(V_t : Set) : Set :=
Indexed_map.t I V_t.
Definition to_context_carbonated {I_t V_t : Set}
{I : Path_encoding.S (t := I_t)}
(ctxt : Context.t) (path : Context.key) (state : t I V_t) : Context.t.
Admitted.
End Indexed_data_storage.
Module Data_set_storage.
Definition t {I_t : Set} (I : Path_encoding.S (t := I_t)) : Set :=
Indexed_set.t I.
End Data_set_storage.
Module Indexed_data_snapshotable_storage.
Module t.
Record record {I_t Snapshot_index_t : Set}
{I : Path_encoding.S (t := I_t)}
{Snapshot_index : Path_encoding.S (t := Snapshot_index_t)}
{V_t : Set} :
Set := {
data : Indexed_map.t I V_t;
snapshots : Indexed_map.t Snapshot_index (Indexed_map.t I V_t);
}.
End t.
Definition t := @t.record.
Arguments t {_ _}.
End Indexed_data_snapshotable_storage.
(_Set I).(_Set.S.t).
End Indexed_set.
Module Indexed_data_storage.
Definition t {I_t : Set} (I : Path_encoding.S (t := I_t))
(V_t : Set) : Set :=
Indexed_map.t I V_t.
Definition to_context_carbonated {I_t V_t : Set}
{I : Path_encoding.S (t := I_t)}
(ctxt : Context.t) (path : Context.key) (state : t I V_t) : Context.t.
Admitted.
End Indexed_data_storage.
Module Data_set_storage.
Definition t {I_t : Set} (I : Path_encoding.S (t := I_t)) : Set :=
Indexed_set.t I.
End Data_set_storage.
Module Indexed_data_snapshotable_storage.
Module t.
Record record {I_t Snapshot_index_t : Set}
{I : Path_encoding.S (t := I_t)}
{Snapshot_index : Path_encoding.S (t := Snapshot_index_t)}
{V_t : Set} :
Set := {
data : Indexed_map.t I V_t;
snapshots : Indexed_map.t Snapshot_index (Indexed_map.t I V_t);
}.
End t.
Definition t := @t.record.
Arguments t {_ _}.
End Indexed_data_snapshotable_storage.