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

Tactics for serialize #549

Merged
merged 20 commits into from
Aug 31, 2024
Merged

Tactics for serialize #549

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
e46edf3
Update and improve `Makefile`s
W95Psp Aug 30, 2024
0fb14cb
Reintroduce BitVecEq from previous proofs
W95Psp Aug 30, 2024
8feb781
intro tactic library to do hybrid norm/rewrite inside terms
W95Psp Aug 30, 2024
47177fe
Kill `let mut`, use array literal instead
W95Psp Aug 30, 2024
77fe334
Serialization pre/post in vector/traits.rs + spec in *Math.fst
W95Psp Aug 30, 2024
2e5a142
gitignore
W95Psp Aug 30, 2024
ff0e6ad
intrinsics
W95Psp Aug 30, 2024
bfeeda3
partial proofs
W95Psp Aug 30, 2024
7c4e54b
avx2: serialize: manual proofs
W95Psp Aug 30, 2024
dd063cc
portable: serialize: manual proofs
W95Psp Aug 30, 2024
64a2732
makefile, more fixes
W95Psp Aug 30, 2024
ea8f110
Comment out pre/post-conditions for serialize fun in vector/traits.rs
mamonet Aug 31, 2024
c8b2d7e
Fix return array in serialize_1
mamonet Aug 31, 2024
3635503
Fix fstar::replace for mm256_srli_epi16
mamonet Aug 31, 2024
10b4615
Update extracted F* files for intrinsics and ml-kem
mamonet Aug 31, 2024
89af067
wip
karthikbhargavan Aug 31, 2024
133225f
wip
karthikbhargavan Aug 31, 2024
56eed0a
verifying
karthikbhargavan Aug 31, 2024
aa003c8
fmt
karthikbhargavan Aug 31, 2024
87ab89d
fstar feat
karthikbhargavan Aug 31, 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: 7 additions & 5 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,16 +2,18 @@
.vscode
.DS_Store
benches/boringssl/build
proofs/fstar/extraction/.depend
proofs/fstar/extraction/#*#
proofs/fstar/extraction/.#*
hax.fst.config.json
fuzz/corpus
fuzz/artifacts
proofs/fstar/extraction/.cache
__pycache__
kyber-crate/
*.llbc

# When using sed
*.bak

# F*
.fstar-cache
.depend
**/proofs/fstar/*/#*#
**/proofs/fstar/*/.#*
hax.fst.config.json
42 changes: 21 additions & 21 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

5 changes: 5 additions & 0 deletions fstar-helpers/Makefile.base
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
# Base Makefile for F* in libcrux.
# This inherits from Makefile.generic, and adds the `specs` folder from HACL and the `libcrux-ml-kem/proofs/fstar/spec` folder.

FSTAR_INCLUDE_DIRS_EXTRA = $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/libcrux-ml-kem/proofs/fstar/spec $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec
include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic
Loading
Loading