Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

simd ml kem generic #243

Closed
wants to merge 3 commits into from
Closed

simd ml kem generic #243

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
cef6e8f
wip
franziskuskiefer Apr 30, 2024
ee2dd68
generic vector
franziskuskiefer Apr 30, 2024
6c0b7a0
F* | not laxing
franziskuskiefer Apr 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion libcrux-ml-kem/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ libcrux-sha3 = { version = "0.0.2-pre.2", path = "../libcrux-sha3" }
hax-lib = { git = "https://github.com/hacspec/hax/" }

[features]
default = []
default = ["simd128"]
simd128 = ["libcrux-sha3/simd128"]
simd256 = ["libcrux-sha3/simd256"]

Expand Down
206 changes: 137 additions & 69 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
View file
Open in desktop

Large diffs are not rendered by default.

39 changes: 31 additions & 8 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,35 +10,44 @@ val into_padded_array (v_LEN: usize) (slice: t_Slice u8)
/// Sample a vector of ring elements from a centered binomial distribution.
val sample_ring_element_cbd
(v_K v_ETA2_RANDOMNESS_SIZE v_ETA2: usize)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(prf_input: t_Array u8 (sz 33))
(domain_separator: u8)
: Prims.Pure
(t_Array u8 (sz 33) & u8 & t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K)
(t_Array u8 (sz 33) & u8 &
t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K)
Prims.l_True
(fun _ -> Prims.l_True)

/// Sample a vector of ring elements from a centered binomial distribution and
/// convert them into their NTT representations.
val sample_vector_cbd_then_ntt
(v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(prf_input: t_Array u8 (sz 33))
(domain_separator: u8)
: Prims.Pure (t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K & u8)
: Prims.Pure (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
Prims.l_True
(fun _ -> Prims.l_True)

/// Call [`compress_then_serialize_ring_element_u`] on each ring element.
val compress_then_serialize_u
(v_K v_OUT_LEN v_COMPRESSION_FACTOR v_BLOCK_LEN: usize)
(input: t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(input: t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K)
: Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True)

/// Call [`deserialize_then_decompress_ring_element_u`] on each ring element
/// in the `ciphertext`.
val deserialize_then_decompress_u
(v_K v_CIPHERTEXT_SIZE v_U_COMPRESSION_FACTOR: usize)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(ciphertext: t_Array u8 v_CIPHERTEXT_SIZE)
: Prims.Pure (t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K)
: Prims.Pure (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K)
Prims.l_True
(fun _ -> Prims.l_True)

Expand Down Expand Up @@ -80,14 +89,20 @@ val deserialize_then_decompress_u
val encrypt
(v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_LEN v_C2_LEN v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR v_BLOCK_LEN v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE:
usize)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(public_key: t_Slice u8)
(message: t_Array u8 (sz 32))
(randomness: t_Slice u8)
: Prims.Pure (t_Array u8 v_CIPHERTEXT_SIZE) Prims.l_True (fun _ -> Prims.l_True)

/// Call [`deserialize_to_uncompressed_ring_element`] for each ring element.
val deserialize_secret_key (v_K: usize) (secret_key: t_Slice u8)
: Prims.Pure (t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K)
val deserialize_secret_key
(v_K: usize)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(secret_key: t_Slice u8)
: Prims.Pure (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K)
Prims.l_True
(fun _ -> Prims.l_True)

Expand All @@ -112,20 +127,26 @@ val deserialize_secret_key (v_K: usize) (secret_key: t_Slice u8)
val decrypt
(v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
usize)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(secret_key: t_Slice u8)
(ciphertext: t_Array u8 v_CIPHERTEXT_SIZE)
: Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True)

/// Call [`serialize_uncompressed_ring_element`] for each ring element.
val serialize_secret_key
(v_K v_OUT_LEN: usize)
(key: t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(key: t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K)
: Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True)

/// Concatenate `t` and `ρ` into the public key.
val serialize_public_key
(v_K v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize)
(tt_as_ntt: t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(tt_as_ntt: t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K)
(seed_for_a: t_Slice u8)
: Prims.Pure (t_Array u8 v_PUBLIC_KEY_SIZE) Prims.l_True (fun _ -> Prims.l_True)

Expand Down Expand Up @@ -165,6 +186,8 @@ val serialize_public_key
val generate_keypair
(v_K v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_RANKED_BYTES_PER_RING_ELEMENT v_ETA1 v_ETA1_RANDOMNESS_SIZE:
usize)
(#v_Vector: Type)
{| i1: Libcrux_ml_kem.Simd.Simd_trait.t_Operations v_Vector |}
(key_generation_seed: t_Slice u8)
: Prims.Pure (t_Array u8 v_PRIVATE_KEY_SIZE & t_Array u8 v_PUBLIC_KEY_SIZE)
Prims.l_True
Expand Down
20 changes: 10 additions & 10 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber1024.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,16 +17,6 @@ let encapsulate
Libcrux_ml_kem.encapsulate (sz 4) (sz 1568) (sz 1568) (sz 1536) (sz 1408) (sz 160) (sz 11) (sz 5)
(sz 352) (sz 2) (sz 128) (sz 2) (sz 128) public_key randomness

let generate_key_pair (randomness: t_Array u8 (sz 64)) =
Libcrux_ml_kem.generate_keypair (sz 4)
(sz 1536)
(sz 3168)
(sz 1568)
(sz 1536)
(sz 2)
(sz 128)
randomness

let validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568)) =
if
Libcrux_ml_kem.validate_public_key (sz 4)
Expand All @@ -41,3 +31,13 @@ let validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1
Core.Option.Option_None
<:
Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568))

