Skip to content

Commit

Permalink
Merge pull request #149 from cryspen/franziskus/hacl-sha3-mb
Browse files Browse the repository at this point in the history 
Use hacl sha3 mb
  • Loading branch information
@franziskuskiefer
franziskuskiefer authored Dec 7, 2023
2 parents 945f16e + 415a4f0 commit 456b566
Show file tree
Hide file tree
Showing 53 changed files with 27,478 additions and 1,672 deletions.
10 changes: 5 additions & 5 deletions Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ members = [
]

[workspace.package]
version = "0.0.2-pre.1"
version = "0.0.2-pre.2"
authors = ["Cryspen"]
license = "Apache-2.0"
homepage = "https://github.com/cryspen/libcrux"
Expand All @@ -34,11 +34,11 @@ exclude = ["/tests", "/specs"]
crate-type = ["staticlib", "cdylib", "lib"]

[build-dependencies]
libcrux-platform = { version = "=0.0.2-pre.1", path = "sys/platform" }
libcrux-platform = { version = "=0.0.2-pre.2", path = "sys/platform" }

[dependencies]
libcrux-hacl = { version = "=0.0.2-pre.1", path = "sys/hacl" }
libcrux-platform = { version = "=0.0.2-pre.1", path = "sys/platform" }
libcrux-hacl = { version = "=0.0.2-pre.2", path = "sys/hacl" }
libcrux-platform = { version = "=0.0.2-pre.2", path = "sys/platform" }
rand = { version = "0.8" }
log = { version = "0.4", optional = true }
# WASM API
Expand All @@ -55,7 +55,7 @@ hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/ha
getrandom = { version = "0.2", features = ["js"] }

[target.'cfg(all(not(target_os = "windows"), target_arch = "x86_64"))'.dependencies]
libjade-sys = { version = "=0.0.2-pre.1", path = "sys/libjade" }
libjade-sys = { version = "=0.0.2-pre.2", path = "sys/libjade" }

[dev-dependencies]
libcrux = { path = ".", features = ["rand"] }
Expand Down
9 changes: 9 additions & 0 deletions PUBLISHING.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
# Release Management

1. Update version in `Cargo.toml` and set all dependencies to that version. Always start with a prerelease version `-pre.A` before doing a full release.
2. Tag the version `git tag vX.Y.Z` and `git push origin vX.Y.Z`.
3. Release crates
1. libcrux-platform in `sys/platform`
2. libcrux-hacl in `sys/hacl`
3. libjade-sys in `sys/libjade`
4. libcrux
2 changes: 2 additions & 0 deletions proofs/fstar/extraction/Libcrux.Digest.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,4 +36,6 @@ val sha3_512_ (payload: t_Slice u8) : t_Array u8 (sz 64)

