-- 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
--
-- Ghost specification for Script_Extensions (UAX #24) file parsing.
--
-- ScriptExtensions.txt has the form:
--
-- CP_or_RANGE ; SCRIPT1 SCRIPT2 ... SCRIPTn # comment
--
-- The codepoint/range field and overall line structure are identical to
-- the standard UCD property file format, so this module reuses
-- UCD_Format_Spec.Is_Data_Line, Is_Range_Line, Line_First_CP, Line_Last_CP,
-- Next_Line_Start, etc.
--
-- The value field, however, contains a SET of space-separated four-letter
-- ISO 15924 script short-codes. This module adds:
--
-- 1. Token iteration helpers (Token_Start, Token_End, Next_Token_Start)
-- walking through the tokens of the value field.
--
-- 2. A recursive ghost function Expected_Scx_Has that, given the raw
-- source bytes, a line position, a codepoint, and a script index,
-- returns whether that script index should appear in CP's Script
-- Extensions set.
--
-- Every function here is Ghost — erased at compile time, zero runtime cost.
-- The solver unfolds expression function bodies directly into proof
-- contexts. The parser's postcondition references Expected_Scx_Has to
-- establish that the parsed per-codepoint script set matches the file's
-- semantics exactly.
--
-- Semantics of ScriptExtensions.txt:
-- Each codepoint appears at most once (as a single line or covered by
-- a range). If a codepoint is covered by some line, its set is the
-- tokens listed on that line. If no line covers a codepoint, the set
-- is the singleton {Script(CP)} — the primary script. The default
-- fallback is handled outside this spec; this spec characterizes only
-- what the FILE explicitly says.
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Format_Spec;
with Lingenic_Text.UCD_Parser;
package Lingenic_Text.Scx_Spec
with SPARK_Mode, Ghost, Pure
is
---------------------------------------------------------------------------
-- Layer 1: Token scanning inside the value field
--
-- A "token" is a maximal run of non-space, non-line-end, non-hash bytes
-- within the value field. Tokens are separated by one or more spaces
-- or tabs. The value field ends at '#', LF, CR, or end-of-source.
---------------------------------------------------------------------------
-- Is byte B a token-terminator inside a value field?
-- space, tab, LF, CR, '#'
function Is_Token_End (B : Byte) return Boolean
is (Is_Field_Space (B)
or else Is_Line_End (B)
or else B = Hash_Byte);
-- Scan from Pos forward skipping field spaces (NOT line ends or '#').
-- Returns the first non-space position, or 0 if a line-end or '#' or
-- end-of-source is hit first.
function Skip_Tok_Spaces
(Source : Byte_Array;
Pos : Positive) return Natural
is (if Is_Line_End (Source (Pos)) then 0
elsif Source (Pos) = Hash_Byte then 0
elsif not Is_Field_Space (Source (Pos)) then Pos
elsif Pos = Source'Last then 0
else Skip_Tok_Spaces (Source, Pos + 1))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Subprogram_Variant => (Decreases => Source'Last - Pos),
Post => (if Skip_Tok_Spaces'Result > 0 then
Skip_Tok_Spaces'Result in Pos .. Source'Last);
-- Length of the token starting at Pos — the number of consecutive
-- non-terminator bytes starting at Pos. Returns 0 if Source(Pos) is
-- already a terminator.
function Token_Length
(Source : Byte_Array;
Pos : Positive) return Natural
is (if Is_Token_End (Source (Pos)) then 0
elsif Pos = Source'Last then 1
else 1 + Token_Length (Source, Pos + 1))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Subprogram_Variant => (Decreases => Source'Last - Pos),
Post => Token_Length'Result <= Source'Last - Pos + 1;
-- Position immediately after the token starting at Pos.
-- If Pos is already a terminator, returns Pos.
function Token_End
(Source : Byte_Array;
Pos : Positive) return Positive
is (if Is_Token_End (Source (Pos)) then Pos
elsif Pos = Source'Last then Source'Last + 1
else Token_End (Source, Pos + 1))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Subprogram_Variant => (Decreases => Source'Last - Pos),
Post => Token_End'Result in Pos .. Source'Last + 1;
---------------------------------------------------------------------------
-- Layer 2: Token matching against Script_Names
--
-- Does the token [Tok_First .. Tok_First + Tok_Len - 1] in the
-- ScriptExtensions source equal the name at Script_Names (I) in the
-- Scripts.txt source buffer?
--
-- Note: the token lives in one byte buffer (the ScriptExtensions.txt
-- contents) while the name lives in a DIFFERENT byte buffer (the
-- Scripts.txt contents where Script_Names point). We pass BOTH
-- buffers explicitly.
---------------------------------------------------------------------------
-- Byte-by-byte equality between Src_A [AF .. AF + Len - 1] and
-- Src_B [BF .. BF + Len - 1]. Len = 0 is trivially equal.
function Two_Buf_Bytes_Equal
(Src_A : Byte_Array;
AF : Positive;
Src_B : Byte_Array;
BF : Positive;
Len : Natural) return Boolean
is (if Len = 0 then True
else Src_A (AF) = Src_B (BF)
and then (if Len = 1 then True
else Two_Buf_Bytes_Equal (Src_A, AF + 1,
Src_B, BF + 1,
Len - 1)))
with Pre => Src_A'First = 1
and then Src_A'Last < Positive'Last
and then Src_B'First = 1
and then Src_B'Last < Positive'Last
and then (if Len > 0 then
AF in Src_A'Range
and then BF in Src_B'Range
and then Src_A'Last - AF >= Len - 1
and then Src_B'Last - BF >= Len - 1),
Subprogram_Variant => (Decreases => Len);
-- Does the token at [Tok_First .. Tok_First + Tok_Len - 1] in Scx_Src
-- match Script_Names (I) in Script_Src?
function Ghost_Token_Matches
(Scx_Src : Byte_Array;
Tok_First : Positive;
Tok_Len : Natural;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
I : UCD_Parser.Property_Index) return Boolean
is (I >= 1
and then Tok_Len > 0
and then Script_Names (I).Last >= Script_Names (I).First
and then Script_Names (I).First in Script_Src'Range
and then Script_Names (I).Last in Script_Src'Range
and then Script_Names (I).Last - Script_Names (I).First + 1 = Tok_Len
and then Two_Buf_Bytes_Equal (Scx_Src, Tok_First,
Script_Src, Script_Names (I).First,
Tok_Len))
with Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then I in 1 .. UCD_Parser.Max_Value_Names
and then (if Tok_Len > 0 then
Tok_First in Scx_Src'Range
and then Scx_Src'Last - Tok_First >= Tok_Len - 1);
---------------------------------------------------------------------------
-- Layer 3: "Does any token on this line match Script_Idx?"
--
-- Recursively walks tokens in the value field from position Pos,
-- checking each against Script_Names (Script_Idx).
---------------------------------------------------------------------------
function Ghost_Value_Has_Script
(Scx_Src : Byte_Array;
Pos : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Idx : UCD_Parser.Property_Index) return Boolean
is (declare
Tok_Start : constant Natural := Skip_Tok_Spaces (Scx_Src, Pos);
begin
(if Tok_Start = 0 then False
else
(declare
TL : constant Natural := Token_Length (Scx_Src, Tok_Start);
Next : constant Positive := Token_End (Scx_Src, Tok_Start);
begin
(if TL = 0 then False
elsif Ghost_Token_Matches (Scx_Src, Tok_Start, TL,
Script_Src, Script_Names,
Script_Idx)
then True
elsif Next > Scx_Src'Last then False
else Ghost_Value_Has_Script (Scx_Src, Next,
Script_Src, Script_Names,
Script_Idx)))))
with Ghost,
Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then Pos in Scx_Src'Range
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then Script_Idx in 1 .. UCD_Parser.Max_Value_Names,
Subprogram_Variant => (Decreases => Scx_Src'Last - Pos);
---------------------------------------------------------------------------
-- Layer 4: Line-level membership — "does the data line starting at
-- Line_Start assert that CP has Script_Idx in its extension set?"
--
-- Composes value-field location (reusing UCD_Format_Spec) with the
-- token-walking predicate.
---------------------------------------------------------------------------
function Ghost_Line_Asserts
(Scx_Src : Byte_Array;
Line_Start : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Idx : UCD_Parser.Property_Index) return Boolean
is (declare
VS : constant Natural :=
UCD_Format_Spec.Value_Start (Scx_Src, Line_Start);
begin
(if VS = 0 then False
else Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, Script_Idx)))
with Ghost,
Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then Line_Start in Scx_Src'Range
and then UCD_Format_Spec.Is_Data_Line (Scx_Src, Line_Start)
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then Script_Idx in 1 .. UCD_Parser.Max_Value_Names;
---------------------------------------------------------------------------
-- Layer 5: File-level "covers" and membership
--
-- Does any line at or after Pos cover CP? (A stopping condition for
-- the main recursion.)
---------------------------------------------------------------------------
function Expected_Scx_Covers
(Scx_Src : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
is (Pos <= Scx_Src'Last
and then
((UCD_Format_Spec.Is_Data_Line (Scx_Src, Pos)
and then UCD_Format_Spec.Line_Covers_CP (Scx_Src, Pos, CP))
or else
(declare
NL : constant Positive :=
UCD_Format_Spec.Next_Line_Start (Scx_Src, Pos);
begin
NL <= Scx_Src'Last
and then Expected_Scx_Covers (Scx_Src, NL, CP))))
with Ghost,
Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then Pos in Scx_Src'Range,
Subprogram_Variant =>
(Decreases => Scx_Src'Last - Pos);
-- Does any line at or after Pos assert that CP has Script_Idx?
-- Because ScriptExtensions.txt lists each codepoint at most once,
-- there is no "later overwrites earlier" semantics: the first line
-- that covers CP (if any) is the authoritative one.
function Expected_Scx_Has
(Scx_Src : Byte_Array;
Pos : Positive;
CP : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Idx : UCD_Parser.Property_Index) return Boolean
is (Pos <= Scx_Src'Last
and then
(if UCD_Format_Spec.Is_Data_Line (Scx_Src, Pos)
and then UCD_Format_Spec.Line_Covers_CP (Scx_Src, Pos, CP)
then
Ghost_Line_Asserts (Scx_Src, Pos,
Script_Src, Script_Names, Script_Idx)
else
(declare
NL : constant Positive :=
UCD_Format_Spec.Next_Line_Start (Scx_Src, Pos);
begin
NL <= Scx_Src'Last
and then Expected_Scx_Has (Scx_Src, NL, CP,
Script_Src, Script_Names,
Script_Idx))))
with Ghost,
Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then Pos in Scx_Src'Range
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then Script_Idx in 1 .. UCD_Parser.Max_Value_Names,
Subprogram_Variant =>
(Decreases => Scx_Src'Last - Pos);
-- Boundary-safe wrapper: what does the file say about (CP, Script_Idx)
-- starting from Pos forward? Returns False when Pos > Scx_Src'Last.
--
-- Deliberately NOT an expression function: the solver treats this as
-- opaque and relies on the postcondition when it needs to see inside.
-- This prevents cascading auto-inlining of Expected_Scx_Has into
-- nested loop invariant VCs where two identical opaque calls can be
-- matched by congruence instead.
function Expected_Scx_Has_From
(Scx_Src : Byte_Array;
Pos : Positive;
CP : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Idx : UCD_Parser.Property_Index) return Boolean
with Ghost,
Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then Script_Idx in 1 .. UCD_Parser.Max_Value_Names,
Post => Expected_Scx_Has_From'Result =
(if Pos > Scx_Src'Last then False
else Expected_Scx_Has (Scx_Src, Pos, CP,
Script_Src, Script_Names,
Script_Idx));
end Lingenic_Text.Scx_Spec;