diff --git a/bin/lxr_assembly.ml b/bin/lxr_assembly.ml
index 351f138..06fc6d7 100644
--- a/bin/lxr_assembly.ml
+++ b/bin/lxr_assembly.ml
@@ -49,7 +49,7 @@ let main () = Arg.parse argspec anon_args_fun "lxr_assembly: vaf";
     let%lwt () = Lwt_io.printlf "rnd256 %d" (Conversion.n2i @@ Utilities.rnd @@ Conversion.i2n 0) in
     let%lwt () = Lwt_io.printlf "sha256 of /bin/sh %s" (Fsutils.fchksum "/bin/sh") in
     let c : Configuration.configuration = { config_nchunks = (Nchunks.from_int 16); path_chunks = "./chunks"; path_db = "/tmp/db"; my_id = "16"} in
-    let e0 = Environment.initial_environment c in
+    let e0 = Environment.EnvironmentWritable.initial_environment c in
     let a = Environment.cur_assembly e0 in
     let b = Environment.cur_buffer e0 in
     let%lwt () = Lwt_io.printlf "assembly %s %d %d" a.aid (Conversion.p2i a.nchunks) (Conversion.n2i a.apos) in
@@ -59,8 +59,8 @@ let main () = Arg.parse argspec anon_args_fun "lxr_assembly: vaf";
     (* let msg = "testing some longer message." in *)
     let content = BufferPlain.buffer_create (Conversion.i2n 1024) in (*  (fun i -> if i < 28 then String.get msg i else '0') in *)
     let (a', bi) = Elykseer__Lxr.Assembly.backup a b (* "test1M" *) (Conversion.i2n 0) content in
-    let e1 = Environment.env_add_file_block "test1M" e0 bi in
-    let e2 = Environment.env_add_aid_key (aid a') e1 {pkey="abc97391af";ivec="323453";localnchunks=Nchunks.to_positive c.config_nchunks;localid=c.my_id} in
+    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 (a'', b') = Elykseer__Lxr.Assembly.finish a' b in
diff --git a/bin/lxr_backup.ml b/bin/lxr_backup.ml
index f1cbf7a..edadabd 100644
--- a/bin/lxr_backup.ml
+++ b/bin/lxr_backup.ml
@@ -76,7 +76,7 @@ let execute_backup_fileblock e _anum (fname,blocks) =
               Cstdio.File.fread buf sz fptr |> function
                 | Ok _nread ->
                   let bplain = Buffer.BufferPlain.from_buffer buf in
-                  Environment.backup e0 fname fpos bplain
+                  EnvironmentWritable.backup e0 fname fpos bplain
                 | Error (errno,errstr) -> 
                   Printf.printf "read error no:%d err:%s\n" errno errstr; e0
               end
@@ -101,7 +101,7 @@ let rec run_backup_for_assembly e0 pid anum acount (bp : backup_plan) =
       let anum_p = Conversion.i2p anum in
       let fileblocks' = extract_fileblocks anum_p bp in
       let e1 = List.fold_left (fun env fb -> execute_backup_fileblock env anum fb) e0 fileblocks' in
-      let e2 = Environment.finalise_and_recreate_assembly e1 in
+      let e2 = Environment.EnvironmentWritable.finalise_and_recreate_assembly e1 in
       run_backup_for_assembly e2 pid (anum + 1) acount bp
   end
 
@@ -178,7 +178,7 @@ let main () = Arg.parse argspec anon_args_fun "lxr_backup: vyxdnji";
                   path_chunks = !arg_chunkpath;
                   path_db     = !arg_dbpath;
                   my_id       = myid } in
-    let e0 = Environment.initial_environment conf in
+    let e0 = Environment.EnvironmentWritable.initial_environment conf in
     let%lwt backup_plan = plan_backup e0 !arg_files in
     let fcount = List.map (fun bpf -> bpf.fhash) backup_plan.bp |> List.sort_uniq (compare) |> List.length
     and acount = List.map (fun bpf -> bpf.curbs) backup_plan.bp |> List.map (List.map BackupPlanner.fbanum) |>
@@ -189,7 +189,7 @@ let main () = Arg.parse argspec anon_args_fun "lxr_backup: vyxdnji";
                               List.flatten |> List.sort_uniq (compare) |> List.length in
                  Lwt_io.printlf "reference contains %d %s" rcount (Utils.pluralise2 "assembly" "assemblies" rcount) in
     let e1 = run_distributed_backup e0 !arg_nproc acount backup_plan in
-    let e2 = Environment.finalise_assembly e1 in
+    let e2 = Environment.EnvironmentWritable.finalise_assembly e1 in
     let%lwt () = output_relations e2 backup_plan in
     let%lwt () = Lwt_io.printl "done." in
     Lwt.return ()
diff --git a/bin/lxr_restore.ml b/bin/lxr_restore.ml
index 8b83b72..362cb57 100644
--- a/bin/lxr_restore.ml
+++ b/bin/lxr_restore.ml
@@ -43,8 +43,8 @@ let ensure_assembly e relk aid =
   match%lwt Relkeys.find aid relk with
   | None -> Lwt.return @@ Error "no key found"
   | Some ki ->
-    let e1 = Environment.env_add_aid_key aid e ki in
-    match Environment.restore_assembly e1 aid with
+    let e1 = Environment.EnvironmentReadable.env_add_aid_key aid e ki in
+    match Environment.EnvironmentReadable.restore_assembly e1 aid with
     | None -> Lwt.return @@ Error "failed to restore assembly"
     | Some e2 -> Lwt.return @@ Ok (e2.cur_assembly, e2.cur_buffer)
 
@@ -53,10 +53,9 @@ let restore_file_blocks e0 relk fptr (fb : Assembly.blockinformation) =
   | Error errstr -> let%lwt () = Lwt_io.printlf "  failed to recall assembly %s with '%s'" fb.blockaid errstr in
                     Lwt.return (0,e0)
   | Ok (a,b) ->
-      let (_a'', b'') = Assembly.finish a b in
       let sz = Conversion.n2i fb.blocksize in
       let fbuf = Cstdio.File.Buffer.create sz in
-      let abuf = Buffer.BufferPlain.to_buffer @@ Assembly.id_buffer_t_from_full b'' in
+      let abuf = Buffer.BufferPlain.to_buffer @@ Assembly.id_buffer_t_from_full b in
       let nread = Elykseer_base.Assembly.get_content ~src:abuf ~sz:sz ~pos:(Conversion.n2i fb.blockapos) ~tgt:fbuf in
       Cstdio.File.fseek fptr (Conversion.n2i fb.filepos) |> function
         | Error _ -> let%lwt () = Lwt_io.printlf "  failed to 'fseek'\n" in Lwt.return (0,e0)
@@ -94,7 +93,7 @@ let restore_file e0 relf relk fname =
               in
             Lwt.return (cnt,e1)
 
-let ensure_all_available (e : Environment.environment) fns =
+let ensure_all_available (e : Environment.EnvironmentReadable.coq_E) fns =
   let%lwt rel = Relfiles.new_map e.config in
   let%lwt ls = Lwt_list.map_s (fun fname -> let fhash = sha256 fname in
                   match%lwt Relfiles.find fhash rel with None -> Lwt.return 0 | Some _ -> Lwt.return 1) fns in
@@ -133,7 +132,7 @@ let main () = Arg.parse argspec anon_args_fun "lxr_restore: vxodnji";
                     path_chunks = !arg_chunkpath;
                     path_db     = !arg_dbpath;
                     my_id       = myid } in
-      let e0 = Environment.initial_environment conf in
+      let e0 = Environment.EnvironmentReadable.initial_environment conf in
       let%lwt relf = Relfiles.new_map conf in
       let%lwt relk = Relkeys.new_map conf in
       restore_files e0 relf relk !arg_files
diff --git a/elykseer-utils/actrl.ml b/elykseer-utils/actrl.ml
index 4b2975a..ffb6820 100644
--- a/elykseer-utils/actrl.ml
+++ b/elykseer-utils/actrl.ml
@@ -2,16 +2,16 @@ open Elykseer__Lxr
 
 type t = {
   myid : string;
-  env : Environment.environment
+  env : Environment.EnvironmentWritable.coq_E
 }
 
 let create (config : Configuration.configuration) = Lwt.return {
   myid = config.my_id;
-  env = Environment.initial_environment config
+  env = Environment.EnvironmentWritable.initial_environment config
 }
 
 let stop actrl =
-  let env = Environment.finalise_assembly actrl.env in
+  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
@@ -22,6 +22,6 @@ let addblock actrl fn (fb : Assembly.blockinformation) buf =
   (* let%lwt () = Lwt_io.printlf "adding block (%d@%d=%d) with buffer (%d)" (Conversion.p2i fb.blockid) (Conversion.n2i fb.filepos) (Conversion.n2i fb.blocksize)
                (Cstdio.File.Buffer.size buf) in *)
   let bplain = Buffer.BufferPlain.from_buffer buf in
-  let env' = Environment.backup actrl.env fn fb.filepos bplain in
+  let env' = Environment.EnvironmentWritable.backup actrl.env fn fb.filepos bplain in
   let (_fname, fb') = List.hd @@ Environment.fblocks env' in
   Lwt.return ({actrl with env = env'}, {fb' with blockid = fb.blockid})
diff --git a/lxr.ml b/lxr.ml
index dc579bd..a16d15f 100644
--- a/lxr.ml
+++ b/lxr.ml
@@ -866,13 +866,45 @@ module Assembly =
   let localnchunks k =
     k.localnchunks
 
+  type blockinformation = { blockid : positive; bchecksum : string;
+                            blocksize : n; filepos : n; blockaid : aid_t;
+                            blockapos : n }
+
+  (** val blockid : blockinformation -> positive **)
+
+  let blockid b =
+    b.blockid
+
+  (** val bchecksum : blockinformation -> string **)
+
+  let bchecksum b =
+    b.bchecksum
+
+  (** val blocksize : blockinformation -> n **)
+
+  let blocksize b =
+    b.blocksize
+
+  (** val filepos : blockinformation -> n **)
+
+  let filepos b =
+    b.filepos
+
+  (** val blockaid : blockinformation -> aid_t **)
+
+  let blockaid b =
+    b.blockaid
+
+  (** val blockapos : blockinformation -> n **)
+
+  let blockapos b =
+    b.blockapos
+
   module type ASS =
    sig
-    type coq_H = assemblyinformation
-
     type coq_B
 
-    val create : Configuration.configuration -> coq_H * coq_B
+    val create : Configuration.configuration -> assemblyinformation * coq_B
 
     val buffer_len : coq_B -> n
 
@@ -881,8 +913,6 @@ module Assembly =
 
   module AssemblyPlainWritable =
    struct
-    type coq_H = assemblyinformation
-
     type coq_B = Buffer.BufferPlain.buffer_t
 
     (** val buffer_len : coq_B -> n **)
@@ -895,7 +925,8 @@ module Assembly =
     let calc_checksum _ =
       "<>"
 
-    (** val create : Configuration.configuration -> coq_H * coq_B **)
+    (** val create :
+        Configuration.configuration -> assemblyinformation * coq_B **)
 
     let create c =
       let chunks = c.Configuration.config_nchunks in
@@ -914,8 +945,6 @@ module Assembly =
 
   module AssemblyEncrypted =
    struct
-    type coq_H = assemblyinformation
-
     type coq_B = Buffer.BufferEncrypted.buffer_t
 
     (** val buffer_len : coq_B -> n **)
@@ -928,7 +957,8 @@ module Assembly =
     let calc_checksum =
       Buffer.BufferEncrypted.calc_checksum
 
-    (** val create : Configuration.configuration -> coq_H * coq_B **)
+    (** val create :
+        Configuration.configuration -> assemblyinformation * coq_B **)
 
     let create c =
       let chunks = c.Configuration.config_nchunks in
@@ -942,8 +972,6 @@ module Assembly =
 
   module AssemblyPlainFull =
    struct
-    type coq_H = assemblyinformation
-
     type coq_B = Buffer.BufferPlain.buffer_t
 
     (** val buffer_len : coq_B -> n **)
@@ -957,8 +985,7 @@ module Assembly =
       Buffer.BufferPlain.calc_checksum
 
     (** val create :
-        Configuration.configuration ->
-        assemblyinformation * Buffer.BufferPlain.buffer_t **)
+        Configuration.configuration -> assemblyinformation * coq_B **)
 
     let create c =
       let chunks = c.Configuration.config_nchunks in
@@ -968,19 +995,115 @@ module Assembly =
       apos = sz }, b)
    end
 