val shake128 (v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN

val shake128x4 (v_LEN: usize) (data0: t_Slice u8) (data1: t_Slice u8) (data2: t_Slice u8) (data3: t_Slice u8): (t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN & t_Array u8 v_LEN)

val shake256 (v_LEN: usize) (data: t_Slice u8) : t_Array u8 v_LEN
111 changes: 88 additions & 23 deletions proofs/fstar/extraction/Libcrux.Kem.Kyber.Hash_functions.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,31 +10,96 @@ let v_H (input: t_Slice u8) : t_Array u8 (sz 32) = Libcrux.Digest.sha3_256_ inpu
let v_PRF (v_LEN: usize) (input: t_Slice u8) : t_Array u8 v_LEN =
Libcrux.Digest.shake256 v_LEN input

let v_XOFx4 (v_LEN v_K: usize) (input: t_Array (t_Array u8 (sz 34)) v_K)
: t_Array (t_Array u8 v_LEN) v_K =
let out:t_Array (t_Array u8 v_LEN) v_K =
Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat 0uy v_LEN <: t_Array u8 v_LEN) v_K
let v_XOFx4 (v_K: usize) (input: t_Array (t_Array u8 (sz 34)) v_K)
: t_Array (t_Array u8 (sz 840)) v_K =
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.repeat (Rust_primitives.Hax.repeat 0uy (sz 840) <: t_Array u8 (sz 840)) v_K
in
let out:t_Array (t_Array u8 v_LEN) 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)
<:
Core.Ops.Range.t_Range usize)
out
(fun out i ->
let out:t_Array (t_Array u8 v_LEN) v_K = out in
let i:usize = i in
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
i
(Libcrux.Digest.shake128 v_LEN
(Rust_primitives.unsize (input.[ i ] <: t_Array u8 (sz 34)) <: t_Slice u8)
let out:t_Array (t_Array u8 (sz 840)) v_K =
if ~.(Libcrux_platform.simd256_support <: bool) || ~.false
then
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
}
<:
t_Array u8 v_LEN)
Core.Ops.Range.t_Range usize)
<:
t_Array (t_Array u8 v_LEN) v_K)
Core.Ops.Range.t_Range usize)
out
(fun out i ->
let out:t_Array (t_Array u8 (sz 840)) v_K = out in
let i:usize = i in
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out
i
(Libcrux.Digest.shake128 (sz 840)
(Rust_primitives.unsize (input.[ i ] <: t_Array u8 (sz 34)) <: t_Slice u8)
<:
t_Array u8 (sz 840))
<:
t_Array (t_Array u8 (sz 840)) v_K)
else
let out:t_Array (t_Array u8 (sz 840)) v_K =
match cast (v_K <: usize) <: u8 with
| 2uy ->
let d0, d1, _, _:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
t_Array u8 (sz 840)) =
Libcrux.Digest.shake128x4 (sz 840)
(Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 0) d0
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 1) d1
in
out
| 3uy ->
let d0, d1, d2, _:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
t_Array u8 (sz 840)) =
Libcrux.Digest.shake128x4 (sz 840)
(Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 2 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 0) d0
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 1) d1
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 2) d2
in
out
| 4uy ->
let d0, d1, d2, d3:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
t_Array u8 (sz 840)) =
Libcrux.Digest.shake128x4 (sz 840)
(Rust_primitives.unsize (input.[ sz 0 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 1 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 2 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
(Rust_primitives.unsize (input.[ sz 3 ] <: t_Array u8 (sz 34)) <: t_Slice u8)
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 0) d0
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 1) d1
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 2) d2
in
let out:t_Array (t_Array u8 (sz 840)) v_K =
Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out (sz 3) d3
in
out
| _ -> out
in
out
in
out
2 changes: 1 addition & 1 deletion proofs/fstar/extraction/Libcrux.Kem.Kyber.Matrix.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -494,7 +494,7 @@ let sample_matrix_A (v_K: usize) (seed: t_Array u8 (sz 34)) (transpose: bool)
seeds)
in
let xof_bytes:t_Array (t_Array u8 (sz 840)) v_K =
Libcrux.Kem.Kyber.Hash_functions.v_XOFx4 (sz 840) v_K seeds
Libcrux.Kem.Kyber.Hash_functions.v_XOFx4 v_K seeds
in
Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
Core.Ops.Range.f_start = sz 0;
Expand Down
4 changes: 4 additions & 0 deletions proofs/fstar/extraction/Libcrux_platform.fsti
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module Libcrux_platform
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

val simd256_support: bool
1 change: 1 addition & 0 deletions proofs/fstar/extraction/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ all:


VERIFIED = \
Libcrux_platform.fsti \
Libcrux.Kem.fst \
Libcrux.Kem.Kyber.Constants.fst \
Libcrux.Digest.fsti \
Expand Down
2 changes: 1 addition & 1 deletion specs/kyber/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ version = "0.1.0"
edition = "2021"

[dependencies]
libcrux = { version = "=0.0.2-pre.1", path = "../../" }
libcrux = { version = "=0.0.2-pre.2", path = "../../" }
hacspec-lib = { version = "0.0.1", path = "../hacspec-lib" }

[dev-dependencies]
Expand Down
78 changes: 43 additions & 35 deletions specs/kyber/proofs/fstar/extraction/Hacspec_kyber.Compress.fst
View file
Original file line number Diff line number Diff line change
@@ -1,23 +1,29 @@
module Hacspec_kyber.Compress
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

