Prepare for alt-ergo 2.5 (#31)

This rewrites a few proofs to make them accepted by both versions of
alt-ergo: 2.4 & 2.5.

proof/correctness/MLKEM_InnerPKE.ec

@@ -1518,8 +1518,8 @@ seq 3 3 : (#pre /\ aT{2} = lift_matrix at{1} /\
 + inline AuxMLKEM.__gen_matrix; conseq />.
   seq 7 3 : (a{1}=aT{2});  last by auto => />;  smt(matrix_unlift).
   while (i0{1} = i{2} /\ 0<=i0{1}<=kvec /\ seed{1}=rho{2} /\ trans{1} /\
-         forall ii jj, 0<=ii<i0{1} => 0<= jj <3 => (a{1}.[ii,jj])%Matrix = (aT{2}.[ii,jj])%Matrix); last  
-          by auto => />; smt(eq_matrixP).
+         forall ii jj, 0<=ii<i0{1} => 0<= jj <3 => (a{1}.[ii,jj])%Matrix = (aT{2}.[ii,jj])%Matrix); last
+          by auto => /> *; apply: eq_matrixP; smt().
   wp; while (i0{1} = i{2} /\ j{1} = j{2} /\ 0<=i0{1}<kvec /\ 0<=j{1}<=kvec /\ seed{1}=rho{2} /\ trans{1} /\
          (forall ii jj, 0<=ii<i0{1} => 0<= jj <3 => (a{1}.[ii,jj])%Matrix = (aT{2}.[ii,jj])%Matrix) /\
          (forall jj, 0 <= jj <j{1} => (a{1}.[i0{1},jj])%Matrix = (aT{2}.[i0{1},jj]))%Matrix); last 
@@ -1828,8 +1828,8 @@ seq 3 3 : (#pre /\ aT{2} = lift_matrix at{1} /\
 + inline AuxMLKEM.__gen_matrix; conseq />.
   seq 7 3 : (a{1}=aT{2});  last by auto => />;  smt(matrix_unlift).
   while (i0{1} = i{2} /\ 0<=i0{1}<=kvec /\ seed{1}=rho{2} /\ trans{1} /\
-         forall ii jj, 0<=ii<i0{1} => 0<= jj <3 => (a{1}.[ii,jj])%Matrix = (aT{2}.[ii,jj])%Matrix); last  
-          by auto => />; smt(eq_matrixP).
+         forall ii jj, 0<=ii<i0{1} => 0<= jj <3 => (a{1}.[ii,jj])%Matrix = (aT{2}.[ii,jj])%Matrix); last
+          by auto => /> *; apply: eq_matrixP; smt().
   wp; while (i0{1} = i{2} /\ j{1} = j{2} /\ 0<=i0{1}<kvec /\ 0<=j{1}<=kvec /\ seed{1}=rho{2} /\ trans{1} /\
          (forall ii jj, 0<=ii<i0{1} => 0<= jj <3 => (a{1}.[ii,jj])%Matrix = (aT{2}.[ii,jj])%Matrix) /\
          (forall jj, 0 <= jj <j{1} => (a{1}.[i0{1},jj])%Matrix = (aT{2}.[i0{1},jj]))%Matrix); last 

proof/correctness/MLKEM_Poly.ec

@@ -1327,6 +1327,8 @@ seq 3 5 :  (r{1} = lift_array256 rp{2} /\ zetasp{2} = jzetas_inv /\
         by rewrite -incoeffM_mod /R qE //= ZqField.mulr1.
       + by rewrite zp /=.
     move => jl rl jr rpr; rewrite ultE /= => ??[#] *.
+    have ? : jl = 256 by smt().
+    subst jl.
     split; last by smt().
     by rewrite tP => x xb; rewrite !mapiE /#.
 
@@ -1698,46 +1700,52 @@ rewrite !to_uintD_small /=; 1..4:smt().
 rewrite !W64.shr_div /= Array64.Array64.initiE /=; 1: smt().
 move => r1 r1val r2 r2val r3 r3val r4 r4val r5 r5val r6 r6val r7 r7val r8 r8val r9 r9val r10 r10val.
 
-have  /= [#] redbl1 redbh1 redv1 := 
-    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr} + 1] * to_sint bp{hr}.[to_uint i{hr} + 1]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have hq : 0 < q && q < SignedReductions.R %/ 2 by rewrite /R /#.
+have hi: 0 <= to_uint i{hr} && to_uint i{hr} < 256 by smt().
+have hip1: 0 <= to_uint i{hr} + 1 && to_uint i{hr} + 1 < 256 by smt().
+have hip2: 0 <= to_uint i{hr} + 2 && to_uint i{hr} + 2 < 256 by smt().
+have hip3: 0 <= to_uint i{hr} + 3 && to_uint i{hr} + 3 < 256 by smt().
 
-have  /= [#] redbl2 redbh2 redv2 := 
-    (SREDCp_corr (to_sint r1 * to_sint jzetas.[64 + to_uint i{hr} %/ 4]) _ _); 1,2:
-     by rewrite /R /=; move : zeta_bound; rewrite /minimum_residues; smt().
+have  /= [#] redbl1 redbh1 redv1 :=
+    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr} + 1] * to_sint bp{hr}.[to_uint i{hr} + 1]) hq _).
+     by move: (ba _ hip1) (bb _ hip1); rewrite /R /#.
 
