diff --git a/_CoqProject b/_CoqProject
index 7a06a88..3c4937c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,5 +10,6 @@ theories/Conversion.v
 theories/Utilities.v
 theories/BackupPlanner.v
 theories/AssemblyCache.v
+theories/Store.v
 theories/MakeML.v
 theories/Version.v
diff --git a/bin/lxr_assembly.ml b/bin/lxr_assembly.ml
index 06fc6d7..5921342 100644
--- a/bin/lxr_assembly.ml
+++ b/bin/lxr_assembly.ml
@@ -62,7 +62,7 @@ let main () = Arg.parse argspec anon_args_fun "lxr_assembly: vaf";
     let e1 = Environment.EnvironmentWritable.env_add_file_block "test1M" e0 bi in
     let e2 = Environment.EnvironmentWritable.env_add_aid_key (aid a') e1 {pkey="abc97391af";ivec="323453";localnchunks=Nchunks.to_positive c.config_nchunks;localid=c.my_id} in
     let relkeys = Environment.keys e2 in
-    let relkey = List.assoc (aid a') relkeys in
+    let relkey = List.assoc (aid a') relkeys.entries in
     let (a'', b') = Elykseer__Lxr.Assembly.finish a' b in
     match Elykseer__Lxr.Assembly.encrypt a'' b' relkey with
     | None -> Lwt_io.printl "failed to encrypt"
diff --git a/bin/lxr_backup.ml b/bin/lxr_backup.ml
index edadabd..2bb40d7 100644
--- a/bin/lxr_backup.ml
+++ b/bin/lxr_backup.ml
@@ -135,7 +135,7 @@ let validate_fileblocks fname fhash bis =
     else Lwt.return ()
 
 let output_rel_files e (bp : backup_plan) =
-  let fbis = Env.consolidate_files e.fblocks in
+  let fbis = Env.consolidate_files e.fblocks.entries in
   if !arg_dryrun then
     Lwt_list.iter_s (fun (fname, bis) -> let fhash = sha256 fname in
                        let%lwt () = validate_fileblocks fname fhash bis in
@@ -159,7 +159,7 @@ let output_rel_files e (bp : backup_plan) =
 let output_rel_keys e =
   let%lwt rel = Relkeys.new_map e.config in
   let%lwt () = Lwt_list.iter_s (fun (aid, ki) ->
-                                let%lwt _ = Relkeys.add aid ki rel in Lwt.return ()) e.keys in
+                                let%lwt _ = Relkeys.add aid ki rel in Lwt.return ()) e.keys.entries in
   Relkeys.close_map rel
 
 let output_relations e (bp : backup_plan) =
diff --git a/doc/00_Content.md b/doc/00_Content.md
new file mode 100644
index 0000000..8daa1de
--- /dev/null
+++ b/doc/00_Content.md
@@ -0,0 +1,12 @@
+
+# Content
+
+## 01 [Functionality](01_Functionality.md)
+
+## 02 Information [Relations](02_Relations.md)
+
+## 03 Data [Storage](03_Storage.md)
+
+## 04 Code organisation in [Modules](04_Modules.md)
+
+## 05 [Caching](05_AssemblyCache.md) data 
\ No newline at end of file
diff --git a/doc/01_Content.md b/doc/01_Content.md
deleted file mode 100644
index d8163e9..0000000
--- a/doc/01_Content.md
+++ /dev/null
@@ -1,10 +0,0 @@
-
-# Content
-
-## [Functionality](02_Functionality.md)
-
-## Information [Relations](03_Relations.md)
-
-## Data [Storage](04_Storage.md)
-
-## Code organisation in [Modules](05_Modules.md)
diff --git a/doc/02_Functionality.md b/doc/01_Functionality.md
similarity index 100%
rename from doc/02_Functionality.md
rename to doc/01_Functionality.md
diff --git a/doc/03_Relations.md b/doc/02_Relations.md
similarity index 100%
rename from doc/03_Relations.md
rename to doc/02_Relations.md
diff --git a/doc/04_Storage.md b/doc/03_Storage.md
similarity index 100%
rename from doc/04_Storage.md
rename to doc/03_Storage.md
diff --git a/doc/05_Modules.md b/doc/04_Modules.md
similarity index 87%
rename from doc/05_Modules.md
rename to doc/04_Modules.md
index 206ce69..bb1b342 100644
--- a/doc/05_Modules.md
+++ b/doc/04_Modules.md
@@ -45,6 +45,10 @@ Computes a plan to backup a file.
 
 Provides a cache of assemblies and recreates them on demand.
 
+### Store
+[Store](../theories/Store.v)
+
+Meta information about file blocks and encryption keys need to be stored in an accessible way. This module provides basic implementations using lists.
 
 ## Other modules
 
diff --git a/doc/05_AssemblyCache.md b/doc/05_AssemblyCache.md
new file mode 100644
index 0000000..3c2c733
--- /dev/null
+++ b/doc/05_AssemblyCache.md
@@ -0,0 +1,13 @@
+[Content](01_Content.md)
+
+# Data caching
+
+The module [AssemblyCache](../theories/AssemblyCache.v) maintains a fixed size cache of assemblies.
+
+* one assembly is writeable. As soon as it is full it will get encrypted and extracted to chunks.
+
+* a fixed number of assemblies are decrypted. Only the one in the first place is readable. If another one is requested and not yet decrypted, then it will be reconstructed from chunks, decrypted and put in front of the others. The last one is dropped.
+
+![Caching of data with AssemblyCache](./img/img4.png)
+
+* client processes interact with the cache to add data to it or retrieve data.
diff --git a/doc/img/img4.png b/doc/img/img4.png
new file mode 100644
index 0000000..0336bac
Binary files /dev/null and b/doc/img/img4.png differ
diff --git a/elykseer-utils/actrl.ml b/elykseer-utils/actrl.ml
index ffb6820..0e486eb 100644
--- a/elykseer-utils/actrl.ml
+++ b/elykseer-utils/actrl.ml
@@ -14,7 +14,7 @@ let stop actrl =
   let env = Environment.EnvironmentWritable.finalise_assembly actrl.env in
   let%lwt relk = Relkeys.new_map env.config in
   let%lwt () = Lwt_list.iter_s (fun (aid, ki) ->
-                                let%lwt _ = Relkeys.add aid ki relk in Lwt.return ()) env.keys in
+                                let%lwt _ = Relkeys.add aid ki relk in Lwt.return ()) env.keys.entries in
   let%lwt () = Relkeys.close_map relk in
   Lwt_io.printlf "stopping assembly controller %s" actrl.myid
 
@@ -23,5 +23,5 @@ let addblock actrl fn (fb : Assembly.blockinformation) buf =
                (Cstdio.File.Buffer.size buf) in *)
   let bplain = Buffer.BufferPlain.from_buffer buf in
   let env' = Environment.EnvironmentWritable.backup actrl.env fn fb.filepos bplain in
-  let (_fname, fb') = List.hd @@ Environment.fblocks env' in
+  let (_fname, fb') = List.hd @@ env'.fblocks.entries in
   Lwt.return ({actrl with env = env'}, {fb' with blockid = fb.blockid})
diff --git a/lxr.ml b/lxr.ml
index a16d15f..67db94a 100644
--- a/lxr.ml
+++ b/lxr.ml
@@ -789,6 +789,10 @@ module Utilities =
      String.cat (Unix.gethostname ()) |> String.cat (Unix.gettimeofday () |> string_of_float) |>
      Elykseer_crypto.Sha256.string
    
+
+  (** val sha256 : string -> string **)
+
+  let sha256 = Elykseer_crypto.Sha256.string
  end
 
 module Assembly =
@@ -1207,14 +1211,103 @@ module Assembly =
       (Utilities.make_list a.nchunks) N0
  end
 
+module Store =
+ struct
+  type 'kVs store = { config : Configuration.configuration; entries : 'kVs }
+
+  (** val config : 'a1 store -> Configuration.configuration **)
+
+  let config s =
+    s.config
+
+  (** val entries : 'a1 store -> 'a1 **)
+
+  let entries s =
+    s.entries
+
+  (** val rec_find : string -> (string * 'a1) list -> 'a1 option **)
+
+  let rec rec_find k = function
+  | [] -> None
+  | p :: r -> let (k', v') = p in if (=) k' k then Some v' else rec_find k r
+
+  module type STORE =
+   sig
+    type coq_K
+
+    type coq_V
+
+    type coq_KVs
+
+    type coq_R
+
+    val init : Configuration.configuration -> coq_R
+
+    val add : coq_K -> coq_V -> coq_R -> coq_R
+
+    val find : coq_K -> coq_R -> coq_V option
+   end
+
+  module KeyListStore =
+   struct
+    type coq_K = string
+
+    type coq_V = Assembly.keyinformation
+
+    type coq_KVs = (coq_K * coq_V) list
+
+    type coq_R = coq_KVs store
+
+    (** val init : Configuration.configuration -> coq_R **)
+
+    let init c =
+      { config = c; entries = [] }
+
+    (** val add : coq_K -> coq_V -> coq_R -> coq_R **)
+
+    let add k v r =
+      { config = r.config; entries = ((k, v) :: r.entries) }
+
+    (** val find : coq_K -> coq_R -> coq_V option **)
+
+    let find k r =
+      rec_find k r.entries
+   end
+
+  module FBlockListStore =
+   struct
+    type coq_K = Assembly.aid_t
+
+    type coq_V = Assembly.blockinformation
+
+    type coq_KVs = (coq_K * coq_V) list
+
+    type coq_R = coq_KVs store
+
+    (** val init : Configuration.configuration -> coq_R **)
+
+    let init c =
+      { config = c; entries = [] }
+
+    (** val add : coq_K -> coq_V -> coq_R -> coq_R **)
+
+    let add k v r =
+      { config = r.config; entries = ((k, v) :: r.entries) }
+
+    (** val find : coq_K -> coq_R -> coq_V option **)
+
+    let find k r =
+      rec_find k r.entries
+   end
+ end
+
 module Environment =
  struct
   type 'aB environment = { cur_assembly : Assembly.assemblyinformation;
                            cur_buffer : 'aB;
                            config : Configuration.configuration;
-                           fblocks : (string * Assembly.blockinformation) list;
-                           keys : (Assembly.aid_t * Assembly.keyinformation)
-                                  list }
+                           fblocks : Store.FBlockListStore.coq_R;
+                           keys : Store.KeyListStore.coq_R }
 
   (** val cur_assembly : 'a1 environment -> Assembly.assemblyinformation **)
 
@@ -1231,14 +1324,12 @@ module Environment =
   let config e =
     e.config
 
-  (** val fblocks :
-      'a1 environment -> (string * Assembly.blockinformation) list **)
+  (** val fblocks : 'a1 environment -> Store.FBlockListStore.coq_R **)
 
   let fblocks e =
     e.fblocks
 
-  (** val keys :
-      'a1 environment -> (Assembly.aid_t * Assembly.keyinformation) list **)
+  (** val keys : 'a1 environment -> Store.KeyListStore.coq_R **)
 
   let keys e =
     e.keys
@@ -1270,8 +1361,8 @@ module Environment =
 
     let initial_environment c =
       let (a, b) = Assembly.AssemblyPlainWritable.create c in
-      { cur_assembly = a; cur_buffer = b; config = c; fblocks = []; keys =
-      [] }
+      { cur_assembly = a; cur_buffer = b; config = c; fblocks =
+      (Store.FBlockListStore.init c); keys = (Store.KeyListStore.init c) }
 
     (** val recreate_assembly : coq_AB environment -> coq_AB environment **)
 
@@ -1286,7 +1377,8 @@ module Environment =
 
     let env_add_file_block fname0 e bi =
       { cur_assembly = e.cur_assembly; cur_buffer = e.cur_buffer; config =
-        e.config; fblocks = ((fname0, bi) :: e.fblocks); keys = e.keys }
+        e.config; fblocks = (Store.FBlockListStore.add fname0 bi e.fblocks);
+        keys = e.keys }
 
     (** val env_add_aid_key :
         Assembly.aid_t -> coq_AB environment -> Assembly.keyinformation ->
@@ -1294,15 +1386,14 @@ module Environment =
 
     let env_add_aid_key aid0 e ki =
       { cur_assembly = e.cur_assembly; cur_buffer = e.cur_buffer; config =
-        e.config; fblocks = e.fblocks; keys = ((aid0, ki) :: e.keys) }
+        e.config; fblocks = e.fblocks; keys =
+        (Store.KeyListStore.add aid0 ki e.keys) }
 
     (** val key_for_aid :
         coq_AB environment -> Assembly.aid_t -> Assembly.keyinformation option **)
 
     let key_for_aid e aid0 =
-      match filter (fun e0 -> (=) (fst e0) aid0) e.keys with
-      | [] -> None
-      | p :: _ -> let (_, ki) = p in Some ki
+      Store.KeyListStore.find aid0 e.keys
 
     (** val finalise_assembly : coq_AB environment -> coq_AB environment **)
 
@@ -1352,7 +1443,7 @@ module Environment =
         Assembly.backup e1.cur_assembly e1.cur_buffer fpos content
       in
       { cur_assembly = a'; cur_buffer = e1.cur_buffer; config = e1.config;
-      fblocks = ((fp, bi) :: e1.fblocks); keys = e1.keys }
+      fblocks = (Store.FBlockListStore.add fp bi e1.fblocks); keys = e1.keys }
    end
 
   module EnvironmentReadable =
@@ -1365,8 +1456,8 @@ module Environment =
 
     let initial_environment c =
       let (a, b) = Assembly.AssemblyPlainFull.create c in
-      { cur_assembly = a; cur_buffer = b; config = c; fblocks = []; keys =
-      [] }
+      { cur_assembly = a; cur_buffer = b; config = c; fblocks =
+      (Store.FBlockListStore.init c); keys = (Store.KeyListStore.init c) }
 
     (** val env_add_aid_key :
         Assembly.aid_t -> coq_AB environment -> Assembly.keyinformation ->
@@ -1374,15 +1465,14 @@ module Environment =
 
     let env_add_aid_key aid0 e ki =
       { cur_assembly = e.cur_assembly; cur_buffer = e.cur_buffer; config =
-        e.config; fblocks = e.fblocks; keys = ((aid0, ki) :: e.keys) }
+        e.config; fblocks = e.fblocks; keys =
+        (Store.KeyListStore.add aid0 ki e.keys) }
 
     (** val key_for_aid :
         coq_AB environment -> Assembly.aid_t -> Assembly.keyinformation option **)
 
     let key_for_aid e aid0 =
-      match filter (fun e0 -> (=) (fst e0) aid0) e.keys with
-      | [] -> None
-      | p :: _ -> let (_, ki) = p in Some ki
+      Store.KeyListStore.find aid0 e.keys
 
     (** val restore_assembly :
         coq_AB environment -> Assembly.aid_t -> coq_AB environment option **)
@@ -1894,7 +1984,7 @@ module Version =
   (** val build : string **)
 
   let build =
-    "6"
+    "7"
 
   (** val version : string **)
 
diff --git a/lxr.mli b/lxr.mli
index a54e57a..6a7ebf0 100644
--- a/lxr.mli
+++ b/lxr.mli
@@ -267,6 +267,8 @@ module Utilities :
   val rnd : n -> n
 
   val rnd256 : string -> string
+
+  val sha256 : string -> string
  end
 
 module Assembly :
@@ -409,14 +411,75 @@ module Assembly :
     AssemblyEncrypted.coq_B -> n
  end
 
+module Store :
+ sig
+  type 'kVs store = { config : Configuration.configuration; entries : 'kVs }
+
+  val config : 'a1 store -> Configuration.configuration
+
+  val entries : 'a1 store -> 'a1
+
+  val rec_find : string -> (string * 'a1) list -> 'a1 option
+
+  module type STORE =
+   sig
+    type coq_K
+
+    type coq_V
+
+    type coq_KVs
+
+    type coq_R
+
+    val init : Configuration.configuration -> coq_R
+
+    val add : coq_K -> coq_V -> coq_R -> coq_R
+
+    val find : coq_K -> coq_R -> coq_V option
+   end
+
+  module KeyListStore :
+   sig
+    type coq_K = string
+
+    type coq_V = Assembly.keyinformation
+
+    type coq_KVs = (coq_K * coq_V) list
+
+    type coq_R = coq_KVs store
+
+    val init : Configuration.configuration -> coq_R
+
+    val add : coq_K -> coq_V -> coq_R -> coq_R
+
+    val find : coq_K -> coq_R -> coq_V option
+   end
+
+  module FBlockListStore :
+   sig
+    type coq_K = Assembly.aid_t
+
+    type coq_V = Assembly.blockinformation
+
+    type coq_KVs = (coq_K * coq_V) list
+
+    type coq_R = coq_KVs store
+
+    val init : Configuration.configuration -> coq_R
+
+    val add : coq_K -> coq_V -> coq_R -> coq_R
+
+    val find : coq_K -> coq_R -> coq_V option
+   end
+ end
+
 module Environment :
  sig
   type 'aB environment = { cur_assembly : Assembly.assemblyinformation;
                            cur_buffer : 'aB;
                            config : Configuration.configuration;
-                           fblocks : (string * Assembly.blockinformation) list;
-                           keys : (Assembly.aid_t * Assembly.keyinformation)
-                                  list }
+                           fblocks : Store.FBlockListStore.coq_R;
+                           keys : Store.KeyListStore.coq_R }
 
   val cur_assembly : 'a1 environment -> Assembly.assemblyinformation
 
@@ -424,10 +487,9 @@ module Environment :
 
   val config : 'a1 environment -> Configuration.configuration
 
-  val fblocks : 'a1 environment -> (string * Assembly.blockinformation) list
+  val fblocks : 'a1 environment -> Store.FBlockListStore.coq_R
 
-  val keys :
-    'a1 environment -> (Assembly.aid_t * Assembly.keyinformation) list
+  val keys : 'a1 environment -> Store.KeyListStore.coq_R
 
   val cpp_mk_key256 : unit -> string
 
diff --git a/theories/Environment.v b/theories/Environment.v
index 2ddcb41..6c4333c 100644
--- a/theories/Environment.v
+++ b/theories/Environment.v
@@ -10,6 +10,7 @@ From RecordUpdate Require Import RecordUpdate.
 From LXR Require Import Assembly.
 From LXR Require Import Buffer.
 From LXR Require Import Configuration.
+From LXR Require Import Store.
 From LXR Require Import Nchunks.
 
 Module Export Environment.
@@ -23,8 +24,8 @@ Record environment (AB : Type) : RecordEnvironment :=
         { cur_assembly : assemblyinformation
         ; cur_buffer : AB
         ; config : configuration
-        ; fblocks : list (string * Assembly.blockinformation)
-        ; keys : list (aid_t * Assembly.keyinformation)
+        ; fblocks : FBlockListStore.R
+        ; keys : KeyListStore.R
         }.
 (* #[export] Instance etaX : Settable _ := settable! mkenvironment (AB) <cur_assembly; cur_buffer; config; fblocks; keys>. *)
 (* Print environment.
@@ -51,8 +52,8 @@ Module EnvironmentWritable <: ENV.
         {| cur_assembly := a
         ;  cur_buffer := b
         ;  config := c
-        ;  fblocks := nil
-        ;  keys := nil
+        ;  fblocks := FBlockListStore.init c
+        ;  keys := KeyListStore.init c
         |}.
     Definition recreate_assembly (e : environment AB) : environment AB :=
         let (a,b) := AssemblyPlainWritable.create (e.(config AB)) in
@@ -65,7 +66,7 @@ Module EnvironmentWritable <: ENV.
         {| cur_assembly := e.(cur_assembly AB)
         ;  cur_buffer := e.(cur_buffer AB)
         ;  config := e.(config AB)
-        ;  fblocks := (fname,bi) :: e.(fblocks AB)
+        ;  fblocks := FBlockListStore.add fname bi e.(fblocks AB)
         ;  keys := e.(keys AB)
         |}.
     Definition env_add_aid_key (aid : aid_t) (e : environment AB) (ki : keyinformation) : environment AB :=
@@ -73,13 +74,10 @@ Module EnvironmentWritable <: ENV.
         ;  cur_buffer := e.(cur_buffer AB)
         ;  config := e.(config AB)
         ;  fblocks := e.(fblocks AB)
-        ;  keys := (aid,ki) :: e.(keys AB)
+        ;  keys := KeyListStore.add aid ki e.(keys AB)
         |}.
     Definition key_for_aid (e : environment AB) (aid : Assembly.aid_t) : option keyinformation :=
-        match List.filter (fun e => String.eqb (fst e) aid) e.(keys AB) with
-        | nil => None
-        | (_,ki) :: _ => Some ki
-        end.
+        KeyListStore.find aid e.(keys AB).
     Definition finalise_assembly (e0 : environment AB) : environment AB :=
         let a0 := e0.(cur_assembly AB) in
         let apos := Assembly.apos a0 in
@@ -114,7 +112,7 @@ Module EnvironmentWritable <: ENV.
         {| cur_assembly := a'
         ;  cur_buffer := e1.(cur_buffer AB)
         ;  config := e1.(config AB)
-        ;  fblocks := (fp,bi) :: e1.(fblocks AB)
+        ;  fblocks := FBlockListStore.add fp bi e1.(fblocks AB)
         ;  keys := e1.(keys AB)
         |}.
 
@@ -129,21 +127,18 @@ Module EnvironmentReadable <: ENV.
         {| cur_assembly := a
         ;  cur_buffer := b
         ;  config := c
-        ;  fblocks := nil
-        ;  keys := nil
+        ;  fblocks := FBlockListStore.init c
+        ;  keys := KeyListStore.init c
         |}.
     Definition env_add_aid_key (aid : aid_t) (e : environment AB) (ki : keyinformation) : environment AB :=
         {| cur_assembly := e.(cur_assembly AB)
         ;  cur_buffer := e.(cur_buffer AB)
         ;  config := e.(config AB)
         ;  fblocks := e.(fblocks AB)
-        ;  keys := (aid,ki) :: e.(keys AB)
+        ;  keys := KeyListStore.add aid ki e.(keys AB)
         |}.
     Definition key_for_aid (e : environment AB) (aid : Assembly.aid_t) : option keyinformation :=
-        match List.filter (fun e => String.eqb (fst e) aid) e.(keys AB) with
-        | nil => None
-        | (_,ki) :: _ => Some ki
-        end.
+        KeyListStore.find aid e.(keys AB).
     Definition restore_assembly (e0 : environment AB) (aid : aid_t) : option (environment AB) :=
         match key_for_aid e0 aid with
         | None => None
diff --git a/theories/Filesupport.v b/theories/Filesupport.v
index 2415772..63bc674 100644
--- a/theories/Filesupport.v
+++ b/theories/Filesupport.v
@@ -7,10 +7,10 @@
  Description: provides abstract definitions of file functions.
  *)
 
- From Coq Require Import Strings.String.
- Require Import NArith.
+From Coq Require Import Strings.String.
+Require Import NArith.
  
- Module Export Filesupport.
+Module Export Filesupport.
 
 Definition filename := string.
 
diff --git a/theories/MakeML.v b/theories/MakeML.v
index 76df1c4..022da6e 100644
--- a/theories/MakeML.v
+++ b/theories/MakeML.v
@@ -7,6 +7,7 @@ Open Scope positive_scope.
 
 From LXR Require Import Assembly.
 From LXR Require Import AssemblyCache.
+From LXR Require Import Store.
 From LXR Require Import BackupPlanner.
 From LXR Require Import Buffer.
 From LXR Require Import Configuration.
@@ -195,6 +196,9 @@ Extract Constant get_file_information =>
           fchecksum = Elykseer_base.Fsutils.fchksum fn }
    ".
 
+Extract Constant sha256 => "Elykseer_crypto.Sha256.string".
+
+
 (* extract into "lxr.ml" all named modules and definitions, and their dependencies *)
 Extraction "lxr.ml"  Version Conversion Utilities Filesupport Nchunks Assembly
-                     Configuration Environment Buffer BackupPlanner AssemblyCache.
+                     Configuration Environment Buffer BackupPlanner AssemblyCache Store.
diff --git a/theories/Store.v b/theories/Store.v
new file mode 100644
index 0000000..8eb1807
--- /dev/null
+++ b/theories/Store.v
@@ -0,0 +1,129 @@
+(**
+      e L y K s e e R
+*)
+
+Require Import NArith PArith.
+From Coq Require Import NArith.BinNat Lists.List Strings.String Program.Basics.
+
+From RecordUpdate Require Import RecordUpdate.
+
+From LXR Require Import Assembly.
+From LXR Require Import Configuration.
+
+Open Scope list_scope.
+
+Import ListNotations.
+
+Module Export Store.
+
+Definition RecordStore := Type.
+Record store (KVs : Type): RecordStore :=
+    mkstore
+        { config : configuration
+        ; entries : KVs
+        }.
+Print RecordStore.
+Print store.
+
+Print option.
+
+Fixpoint rec_find {V : Type} (k : string) (es : list (string * V)) : option V :=
+    match es with
+    | [] => None
+    | (k', v')::r => if k' =? k then Some v'
+                     else rec_find k r
+    end.
+
+Module Type STORE.
+    Parameter K : Type.
+    Parameter V : Type.
+    Parameter KVs : Type.
+    Parameter R : Type.
+    Parameter init : configuration -> R.
+    Parameter add : K -> V -> R -> R.
+    Parameter find : K -> R -> option V.
+End STORE.
+Print STORE.
+
+Module KeyListStore <: STORE.
+    Definition K := String.string.
+    Definition V := Assembly.keyinformation.
+    Definition KVs := list (K * V).
+    Definition R : RecordStore := store KVs.
+    Definition init (c : configuration) : R := {| config := c; entries := [] |}.
+    Definition add (k : K) (v : V) (r : R) : R :=
+        {| config := r.(config KVs); entries := (k, v) :: r.(entries KVs) |}.
+    Definition find (k : K) (r : R) : option V :=
+        rec_find k r.(entries KVs).
+End KeyListStore.
+Print KeyListStore.
+
+Module FBlockListStore <: STORE.
+    Definition K := Assembly.aid_t.
+    Definition V := Assembly.blockinformation.
+    Definition KVs := list (K * V).
+    Definition R : RecordStore := store KVs.
+    Definition init (c : configuration) : R := {| config := c; entries := [] |}.
+    Definition add (k : K) (v : V) (r : R) : R :=
+        {| config := r.(config KVs); entries := (k, v) :: r.(entries KVs) |}.
+    Definition find (k : K) (r : R) : option V :=
+        rec_find k r.(entries KVs).
+
+End FBlockListStore.
+Print FBlockListStore.
+
+
+Example find_entry_in_empty : forall c,
+    let es := FBlockListStore.init c in
+    let k : Assembly.aid_t := "t1" in
+    FBlockListStore.find k es = None. 
+
+Proof.
+    intros.
+    unfold FBlockListStore.find.
+    unfold rec_find. simpl. reflexivity.
+Qed.
+
+Example add_then_find_entry : forall c,
+    let es := FBlockListStore.init c in
+    let v := {| blockid := 1; bchecksum := "chksum"; blocksize := 1024; filepos := 0; blockaid := "aid001"; blockapos := 42 |} in
+    let k : Assembly.aid_t := "t1" in
+    FBlockListStore.find k (FBlockListStore.add k v es) = Some v. 
+
+Proof.
+    intros.
+    unfold FBlockListStore.add.
+    unfold FBlockListStore.find.
+    unfold rec_find. simpl. reflexivity.
+Qed.
+
+Example add_add_then_find_entry : forall c,
+    let es := FBlockListStore.init c in
+    let v1 := {| blockid := 1; bchecksum := "chksum"; blocksize := 1024; filepos := 0; blockaid := "aid001"; blockapos := 42 |} in
+    let v2 := {| blockid := 2; bchecksum := "chksum"; blocksize := 1024; filepos := 42; blockaid := "aid001"; blockapos := 1066 |} in
+    let k1 : Assembly.aid_t := "t1" in
+    let k2 : Assembly.aid_t := "t2" in
+    FBlockListStore.find k1 (FBlockListStore.add k2 v2 (FBlockListStore.add k1 v1 es)) = Some v1.
+
+Proof.
+    intros.
+    unfold FBlockListStore.add. simpl.
+    unfold FBlockListStore.find.
+    unfold rec_find. simpl. reflexivity.
+Qed.
+
+Example add_then_find_another_entry : forall c,
+    let es := FBlockListStore.init c in
+    let v := {| blockid := 1; bchecksum := "chksum"; blocksize := 1024; filepos := 0; blockaid := "aid001"; blockapos := 42 |} in
+    let k1 : Assembly.aid_t := "t1" in
+    let k2 : Assembly.aid_t := "t2" in
+    FBlockListStore.find k2 (FBlockListStore.add k1 v es) = None. 
+
+Proof.
+    intros.
+    unfold FBlockListStore.add.
+    unfold FBlockListStore.find.
+    unfold rec_find. simpl. reflexivity.
+Qed.
+
+End Store.
\ No newline at end of file
diff --git a/theories/Utilities.v b/theories/Utilities.v
index 0391482..2db9c8d 100644
--- a/theories/Utilities.v
+++ b/theories/Utilities.v
@@ -32,6 +32,10 @@ Axiom rnd : N -> N.
 *)
 Axiom rnd256 : string -> string.
 
+(* returns hash of a string
+*)
+Axiom sha256 : string -> string.
+
 End axioms.
 
 End Utilities.
diff --git a/theories/Version.v b/theories/Version.v
index 3a9cfcc..9d230c0 100644
--- a/theories/Version.v
+++ b/theories/Version.v
@@ -10,7 +10,7 @@ Open Scope string_scope.
 
 Definition major : string := "0".
 Definition minor : string :=     "9".
-Definition build : string :=         "6".
+Definition build : string :=         "7".
 Definition version : string := major ++ "." ++ minor ++ "." ++ build.
 
 End Version.