-- 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 ghost specification: RFC 3629 encoding rules as expression functions.
--
-- Section 3: encoding table (codepoint ranges → byte sequence lengths)
-- Section 4: ABNF well-formedness (byte range constraints per sequence type)
--
-- Every function here is Ghost — erased at compile time, zero runtime cost.
-- The solver unfolds expression function bodies directly into proof contexts.
-------------------------------------------------------------------------------
package Lingenic_Text.UTF8_Spec
with SPARK_Mode, Ghost, Pure
is
---------------------------------------------------------------------------
-- Continuation byte: 10xxxxxx = 80..BF
---------------------------------------------------------------------------
function Is_Continuation (B : Byte) return Boolean is
(B in 16#80# .. 16#BF#);
---------------------------------------------------------------------------
-- Lead byte → sequence length (0 = invalid lead byte)
--
-- 00..7F → 1 (ASCII)
-- 80..BF → 0 (continuation, not a valid lead)
-- C0..C1 → 0 (overlong 2-byte for ASCII range)
-- C2..DF → 2
-- E0..EF → 3
-- F0..F4 → 4
-- F5..FF → 0 (would encode > U+10FFFF)
---------------------------------------------------------------------------
function Lead_Length (B : Byte) return Natural is
(if B <= 16#7F# then 1
elsif B <= 16#C1# then 0
elsif B <= 16#DF# then 2
elsif B <= 16#EF# then 3
elsif B <= 16#F4# then 4
else 0);
---------------------------------------------------------------------------
-- Codepoint → encoded byte count (RFC 3629 Section 3 table)
--
-- U+0000..U+007F → 1 byte
-- U+0080..U+07FF → 2 bytes
-- U+0800..U+FFFF → 3 bytes
-- U+10000..U+10FFFF → 4 bytes
---------------------------------------------------------------------------
function Encoded_Length (CP : Codepoint) return Positive is
(if CP <= 16#7F# then 1
elsif CP <= 16#7FF# then 2
elsif CP <= 16#FFFF# then 3
else 4);
---------------------------------------------------------------------------
-- Well-formedness per RFC 3629 Section 4 ABNF
--
-- UTF8-1 = %x00-7F
-- UTF8-2 = %xC2-DF UTF8-tail
-- UTF8-3 = %xE0 %xA0-BF UTF8-tail
-- / %xE1-EC UTF8-tail UTF8-tail
-- / %xED %x80-9F UTF8-tail (excludes surrogates)
-- / %xEE-EF UTF8-tail UTF8-tail
-- UTF8-4 = %xF0 %x90-BF UTF8-tail UTF8-tail
-- / %xF1-F3 UTF8-tail UTF8-tail UTF8-tail
-- / %xF4 %x80-8F UTF8-tail UTF8-tail (max U+10FFFF)
-- UTF8-tail = %x80-BF
---------------------------------------------------------------------------
function WF1 (B0 : Byte) return Boolean is
(B0 <= 16#7F#);
function WF2 (B0, B1 : Byte) return Boolean is
(B0 in 16#C2# .. 16#DF#
and then Is_Continuation (B1));
function WF3 (B0, B1, B2 : Byte) return Boolean is
((B0 = 16#E0#
and then B1 in 16#A0# .. 16#BF#
and then Is_Continuation (B2))
or else
(B0 in 16#E1# .. 16#EC#
and then Is_Continuation (B1)
and then Is_Continuation (B2))
or else
(B0 = 16#ED#
and then B1 in 16#80# .. 16#9F#
and then Is_Continuation (B2))
or else
(B0 in 16#EE# .. 16#EF#
and then Is_Continuation (B1)
and then Is_Continuation (B2)));
function WF4 (B0, B1, B2, B3 : Byte) return Boolean is
((B0 = 16#F0#
and then B1 in 16#90# .. 16#BF#
and then Is_Continuation (B2)
and then Is_Continuation (B3))
or else
(B0 in 16#F1# .. 16#F3#
and then Is_Continuation (B1)
and then Is_Continuation (B2)
and then Is_Continuation (B3))
or else
(B0 = 16#F4#
and then B1 in 16#80# .. 16#8F#
and then Is_Continuation (B2)
and then Is_Continuation (B3)));
---------------------------------------------------------------------------
-- Decoding formulas
--
-- Given well-formed bytes, extract the codepoint value.
-- Each Pre requires the corresponding WF predicate so the solver
-- can verify the result fits in Codepoint (0 .. 16#10_FFFF#).
---------------------------------------------------------------------------
function Decode_1 (B0 : Byte) return Codepoint is
(B0)
with Pre => WF1 (B0);
function Decode_2 (B0, B1 : Byte) return Codepoint is
((B0 - 16#C0#) * 64
+ (B1 - 16#80#))
with Pre => WF2 (B0, B1);
function Decode_3 (B0, B1, B2 : Byte) return Codepoint is
((B0 - 16#E0#) * 4096
+ (B1 - 16#80#) * 64
+ (B2 - 16#80#))
with Pre => WF3 (B0, B1, B2);
function Decode_4 (B0, B1, B2, B3 : Byte) return Codepoint is
((B0 - 16#F0#) * 262144
+ (B1 - 16#80#) * 4096
+ (B2 - 16#80#) * 64
+ (B3 - 16#80#))
with Pre => WF4 (B0, B1, B2, B3);
---------------------------------------------------------------------------
-- Encoding byte formulas
--
-- Given a codepoint in the correct range, compute each output byte.
-- Pre ensures the result fits in Byte (0 .. 255).
---------------------------------------------------------------------------
-- 1-byte encoding
function Enc_1_B0 (CP : Codepoint) return Byte is
(CP)
with Pre => CP <= 16#7F#;
-- 2-byte encoding
function Enc_2_B0 (CP : Codepoint) return Byte is
(16#C0# + CP / 64)
with Pre => CP in 16#80# .. 16#7FF#;
function Enc_2_B1 (CP : Codepoint) return Byte is
(16#80# + CP mod 64)
with Pre => CP in 16#80# .. 16#7FF#;
-- 3-byte encoding
function Enc_3_B0 (CP : Codepoint) return Byte is
(16#E0# + CP / 4096)
with Pre => CP in 16#800# .. 16#FFFF#;
function Enc_3_B1 (CP : Codepoint) return Byte is
(16#80# + (CP / 64) mod 64)
with Pre => CP in 16#800# .. 16#FFFF#;
function Enc_3_B2 (CP : Codepoint) return Byte is
(16#80# + CP mod 64)
with Pre => CP in 16#800# .. 16#FFFF#;
-- 4-byte encoding
function Enc_4_B0 (CP : Codepoint) return Byte is
(16#F0# + CP / 262144)
with Pre => CP in 16#1_0000# .. 16#10_FFFF#;
function Enc_4_B1 (CP : Codepoint) return Byte is
(16#80# + (CP / 4096) mod 64)
with Pre => CP in 16#1_0000# .. 16#10_FFFF#;
function Enc_4_B2 (CP : Codepoint) return Byte is
(16#80# + (CP / 64) mod 64)
with Pre => CP in 16#1_0000# .. 16#10_FFFF#;
function Enc_4_B3 (CP : Codepoint) return Byte is
(16#80# + CP mod 64)
with Pre => CP in 16#1_0000# .. 16#10_FFFF#;
---------------------------------------------------------------------------
-- Array-level predicates
--
-- These connect the byte-level checks to array positions.
-- Pre requires Source'Last < Positive'Last to guarantee that
-- Pos + 1, Pos + 2, Pos + 3 cannot overflow Positive.
---------------------------------------------------------------------------
-- Is there a well-formed UTF-8 sequence starting at Pos?
function Well_Formed_At
(Source : Byte_Array;
Pos : Positive) return Boolean
is (Pos in Source'Range
and then Lead_Length (Source (Pos)) >= 1
and then Source'Last - Pos >= Lead_Length (Source (Pos)) - 1
and then
(case Lead_Length (Source (Pos)) is
when 1 => WF1 (Source (Pos)),
when 2 => WF2 (Source (Pos), Source (Pos + 1)),
when 3 => WF3 (Source (Pos), Source (Pos + 1),
Source (Pos + 2)),
when 4 => WF4 (Source (Pos), Source (Pos + 1),
Source (Pos + 2), Source (Pos + 3)),
when others => False))
with Pre => Source'Last < Positive'Last;
-- Decoded codepoint at Pos (only meaningful when Well_Formed_At)
function Decoded_At
(Source : Byte_Array;
Pos : Positive) return Codepoint
is (case Lead_Length (Source (Pos)) is
when 1 => Decode_1 (Source (Pos)),
when 2 => Decode_2 (Source (Pos), Source (Pos + 1)),
when 3 => Decode_3 (Source (Pos), Source (Pos + 1),
Source (Pos + 2)),
when 4 => Decode_4 (Source (Pos), Source (Pos + 1),
Source (Pos + 2), Source (Pos + 3)),
when others => 0)
with Pre => Source'Last < Positive'Last
and then Well_Formed_At (Source, Pos);
-- Are the bytes at Pos the correct encoding of CP?
function Encoded_At
(Target : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
is (Pos in Target'Range
and then Target'Last - Pos >= Encoded_Length (CP) - 1
and then
(case Encoded_Length (CP) is
when 1 => Target (Pos) = Enc_1_B0 (CP),
when 2 => Target (Pos) = Enc_2_B0 (CP)
and then Target (Pos + 1) = Enc_2_B1 (CP),
when 3 => Target (Pos) = Enc_3_B0 (CP)
and then Target (Pos + 1) = Enc_3_B1 (CP)
and then Target (Pos + 2) = Enc_3_B2 (CP),
when 4 => Target (Pos) = Enc_4_B0 (CP)
and then Target (Pos + 1) = Enc_4_B1 (CP)
and then Target (Pos + 2) = Enc_4_B2 (CP)
and then Target (Pos + 3) = Enc_4_B3 (CP),
when others => False))
with Pre => Target'Last < Positive'Last;
end Lingenic_Text.UTF8_Spec;