+  (** val id_assembly_full_ainfo_from_writable :
+      assemblyinformation -> assemblyinformation **)
+
+  let id_assembly_full_ainfo_from_writable = fun b -> Helper.cpp_buffer_id b
+
+  (** val id_assembly_full_buffer_from_writable :
+      AssemblyPlainWritable.coq_B -> AssemblyPlainFull.coq_B **)
+
+  let id_assembly_full_buffer_from_writable = fun b -> Helper.cpp_buffer_id b
+
+  (** val finish :
+      assemblyinformation -> AssemblyPlainWritable.coq_B ->
+      assemblyinformation * AssemblyPlainFull.coq_B **)
+
+  let finish a b =
+    ((id_assembly_full_ainfo_from_writable a),
+      (id_assembly_full_buffer_from_writable b))
+
+  (** val assembly_add_content :
+      Buffer.BufferPlain.buffer_t -> n -> n -> AssemblyPlainWritable.coq_B ->
+      n **)
+
+  let assembly_add_content = 
+    fun src sz_N pos_N tgt ->
+      let sz = Conversion.n2i sz_N
+      and pos = Conversion.n2i pos_N in
+      Elykseer_base.Assembly.add_content ~src:src ~sz:sz ~pos:pos ~tgt:tgt |> Conversion.i2n
+   
+
+  (** val backup :
+      assemblyinformation -> AssemblyPlainWritable.coq_B -> n ->
+      Buffer.BufferPlain.buffer_t -> assemblyinformation * blockinformation **)
+
+  let backup a b fpos content =
+    let apos_n = a.apos in
+    let bsz = Buffer.BufferPlain.buffer_len content in
+    let chksum = Buffer.BufferPlain.calc_checksum content in
+    let nwritten = assembly_add_content content bsz apos_n b in
+    let bi = { blockid = XH; bchecksum = chksum; blocksize = nwritten;
+      filepos = fpos; blockaid = a.aid; blockapos = apos_n }
+    in
+    let a' =
+      set (fun a0 -> a0.apos) (fun f ->
+        let n0 = fun r -> f r.apos in
+        (fun x -> { nchunks = x.nchunks; aid = x.aid; apos = (n0 x) }))
+        (fun ap -> N.add ap nwritten) a
+    in
+    (a', bi)
+
+  (** val id_buffer_t_from_full :
+      AssemblyPlainFull.coq_B -> Buffer.BufferPlain.buffer_t **)
+
+  let id_buffer_t_from_full = fun b -> Helper.cpp_buffer_id b
+
+  (** val id_assembly_enc_buffer_t_from_buf :
+      Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B **)
+
+  let id_assembly_enc_buffer_t_from_buf = fun b -> Helper.cpp_buffer_id b
+
+  (** val encrypt :
+      assemblyinformation -> AssemblyPlainFull.coq_B -> keyinformation ->
+      (assemblyinformation * AssemblyEncrypted.coq_B) option **)
+
+  let encrypt a b ki =
+    let a' =
+      set (fun a0 -> a0.apos) (fun f ->
+        let n0 = fun r -> f r.apos in
+        (fun x -> { nchunks = x.nchunks; aid = x.aid; apos = (n0 x) }))
+        (const (assemblysize a.nchunks)) a
+    in
+    let benc = Buffer.encrypt (id_buffer_t_from_full b) ki.ivec ki.pkey in
+    let b' = id_assembly_enc_buffer_t_from_buf benc in Some (a', b')
+
+  (** val assembly_get_content :
+      AssemblyPlainFull.coq_B -> n -> n -> Buffer.BufferPlain.buffer_t -> n **)
+
+  let assembly_get_content = 
+    fun src sz_N pos_N tgt ->
+      let sz = Conversion.n2i sz_N
+      and pos = Conversion.n2i pos_N in
+      Elykseer_base.Assembly.get_content ~src:src ~sz:sz ~pos:pos ~tgt:tgt |> Conversion.i2n
+   
+
+  (** val restore :
+      AssemblyPlainFull.coq_B -> blockinformation ->
+      Buffer.BufferPlain.buffer_t option **)
+
+  let restore b bi =
+    let bsz = bi.blocksize in
+    let b' = Buffer.BufferPlain.buffer_create bsz in
+    let nw = assembly_get_content b bsz bi.blockapos b' in
+    if N.eqb nw bsz
+    then let bcksum = Buffer.BufferPlain.calc_checksum b' in
+         if (=) bcksum bi.bchecksum then Some b' else None
+    else None
+
   (** val id_buffer_t_from_enc :
       AssemblyEncrypted.coq_B -> Buffer.BufferEncrypted.buffer_t **)
 
   let id_buffer_t_from_enc = fun b -> Helper.cpp_buffer_id b
 
   (** val id_assembly_plain_buffer_t_from_buf :
-      Buffer.BufferPlain.buffer_t -> AssemblyPlainWritable.coq_B **)
+      Buffer.BufferPlain.buffer_t -> AssemblyPlainFull.coq_B **)
 
   let id_assembly_plain_buffer_t_from_buf = fun b -> Helper.cpp_buffer_id b
 
   (** val decrypt :
-      AssemblyEncrypted.coq_H -> AssemblyEncrypted.coq_B -> keyinformation ->
-      (AssemblyPlainWritable.coq_H * AssemblyPlainWritable.coq_B) option **)
+      assemblyinformation -> AssemblyEncrypted.coq_B -> keyinformation ->
+      (assemblyinformation * AssemblyPlainFull.coq_B) option **)
 
   let decrypt a b ki =
     let a' =
@@ -1025,8 +1148,8 @@ module Assembly =
   let id_enc_from_buffer_t = fun b -> Helper.cpp_buffer_id b
 
   (** val recall :
-      Configuration.configuration -> AssemblyEncrypted.coq_H ->
-      (AssemblyEncrypted.coq_H * AssemblyEncrypted.coq_B) option **)
+      Configuration.configuration -> assemblyinformation ->
+      (assemblyinformation * AssemblyEncrypted.coq_B) option **)
 
   let recall c a =
     let cidlist = Utilities.make_list a.nchunks in
@@ -1070,7 +1193,7 @@ module Assembly =
    
 
   (** val extract :
-      Configuration.configuration -> AssemblyEncrypted.coq_H ->
+      Configuration.configuration -> assemblyinformation ->
       AssemblyEncrypted.coq_B -> n **)
 
   let extract c a b =
@@ -1082,241 +1205,44 @@ module Assembly =
       in
       N.add nwritten (ext_store_chunk_to_path cpath chunksize_N apos0 buf))
       (Utilities.make_list a.nchunks) N0
-
-  (** val id_buffer_t_from_full :
-      AssemblyPlainFull.coq_B -> Buffer.BufferPlain.buffer_t **)
-
-  let id_buffer_t_from_full = fun b -> Helper.cpp_buffer_id b
-
-  (** val id_assembly_enc_buffer_t_from_buf :
-      Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B **)
-
-  let id_assembly_enc_buffer_t_from_buf = fun b -> Helper.cpp_buffer_id b
-
-  (** val id_assembly_full_buffer_from_writable :
-      AssemblyPlainWritable.coq_B -> AssemblyPlainFull.coq_B **)
-
-  let id_assembly_full_buffer_from_writable = fun b -> Helper.cpp_buffer_id b
-
-  (** val finish :
-      AssemblyPlainWritable.coq_H -> AssemblyPlainWritable.coq_B ->
-      AssemblyPlainFull.coq_H * AssemblyPlainFull.coq_B **)
-
-  let finish a b =
-    (a, (id_assembly_full_buffer_from_writable b))
-
-  (** val encrypt :
-      AssemblyPlainFull.coq_H -> AssemblyPlainFull.coq_B -> keyinformation ->
-      (AssemblyEncrypted.coq_H * AssemblyEncrypted.coq_B) option **)
-
-  let encrypt a b ki =
-    let a' =
-      set (fun a0 -> a0.apos) (fun f ->
-        let n0 = fun r -> f r.apos in
-        (fun x -> { nchunks = x.nchunks; aid = x.aid; apos = (n0 x) }))
-        (const (assemblysize a.nchunks)) a
-    in
-    let benc = Buffer.encrypt (id_buffer_t_from_full b) ki.ivec ki.pkey in
-    let b' = id_assembly_enc_buffer_t_from_buf benc in Some (a', b')
-
-  type blockinformation = { blockid : positive; bchecksum : string;
-                            blocksize : n; filepos : n; blockaid : string;
-                            blockapos : n }
-
-  (** val blockid : blockinformation -> positive **)
-
-  let blockid b =
-    b.blockid
-
-  (** val bchecksum : blockinformation -> string **)
-
-  let bchecksum b =
-    b.bchecksum
-
-  (** val blocksize : blockinformation -> n **)
-
-  let blocksize b =
-    b.blocksize
-
-  (** val filepos : blockinformation -> n **)
-
-  let filepos b =
-    b.filepos
-
-  (** val blockaid : blockinformation -> string **)
-
-  let blockaid b =
-    b.blockaid
-
-  (** val blockapos : blockinformation -> n **)
-
-  let blockapos b =
-    b.blockapos
-
-  (** val assembly_add_content :
-      Buffer.BufferPlain.buffer_t -> n -> n -> AssemblyPlainWritable.coq_B ->
-      n **)
-
-  let assembly_add_content = 
-    fun src sz_N pos_N tgt ->
-      let sz = Conversion.n2i sz_N
-      and pos = Conversion.n2i pos_N in
-      Elykseer_base.Assembly.add_content ~src:src ~sz:sz ~pos:pos ~tgt:tgt |> Conversion.i2n
-   
-
-  (** val backup :
-      AssemblyPlainWritable.coq_H -> AssemblyPlainWritable.coq_B -> n ->
-      Buffer.BufferPlain.buffer_t ->
-      AssemblyPlainWritable.coq_H * blockinformation **)
-
-  let backup a b fpos content =
-    let apos_n = a.apos in
-    let bsz = Buffer.BufferPlain.buffer_len content in
-    let chksum = Buffer.BufferPlain.calc_checksum content in
-    let nwritten = assembly_add_content content bsz apos_n b in
-    let bi = { blockid = XH; bchecksum = chksum; blocksize = nwritten;
-      filepos = fpos; blockaid = a.aid; blockapos = apos_n }
-    in
-    let a' =
-      set (fun a0 -> a0.apos) (fun f ->
-        let n0 = fun r -> f r.apos in
-        (fun x -> { nchunks = x.nchunks; aid = x.aid; apos = (n0 x) }))
-        (fun ap -> N.add ap nwritten) a
-    in
-    (a', bi)
-
-  (** val assembly_get_content :
-      AssemblyPlainFull.coq_B -> n -> n -> Buffer.BufferPlain.buffer_t -> n **)
-
-  let assembly_get_content = 
-    fun src sz_N pos_N tgt ->
-      let sz = Conversion.n2i sz_N
-      and pos = Conversion.n2i pos_N in
-      Elykseer_base.Assembly.get_content ~src:src ~sz:sz ~pos:pos ~tgt:tgt |> Conversion.i2n
-   
-
-  (** val restore :
-      AssemblyPlainFull.coq_B -> blockinformation ->
-      Buffer.BufferPlain.buffer_t option **)
-
-  let restore b bi =
-    let bsz = bi.blocksize in
-    let b' = Buffer.BufferPlain.buffer_create bsz in
-    let nw = assembly_get_content b bsz bi.blockapos b' in
-    if N.eqb nw bsz
-    then let bcksum = Buffer.BufferPlain.calc_checksum b' in
-         if (=) bcksum bi.bchecksum then Some b' else None
-    else None
  end
 
 module Environment =
  struct
-  type environment = { cur_assembly : Assembly.AssemblyPlainWritable.coq_H;
-                       cur_buffer : Assembly.AssemblyPlainWritable.coq_B;
-                       config : Configuration.configuration;
-                       fblocks : (string * Assembly.blockinformation) list;
-                       keys : (string * Assembly.keyinformation) list }
+  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 }
 
