final fixes

proof/correctness/MLKEM_keccak_ref.ec

@@ -76,60 +76,3 @@ axiom sha_g buf:
           res = Array64.init (fun k => if k < 32 then bytes.`1.[k] else bytes.`2.[k-32])] = 1%r.
 
 
-(*
-axiom sha3_512_33_64 buf seed : 
-   phoare [Jkem.M(Jkem.Syscall)._sha3512_33 : 
-               arg = (buf,seed) ==>
-               Array32.init(fun i => res.[i]) = (SHA3_512_33_64 seed).`1 /\
-               Array32.init(fun i => res.[32 + i]) = (SHA3_512_33_64 seed).`2  ] = 1%r.
-
-axiom shake_absorb (seed : W8.t Array34.t) state : 
-   phoare [Jkem.M(Jkem.Syscall)._shake128_absorb34 : 
-               arg = (state,seed) ==>
-               res = SHAKE128_ABSORB_34 
-                         (Array32.init (fun k => seed.[k])) (seed.[32]) (seed.[33]) ] = 1%r.
-
-axiom shake_squeeze buf state : 
-   phoare [Jkem.M(Jkem.Syscall)._shake128_squeezeblock : 
-               arg = (state,buf) ==>
-               res = SHAKE128_SQUEEZE_168 state ] = 1%r.
-
-axiom shake256_33_128 buf seed : 
-   phoare [Jkem.M(Jkem.Syscall)._shake256_128_33 : 
-               arg = (buf,seed) ==>
-               res = SHAKE256_33_128 (Array32.init (fun i => seed.[i])) seed.[32] ] = 1%r.
-
-
-axiom pkH_sha mem _ptr inp: 
-    phoare [Jkem.M(Jkem.Syscall)._isha3_256 :
-          arg = (inp,W64.of_int _ptr,W64.of_int (3*384+32)) /\
-          valid_ptr _ptr 1184 /\
-          Glob.mem = mem
-          ==> 
-          Glob.mem = mem /\
-          res = SHA3_256_1184_32
-            (Array1152.init (fun k =>  mem.[_ptr+k]),
-            (Array32.init (fun k => mem.[_ptr+1152+k])))] = 1%r.
-
-axiom j_shake mem _pout _pin1 _pin2: 
-    phoare [Jkem.M(Syscall)._shake256_1120_32  :
-          arg = (W64.of_int _pout,W64.of_int _pin1,W64.of_int _pin2) /\
-          valid_ptr _pout 32 /\
-          valid_ptr _pin1 32 /\
-          valid_ptr _pin2 1088 /\
-          Glob.mem = mem
-          ==> 
-          touches Glob.mem mem _pout 32 /\
-          (Array32.init (fun k =>  Glob.mem.[_pout+k])) = 
-             SHAKE_256_1120_32 (Array32.init (fun k => mem.[_pin1+k])) 
-                            (Array960.init (fun k => mem.[_pin2+k]), Array128.init (fun k => mem.[_pin2+960+k])) ] = 1%r.
-
-axiom sha_g buf inp: 
-    phoare [Jkem.M(Jkem.Syscall)._sha3_512_64 :
-          arg = (inp,buf)
-          ==> 
-          let bytes = SHA3_512_64_64 (Array32.init (fun k => buf.[k])) 
-                                     (Array32.init (fun k => buf.[k+32])) in
-          res = Array64.init (fun k => if k < 32 then bytes.`1.[k] else bytes.`2.[k-32])] = 1%r.
-
-*)

proof/correctness/avx2/MLKEM_KEM_avx2.ec

