Rework ArrayCast / ArrayWord / SubArray th + extraction

compiler/src/toEC.ml

@@ -475,6 +475,8 @@ module Env: EnvT = struct
     env.array_theories := Sarraytheory.add (SubArrayCast {sizews; sizewb; sizes; sizeb}) !(env.array_theories)
 
   let add_ArrayAccessCast env sizews sizewb sizeb =
+    add_Array env sizeb;
+    add_WArray env (sizeb * sizewb);
     add_ArrayWords env sizewb sizeb;
     env.array_theories := Sarraytheory.add (ArrayAccessCast {sizews; sizewb; sizeb}) !(env.array_theories)
 
@@ -792,24 +794,37 @@ let fmt_warray_decl fmt i =
 
 let fmt_op fmt (op_name, v) = Format.fprintf fmt "op %s <- %i" op_name v
 
-let fmt_the fmt (th, v) = Format.fprintf fmt "theory %s <- %s" th v
+let fmt_the_fmt fmt (th, pp, v) = Format.fprintf fmt "theory %s <- %a" th pp v
+
+let fmt_the fmt (th, v) =
+  fmt_the_fmt fmt (th, Format.pp_print_string, v)
 
 let fmt_th fmt (th, v) = Format.fprintf fmt "theory %s <= %s" th v
 
+let fmt_word_packing (fmt : Format.formatter) ((s, b) : int * int) =
+  Format.fprintf fmt "W%du%d {@\n  @[<v 2>rename @[ \
+      @\n \"'Ru'S\" as \"%du%d\" \
+      @\n \"'R\" as \"%d\" \
+      @\n \"'S\" as \"%d\" \
+      @\n \"'B\" as \"%d\" \
+    @]@]@\n}"
+    s b s b s b (s * b)
+
 let fmt_arraywords_decl fmt (aw: arraywords) =
   let arrayn = Format.sprintf "Array%i" aw.sizea in
   let warrayn = Format.sprintf "WArray%i" (aw.sizew*aw.sizea) in
   let fmt_insts fmt (aw: arraywords) =
-    Format.fprintf fmt "%a,@ %a,@ %a,@ %a,@ %a"
+    Format.fprintf fmt "%a,@ %a,@ %a,@ %a,@ %a,@ %a"
     fmt_op ("sizeW", aw.sizew)
     fmt_op ("sizeA", aw.sizea)
-    fmt_th ("Word", Format.sprintf "W%i" (8*aw.sizew))
-    fmt_th ("ArrayN", arrayn)
-    fmt_th ("WArrayN", warrayn)
+    fmt_the ("Word", Format.sprintf "W%i" (8*aw.sizew))
+    fmt_the ("ArrayN", arrayn)
+    fmt_the ("WArrayN", warrayn)
+    fmt_the_fmt ("Wu8", fmt_word_packing, (aw.sizew, 8))
   in
   Format.fprintf fmt "@[<v>from Jasmin require import JWord JWord_array.@ @ ";
   Format.fprintf fmt "@[<v>require import %s %s.@ @ " arrayn warrayn;
-  Format.fprintf fmt "clone export ArrayWords as %s  with @[%a@].@]@."
+  Format.fprintf fmt "clone export ArrayWords as %s with @\n@[  @[<v 0>%a@ proof * by done@]@].@]@."
     (fmt_array_theory (ArrayWords aw))
     fmt_insts aw
 
@@ -869,18 +884,32 @@ let fmt_subarraycast_decl fmt (s: subarraycast) =
 
 let fmt_arrayaccesscast_decl fmt (s: arrayaccesscast) =
   let arraywb = fmt_array_theory (ArrayWords {sizew=s.sizewb; sizea=s.sizeb}) in
+  let arrayb = fmt_array_theory (Array s.sizeb) in
+  let warraybwb = fmt_array_theory (WArray (s.sizeb * s.sizewb)) in
+  let aligned = (s.sizewb mod s.sizews) = 0 in
   let fmt_insts fmt (s: arrayaccesscast) =
-    Format.fprintf fmt "%a,@ %a,@ %a,@ %a,@ %a,@ %a"
+    Format.fprintf fmt "%a,@ %a,@ %a,@ %a,@ %a,@ %a,@ %a,@ %a,@ %a,@ %a%t"
     fmt_op ("sizeWS", s.sizews)
     fmt_op ("sizeWB", s.sizewb)
     fmt_op ("sizeB", s.sizeb)
     fmt_the ("WordS", Format.sprintf "W%i" (8*s.sizews))
     fmt_the ("WordB", Format.sprintf "W%i" (8*s.sizewb))
