Skip to content

Files

Latest commit

R1kMR1kM
Add spec tests for Blake2 last_node
Apr 17, 2024
9748890 · Apr 17, 2024

History

History
This branch is 105 commits behind hacl-star/hacl-star:main.

specs

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
drbg
drbg
Apr 11, 2023
frodo
frodo
Mar 27, 2023
lemmas
lemmas
Apr 17, 2024
tests
tests
Apr 17, 2024
Makefile
Makefile
Mar 10, 2022
README.md
README.md
Jan 3, 2020
Spec.AES.fst
Spec.AES.fst
Jun 12, 2019
Spec.Agile.AEAD.fst
Spec.Agile.AEAD.fst
Jan 29, 2020
Spec.Agile.AEAD.fsti
Spec.Agile.AEAD.fsti
Jun 3, 2022
Spec.Agile.CTR.fst
Spec.Agile.CTR.fst
Jul 2, 2019
Spec.Agile.Cipher.fst
Spec.Agile.Cipher.fst
Sep 24, 2019
Spec.Agile.Cipher.fsti
Spec.Agile.Cipher.fsti
Sep 24, 2019
Spec.Agile.DH.fst
Spec.Agile.DH.fst
Apr 19, 2023
Spec.Agile.HKDF.fst
Spec.Agile.HKDF.fst
Apr 11, 2023
Spec.Agile.HKDF.fsti
Spec.Agile.HKDF.fsti
Apr 11, 2023
Spec.Agile.HMAC.fst
Spec.Agile.HMAC.fst
Apr 11, 2023
Spec.Agile.HMAC.fsti
Spec.Agile.HMAC.fsti
Apr 11, 2023
Spec.Agile.HPKE.fst
Spec.Agile.HPKE.fst
Nov 29, 2022
Spec.Agile.HPKE.fsti
Spec.Agile.HPKE.fsti
Nov 29, 2022
Spec.Agile.Hash.fst
Spec.Agile.Hash.fst
Apr 17, 2024
Spec.Agile.Hash.fsti
Spec.Agile.Hash.fsti
Apr 11, 2023
Spec.Blake2.Definitions.fst
Spec.Blake2.Definitions.fst
Apr 1, 2024
Spec.Blake2.fst
Spec.Blake2.fst
Apr 17, 2024
Spec.Box.fst
Spec.Box.fst
Aug 9, 2019
Spec.Chacha20.fst
Spec.Chacha20.fst
Oct 16, 2019
Spec.Chacha20Poly1305.fst
Spec.Chacha20Poly1305.fst
Oct 18, 2021
Spec.Cipher.Expansion.fst
Spec.Cipher.Expansion.fst
Jul 3, 2019
Spec.Cipher.Expansion.fsti
Spec.Cipher.Expansion.fsti
Oct 11, 2019
Spec.Curve25519.fst
Spec.Curve25519.fst
Jul 20, 2022
Spec.Ed25519.PointOps.fst
Spec.Ed25519.PointOps.fst
Jul 20, 2022
Spec.Ed25519.fst
Spec.Ed25519.fst
Oct 24, 2022
Spec.Exponentiation.fst
Spec.Exponentiation.fst
Oct 24, 2022
Spec.Exponentiation.fsti
Spec.Exponentiation.fsti
Oct 24, 2022
Spec.FFDHE.fst
Spec.FFDHE.fst
Jan 15, 2021
Spec.GaloisField.fst
Spec.GaloisField.fst
Oct 14, 2019
Spec.Hash.Definitions.fst
Spec.Hash.Definitions.fst
Apr 14, 2023
Spec.Hash.MD.fst
Spec.Hash.MD.fst
Dec 9, 2022
Spec.K256.PointOps.fst
Spec.K256.PointOps.fst
Apr 21, 2023
Spec.K256.fst
Spec.K256.fst
Apr 21, 2023
Spec.MD5.fst
Spec.MD5.fst
Dec 8, 2022
Spec.MD5.fsti
Spec.MD5.fsti
Dec 8, 2022
Spec.P256.PointOps.fst
Spec.P256.PointOps.fst
Apr 13, 2023
Spec.P256.fst
Spec.P256.fst
Apr 19, 2023
Spec.Poly1305.fst
Spec.Poly1305.fst
Aug 8, 2019
Spec.RSAPSS.fst
Spec.RSAPSS.fst
Nov 29, 2022
Spec.SHA1.fst
Spec.SHA1.fst
Dec 8, 2022
Spec.SHA1.fsti
Spec.SHA1.fsti
Dec 8, 2022
Spec.SHA2.Constants.fst
Spec.SHA2.Constants.fst
Aug 9, 2019
Spec.SHA2.fst
Spec.SHA2.fst
Dec 8, 2022
Spec.SHA2.fsti
Spec.SHA2.fsti
Dec 8, 2022
Spec.SHA3.Constants.fst
Spec.SHA3.Constants.fst
Jul 30, 2019
Spec.SHA3.fst
Spec.SHA3.fst
Dec 24, 2023
Spec.Salsa20.fst
Spec.Salsa20.fst
Aug 9, 2019
Spec.SecretBox.fst
Spec.SecretBox.fst
Aug 9, 2019
make_hpke_constants.py
make_hpke_constants.py
Jun 3, 2022
make_md5_tests.sh
make_md5_tests.sh
Mar 18, 2021
make_sha1_tests.sh
make_sha1_tests.sh
Mar 18, 2021

README.md

HACL* specifications

This directory contains F* formal specifications against which the code of HACL*, Vale, and EverCrypt are verified.

These specifications have been written with a view towards succinctness and readability, and we encourage others to carefully review them, since they constitute an important part of our trusted computing base (TCB).

All our specifications are written in the Pure fragment of F* and rely only on F* builtins and the HACL* libraries in /lib. Each specification is typechecked using F* and tested against standard test vectors by compilation to OCaml. (See the included Makefile for details.)