Skip to content

v0.1.0

Latest
Latest

Choose a tag to compare

View all tags
@b-erdem b-erdem released this 30 Apr 10:27
v0.1.0
cdde31c

First Alire-index release of hkdf_ada — a SPARK-proved HKDF (RFC 5869) implementation.

Highlights

  • HKDF-SHA-256 fully proved at SPARK Level 2: 266/266 checks discharged, zero pragma Assume, zero unproved.
  • HKDF Extract + Expand per RFC 5869.
  • Generic HKDF package for use with other HMAC functions (unproved convenience layer).
  • Built on hmac_ada ~0.2.0. Public PRK_Type is Storage_Array (1 .. 32) — plain bytes.
  • pragma Pure, no heap allocation, stack-bounded. Suitable for embedded and constrained-runtime (Light, ZFP) targets.
  • Passes all RFC 5869 Appendix A SHA-256 test vectors; boundary-tested at OKM lengths 1, 32, 33, and 8160 (max).
  • Secure wipe of intermediate key material with pragma Inspection_Point.

Layout

Tests and gnatprove live in a nested tests/ crate that depends on the top-level crate via a local path pin. The published crate has zero dev-only dependencies.

Install

alr with hkdf_ada
Assets 2
Loading