-- Copyright © 2026 Lingenic LLC. All rights reserved.
-- Licensed under the Lingenic Source-Available License v2.3.
-- Production use requires a separate license from Licensor.
-- See LICENSE.md and COPYRIGHT in the project root.
--
-------------------------------------------------------------------------------
-- Lingenic-Text
-- Formally Verified Unicode Text Processing Library
--
-- UTF-8 implementation body.
--
-- The structure mirrors the RFC 3629 §4 ABNF exactly:
-- - Lead byte determines sequence length
-- - Subsequent byte range checks match the ABNF productions
-- - Decode/encode arithmetic matches the ghost spec formulas
-------------------------------------------------------------------------------
package body Lingenic_Text.UTF8
with SPARK_Mode
is
procedure Decode
(Source : Byte_Array;
Pos : Positive;
CP : out Codepoint;
Length : out Positive;
Valid : out Boolean)
is
B0 : constant Byte := Source (Pos);
begin
if B0 <= 16#7F# then
-- UTF8-1: %x00-7F
CP := B0;
Length := 1;
Valid := True;
elsif B0 <= 16#C1# then
-- 80..BF: continuation (not a valid lead)
-- C0..C1: overlong 2-byte for ASCII range
CP := 0;
Length := 1;
Valid := False;
elsif B0 <= 16#DF# then
-- UTF8-2: %xC2-DF UTF8-tail
if Source'Last - Pos >= 1
and then Source (Pos + 1) in 16#80# .. 16#BF#
then
CP := (B0 - 16#C0#) * 64
+ (Source (Pos + 1) - 16#80#);
Length := 2;
Valid := True;
else
CP := 0;
Length := 1;
Valid := False;
end if;
elsif B0 <= 16#EF# then
-- UTF8-3: E0 A0-BF tail / E1-EC tail tail /
-- ED 80-9F tail / EE-EF tail tail
if Source'Last - Pos >= 2
and then
((B0 = 16#E0#
and then Source (Pos + 1) in 16#A0# .. 16#BF#)
or else
(B0 in 16#E1# .. 16#EC#
and then Source (Pos + 1) in 16#80# .. 16#BF#)
or else
(B0 = 16#ED#
and then Source (Pos + 1) in 16#80# .. 16#9F#)
or else
(B0 in 16#EE# .. 16#EF#
and then Source (Pos + 1) in 16#80# .. 16#BF#))
and then Source (Pos + 2) in 16#80# .. 16#BF#
then
CP := (B0 - 16#E0#) * 4096
+ (Source (Pos + 1) - 16#80#) * 64
+ (Source (Pos + 2) - 16#80#);
Length := 3;
Valid := True;
else
CP := 0;
Length := 1;
Valid := False;
end if;
elsif B0 <= 16#F4# then
-- UTF8-4: F0 90-BF tail tail / F1-F3 tail tail tail /
-- F4 80-8F tail tail
if Source'Last - Pos >= 3
and then
((B0 = 16#F0#
and then Source (Pos + 1) in 16#90# .. 16#BF#)
or else
(B0 in 16#F1# .. 16#F3#
and then Source (Pos + 1) in 16#80# .. 16#BF#)
or else
(B0 = 16#F4#
and then Source (Pos + 1) in 16#80# .. 16#8F#))
and then Source (Pos + 2) in 16#80# .. 16#BF#
and then Source (Pos + 3) in 16#80# .. 16#BF#
then
CP := (B0 - 16#F0#) * 262144
+ (Source (Pos + 1) - 16#80#) * 4096
+ (Source (Pos + 2) - 16#80#) * 64
+ (Source (Pos + 3) - 16#80#);
Length := 4;
Valid := True;
else
CP := 0;
Length := 1;
Valid := False;
end if;
else
-- F5..FF: would encode > U+10FFFF
CP := 0;
Length := 1;
Valid := False;
end if;
end Decode;
procedure Encode
(CP : Codepoint;
Target : in out Byte_Array;
Pos : Positive;
Length : out Positive)
is
begin
if CP <= 16#7F# then
Target (Pos) := CP;
Length := 1;
elsif CP <= 16#7FF# then
Target (Pos) := 16#C0# + CP / 64;
Target (Pos + 1) := 16#80# + CP mod 64;
Length := 2;
elsif CP <= 16#FFFF# then
Target (Pos) := 16#E0# + CP / 4096;
Target (Pos + 1) := 16#80# + (CP / 64) mod 64;
Target (Pos + 2) := 16#80# + CP mod 64;
Length := 3;
else
Target (Pos) := 16#F0# + CP / 262144;
Target (Pos + 1) := 16#80# + (CP / 4096) mod 64;
Target (Pos + 2) := 16#80# + (CP / 64) mod 64;
Target (Pos + 3) := 16#80# + CP mod 64;
Length := 4;
end if;
end Encode;
end Lingenic_Text.UTF8;