cleanup

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

lxr.ml

@@ -941,11 +941,6 @@ module Assembly =
 
   let id_buffer_t_from_enc = fun b -> Helper.cpp_buffer_id b
 
-  (** val id_enc_from_buffer_t :
-      Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B **)
-
-  let id_enc_from_buffer_t = fun b -> Helper.cpp_buffer_id b
-
   (** val id_assembly_plain_buffer_t_from_buf :
       Buffer.BufferPlain.buffer_t -> AssemblyPlainWritable.coq_B **)
 
@@ -987,6 +982,11 @@ module Assembly =
     fun fp -> Helper.load_chunk_from_path (Mlcpp_filesystem.Filesystem.Path.from_string fp)
 
 
+  (** val id_enc_from_buffer_t :
+      Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B **)
+
+  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 **)
@@ -1046,11 +1046,6 @@ module Assembly =
 
   let id_buffer_t_from_full = fun b -> Helper.cpp_buffer_id b
 
-  (** val id_buffer_t_from_writable :
-      AssemblyPlainWritable.coq_B -> Buffer.BufferPlain.buffer_t **)
-
-  let id_buffer_t_from_writable = fun b -> Helper.cpp_buffer_id b
-
   (** val id_assembly_enc_buffer_t_from_buf :
       Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B **)
 
@@ -1784,8 +1779,8 @@ module BackupPlanner =
   (** val max_block_size : n **)
 
   let max_block_size =
-    Npos (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO (XO
-      XH)))))))))))))))))
+    N.mul (Npos (XO (XO (XO (XO (XO (XO (XO XH)))))))) (Npos (XO (XO (XO (XO
+      (XO (XO (XO (XO (XO (XO XH)))))))))))
 
   (** val analyse_file :
       positive -> n -> positive -> string ->
@@ -1821,7 +1816,7 @@ module Version =
   (** val build : string **)
 
   let build =
-    "2"
+    "4"
 
   (** val version : string **)
 

lxr.mli

@@ -316,9 +316,6 @@ module Assembly :
   val id_buffer_t_from_enc :
     AssemblyEncrypted.coq_B -> Buffer.BufferEncrypted.buffer_t
 
-  val id_enc_from_buffer_t :
-    Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B
-
   val id_assembly_plain_buffer_t_from_buf :
     Buffer.BufferPlain.buffer_t -> AssemblyPlainWritable.coq_B
 
@@ -335,6 +332,9 @@ module Assembly :
   val ext_load_chunk_from_path :
     string -> Buffer.BufferEncrypted.buffer_t option
 
+  val id_enc_from_buffer_t :
+    Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B
+
   val recall :
     Configuration.configuration -> AssemblyEncrypted.coq_H ->
     (AssemblyEncrypted.coq_H * AssemblyEncrypted.coq_B) option
@@ -349,9 +349,6 @@ module Assembly :
   val id_buffer_t_from_full :
     AssemblyPlainFull.coq_B -> Buffer.BufferPlain.buffer_t
 
-  val id_buffer_t_from_writable :
-    AssemblyPlainWritable.coq_B -> Buffer.BufferPlain.buffer_t
-
   val id_assembly_enc_buffer_t_from_buf :
     Buffer.BufferEncrypted.buffer_t -> AssemblyEncrypted.coq_B
 

theories/Assembly.v

@@ -2,6 +2,12 @@
       e L y K s e e R
 *)
 
+From Coq Require Import Strings.String .
+Require Import ZArith NArith PArith.
+From Coq Require Import NArith.BinNat.
+
+From LXR Require Import Nchunks Buffer Configuration Conversion Utilities.
+
 Module Export Assembly.
 
 (**
@@ -15,17 +21,11 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 (* Unset Printing Implicit Defensive. *)
 
-From Coq Require Import Strings.String .
-Require Import ZArith NArith PArith.
-From Coq Require Import NArith.BinNat.
 Open Scope positive_scope.
 Open Scope N_scope.
 Open Scope list_scope.
 Open Scope string_scope.
 
-From LXR Require Import Nchunks Buffer Configuration Conversion Utilities.
-
-
 Definition chunkwidth  : positive := 256%positive.
 Definition chunklength : positive := 1024%positive.
 Definition chunksize   : positive := chunkwidth * chunklength.
@@ -98,7 +98,6 @@ Section Code_Encrypted.
 (** operations on AssemblyEncrypted *)
 
 Axiom id_buffer_t_from_enc : AssemblyEncrypted.B -> BufferEncrypted.buffer_t.
-Axiom id_enc_from_buffer_t : BufferEncrypted.buffer_t -> AssemblyEncrypted.B.
 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) :=
     let a' := mkassembly (nchunks a) (aid a) 0 in
