Skip to content

Commit

Permalink
Update traits.rs
Browse files Browse the repository at this point in the history
  • Loading branch information
mamonet committed Sep 23, 2024
1 parent ec66aac commit aee4c5b
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion libcrux-ml-kem/src/vector/traits.rs
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,6 @@ pub fn to_standard_domain<T: Operations>(v: T) -> T {
T::montgomery_multiply_by_constant(v, MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS as i16)
}

#[hax_lib::fstar::verification_status(lax)]
#[hax_lib::fstar::options("--z3rlimit 100")]
#[hax_lib::requires(fstar!("Spec.Utils.is_i16b_array 3328 (i1._super_8706949974463268012.f_repr a)"))]
#[hax_lib::ensures(|result| fstar!("forall i.
Expand Down

0 comments on commit aee4c5b

Please sign in to comment.