-
Notifications
You must be signed in to change notification settings - Fork 13
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
Draft
karthikbhargavan
wants to merge
407
commits into
main
Choose a base branch
from
dev
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Changes from 250 commits
Commits
Show all changes
407 commits
Select commit
Hold shift + click to select a range
1628ec4
Make avx2 arithmetic.rs compress.rs ntt.rs panic-free
mamonet e326838
wip
W95Psp 2212e8c
more specs
karthikbhargavan 1655f6e
merged
karthikbhargavan f623c89
merged
karthikbhargavan dad7a37
fstar
karthikbhargavan 73c17b3
fixes
karthikbhargavan 22a1ced
cleanup
karthikbhargavan b702c3f
verification is back
karthikbhargavan 1012a58
attempts to restore c extraction
karthikbhargavan 31e4417
Make avx2 sampling.rs panic-free
mamonet 4f51921
Merge pull request #538 from cryspen/vector-spec
karthikbhargavan 57b2977
wip
W95Psp 2a5a84e
wip, working tactic
W95Psp 3e71e68
cca
karthikbhargavan b03baf1
decap to lax
karthikbhargavan 1ecfc74
decap panic free
karthikbhargavan 293f3b5
c code
karthikbhargavan 9201ec6
refreshed c and fstar
karthikbhargavan 084040f
Merge pull request #541 from cryspen/dev-ind-cca-fix
karthikbhargavan b934c24
wip
W95Psp 48fad7e
more
W95Psp e43bc13
Merge branch 'dev' into lf-more-serialize-proofs
W95Psp aaafdfc
norm array_of_list
W95Psp d1bbc2a
reduce f_elements
W95Psp b528d43
math proofs
karthikbhargavan 84795a2
Update serialize.rs
mamonet 3a21d67
verif
karthikbhargavan e46edf3
Update and improve `Makefile`s
W95Psp 0fb14cb
Reintroduce BitVecEq from previous proofs
W95Psp 8feb781
intro tactic library to do hybrid norm/rewrite inside terms
W95Psp 47177fe
Kill `let mut`, use array literal instead
W95Psp 77fe334
Serialization pre/post in vector/traits.rs + spec in *Math.fst
W95Psp 37cab51
hax
karthikbhargavan 7cd7a08
c code
karthikbhargavan 2e5a142
gitignore
W95Psp ff0e6ad
intrinsics
W95Psp bfeeda3
partial proofs
W95Psp 7c4e54b
avx2: serialize: manual proofs
W95Psp dd063cc
portable: serialize: manual proofs
W95Psp 64a2732
makefile, more fixes
W95Psp bab1d08
c code
karthikbhargavan 8d9d191
Merge pull request #548 from cryspen/dev-bounded-poly
karthikbhargavan 0de2f94
stabilize ind-cca
karthikbhargavan a5eeb0b
Merge branch 'dev' into dev-arithmetic-proofs
karthikbhargavan bc45818
arith
karthikbhargavan 7b03687
portable/arithmetic
karthikbhargavan b6cb1c4
avx2 arithmetic
karthikbhargavan 8a8e806
Add lemmas for Portable serialize/deserialize functions
mamonet ea8f110
Comment out pre/post-conditions for serialize fun in vector/traits.rs
mamonet c8b2d7e
Fix return array in serialize_1
mamonet 3635503
Fix fstar::replace for mm256_srli_epi16
mamonet 10b4615
Update extracted F* files for intrinsics and ml-kem
mamonet 89af067
wip
karthikbhargavan 133225f
wip
karthikbhargavan 56eed0a
verifying
karthikbhargavan ec6b25a
Merge pull request #550 from cryspen/lf-more-serilize-proofs-2
karthikbhargavan aa003c8
fmt
karthikbhargavan 87ab89d
fstar feat
karthikbhargavan db6b548
Merge pull request #549 from cryspen/lf-tactics-serialize
karthikbhargavan 894d5ee
arithmetic
karthikbhargavan 11c8589
wip
karthikbhargavan 33d08ed
Merge branch 'dev' into vector-spec-sampling-pf
karthikbhargavan 0ad4043
Use z3refresh on tactic calls for serialize.rs
mamonet 37d4f52
makefile: add a `SLOW_MODULES` variable
W95Psp 61a2488
refreshed c code
karthikbhargavan 38c246d
new eurydice_glue
karthikbhargavan 985a794
Merge pull request #539 from cryspen/vector-spec-sampling-pf
karthikbhargavan 579a042
mont spec
karthikbhargavan 2689950
verified
karthikbhargavan e86a762
Merge branch 'dev' into dev-arithmetic-proofs
karthikbhargavan 87f0789
z3 limits for montred
karthikbhargavan 65df9ca
Add pre/post-conditions for portable serialize/deserialize
mamonet bfd737a
ntt
karthikbhargavan b7b237f
Update vector/avx2.rs
mamonet c04abb6
Remove unsafe code from include to avoid being rejected by hax.
maximebuyse 481b7dc
Update MLKEM Makefile
mamonet 24d98fb
Merge remote-tracking branch 'origin/dev' into lf-more-serialize-proofs
mamonet e945931
Update Cargo.lock
mamonet 5bd655e
Remove unnecessary files
mamonet be21196
Remove unsafe code from include to avoid being rejected by hax.
maximebuyse 3183572
Update MLKEM Makefile
mamonet cadb420
Merge branch 'dev-constant-time' of https://github.com/cryspen/libcru…
mamonet 1b7fe71
ntt wip
karthikbhargavan b6df944
Merge pull request #551 from cryspen/lf-more-serialize-proofs
karthikbhargavan bd25135
Remove unsafe code from include to avoid being rejected by hax.
maximebuyse 705320f
wip
W95Psp 574a60b
feat: tactic: do nothing if smt queries are admitted
W95Psp 16af53b
serialize
karthikbhargavan 9be19e9
feat: tactic: do nothing if smt queries are admitted
W95Psp e6aa9af
Backport proof for compare in constant_time_ops
mamonet 4b5a63b
Backport proofs for constant_time_ops.rs
mamonet 7dc12e9
port
karthikbhargavan 2d5878d
arith wip
karthikbhargavan af7a337
merged
karthikbhargavan 9b026b5
merged
karthikbhargavan b01cd8c
Remove curly brackets from Tactics.GetBit.fst
mamonet a259ee4
Merge branch 'dev' into dev-constant-time
karthikbhargavan 0907ca1
Mark functions at samplings.rs and serialize.rs as lax
mamonet 3eb8ac8
Make two functions in sampling.rs panic-free
mamonet a8e27d4
Make remaining functions in sampling.rs panic-free
mamonet 3ee84f3
Fix verifying ZETAS_TIMES_MONTGOMERY_R
mamonet 2b4497b
wip
karthikbhargavan ef7dcf2
updated hax and fstar extraction
karthikbhargavan 97fc0f7
cargo
karthikbhargavan 5100963
cargo
karthikbhargavan 5f60d88
removed new F* feature use
karthikbhargavan 6284a1e
seq
karthikbhargavan e2a1da0
Merge pull request #570 from cryspen/dev-generic-cleanup
karthikbhargavan 277b1ff
feat: tactic: do nothing if smt queries are admitted
W95Psp 5cb76a3
fixing c extraction
karthikbhargavan 3782ca7
regen
karthikbhargavan 9799c05
workflow fix
karthikbhargavan 26dc5e5
hax lib
karthikbhargavan b6d5636
cargo fix
karthikbhargavan 89225f5
lock
karthikbhargavan 1f4aea1
c code refresh
karthikbhargavan ae845b0
retry with pinned eurydice
karthikbhargavan 2db9db9
updated intrin
karthikbhargavan c4afd33
updated intrin
karthikbhargavan 0437f70
fix build and hax
karthikbhargavan 831bd69
fixed glue for Some/None
karthikbhargavan 2c21fef
Mark functions at samplings.rs and serialize.rs as lax
mamonet 57b83e2
Make two functions in sampling.rs panic-free
karthikbhargavan aa958de
Make remaining functions in sampling.rs panic-free
mamonet 14564df
Fix verifying ZETAS_TIMES_MONTGOMERY_R
karthikbhargavan 367d23c
updated hax and fstar extraction
karthikbhargavan 8d2620c
cargo
karthikbhargavan 7519c45
cargo
karthikbhargavan 505bead
removed new F* feature use
karthikbhargavan 7e22223
seq
karthikbhargavan 415ed4c
updated intrin
karthikbhargavan b4a143f
refresh
karthikbhargavan 07c5cbc
glue diff
karthikbhargavan 5c2056b
Merge branch 'dev' into fix-c-extraction
karthikbhargavan 162bfef
glue diff
karthikbhargavan 60f4457
glue diff
karthikbhargavan 60edf67
fixed sha3 calls
karthikbhargavan e22fa84
diff
karthikbhargavan 69e8501
fix for sha3 bench
karthikbhargavan a94aed7
Merge pull request #575 from cryspen/fix-c-extraction
karthikbhargavan 1735cba
Merge branch 'dev' into dev-arithmetic-proofs
karthikbhargavan e757771
refreshed c and fstar
karthikbhargavan 35b79f3
fixed spec utils
karthikbhargavan c67b8d8
polished proofs
karthikbhargavan 1ac1f28
arith
karthikbhargavan 3a99b2e
avx2 arithmetic propagate
karthikbhargavan 0058af2
rlimit
karthikbhargavan fcd536f
poly
karthikbhargavan 8e8d461
refresh
karthikbhargavan 4f229b2
spec rlimit
karthikbhargavan 149d519
wip
karthikbhargavan a5f2e75
portable arithmetic
karthikbhargavan da043be
Make ntt panic free
mamonet 275e832
Make Invert_ntt panic free
mamonet 5720ce5
avx2 arithmetic
karthikbhargavan abe0786
ntt wip
karthikbhargavan 3b00cb4
wip
karthikbhargavan b878b9b
wip
karthikbhargavan 042e808
wip
karthikbhargavan 24e4a0d
wip
karthikbhargavan ca568c3
wip
karthikbhargavan c44ad6b
wip: more intrinsics
W95Psp fa71b36
Add conditions for generic compress and serialize functions
mamonet 9ab86ed
Update F* files
mamonet 774431c
fstar: avx2: serialize_4 basically works
W95Psp 173821f
wip
karthikbhargavan e8928fc
ready to pr
karthikbhargavan 81cec41
refreshed c
karthikbhargavan 1e994bd
fmt
karthikbhargavan 89f91b1
portable
karthikbhargavan 5d35b6c
Merge pull request #589 from cryspen/dev-arithmetic-proofs
karthikbhargavan 84773cc
Merge remote-tracking branch 'origin/dev' into dev-serialize
mamonet a0fca27
trait
karthikbhargavan 645c229
wip
W95Psp f1a7d89
wip
W95Psp 8e5530a
Merge branch 'dev' into lf-avx2-serialize-deserialize-4
W95Psp 11cd991
fixes
W95Psp 1afb5c2
regenerated F*
W95Psp 48b0caa
Avx2.Serialize: verified
W95Psp d16265c
arith
karthikbhargavan 2f27e11
spec
karthikbhargavan aaee079
fix specs
W95Psp 0edeee6
Merge branch 'dev' into dev-arithmetic-proofs
karthikbhargavan f77fcb1
fix specs
W95Psp 539638b
Merge pull request #591 from cryspen/dev-arithmetic-proofs
karthikbhargavan 09cde63
Update Libcrux_ml_kem.Ind_cpa
mamonet 0f5121e
verified
karthikbhargavan 37d35d8
c code refresh
karthikbhargavan 2cc5d08
boring C not working
karthikbhargavan 2914855
Use opaque_to_smt to make serialize functions fast to verify
mamonet a0a7d89
Use `fold-enum-slice` hax branch
mamonet da48c5a
Merge remote-tracking branch 'origin/dev' into dev-serialize
mamonet 737bf43
Use main branch of hax
mamonet c7c3b3e
Remove `use crate::vector::FIELD_MODULUS`
mamonet ec66aac
Update serialize.rs
mamonet aee4c5b
Update traits.rs
mamonet 57abb85
update C code
franziskuskiefer 3631be6
removed typeclass _super constraint
karthikbhargavan 44af8ba
Mark to_unsigned_representative as lax
mamonet db5ff02
Merge remote-tracking branch 'origin/dev' into dev-constant-time
mamonet ab29fdc
traits
karthikbhargavan 9468162
hax passes
karthikbhargavan 4a21ab1
Merge pull request #593 from cryspen/ml-kem-merge-main
karthikbhargavan 878e250
Merge branch 'main' into dev
karthikbhargavan 5c647eb
Merge branch 'dev' into dev-serialize
karthikbhargavan 9e07b1b
f* reextract
karthikbhargavan 5971b69
c code refresh
karthikbhargavan bc1ba13
Add proofs for encapsulate/decapsulate in Ind_cca
mamonet ff16b9e
c regen
karthikbhargavan 6758f5c
pinned versions
karthikbhargavan 04a7e4f
Merge pull request #587 from cryspen/dev-serialize
karthikbhargavan 6f38bb3
Merge remote-tracking branch 'origin/dev' into dev-constant-time
mamonet 15d46eb
Add post-condition for entropy_preprocess
mamonet ff43a65
Merge branch 'dev' into dev-constant-time
karthikbhargavan 970017b
fstar
karthikbhargavan b1ecb42
verifies
karthikbhargavan a1aebab
c code refresh
karthikbhargavan bc88361
Merge pull request #559 from cryspen/dev-constant-time
karthikbhargavan 20e19ce
Merge remote-tracking branch 'origin/dev' into ntt-panic-free
mamonet d48d4d6
Make ind_cpar.rs panic-free
mamonet fc84fe8
progress
W95Psp 2de5cca
Update ind_cpa and matrix
mamonet 772653d
Update serialize.rs
mamonet 096b016
progress
W95Psp 99cef83
progress
W95Psp 89cc0d5
wip
karthikbhargavan c52ef6e
progress
W95Psp 4fb6bae
Merge branch 'dev' into lf-avx2-serialize-deserialize-4
W95Psp 232fbde
avx2: proofs: spec + proof for `serialize_12`
W95Psp a089e86
chore: regenerate F* files
W95Psp ea45bea
fixed some hax issues, refreshed C code
karthikbhargavan 22f2b93
Merge pull request #590 from cryspen/lf-avx2-serialize-deserialize-4
karthikbhargavan ebbbcbd
proofs
karthikbhargavan 9b1f1c3
removed some lax
karthikbhargavan deedd5a
Update invert_ntt
mamonet 1c3c00c
removed some lax
karthikbhargavan 6a84ae4
Update generic ntt.rs
mamonet ac15d16
in-ntt
karthikbhargavan 5f23a82
ntt
karthikbhargavan 96c8bf6
ntt-spec
karthikbhargavan 3d6773f
spec-utils
karthikbhargavan f7ae1f1
Merge branch 'dev-arithmetic-proofs' into ntt-panic-free
karthikbhargavan 0e1943a
verifies
karthikbhargavan 585fd7d
c code
karthikbhargavan 098de7d
Merge branch 'dev' into ntt-panic-free
karthikbhargavan 2ac0798
wip
karthikbhargavan 101ed40
arith
karthikbhargavan de52651
verifies
karthikbhargavan f0bd4d2
Merge pull request #576 from cryspen/ntt-panic-free
karthikbhargavan File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This feature doesn't exist anymore. Remove