@@ -343,7 +343,7 @@ seq 13 4 : (#[/1:-2]post
   move => mm ii;do split => ???????; 1: smt().
   by rewrite /load_array32 tP => kk kkb; smt(Array32.initiE).
 wp; call (mlkem_correct_enc_0_avx2 mem _ctp _pkp).
-wp; ecall {1} (sha3_512A_A64_ph buf{1} kr{1}).
+wp; ecall {1} (sha3_512A_A64_ph buf{1}).
 wp; ecall {1} (sha3_256A_M1184_ph mem (_pkp)).
 seq 8 0 : (#pre /\ s_pkp{1} = pkp{1} /\ s_ctp{1} = ctp{1} /\  s_shkp{1} = shkp{1} /\ randomnessp{1} = Array32.init (fun i => buf{1}.[i])).
 + sp ; conseq />.

proof/correctness/avx2/MLKEM_Poly_avx2_proof.ec

@@ -3707,7 +3707,10 @@ proof.
     apply Array8.ext_eq => x x_i.
     rewrite f_def 1:x_i //= Array8.initiE 1:x_i //=.
 
-  smt().
+  have ->: k %% (15 - (linear_idx %% 32 + n) %% 16) = k %% 4 by smt().
+  move => ->; congr; congr; congr; congr. 
+   by congr; congr; smt(). 
+  smt(). 
 
   move => k k_lb k_ub.
 

proof/correctness/avx2/MLKEM_keccak_avx2.ec

@@ -684,6 +684,11 @@ qed.
 
 (*********************************************************************************)
 equiv sha3_512A_A64_eq:
+  M(Syscall)._sha3_512A_A64 ~ K._sha3_512A_A64
+ : ={arg} ==> ={res}
+by sim.
+
+equiv sha3_512A_A64_stack_eq:
   Jkem_avx2_stack.M._sha3_512A_A64 ~ K._sha3_512A_A64
  : ={arg} ==> ={res}
 by sim.
@@ -722,6 +727,36 @@ proof.
 by conseq sha3_512A_A64_ll (sha3_512A_A64_h' _in).
 qed.
 
+phoare sha3_512A_A64_ph inp: 
+ [ M(Syscall)._sha3_512A_A64
+ : arg.`2 = inp
+ ==>
+  let bytes = SHA3_512_64_64 (Array32.init (fun k => inp.[k])) 
+                             (Array32.init (fun k => inp.[k+32]))
+  in res = Array64.init (fun k => if k < 32
+                                  then bytes.`1.[k]
+                                  else bytes.`2.[k-32])
+ ] = 1%r.
+proof.
+conseq sha3_512A_A64_eq (sha3_512A_A64_ph' inp) => /> &m.
+ by exists arg{m} => />.
+rewrite -(Array64.of_listK W8.zero (SHA3_512 (to_list inp))).
+ by rewrite size_SQUEEZE1600 /#.
+move=> /Array64.to_list_inj ->.
+rewrite tP => i Hi.
+rewrite get_of_list 1:// initiE 1:// /= /SHA3_512_64_64 /=.
+rewrite {1}/Array64.to_list (mkseq_add _ 32 32) 1..2://.
+case: (i<32) => C.
+ rewrite initiE 1:/# /= (nth_take _ 32) 1..2:/#; congr; congr; congr.
+  apply eq_in_mkseq => k Hk /=.
+  by rewrite initiE 1:/#.
+ apply eq_in_mkseq => k Hk /=.
+ by rewrite initiE /#.
+rewrite get_of_list 1:/# nth_drop 1..2:/#; congr.
+ by congr; congr; apply eq_in_mkseq => k Hk /=; rewrite initiE /#.
+smt().
+qed.
+
 phoare sha3_512A_512A_A64_stack m hpk:
  [ Jkem_avx2_stack.M._sha3_512A_A64
  : 
@@ -746,7 +781,7 @@ conseq (: arg.`2 = _in
  have ->: in_0{m}.[i] = hpk.[i-32].
   by rewrite E2 initiE 1:/#.
  by rewrite get_of_list 1:// nth_cat size_to_list C /=.
-conseq sha3_512A_A64_eq (sha3_512A_A64_ph' _in) => />.
+conseq sha3_512A_A64_stack_eq (sha3_512A_A64_ph' _in) => />.
  by move=> &m ?; exists arg{m} => /=.
 move=> &m; rewrite /_in of_listK.
  by rewrite size_cat !size_to_list.