-have  /= [#] redbl3 redbh3 redv3 := 
-    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}] * to_sint bp{hr}.[to_uint i{hr}]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have  /= [#] redbl2 redbh2 redv2 :=
+    (SREDCp_corr (to_sint r1 * to_sint jzetas.[64 + to_uint i{hr} %/ 4]) hq _).
+     by rewrite /R /=; move : (zeta_bound (64 + to_uint i{hr} %/ 4)); rewrite /minimum_residues; smt().
 
-have  /= [#] redbl4 redbh4 redv4 := 
-    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}] * to_sint bp{hr}.[to_uint i{hr} + 1]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have  /= [#] redbl3 redbh3 redv3 :=
+    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}] * to_sint bp{hr}.[to_uint i{hr}]) hq _).
+     by move: (ba _ hi) (bb _ hi); rewrite /R /#.
 
-have  /= [#] redbl5 redbh5 redv5 := 
-    (SREDCp_corr(to_sint ap{hr}.[to_uint i{hr} + 1] * to_sint bp{hr}.[to_uint i{hr}]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have  /= [#] redbl4 redbh4 redv4 :=
+    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}] * to_sint bp{hr}.[to_uint i{hr} + 1]) hq _).
+     by move: (ba _ hi) (bb _ hip1); rewrite /R /#.
 
-have  /= [#] redbl6 redbh6 redv6 := 
-    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr} + 3] * to_sint bp{hr}.[to_uint i{hr} + 3]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have  /= [#] redbl5 redbh5 redv5 :=
+    (SREDCp_corr(to_sint ap{hr}.[to_uint i{hr} + 1] * to_sint bp{hr}.[to_uint i{hr}]) hq _).
+     by move: (ba _ hip1) (bb _ hi); rewrite /R /#.
 
-have  /= [#] redbl7 redbh7 redv7 := 
-    (SREDCp_corr (to_sint r6 * to_sint (- jzetas.[64 + to_uint i{hr} %/ 4])) _ _); 1: by rewrite /R /=; smt().
-+ rewrite /R /=; move : zeta_bound; rewrite /minimum_residues /bpos16 => zb.
+have  /= [#] redbl6 redbh6 redv6 :=
+    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr} + 3] * to_sint bp{hr}.[to_uint i{hr} + 3]) hq _).
+     by move: (ba _ hip3) (bb _ hip3); rewrite /R /#.
+
+have  /= [#] redbl7 redbh7 redv7 :=
+    (SREDCp_corr (to_sint r6 * to_sint (- jzetas.[64 + to_uint i{hr} %/ 4])) hq _).
++ rewrite /R /=; move : (zeta_bound (64 + to_uint i{hr} %/ 4)); rewrite /minimum_residues /bpos16 => zb.
   rewrite to_sintN /=; do split; smt().  
 
-have  /= [#] redbl8 redbh8 redv8 := 
-    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}+2] * to_sint bp{hr}.[to_uint i{hr}+2]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have  /= [#] redbl8 redbh8 redv8 :=
+    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}+2] * to_sint bp{hr}.[to_uint i{hr}+2]) hq _).
+     by move: (ba _ hip2) (bb _ hip2); rewrite /R /#.
 
