verifies

libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti

@@ -10,15 +10,15 @@ val inz (value: u8)
       (ensures
         fun result ->
           let result:u8 = result in
-          (value == 0uy ==> result == 0uy) /\ (value !==0uy ==> result == 1uy))
+          (value == 0uy ==> result == 0uy) /\ (value =!= 0uy ==> result == 1uy))
 
 val is_non_zero (value: u8)
     : Prims.Pure u8
       Prims.l_True
       (ensures
         fun result ->
           let result:u8 = result in
-          (value == 0uy ==> result == 0uy) /\ (value !==0uy ==> result == 1uy))
+          (value == 0uy ==> result == 0uy) /\ (value =!= 0uy ==> result == 1uy))
 
 /// Return 1 if the bytes of `lhs` and `rhs` do not exactly
 /// match and 0 otherwise.
@@ -28,15 +28,15 @@ val compare (lhs rhs: t_Slice u8)
       (ensures
         fun result ->
           let result:u8 = result in
-          (lhs == rhs ==> result == 0uy) /\ (lhs !==rhs ==> result == 1uy))
+          (lhs == rhs ==> result == 0uy) /\ (lhs =!= rhs ==> result == 1uy))
 
 val compare_ciphertexts_in_constant_time (lhs rhs: t_Slice u8)
     : Prims.Pure u8
       (requires (Core.Slice.impl__len #u8 lhs <: usize) =. (Core.Slice.impl__len #u8 rhs <: usize))
       (ensures
         fun result ->
           let result:u8 = result in
-          (lhs == rhs ==> result == 0uy) /\ (lhs !==rhs ==> result == 1uy))
+          (lhs == rhs ==> result == 0uy) /\ (lhs =!= rhs ==> result == 1uy))
 
 /// If `selector` is not zero, return the bytes in `rhs`; return the bytes in
 /// `lhs` otherwise.
@@ -48,7 +48,7 @@ val select_ct (lhs rhs: t_Slice u8) (selector: u8)
       (ensures
         fun result ->
           let result:t_Array u8 (sz 32) = result in
-          (selector == 0uy ==> result == lhs) /\ (selector !==0uy ==> result == rhs))
+          (selector == 0uy ==> result == lhs) /\ (selector =!= 0uy ==> result == rhs))
 
 val select_shared_secret_in_constant_time (lhs rhs: t_Slice u8) (selector: u8)
     : Prims.Pure (t_Array u8 (sz 32))
@@ -58,7 +58,7 @@ val select_shared_secret_in_constant_time (lhs rhs: t_Slice u8) (selector: u8)
       (ensures
         fun result ->
           let result:t_Array u8 (sz 32) = result in
-          (selector == 0uy ==> result == lhs) /\ (selector !==0uy ==> result == rhs))
+          (selector == 0uy ==> result == lhs) /\ (selector =!= 0uy ==> result == rhs))
 
 val compare_ciphertexts_select_shared_secret_in_constant_time (lhs_c rhs_c lhs_s rhs_s: t_Slice u8)
     : Prims.Pure (t_Array u8 (sz 32))
@@ -70,4 +70,4 @@ val compare_ciphertexts_select_shared_secret_in_constant_time (lhs_c rhs_c lhs_s
         fun result ->
           let result:t_Array u8 (sz 32) = result in
           let selector = if lhs_c =. rhs_c then 0uy else 1uy in
-          ((selector == 0uy ==> result == lhs_s) /\ (selector !==0uy ==> result == rhs_s)))
+          ((selector == 0uy ==> result == lhs_s) /\ (selector =!= 0uy ==> result == rhs_s)))

libcrux-ml-kem/src/constant_time_ops.rs

@@ -12,7 +12,7 @@ use crate::constants::SHARED_SECRET_SIZE;
 
 /// Return 1 if `value` is not zero and 0 otherwise.
 #[hax_lib::ensures(|result| fstar!("($value == 0uy ==> $result == 0uy) /\\
