Merge branch 'assembly_16_random_byte_prefix'

elykseer-utils/utils.ml

@@ -22,7 +22,7 @@ let c2j c = "{ \"config_nchunks\": \"" ^ (string_of_int @@ Conversion.n2i @@ Nch
           ^ ", \"my_id\": " ^ (string_of_int @@ Conversion.n2i @@ c.my_id) ^ " }"
 
 let pluralise s m =
-  let post = if m > 1 then "s" else "" in
-  s^post
+  if m > 1 then s^"s" else s
+
 let pluralise2 s1 s2 m =
   if m > 1 then s2 else s1

helper.ml

@@ -52,5 +52,10 @@ let load_chunk_from_path fp =
     end
   else None
 
-let cpp_mk_key256 () = Elykseer_crypto.Key256.mk () |> Elykseer_crypto.Key256.to_hex
-let cpp_mk_key128 () = Elykseer_crypto.Key128.mk () |> Elykseer_crypto.Key128.to_hex
+let mk_key256 () = Elykseer_crypto.Key256.mk () |> Elykseer_crypto.Key256.to_hex
+let mk_key128 () = Elykseer_crypto.Key128.mk () |> Elykseer_crypto.Key128.to_hex
+
+let ranbuf128 () =
+  let r = Elykseer_crypto.Key128.mk () |> Elykseer_crypto.Key128.to_bytes in
+  let b = Cstdio.File.Buffer.create (16) in
+  Cstdio.File.Buffer.copy_string r b 16; b

lxr.ml

@@ -455,6 +455,18 @@ let rec seq start = function
 | O -> []
 | S len0 -> start :: (seq (S start) len0)
 
+type 't settable =
+  't -> 't
+  (* singleton inductive, whose constructor was Build_Settable *)
+
+type ('r, 't) setter = ('t -> 't) -> 'r -> 'r
+
+(** val set :
+    ('a1 -> 'a2) -> ('a1, 'a2) setter -> ('a2 -> 'a2) -> 'a1 -> 'a1 **)
+
+let set _ setter0 =
+  setter0
+
 module Conversion =
  struct
   (** val pos2N : positive -> n **)
@@ -716,6 +728,15 @@ module Buffer =
 
   let decrypt =
     cpp_decrypt_buffer
+
+  (** val cpp_ranbuf128 : unit -> cstdio_buffer **)
+
+  let cpp_ranbuf128 = fun () -> Helper.ranbuf128 ()
+
+  (** val ranbuf128 : unit -> BufferPlain.buffer_t **)
+
+  let ranbuf128 _ =
+    let rb = cpp_ranbuf128 () in BufferPlain.from_buffer rb
  end
 
 module Configuration =
@@ -816,6 +837,11 @@ module Assembly =
   let apos a =
     a.apos
 
+  (** val etaX : assemblyinformation settable **)
+
+  let etaX x =
+    { nchunks = x.nchunks; aid = x.aid; apos = x.apos }
+
   type keyinformation = { ivec : string; pkey : string; localid : n;
                           localnchunks : positive }
 
@@ -876,8 +902,13 @@ module Assembly =
         Buffer.BufferPlain.buffer_create
           (N.mul chunksize_N (Nchunks.to_N chunks))
       in
+      let rb = Buffer.ranbuf128 () in
+      let nb =
+        Buffer.BufferPlain.copy_sz_pos rb N0 (Npos (XO (XO (XO (XO XH))))) b
+          N0
+      in
       ({ nchunks = chunks; aid = (Utilities.rnd256 c.Configuration.my_id);
-      apos = N0 }, b)
+      apos = nb }, b)
    end
 
   module AssemblyEncrypted =
@@ -951,7 +982,12 @@ module Assembly =
       (AssemblyPlainWritable.coq_H * AssemblyPlainWritable.coq_B) option **)
 
   let decrypt a b ki =
-    let a' = { nchunks = a.nchunks; aid = a.aid; apos = N0 } 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) }))
+        (const N0) a
+    in
     let bdec = Buffer.decrypt (id_buffer_t_from_enc b) ki.ivec ki.pkey in
     let b' = id_assembly_plain_buffer_t_from_buf bdec in Some (a', b')
 
@@ -1015,7 +1051,12 @@ module Assembly =
            else nread
          | None -> nread)) cidlist N0
     in
