UTF-8 MODULE
============
Standard: RFC 3629
Files: src/lingenic_text-utf8_spec.ads (ghost specification)
src/lingenic_text-utf8.ads (public API)
src/lingenic_text-utf8.adb (implementation)
PURPOSE
-------
The UTF-8 module is the sole entry point from raw bytes to Unicode
codepoints. Every algorithm module in the library receives its input
as Byte_Array and uses UTF8.Decode to extract codepoints. Surrogates
are structurally excluded by the well-formedness predicates -- any
codepoint that reaches the algorithm layer via Decode is already a
Unicode scalar value.
GHOST SPECIFICATION (UTF8_Spec)
-------------------------------
Package Lingenic_Text.UTF8_Spec is Ghost and Pure. All functions are
expression functions, erased at compile time, zero runtime cost. The
solver unfolds their bodies directly into proof contexts.
Byte Classification:
Is_Continuation(B) True if B is a continuation byte (16#80#..16#BF#)
Lead_Length(B) Sequence length from lead byte:
00..7F -> 1 (ASCII)
80..BF -> 0 (continuation, not valid lead)
C0..C1 -> 0 (overlong)
C2..DF -> 2
E0..EF -> 3
F0..F4 -> 4
F5..FF -> 0 (would exceed U+10FFFF)
Codepoint to Length:
Encoded_Length(CP) Byte count for encoding CP:
U+0000..U+007F -> 1
U+0080..U+07FF -> 2
U+0800..U+FFFF -> 3
U+10000..U+10FFFF -> 4
Well-Formedness (RFC 3629 Section 4 ABNF):
WF1(B0) True if B0 is valid 1-byte sequence
WF2(B0, B1) True if (B0, B1) is valid 2-byte sequence
WF3(B0, B1, B2) True if (B0, B1, B2) is valid 3-byte sequence
WF4(B0, B1, B2, B3) True if (B0, B1, B2, B3) is valid 4-byte sequence
WF3 encodes the surrogate exclusion: ED followed by 80..9F (not A0..BF)
ensures U+D800..U+DFFF cannot be encoded.
WF4 encodes the ceiling: F4 followed by 80..8F ensures the maximum
codepoint is U+10FFFF.
Decoding Formulas:
Decode_1(B0) B0 (identity for ASCII)
Decode_2(B0, B1) (B0 - C0) * 64 + (B1 - 80)
Decode_3(B0, B1, B2) (B0 - E0) * 4096 + (B1 - 80) * 64 + (B2 - 80)
Decode_4(B0, B1, B2, B3) (B0 - F0) * 262144 + (B1 - 80) * 4096
+ (B2 - 80) * 64 + (B3 - 80)
Each has Pre requiring the corresponding WF predicate.
Encoding Byte Formulas:
Enc_1_B0(CP) CP (identity for ASCII)
Enc_2_B0(CP) C0 + CP / 64
Enc_2_B1(CP) 80 + CP mod 64
Enc_3_B0(CP) E0 + CP / 4096
Enc_3_B1(CP) 80 + (CP / 64) mod 64
Enc_3_B2(CP) 80 + CP mod 64
Enc_4_B0(CP) F0 + CP / 262144
Enc_4_B1(CP) 80 + (CP / 4096) mod 64
Enc_4_B2(CP) 80 + (CP / 64) mod 64
Enc_4_B3(CP) 80 + CP mod 64
Array-Level Predicates:
Well_Formed_At(Source, Pos)
True if there is a well-formed UTF-8 sequence starting at Pos in
Source. Dispatches to WF1/WF2/WF3/WF4 based on Lead_Length.
Pre: Source'Last < Positive'Last (overflow safety).
Decoded_At(Source, Pos)
The codepoint value at Pos. Dispatches to Decode_1/2/3/4.
Pre: Well_Formed_At(Source, Pos).
Encoded_At(Target, Pos, CP)
True if the bytes at Pos in Target are the correct encoding of CP.
Checks each byte against the corresponding Enc_N_BM formula.
PUBLIC API
----------
procedure Decode
(Source : Byte_Array;
Pos : Positive;
CP : out Codepoint;
Length : out Positive;
Valid : out Boolean);
Pre: Pos in Source'Range, Source'Last < Positive'Last
Post: Length in 1..4
Valid = Well_Formed_At(Source, Pos) -- completeness
if Valid:
Length = Lead_Length(Source(Pos)) -- length
CP = Decoded_At(Source, Pos) -- value
Is_Scalar_Value(CP) -- no surrogates
Encoded_At(Source, Pos, CP) -- round-trip
if not Valid:
CP = 0, Length = 1 -- error recovery
The Valid output is bidirectional: True if and only if the bytes are
well-formed. This is not just "if well-formed then Valid" but also
"if Valid then well-formed" -- the equivalence is proved.
On invalid input, Length = 1 ensures the caller advances by one byte,
matching the W3C "replacement of maximal subparts" strategy.
procedure Encode
(CP : Codepoint;
Target : in out Byte_Array;
Pos : Positive;
Length : out Positive);
Pre: Is_Scalar_Value(CP) -- no surrogates
Pos in Target'Range, Target'Last < Positive'Last
Target'Last - Pos >= Encoded_Length(CP) - 1 -- room in buffer
Post: Length = Encoded_Length(CP) -- length
Encoded_At(Target, Pos, CP) -- bytes correct
Well_Formed_At(Target, Pos) -- well-formed
Decoded_At(Target, Pos) = CP -- round-trip
Frame: bytes outside [Pos..Pos+Length-1] unchanged
IMPLEMENTATION
--------------
The implementation (utf8.adb) mirrors the RFC 3629 Section 4 ABNF exactly:
- The lead byte determines the sequence length via range checks
- Subsequent byte range checks match the ABNF productions
- Decode and encode arithmetic match the ghost spec formulas
The code is 150 lines. No loops, no auxiliary data structures. Each
branch of the if-elsif chain handles one ABNF production.
The structure is deliberately transparent to the prover: the case
analysis in the code matches the case analysis in the ghost spec,
so GNATprove can verify each branch independently.
USAGE BY OTHER MODULES
-----------------------
All algorithm modules use the same Ghost helper pattern to bridge
UTF-8 decoding into their ghost specifications:
function Ghost_Step_Length(Text, Cur) return Positive
Well-formed -> Lead_Length, invalid -> 1
function Ghost_CP(Text, Cur) return Codepoint
Well-formed -> Decoded_At, invalid -> 0
function Ghost_Valid(Text, Cur) return Boolean
= Well_Formed_At(Text, Cur)
These are defined per-module (not shared) so each module's ghost
function is self-contained for solver unfolding.