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

Make unpacked ML-KEM API extractable #586

Merged
merged 20 commits into from
Sep 17, 2024
Merged

Make unpacked ML-KEM API extractable #586

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
76a08da
wip
franziskuskiefer Sep 10, 2024
08a3cad
updated unpacked api
franziskuskiefer Sep 10, 2024
16c5cbb
serialize functions for unpacked keys
franziskuskiefer Sep 11, 2024
e992824
serialize functions for unpacked and C
franziskuskiefer Sep 11, 2024
28acae7
minor tweak
msprotz Sep 12, 2024
f4cf47e
wip
msprotz Sep 12, 2024
f07d78f
wip
msprotz Sep 12, 2024
e889dcc
updated cg.yaml
franziskuskiefer Sep 13, 2024
af73d01
unpacked API for cg
franziskuskiefer Sep 15, 2024
1187505
drop unpacked feature
franziskuskiefer Sep 16, 2024
1e523e8
update C code
franziskuskiefer Sep 16, 2024
4072680
update F*
franziskuskiefer Sep 16, 2024
422ff05
Merge branch 'main' into franziskus/mlkem-usable-unpacked
franziskuskiefer Sep 16, 2024
866aace
remove unpacked job from ci
franziskuskiefer Sep 16, 2024
f06414b
work around hax issues
franziskuskiefer Sep 16, 2024
521b98d
update docker image for C extraction
franziskuskiefer Sep 16, 2024
97f7cef
fix kyber
franziskuskiefer Sep 16, 2024
65d06b7
update C extraction
franziskuskiefer Sep 16, 2024
89b109d
update C clang-format
franziskuskiefer Sep 16, 2024
30f0fb3
remove commented code in self.rs
franziskuskiefer Sep 17, 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
12 changes: 6 additions & 6 deletions .docker/c/ext-tools.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,23 +4,23 @@ set -v -e -x

source $HOME/.profile

curl -L https://github.com/AeneasVerif/charon/archive/b351338f6a84c7a1afc27433eb0ffdc668b3581d.zip \
curl -L https://github.com/AeneasVerif/charon/archive/28d543bfacc902ba9cc2a734b76baae9583892a4.zip \
--output charon.zip
unzip charon.zip
rm -rf charon.zip
mv charon-b351338f6a84c7a1afc27433eb0ffdc668b3581d/ charon
mv charon-28d543bfacc902ba9cc2a734b76baae9583892a4/ charon

curl -L https://github.com/FStarLang/karamel/archive/c96fb69d15693284644d6aecaa90afa37e4de8f0.zip \
curl -L https://github.com/FStarLang/karamel/archive/15d4bce74a2d43e34a64f48f8311b7d9bcb0e152.zip \
--output karamel.zip
unzip karamel.zip
rm -rf karamel.zip
mv karamel-c96fb69d15693284644d6aecaa90afa37e4de8f0/ karamel
mv karamel-15d4bce74a2d43e34a64f48f8311b7d9bcb0e152/ karamel

curl -L https://github.com/AeneasVerif/eurydice/archive/7efec1624422fd5e94388ef06b9c76dfe7a48d46.zip \
curl -L https://github.com/AeneasVerif/eurydice/archive/1a65dbf3758fe310833718c645a64266294a29ac.zip \
--output eurydice.zip
unzip eurydice.zip
rm -rf eurydice.zip
mv eurydice-7efec1624422fd5e94388ef06b9c76dfe7a48d46/ eurydice
mv eurydice-1a65dbf3758fe310833718c645a64266294a29ac/ eurydice

echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile
Expand Down
5 changes: 0 additions & 5 deletions .github/workflows/mlkem.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,11 +87,6 @@ jobs:
rustc --print=cfg
cargo build --verbose $RUST_TARGET_FLAG --features pre-verification

- name: 🔨 Build unpacked
run: |
rustc --print=cfg
cargo build --verbose $RUST_TARGET_FLAG --features pre-verification,unpacked

- name: 🔨 Build Release
run: cargo build --verbose --release $RUST_TARGET_FLAG --features pre-verification

Expand Down
55 changes: 55 additions & 0 deletions libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,23 +3,39 @@ module Libcrux_intrinsics.Avx2_extract
open Core
open FStar.Mul

