Skip to content

Commit

Permalink
fix verification
Browse files Browse the repository at this point in the history
  • Loading branch information
@franziskuskiefer
franziskuskiefer committed Dec 6, 2023
1 parent ccaf0f2 commit 2aeea4f
Show file tree
Hide file tree
Showing 5 changed files with 54 additions and 23 deletions.
47 changes: 39 additions & 8 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,40 @@ module Libcrux.Kem.Kyber.Ind_cpa
open Core
open FStar.Mul

let into_padded_array (v_LEN: usize) (slice: t_Slice u8) : t_Array u8 v_LEN =
let _:Prims.unit =
if true
then
let _:Prims.unit =
if ~.((Core.Slice.impl__len slice <: usize) <=. v_LEN <: bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: slice.len() <= LEN"

<:
Rust_primitives.Hax.t_Never)
in
()
in
let out:t_Array u8 v_LEN = Rust_primitives.Hax.repeat 0uy v_LEN in
let out:t_Array u8 v_LEN =
Rust_primitives.Hax.Monomorphized_update_at.update_at_range out
({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = Core.Slice.impl__len slice <: usize }
<:
Core.Ops.Range.t_Range usize)
(Core.Slice.impl__copy_from_slice (out.[ {
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = Core.Slice.impl__len slice <: usize
}
<:
Core.Ops.Range.t_Range usize ]
<:
t_Slice u8)
slice
<:
t_Slice u8)
in
out

let sample_ring_element_cbd
(v_K v_ETA2_RANDOMNESS_SIZE v_ETA2: usize)
(prf_input: t_Array u8 (sz 33))
Expand Down Expand Up @@ -337,12 +371,10 @@ let encrypt
(t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
Libcrux.Kem.Kyber.Matrix.sample_matrix_A v_K
(Libcrux.Kem.Kyber.Conversions.into_padded_array (sz 34) seed <: t_Array u8 (sz 34))
(into_padded_array (sz 34) seed <: t_Array u8 (sz 34))
false
in
let (prf_input: t_Array u8 (sz 33)):t_Array u8 (sz 33) =
Libcrux.Kem.Kyber.Conversions.into_padded_array (sz 33) randomness
in
let (prf_input: t_Array u8 (sz 33)):t_Array u8 (sz 33) = into_padded_array (sz 33) randomness in
let r_as_ntt, domain_separator:(t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K &
u8) =
sample_vector_cbd_then_ntt v_K v_ETA1 v_ETA1_RANDOMNESS_SIZE prf_input 0uy
Expand Down Expand Up @@ -387,8 +419,7 @@ let encrypt
v
in
let (ciphertext: t_Array u8 v_CIPHERTEXT_SIZE):t_Array u8 v_CIPHERTEXT_SIZE =
Libcrux.Kem.Kyber.Conversions.into_padded_array v_CIPHERTEXT_SIZE
(Rust_primitives.unsize c1 <: t_Slice u8)
into_padded_array v_CIPHERTEXT_SIZE (Rust_primitives.unsize c1 <: t_Slice u8)
in
let ciphertext:t_Array u8 v_CIPHERTEXT_SIZE =
Rust_primitives.Hax.Monomorphized_update_at.update_at_range_from ciphertext
Expand Down Expand Up @@ -529,11 +560,11 @@ let generate_keypair
(t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K) v_K &
Core.Option.t_Option Libcrux.Kem.Kyber.Types.t_Error) =
Libcrux.Kem.Kyber.Matrix.sample_matrix_A v_K
(Libcrux.Kem.Kyber.Conversions.into_padded_array (sz 34) seed_for_A <: t_Array u8 (sz 34))
(into_padded_array (sz 34) seed_for_A <: t_Array u8 (sz 34))
true
in
let (prf_input: t_Array u8 (sz 33)):t_Array u8 (sz 33) =
Libcrux.Kem.Kyber.Conversions.into_padded_array (sz 33) seed_for_secret_and_error
into_padded_array (sz 33) seed_for_secret_and_error
in
let secret_as_ntt, domain_separator:(t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
v_K &
Expand Down
8 changes: 4 additions & 4 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ let decapsulate
ciphertext.Libcrux.Kem.Kyber.Types.f_value
in
let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) =
Libcrux.Kem.Kyber.Conversions.into_padded_array (sz 64)
Libcrux.Kem.Kyber.Ind_cpa.into_padded_array (sz 64)
(Rust_primitives.unsize decrypted <: t_Slice u8)
in
let to_hash:t_Array u8 (sz 64) =
Expand Down Expand Up @@ -168,7 +168,7 @@ let decapsulate
in
let (to_hash: t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE):t_Array u8
v_IMPLICIT_REJECTION_HASH_INPUT_SIZE =
Libcrux.Kem.Kyber.Conversions.into_padded_array v_IMPLICIT_REJECTION_HASH_INPUT_SIZE
Libcrux.Kem.Kyber.Ind_cpa.into_padded_array v_IMPLICIT_REJECTION_HASH_INPUT_SIZE
implicit_rejection_value
in
let to_hash:t_Array u8 v_IMPLICIT_REJECTION_HASH_INPUT_SIZE =
Expand Down Expand Up @@ -200,7 +200,7 @@ let decapsulate
let selector:u8 =
Libcrux.Kem.Kyber.Constant_time_ops.compare_ciphertexts_in_constant_time v_CIPHERTEXT_SIZE
(Core.Convert.f_as_ref ciphertext <: t_Slice u8)
(Core.Convert.f_as_ref expected_ciphertext <: t_Slice u8)
(Rust_primitives.unsize expected_ciphertext <: t_Slice u8)
in
Libcrux.Kem.Kyber.Constant_time_ops.select_shared_secret_in_constant_time shared_secret
(Rust_primitives.unsize implicit_rejection_shared_secret <: t_Slice u8)
Expand All @@ -215,7 +215,7 @@ let encapsulate
(Libcrux.Kem.Kyber.Types.t_KyberCiphertext v_CIPHERTEXT_SIZE & t_Array u8 (sz 32))
Libcrux.Kem.Kyber.Types.t_Error =
let (to_hash: t_Array u8 (sz 64)):t_Array u8 (sz 64) =
Libcrux.Kem.Kyber.Conversions.into_padded_array (sz 64)
Libcrux.Kem.Kyber.Ind_cpa.into_padded_array (sz 64)
(Rust_primitives.unsize randomness <: t_Slice u8)
in
let to_hash:t_Array u8 (sz 64) =
Expand Down
5 changes: 2 additions & 3 deletions src/kem/kyber.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ pub(crate) mod constants;
mod arithmetic;
mod compress;
mod constant_time_ops;
mod conversions;
mod hash_functions;
mod ind_cpa;
mod matrix;
Expand All @@ -36,8 +35,8 @@ use self::{
compare_ciphertexts_in_constant_time, select_shared_secret_in_constant_time,
},
constants::{CPA_PKE_KEY_GENERATION_SEED_SIZE, H_DIGEST_SIZE, SHARED_SECRET_SIZE},
conversions::into_padded_array,
hash_functions::{G, H, PRF},
ind_cpa::into_padded_array,
};

