Skip to main content

💾 Storage_sigs.v

Simulations

See code, Gitlab , OCaml

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.
Simulation state for a [Single_data_storage].
  Definition t (a : Set) : Set := option a.

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
    | NoneNone
    | Some value
      match Data_encoding.Binary.to_bytes_opt None encoding value with
      | NoneNone (* We will expect this case not to happen in the proofs *)
      | Some bytesSome 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.

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 |}.

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

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

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.