Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

0.1.0 - 2026-04-30

Initial release.

HKDF Extract + Expand per RFC 5869
HKDF-SHA-256 concrete instantiation, 100% SPARK Level 2 proved (264/264 checks, 0 pragma Assume, 0 justified, 0 unproved)
Generic HKDF package for other HMAC functions (unproved convenience layer)
Built on hmac_ada ~0.2.0. Uses its distinct HMAC_Digest type internally and converts to Storage_Array at the API boundary, so PRK_Type stays Storage_Array (1 .. 32).
Uses System.Storage_Elements.Storage_Array (not Ada.Streams) for embedded and constrained-runtime (Light, ZFP) compatibility
HKDF_SHA256.Byte_Array subtype alias so users do not need to with System.Storage_Elements directly
pragma Pure, no heap allocation, stack-bounded
Passes all RFC 5869 Appendix A SHA-256 test vectors
Boundary-tested: OKM lengths 1, 32, 33, and 8160 (max)
Secure wipe of intermediate key material with pragma Inspection_Point