-    let a' = { nchunks = a.nchunks; aid = aid0; apos = nread } 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) }))
+        (const nread) a
+    in
     let b' = id_enc_from_buffer_t b in
     if N.eqb nread blen then Some (a', b') else None
 
@@ -1061,16 +1102,18 @@ module Assembly =
       AssemblyPlainFull.coq_H * AssemblyPlainFull.coq_B **)
 
   let finish a b =
-    ({ nchunks = a.nchunks; aid = a.aid; apos = a.apos },
-      (id_assembly_full_buffer_from_writable 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' = { nchunks = a.nchunks; aid = a.aid; apos =
-      (assemblysize a.nchunks) }
+    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')
@@ -1133,8 +1176,11 @@ module Assembly =
     let bi = { blockid = XH; bchecksum = chksum; blocksize = nwritten;
       filepos = fpos; blockaid = a.aid; blockapos = apos_n }
     in
-    let a' = { nchunks = a.nchunks; aid = a.aid; apos =
-      (N.add apos_n nwritten) }
+    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)
 
@@ -1162,18 +1208,6 @@ module Assembly =
     else None
  end
 
-type 't settable =
-  't -> 't
-  (* singleton inductive, whose constructor was Build_Settable *)
-
-type ('r, 't) setter = ('t -> 't) -> 'r -> 'r
-
-(** val set :
-    ('a1 -> 'a2) -> ('a1, 'a2) setter -> ('a2 -> 'a2) -> 'a1 -> 'a1 **)
-
-let set _ setter0 =
-  setter0
-
 module Environment =
  struct
   type environment = { cur_assembly : Assembly.AssemblyPlainWritable.coq_H;
@@ -1284,11 +1318,11 @@ module Environment =
 
   (** val cpp_mk_key256 : unit -> string **)
 
-  let cpp_mk_key256 = fun () -> Helper.cpp_mk_key256 ()
+  let cpp_mk_key256 = fun () -> Helper.mk_key256 ()
 
   (** val cpp_mk_key128 : unit -> string **)
 
-  let cpp_mk_key128 = fun () -> Helper.cpp_mk_key128 ()
+  let cpp_mk_key128 = fun () -> Helper.mk_key128 ()
 
   (** val finalise_assembly : environment -> environment **)
 

lxr.mli

@@ -135,6 +135,14 @@ val filter : ('a1 -> bool) -> 'a1 list -> 'a1 list
 
 val seq : nat -> nat -> nat list
 
+type 't settable =
+  't -> 't
+  (* singleton inductive, whose constructor was Build_Settable *)
+
+type ('r, 't) setter = ('t -> 't) -> 'r -> 'r
+
+val set : ('a1 -> 'a2) -> ('a1, 'a2) setter -> ('a2 -> 'a2) -> 'a1 -> 'a1
+
 module Conversion :
  sig
   val pos2N : positive -> n
@@ -232,6 +240,10 @@ module Buffer :
 
   val decrypt :
     BufferEncrypted.buffer_t -> string -> string -> BufferPlain.buffer_t
+
+  val cpp_ranbuf128 : unit -> cstdio_buffer
+
+  val ranbuf128 : unit -> BufferPlain.buffer_t
  end
 
 module Configuration :
@@ -280,6 +292,8 @@ module Assembly :
 
   val apos : assemblyinformation -> n
 
+  val etaX : assemblyinformation settable
+
   type keyinformation = { ivec : string; pkey : string; localid : n;
                           localnchunks : positive }
 
@@ -395,14 +409,6 @@ module Assembly :
     Buffer.BufferPlain.buffer_t option
  end
 
-type 't settable =
-  't -> 't
-  (* singleton inductive, whose constructor was Build_Settable *)
-
-type ('r, 't) setter = ('t -> 't) -> 'r -> 'r
-
-val set : ('a1 -> 'a2) -> ('a1, 'a2) setter -> ('a2 -> 'a2) -> 'a1 -> 'a1
-
 module Environment :
  sig
   type environment = { cur_assembly : Assembly.AssemblyPlainWritable.coq_H;

theories/Assembly.v

@@ -2,10 +2,12 @@
       e L y K s e e R
 *)
 
-From Coq Require Import Strings.String .
+From Coq Require Import Strings.String Program.Basics.
 Require Import ZArith NArith PArith.
 From Coq Require Import NArith.BinNat.
 
+From RecordUpdate Require Import RecordUpdate.
+
 From LXR Require Import Nchunks Buffer Configuration Conversion Utilities.
 
 Module Export Assembly.
@@ -40,6 +42,8 @@ Record assemblyinformation : Type :=
         ; aid : aid_t
         ; apos : N }.
 
+#[export] Instance etaX : Settable _ := settable! mkassembly <nchunks; aid; apos>.
+
 Record keyinformation : Type :=
     mkkeyinformation
         { ivec : string
@@ -66,7 +70,9 @@ Module AssemblyPlainWritable : ASS.
     Definition create (c : configuration) : H * B :=
         let chunks := config_nchunks c in
         let b := BufferPlain.buffer_create (chunksize_N * Nchunks.to_N chunks) in
-        (mkassembly chunks (Utilities.rnd256 (my_id c)) 0, b).
+        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.
 
 Module AssemblyEncrypted : ASS.
@@ -100,7 +106,7 @@ Section Code_Encrypted.
 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) :=
-    let a' := mkassembly (nchunks a) (aid a) 0 in
+    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
     Some (a', b').
@@ -130,7 +136,7 @@ Program Definition recall (c : configuration) (a : AssemblyEncrypted.H) : option
                     )
                     cidlist
                     0 in
