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.

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

[ML-KEM] Merge verified code back to main #598

Merged
merged 101 commits into from
Dec 17, 2024
Merged
Show file tree
Hide file tree
Changes from 58 commits
Commits
Show all changes
101 commits
Select commit Hold shift + click to select a range
e6f5c98
Proofs for Ind-cpa and portable compress modules
mamonet Oct 30, 2024
020cd93
Update Cargo.lock
mamonet Oct 30, 2024
7f7e08c
refreshed C code
karthikbhargavan Oct 30, 2024
4b0d787
restored c/cg
karthikbhargavan Oct 30, 2024
18a089c
c code refresh
karthikbhargavan Oct 30, 2024
fb469cb
merged main
karthikbhargavan Nov 1, 2024
cef1e01
regen c files
karthikbhargavan Nov 1, 2024
8067654
Merge pull request #647 from cryspen/dev-cpa-compress
karthikbhargavan Nov 1, 2024
1b88555
Proofs for Ind-cca unpacked functions
mamonet Nov 4, 2024
7ed909f
Remove Ind_cca.Unpacked module from ADMIT_MODULES
mamonet Nov 4, 2024
168a963
boring C refresh
karthikbhargavan Nov 6, 2024
0eabf66
Merge pull request #652 from cryspen/dev-ind-cca-unpacked
karthikbhargavan Nov 6, 2024
38837f1
lax works again
karthikbhargavan Nov 8, 2024
08e01cc
refreshed c
karthikbhargavan Nov 8, 2024
f68ccf2
ml-dsa make
karthikbhargavan Nov 8, 2024
7026b9f
ml-dsa restored
karthikbhargavan Nov 8, 2024
a081805
spec fix
karthikbhargavan Nov 11, 2024
392604e
fstar refresh
karthikbhargavan Nov 11, 2024
5a38a61
fstar
karthikbhargavan Nov 11, 2024
bf1ba73
fstar
karthikbhargavan Nov 11, 2024
9c7d46a
fstar
karthikbhargavan Nov 11, 2024
595517c
fstar
karthikbhargavan Nov 11, 2024
2c93acc
fstar
karthikbhargavan Nov 11, 2024
354e3ef
Fix generic module failures
mamonet Nov 12, 2024
ae7ab07
Update Spec.MLKEM.fst
mamonet Nov 12, 2024
22dc07b
Fix failure in generic serialize module
mamonet Nov 12, 2024
d1b75ab
Fix failure in portable compress module
mamonet Nov 12, 2024
69a27e4
Reomve Libcrux_ml_kem.Vector.Portable from ADMIT_MODULES
mamonet Nov 13, 2024
89568ab
Add pre-conditions for Unpacked functions
mamonet Nov 14, 2024
50e4b97
fix(f*/ml-kem): restore z3rlimit to 80
W95Psp Nov 14, 2024
faee7a5
feat: verify Avx2.Serialize
W95Psp Nov 14, 2024
e42d9da
cleanup
karthikbhargavan Nov 14, 2024
974422b
fstar
karthikbhargavan Nov 14, 2024
3b3cafa
merged main
karthikbhargavan Nov 15, 2024
33f952d
fstar update
karthikbhargavan Nov 16, 2024
63a1e7d
fstar
karthikbhargavan Nov 16, 2024
86e27d8
fixes
karthikbhargavan Nov 27, 2024
82871a3
edits
karthikbhargavan Nov 28, 2024
56e38bb
fix
karthikbhargavan Nov 28, 2024
873fa48
Fix build_unpacked_public_key_mut
mamonet Nov 29, 2024
c2a5c69
Fix build_unpacked_public_key
mamonet Nov 29, 2024
3e8515b
hand edited fixes to impl-interfaces
karthikbhargavan Nov 29, 2024
265435c
Remove lax/panic-free verification options from ind-cca
mamonet Nov 29, 2024
c7df39e
delete stale file
karthikbhargavan Nov 29, 2024
e2b0855
Mark serialize_unpacked_secret_key as lax
mamonet Nov 29, 2024
91fae43
dsa
karthikbhargavan Nov 30, 2024
8fa4c2d
dsa extra
karthikbhargavan Nov 30, 2024
2ecc08a
boring c code
karthikbhargavan Dec 1, 2024
1591860
c code refresh
karthikbhargavan Dec 1, 2024
0a935fe
fstar
karthikbhargavan Dec 1, 2024
5a621c7
Merge pull request #662 from cryspen/dev-merge-main
karthikbhargavan Dec 1, 2024
e7d31cc
drop mlkem pre-verification feature
franziskuskiefer Dec 2, 2024
4c3ea11
update mlkem C code
franziskuskiefer Dec 2, 2024
7fa7712
disable tests that relied on the old ipd mlkem
franziskuskiefer Dec 2, 2024
9d4ad0e
fix acvp mlekm tests
franziskuskiefer Dec 2, 2024
3e54f3c
update C code extraction
franziskuskiefer Dec 2, 2024
470eb78
udpate C extraction
franziskuskiefer Dec 2, 2024
a7104e5
add ignore to mlkem cg glue
franziskuskiefer Dec 2, 2024
fe49cc5
fixing code to address review comments
karthikbhargavan Dec 3, 2024
0e587d6
assert to help proofs
karthikbhargavan Dec 3, 2024
cbc0d48
fmt
karthikbhargavan Dec 3, 2024
fbef364
c code refresh
karthikbhargavan Dec 3, 2024
98f9a92
c code
karthikbhargavan Dec 3, 2024
294c580
fstar
karthikbhargavan Dec 3, 2024
83a72e7
fstar
karthikbhargavan Dec 3, 2024
52178f6
F* update
karthikbhargavan Dec 4, 2024
18c6c50
f* refresh\
karthikbhargavan Dec 4, 2024
bcca540
bitveveq
karthikbhargavan Dec 4, 2024
933ef33
Merge branch 'dev-review-comments' into dev-verification-status
karthikbhargavan Dec 4, 2024
4ac64bc
status
karthikbhargavan Dec 4, 2024
7cb4a1b
Merge pull request #705 from cryspen/dev-review-comments
karthikbhargavan Dec 5, 2024
0d5c258
rlimit
karthikbhargavan Dec 5, 2024
4fe679b
Fix verification
mamonet Dec 6, 2024
0972f98
Fix verification
mamonet Dec 6, 2024
6fe9324
make verification
mamonet Dec 6, 2024
adbf482
fix verification
mamonet Dec 6, 2024
d1a299a
verif status
karthikbhargavan Dec 9, 2024
4d93aa6
Update Makefile
mamonet Dec 10, 2024
c70eb87
Remove AVX2 modules from ADMIT_MODULES
mamonet Dec 10, 2024
2f140ae
Remove admits from vector/avx2.rs
mamonet Dec 10, 2024
ce63901
updated verification status
karthikbhargavan Dec 11, 2024
703cabd
Merge branch 'dev' into dev-verification-status
karthikbhargavan Dec 11, 2024
a197c4d
fmt
karthikbhargavan Dec 11, 2024
d3bc868
c code refresh
karthikbhargavan Dec 11, 2024
b0ff2c5
Put Vector.Rej_sample_table in SLOW_MODULES
mamonet Dec 11, 2024
d1cba65
table for verification status
karthikbhargavan Dec 11, 2024
d8a1a29
linked issue
karthikbhargavan Dec 11, 2024
38cc1db
verif status
karthikbhargavan Dec 11, 2024
578d7f6
raw strings
karthikbhargavan Dec 11, 2024
0953378
raw strings
karthikbhargavan Dec 11, 2024
939e5ea
issue ref
karthikbhargavan Dec 11, 2024
36f84bf
Merge pull request #711 from cryspen/dev-verification-status
karthikbhargavan Dec 11, 2024
0fc11d0
restoring F* extraction
karthikbhargavan Dec 15, 2024
a51b250
c cg fstar refresh
karthikbhargavan Dec 16, 2024
2ce6936
addressed comments
karthikbhargavan Dec 16, 2024
af3367d
Merge pull request #714 from cryspen/dev-merging-main
karthikbhargavan Dec 16, 2024
2ad3090
c code refresh
karthikbhargavan Dec 16, 2024
887cc3c
Merge branch 'main' into dev
franziskuskiefer Dec 16, 2024
2009b0d
Merge branch 'main' into dev
franziskuskiefer Dec 17, 2024
da72c14
c code refresh
karthikbhargavan Dec 17, 2024
07b53c6
removed some unused args and regenerated c anf f*
karthikbhargavan Dec 17, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
16 changes: 8 additions & 8 deletions .github/workflows/mlkem.yml
Original file line number Diff line number Diff line change
Expand Up @@ -85,14 +85,14 @@ jobs:
- name: 🔨 Build
run: |
rustc --print=cfg
cargo build --verbose $RUST_TARGET_FLAG --features pre-verification
cargo build --verbose $RUST_TARGET_FLAG

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

