-- 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
--
-- Grapheme cluster segmentation (UAX #29).
--
-- Implements the Unicode Grapheme Cluster Boundary algorithm as a forward
-- state machine over UTF-8 text. Each call to Next_Grapheme_Cluster_Break
-- returns the byte position of the next grapheme cluster boundary.
--
-- The algorithm references the ghost specification in Graphemes_Spec,
-- which encodes GB rules 3 through 999 as expression functions.
--
-- Invalid UTF-8 bytes are treated as single-codepoint clusters with
-- GBP = Other.
--
-- SPARK Platinum: the postcondition references the recursive ghost function
-- Next_GCB_From, which simulates the algorithm as an expression function.
-- GNATprove verifies the implementation matches this specification.
-------------------------------------------------------------------------------
with Lingenic_Text.Properties;
with Lingenic_Text.Graphemes_Spec;
with Lingenic_Text.UTF8_Spec;
package Lingenic_Text.Graphemes
with SPARK_Mode
is
use type Graphemes_Spec.Conjunct_State;
---------------------------------------------------------------------------
-- Ghost state record for grapheme break state machine
--
-- Plain record (not "with Ghost") because GNAT 15 rejects ghost types
-- as parameters. Used only in ghost expression functions.
---------------------------------------------------------------------------
type GCB_State is record
Prev_GBP : Graphemes_Spec.GBP_Value;
Ext_Pict_Seq : Boolean;
Conj_State : Graphemes_Spec.Conjunct_State;
RI_Count : Natural;
end record;
---------------------------------------------------------------------------
-- Ghost helper functions
--
-- These mirror the runtime decode + property lookup logic as expression
-- functions so the solver can unfold them.
---------------------------------------------------------------------------
-- Step length at position Cur: how many bytes the codepoint consumes.
-- Mirrors UTF8.Decode: well-formed → Lead_Length, invalid → 1.
function Ghost_Step_Length
(Text : Byte_Array;
Cur : Positive) return Positive
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then UTF8_Spec.Lead_Length (Text (Cur))
else 1)
with Ghost,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range;
-- Decoded codepoint at Cur.
-- Mirrors UTF8.Decode: well-formed → Decoded_At, invalid → 0.
function Ghost_CP
(Text : Byte_Array;
Cur : Positive) return Codepoint
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then UTF8_Spec.Decoded_At (Text, Cur)
else 0)
with Ghost,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range;
-- GBP value at Cur.
-- The invalid branch uses GBP_To_Abstract(0) rather than the literal
-- GBP_Other so the solver can connect this to the body's computation
-- path (where First_GBP/This_GBP_Idx is set to 0 on invalid).
function Ghost_GBP
(Text : Byte_Array;
Cur : Positive) return Graphemes_Spec.GBP_Value
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then Properties.GBP_To_Abstract
(Properties.Get_GBP (UTF8_Spec.Decoded_At (Text, Cur)))
else Properties.GBP_To_Abstract (0))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
-- ExtPict flag at Cur.
function Ghost_ExtPict
(Text : Byte_Array;
Cur : Positive) return Boolean
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then Properties.Get_ExtPict (UTF8_Spec.Decoded_At (Text, Cur))
else False)
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
-- InCB value at Cur.
-- Invalid branch uses InCB_To_Abstract(0) to match the body's path.
function Ghost_InCB
(Text : Byte_Array;
Cur : Positive) return Graphemes_Spec.InCB_Value
is (if UTF8_Spec.Well_Formed_At (Text, Cur)
then Properties.InCB_To_Abstract
(Properties.Get_InCB (UTF8_Spec.Decoded_At (Text, Cur)))
else Properties.InCB_To_Abstract (0))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
-- Break decision given state St and codepoint at Cur.
function Ghost_Break
(St : GCB_State;
Text : Byte_Array;
Cur : Positive) return Boolean
is (Graphemes_Spec.Is_Grapheme_Break
(A_GBP => St.Prev_GBP,
B_GBP => Ghost_GBP (Text, Cur),
B_ExtPict => Ghost_ExtPict (Text, Cur),
B_InCB => Ghost_InCB (Text, Cur),
In_ExtPict_Seq => St.Ext_Pict_Seq,
RI_Count_Odd => St.RI_Count mod 2 = 1,
In_Conjunct => St.Conj_State = Graphemes_Spec.CS_Linker))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
-- Max RI counter (same as body).
Ghost_Max_RI : constant := Natural'Last - 1;
-- Updated state after processing codepoint at Cur (no break).
-- Mirrors the state update logic in the loop body (lines 152-169).
function Updated_State
(St : GCB_State;
Text : Byte_Array;
Cur : Positive) return GCB_State
is (GCB_State'
(Prev_GBP => Ghost_GBP (Text, Cur),
Ext_Pict_Seq => Graphemes_Spec.Next_ExtPict_Seq
(St.Ext_Pict_Seq,
Ghost_GBP (Text, Cur),
Ghost_ExtPict (Text, Cur)),
Conj_State => Graphemes_Spec.Next_Conjunct_State
(St.Conj_State,
Ghost_InCB (Text, Cur)),
RI_Count =>
(if Ghost_GBP (Text, Cur) = Graphemes_Spec.GBP_Regional_Indicator
then (if St.RI_Count < Ghost_Max_RI - 1
then St.RI_Count + 1
else St.RI_Count)
else 0)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur in Text'Range
and then Properties.Initialized;
-- Initial state after processing the first codepoint at Pos.
-- Mirrors lines 81-86 in the body.
function Initial_State
(Text : Byte_Array;
Pos : Positive) return GCB_State
is (GCB_State'
(Prev_GBP => Ghost_GBP (Text, Pos),
Ext_Pict_Seq => Graphemes_Spec.Next_ExtPict_Seq
(False,
Ghost_GBP (Text, Pos),
Ghost_ExtPict (Text, Pos)),
Conj_State => Graphemes_Spec.Next_Conjunct_State
(Graphemes_Spec.CS_None,
Ghost_InCB (Text, Pos)),
RI_Count =>
(if Ghost_GBP (Text, Pos) = Graphemes_Spec.GBP_Regional_Indicator
then 1 else 0)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Pos in Text'Range
and then Properties.Initialized;
---------------------------------------------------------------------------
-- Recursive ghost function: simulates the forward loop.
--
-- Given Text, current position Cur, and accumulated state St,
-- returns the position of the next grapheme cluster break.
--
-- The recursion decreases Text'Last - Cur + 1 at each step because
-- Ghost_Step_Length >= 1, so Cur strictly increases.
---------------------------------------------------------------------------
function Next_GCB
(Text : Byte_Array;
Cur : Positive;
St : GCB_State) return Positive
is (if Cur not in Text'Range then
-- GB2: past end of text
(if Cur <= Text'Last + 1 then Cur else Text'Last + 1)
elsif Ghost_Break (St, Text, Cur) then
-- Break found at Cur
Cur
elsif Cur > Text'Last - Ghost_Step_Length (Text, Cur) + 1 then
-- This codepoint reaches end of text; return past end
Cur + Ghost_Step_Length (Text, Cur)
else
-- No break: advance and recurse
Next_GCB (Text,
Cur + Ghost_Step_Length (Text, Cur),
Updated_State (St, Text, Cur)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Cur > 0
and then Properties.Initialized,
Subprogram_Variant => (Decreases => Text'Last - Cur + 1);
---------------------------------------------------------------------------
-- Top-level wrapper: computes the break starting from Pos.
--
-- Handles the first codepoint (GB1), then delegates to Next_GCB
-- for subsequent codepoints.
---------------------------------------------------------------------------
function Next_GCB_From
(Text : Byte_Array;
Pos : Positive) return Positive
is (if Pos > Text'Last - Ghost_Step_Length (Text, Pos) + 1 then
-- First codepoint reaches end; single-codepoint cluster (GB2)
Pos + Ghost_Step_Length (Text, Pos)
else
-- Recurse starting from second codepoint position
Next_GCB (Text,
Pos + Ghost_Step_Length (Text, Pos),
Initial_State (Text, Pos)))
with Ghost,
Global => Properties.Property_State,
Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Pos in Text'Range
and then Properties.Initialized;
---------------------------------------------------------------------------
-- Next_Grapheme_Cluster_Break
--
-- Given a UTF-8 encoded byte array and a current byte position Pos,
-- finds the next grapheme cluster boundary. Returns Next_Pos such that
-- Text(Pos .. Next_Pos - 1) is a complete grapheme cluster.
--
-- SPARK Platinum postcondition: Next_Pos equals the result of the
-- recursive ghost specification Next_GCB_From.
---------------------------------------------------------------------------
procedure Next_Grapheme_Cluster_Break
(Text : Byte_Array;
Pos : Positive;
Next_Pos : out Positive)
with Pre => Text'First = 1
and then Text'Last >= 1
and then Text'Last < Positive'Last
and then Pos in Text'Range
and then Properties.Initialized,
Post => Next_Pos = Next_GCB_From (Text, Pos)
and then Next_Pos > Pos
and then Next_Pos <= Text'Last + 1;
end Lingenic_Text.Graphemes;