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

Jump to bottom

Rearranged some code to speed things up and get bounds on compress_q and decompress_q. #124

Merged
merged 5 commits into from
Oct 30, 2023
Merged

Rearranged some code to speed things up and get bounds on compress_q and decompress_q. #124

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7ddbda4
Rearranged some code to speed things up and get bounds on compress_q …
xvzcf Oct 26, 2023
c012331
Slightly refine the precondition for decompress.
xvzcf Oct 27, 2023
7aabdec
Deduplicated ntt_at_layer macro.
xvzcf Oct 27, 2023
8aa11d2
Removed all traits on KyberPolynomialRingElement for F-star proofs.
xvzcf Oct 27, 2023
9287a20
Removed one TODO in NTT.
xvzcf Oct 27, 2023
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 hax-driver.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ def shell(command, expect=0, cwd=None):
"hax",
"into",
"-i",
"-** +libcrux::kem::kyber::** -libcrux::kem::kyber::arithmetic::mutable_operations::** -libcrux::hacl::sha3::** -libcrux::digest::**",
"-** +libcrux::kem::kyber::** -libcrux::hacl::sha3::** -libcrux::digest::**",
"fstar",
],
cwd=".",
Expand Down
103 changes: 25 additions & 78 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -155,87 +155,34 @@ let montgomery_reduce (value: i32) : i32 =
in
reduced

let to_montgomery_domain (value: i32) : i32 = montgomery_reduce (1353l *! value <: i32)

type t_KyberPolynomialRingElement = { f_coefficients:t_Array i32 (sz 256) }

let impl__KyberPolynomialRingElement__ZERO: t_KyberPolynomialRingElement =
{ f_coefficients = Rust_primitives.Hax.repeat 0l (sz 256) }

let impl_1: Core.Ops.Index.t_Index t_KyberPolynomialRingElement usize =
{
f_Output = i32;
f_index
=
fun (self: t_KyberPolynomialRingElement) (index: usize) -> self.f_coefficients.[ index ]
}

let impl_2: Core.Iter.Traits.Collect.t_IntoIterator t_KyberPolynomialRingElement =
{
f_Item = i32;
f_IntoIter = Core.Array.Iter.t_IntoIter i32 (sz 256);
f_into_iter
=
fun (self: t_KyberPolynomialRingElement) ->
Core.Iter.Traits.Collect.f_into_iter self.f_coefficients
}

let impl_3: Core.Ops.Arith.t_Add t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
{
f_Output = t_KyberPolynomialRingElement;
f_add
=
fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) ->
let result:t_KyberPolynomialRingElement = impl__KyberPolynomialRingElement__ZERO in
let result:t_KyberPolynomialRingElement =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT
})
<:
Core.Ops.Range.t_Range usize)
result
(fun result i ->
{
result with
f_coefficients
=
Rust_primitives.Hax.update_at result.f_coefficients
i
((self.f_coefficients.[ i ] <: i32) +! (other.f_coefficients.[ i ] <: i32) <: i32)
<:
t_KyberPolynomialRingElement
})
in
result
}

