From b1ecb428c60dd375b8bdd05c258cd0e4d5f1fec1 Mon Sep 17 00:00:00 2001 From: karthikbhargavan Date: Tue, 24 Sep 2024 20:39:58 +0000 Subject: [PATCH] verifies --- .../Libcrux_ml_kem.Constant_time_ops.fsti | 14 +++++++------- libcrux-ml-kem/src/constant_time_ops.rs | 14 +++++++------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti index 4b08592c4..dc6fd2b46 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti @@ -10,7 +10,7 @@ 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 @@ -18,7 +18,7 @@ val is_non_zero (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)) /// Return 1 if the bytes of `lhs` and `rhs` do not exactly /// match and 0 otherwise. @@ -28,7 +28,7 @@ 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 @@ -36,7 +36,7 @@ val compare_ciphertexts_in_constant_time (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)) /// 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))) diff --git a/libcrux-ml-kem/src/constant_time_ops.rs b/libcrux-ml-kem/src/constant_time_ops.rs index dc83a397b..02ea01eca 100644 --- a/libcrux-ml-kem/src/constant_time_ops.rs +++ b/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],