- name: 🏃🏻 Asan MacOS
if: ${{ matrix.os == 'macos-latest' }}
run: RUSTDOCFLAGS=-Zsanitizer=address RUSTFLAGS=-Zsanitizer=address cargo +nightly test --release --target aarch64-apple-darwin --features pre-verification
run: RUSTDOCFLAGS=-Zsanitizer=address RUSTFLAGS=-Zsanitizer=address cargo +nightly test --release --target aarch64-apple-darwin

# - name: ⬆ Upload build
# uses: ./.github/actions/upload_artifacts
Expand Down Expand Up @@ -135,27 +135,27 @@ jobs:
- name: 🏃🏻‍♀️ Test
run: |
cargo clean
cargo test --verbose $RUST_TARGET_FLAG --features pre-verification
cargo test --verbose $RUST_TARGET_FLAG

- name: 🏃🏻‍♀️ Test Release
run: |
cargo clean
cargo test --verbose --release $RUST_TARGET_FLAG --features pre-verification
cargo test --verbose --release $RUST_TARGET_FLAG

- name: 🏃🏻‍♀️ Test Portable
run: |
cargo clean
LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose $RUST_TARGET_FLAG --features pre-verification
LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose $RUST_TARGET_FLAG

- name: 🏃🏻‍♀️ Test Portable Release
run: |
cargo clean
LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose --release $RUST_TARGET_FLAG --features pre-verification
LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose --release $RUST_TARGET_FLAG

- name: 🏃🏻‍♀️ Test Kyber
run: |
cargo clean
cargo test --features pre-verification,kyber --verbose $RUST_TARGET_FLAG
cargo test ,kyber --verbose $RUST_TARGET_FLAG

- name: 🏃🏻‍♀️ Cargo Check Features
if: ${{ matrix.bits == 64 }}
Expand Down
Loading
Loading