cbor_ada 0.3.0

CBOR (RFC 8949) encoder/decoder for Ada 2022 in SPARK.

Headline: the encode/decode round trip is now machine-proved. Decode(Encode(x)) = x is a SPARK theorem for every major-type head (integers, tags, array/map headers, simple values, booleans, null/undefined) plus byte-exact float payload pass-through — functional correctness beyond absence of run-time errors, via a shared ghost denotation (CBOR.Model) the encoder and decoder are both specified against.

• Whole library: 1082/1082 VCs proved at level 2, 0 unproved, 0 pragma Assume (was 517 core VCs with the round-trip lemmas open).
• No heap, pragma Pure, full RFC 8949 well-formedness validation.

License: Apache-2.0.
Alire: merged to the community index — alr get cbor_ada.

See CHANGELOG.md for details.

v0.2.0

BREAKING: Replace Ada.Streams with System.Storage_Elements for constrained runtime compatibility (Light, ZFP). Closes #1.

Changed

• Stream_Element → Storage_Element (aliased as CBOR.Byte)
• Stream_Element_Array → Storage_Array (aliased as CBOR.Byte_Array)
• Stream_Element_Offset → Storage_Offset (aliased as CBOR.SE_Offset)
• Child packages now use CBOR-level types instead of directly referencing the underlying package

Migration

Replace with Ada.Streams; use Ada.Streams; with with System.Storage_Elements; use System.Storage_Elements;.

Full changelog: https://github.com/b-erdem/cbor_ada/blob/main/CHANGELOG.md

v0.1.1

Safety-critical hardening release based on comprehensive security review.

Fixed

• Stale cumulative length tracking for indefinite-length strings at the same nesting depth

Added

• Post contracts on all public encoder/decoder functions
• Runtime hardening: -gnato (overflow checks) and -gnatVa (validity checks)
• SPARK proofs now run on pull requests in CI
• SECURITY.md — threat model and security documentation
• 21 new edge-case tests (697 total)

Changed

• Check_UTF8 default changed from False to True
• 517 SPARK proof obligations, 0 unproved (up from 486)

Full changelog: https://github.com/b-erdem/cbor_ada/blob/main/CHANGELOG.md

v0.1.0

cbor_ada v0.1.0

First release of the CBOR (RFC 8949) encoding/decoding library for Ada/SPARK.

Highlights

• 100% SPARK-proved encoder and decoder (475 checks, 0 unproved)
• Full RFC 8949 well-formedness validation
• No heap allocation — stack-only, embedded-ready
• pragma Pure — stateless, no side effects
• 671 tests passing

Encoder

All 8 CBOR major types supported: unsigned/negative/signed integers, byte strings, text strings (Latin-1 and UTF-8), arrays, maps, tags, simple values, floats (opaque bytes), indefinite-length containers, and break codes.

Decoder

• Decode — single-item decode with two overloads
• Decode_All — full item tree decode with configurable depth and string length limits
• Decode_All_Strict — rejects trailing bytes
• Is_Valid_UTF8 — optional RFC 3629 validation
• 9 distinct error codes for precise failure diagnosis

Security

Configurable Max_Depth, Max_String_Len, and Check_UTF8 parameters for safe handling of untrusted input.

Requirements

• GNAT >= 15.1 (Ada 2022)
• gnatprove >= 15.1 (for SPARK proofs only)