The hash functions take a message of n bytes as an Array UInt64 holding eight bytes per word in little-endian order, together with the byte count n. Byte i is bits 8 (i % 8) to 8 (i % 8) + 7 of word i / 8, the layout of Wasm memory, so a file read as little-endian words is a message. A digest uses the same packing in a structure of words, so that a call returns its digest as several WebAssembly results and allocates nothing. An output of SHAKE is an array of words in the same packing, the one allocation of its call. The word module defines the structures, bswap, and the rotation helper. The packed-byte module defines bytes, the bytes that packed words denote, which the correctness theorems use to state their arguments, and the digest module defines the bytes of a digest.
| Family | Functions | Proved results |
|---|---|---|
| SHA-256 | SHA-256 and SHA-224 of FIPS 180-4 | For messages of fewer than 2^61 bytes, each export returns without a trap the digest of a Lean transcription of FIPS 180-4, and the emitted file holds the module. |
| SHA-512 | SHA-512, SHA-384, SHA-512/256, and SHA-512/224 of FIPS 180-4 | The same, for the four functions of the SHA-512 compression. |
| HMAC | HMAC-SHA-256 and HMAC-SHA-512 of FIPS 198-1 | For keys of fewer than 2^61 bytes and messages that leave the inner message below 2^61 bytes, each export returns without a trap the MAC of a Lean transcription of FIPS 198-1 for the key and message bits, and the emitted files hold the modules. |
| SHA-3 | SHA3-224, SHA3-256, SHA3-384, SHA3-512, SHAKE128, and SHAKE256 of FIPS 202 | For messages of fewer than 2^61 bytes, each hash export returns without a trap and without allocating the digest of a Lean transcription of FIPS 202, and each SHAKE export returns an output of d < 2^61 bytes in one allocated block. FIPS 202 reads each byte least significant bit first, and the theorems read message and digest bytes in that order. The emitted file holds the module. |
| CRC-32 and CRC-32C | CRC-32 of ITU-T V.42 and CRC-32C of RFC 3720, with update functions that continue from the CRC of earlier bytes | For messages of any length, each export returns without a trap the CRC of a Lean transcription of the two documents, which an independent review compared with them. The emitted file holds the module. |
| SipHash | SipHash-2-4 and SipHash-1-3 of the SipHash paper, with a 128-bit key | For messages of any length, each export returns without a trap the 64-bit value of a Lean transcription of the paper's §2, which reaches every intermediate state of its Appendix A. The emitted file holds the module. |
| XXH64 | XXH64 of the xxHash specification, with a 64-bit seed | For messages of any length, the export returns without a trap the 64-bit value of a Lean transcription of the specification's XXH64 description. The emitted file holds the module. |
The Merkle–Damgård module proves that two distinct messages with equal SHA-256 digests give two distinct pairs of a hash value and a block on which SHS.SHA256.compress agrees, and the same for SHA-512 and SHS.SHA512.compress. sha256_collision and sha512_collision state the reduction for bit messages within the length limits of FIPS 180-4, and sha256_bytes_collision and sha512_bytes_collision state it for byte strings of fewer than 2^61 bytes. Each call theorem equates the bytes of the returned words with the transcription's digest of the message bytes, so two calls that return the same words for distinct messages satisfy the hypotheses of the byte theorem. When the message lengths differ, the length fields make the final blocks differ, and the last compression collides. When the lengths agree, the messages have the same number of blocks, and the last step at which the hash values or the blocks differ collides. The proof covers any compression function on eight words and blocks of sixteen words with the padding and parsing of FIPS 180-4. The digests of SHA-224, SHA-384, and SHA-512/t omit part of the final hash value, and the module proves nothing about them.
Sha2 holds material copied from fips-180-4-lean: the transcription of FIPS 180-4 in Spec, an implementation on bytes in Impl, and its equivalence proofs in Equiv. The NOTICE gives the source, the license, and the changes made to build under Lean 4.34. The SHA-256 and SHA-512 proofs relate their programs to Impl and use Equiv's theorems about it. The NIST test vectors are in data/hashing.