From d702a45cf8e898fddb3ab26e461a976ed059ede5 Mon Sep 17 00:00:00 2001 From: Gustavo Delerue Date: Mon, 4 Nov 2024 15:35:55 +0000 Subject: [PATCH] Yes --- proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec b/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec index aab3e17a..593eab6b 100644 --- a/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec +++ b/proof/correctness/avx2/MLKEM_InnerPKE_avx2.ec @@ -2109,7 +2109,7 @@ case : (to_uint bv2 < 64). + rewrite /(`<<`) W64.to_uint_shl; 1: by smt(W8.to_uint_cmp). rewrite /truncateu8 => bv2bnd />. do 2! (rewrite (pmod_small (to_uint bv2) _);smt(W64.to_uint_cmp)). -admit. (* What is the circuit behavior? Does it give zero? *) +admit. (* What is the circuit behavior? Does it give zero? Yes. *) qed. bind op [W32.t & W16.t] W2u16.truncateu16 "truncate".