Yes

formosa-crypto · Nov 4, 2024 · d702a45 · d702a45
1 parent 6068dcb
commit d702a45
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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".