let impl_4: Core.Ops.Arith.t_Sub t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
{
f_Output = t_KyberPolynomialRingElement;
f_sub
=
fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) ->
let result:t_KyberPolynomialRingElement = impl__KyberPolynomialRingElement__ZERO in
let result:t_KyberPolynomialRingElement =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT
})
let add_to_ring_element (lhs rhs: t_KyberPolynomialRingElement) : t_KyberPolynomialRingElement =
let lhs:t_KyberPolynomialRingElement =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end
=
Core.Slice.impl__len (Rust_primitives.unsize lhs.f_coefficients <: t_Slice i32)
<:
usize
})
<:
Core.Ops.Range.t_Range usize)
lhs
(fun lhs i ->
{
lhs with
f_coefficients
=
Rust_primitives.Hax.update_at lhs.f_coefficients
i
((lhs.f_coefficients.[ i ] <: i32) +! (rhs.f_coefficients.[ i ] <: i32) <: i32)
<:
Core.Ops.Range.t_Range usize)
result
(fun result i ->
{
result with
f_coefficients
=
Rust_primitives.Hax.update_at result.f_coefficients
i
((self.f_coefficients.[ i ] <: i32) -! (other.f_coefficients.[ i ] <: i32) <: i32)
<:
t_KyberPolynomialRingElement
})
in
result
}
t_KyberPolynomialRingElement
})
in
lhs
57 changes: 53 additions & 4 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,23 @@ let compress_q (#v_COEFFICIENT_BITS: usize) (fe: u16) : i32 =
if true
then
let _:Prims.unit =
if ~.(v_COEFFICIENT_BITS <=. Libcrux.Kem.Kyber.Constants.v_BITS_PER_COEFFICIENT <: bool)
if ~.(v_COEFFICIENT_BITS <=. sz 11 <: bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS <= BITS_PER_COEFFICIENT"
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS <= 11"

<:
Rust_primitives.Hax.t_Never)
in
()
in
let _:Prims.unit =
if true
then
let _:Prims.unit =
if
~.((Core.Convert.f_from fe <: i32) <. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: i32::from(fe) < FIELD_MODULUS"

<:
Rust_primitives.Hax.t_Never)
Expand Down Expand Up @@ -46,9 +60,22 @@ let decompress_q (#v_COEFFICIENT_BITS: usize) (fe: i32) : i32 =
if true
then
let _:Prims.unit =
if ~.(v_COEFFICIENT_BITS <=. Libcrux.Kem.Kyber.Constants.v_BITS_PER_COEFFICIENT <: bool)
if ~.(v_COEFFICIENT_BITS <=. sz 11 <: bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS <= 11"

<:
Rust_primitives.Hax.t_Never)
in
()
in
let _:Prims.unit =
if true
then
let _:Prims.unit =
if ~.((0l <=. fe <: bool) && (fe <. (1l <<! v_COEFFICIENT_BITS <: i32) <: bool))
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS <= BITS_PER_COEFFICIENT"
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: 0 <= fe && fe < (1 << COEFFICIENT_BITS)"

<:
Rust_primitives.Hax.t_Never)
Expand All @@ -60,6 +87,28 @@ let decompress_q (#v_COEFFICIENT_BITS: usize) (fe: i32) : i32 =
in
let decompressed:u32 = (decompressed <<! 1l <: u32) +! (1ul <<! v_COEFFICIENT_BITS <: u32) in
let decompressed:u32 = decompressed >>! (v_COEFFICIENT_BITS +! sz 1 <: usize) in
let _:Prims.unit =
if true
then
let _:Prims.unit =
if
~.(decompressed <.
(Core.Result.impl__unwrap (Core.Convert.f_try_from Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS

<:
Core.Result.t_Result u32 Core.Num.Error.t_TryFromIntError)
<:
u32)
<:
bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: decompressed < u32::try_from(FIELD_MODULUS).unwrap()"

<:
Rust_primitives.Hax.t_Never)
in
()
in
cast decompressed <: i32

let decompress
Expand Down
53 changes: 7 additions & 46 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ let cbd (#v_K #v_ETA #v_ETA_RANDOMNESS_SIZE: usize) (prf_input: t_Array u8 (sz 3
let re_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
Rust_primitives.Hax.update_at re_as_ntt
i
(Libcrux.Kem.Kyber.Ntt.ntt_with_debug_asserts r (cast v_ETA <: i32)
(Libcrux.Kem.Kyber.Ntt.ntt_binomially_sampled_ring_element r
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
in
Expand Down Expand Up @@ -411,7 +411,7 @@ let generate_keypair
let secret_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
Rust_primitives.Hax.update_at secret_as_ntt
i
(Libcrux.Kem.Kyber.Ntt.ntt_with_debug_asserts secret (cast v_ETA1 <: i32)
(Libcrux.Kem.Kyber.Ntt.ntt_binomially_sampled_ring_element secret
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
in
Expand Down Expand Up @@ -444,7 +444,7 @@ let generate_keypair
let error_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
Rust_primitives.Hax.update_at error_as_ntt
i
(Libcrux.Kem.Kyber.Ntt.ntt_with_debug_asserts error (cast v_ETA1 <: i32)
(Libcrux.Kem.Kyber.Ntt.ntt_binomially_sampled_ring_element error
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
in
Expand Down Expand Up @@ -622,45 +622,13 @@ let encrypt
t_Slice u8)
in
let u:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
Libcrux.Kem.Kyber.Ntt.multiply_matrix_by_column_montgomery v_A_transpose r_as_ntt
in
let u:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_K
})
<:
Core.Ops.Range.t_Range usize)
u
(fun u i ->
Rust_primitives.Hax.update_at u
i
((Libcrux.Kem.Kyber.Ntt.invert_ntt_montgomery (u.[ i ]
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +!
(error_1_.[ i ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
<:
t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K)
Libcrux.Kem.Kyber.Ntt.compute_vector_u v_A_transpose r_as_ntt error_1_
in
let message_as_ring_element:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement =
Libcrux.Kem.Kyber.Serialize.deserialize_then_decompress_message message
in
let v:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement =
((Libcrux.Kem.Kyber.Ntt.invert_ntt_montgomery (Libcrux.Kem.Kyber.Ntt.multiply_row_by_column_montgomery
tt_as_ntt
r_as_ntt
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +!
error_2_
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +!
message_as_ring_element
Libcrux.Kem.Kyber.Ntt.compute_ring_element_v tt_as_ntt r_as_ntt error_2_ message_as_ring_element
in
let c1:t_Array u8 v_C1_LEN = compress_then_encode_u u in
let c2:t_Array u8 v_C2_LEN =
Expand Down Expand Up @@ -729,7 +697,7 @@ let decrypt
let u_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K =
Rust_primitives.Hax.update_at u_as_ntt
i
(Libcrux.Kem.Kyber.Ntt.ntt_representation u
(Libcrux.Kem.Kyber.Ntt.ntt_vector_u u
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
in
Expand Down Expand Up @@ -764,13 +732,6 @@ let decrypt
t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K)
in
let message:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement =
v -!
(Libcrux.Kem.Kyber.Ntt.invert_ntt_montgomery (Libcrux.Kem.Kyber.Ntt.multiply_row_by_column_montgomery
secret_as_ntt
u_as_ntt
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
<:
Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
Libcrux.Kem.Kyber.Ntt.compute_message v secret_as_ntt u_as_ntt
in
Libcrux.Kem.Kyber.Serialize.compress_then_serialize_message message
Loading