-    fmt_th ("ArrayWordsB", arraywb)
+    fmt_the ("ArrayN", Format.sprintf "Array%i" s.sizeb)
+    fmt_the ("WArrayN", Format.sprintf "WArray%i" (s.sizeb*s.sizewb))
+    fmt_the ("ArrayWordsB", arraywb)
+    fmt_the_fmt ("WSu8", fmt_word_packing, (s.sizews, 8))
+    fmt_the_fmt ("WBu8", fmt_word_packing, (s.sizewb, 8))
+    (fun fmt ->
+       if aligned then
+         Format.fprintf fmt ",@ %a"
+         fmt_the_fmt ("WSuB", fmt_word_packing, (s.sizewb / s.sizews, 8*s.sizews)))
   in
   Format.fprintf fmt "@[<v>from Jasmin require import JWord JWord_array.@ @ ";
+  Format.fprintf fmt "@[<v>require import %s.@ " arrayb;
+  Format.fprintf fmt "@[<v>require import %s.@ " warraybwb;
   Format.fprintf fmt "@[<v>require import %s.@ @ " arraywb;
-  Format.fprintf fmt "clone export ArrayAccessCast as %s  with @[%a@].@]@."
+  Format.fprintf fmt "clone export ArrayAccessCast%s as %s with @\n@[  @[<v 0>%a@ proof * by done@]@].@]@."
+    (if aligned then "Aligned" else "")
     (fmt_array_theory (ArrayAccessCast s))
     fmt_insts s
 

eclib/JWord.ec

@@ -2618,6 +2618,12 @@ abstract theory W_WS.
 
 end W_WS.
 
+clone export W_WS as W1u8 with
+  op sizeS <- W8.size, op sizeB <- W8.size, op r <- 1,
+  theory WS <- W8, theory WB <- W8
+  proof gt0_r by done, sizeBrS by done
+  rename [op, lemma] "'Ru'S" as "1u8" "'R" as "1" "'S" as "8" "'B" as "8".
+
 clone export W_WS as W2u8 with
   op sizeS <- W8.size, op sizeB <- W16.size, op r <- 2,
   theory WS <- W8, theory WB <- W16

eclib/JWord_array.ec

@@ -290,8 +290,8 @@ abstract theory ArrayWords.
 
   (* Conversion between WArrayN.t and Word.t ArrayN.t *)
   clone W_WS as Wu8 with
-    op sizeS <= W8.size, op sizeB <= W8.size*sizeW, op r <= sizeW,
-    theory WS <= W8, theory WB <= Word
+    op sizeS <- W8.size, op sizeB <- W8.size*sizeW, op r <- sizeW,
+    theory WS <- W8, theory WB <- Word
     proof gt0_r by apply gt0_sizeW, sizeBrS by rewrite mulzC.
 
   (* direct means offset in bytes, not in words *)
@@ -401,34 +401,104 @@ abstract theory ArrayAccessCast.
     op size <- 8 * sizeWB
     proof gt0_size by rewrite pmulr_rgt0 1:// gt0_sizeWB.
 
-  clone ArrayWords as ArrayWordsB with
-    op sizeW <- sizeWB, op sizeA <- sizeB, theory Word <- WordB
-    proof gt0_sizeW by apply gt0_sizeWB, gt0_sizeA by apply gt0_sizeB.
+  clone PolyArray as ArrayN
+    with op size <- sizeB
+    proof ge0_size by apply/ltzW/gt0_sizeB.
+
+  clone import WArray as WArrayN with
+    op size <- sizeWB * sizeB
+    proof ge0_size by smt(gt0_sizeWB gt0_sizeB).
 
   clone W_WS as WSu8 with
-    op sizeS <= W8.size, op sizeB <= W8.size*sizeWS, op r <= sizeWS,
-    theory WS <= W8, theory WB <= WordS
+    op sizeS <- W8.size, op sizeB <- W8.size*sizeWS, op r <- sizeWS,
+    theory WS <- W8, theory WB <- WordS
     proof gt0_r by apply gt0_sizeWS, sizeBrS by rewrite mulzC.
 
+  clone W_WS as WBu8 with
+    op sizeS <- W8.size, op sizeB <- W8.size*sizeWB, op r <- sizeWB,
+    theory WS <- W8, theory WB <- WordB
+    proof gt0_r by apply gt0_sizeWB, sizeBrS by rewrite mulzC.
 
-  op get_cast_direct (a: WordB.t ArrayWordsB.ArrayN.t) (i: int) =
+  clone ArrayWords as ArrayWordsB with
+    op sizeW <- sizeWB, op sizeA <- sizeB, theory Word <- WordB,
+    theory ArrayN <- ArrayN, theory WArrayN <- WArrayN, theory Wu8 <- WBu8
+    proof gt0_sizeW by apply gt0_sizeWB, gt0_sizeA by apply gt0_sizeB.
+
+  op get_cast_direct (a: WordB.t ArrayN.t) (i: int) =
     WSu8.pack'R_t (
