A CBOR (RFC 8949) encoding and decoding library for Ada 2022, built with SPARK formal verification.
The encoder and decoder are 100% SPARK-proved at Level 2 — mathematically guaranteed free of runtime errors (no buffer overflows, no range violations, no integer overflows, no uninitialized reads).
- Formally verified core — 517 proof obligations on the encoder + decoder, 0 unproved (CVC5/Z3). Optional round-trip lemmas in
CBOR.Propertiesare aspirational and not yet fully discharged; see SPARK proof status. - RFC 8949 compliant — full well-formedness validation with shortest-form checking
- No heap allocation — stack-only, suitable for embedded and safety-critical systems
- Stateless —
pragma Pure, no global state, no side effects - Zero dependencies — only the Ada standard library
alr with cbor_ada
Or add to your alire.toml:
[[depends-on]] cbor_ada = "~0.2.0"
with System.Storage_Elements; use System.Storage_Elements; with CBOR.Encoding; procedure Example is package Enc renames CBOR.Encoding; begin -- Integers Enc.Encode_Unsigned (42); -- major type 0 Enc.Encode_Negative (9); -- major type 1: encodes -10 Enc.Encode_Integer (-10); -- auto-selects: same as above -- Strings Enc.Encode_Text_String ("hello"); Enc.Encode_Text_String_UTF8 (UTF8_Bytes); -- raw UTF-8 bytes Enc.Encode_Byte_String (Raw_Data); -- Containers (header + elements) declare Output : constant Storage_Array := Enc.Encode_Array (3) & Enc.Encode_Unsigned (1) & Enc.Encode_Text_String ("two") & Enc.Encode_Bool (True); begin null; end; -- Maps, tags, simple values, floats, indefinite-length — all supported end Example;
with System.Storage_Elements; use System.Storage_Elements; with CBOR; use CBOR; with CBOR.Decoding; procedure Example is Input : constant Storage_Array := ...; begin -- Single item declare R : constant Decode_Result := Decoding.Decode (Input); begin if R.Status = OK then case R.Item.Kind is when MT_Unsigned_Integer => ... -- R.Item.UInt_Value when MT_Text_String => ... -- Decoding.Get_String (Input, R.Item.TS_Ref) when others => ... end case; end if; end; -- Full item tree (arrays, maps, tags expanded) declare R : constant Decode_All_Result := Decoding.Decode_All (Input); begin -- R.Items (1 .. R.Count) in depth-first order -- R.Next = first unconsumed byte position null; end; -- Walk manually declare R1 : constant Decode_Result := Decoding.Decode (Input); R2 : constant Decode_Result := Decoding.Decode (Input, R1.Next); begin null; end; end Example;
-- Reject trailing bytes after the top-level item R := Decoding.Decode_All_Strict (Input); -- Limit nesting depth (default: 16) R := Decoding.Decode_All (Input, Max_Depth => 4); -- Limit string lengths (default: no limit) R := Decoding.Decode_All (Input, Max_String_Len => 4096); -- Validate UTF-8 in text strings R := Decoding.Decode_All (Input, Check_UTF8 => True);
The decoder enforces all RFC 8949 well-formedness requirements:
| Check | Reference |
|---|---|
| Reserved additional information 28-30 rejected | Section 3 |
| Simple values 0-31 in two-byte form rejected | Section 3.3 |
| Shortest-form encoding required for all arguments | Section 4.1 |
| Indefinite-length rejected for major types 0, 1, 6 | Section 3.2.6 |
| Break code rejected outside indefinite-length containers | Section 3.2.1 |
| Indefinite-length string chunks must match parent type | Section 3.2.3 |
| Indefinite-length maps must have even item count | Section 3.2.2 |
| Truncated input detected | - |
| Status | Meaning |
|---|---|
OK |
Successful decode |
Err_Not_Well_Formed |
RFC 8949 well-formedness violation |
Err_Truncated |
Input ends mid-item |
Err_Trailing_Data |
Extra bytes after top-level item (strict mode) |
Err_Depth_Exceeded |
Nesting exceeds Max_Depth (configurable, default 16) |
Err_Invalid_UTF8 |
Invalid UTF-8 in text string (Check_UTF8 => True) |
Err_Too_Many_Items |
Item tree exceeds 128 items |
Err_String_Too_Long |
String length exceeds Max_String_Len |
Err_Resource_Limit |
Map entry count too large to track |
The runtime-critical surface — CBOR.Encoding and CBOR.Decoding — is fully proved at Level 2:
SPARK Analysis results Total Flow Provers Unproved
Total 517 47 470 .
All 517 checks on the encoder + decoder are proved. No pragma Assume or Justified annotations — every obligation is machine-verified.
CBOR.Properties is a separate package of round-trip lemmas (Lemma_Round_Trip_Unsigned, _Negative, _Bool, _Float_*, etc.) that aim to prove the algebraic property Decode (Encode (x)) = x for each major type. These lemmas are not on the runtime path — they exist purely as proof artefacts — and they are still work-in-progress: at the time of writing, 90 of their 198 obligations are unproved at Level 2 / 120 s. Consumers who only call the encoder/decoder are unaffected; consumers who want to compose CBOR.Properties into larger proofs should expect to need their own assumes or higher prover budgets until the lemmas are closed.
# Prove core packages (~30 seconds) scripts/prove # Prove everything including the in-progress round-trip lemmas (slow) scripts/prove 2 120 all
| Function | Description |
|---|---|
Encode_Unsigned (Value) |
Major type 0 — unsigned integer (0 to 2^64-1) |
Encode_Negative (Arg) |
Major type 1 — negative integer (-1 - Arg) |
Encode_Integer (Value) |
Signed integer — auto-selects type 0 or 1 |
Encode_Byte_String (Data) |
Major type 2 — definite-length byte string |
Encode_Text_String (Text) |
Major type 3 — text string (Latin-1 bytes) |
Encode_Text_String_UTF8 (Data) |
Major type 3 — text string from raw UTF-8 bytes |
Encode_Array (Count) |
Major type 4 — definite-length array header |
Encode_Map (Count) |
Major type 5 — definite-length map header |
Encode_Tag (Tag_Number) |
Major type 6 — semantic tag |
Encode_Simple (Value) |
Major type 7 — simple value (0-23, 32-255) |
Encode_Bool (Value) |
Boolean (simple values 20/21) |
Encode_Null |
Null (simple value 22) |
Encode_Undefined |
Undefined (simple value 23) |
Encode_Float_Half (Bytes) |
Half-precision float (2 raw bytes) |
Encode_Float_Single (Bytes) |
Single-precision float (4 raw bytes) |
Encode_Float_Double (Bytes) |
Double-precision float (8 raw bytes) |
Encode_Array_Start |
Indefinite-length array (0x9F) |
Encode_Map_Start |
Indefinite-length map (0xBF) |
Encode_Byte_String_Start |
Indefinite-length byte string (0x5F) |
Encode_Text_String_Start |
Indefinite-length text string (0x7F) |
Encode_Break |
Break stop code (0xFF) |
- Float values are opaque byte arrays (no IEEE 754 conversion)
Encode_Text_Stringpasses through Latin-1 bytes; useEncode_Text_String_UTF8for pre-encoded UTF-8Decode_Allreturns at most 128 items; use manualDecode+Nextwalking for larger structures- Tag content semantics (e.g., tag 0 date format) are not validated
- UTF-8 validation is enabled by default; disable with
Check_UTF8 => Falsewhen input is pre-validated
- GNAT >= 15.1 with Ada 2022 support
- gnatprove >= 15.1 (for running SPARK proofs only — not a library dependency)
- Alire >= 2.0 (package manager)
Apache-2.0 — see LICENSE.
Certification artifacts, safety case documentation, and formal verification evidence packages available for safety-critical deployments — contact baris@erdem.dev.