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

Add Kyber512 and Kyber1024 reference implementation #109

Merged
merged 19 commits into from
Oct 11, 2023
Merged

Add Kyber512 and Kyber1024 reference implementation #109

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
df1ccac
Some reorganization and refactoring.
xvzcf Oct 4, 2023
c9b5d90
Added reference implementation of Kyber512.
xvzcf Oct 5, 2023
b705249
Added reference implementation of Kyber1024.
xvzcf Oct 6, 2023
403ad3e
cargo fmt
xvzcf Oct 10, 2023
a67bea5
Updated kyber tests.
xvzcf Oct 10, 2023
4890bf9
Update F-star extraction.
xvzcf Oct 10, 2023
015bcd7
chunks -> chunks_exact
xvzcf Oct 10, 2023
d7ec486
Slight refactoring.
xvzcf Oct 10, 2023
8860224
Don't take needless references.
xvzcf Oct 10, 2023
22202bc
Ensure secret key is actually modified.
xvzcf Oct 10, 2023
65aefb6
Add python scripts to generate the KATs.
xvzcf Oct 11, 2023
a053828
Add generic parameter to decompress.
xvzcf Oct 11, 2023
e0d804f
Misc review comments.
xvzcf Oct 11, 2023
2fc1467
Refactored kyber_nistkats test code.
xvzcf Oct 11, 2023
b185f45
Update F-star extraction script and it's use in CI to reflect the lat…
xvzcf Oct 11, 2023
f764d5b
Update F-star extraction for Kyber reference code.
xvzcf Oct 11, 2023
0a02f62
Fix bugs in extraction script.
xvzcf Oct 11, 2023
d61e642
Update F-star extraction for Kyber specification.
xvzcf Oct 11, 2023
01e1ea6
More fixing extract_to_fstar.py.
xvzcf Oct 11, 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
118 changes: 75 additions & 43 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 @@ -2,108 +2,140 @@ module Libcrux.Kem.Kyber.Arithmetic
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core

let t_KyberFieldElement = i32

let v_BARRETT_SHIFT: i32 = 26l

let v_BARRETT_R: i32 = 1l <<! v_BARRETT_SHIFT
let v_BARRETT_R: i32 = 1l >>. v_BARRETT_SHIFT

let v_BARRETT_MULTIPLIER: i32 = 20159l

let barrett_reduce (value: i32) : i32 =
let quotient:i32 =
((value *! v_BARRETT_MULTIPLIER <: i32) +! (v_BARRETT_R >>! 1l <: i32) <: i32) >>!
((value *. v_BARRETT_MULTIPLIER <: i32) +. (v_BARRETT_R <<. 1l <: i32) <: i32) <<.
v_BARRETT_SHIFT
in
value -! (quotient *! Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32)
value -. (quotient *. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32)

let v_MONTGOMERY_SHIFT: i64 = 16L

let v_MONTGOMERY_R: i64 = 1L <<! v_MONTGOMERY_SHIFT
let v_MONTGOMERY_R: i64 = 1L >>. v_MONTGOMERY_SHIFT

let v_INVERSE_OF_MODULUS_MOD_R: i64 = (-3327L)
let v_INVERSE_OF_MODULUS_MOD_R: i64 = 3327L