/// Seed size for key generation
Expand Down Expand Up @@ -220,7 +219,7 @@ pub(super) fn decapsulate<

let selector = compare_ciphertexts_in_constant_time::<CIPHERTEXT_SIZE>(
ciphertext.as_ref(),
expected_ciphertext.as_ref(),
&expected_ciphertext,
);

select_shared_secret_in_constant_time(
Expand Down
7 changes: 0 additions & 7 deletions src/kem/kyber/conversions.rs
View file

This file was deleted.

10 changes: 9 additions & 1 deletion src/kem/kyber/ind_cpa.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ use std::usize;
use super::{
arithmetic::PolynomialRingElement,
constants::{BYTES_PER_RING_ELEMENT, COEFFICIENTS_IN_RING_ELEMENT, SHARED_SECRET_SIZE},
conversions::into_padded_array,
hash_functions::{G, PRF},
matrix::*,
ntt::*,
Expand All @@ -17,6 +16,15 @@ use super::{
Error,
};

/// Pad the `slice` with `0`s at the end.
#[inline(always)]
pub(super) fn into_padded_array<const LEN: usize>(slice: &[u8]) -> [u8; LEN] {
debug_assert!(slice.len() <= LEN);
let mut out = [0u8; LEN];
out[0..slice.len()].copy_from_slice(slice);
out
}

/// Concatenate `t` and `ρ` into the public key.
#[inline(always)]
fn serialize_public_key<
Expand Down

0 comments on commit 2aeea4f

Please sign in to comment.