Skip to content

Commit

Permalink
workaround hax F* extraction issue with usize
Browse files Browse the repository at this point in the history
  • Loading branch information
@franziskuskiefer
franziskuskiefer committed Oct 9, 2023
1 parent f0aaecf commit 638c2d9
Show file tree
Hide file tree
Showing 26 changed files with 1,905 additions and 1,391 deletions.
7 changes: 3 additions & 4 deletions extract_to_fstar.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,9 +18,7 @@ def shell(command, expect=0, cwd=None, format_selection_string=False):

print("\nDirectory: {}".format(cwd))

ret = subprocess.run(
command, stdout=subprocess.PIPE, stderr=subprocess.PIPE, cwd=cwd
)
ret = subprocess.run(command, cwd=cwd)
if ret.returncode != expect:
raise Exception("Error {}. Expected {}.".format(ret, expect))

Expand Down Expand Up @@ -72,7 +70,8 @@ def shell(command, expect=0, cwd=None, format_selection_string=False):
options.modules = " {}".format(options.modules)

if options.functions:
options.functions = " ".join(["+" + function for function in options.functions])
options.functions = " ".join(
["+" + function for function in options.functions])
options.functions = " {}".format(options.functions)

shell(
Expand Down
38 changes: 38 additions & 0 deletions proofs/fstar/extraction/Libcrux.Digest.fst
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
module Libcrux.Digest
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core

type t_Algorithm =
| Algorithm_Sha1 : t_Algorithm
| Algorithm_Sha224 : t_Algorithm
| Algorithm_Sha256 : t_Algorithm
| Algorithm_Sha384 : t_Algorithm
| Algorithm_Sha512 : t_Algorithm
| Algorithm_Blake2s : t_Algorithm
| Algorithm_Blake2b : t_Algorithm
| Algorithm_Sha3_224_ : t_Algorithm
| Algorithm_Sha3_256_ : t_Algorithm
| Algorithm_Sha3_384_ : t_Algorithm
| Algorithm_Sha3_512_ : t_Algorithm

let digest_size (mode: t_Algorithm) : usize =
match mode with
| Algorithm_Sha1 -> sz 20
| Algorithm_Sha224 -> sz 28
| Algorithm_Sha256 -> sz 32
| Algorithm_Sha384 -> sz 48
| Algorithm_Sha512 -> sz 64
| Algorithm_Blake2s -> sz 32
| Algorithm_Blake2b -> sz 64
| Algorithm_Sha3_224_ -> sz 28
| Algorithm_Sha3_256_ -> sz 32
| Algorithm_Sha3_384_ -> sz 48
| Algorithm_Sha3_512_ -> sz 64

let sha3_256_ (payload: slice u8) : array u8 (sz 32) = Libcrux.Hacl.Sha3.sha256 payload

let sha3_512_ (payload: slice u8) : array u8 (sz 64) = Libcrux.Hacl.Sha3.sha512 payload

let shake128 (#v_LEN: usize) (data: slice u8) : array u8 v_LEN = Libcrux.Hacl.Sha3.shake128 data

let shake256 (#v_LEN: usize) (data: slice u8) : array u8 v_LEN = Libcrux.Hacl.Sha3.shake256 data
39 changes: 39 additions & 0 deletions proofs/fstar/extraction/Libcrux.Hacl.Sha3.fst
View file

Large diffs are not rendered by default.

118 changes: 43 additions & 75 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,140 +2,108 @@ 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.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 (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 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 256sz }
type t_KyberPolynomialRingElement = { f_coefficients:array i32 (sz 256) }

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

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

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

let impl: Core.Ops.Arith.t_Add t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
let impl_3: Core.Ops.Arith.t_Add t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
{
output = t_KyberPolynomialRingElement;
add
f_impl_3__Output = t_KyberPolynomialRingElement;
f_impl_3__add
=
fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) ->
let result:t_KyberPolynomialRingElement = v_ZERO_under_impl in
let result:t_KyberPolynomialRingElement = impl__ZERO in
let result:t_KyberPolynomialRingElement =
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
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
})
<:
_)
_.f_IntoIter)
result
(fun result i ->
{
result with
Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
f_coefficients
=
Rust_primitives.Hax.update_at result
.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
Rust_primitives.Hax.update_at result.f_coefficients
i
((self.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32) +.
(other.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32)
<:
i32)
((self.f_coefficients.[ i ] <: i32) +! (other.f_coefficients.[ i ] <: i32) <: i32)
<:
t_KyberPolynomialRingElement
})
in
result
}

let impl: Core.Ops.Arith.t_Sub t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
let impl_4: Core.Ops.Arith.t_Sub t_KyberPolynomialRingElement t_KyberPolynomialRingElement =
{
output = t_KyberPolynomialRingElement;
sub
f_impl_4__Output = t_KyberPolynomialRingElement;
f_impl_4__sub
=
fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) ->
let result:t_KyberPolynomialRingElement = v_ZERO_under_impl in
let result:t_KyberPolynomialRingElement = impl__ZERO in
let result:t_KyberPolynomialRingElement =
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
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
})
<:
_)
_.f_IntoIter)
result
(fun result i ->
{
result with
Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
f_coefficients
=
Rust_primitives.Hax.update_at result
.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients
Rust_primitives.Hax.update_at result.f_coefficients
i
((self.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32) -.
(other.Libcrux.Kem.Kyber.Arithmetic.KyberPolynomialRingElement.f_coefficients.[ i
]
<:
i32)
<:
i32)
((self.f_coefficients.[ i ] <: i32) -! (other.f_coefficients.[ i ] <: i32) <: i32)
<:
t_KyberPolynomialRingElement
})
Expand Down
44 changes: 25 additions & 19 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,16 +3,15 @@ module Libcrux.Kem.Kyber.Compress
open Core

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

let compress_q (#coefficient_bits: usize) (fe: u16) : i32 =
let compress_q (#v_COEFFICIENT_BITS: u32) (fe: u16) : i32 =
let _:Prims.unit =
if true
then
let _:Prims.unit =
if ~.(v_COEFFICIENT_BITS <=. Libcrux.Kem.Kyber.Constants.v_BITS_PER_COEFFICIENT <: bool)
if
~.((cast v_COEFFICIENT_BITS <: usize) <=.
Libcrux.Kem.Kyber.Constants.v_BITS_PER_COEFFICIENT
<:
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 as usize <= BITS_PER_COEFFICIENT"

<:
Rust_primitives.Hax.t_Never)
in
()
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 two_pow_bit_size:u32 = 1ul <<! v_COEFFICIENT_BITS in
let compressed:u32 = (cast fe <: u32) *! (two_pow_bit_size <<! 1l <: u32) in
let compressed:Prims.unit =
compressed +! (cast Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: u32)
in
let compressed:Prims.unit =
compressed /. cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS >>. 1l <: i32)
compressed /! (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <<! 1l <: i32) <: u32)
in
cast (compressed &. (two_pow_bit_size -. 1ul <: u32))
cast (compressed &. (two_pow_bit_size -! 1ul <: u32)) <: i32

let decompress_q (fe: i32) (to_bit_size: usize) : i32 =
let _:Prims.unit =
Expand All @@ -73,7 +77,9 @@ let decompress_q (fe: i32) (to_bit_size: usize) : i32 =
in
()
in
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
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
Loading

0 comments on commit 638c2d9

Please sign in to comment.