let montgomery_reduce (value: i32) : i32 =
let (t: i64):i64 = (Core.Convert.f_from value <: i64) *! v_INVERSE_OF_MODULUS_MOD_R in
let (t: i32):i32 = cast (t &. (v_MONTGOMERY_R -! 1L <: i64)) <: i32 in
(value -! (t *! Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: i32) >>! v_MONTGOMERY_SHIFT
let (t: i64):i64 = (Core.Convert.From.from value <: i64) *. v_INVERSE_OF_MODULUS_MOD_R in
let (t: i32):i32 = cast (t &. (v_MONTGOMERY_R -. 1L <: i64)) in
(value -. (t *. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: i32) <<. v_MONTGOMERY_SHIFT

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

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

let impl__ZERO: t_KyberPolynomialRingElement =
{ f_coefficients = Rust_primitives.Hax.repeat 0l (sz 256) }
let v_ZERO_under_impl: t_KyberPolynomialRingElement =
{
Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
=
Rust_primitives.Hax.repeat 0l 256sz
}

let impl_1: Core.Ops.Index.t_Index t_KyberPolynomialRingElement usize =
let impl: Core.Ops.Index.t_Index t_KyberPolynomialRingElement usize =
{
f_impl_1__Output = i32;
f_impl_1__index
output = i32;
index
=
fun (self: t_KyberPolynomialRingElement) (index: usize) -> self.f_coefficients.[ index ]
fun (self: t_KyberPolynomialRingElement) (index: usize) ->
self.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ index ]
}

let impl_2: Core.Iter.Traits.Collect.t_IntoIterator t_KyberPolynomialRingElement =
let impl: Core.Iter.Traits.Collect.t_IntoIterator t_KyberPolynomialRingElement =
{
f_impl_2__Item = i32;
f_impl_2__IntoIter = Core.Array.Iter.t_IntoIter i32 (sz 256);
f_impl_2__into_iter
item = i32;
intoIter = Core.Array.Iter.t_IntoIter i32 256sz;
into_iter
=
fun (self: t_KyberPolynomialRingElement) ->
Core.Iter.Traits.Collect.f_into_iter self.f_coefficients
Core.Iter.Traits.Collect.IntoIterator.into_iter self
.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
}

let impl_3: Core.Ops.Arith.t_Add t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
let impl: Core.Ops.Arith.t_Add t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
{
f_impl_3__Output = t_KyberPolynomialRingElement;
f_impl_3__add
output = t_KyberPolynomialRingElement;
add
=
fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) ->
let result:t_KyberPolynomialRingElement = impl__ZERO in
let result:t_KyberPolynomialRingElement = v_ZERO_under_impl in
let result:t_KyberPolynomialRingElement =
Core.Iter.Traits.Iterator.Iterator.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.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
Core.Ops.Range.Range.f_start = 0sz;
Core.Ops.Range.Range.f_end
=
Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT
})
<:
_.f_IntoIter)
_)
result
(fun result i ->
{
result with
f_coefficients
Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
=
Rust_primitives.Hax.update_at result.f_coefficients
Rust_primitives.Hax.update_at result
.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
i
((self.f_coefficients.[ i ] <: i32) +! (other.f_coefficients.[ i ] <: i32) <: i32)
((self.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32) +.
(other.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32)
<:
i32)
<:
t_KyberPolynomialRingElement
})
in
result
}

let impl_4: Core.Ops.Arith.t_Sub t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
let impl: Core.Ops.Arith.t_Sub t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
{
f_impl_4__Output = t_KyberPolynomialRingElement;
f_impl_4__sub
output = t_KyberPolynomialRingElement;
sub
=
fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) ->
let result:t_KyberPolynomialRingElement = impl__ZERO in
let result:t_KyberPolynomialRingElement = v_ZERO_under_impl in
let result:t_KyberPolynomialRingElement =
Core.Iter.Traits.Iterator.Iterator.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.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
Core.Ops.Range.Range.f_start = 0sz;
Core.Ops.Range.Range.f_end
=
Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT
})
<:
_.f_IntoIter)
_)
result
(fun result i ->
{
result with
f_coefficients
Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
=
Rust_primitives.Hax.update_at result.f_coefficients
Rust_primitives.Hax.update_at result
.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
i
((self.f_coefficients.[ i ] <: i32) -! (other.f_coefficients.[ i ] <: i32) <: i32)
((self.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32) -.
(other.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32)
<:
i32)
<:
t_KyberPolynomialRingElement
})
Expand Down
36 changes: 17 additions & 19 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 @@ -3,15 +3,16 @@ module Libcrux.Kem.Kyber.Compress
open Core