-      WSu8.Pack.init (fun j => ArrayWordsB.WArrayN."_.[_]" (ArrayWordsB.of_word_array a) (i+j))
+      WSu8.Pack.init (fun j => WArrayN."_.[_]" (ArrayWordsB.of_word_array a) (i+j))
     ).
 
-  op set_cast_direct (a: WordB.t ArrayWordsB.ArrayN.t) (i: int) (b: WordS.t) =
+  op set_cast_direct (a: WordB.t ArrayN.t) (i: int) (b: WordS.t) =
     ArrayWordsB.to_word_array (
-      ArrayWordsB.WArrayN.init (fun j =>
+      WArrayN.init (fun j =>
         if i <= j < i + sizeWS then
           WSu8.\bits'S b (j - i)
         else
-          ArrayWordsB.WArrayN."_.[_]" (ArrayWordsB.of_word_array a) j
+          WArrayN."_.[_]" (ArrayWordsB.of_word_array a) j
         )
       ).
 
-  op get_cast (a: WordB.t ArrayWordsB.ArrayN.t) (i: int) =
-    get_cast_direct a (sizeWB*i).
+  op get_cast (a: WordB.t ArrayN.t) (i: int) =
+    get_cast_direct a (sizeWS*i).
 
-  op set_cast (a: WordB.t ArrayWordsB.ArrayN.t) (i: int) (b: WordS.t) =
-    set_cast_direct a (sizeWB*i) b.
+  op set_cast (a: WordB.t ArrayN.t) (i: int) (b: WordS.t) =
+    set_cast_direct a (sizeWS*i) b.
 end ArrayAccessCast.
+
+theory ArrayAccessCastAligned.
+  clone include ArrayAccessCast.
+
+  import ArrayN.
+
+  axiom aligned : sizeWS %| sizeWB.
+
+  clone import W_WS as WSuB with
+    op sizeS <- 8 * sizeWS,
+    op sizeB <- 8 * sizeWB,
+    op r <- sizeWB %/ sizeWS,
+    theory WS <- WordS,
+    theory WB <- WordB
+    proof gt0_r, sizeBrS.
+
+  realize gt0_r.
+  proof. smt(gt0_sizeWS gt0_sizeWB aligned). qed.
+
+  realize sizeBrS.
+  proof. by rewrite mulrCA divzK // aligned. qed.
+
+  lemma get_castiE (a : WordB.t ArrayN.t) (i : int) :
+      0 <= i < sizeB * (sizeWB %/ sizeWS)
+   =>   get_cast a i
+      = a.[i %/ (sizeWB %/ sizeWS)] \bits'S (i %% (sizeWB %/ sizeWS)).
+  proof.
+  have ? := gt0_sizeWS; have ? := gt0_sizeWB; have ? := gt0_sizeB.
+  move=> rgi; rewrite /get_cast.
+  rewrite /get_cast_direct /of_word_array.
+  apply: WSu8.wordP => j rgj.
+  apply: W8.ext_eq => k rgk.
+  rewrite !WSu8.bits'SiE // !WSuB.bits'SiE ~-1:/#.
+  rewrite WSu8.pack'RwE 1:/#.
+  rewrite WSu8.Pack.initiE 1:/# /=.
+  rewrite WArrayN.initiE /=.
+  - split=> [|_]; first smt().
+    rewrite divzMDl // pdiv_small //=.
+    case: rgi => ?; rewrite ltzE -ler_subr_addr.
+    by rewrite -(ler_pmul2l sizeWS) //#.
+  rewrite WBu8.bits'SiE 1:/#; congr; first congr.
+  - rewrite divzMDl // [k %/ 8]pdiv_small //=.
+    case/dvdzP: aligned rgi => q -> rgi.
+    by rewrite [q*_]mulrC divzMr //#.
+  - rewrite divzMDl // [k %/ 8]pdiv_small //=.
+    rewrite modzMDl // [k %% 8]pmod_small //=.
+    rewrite addrA; congr.
+    rewrite mulrA mulrAC -mulrDl; congr.
+    case/dvdzP: aligned rgi => q ->.
+    rewrite mulzK 1:/# => rgi.
+    rewrite -modzDml [sizeWS * i]mulrC -mulz_modl //.
+    rewrite pmod_small //; split=> [|_]; first smt().
+    rewrite {2}[q](_ : q = q - 1 + 1) //.
+    rewrite mulrDl &(ler_lt_add) -1:/#.
+    by rewrite &(ler_pmul2r) //#.
+  qed.
+end ArrayAccessCastAligned.