errors fixed

formosa-crypto · Nov 22, 2023 · e23ad83 · e23ad83
1 parent 3a10285
commit e23ad83
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 23 deletions.
diff --git a/proof/correctness/Fq.ec b/proof/correctness/Fq.ec
@@ -48,15 +48,15 @@ module FQMUL_AVX = {
     ad <- (sigextu32 a);
     bd <- (sigextu32 b);
     c <- (ad * bd);
-    u <- (c * (W32.of_int (62209 `<<` 16)));
+    u <- (c * (W32.of_int 62209));
+    u <- (u `<<` (W8.of_int 16));
     u <- (u `|>>` (W8.of_int 16));
-    t <- (u * (W32.of_int (- 3329)));
-    t <- (t + c);
+    t <- (u * (W32.of_int 3329));
+    t <- (c - t);
     t <- (t `|>>` (W8.of_int 16));
     r <- (truncateu16 t);
     return (r);
-    }
-  }.
+  }  }.
 
 lemma fqmul_old_corr_h _a _b: 
    hoare[FQMUL_AVX.__fqmul : 
@@ -65,9 +65,18 @@ proof.
 proc; wp; skip  => &hr [#] /= H H0.
 rewrite /SREDC SAR_sem16 SAR_sem16 /=. 
 rewrite smod_W32 smod_W32 smod_W16 W16.of_sintK /(`<<`) /sigextu32 /truncateu16 /=  H H0.
+rewrite shlMP; first by smt(). 
 by rewrite W32.to_sintE W32.of_uintK W32.of_uintK W32.of_sintK qE /= !modz_dvd /R /=; smt().
 qed.
 
+lemma fqmul_old_ll : islossless FQMUL_AVX.__fqmul by proc; islossless.
+
+lemma fqmul_old_corr _a _b :
+  phoare [FQMUL_AVX.__fqmul : 
+     W16.to_sint a = _a /\ W16.to_sint b = _b ==> 
+         W16.to_sint res = SREDC (_a * _b)] = 1%r.
+proof. by conseq fqmul_old_ll (fqmul_old_corr_h _a _b). qed.
+
 
 lemma fqmul_corr_h _a _b: 
    hoare[Jkem.M(Jkem.Syscall).__fqmul : 

diff --git a/proof/correctness/avx2/Fq_avx2.ec b/proof/correctness/avx2/Fq_avx2.ec
@@ -564,22 +564,22 @@ Pr[Kyber_AVX2_cf.__fqmul_x16(a{m}, b{m}) @ &m :
    forall (k : int), 0 <= k && k < 16 => to_sint res.[k] = SREDC (_a.[k] * _b.[k])]; last by  byequiv fqmulx16_corr_h => //=. 
 byphoare (_: a = a{m} /\ b = b{m} ==> forall (k : int), 0 <= k && k < 16 => to_sint res.[k] = SREDC (_a.[k] * _b.[k]))=> //=.
 proc; unroll for 3.
-wp; call (fqmul_corr _a.[15] _b.[15]).
-wp; call (fqmul_corr _a.[14] _b.[14]).
-wp; call (fqmul_corr _a.[13] _b.[13]).
-wp; call (fqmul_corr _a.[12] _b.[12]).
-wp; call (fqmul_corr _a.[11] _b.[11]).
-wp; call (fqmul_corr _a.[10] _b.[10]).
-wp; call (fqmul_corr _a.[9] _b.[9]).
-wp; call (fqmul_corr _a.[8] _b.[8]).
-wp; call (fqmul_corr _a.[7] _b.[7]).
-wp; call (fqmul_corr _a.[6] _b.[6]).
-wp; call (fqmul_corr _a.[5] _b.[5]).
-wp; call (fqmul_corr _a.[4] _b.[4]).
-wp; call (fqmul_corr _a.[3] _b.[3]).
-wp; call (fqmul_corr _a.[2] _b.[2]).
-wp; call (fqmul_corr _a.[1] _b.[1]).
-wp; call (fqmul_corr _a.[0] _b.[0]).
+wp; call (fqmul_old_corr _a.[15] _b.[15]).
+wp; call (fqmul_old_corr _a.[14] _b.[14]).
+wp; call (fqmul_old_corr _a.[13] _b.[13]).
+wp; call (fqmul_old_corr _a.[12] _b.[12]).
+wp; call (fqmul_old_corr _a.[11] _b.[11]).
+wp; call (fqmul_old_corr _a.[10] _b.[10]).
+wp; call (fqmul_old_corr _a.[9] _b.[9]).
+wp; call (fqmul_old_corr _a.[8] _b.[8]).
+wp; call (fqmul_old_corr _a.[7] _b.[7]).
+wp; call (fqmul_old_corr _a.[6] _b.[6]).
+wp; call (fqmul_old_corr _a.[5] _b.[5]).
+wp; call (fqmul_old_corr _a.[4] _b.[4]).
+wp; call (fqmul_old_corr _a.[3] _b.[3]).
+wp; call (fqmul_old_corr _a.[2] _b.[2]).
+wp; call (fqmul_old_corr _a.[1] _b.[1]).
+wp; call (fqmul_old_corr _a.[0] _b.[0]).
 auto => />. 
 rewrite /lift_array16 tP /= in H.
 rewrite /lift_array16 tP /= in H0.

diff --git a/proof/correctness/avx2/Kyber_AVX2_cf.ec b/proof/correctness/avx2/Kyber_AVX2_cf.ec
@@ -2,7 +2,7 @@ require import AllCore List Int IntDiv StdOrder CoreMap Real Number.
 import IntOrder.
 from Jasmin require import JModel.
 require import Array16 Array32 Array64 Array128 Array168 Array256 Array384 Array768 Array960 Array1152.
-require import KyberFCLib W8extra List_extra.
+require import Fq KyberFCLib W8extra List_extra.
 
 
 require import Jkem.
@@ -317,7 +317,7 @@ module Kyber_AVX2_cf = {
     rd <- witness;
     i <- 0;
     while(i < 16) {
-      t <@Jkem.M(Jkem.Syscall).__fqmul(a.[i], b.[i]);
+      t <@ Fq.FQMUL_AVX.__fqmul(a.[i], b.[i]);
       rd.[i] <- t;
       i <- i + 1;
     }