Port specifications from repository `hacspec/specs`

[W95Psp]

• tls_cryptolib (fstar: ❌CE0001¹, coq: ❌CE0001¹)
• hacspec-curve25519 (fstar: ✅, coq: ✅)
• hacspec-chacha20 (fstar: ✅, coq: ✅)
• hacspec-ristretto (fstar: ✅, coq: ✅)
• hacspec-linalg (fstar: ✅, coq: ✅)
• hacspec-merlin (fstar: ❌CE0002², coq: ❌CE0002²)
• hacspec-poly1305 (fstar: ✅, coq: ✅)
• hacspec-chacha20poly1305 (fstar: ✅, coq: ✅)
• hacspec-gimli (fstar: ✅, coq: ✅)
• hacspec-sha1 (fstar: ✅, coq: ✅)
• hacspec-sha256 (fstar: ✅, coq: ✅)
• hacspec-sha3 (fstar: ✅, coq: ✅)
• hacspec-ntru-prime (fstar: ✅, coq: ✅)
• hacspec-riot-bootloader (fstar: ✅, coq: ✅)
• hacspec-riot-runqueue (fstar: ✅, coq: ✅)
• hacspec-hmac (fstar: ✅, coq: ✅)
• hacspec-hkdf (fstar: ✅, coq: ✅)
• hacspec-p256 (fstar: ✅, coq: ✅)
• hacspec-bls12-381 (fstar: ✅, coq: ✅)
• hacspec-ecdsa-p256-sha256 (fstar: ✅, coq: ✅)
• hacspec-aes (fstar: ✅, coq: ✅)
• hacspec-aes-jazz (fstar: ✅, coq: ✅)
• hacspec-gf128 (fstar: ✅, coq: ✅)
• hacspec-aes128-gcm (fstar: ✅, coq: ✅)
• hacspec-bls12-381-hash (fstar: ✅, coq: ✅)
• hacspec-ed25519 (fstar: ✅, coq: ✅)
• hacspec-edwards25519 (fstar: ✅, coq: ✅)
• hacspec-edwards25519-hash (fstar: ✅, coq: ✅)
• hacspec-edwards25519-ecvrf (fstar: ✅, coq: ✅)
• hacspec-rsa-pkcs1 (fstar: ✅, coq: ✅)
• hacspec-bip-340 (fstar: ✅, coq: ✅)
• hacspec-rsa-fdh-vrf (fstar: ✅, coq: ✅)
• hacspec-xor (fstar: ✅, coq: ✅)

Footnotes

1. (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet. Loop without mutation? ↩ ↩²

2. Fatal error: something we considered as impossible occurred! Please report this by submitting an issue on GitHub! Details: Import_thir.UnsafeBlock ↩ ↩²