let compress
(#v_COEFFICIENT_BITS: usize)
(#coefficient_bits: usize)
(re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement =
let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement =
{
re with
Libcrux.Kem.Kyber.Arithmetic.f_coefficients
Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
=
Core.Array.impl_23__map re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients
Core.Array.map_under_impl_23 re
.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
(fun coefficient ->
compress_q (Libcrux.Kem.Kyber.Conversions.to_unsigned_representative coefficient <: u16)
<:
Expand All @@ -27,15 +28,16 @@ let decompress
let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement =
{
re with
Libcrux.Kem.Kyber.Arithmetic.f_coefficients
Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
=
Core.Array.impl_23__map re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients
Core.Array.map_under_impl_23 re
.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
(fun coefficient -> decompress_q coefficient bits_per_compressed_coefficient <: i32)
}
in
re

let compress_q (#v_COEFFICIENT_BITS: usize) (fe: u16) : i32 =
let compress_q (#coefficient_bits: usize) (fe: u16) : i32 =
let _:Prims.unit =
if true
then
Expand All @@ -49,15 +51,13 @@ let compress_q (#v_COEFFICIENT_BITS: usize) (fe: u16) : i32 =
in
()
in
let two_pow_bit_size:u32 = 1ul <<! v_COEFFICIENT_BITS in
let compressed:u32 = (cast fe <: u32) *! (two_pow_bit_size <<! 1l <: u32) in
let two_pow_bit_size:u32 = 1ul >>. v_COEFFICIENT_BITS in
let compressed:u32 = cast fe *. (two_pow_bit_size >>. 1l <: u32) in
let compressed:Prims.unit = compressed +. cast Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS in
let compressed:Prims.unit =
compressed +! (cast Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: u32)
compressed /. cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS >>. 1l <: i32)
in
let compressed:Prims.unit =
compressed /! (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <<! 1l <: i32) <: u32)
in
cast (compressed &. (two_pow_bit_size -! 1ul <: u32)) <: i32
cast (compressed &. (two_pow_bit_size -. 1ul <: u32))

let decompress_q (fe: i32) (to_bit_size: usize) : i32 =
let _:Prims.unit =
Expand All @@ -73,9 +73,7 @@ let decompress_q (fe: i32) (to_bit_size: usize) : i32 =
in
()
in
let decompressed:u32 =
(cast fe <: u32) *! (cast Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: u32)
in
let decompressed:u32 = (decompressed <<! 1l <: u32) +! (1ul <<! to_bit_size <: u32) in
let decompressed:Prims.unit = decompressed >>! (to_bit_size +! sz 1 <: usize) in
cast decompressed <: i32
let decompressed:u32 = cast fe *. cast Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS in
let decompressed:u32 = (decompressed >>. 1l <: u32) +. (1ul >>. to_bit_size <: u32) in
let decompressed:Prims.unit = decompressed <<. (to_bit_size +. 1sz <: usize) in
cast decompressed
40 changes: 20 additions & 20 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,15 @@ module Libcrux.Kem.Kyber.Constant_time_ops
open Core

let is_non_zero (value: u8) : u8 =
let value_negated:i8 = Core.Ops.Arith.Neg.neg (cast value <: i8) in
((value |. (cast value_negated <: u8) <: u8) >>! 7l <: u8) &. 1uy
let value_negated:i8 = Core.Ops.Arith.Neg.neg (cast value) in
((value |. cast value_negated <: u8) <<. 7l <: u8) &. 1uy

let compare_ciphertexts_in_constant_time (#v_CIPHERTEXT_SIZE: usize) (lhs rhs: slice u8) : u8 =
let compare_ciphertexts_in_constant_time (#ciphertext_size: usize) (lhs rhs: slice u8) : u8 =
let _:Prims.unit =
if true
then
let _:Prims.unit =
match Core.Slice.impl__len lhs, Core.Slice.impl__len rhs with
match Core.Slice.len_under_impl lhs, Core.Slice.len_under_impl rhs with
| left_val, right_val ->
if ~.(left_val =. right_val <: bool)
then
Expand All @@ -29,7 +29,7 @@ let compare_ciphertexts_in_constant_time (#v_CIPHERTEXT_SIZE: usize) (lhs rhs: s
if true
then
let _:Prims.unit =
match Core.Slice.impl__len lhs, v_CIPHERTEXT_SIZE with
match Core.Slice.len_under_impl lhs, v_CIPHERTEXT_SIZE with
| left_val, right_val ->
if ~.(left_val =. right_val <: bool)
then
Expand All @@ -45,23 +45,23 @@ let compare_ciphertexts_in_constant_time (#v_CIPHERTEXT_SIZE: usize) (lhs rhs: s
in
let (r: u8):u8 = 0uy in
let r:Prims.unit =
Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Core.Ops.Range.f_end = v_CIPHERTEXT_SIZE
Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
Core.Ops.Range.Range.f_start = 0sz;
Core.Ops.Range.Range.f_end = v_CIPHERTEXT_SIZE
})
<:
_.f_IntoIter)
_)
r
(fun r i -> r |. ((lhs.[ i ] <: u8) ^. (rhs.[ i ] <: u8) <: u8) <: Prims.unit)
in
is_non_zero r

let select_shared_secret_in_constant_time (lhs rhs: slice u8) (selector: u8) : array u8 (sz 32) =
let select_shared_secret_in_constant_time (lhs rhs: slice u8) (selector: u8) : array u8 32sz =
let _:Prims.unit =
if true
then
let _:Prims.unit =
match Core.Slice.impl__len lhs, Core.Slice.impl__len rhs with
match Core.Slice.len_under_impl lhs, Core.Slice.len_under_impl rhs with
| left_val, right_val ->
if ~.(left_val =. right_val <: bool)
then
Expand All @@ -79,7 +79,7 @@ let select_shared_secret_in_constant_time (lhs rhs: slice u8) (selector: u8) : a
if true
then
let _:Prims.unit =
match Core.Slice.impl__len lhs, Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE with
match Core.Slice.len_under_impl lhs, Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE with
| left_val, right_val ->
if ~.(left_val =. right_val <: bool)
then
Expand All @@ -93,15 +93,15 @@ let select_shared_secret_in_constant_time (lhs rhs: slice u8) (selector: u8) : a
in
()
in
let mask:u8 = Core.Num.impl_6__wrapping_sub (is_non_zero selector <: u8) 1uy in
let out:array u8 (sz 32) = Rust_primitives.Hax.repeat 0uy (sz 32) in
let out:array u8 (sz 32) =
Core.Iter.Traits.Iterator.Iterator.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_SHARED_SECRET_SIZE
let mask:u8 = Core.Num.wrapping_sub_under_impl_6 (is_non_zero selector <: u8) 1uy in
let out:array u8 32sz = Rust_primitives.Hax.repeat 0uy 32sz in
let out:array u8 32sz =
Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.IntoIterator.into_iter ({
Core.Ops.Range.Range.f_start = 0sz;
Core.Ops.Range.Range.f_end = Libcrux.Kem.Kyber.Constants.v_SHARED_SECRET_SIZE
})
<:
_.f_IntoIter)
_)
out
(fun out i ->
Rust_primitives.Hax.update_at out
Expand All @@ -113,6 +113,6 @@ let select_shared_secret_in_constant_time (lhs rhs: slice u8) (selector: u8) : a
<:
Prims.unit)
<:
array u8 (sz 32))
array u8 32sz)
in
out
14 changes: 7 additions & 7 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Constants.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,18 +4,18 @@ open Core

let v_FIELD_MODULUS: i32 = 3329l

let v_BITS_PER_COEFFICIENT: usize = sz 12
let v_BITS_PER_COEFFICIENT: usize = 12sz

let v_COEFFICIENTS_IN_RING_ELEMENT: usize = sz 256
let v_COEFFICIENTS_IN_RING_ELEMENT: usize = 256sz

let v_BITS_PER_RING_ELEMENT: usize = v_COEFFICIENTS_IN_RING_ELEMENT *! sz 12
let v_BITS_PER_RING_ELEMENT: usize = v_COEFFICIENTS_IN_RING_ELEMENT *. 12sz

let v_BYTES_PER_RING_ELEMENT: usize = v_BITS_PER_RING_ELEMENT /! sz 8
let v_BYTES_PER_RING_ELEMENT: usize = v_BITS_PER_RING_ELEMENT /. 8sz

let v_REJECTION_SAMPLING_SEED_SIZE: usize = sz 168 *! sz 5
let v_REJECTION_SAMPLING_SEED_SIZE: usize = 168sz *. 5sz

let v_SHARED_SECRET_SIZE: usize = sz 32
let v_SHARED_SECRET_SIZE: usize = 32sz

let v_CPA_PKE_KEY_GENERATION_SEED_SIZE: usize = sz 32
let v_CPA_PKE_KEY_GENERATION_SEED_SIZE: usize = 32sz

let v_H_DIGEST_SIZE: usize = Libcrux.Digest.digest_size Libcrux.Digest.Algorithm_Sha3_256_
Loading