val mm256_abs_epi32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_add_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_add_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_add_epi64 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_and_si256 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_andnot_si256 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_blend_epi16 (v_CONTROL: i32) (lhs rhs: u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_blend_epi32 (v_CONTROL: i32) (lhs rhs: u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_bsrli_epi128 (v_SHIFT_BY: i32) (x: u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_castsi128_si256 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_castsi256_ps (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_castsi256_si128 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_cmpeq_epi32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_cmpgt_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_cmpgt_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_cvtepi16_epi32 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_extracti128_si256 (v_CONTROL: i32) (vector: u8)
Expand All @@ -30,10 +46,16 @@ val mm256_inserti128_si256 (v_CONTROL: i32) (vector vector_i128: u8)

val mm256_loadu_si256_i16 (input: t_Slice i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_loadu_si256_i32 (input: t_Slice i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_loadu_si256_u8 (input: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_madd_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_movemask_ps (a: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)

val mm256_mul_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_mul_epu32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_mulhi_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
Expand All @@ -42,6 +64,8 @@ val mm256_mullo_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims

val mm256_mullo_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_or_si256 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_packs_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_permute2x128_si256 (v_IMM8: i32) (a b: u8)
Expand All @@ -67,18 +91,25 @@ val mm256_set_epi16
val mm256_set_epi32 (input7 input6 input5 input4 input3 input2 input1 input0: i32)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_set_epi64x (input3 input2 input1 input0: i64)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_set_epi8
(byte31 byte30 byte29 byte28 byte27 byte26 byte25 byte24 byte23 byte22 byte21 byte20 byte19 byte18 byte17 byte16 byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0:
i8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_set_m128i (hi lo: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_setzero_si256: Prims.unit -> Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_shuffle_epi32 (v_CONTROL: i32) (vector: u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_shuffle_epi8 (vector control: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_sign_epi32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_slli_epi16 (v_SHIFT_BY: i32) (vector: u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

Expand All @@ -104,14 +135,25 @@ val mm256_srli_epi32 (v_SHIFT_BY: i32) (vector: u8)
val mm256_srli_epi64 (v_SHIFT_BY: i32) (vector: u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_srlv_epi32 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_srlv_epi64 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_storeu_si256_i16 (output: t_Slice i16) (vector: u8)
: Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)

val mm256_storeu_si256_i32 (output: t_Slice i32) (vector: u8)
: Prims.Pure (t_Slice i32) Prims.l_True (fun _ -> Prims.l_True)

val mm256_storeu_si256_u8 (output: t_Slice u8) (vector: u8)
: Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

val mm256_sub_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_sub_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_testz_si256 (lhs rhs: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)

val mm256_unpackhi_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm256_unpackhi_epi64 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
Expand All @@ -136,17 +178,30 @@ val mm_packs_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_

val mm_set1_epi16 (constant: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm_set_epi32 (input3 input2 input1 input0: i32)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm_set_epi8
(byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0:
u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm_shuffle_epi8 (vector control: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm_sllv_epi32 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm_srli_epi64 (v_SHIFT_BY: i32) (vector: u8)
: Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val mm_storeu_bytes_si128 (output: t_Slice u8) (vector: u8)
: Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

val mm_storeu_si128 (output: t_Slice i16) (vector: u8)
: Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)

val mm_storeu_si128_i32 (output: t_Slice i32) (vector: u8)
: Prims.Pure (t_Slice i32) Prims.l_True (fun _ -> Prims.l_True)

val mm_sub_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val vec256_blendv_epi32 (a b mask: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
5 changes: 1 addition & 4 deletions libcrux-ml-kem/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,9 +47,6 @@ mlkem512 = []
mlkem768 = []
mlkem1024 = []

# Enable the unpacked API
unpacked = []

# Enable Round 3 Kyber in addition to ML-KEM
kyber = []

Expand Down Expand Up @@ -86,7 +83,7 @@ name = "keygen"
required-features = ["mlkem768"]

[package.metadata."docs.rs"]
features = ["pre-verification", "kyber", "unpacked"]
features = ["pre-verification", "kyber"]
rustdoc-args = ["--cfg", "doc_cfg"]

[lints.rust]
Expand Down
Loading
Loading