Home

Welcome to the hacspec wiki!

hacspec architecture

Specs state

There's a list of hacspecs implemented to test the library and compiler implementations. The following table gives an overview of the specs and their compilation targets.

Algorithm	Valid (py)	Valid	F* compilation	F* type checked
Poly1305	✓	✓	✓	✓
ChaCha20	✓	✓	✓	✓
AEAD ChaCha20Poly1305	✓	✓	❌	❌
AES	✓	✓	✓	❌
GF128	✓	✓	✓	✓
AEAD AES-GCM 128	✓	✓	❌	❌
Sha2	✓	❌	❌	❌
Sha3	✓	❌	❌	❌
Curve25519	✓	✓	✓	❌
Cuve448	✓	✓	✓	❌
ED25519	✓	❌	❌	❌
P256	✓	❌	❌	❌
RSA PSS	✓	❌	❌	❌
Blake2	✓	❌	❌	❌
WOTS	✓	❌	❌	❌
XMSS (verify)	✓	❌	❌	❌
Frodo	❌	❌	❌	❌
Argon2i	❌	❌	❌	❌