Store of keys | fblocks (#9)

* +store for keys, fblocks

* + Store.v

Signed-off-by: Alexander Diemand <codieplusplus@apax.net>

_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

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"

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

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 

doc/05_Modules.md → 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
 

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.

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

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,23 +1377,23 @@ 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 ->
         coq_AB 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,24 +1456,23 @@ 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 ->
         coq_AB 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 **)