let decompress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size: usize)
: Hacspec_lib.Field.t_PrimeFieldElement 3329us =
let _:Prims.unit =
if ~.(to_bit_size <=. Hacspec_kyber.Parameters.v_BITS_PER_COEFFICIENT <: bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= parameters::BITS_PER_COEFFICIENT"

let compress
(re:
Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
(sz 256))
(bits_per_compressed_coefficient: usize)
: Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
(sz 256) =
Hacspec_lib.Ring.impl_2__new (Core.Array.impl_23__map (Hacspec_lib.Ring.impl_2__coefficients re
<:
t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
(fun coefficient ->
compress_d coefficient bits_per_compressed_coefficient
<:
Hacspec_lib.Field.t_PrimeFieldElement 3329us)
Rust_primitives.Hax.t_Never)
in
let decompressed:u32 =
(((2ul *! (Core.Convert.f_from fe.Hacspec_lib.Field.f_value <: u32) <: u32) *!
(Core.Convert.f_from Hacspec_lib.Field.impl_2__MODULUS_1 <: u32)
<:
u32) +!
(1ul <<! to_bit_size <: u32)
<:
t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
u32) >>!
(to_bit_size +! sz 1 <: usize)
in
Core.Convert.f_into decompressed

let decompress
(re:
Expand All @@ -26,10 +32,13 @@ let decompress
(bits_per_compressed_coefficient: usize)
: Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
(sz 256) =
Hacspec_lib.Ring.impl_2__new (Core.Array.impl_23__map (Hacspec_lib.Ring.impl_2__coefficients re
Hacspec_lib.Ring.impl_2__new (sz 256)
(Core.Array.impl_23__map (sz 256)
(Hacspec_lib.Ring.impl_2__coefficients (sz 256) re
<:
t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
(fun coefficient ->
let coefficient:Hacspec_lib.Field.t_PrimeFieldElement 3329us = coefficient in
decompress_d coefficient bits_per_compressed_coefficient
<:
Hacspec_lib.Field.t_PrimeFieldElement 3329us)
Expand All @@ -51,7 +60,8 @@ let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size:
(Core.Result.impl__unwrap_or_else (Core.Convert.f_try_into to_bit_size
<:
Core.Result.t_Result u32 Core.Num.Error.t_TryFromIntError)
(fun _ ->
(fun temp_0_ ->
let _:Core.Num.Error.t_TryFromIntError = temp_0_ in
Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize
(let list =
[
Expand Down Expand Up @@ -95,24 +105,22 @@ let compress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size:
in
Core.Convert.f_into (compressed %! two_pow_bit_size <: u32)

let decompress_d (fe: Hacspec_lib.Field.t_PrimeFieldElement 3329us) (to_bit_size: usize)
: Hacspec_lib.Field.t_PrimeFieldElement 3329us =
let _:Prims.unit =
if ~.(to_bit_size <=. Hacspec_kyber.Parameters.v_BITS_PER_COEFFICIENT <: bool)
then
Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= parameters::BITS_PER_COEFFICIENT"

let compress
(re:
Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
(sz 256))
(bits_per_compressed_coefficient: usize)
: Hacspec_lib.Ring.t_PolynomialRingElement (Hacspec_lib.Field.t_PrimeFieldElement 3329us)
(sz 256) =
Hacspec_lib.Ring.impl_2__new (sz 256)
(Core.Array.impl_23__map (sz 256)
(Hacspec_lib.Ring.impl_2__coefficients (sz 256) re
<:
Rust_primitives.Hax.t_Never)
in
let decompressed:u32 =
(((2ul *! (Core.Convert.f_from fe.Hacspec_lib.Field.f_value <: u32) <: u32) *!
(Core.Convert.f_from Hacspec_lib.Field.impl_2__MODULUS_1 <: u32)
<:
u32) +!
(1ul <<! to_bit_size <: u32)
t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
(fun coefficient ->
let coefficient:Hacspec_lib.Field.t_PrimeFieldElement 3329us = coefficient in
compress_d coefficient bits_per_compressed_coefficient
<:
Hacspec_lib.Field.t_PrimeFieldElement 3329us)
<:
u32) >>!
(to_bit_size +! sz 1 <: usize)
in
Core.Convert.f_into decompressed
t_Array (Hacspec_lib.Field.t_PrimeFieldElement 3329us) (sz 256))
Loading

0 comments on commit 456b566

Please sign in to comment.