Sha3

Website:

https://github.com/b-erdem/sha3_ada

Author:

Baris Erdem

Maintainer:

Baris Erdem <baris@erdem.dev>

License:

Apache-2.0

Version:

1.0.0

Alire CI:

Dependencies:

gnat >=14.2.1

Dependents:

Badge:

Copy image location: https://img.shields.io/endpoint?url=https://alire.ada.dev/badges/sha3.json

SPARK-proved SHA-3/SHAKE (FIPS 202) hash functions

#sha3 #keccak #hash #cryptography #spark #embedded #security #verified

SPARK-proved SHA-3 and SHAKE implementations for Ada 2022. Implements FIPS 202 with SHA3-256, SHA3-512, SHAKE128, and SHAKE256. Keccak-f[1600] permutation and sponge construction are formally verified at SPARK level 2: 159/159 proof obligations discharged, zero pragma Assume, zero unproved VCs, termination verified via Always_Terminates aspects on every public subprogram.

No heap allocation, pragma Pure, suitable for embedded and safety-critical systems. Incremental API (Init/Absorb/Squeeze) and one-shot convenience functions. Tested against NIST Known Answer Test vectors.

Constant-time execution and FIPS 140-3 validation are out of scope for this release. See SECURITY.md for the full threat model.