final touches

formosa-crypto · Jan 15, 2025 · 9abd13a · 9abd13a
1 parent e32d9c3
commit 9abd13a
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 4 deletions.
diff --git a/formosa-keccak b/formosa-keccak
diff --git a/proof/correctness/avx2/MLKEM_KEM_avx2.ec b/proof/correctness/avx2/MLKEM_KEM_avx2.ec
@@ -627,7 +627,7 @@ seq 7 1 : (#pre /\
            (forall k, 0<=k<32 => buf{1}.[k] = m{2}.[k]) /\
            (forall k, 0<=k<32 => kr{1}.[k] = _K{2}.[k]) /\
            (forall k, 0<=k<32 => kr{1}.[k+32] = r{2}.[k])).
-ecall {1} (sha3_512A_A64_ph buf{1} kr{1}).
+ecall {1} (sha3_512A_A64_ph buf{1}).
 wp; conseq (_: _ ==> 
    (forall k, 0<=k<32 => buf{1}.[k] = m{2}.[k]) /\
    (forall k, 32<=k<64 => buf{1}.[k] = mem.[_skp + 2336 + k - 32]) /\
@@ -743,4 +743,3 @@ move => goodc mm back c0 c1;split.
     rewrite !tP => H k kb.
     by rewrite (H k kb) initiE /#.
 qed.
-
diff --git a/proof/correctness/avx2/MLKEM_keccak_avx2.ec b/proof/correctness/avx2/MLKEM_keccak_avx2.ec
@@ -75,7 +75,7 @@ equiv addratebit_avx2x4_eq:
 (****************************************************************************)
 (****************************************************************************)
 
-from Keccak require import Keccakf1600_ref.
+from Keccak require import Keccakf1600_ref Keccakf1600_avx2x4.
 from JazzEC require import WArray768.
 from JazzEC require import Array24 Array5.