From 46f0c3cc102b325811a025382137c5a0e63e42c9 Mon Sep 17 00:00:00 2001 From: Guilhem Mizrahi Date: Tue, 5 May 2026 14:41:02 +0200 Subject: [PATCH] Rework ArrayCast / ArrayWord / SubArray th + extraction - fix bugs (invalid scaling) in ArrayCast - proper clone chain szo that no top-level theories is duplicated --- compiler/src/toEC.ml | 47 ++++++++++++++++---- eclib/JWord.ec | 6 +++ eclib/JWord_array.ec | 102 ++++++++++++++++++++++++++++++++++++------- 3 files changed, 130 insertions(+), 25 deletions(-) diff --git a/compiler/src/toEC.ml b/compiler/src/toEC.ml index 3fabf2f233..6af4fd414d 100644 --- a/compiler/src/toEC.ml +++ b/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 @[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 "@[from Jasmin require import JWord JWord_array.@ @ "; Format.fprintf fmt "@[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@[ @[%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 "@[from Jasmin require import JWord JWord_array.@ @ "; + Format.fprintf fmt "@[require import %s.@ " arrayb; + Format.fprintf fmt "@[require import %s.@ " warraybwb; Format.fprintf fmt "@[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@[ @[%a@ proof * by done@]@].@]@." + (if aligned then "Aligned" else "") (fmt_array_theory (ArrayAccessCast s)) fmt_insts s diff --git a/eclib/JWord.ec b/eclib/JWord.ec index 3e4d9e057d..bd20666b51 100644 --- a/eclib/JWord.ec +++ b/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 diff --git a/eclib/JWord_array.ec b/eclib/JWord_array.ec index 3b27043c68..1774a57b9e 100644 --- a/eclib/JWord_array.ec +++ b/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.