@@ -111,6 +110,7 @@ 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) :=
     let cidlist := Utilities.make_list (nchunks a) in
     let b := BufferEncrypted.buffer_create (Conversion.pos2N (nchunks a) * chunksize_N) in
@@ -155,7 +155,7 @@ 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_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.
 

theories/AssemblyCache.v

@@ -2,16 +2,10 @@
       e L y K s e e R
 *)
 
-Module Export AssemblyCache.
-
 Require Import Program.
 Require Import NArith PArith.
 From Coq Require Import NArith.BinNat Lists.List Strings.String Lia.
 
-Open Scope N_scope.
-Open Scope list_scope.
-Open Scope string_scope.
-
 From LXR Require Import Assembly.
 From LXR Require Import Buffer.
 From LXR Require Import Configuration.
@@ -20,6 +14,12 @@ From LXR Require Import Environment.
 From LXR Require Import Nchunks.
 From LXR Require Import Utilities.
 
+Module Export AssemblyCache.
+
+Open Scope N_scope.
+Open Scope list_scope.
+Open Scope string_scope.
+
 Record readqueueentity : Type :=
     mkreadqueueentity
         { qaid : Assembly.aid_t
@@ -168,14 +168,17 @@ Program Fixpoint run_read_requests (ac0 : assemblycache) (reqs : list readqueuee
         end
     end.
 
-Program Fixpoint run_write_requests (ac0 : assemblycache) (reqs : list writequeueentity) (res : list writequeueresult) : (list writequeueresult * assemblycache) :=
+Program Fixpoint run_write_requests (ac0 : assemblycache) (reqs : list writequeueentity) (res : list writequeueresult)
+                                  : (list writequeueresult * assemblycache) :=
     match reqs with
     | nil => (res, ac0)
     | h :: r =>
         let env := Environment.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 := aid env.(cur_assembly); qapos := apos env.(cur_assembly); qrlen := buffer_len h.(qbuffer) |} |} :: res)
+        run_write_requests ac1 r ({| writerequest := h;
+                                     wresult := {| qaid := env.(cur_assembly).(aid); qapos := env.(cur_assembly).(apos);
+                                                   qrlen := buffer_len h.(qbuffer) |} |} :: res)
     end.
 
 
