From 9bdbbbc9ec1c96c58e7927066ed8607ed8c032fe Mon Sep 17 00:00:00 2001 From: Baris Erdem Date: Sat, 25 Apr 2026 13:26:00 +0300 Subject: [PATCH] hmac_ada 0.1.0 (#1871) SPARK-proved HMAC (RFC 2104) with standalone SHA-256 for Ada 2022. --- index/hm/hmac_ada/hmac_ada-0.1.0.toml | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 index/hm/hmac_ada/hmac_ada-0.1.0.toml diff --git a/index/hm/hmac_ada/hmac_ada-0.1.0.toml b/index/hm/hmac_ada/hmac_ada-0.1.0.toml new file mode 100644 index 00000000..5d2a4c6f --- /dev/null +++ b/index/hm/hmac_ada/hmac_ada-0.1.0.toml @@ -0,0 +1,23 @@ +name = "hmac_ada" +description = "SPARK-proved HMAC (RFC 2104) implementation for Ada/SPARK" +version = "0.1.0" + +authors = ["Baris Erdem"] +maintainers = ["Baris Erdem "] +maintainers-logins = ["b-erdem"] +licenses = "Apache-2.0" +website = "https://github.com/b-erdem/hmac_ada" +tags = ["hmac", "rfc2104", "cryptography", "spark", "embedded", "security"] + +long-description = """ +SPARK-proved HMAC (RFC 2104) with standalone SHA-256 (FIPS 180-4) for Ada 2022. +174 proof obligations fully discharged at Level 2 with zero pragma Assume. +Constant-time digest comparison, secure wipe of key material, no heap +allocation, pragma Pure. Suitable for embedded and safety-critical systems. +Includes streaming and one-shot APIs, plus a generic HMAC package for other +hash functions. +""" + +[origin] +commit = "fa03673fd91b3e8a155ae321d03ca1f0bc839540" +url = "git+https://github.com/b-erdem/hmac_ada.git"