-    ($value !== 0uy ==> $result == 1uy)"))]
+    ($value =!= 0uy ==> $result == 1uy)"))]
 fn inz(value: u8) -> u8 {
     let _orig_value = value;
     let value = value as u16;
@@ -48,7 +48,7 @@ fn inz(value: u8) -> u8 {
 
 #[inline(never)] // Don't inline this to avoid that the compiler optimizes this out.
 #[hax_lib::ensures(|result| fstar!("($value == 0uy ==> $result == 0uy) /\\
-    ($value !== 0uy ==> $result == 1uy)"))]
+    ($value =!= 0uy ==> $result == 1uy)"))]
 fn is_non_zero(value: u8) -> u8 {
     #[cfg(eurydice)]
     return inz(value);
@@ -61,7 +61,7 @@ fn is_non_zero(value: u8) -> u8 {
 /// match and 0 otherwise.
 #[hax_lib::requires(lhs.len() == rhs.len())]
 #[hax_lib::ensures(|result| fstar!("($lhs == $rhs ==> $result == 0uy) /\\
-    ($lhs !== $rhs ==> $result == 1uy)"))]
+    ($lhs =!= $rhs ==> $result == 1uy)"))]
 fn compare(lhs: &[u8], rhs: &[u8]) -> u8 {
     let mut r: u8 = 0;
     for i in 0..lhs.len() {
@@ -111,7 +111,7 @@ fn compare(lhs: &[u8], rhs: &[u8]) -> u8 {
     lhs.len() == SHARED_SECRET_SIZE
 )]
 #[hax_lib::ensures(|result| fstar!("($selector == 0uy ==> $result == $lhs) /\\
-        ($selector !== 0uy ==> $result == $rhs)"))]
+        ($selector =!= 0uy ==> $result == $rhs)"))]
 #[hax_lib::fstar::options("--ifuel 0 --z3rlimit 50")]
 fn select_ct(lhs: &[u8], rhs: &[u8], selector: u8) -> [u8; SHARED_SECRET_SIZE] {
     let mask = is_non_zero(selector).wrapping_sub(1);
@@ -164,7 +164,7 @@ fn select_ct(lhs: &[u8], rhs: &[u8], selector: u8) -> [u8; SHARED_SECRET_SIZE] {
 #[inline(never)] // Don't inline this to avoid that the compiler optimizes this out.
 #[hax_lib::requires(lhs.len() == rhs.len())]
 #[hax_lib::ensures(|result| fstar!("($lhs == $rhs ==> $result == 0uy) /\\
-    ($lhs !== $rhs ==> $result == 1uy)"))]
+    ($lhs =!= $rhs ==> $result == 1uy)"))]
 pub(crate) fn compare_ciphertexts_in_constant_time(lhs: &[u8], rhs: &[u8]) -> u8 {
     #[cfg(eurydice)]
     return compare(lhs, rhs);
@@ -179,7 +179,7 @@ pub(crate) fn compare_ciphertexts_in_constant_time(lhs: &[u8], rhs: &[u8]) -> u8
     lhs.len() == SHARED_SECRET_SIZE
 )]
 #[hax_lib::ensures(|result| fstar!("($selector == 0uy ==> $result == $lhs) /\\
-       ($selector !== 0uy ==> $result == $rhs)"))]
+       ($selector =!= 0uy ==> $result == $rhs)"))]
 pub(crate) fn select_shared_secret_in_constant_time(
     lhs: &[u8],
     rhs: &[u8],
@@ -199,7 +199,7 @@ pub(crate) fn select_shared_secret_in_constant_time(
 )]
 #[hax_lib::ensures(|result| fstar!("let selector = if $lhs_c =. $rhs_c then 0uy else 1uy in
     ((selector == 0uy ==> $result == $lhs_s) /\\
-     (selector !== 0uy ==> $result == $rhs_s))"))]
+     (selector =!= 0uy ==> $result == $rhs_s))"))]
 pub(crate) fn compare_ciphertexts_select_shared_secret_in_constant_time(
     lhs_c: &[u8],
     rhs_c: &[u8],