let generate_key_pair (randomness: t_Array u8 (sz 64)) =
Libcrux_ml_kem.generate_keypair (sz 4)
(sz 1536)
(sz 3168)
(sz 1568)
(sz 1536)
(sz 2)
(sz 128)
randomness
12 changes: 6 additions & 6 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber1024.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,15 +85,15 @@ val encapsulate
Prims.l_True
(fun _ -> Prims.l_True)

/// Generate ML-KEM 1024 Key Pair
val generate_key_pair (randomness: t_Array u8 (sz 64))
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 3168) (sz 1568))
Prims.l_True
(fun _ -> Prims.l_True)

/// Validate a public key.
/// Returns `Some(public_key)` if valid, and `None` otherwise.
val validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568))
: Prims.Pure (Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568)))
Prims.l_True
(fun _ -> Prims.l_True)

/// Generate ML-KEM 1024 Key Pair
val generate_key_pair (randomness: t_Array u8 (sz 64))
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 3168) (sz 1568))
Prims.l_True
(fun _ -> Prims.l_True)
20 changes: 10 additions & 10 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber512.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,16 +17,6 @@ let encapsulate
Libcrux_ml_kem.encapsulate (sz 2) (sz 768) (sz 800) (sz 768) (sz 640) (sz 128) (sz 10) (sz 4)
(sz 320) (sz 3) (sz 192) (sz 2) (sz 128) public_key randomness

let generate_key_pair (randomness: t_Array u8 (sz 64)) =
Libcrux_ml_kem.generate_keypair (sz 2)
(sz 768)
(sz 1632)
(sz 800)
(sz 768)
(sz 3)
(sz 192)
randomness

let validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) =
if
Libcrux_ml_kem.validate_public_key (sz 2)
Expand All @@ -39,3 +29,13 @@ let validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 8
Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800))
else
Core.Option.Option_None <: Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800))

let generate_key_pair (randomness: t_Array u8 (sz 64)) =
Libcrux_ml_kem.generate_keypair (sz 2)
(sz 768)
(sz 1632)
(sz 800)
(sz 768)
(sz 3)
(sz 192)
randomness
12 changes: 6 additions & 6 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber512.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,15 +85,15 @@ val encapsulate
Prims.l_True
(fun _ -> Prims.l_True)

/// Generate ML-KEM 512 Key Pair
val generate_key_pair (randomness: t_Array u8 (sz 64))
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 1632) (sz 800))
Prims.l_True
(fun _ -> Prims.l_True)

/// Validate a public key.
/// Returns `Some(public_key)` if valid, and `None` otherwise.
val validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800))
: Prims.Pure (Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)))
Prims.l_True
(fun _ -> Prims.l_True)

/// Generate ML-KEM 512 Key Pair
val generate_key_pair (randomness: t_Array u8 (sz 64))
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 1632) (sz 800))
Prims.l_True
(fun _ -> Prims.l_True)
20 changes: 10 additions & 10 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber768.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,16 +17,6 @@ let encapsulate
Libcrux_ml_kem.encapsulate (sz 3) (sz 1088) (sz 1184) (sz 1152) (sz 960) (sz 128) (sz 10) (sz 4)
(sz 320) (sz 2) (sz 128) (sz 2) (sz 128) public_key randomness

let generate_key_pair (randomness: t_Array u8 (sz 64)) =
Libcrux_ml_kem.generate_keypair (sz 3)
(sz 1152)
(sz 2400)
(sz 1184)
(sz 1152)
(sz 2)
(sz 128)
randomness

let validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184)) =
if
Libcrux_ml_kem.validate_public_key (sz 3)
Expand All @@ -41,3 +31,13 @@ let validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1
Core.Option.Option_None
<:
Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184))

let generate_key_pair (randomness: t_Array u8 (sz 64)) =
Libcrux_ml_kem.generate_keypair (sz 3)
(sz 1152)
(sz 2400)
(sz 1184)
(sz 1152)
(sz 2)
(sz 128)
randomness
12 changes: 6 additions & 6 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber768.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,15 +85,15 @@ val encapsulate
Prims.l_True
(fun _ -> Prims.l_True)

/// Generate ML-KEM 768 Key Pair
val generate_key_pair (randomness: t_Array u8 (sz 64))
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 2400) (sz 1184))
Prims.l_True
(fun _ -> Prims.l_True)

/// Validate a public key.
/// Returns `Some(public_key)` if valid, and `None` otherwise.
val validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184))
: Prims.Pure (Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184)))
Prims.l_True
(fun _ -> Prims.l_True)

/// Generate ML-KEM 768 Key Pair
val generate_key_pair (randomness: t_Array u8 (sz 64))
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 2400) (sz 1184))
Prims.l_True
(fun _ -> Prims.l_True)
Loading