-have  /= [#] redbl9 redbh9 redv9 := 
-    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}+2] * to_sint bp{hr}.[to_uint i{hr} + 3]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have  /= [#] redbl9 redbh9 redv9 :=
+    (SREDCp_corr (to_sint ap{hr}.[to_uint i{hr}+2] * to_sint bp{hr}.[to_uint i{hr} + 3]) hq _).
+     by move: (ba _ hip2) (bb _ hip3); rewrite /R /#.
 
-have  /= [#] redbl10 redbh10 redv10 := 
-    (SREDCp_corr(to_sint ap{hr}.[to_uint i{hr} + 3] * to_sint bp{hr}.[to_uint i{hr}+2]) _ _); 1,2:
-     by rewrite /R /=; smt().
+have  /= [#] redbl10 redbh10 redv10 :=
+    (SREDCp_corr(to_sint ap{hr}.[to_uint i{hr} + 3] * to_sint bp{hr}.[to_uint i{hr}+2]) hq _).
+     by move: (ba _ hip3) (bb _ hip2); rewrite /R /#.
 
 rewrite -r1val in redbl1;rewrite -r1val in redbh1;rewrite -r1val eq_incoeff in redv1.
 rewrite -r2val in redbl2;rewrite -r2val in redbh2;rewrite -r2val eq_incoeff in redv2.
@@ -1763,7 +1771,7 @@ move => zv2.
 do split; 1..3: smt().
 
 + move => k kb; case (k < to_uint i{hr}).
-  + by move => *; rewrite !set_neqiE /#. 
+  + move => *; rewrite !set_neqiE // 1..4:/#; apply: bprev => /#.
   move => *; case (k = to_uint i{hr}).
   + move => *. 
     rewrite set_neqiE; 1,2: smt().

proof/correctness/MLKEM_PolyVec.ec

@@ -635,8 +635,10 @@ while (#{~i{2}=0}{~j{2}=0}pre /\ to_uint i{1} = i{2} /\ 0<=i{2}<=768  /\
   split; 1:  smt(). 
   rewrite /lift_polyvec /decompress_polyvec eq_vectorP => i ib.
   rewrite /lift_array256 /subarray256 !tP   !offunvE //=. 
-  by rewrite !setvE;smt(zerovE offunvE offunvK Array256.mapiE Array256.initiE).
-
+  rewrite !setvE => k k_range.
+  rewrite Array256.mapiE // Array256.initiE // offunvE // zerovE !offunvK /=.
+  smt(Array256.mapiE Array256.initiE).
+
 unroll for {1} 22; unroll for {1} 2.
 
 auto => /> &1 &2 vpl vph il ih jv im0 prior priorb; rewrite ultE of_uintK /= => enter _.

proof/security/FO_TT.ec

@@ -1436,7 +1436,7 @@ proof.
   move => gs_ok A_count A_ll.
   have := (OW_PCVA_G_PCO &m).
   rewrite (PCO_PCO2 &m) (G_PCO2_G0 &m).
-  move: (G0_G1_1 &m A_count A_ll) (H_bad_Orclb1' &m) (H_bad_gamma_spread &m) ge0_qV. 
+  move: (G0_G1_1 &m A_count A_ll) (H_bad_Orclb1' &m) (H_bad_gamma_spread &m _ gs_ok) ge0_qV.
   by smt().
 qed.
 

proof/security/MLWE_PKE.ec

@@ -788,7 +788,7 @@ byequiv => //; proc; inline *.
 wp;call{1}(_: true ==> true); 1: by apply (A_ll ( (Sim(RO_H.LRO))));  apply (S_h_ll (RO_H.LRO)); apply RO_H.RO_get_ll; smt(duni_matrix_ll). 
 rcondt{1}6; 1: by move => *; auto => />;call(_: true);auto => />; smt(mem_empty).
 rnd{1};rnd;rnd{1}.
-auto => />; 1: by smt(). 
+auto => /> *; 1: by smt().
 call {1} (_: true ==> true); 1: by  apply (S_i_ll (RO_H.LRO)); apply RO_H.RO_get_ll; smt(duni_matrix_ll).  
 by auto => />;smt(dshort_R_ll dshort_ll get_set_sameE).
 qed.