@@ -189,7 +192,7 @@ Program Definition iterate_read_queue (ac0 : assemblycache) : (list readqueueres
         let aid := h.(qaid) in
         let sel := List.filter (fun e => String.eqb e.(qaid) aid) r in
         let ac1 := {| acenvs := ac0.(acenvs); acsize := ac0.(acsize); acwriteenv := ac0.(acwriteenv); acconfig := ac0.(acconfig);
-                      acreadq := {| rqueue := List.filter (fun e => negb (String.eqb e.(qaid) aid)) r; rqueuesz := rqueuesz ac0.(acreadq) |};
+                      acreadq := {| rqueue := List.filter (fun e => negb (String.eqb e.(qaid) aid)) r; rqueuesz := ac0.(acreadq).(rqueuesz) |};
                       acwriteq := ac0.(acwriteq)|} in
         run_read_requests ac1 (h :: sel) nil
     end.
@@ -222,15 +225,15 @@ Program Definition close (ac0 : assemblycache) : assemblycache :=
 
 Section Validation.
 
-(* the assembly with id "aid_found" exists and can be restored *)
-Axiom env_for_known_aid : forall e c,
+(* 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);
         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 env_none_default : forall a c,
+Axiom db_env_none_default : forall a c,
     let env := initial_environment c in
     try_restore_assembly c a = None.
 
@@ -239,16 +242,17 @@ Lemma emptyread_id : forall c k, let ac := prepare_assemblycache c k in iterate_
 Proof.
     intros.
     unfold iterate_read_queue. simpl.
-    trivial.
+    reflexivity.
 Qed.
 
 Lemma emptywrite_id : forall c k, let ac := prepare_assemblycache c k in iterate_write_queue ac = (nil, ac).
 Proof.
     intros.
     unfold iterate_write_queue. simpl.
-    trivial.
+    reflexivity.
 Qed.
 
+Section Unfinished.
 Axiom run_read_requests_same_length : forall ac reqs,
     let len1 := List.length reqs in
     let (lres, _) := run_read_requests ac reqs nil in
@@ -271,7 +275,8 @@ Proof.
     induction reqs. simpl.
     - reflexivity.
     - apply run_read_requests_same_length. 
-Qed.
+Abort.
+End Unfinished.
 
 (* running the read queue with a single read request,
    returns exactly one result *)
@@ -288,7 +293,7 @@ Proof.
     unfold filter. simpl.
     unfold ensure_assembly. simpl.
     set (e0 := initial_environment Config).
-    rewrite env_for_known_aid with (e := e0).
+    rewrite db_env_for_known_aid with (e := e0).
     auto.
 Qed.
 
@@ -306,12 +311,12 @@ Proof.
     intro Config.
     unfold ensure_assembly. simpl.
     set (e0 := initial_environment Config).
-    rewrite env_for_known_aid with (e := e0).
+    rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. reflexivity.
 Qed.
 
-Axiom aid_of_initial_environment : forall c,
-    aid (cur_assembly (initial_environment c)) = "".
+(* Axiom aid_of_initial_environment : forall c,
+    aid (cur_assembly (initial_environment c)) = "". *)
 
 Example second_of3_env_for_not_filled_cache : forall c,
     let ac0 := prepare_assemblycache c 3 in
@@ -335,7 +340,7 @@ Proof.
     intro Config.
     unfold ensure_assembly. simpl.
     set (e0 := initial_environment Config).
-    rewrite env_for_known_aid with (e := e0).
+    rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. simpl. reflexivity.
 Qed.
 
@@ -361,7 +366,7 @@ Proof.
     intro Config.
     unfold ensure_assembly. simpl.
     set (e0 := initial_environment Config).
-    rewrite env_for_known_aid with (e := e0).
+    rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. simpl. reflexivity.
 Qed.
 
@@ -390,7 +395,7 @@ Proof.
     intro Config.
     unfold ensure_assembly. simpl.
     set (e0 := initial_environment Config).
-    rewrite env_for_known_aid with (e := e0).
+    rewrite db_env_for_known_aid with (e := e0).
     unfold set_envs. simpl. reflexivity.
 Qed.
 

theories/BackupPlanner.v

@@ -4,15 +4,10 @@
 
 (** modeling backup of multiple files to LXR *)
 
-Module Export BackupPlanner.
-
-(** imports *)
 From Coq Require Import Strings.String Strings.Byte Lists.List Lia.
 (* Require Import Arith Number. *)
 Require Import ZArith NArith PArith.
 From Coq Require Import NArith.BinNat Program.Wf.
-Open Scope positive_scope.
-Open Scope N_scope.
 
 From LXR Require Import Assembly.
 From LXR Require Import Buffer.
@@ -21,6 +16,10 @@ From LXR Require Import Conversion.
 From LXR Require Import Environment.
 From LXR Require Import Filesupport.
 
+Module Export BackupPlanner.
+
+Open Scope positive_scope.
+Open Scope N_scope.
 Open Scope string_scope.
 
 Record fileblock : Type :=
@@ -77,7 +76,7 @@ End prepare_blocks.
 Section analyse_file.
 
 Variable nchunks : positive.
-Definition max_block_size : N := 131072.
+Definition max_block_size : N := 128 * 1024 (* 131072 *).
 
 Definition analyse_file (afree_p : N) (anum_p : positive) (fn : string) : (positive * N) * fileblockinformation :=
   (* Printf.printf "backup %s\n" fn; *)

theories/Buffer.v

@@ -2,6 +2,11 @@
       e L y K s e e R
 *)
 
+From Coq Require Import Strings.String.
+Require Import NArith.
+
+From LXR Require Import Conversion.
+
 Module Export Buffer.
 
 (**
@@ -13,12 +18,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-From Coq Require Import Strings.String.
-Require Import NArith.
 Open Scope N_scope.
 
-From LXR Require Import Conversion.
-
 Inductive EncryptionState := Plain | Encrypted.
 
 Axiom cstdio_buffer : Type.

theories/Configuration.v

@@ -2,13 +2,13 @@
       e L y K s e e R
 *)
 
-Module Export Configuration.
-
 Require Import NArith PArith.
 From Coq Require Import Strings.String.
 
 From LXR Require Import Nchunks.
 
+Module Export Configuration.
+
 Record configuration : Type :=
     mkconfiguration
         { config_nchunks : Nchunks.t

theories/Conversion.v

@@ -2,15 +2,15 @@
       e L y K s e e R
 *)
 
-Module Export Conversion.
-
 (**
  Module: Conversion
  Description: conversion functions
  *)
 
 From Coq Require Import NArith.BinNat.
 
+Module Export Conversion.
+
 Definition pos2N (p : positive) : N :=
     Npos p.