-    let a' := mkassembly (nchunks a) aid nread in
+    let a' := set apos (const nread) a in
     let b' := id_enc_from_buffer_t b in
     if N.eqb nread blen
     then Some (a', b')
@@ -160,11 +166,11 @@ Axiom id_assembly_enc_buffer_t_from_buf : BufferEncrypted.buffer_t -> AssemblyEn
 Axiom id_assembly_full_buffer_from_writable : AssemblyPlainWritable.B -> AssemblyPlainFull.B.
 
 Program Definition finish (a : AssemblyPlainWritable.H) (b : AssemblyPlainWritable.B) : (AssemblyPlainFull.H * AssemblyPlainFull.B) :=
-    ( mkassembly (nchunks a) (aid a) (apos a)
+    ( 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' := mkassembly (nchunks a) (aid a) (assemblysize (nchunks a)) in
+    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').
@@ -193,7 +199,7 @@ Program Definition backup (a : AssemblyPlainWritable.H) (b : AssemblyPlainWritab
                ; filepos   := fpos
                ; blockaid  := aid a
                ; blockapos := apos_n |} in
-    let a' := {| nchunks := nchunks a; aid := aid a; apos := apos_n + nwritten |} in
+    let a' := set apos (fun ap => ap + nwritten) a in
     (a', bi).
 
 (** restore: copy buffer from an assembly

theories/Buffer.v

@@ -69,4 +69,9 @@ Axiom cpp_decrypt_buffer : BufferEncrypted.buffer_t -> string -> string -> Buffe
 Definition decrypt (bin : BufferEncrypted.buffer_t) (iv : string) (pw : string) : BufferPlain.buffer_t :=
   cpp_decrypt_buffer bin iv pw.
 
+Axiom cpp_ranbuf128 : unit -> cstdio_buffer.
+Program Definition ranbuf128 (_ : unit) : BufferPlain.buffer_t :=
+  let rb := cpp_ranbuf128 tt in
+  BufferPlain.from_buffer rb.
+
 End Buffer.

theories/MakeML.v

@@ -140,8 +140,9 @@ Extract Constant id_assembly_full_buffer_from_writable => "fun b -> Helper.cpp_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".
 
-Extract Constant cpp_mk_key256 => "fun () -> Helper.cpp_mk_key256 ()".
-Extract Constant cpp_mk_key128 => "fun () -> Helper.cpp_mk_key128 ()".
+Extract Constant cpp_mk_key256 => "fun () -> Helper.mk_key256 ()".
+Extract Constant cpp_mk_key128 => "fun () -> Helper.mk_key128 ()".
+Extract Constant cpp_ranbuf128 => "fun () -> Helper.ranbuf128 ()".
 
 Extract Constant assembly_add_content => (* BufferPlain.buffer_t -> N -> N -> AssemblyPlainWritable.B -> N. *)
    "