-  (** val cur_assembly :
-      environment -> Assembly.AssemblyPlainWritable.coq_H **)
+  (** val cur_assembly : 'a1 environment -> Assembly.assemblyinformation **)
 
   let cur_assembly e =
     e.cur_assembly
 
-  (** val cur_buffer : environment -> Assembly.AssemblyPlainWritable.coq_B **)
+  (** val cur_buffer : 'a1 environment -> 'a1 **)
 
   let cur_buffer e =
     e.cur_buffer
 
-  (** val config : environment -> Configuration.configuration **)
+  (** val config : 'a1 environment -> Configuration.configuration **)
 
   let config e =
     e.config
 
   (** val fblocks :
-      environment -> (string * Assembly.blockinformation) list **)
+      'a1 environment -> (string * Assembly.blockinformation) list **)
 
   let fblocks e =
     e.fblocks
 
-  (** val keys : environment -> (string * Assembly.keyinformation) list **)
+  (** val keys :
+      'a1 environment -> (Assembly.aid_t * Assembly.keyinformation) list **)
 
   let keys e =
     e.keys
 
-  (** val etaX : environment settable **)
-
-  let etaX x =
-    { cur_assembly = x.cur_assembly; cur_buffer = x.cur_buffer; config =
-      x.config; fblocks = x.fblocks; keys = x.keys }
-
-  (** val initial_environment : Configuration.configuration -> environment **)
-
-  let initial_environment c =
-    let (a, b) = Assembly.AssemblyPlainWritable.create c in
-    { cur_assembly = a; cur_buffer = b; config = c; fblocks = []; keys = [] }
-
-  (** val recreate_assembly : environment -> environment **)
-
-  let recreate_assembly e =
-    let (a, b) = Assembly.AssemblyPlainWritable.create e.config in
-    set (fun e0 -> e0.cur_assembly) (fun f ->
-      let h = fun r -> f r.cur_assembly in
-      (fun x -> { cur_assembly = (h x); cur_buffer = x.cur_buffer; config =
-      x.config; fblocks = x.fblocks; keys = x.keys })) (const a)
-      (set (fun e0 -> e0.cur_buffer) (fun f ->
-        let b0 = fun r -> f r.cur_buffer in
-        (fun x -> { cur_assembly = x.cur_assembly; cur_buffer = (b0 x);
-        config = x.config; fblocks = x.fblocks; keys = x.keys })) (const b) e)
-
-  (** val env_add_file_block :
-      string -> environment -> Assembly.blockinformation -> environment **)
-
-  let env_add_file_block fname0 e bi =
-    set (fun e0 -> e0.fblocks) (fun f ->
-      let l = fun r -> f r.fblocks in
-      (fun x -> { cur_assembly = x.cur_assembly; cur_buffer = x.cur_buffer;
-      config = x.config; fblocks = (l x); keys = x.keys })) (fun bs ->
-      (fname0, bi) :: bs) e
-
-  (** val env_add_aid_key :
-      string -> environment -> Assembly.keyinformation -> environment **)
-
-  let env_add_aid_key aid0 e ki =
-    set (fun e0 -> e0.keys) (fun f ->
-      let l = fun r -> f r.keys in
-      (fun x -> { cur_assembly = x.cur_assembly; cur_buffer = x.cur_buffer;
-      config = x.config; fblocks = x.fblocks; keys = (l x) })) (fun ks ->
-      (aid0, ki) :: ks) e
-
-  (** val key_for_aid :
-      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
-
-  (** val restore_assembly :
-      environment -> Assembly.aid_t -> environment option **)
-
-  let restore_assembly e0 aid0 =
-    match key_for_aid e0 aid0 with
-    | Some k ->
-      (match Assembly.recall e0.config { Assembly.nchunks =
-               e0.config.Configuration.config_nchunks; Assembly.aid = aid0;
-               Assembly.apos = N0 } with
-       | Some p ->
-         let (a1, b1) = p in
-         (match Assembly.decrypt a1 b1 k with
-          | Some p0 ->
-            let (a2, b2) = p0 in
-            Some { cur_assembly = a2; cur_buffer = b2; config = e0.config;
-            fblocks = e0.fblocks; keys = e0.keys }
-          | None -> None)
-       | None -> None)
-    | None -> None
-
   (** val cpp_mk_key256 : unit -> string **)
 
   let cpp_mk_key256 = fun () -> Helper.mk_key256 ()
@@ -1325,52 +1251,159 @@ module Environment =
 
   let cpp_mk_key128 = fun () -> Helper.mk_key128 ()
 
-  (** val finalise_assembly : environment -> environment **)
-
-  let finalise_assembly e0 =
-    let a0 = e0.cur_assembly in
-    let apos0 = a0.Assembly.apos in
-    if N.ltb N0 apos0
-    then let (a, b) = Assembly.finish a0 e0.cur_buffer in
-         let ki = { Assembly.ivec = (cpp_mk_key128 ()); Assembly.pkey =
-           (cpp_mk_key256 ()); Assembly.localid =
-           e0.config.Configuration.my_id; Assembly.localnchunks =
-           e0.config.Configuration.config_nchunks }
-         in
-         let e1 = env_add_aid_key a.Assembly.aid e0 ki in
-         (match Assembly.encrypt a b ki with
-          | Some p ->
-            let (a', b') = p in
-            let n0 = Assembly.extract e1.config a' b' in
-            if N.eqb n0
-                 (Assembly.assemblysize
-                   e0.config.Configuration.config_nchunks)
-            then e1
-            else e0
-          | None -> e0)
-    else e0
-
-  (** val finalise_and_recreate_assembly : environment -> environment **)
-
-  let finalise_and_recreate_assembly e0 =
-    let e1 = finalise_assembly e0 in recreate_assembly e1
+  module type ENV =
+   sig
+    type coq_AB
 
-  (** val backup :
-      environment -> string -> n -> Buffer.BufferPlain.buffer_t -> environment **)
+    type coq_E = coq_AB environment
 
-  let backup e0 fp fpos content =
-    let afree =
-      N.sub (Assembly.assemblysize e0.config.Configuration.config_nchunks)
-        e0.cur_assembly.Assembly.apos
-    in
-    let blen = Buffer.BufferPlain.buffer_len content in
-    let e1 =
-      if N.ltb afree blen then finalise_and_recreate_assembly e0 else e0
-    in
-    let (a', bi) = 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 }
+    val initial_environment : Configuration.configuration -> coq_E
+   end
+
+  module EnvironmentWritable =
+   struct
+    type coq_AB = Assembly.AssemblyPlainWritable.coq_B
+
+    type coq_E = coq_AB environment
+
+    (** val initial_environment : Configuration.configuration -> coq_E **)
+
+    let initial_environment c =
+      let (a, b) = Assembly.AssemblyPlainWritable.create c in
+      { cur_assembly = a; cur_buffer = b; config = c; fblocks = []; keys =
+      [] }
+
+    (** val recreate_assembly : coq_AB environment -> coq_AB environment **)
+
+    let recreate_assembly e =
+      let (a, b) = Assembly.AssemblyPlainWritable.create e.config in
+      { cur_assembly = a; cur_buffer = b; config = e.config; fblocks =
+      e.fblocks; keys = e.keys }
+
+    (** val env_add_file_block :
+        string -> coq_AB environment -> Assembly.blockinformation -> coq_AB
+        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 }
+
+    (** 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) }
+
+    (** 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
+
+    (** val finalise_assembly : coq_AB environment -> coq_AB environment **)
+
+    let finalise_assembly e0 =
+      let a0 = e0.cur_assembly in
+      let apos0 = a0.Assembly.apos in
+      if N.ltb N0 apos0
+      then let (a, b) = Assembly.finish a0 e0.cur_buffer in
+           let ki = { Assembly.ivec = (cpp_mk_key128 ()); Assembly.pkey =
+             (cpp_mk_key256 ()); Assembly.localid =
+             e0.config.Configuration.my_id; Assembly.localnchunks =
+             e0.config.Configuration.config_nchunks }
+           in
+           let e1 = env_add_aid_key a.Assembly.aid e0 ki in
+           (match Assembly.encrypt a b ki with
+            | Some p ->
+              let (a', b') = p in
+              let n0 = Assembly.extract e1.config a' b' in
+              if N.eqb n0
+                   (Assembly.assemblysize
+                     e0.config.Configuration.config_nchunks)
+              then e1
+              else e0
+            | None -> e0)
+      else e0
+
+    (** val finalise_and_recreate_assembly :
+        coq_AB environment -> coq_AB environment **)
+
+    let finalise_and_recreate_assembly e0 =
+      let e1 = finalise_assembly e0 in recreate_assembly e1
+
+    (** val backup :
+        coq_AB environment -> string -> n -> Buffer.BufferPlain.buffer_t ->
+        coq_AB environment **)
+
+    let backup e0 fp fpos content =
+      let afree =
+        N.sub (Assembly.assemblysize e0.config.Configuration.config_nchunks)
+          e0.cur_assembly.Assembly.apos
+      in
+      let blen = Buffer.BufferPlain.buffer_len content in
+      let e1 =
+        if N.ltb afree blen then finalise_and_recreate_assembly e0 else e0
+      in
+      let (a', bi) =
+        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 }
+   end
+
+  module EnvironmentReadable =
+   struct
+    type coq_AB = Assembly.AssemblyPlainFull.coq_B
+
+    type coq_E = coq_AB environment
+
+    (** val initial_environment : Configuration.configuration -> coq_E **)
+
+    let initial_environment c =
+      let (a, b) = Assembly.AssemblyPlainFull.create c in
+      { cur_assembly = a; cur_buffer = b; config = c; fblocks = []; 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) }
+
+    (** 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
+
+    (** val restore_assembly :
+        coq_AB environment -> Assembly.aid_t -> coq_AB environment option **)
+
+    let restore_assembly e0 aid0 =
+      match key_for_aid e0 aid0 with
+      | Some k ->
+        (match Assembly.recall e0.config { Assembly.nchunks =
+                 e0.config.Configuration.config_nchunks; Assembly.aid = aid0;
+                 Assembly.apos = N0 } with
+         | Some p ->
+           let (a1, b1) = p in
+           (match Assembly.decrypt a1 b1 k with
+            | Some p0 ->
+              let (a2, b2) = p0 in
+              Some { cur_assembly = a2; cur_buffer = b2; config = e0.config;
+              fblocks = e0.fblocks; keys = e0.keys }
+            | None -> None)
+         | None -> None)
+      | None -> None
+   end
  end
 
 module AssemblyCache =
@@ -1465,12 +1498,14 @@ module AssemblyCache =
   let wqueuesz w =
     w.wqueuesz
 
-  type assemblycache = { acenvs : Environment.environment list; acsize : 
-                         nat; acwriteenv : Environment.environment;
+  type assemblycache = { acenvs : Environment.EnvironmentReadable.coq_E list;
+                         acsize : nat;
+                         acwriteenv : Environment.EnvironmentWritable.coq_E;
                          acconfig : Configuration.configuration;
                          acwriteq : writequeue; acreadq : readqueue }
 
-  (** val acenvs : assemblycache -> Environment.environment list **)
+  (** val acenvs :
+      assemblycache -> Environment.EnvironmentReadable.coq_E list **)
 
   let acenvs a =
     a.acenvs
@@ -1480,7 +1515,8 @@ module AssemblyCache =
   let acsize a =
     a.acsize
 
-  (** val acwriteenv : assemblycache -> Environment.environment **)
+  (** val acwriteenv :
+      assemblycache -> Environment.EnvironmentWritable.coq_E **)
 
   let acwriteenv a =
     a.acwriteenv
@@ -1505,9 +1541,9 @@ module AssemblyCache =
 
   let prepare_assemblycache c size =
     { acenvs = []; acsize = (Coq_Pos.to_nat size); acwriteenv =
-      (Environment.initial_environment c); acconfig = c; acwriteq =
-      { wqueue = []; wqueuesz = qsize }; acreadq = { rqueue = []; rqueuesz =
-      qsize } }
+      (Environment.EnvironmentWritable.initial_environment c); acconfig = c;
+      acwriteq = { wqueue = []; wqueuesz = qsize }; acreadq = { rqueue = [];
+      rqueuesz = qsize } }
 
   (** val enqueue_write_request :
       assemblycache -> writequeueentity -> bool * assemblycache **)
@@ -1535,14 +1571,15 @@ module AssemblyCache =
 
   (** val try_restore_assembly :
       Configuration.configuration -> Assembly.aid_t ->
-      Environment.environment option **)
+      Environment.EnvironmentReadable.coq_E option **)
 
   let try_restore_assembly config0 sel_aid =
-    Environment.restore_assembly (Environment.initial_environment config0)
-      sel_aid
+    Environment.EnvironmentReadable.restore_assembly
+      (Environment.EnvironmentReadable.initial_environment config0) sel_aid
 
   (** val set_envs :
-      assemblycache -> Environment.environment list -> assemblycache **)
+      assemblycache -> Environment.EnvironmentReadable.coq_E list ->
+      assemblycache **)
 
   let set_envs ac0 envs =
     { acenvs = envs; acsize = ac0.acsize; acwriteenv = ac0.acwriteenv;
@@ -1551,7 +1588,7 @@ module AssemblyCache =
 
   (** val ensure_assembly :
       assemblycache -> Assembly.aid_t ->
-      (Environment.environment * assemblycache) option **)
+      (Environment.EnvironmentReadable.coq_E * assemblycache) option **)
 
   let ensure_assembly ac0 sel_aid =
     let filtered_var = ac0.acenvs in
@@ -1630,7 +1667,9 @@ module AssemblyCache =
     match reqs with
     | [] -> (res, ac0)
     | h :: r ->
-      let env = Environment.backup ac0.acwriteenv h.qfhash h.qfpos h.qbuffer
+      let env =
+        Environment.EnvironmentWritable.backup ac0.acwriteenv h.qfhash
+          h.qfpos h.qbuffer
       in
       let ac1 = { acenvs = ac0.acenvs; acsize = ac0.acsize; acwriteenv = env;
         acconfig = ac0.acconfig; acwriteq = { wqueue = []; wqueuesz =
@@ -1675,14 +1714,18 @@ module AssemblyCache =
   (** val flush : assemblycache -> assemblycache **)
 
   let flush ac0 =
-    let env = Environment.finalise_and_recreate_assembly ac0.acwriteenv in
+    let env =
+      Environment.EnvironmentWritable.finalise_and_recreate_assembly
+        ac0.acwriteenv
+    in
     { acenvs = []; acsize = ac0.acsize; acwriteenv = env; acconfig =
     ac0.acconfig; acwriteq = ac0.acwriteq; acreadq = ac0.acreadq }
 
   (** val close : assemblycache -> assemblycache **)
 
   let close ac0 =
-    let env = Environment.finalise_assembly ac0.acwriteenv in
+    let env = Environment.EnvironmentWritable.finalise_assembly ac0.acwriteenv
+    in
     { acenvs = []; acsize = ac0.acsize; acwriteenv = env; acconfig =
     ac0.acconfig; acwriteq = ac0.acwriteq; acreadq = ac0.acreadq }
  end
@@ -1851,7 +1894,7 @@ module Version =
   (** val build : string **)
 
   let build =
-    "5"
+    "6"
 
   (** val version : string **)
 
diff --git a/lxr.mli b/lxr.mli
index 7600c87..a54e57a 100644
--- a/lxr.mli
+++ b/lxr.mli
@@ -305,13 +305,27 @@ module Assembly :
 
   val localnchunks : keyinformation -> positive
 
+  type blockinformation = { blockid : positive; bchecksum : string;
+                            blocksize : n; filepos : n; blockaid : aid_t;
+                            blockapos : n }
+
+  val blockid : blockinformation -> positive
+
+  val bchecksum : blockinformation -> string
+
+  val blocksize : blockinformation -> n
+
+  val filepos : blockinformation -> n
+
+  val blockaid : blockinformation -> aid_t
+
+  val blockapos : blockinformation -> n
+
   module type ASS =
    sig
-    type coq_H = assemblyinformation
-
     type coq_B
 
-    val create : Configuration.configuration -> coq_H * coq_B
+    val create : Configuration.configuration -> assemblyinformation * coq_B
 
     val buffer_len : coq_B -> n
 
@@ -327,15 +341,49 @@ module Assembly :
   module AssemblyPlainFull :
    ASS
 
+  val id_assembly_full_ainfo_from_writable :
+    assemblyinformation -> assemblyinformation
+
+  val id_assembly_full_buffer_from_writable :
+    AssemblyPlainWritable.coq_B -> AssemblyPlainFull.coq_B
+
+  val finish :
+    assemblyinformation -> AssemblyPlainWritable.coq_B ->
+    assemblyinformation * AssemblyPlainFull.coq_B
+
+  val assembly_add_content :
+    Buffer.BufferPlain.buffer_t -> n -> n -> AssemblyPlainWritable.coq_B -> n
+
+  val backup :
+    assemblyinformation -> AssemblyPlainWritable.coq_B -> n ->
+    Buffer.BufferPlain.buffer_t -> assemblyinformation * blockinformation
+
+  val id_buffer_t_from_full :
+    AssemblyPlainFull.coq_B -> Buffer.BufferPlain.buffer_t
+
+  val id_assembly_enc_buffer_t_from_buf :
+    Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B
+
+  val encrypt :
+    assemblyinformation -> AssemblyPlainFull.coq_B -> keyinformation ->
+    (assemblyinformation * AssemblyEncrypted.coq_B) option
+
+  val assembly_get_content :
+    AssemblyPlainFull.coq_B -> n -> n -> Buffer.BufferPlain.buffer_t -> n
+
+  val restore :
+    AssemblyPlainFull.coq_B -> blockinformation ->
+    Buffer.BufferPlain.buffer_t option
+
   val id_buffer_t_from_enc :
     AssemblyEncrypted.coq_B -> Buffer.BufferEncrypted.buffer_t
 
   val id_assembly_plain_buffer_t_from_buf :
-    Buffer.BufferPlain.buffer_t -> AssemblyPlainWritable.coq_B
+    Buffer.BufferPlain.buffer_t -> AssemblyPlainFull.coq_B
 
   val decrypt :
-    AssemblyEncrypted.coq_H -> AssemblyEncrypted.coq_B -> keyinformation ->
-    (AssemblyPlainWritable.coq_H * AssemblyPlainWritable.coq_B) option
+    assemblyinformation -> AssemblyEncrypted.coq_B -> keyinformation ->
+    (assemblyinformation * AssemblyPlainFull.coq_B) option
 
   val chunk_identifier :
     Configuration.configuration -> aid_t -> positive -> string
@@ -350,110 +398,99 @@ module Assembly :
     Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B
 
   val recall :
-    Configuration.configuration -> AssemblyEncrypted.coq_H ->
-    (AssemblyEncrypted.coq_H * AssemblyEncrypted.coq_B) option
+    Configuration.configuration -> assemblyinformation ->
+    (assemblyinformation * AssemblyEncrypted.coq_B) option
 
   val ext_store_chunk_to_path :
     string -> n -> n -> Buffer.BufferEncrypted.buffer_t -> n
 
   val extract :
-    Configuration.configuration -> AssemblyEncrypted.coq_H ->
+    Configuration.configuration -> assemblyinformation ->
     AssemblyEncrypted.coq_B -> n
+ end
 
-  val id_buffer_t_from_full :
-    AssemblyPlainFull.coq_B -> Buffer.BufferPlain.buffer_t
-
-  val id_assembly_enc_buffer_t_from_buf :
-    Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B
-
-  val id_assembly_full_buffer_from_writable :
-    AssemblyPlainWritable.coq_B -> AssemblyPlainFull.coq_B
-
-  val finish :
-    AssemblyPlainWritable.coq_H -> AssemblyPlainWritable.coq_B ->
-    AssemblyPlainFull.coq_H * AssemblyPlainFull.coq_B
-
-  val encrypt :
-    AssemblyPlainFull.coq_H -> AssemblyPlainFull.coq_B -> keyinformation ->
-    (AssemblyEncrypted.coq_H * AssemblyEncrypted.coq_B) option
-
-  type blockinformation = { blockid : positive; bchecksum : string;
-                            blocksize : n; filepos : n; blockaid : string;
-                            blockapos : n }
-
-  val blockid : blockinformation -> positive
-
-  val bchecksum : blockinformation -> string
+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 }
 
-  val blocksize : blockinformation -> n
+  val cur_assembly : 'a1 environment -> Assembly.assemblyinformation
 
-  val filepos : blockinformation -> n
+  val cur_buffer : 'a1 environment -> 'a1
 
-  val blockaid : blockinformation -> string
+  val config : 'a1 environment -> Configuration.configuration
 
-  val blockapos : blockinformation -> n
+  val fblocks : 'a1 environment -> (string * Assembly.blockinformation) list
 
-  val assembly_add_content :
-    Buffer.BufferPlain.buffer_t -> n -> n -> AssemblyPlainWritable.coq_B -> n
+  val keys :
+    'a1 environment -> (Assembly.aid_t * Assembly.keyinformation) list
 
-  val backup :
-    AssemblyPlainWritable.coq_H -> AssemblyPlainWritable.coq_B -> n ->
-    Buffer.BufferPlain.buffer_t ->
-    AssemblyPlainWritable.coq_H * blockinformation
+  val cpp_mk_key256 : unit -> string
 
-  val assembly_get_content :
-    AssemblyPlainFull.coq_B -> n -> n -> Buffer.BufferPlain.buffer_t -> n
+  val cpp_mk_key128 : unit -> string
 
-  val restore :
-    AssemblyPlainFull.coq_B -> blockinformation ->
-    Buffer.BufferPlain.buffer_t option
- end
+  module type ENV =
+   sig
+    type coq_AB
 
-module Environment :
- sig
-  type environment = { cur_assembly : Assembly.AssemblyPlainWritable.coq_H;
-                       cur_buffer : Assembly.AssemblyPlainWritable.coq_B;
-                       config : Configuration.configuration;
-                       fblocks : (string * Assembly.blockinformation) list;
-                       keys : (string * Assembly.keyinformation) list }
+    type coq_E = coq_AB environment
 
-  val cur_assembly : environment -> Assembly.AssemblyPlainWritable.coq_H
+    val initial_environment : Configuration.configuration -> coq_E
+   end
 
-  val cur_buffer : environment -> Assembly.AssemblyPlainWritable.coq_B
+  module EnvironmentWritable :
+   sig
+    type coq_AB = Assembly.AssemblyPlainWritable.coq_B
 
-  val config : environment -> Configuration.configuration
+    type coq_E = coq_AB environment
 
-  val fblocks : environment -> (string * Assembly.blockinformation) list
+    val initial_environment : Configuration.configuration -> coq_E
 
-  val keys : environment -> (string * Assembly.keyinformation) list
+    val recreate_assembly : coq_AB environment -> coq_AB environment
 
-  val etaX : environment settable
+    val env_add_file_block :
+      string -> coq_AB environment -> Assembly.blockinformation -> coq_AB
+      environment
 
-  val initial_environment : Configuration.configuration -> environment
+    val env_add_aid_key :
+      Assembly.aid_t -> coq_AB environment -> Assembly.keyinformation ->
+      coq_AB environment
 
-  val recreate_assembly : environment -> environment
+    val key_for_aid :
+      coq_AB environment -> Assembly.aid_t -> Assembly.keyinformation option
 
-  val env_add_file_block :
-    string -> environment -> Assembly.blockinformation -> environment
+    val finalise_assembly : coq_AB environment -> coq_AB environment
 
-  val env_add_aid_key :
-    string -> environment -> Assembly.keyinformation -> environment
+    val finalise_and_recreate_assembly :
+      coq_AB environment -> coq_AB environment
 
-  val key_for_aid :
-    environment -> Assembly.aid_t -> Assembly.keyinformation option
+    val backup :
+      coq_AB environment -> string -> n -> Buffer.BufferPlain.buffer_t ->
+      coq_AB environment
+   end
 
-  val restore_assembly : environment -> Assembly.aid_t -> environment option
+  module EnvironmentReadable :
+   sig
+    type coq_AB = Assembly.AssemblyPlainFull.coq_B
 
-  val cpp_mk_key256 : unit -> string
+    type coq_E = coq_AB environment
 
-  val cpp_mk_key128 : unit -> string
+    val initial_environment : Configuration.configuration -> coq_E
 
-  val finalise_assembly : environment -> environment
+    val env_add_aid_key :
+      Assembly.aid_t -> coq_AB environment -> Assembly.keyinformation ->
+      coq_AB environment
 
-  val finalise_and_recreate_assembly : environment -> environment
+    val key_for_aid :
+      coq_AB environment -> Assembly.aid_t -> Assembly.keyinformation option
 
-  val backup :
-    environment -> string -> n -> Buffer.BufferPlain.buffer_t -> environment
+    val restore_assembly :
+      coq_AB environment -> Assembly.aid_t -> coq_AB environment option
+   end
  end
 
 module AssemblyCache :
@@ -503,16 +540,17 @@ module AssemblyCache :
 
   val wqueuesz : writequeue -> positive
 
-  type assemblycache = { acenvs : Environment.environment list; acsize : 
-                         nat; acwriteenv : Environment.environment;
+  type assemblycache = { acenvs : Environment.EnvironmentReadable.coq_E list;
+                         acsize : nat;
+                         acwriteenv : Environment.EnvironmentWritable.coq_E;
                          acconfig : Configuration.configuration;
                          acwriteq : writequeue; acreadq : readqueue }
 
-  val acenvs : assemblycache -> Environment.environment list
+  val acenvs : assemblycache -> Environment.EnvironmentReadable.coq_E list
 
   val acsize : assemblycache -> nat
 
-  val acwriteenv : assemblycache -> Environment.environment
+  val acwriteenv : assemblycache -> Environment.EnvironmentWritable.coq_E
 
   val acconfig : assemblycache -> Configuration.configuration
 
@@ -530,15 +568,16 @@ module AssemblyCache :
     assemblycache -> readqueueentity -> bool * assemblycache
 
   val try_restore_assembly :
-    Configuration.configuration -> Assembly.aid_t -> Environment.environment
-    option
+    Configuration.configuration -> Assembly.aid_t ->
+    Environment.EnvironmentReadable.coq_E option
 
   val set_envs :
-    assemblycache -> Environment.environment list -> assemblycache
+    assemblycache -> Environment.EnvironmentReadable.coq_E list ->
+    assemblycache
 
   val ensure_assembly :
     assemblycache -> Assembly.aid_t ->
-    (Environment.environment * assemblycache) option
+    (Environment.EnvironmentReadable.coq_E * assemblycache) option
 
   val run_read_requests :
     assemblycache -> readqueueentity list -> readqueueresult list ->
diff --git a/theories/Assembly.v b/theories/Assembly.v
index edab9f5..197a338 100644
--- a/theories/Assembly.v
+++ b/theories/Assembly.v
@@ -36,15 +36,20 @@ Definition assemblysize (n : Nchunks.Private.t) : N := chunksize_N * (to_N n).
 
 Definition aid_t := string.
 
-Record assemblyinformation : Type :=
+Definition RecordAssemblyInformation := Set.
+Record assemblyinformation : RecordAssemblyInformation :=
     mkassembly
         { nchunks : Nchunks.Private.t
         ; aid : aid_t
         ; apos : N }.
+Print assemblyinformation.
 
 #[export] Instance etaX : Settable _ := settable! mkassembly <nchunks; aid; apos>.
+(* Print set.
+Print Setter. *)
 
-Record keyinformation : Type :=
+Definition RecordKeyInformation := Set.
+Record keyinformation : RecordKeyInformation :=
     mkkeyinformation
         { ivec : string
         ; pkey : string
@@ -52,60 +57,127 @@ Record keyinformation : Type :=
         ; localnchunks : positive
         }.
 
+Definition RecordBlockInformation := Set.
+Record blockinformation : RecordBlockInformation :=
+    mkblockinformation
+        { blockid : positive
+        ; bchecksum : string
+        ; blocksize : N
+        ; filepos : N
+        ; blockaid : aid_t
+        ; blockapos : N
+        }.
 
 Module Type ASS.
-    Definition H : Type := assemblyinformation.
+    (* Parameter H : RecordAssemblyInformation. *)
     Parameter B : Type.
-    (* Parameter assembly : Type. *)
-    Axiom create : configuration -> (H * B).
+    Axiom create : configuration -> (assemblyinformation * B).
     Axiom buffer_len : B -> N.
     Axiom calc_checksum : B -> string.
 End ASS.
+Print ASS.
 
 Module AssemblyPlainWritable : ASS.
-    Definition H : Type := assemblyinformation.
+    (* Definition H : RecordAssemblyInformation := assemblyinformation. *)
     Definition B := BufferPlain.buffer_t.
     Definition buffer_len : B -> N := BufferPlain.buffer_len.
     Definition calc_checksum : B -> string := fun _ => "<>".
-    Definition create (c : configuration) : H * B :=
+    Definition create (c : configuration) : assemblyinformation * B :=
         let chunks := config_nchunks c in
         let b := BufferPlain.buffer_create (chunksize_N * Nchunks.to_N chunks) in
         let rb := Buffer.ranbuf128 tt in
         let nb := BufferPlain.copy_sz_pos rb 0 16 b 0 in
         (mkassembly chunks (Utilities.rnd256 (my_id c)) nb, b).
 End AssemblyPlainWritable.
+Print AssemblyPlainWritable.
 
 Module AssemblyEncrypted : ASS.
-    Definition H : Type := assemblyinformation.
+    (* Definition H : RecordAssemblyInformation := assemblyinformation. *)
     Definition B := BufferEncrypted.buffer_t.
     Definition buffer_len : B -> N := BufferEncrypted.buffer_len.
     Definition calc_checksum : B -> string := BufferEncrypted.calc_checksum.
-    Definition create (c : configuration) : H * B :=
+    Definition create (c : configuration) : assemblyinformation * B :=
         let chunks := config_nchunks c in
         let b := BufferEncrypted.buffer_create (chunksize_N * Nchunks.to_N chunks) in
         (mkassembly chunks (Utilities.rnd256 (my_id c)) 0, b).
 End AssemblyEncrypted.
-(* Print AssemblyEncrypted. *)
+Print AssemblyEncrypted.
 
 Module AssemblyPlainFull : ASS.
-    Definition H : Type := assemblyinformation.
+    (* Definition H : RecordAssemblyInformation := assemblyinformation. *)
     Definition B := BufferPlain.buffer_t.
     Definition buffer_len : B -> N := BufferPlain.buffer_len.
     Definition calc_checksum : B -> string := BufferPlain.calc_checksum.
-    Definition create (c : configuration) :=
+    Definition create (c : configuration) : assemblyinformation * B :=
         let chunks := config_nchunks c in
         let sz := chunksize_N * Nchunks.to_N chunks in
         let b := BufferPlain.buffer_create sz in
         (mkassembly chunks (Utilities.rnd256 (my_id c)) sz, b).
 End AssemblyPlainFull.
+Print AssemblyPlainFull.
+
+
+Section Code_Writeable.
+(** operations on AssemblyPlainWriteable *)
+
+Axiom id_assembly_full_ainfo_from_writable : assemblyinformation -> assemblyinformation.
+Axiom id_assembly_full_buffer_from_writable : AssemblyPlainWritable.B -> AssemblyPlainFull.B.
+Program Definition finish (a : assemblyinformation) (b : AssemblyPlainWritable.B) : (assemblyinformation * AssemblyPlainFull.B) :=
+    ( id_assembly_full_ainfo_from_writable a
+    , id_assembly_full_buffer_from_writable b ).
+
+Axiom assembly_add_content : BufferPlain.buffer_t -> N -> N -> AssemblyPlainWritable.B -> N.
+Program Definition backup (a : assemblyinformation) (b : AssemblyPlainWritable.B) (fpos : N) (content : BufferPlain.buffer_t) : (assemblyinformation * blockinformation) :=
+    let apos_n := apos a in
+    let bsz := BufferPlain.buffer_len content in
+    let chksum := calc_checksum content in
+    let nwritten := assembly_add_content content bsz apos_n b in
+    let bi := {| blockid   := 1
+            ; bchecksum := chksum
+            ; blocksize := nwritten
+            ; filepos   := fpos
+            ; blockaid  := aid a
+            ; blockapos := apos_n |} in
+    let a' := set apos (fun ap => ap + nwritten) a in
+    (a', bi).
+
+End Code_Writeable.
+
+
+Section Code_Readable.
+(** operations on AssemblyPlainFull *)
+
+Axiom id_buffer_t_from_full : AssemblyPlainFull.B -> BufferPlain.buffer_t.
+(* Axiom id_buffer_t_from_writable : AssemblyPlainWritable.B -> BufferPlain.buffer_t. *)
+Axiom id_assembly_enc_buffer_t_from_buf : BufferEncrypted.buffer_t -> AssemblyEncrypted.B.
+Program Definition encrypt (a : assemblyinformation) (b : AssemblyPlainFull.B) (ki : keyinformation) : option (assemblyinformation * AssemblyEncrypted.B) :=
+    let a' := set apos (const (assemblysize (nchunks a))) a in
+    let benc  := Buffer.encrypt (id_buffer_t_from_full b) (ivec ki) (pkey ki) in
+    let b' := id_assembly_enc_buffer_t_from_buf benc in
+    Some (a', b').
+
+Axiom assembly_get_content : AssemblyPlainFull.B -> N -> N -> BufferPlain.buffer_t -> N.
+Program Definition restore (b : AssemblyPlainFull.B) (bi : blockinformation) : option BufferPlain.buffer_t :=
+    let bsz := blocksize bi in
+    let b' := BufferPlain.buffer_create bsz in
+    let nw := assembly_get_content b bsz (blockapos bi) b' in
+    if N.eqb nw bsz then
+        let bcksum := calc_checksum b' in
+        if String.eqb bcksum (bchecksum bi) then
+            Some b'
+        else
+            None
+    else None.
+
+End Code_Readable.
 
 
 Section Code_Encrypted.
 (** operations on AssemblyEncrypted *)
 
 Axiom id_buffer_t_from_enc : AssemblyEncrypted.B -> BufferEncrypted.buffer_t.
-Axiom id_assembly_plain_buffer_t_from_buf : BufferPlain.buffer_t -> AssemblyPlainWritable.B.
-Program Definition decrypt (a : AssemblyEncrypted.H) (b : AssemblyEncrypted.B) (ki : keyinformation) : option (AssemblyPlainWritable.H * AssemblyPlainWritable.B) :=
+Axiom id_assembly_plain_buffer_t_from_buf : BufferPlain.buffer_t -> AssemblyPlainFull.B.
+Program Definition decrypt (a : assemblyinformation) (b : AssemblyEncrypted.B) (ki : keyinformation) : option (assemblyinformation * AssemblyPlainFull.B) :=
     let a' := set apos (const 0) a in
     let bdec := Buffer.decrypt (id_buffer_t_from_enc b) (ivec ki) (pkey ki) in
     let b' := id_assembly_plain_buffer_t_from_buf bdec in
@@ -113,11 +185,9 @@ Program Definition decrypt (a : AssemblyEncrypted.H) (b : AssemblyEncrypted.B) (
 
 Axiom chunk_identifier : configuration -> aid_t -> positive -> string.
 Axiom chunk_identifier_path : configuration -> aid_t -> positive -> string.
-
 Axiom ext_load_chunk_from_path : string -> option BufferEncrypted.buffer_t.
-
 Axiom id_enc_from_buffer_t : BufferEncrypted.buffer_t -> AssemblyEncrypted.B.
-Program Definition recall (c : configuration) (a : AssemblyEncrypted.H) : option (AssemblyEncrypted.H * AssemblyEncrypted.B) :=
+Program Definition recall (c : configuration) (a : assemblyinformation) : option (assemblyinformation * AssemblyEncrypted.B) :=
     let cidlist := Utilities.make_list (nchunks a) in
     let b := BufferEncrypted.buffer_create (Conversion.pos2N (nchunks a) * chunksize_N) in
     let aid := aid a in
@@ -143,7 +213,7 @@ Program Definition recall (c : configuration) (a : AssemblyEncrypted.H) : option
     else None.
 
 Axiom ext_store_chunk_to_path : string -> N -> N -> BufferEncrypted.buffer_t -> N.
-Program Definition extract (c : configuration) (a : AssemblyEncrypted.H) (b : AssemblyEncrypted.B) : N :=
+Program Definition extract (c : configuration) (a : assemblyinformation) (b : AssemblyEncrypted.B) : N :=
     let aid := aid a in
     let buf := id_buffer_t_from_enc b in
     List.fold_left
@@ -157,87 +227,4 @@ Program Definition extract (c : configuration) (a : AssemblyEncrypted.H) (b : As
 
 End Code_Encrypted.
 
-Section Code_Plain.
-(** operations on AssemblyPlain *)
-
-Axiom id_buffer_t_from_full : AssemblyPlainFull.B -> BufferPlain.buffer_t.
-(* Axiom id_buffer_t_from_writable : AssemblyPlainWritable.B -> BufferPlain.buffer_t. *)
-Axiom id_assembly_enc_buffer_t_from_buf : BufferEncrypted.buffer_t -> AssemblyEncrypted.B.
-Axiom id_assembly_full_buffer_from_writable : AssemblyPlainWritable.B -> AssemblyPlainFull.B.
-
-Program Definition finish (a : AssemblyPlainWritable.H) (b : AssemblyPlainWritable.B) : (AssemblyPlainFull.H * AssemblyPlainFull.B) :=
-    ( a
-    , id_assembly_full_buffer_from_writable b ).
-
-Program Definition encrypt (a : AssemblyPlainFull.H) (b : AssemblyPlainFull.B) (ki : keyinformation) : option (AssemblyEncrypted.H * AssemblyEncrypted.B) :=
-    let a' := set apos (const (assemblysize (nchunks a))) a in
-    let benc  := Buffer.encrypt (id_buffer_t_from_full b) (ivec ki) (pkey ki) in
-    let b' := id_assembly_enc_buffer_t_from_buf benc in
-    Some (a', b').
-
-(** backup: add a buffer to an assembly
-    return blockinformation *)
-
-Record blockinformation : Type := mkblockinformation
-    { blockid : positive
-    ; bchecksum : string
-    ; blocksize : N
-    ; filepos : N
-    ; blockaid : string
-    ; blockapos : N
-    }.
-
-Axiom assembly_add_content : BufferPlain.buffer_t -> N -> N -> AssemblyPlainWritable.B -> N.
-Program Definition backup (a : AssemblyPlainWritable.H) (b : AssemblyPlainWritable.B) (fpos : N) (content : BufferPlain.buffer_t) : (AssemblyPlainWritable.H * blockinformation) :=
-    let apos_n := apos a in
-    let bsz := BufferPlain.buffer_len content in
-    let chksum := calc_checksum content in
-    let nwritten := assembly_add_content content bsz apos_n b in
-    let bi := {| blockid   := 1
-               ; bchecksum := chksum
-               ; blocksize := nwritten
-               ; filepos   := fpos
-               ; blockaid  := aid a
-               ; blockapos := apos_n |} in
-    let a' := set apos (fun ap => ap + nwritten) a in
-    (a', bi).
-
-(** restore: copy buffer from an assembly
-    and return it *)
-Axiom assembly_get_content : AssemblyPlainFull.B -> N -> N -> BufferPlain.buffer_t -> N.
-Program Definition restore (b : AssemblyPlainFull.B) (bi : blockinformation) : option BufferPlain.buffer_t :=
-    let bsz := blocksize bi in
-    let b' := BufferPlain.buffer_create bsz in
-    let nw := assembly_get_content b bsz (blockapos bi) b' in
-    if N.eqb nw bsz then
-        let bcksum := calc_checksum b' in
-        if String.eqb bcksum (bchecksum bi) then
-            Some b'
-        else
-            None
-    else None.
-
-End Code_Plain.
-
-(* Section lemmas.
-
-Variable c : configuration.
-Variable a : assemblyinformation.
-
-Fact external_decrypt_of_encrypt_id : forall (b : AssemblyPlainFull.B) (p : string), cpp_decrypt_assembly (cpp_encrypt_assembly b p) p = b.
-Proof.
-    intros.
-    Admitted.
-
-Lemma decrypt_of_encrypt_id :
-    forall (b : AssemblyPlainFull.B) (b' : AssemblyEncrypted.B) (b'' : AssemblyPlainFull.B)  (map : RelationAidKey.Map), 
-    encrypt a b map = Some b' /\ decrypt a b' map = Some b'' -> b'' = b.
-Proof.
-    intros.
-    (* unfold decrypt. unfold encrypt. *)
-    (* apply external_decrypt_of_encrypt_id. *)
-    Admitted.
-
-End lemmas. *)
-
 End Assembly.
diff --git a/theories/AssemblyCache.v b/theories/AssemblyCache.v
index c0c9e30..bbd4ec3 100644
--- a/theories/AssemblyCache.v
+++ b/theories/AssemblyCache.v
@@ -60,10 +60,10 @@ Record writequeue : Type :=
 
 Record assemblycache : Type :=
     mkassemblycache
-        { acenvs : list environment
+        { acenvs : list EnvironmentReadable.E
         ; acsize : nat
             (* ^ read environments of a fixed maximal size *)
-        ; acwriteenv : environment
+        ; acwriteenv : EnvironmentWritable.E
             (* ^ write environment, exactly one *)
         ; acconfig : configuration
             (* ^ configuration needed to create new assemblies *)
@@ -77,7 +77,7 @@ Record assemblycache : Type :=
 Definition prepare_assemblycache (c : configuration) (size : positive) : assemblycache :=
     {| acenvs := nil
      ; acsize := Pos.to_nat size
-     ; acwriteenv := Environment.initial_environment c
+     ; acwriteenv := EnvironmentWritable.initial_environment c
      ; acconfig := c
      ; acwriteq := (mkwritequeue nil qsize)
      ; acreadq := (mkreadqueue nil qsize)
@@ -101,17 +101,17 @@ Program Definition enqueue_read_request (ac : assemblycache) (req : readqueueent
                   acreadq := {| rqueue := List.app (rqueue ac.(acreadq)) (req :: nil); rqueuesz := rqueuesz ac.(acreadq) |};
                   acwriteq := ac.(acwriteq)  |}).
 
-Program Definition try_restore_assembly (config : Configuration.configuration) (sel_aid : Assembly.aid_t) : option environment :=
-    Environment.restore_assembly (Environment.initial_environment config) sel_aid.
+Program Definition try_restore_assembly (config : Configuration.configuration) (sel_aid : Assembly.aid_t) : option EnvironmentReadable.E :=
+    EnvironmentReadable.restore_assembly (EnvironmentReadable.initial_environment config) sel_aid.
 
-Program Definition set_envs (ac0 : assemblycache) (envs : list Environment.environment) : assemblycache :=
+Program Definition set_envs (ac0 : assemblycache) (envs : list EnvironmentReadable.E) : assemblycache :=
     {| acenvs := envs; acsize := ac0.(acsize);
        acwriteenv := ac0.(acwriteenv); acconfig := ac0.(acconfig);
        acreadq := ac0.(acreadq); acwriteq := ac0.(acwriteq) |}.
 
 (* ensure that an environment with assembly (by aid) is available
    and that it is in the head position of the list of envs *)
-Program Definition ensure_assembly (ac0 : assemblycache) (sel_aid : Assembly.aid_t) : option (environment * assemblycache) :=
+Program Definition ensure_assembly (ac0 : assemblycache) (sel_aid : Assembly.aid_t) : option (EnvironmentReadable.E * assemblycache) :=
     match ac0.(acenvs) with
     | nil => (* create first env *)
         match try_restore_assembly ac0.(acconfig) sel_aid with
@@ -120,7 +120,7 @@ Program Definition ensure_assembly (ac0 : assemblycache) (sel_aid : Assembly.aid
            Some (env, set_envs ac0 (env :: nil))
         end
     | e1 :: nil =>
-        if String.eqb (aid e1.(cur_assembly)) sel_aid then
+        if String.eqb (aid e1.(cur_assembly AssemblyPlainFull.B)) sel_aid then
             Some (e1, ac0)
         else
             match try_restore_assembly ac0.(acconfig) sel_aid with
@@ -131,15 +131,15 @@ Program Definition ensure_assembly (ac0 : assemblycache) (sel_aid : Assembly.aid
                 else Some (env, set_envs ac0 (env :: e1 :: nil))
             end
     | e1 :: r =>
-        if String.eqb (aid e1.(cur_assembly)) sel_aid then
+        if String.eqb (aid e1.(cur_assembly AssemblyPlainFull.B)) sel_aid then
             (* found in first position *)
             Some (e1, ac0)
         else
-            let found := List.filter (fun e => String.eqb (aid e.(cur_assembly)) sel_aid) r in
+            let found := List.filter (fun e => String.eqb (aid e.(cur_assembly AssemblyPlainFull.B)) sel_aid) r in
             match found with
             | efound :: _ =>
                 (* found further down -> move to first position *)
-                let r' := List.filter (fun e => negb (String.eqb (aid e.(cur_assembly)) sel_aid)) r in
+                let r' := List.filter (fun e => negb (String.eqb (aid e.(cur_assembly AssemblyPlainFull.B)) sel_aid)) r in
                 Some (efound, set_envs ac0 (efound :: e1 :: r'))
             | nil =>
                 match try_restore_assembly ac0.(acconfig) sel_aid with
@@ -163,7 +163,7 @@ Program Fixpoint run_read_requests (ac0 : assemblycache) (reqs : list readqueuee
         | None => (res, ac0)
         | Some (env, ac1) =>
             let buf := BufferPlain.buffer_create h.(qrlen) in
-            let _ := assembly_get_content (id_assembly_full_buffer_from_writable env.(cur_buffer)) h.(qrlen) h.(qapos) buf in
+            let _ := assembly_get_content env.(cur_buffer AssemblyPlainFull.B) h.(qrlen) h.(qapos) buf in
             run_read_requests ac1 r ({| readrequest := h; rresult := buf |} :: res)
         end
     end.
@@ -173,11 +173,11 @@ Program Fixpoint run_write_requests (ac0 : assemblycache) (reqs : list writequeu
     match reqs with
     | nil => (res, ac0)
     | h :: r =>
-        let env := Environment.backup ac0.(acwriteenv) h.(qfhash) h.(qfpos) h.(qbuffer) in
+        let env := EnvironmentWritable.backup ac0.(acwriteenv) h.(qfhash) h.(qfpos) h.(qbuffer) in
         let ac1 := {| acenvs := ac0.(acenvs); acsize := ac0.(acsize); acwriteenv := env; acconfig := ac0.(acconfig);
                       acreadq := ac0.(acreadq); acwriteq := {| wqueue := nil; wqueuesz := wqueuesz ac0.(acwriteq) |} |} in
         run_write_requests ac1 r ({| writerequest := h;
-                                     wresult := {| qaid := env.(cur_assembly).(aid); qapos := env.(cur_assembly).(apos);
+                                     wresult := {| qaid := env.(cur_assembly AssemblyPlainWritable.B).(aid); qapos := env.(cur_assembly AssemblyPlainWritable.B).(apos);
                                                    qrlen := buffer_len h.(qbuffer) |} |} :: res)
     end.
 
@@ -211,13 +211,13 @@ Program Definition iterate_write_queue (ac0 : assemblycache) : (list writequeuer
 
 (* finalise and recreate writable environment, and extract chunks from it *)
 Program Definition flush (ac0 : assemblycache) : assemblycache :=
-    let env := Environment.finalise_and_recreate_assembly ac0.(acwriteenv) in
+    let env := EnvironmentWritable.finalise_and_recreate_assembly ac0.(acwriteenv) in
     {| acenvs := nil; acsize := ac0.(acsize); acwriteenv := env; acconfig := ac0.(acconfig);
        acreadq := ac0.(acreadq); acwriteq := ac0.(acwriteq) |}.
 
 (* terminate cache: finalise writable environment and extract chunks from it *)
 Program Definition close (ac0 : assemblycache) : assemblycache :=
-    let env := Environment.finalise_assembly ac0.(acwriteenv) in
+    let env := EnvironmentWritable.finalise_assembly ac0.(acwriteenv) in
     {| acenvs := nil; acsize := ac0.(acsize); acwriteenv := env; acconfig := ac0.(acconfig);
        acreadq := ac0.(acreadq); acwriteq := ac0.(acwriteq) |}.
 
@@ -228,13 +228,13 @@ Section Validation.
 (* our database: the assembly with id "aid_found" exists and can be restored *)
 Axiom db_env_for_known_aid : forall e c,
     let env :=
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+        {| fblocks := e.(fblocks AssemblyPlainFull.B); keys := e.(keys AssemblyPlainFull.B); config := e.(config AssemblyPlainFull.B); cur_buffer := e.(cur_buffer AssemblyPlainFull.B);
         cur_assembly := mkassembly c.(config_nchunks) "aid_found" 0 |} in
     try_restore_assembly c "aid_found" = Some env.
 
 (* all other assemblies are not found. *)
 Axiom db_env_none_default : forall a c,
-    let env := initial_environment c in
+    let env := EnvironmentReadable.initial_environment c in
     try_restore_assembly c a = None.
 
 
@@ -275,7 +275,8 @@ Proof.
     induction reqs. simpl.
     - reflexivity.
     - apply run_read_requests_same_length. 
-Abort.
+Qed.
+
 End Unfinished.
 
 (* running the read queue with a single read request,
@@ -292,14 +293,14 @@ Proof.
     unfold iterate_read_queue.
     unfold filter. simpl.
     unfold ensure_assembly. simpl.
-    set (e0 := initial_environment Config).
+    set (e0 := EnvironmentReadable.initial_environment Config).
     rewrite db_env_for_known_aid with (e := e0).
     auto.
 Qed.
 
 Example first_env_for_empty_cache : forall c,
     let ac0 := prepare_assemblycache c 3 in
-    let e0 := Environment.initial_environment c in
+    let e0 := EnvironmentReadable.initial_environment c in
     let env1 := match try_restore_assembly c "aid_found" with
                | Some e => e
                | None => e0
@@ -310,7 +311,7 @@ Example first_env_for_empty_cache : forall c,
 Proof.
     intro Config.
     unfold ensure_assembly. simpl.
-    set (e0 := initial_environment Config).
+    set (e0 := EnvironmentReadable.initial_environment Config).
     rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. reflexivity.
 Qed.
@@ -319,18 +320,19 @@ Qed.
     aid (cur_assembly (initial_environment c)) = "". *)
 
 Example second_of3_env_for_not_filled_cache : forall c,
+    let AB := AssemblyPlainFull.B in
     let ac0 := prepare_assemblycache c 3 in
-    let e0 := Environment.initial_environment c in
-    let env1 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let e0 := EnvironmentReadable.initial_environment c in
+    let env1 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_some" 0 |} in
     (* from this assembly cache: *)
     let ac1 := set_envs ac0 (env1 :: nil) in
     let env2 := match try_restore_assembly c "aid_found" with
                 | Some e =>
-                    {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+                    {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
                     cur_assembly := mkassembly c.(config_nchunks) "aid_found" 0 |}
-                | None => Environment.initial_environment c
+                | None => EnvironmentReadable.initial_environment c
                 end in
     (* to this assembly cache: env2 added to head *)
     let ac' := {| acenvs := env2 :: env1 :: nil; acsize := ac1.(acsize); acwriteenv := ac1.(acwriteenv); acconfig := ac1.(acconfig);
@@ -339,24 +341,25 @@ Example second_of3_env_for_not_filled_cache : forall c,
 Proof.
     intro Config.
     unfold ensure_assembly. simpl.
-    set (e0 := initial_environment Config).
+    set (e0 := EnvironmentReadable.initial_environment Config).
     rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. simpl. reflexivity.
 Qed.
 
 Example second_of2_env_for_not_filled_cache : forall c,
+    let AB := AssemblyPlainFull.B in
     let ac0 := prepare_assemblycache c 2 in
-    let e0 := Environment.initial_environment c in
-    let env1 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let e0 := EnvironmentReadable.initial_environment c in
+    let env1 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_some" 0 |} in
     (* from this assembly cache: *)
     let ac1 := set_envs ac0 (env1 :: nil) in
     let env2 := match try_restore_assembly c "aid_found" with
                 | Some e =>
-                    {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+                    {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
                     cur_assembly := mkassembly c.(config_nchunks) "aid_found" 0 |}
-                | None => Environment.initial_environment c
+                | None => EnvironmentReadable.initial_environment c
                 end in
     (* to this assembly cache: env2 added to head *)
     let ac' := {| acenvs := env2 :: env1 :: nil; acsize := ac1.(acsize); acwriteenv := ac1.(acwriteenv); acconfig := ac1.(acconfig);
@@ -365,27 +368,28 @@ Example second_of2_env_for_not_filled_cache : forall c,
 Proof.
     intro Config.
     unfold ensure_assembly. simpl.
-    set (e0 := initial_environment Config).
+    set (e0 := EnvironmentReadable.initial_environment Config).
     rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. simpl. reflexivity.
 Qed.
 
 Example third_of2_env_for_filled_cache : forall c,
+    let AB := AssemblyPlainFull.B in
     let ac0 := prepare_assemblycache c 2 in
-    let e0 := Environment.initial_environment c in
-    let env1 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let e0 := EnvironmentReadable.initial_environment c in
+    let env1 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_some" 0 |} in
-    let env2 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let env2 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_other" 0 |} in
     (* from this "full" assembly cache: env3 at head, env1 dropped *)
     let ac1 := set_envs ac0 (env2 :: env1 :: nil) in
     let env3 := match try_restore_assembly c "aid_found" with
                 | Some e =>
-                    {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+                    {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
                     cur_assembly := mkassembly c.(config_nchunks) "aid_found" 0 |}
-                | None => Environment.initial_environment c
+                | None => EnvironmentReadable.initial_environment c
                 end in
     (* to this "full" assembly cache: *)
     let ac' := {| acenvs := env3 :: env2 :: nil; acsize := ac1.(acsize); acwriteenv := ac1.(acwriteenv); acconfig := ac1.(acconfig);
@@ -394,19 +398,20 @@ Example third_of2_env_for_filled_cache : forall c,
 Proof.
     intro Config.
     unfold ensure_assembly. simpl.
-    set (e0 := initial_environment Config).
+    set (e0 := EnvironmentReadable.initial_environment Config).
     rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. simpl. reflexivity.
 Qed.
 
 Example found_assembly_in_filled_cache_of_size_2 : forall c,
+    let AB := AssemblyPlainFull.B in
     let ac0 := prepare_assemblycache c 2 in
-    let e0 := Environment.initial_environment c in
-    let env1 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let e0 := EnvironmentReadable.initial_environment c in
+    let env1 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_found" 0 |} in
-    let env2 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let env2 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_other" 0 |} in
     (* from this "full" assembly cache: *)
     let ac1 := set_envs ac0 (env2 :: env1 :: nil) in
@@ -417,21 +422,22 @@ Example found_assembly_in_filled_cache_of_size_2 : forall c,
 Proof.
     intro Config.
     unfold ensure_assembly. simpl.
-    set (e0 := initial_environment Config).
+    set (e0 := EnvironmentReadable.initial_environment Config).
     unfold set_envs. simpl. reflexivity.
 Qed.
 
 Example found_assembly_in_filled_cache_of_size_3 : forall c,
+    let AB := AssemblyPlainFull.B in
     let ac0 := prepare_assemblycache c 3 in
-    let e0 := Environment.initial_environment c in
-    let env1 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let e0 := EnvironmentReadable.initial_environment c in
+    let env1 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_found" 0 |} in
-    let env2 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let env2 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_other" 0 |} in
-    let env3 := let e := Environment.initial_environment c in
-        {| fblocks := e.(fblocks); keys := e.(keys); config := e.(config); cur_buffer := e.(cur_buffer);
+    let env3 := let e := EnvironmentReadable.initial_environment c in
+        {| fblocks := e.(fblocks AB); keys := e.(keys AB); config := e.(config AB); cur_buffer := e.(cur_buffer AB);
         cur_assembly := mkassembly c.(config_nchunks) "aid_latest" 0 |} in
     (* from this "full" assembly cache: *)
     let ac1 := set_envs ac0 (env3 :: env2 :: env1 :: nil) in
@@ -442,7 +448,7 @@ Example found_assembly_in_filled_cache_of_size_3 : forall c,
 Proof.
     intro Config.
     unfold ensure_assembly. simpl.
-    set (e0 := initial_environment Config).
+    set (e0 := EnvironmentReadable.initial_environment Config).
     unfold set_envs. simpl. reflexivity.
 Qed.
 
diff --git a/theories/Environment.v b/theories/Environment.v
index 6664f8d..2ddcb41 100644
--- a/theories/Environment.v
+++ b/theories/Environment.v
@@ -14,102 +14,152 @@ From LXR Require Import Nchunks.
 
 Module Export Environment.
 
-(* Open Scope positive_scope. *)
 Open Scope N_scope.
 
-Record environment : Type :=
+
+Definition RecordEnvironment := Type.
+Record environment (AB : Type) : RecordEnvironment :=
     mkenvironment
-        { cur_assembly : AssemblyPlainWritable.H
-        ; cur_buffer : AssemblyPlainWritable.B
+        { cur_assembly : assemblyinformation
+        ; cur_buffer : AB
         ; config : configuration
         ; fblocks : list (string * Assembly.blockinformation)
-        ; keys : list (string * Assembly.keyinformation)
+        ; keys : list (aid_t * Assembly.keyinformation)
         }.
+(* #[export] Instance etaX : Settable _ := settable! mkenvironment (AB) <cur_assembly; cur_buffer; config; fblocks; keys>. *)
+(* Print environment.
+Print cur_assembly.
+Print set.
+Print Setter.  *)
 
-#[export] Instance etaX : Settable _ := settable! mkenvironment <cur_assembly; cur_buffer; config; fblocks; keys>.
-
-Definition initial_environment (c : configuration) : environment :=
-    let (a,b) := AssemblyPlainWritable.create c in
-    {| cur_assembly := a
-    ;  cur_buffer := b
-    ;  config := c
-    ;  fblocks := nil
-    ;  keys := nil
-    |}.
+Axiom cpp_mk_key256 : unit -> string.
+Axiom cpp_mk_key128 : unit -> string.
 
-Definition recreate_assembly (e : environment) : environment :=
-    let (a,b) := AssemblyPlainWritable.create e.(config) in
-    set cur_assembly (const a) (set cur_buffer (const b) e).
 
-Definition env_add_file_block (fname : string) (e : environment) (bi : Assembly.blockinformation) : environment :=
-    set fblocks (fun bs => (fname,bi) :: bs) e.
+Module Type ENV.
+    Parameter AB : Type.
+    Definition E : RecordEnvironment := environment AB.
+    Axiom initial_environment : configuration -> E.
+End ENV.
+Print ENV.
 
-Definition env_add_aid_key (aid : string) (e : environment) (ki : keyinformation) : environment :=
-    set keys (fun ks => (aid,ki) :: ks) e.
+Module EnvironmentWritable <: ENV.
+    Definition AB := AssemblyPlainWritable.B.
+    Definition E : RecordEnvironment := environment AB.
+    Definition initial_environment (c : configuration) : E :=
+        let (a,b) := AssemblyPlainWritable.create c in
+        {| cur_assembly := a
+        ;  cur_buffer := b
+        ;  config := c
+        ;  fblocks := nil
+        ;  keys := nil
+        |}.
+    Definition recreate_assembly (e : environment AB) : environment AB :=
+        let (a,b) := AssemblyPlainWritable.create (e.(config AB)) in
+        {| cur_assembly := a; cur_buffer := b
+        ;  config := e.(config AB)
+        ;  fblocks := e.(fblocks AB)
+        ;  keys := e.(keys AB)
+        |}.
+    Definition env_add_file_block (fname : string) (e : environment AB) (bi : Assembly.blockinformation) : environment AB :=
+        {| cur_assembly := e.(cur_assembly AB)
+        ;  cur_buffer := e.(cur_buffer AB)
+        ;  config := e.(config AB)
+        ;  fblocks := (fname,bi) :: e.(fblocks AB)
+        ;  keys := e.(keys AB)
+        |}.
+    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)
+        |}.
+    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.
+    Definition finalise_assembly (e0 : environment AB) : environment AB :=
+        let a0 := e0.(cur_assembly AB) in
+        let apos := Assembly.apos a0 in
+        if N.ltb 0 apos then
+            let (a,b) := Assembly.finish a0 e0.(cur_buffer AB) in
+            let ki := {| pkey := cpp_mk_key256 tt
+                    ; ivec := cpp_mk_key128 tt
+                    ; localnchunks := e0.(config AB).(Configuration.config_nchunks)
+                    ; localid := e0.(config AB).(Configuration.my_id) |} in
+            let e1 := env_add_aid_key (aid a) e0 ki in
+            match Assembly.encrypt a b ki with
+            | None => e0
+            | Some (a',b') =>
+                let n := Assembly.extract e1.(config AB) a' b' in
+                if N.eqb n (Assembly.assemblysize e0.(config AB).(Configuration.config_nchunks))
+                then e1
+                else e0
+            end
+        else e0.
+    
+    Definition finalise_and_recreate_assembly (e0 : environment AB) : environment AB :=
+        let e1 := finalise_assembly e0 in
+        EnvironmentWritable.recreate_assembly e1.
+    
+    Program Definition backup (e0 : environment AB) (fp : string) (fpos : N) (content : BufferPlain.buffer_t) : environment AB :=
+        let afree := N.sub (Assembly.assemblysize e0.(config AB).(Configuration.config_nchunks)) e0.(cur_assembly AB).(apos) in
+        let blen := BufferPlain.buffer_len content in
+        let e1 := if N.ltb afree blen then
+                    finalise_and_recreate_assembly e0
+                else e0 in
+        let (a', bi) := Assembly.backup e1.(cur_assembly AB) e1.(cur_buffer AB) fpos content in
+        {| cur_assembly := a'
+        ;  cur_buffer := e1.(cur_buffer AB)
+        ;  config := e1.(config AB)
+        ;  fblocks := (fp,bi) :: e1.(fblocks AB)
+        ;  keys := e1.(keys AB)
+        |}.
 
-(* find a key for an aid *)
-Definition key_for_aid (e : environment) (aid : Assembly.aid_t) : option keyinformation :=
-    match List.filter (fun e => String.eqb (fst e) aid) e.(keys) with
-    | nil => None
-    | (_,ki) :: _ => Some ki
-    end.
+End EnvironmentWritable.
+Print EnvironmentWritable.
 
-(* the decryption key needs to be preloaded in the key list
-   TODO: pass the key in
- *)
-Definition restore_assembly (e0 : environment) (aid : Assembly.aid_t) : option environment :=
-    match key_for_aid e0 aid with
-    | None => None
-    | Some k =>
-        match Assembly.recall e0.(config) {| nchunks := e0.(config).(Configuration.config_nchunks); aid := aid; apos := 0 |} with
+Module EnvironmentReadable <: ENV.
+    Definition AB := AssemblyPlainFull.B.
+    Definition E : RecordEnvironment := environment AB.
+    Definition initial_environment (c : configuration) : E :=
+        let (a,b) := AssemblyPlainFull.create c in
+        {| cur_assembly := a
+        ;  cur_buffer := b
+        ;  config := c
+        ;  fblocks := nil
+        ;  keys := nil
+        |}.
+    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)
+        |}.
+    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.
+    Definition restore_assembly (e0 : environment AB) (aid : aid_t) : option (environment AB) :=
+        match key_for_aid e0 aid with
         | None => None
-        | Some (a1, b1) =>
-            match Assembly.decrypt a1 b1 k with
+        | Some k =>
+            match Assembly.recall e0.(config AB) {| nchunks := e0.(config AB).(Configuration.config_nchunks); aid := aid; apos := 0 |} with
             | None => None
-            | Some (a2, b2) =>
-                Some {| cur_assembly := a2; cur_buffer := b2; config := e0.(config); fblocks := e0.(fblocks); keys := e0.(keys) |}
+            | Some (a1, b1) =>
+                match Assembly.decrypt a1 b1 k with
+                | None => None
+                | Some (a2, b2) =>
+                    Some {| cur_assembly := a2; cur_buffer := b2; config := e0.(config AB); fblocks := e0.(fblocks AB); keys := e0.(keys AB) |}
+                end
             end
-        end
-    end.
+        end.
 
-Axiom cpp_mk_key256 : unit -> string.
-Axiom cpp_mk_key128 : unit -> string.
-Definition finalise_assembly (e0 : environment) : environment :=
-    let a0 := cur_assembly e0 in
-    let apos := apos a0 in
-    if N.ltb 0 apos then
-        let (a,b) := Assembly.finish a0 (cur_buffer e0) in
-        let ki := {| pkey := cpp_mk_key256 tt
-                   ; ivec := cpp_mk_key128 tt
-                   ; localnchunks := e0.(config).(Configuration.config_nchunks)
-                   ; localid := e0.(config).(Configuration.my_id) |} in
-        let e1 := env_add_aid_key (aid a) e0 ki in
-        match Assembly.encrypt a b ki with
-        | None => e0
-        | Some (a',b') =>
-            let n := Assembly.extract (config e1) a' b' in
-            if N.eqb n (Assembly.assemblysize e0.(config).(Configuration.config_nchunks))
-            then e1
-            else e0
-        end
-    else e0.
-  
-Definition finalise_and_recreate_assembly (e0 : environment) : environment :=
-    let e1 := finalise_assembly e0 in
-    recreate_assembly e1.
-  
-Program Definition backup (e0 : environment) (fp : string) (fpos : N) (content : BufferPlain.buffer_t) : environment :=
-    let afree := N.sub (Assembly.assemblysize e0.(config).(Configuration.config_nchunks)) e0.(cur_assembly).(apos) in
-    let blen := BufferPlain.buffer_len content in
-    let e1 := if N.ltb afree blen then
-                finalise_and_recreate_assembly e0
-              else e0 in
-    let (a', bi) := 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)
-    |}.
+End EnvironmentReadable.
+Print EnvironmentReadable.
 
 End Environment.
\ No newline at end of file
diff --git a/theories/MakeML.v b/theories/MakeML.v
index 8978820..76df1c4 100644
--- a/theories/MakeML.v
+++ b/theories/MakeML.v
@@ -136,6 +136,7 @@ Extract Constant id_assembly_plain_buffer_t_from_buf => "fun b -> Helper.cpp_buf
 Extract Constant id_assembly_enc_buffer_t_from_buf => "fun b -> Helper.cpp_buffer_id b".
 Extract Constant id_enc_from_buffer_t => "fun b -> Helper.cpp_buffer_id b".
 Extract Constant id_assembly_full_buffer_from_writable => "fun b -> Helper.cpp_buffer_id b".
+Extract Constant id_assembly_full_ainfo_from_writable => "fun b -> Helper.cpp_buffer_id b".
 
 Extract Constant cpp_encrypt_buffer => "fun b iv pw -> Helper.cpp_encrypt_buffer b iv pw".
 Extract Constant cpp_decrypt_buffer => "fun b iv pw -> Helper.cpp_decrypt_buffer b iv pw".
diff --git a/theories/Version.v b/theories/Version.v
index 7087448..3a9cfcc 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 :=         "5".
+Definition build : string :=         "6".
 Definition version : string := major ++ "." ++ minor ++ "." ++ build.
 
 End Version.