-- 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
--
-- Script_Extensions parser body — Platinum-proved.
--
-- Implements Parse_Script_Extensions so that its output exactly matches the
-- ghost specification in Lingenic_Text.Scx_Spec. The body is organized in
-- layers, each layer's private helpers proving equivalence to the
-- corresponding ghost function in Scx_Spec or UCD_Format_Spec:
--
-- Layer 1: Runtime token scanners (R_Skip_Tok_Spaces, R_Token_Length,
-- R_Token_End) mirroring Scx_Spec.Skip_Tok_Spaces,
-- Scx_Spec.Token_Length, Scx_Spec.Token_End.
--
-- Layer 2: Token matching against a Script_Names entry, linked to
-- Scx_Spec.Ghost_Token_Matches.
--
-- Layer 3: Per-line set building, with a universal postcondition linking
-- the produced Script_Set to Scx_Spec.Ghost_Value_Has_Script.
--
-- Layer 4: Pool find-or-insert, preserving well-formedness and answering
-- Pool_Has queries.
--
-- Layer 5: Line header parsing (is-data, CP range, value start) with a
-- postcondition linking to UCD_Format_Spec.Is_Data_Line,
-- Line_First_CP, Line_Last_CP, Value_Start.
--
-- Layer 6: Ghost lemmas advancing Expected_Scx_Has_From over non-data
-- lines, over data lines that don't cover CP, and folding a
-- data line that does cover CP into Ghost_Line_Asserts.
--
-- Layer 7: Parse_Script_Extensions outer loop with the two-part
-- first-match-wins invariant.
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Format_Spec;
package body Lingenic_Text.Scx_Parser
with SPARK_Mode
is
---------------------------------------------------------------------------
-- Pool_Has body (regular function, opaque to the solver).
---------------------------------------------------------------------------
function Pool_Has
(Pool : Scx_Pool_Array;
Pool_End : Natural;
P : Scx_Pool_Id;
Script_Idx : UCD_Parser.Property_Index) return Boolean
is
begin
return P >= 1
and then P <= Pool_End
and then P <= Max_Unique_Scx
and then Set_Has (Pool (P), Script_Idx);
end Pool_Has;
---------------------------------------------------------------------------
-- Layer 1: Runtime token scanners
--
-- Each scanner is a regular (non-ghost) iterative function whose
-- postcondition equates its result to the corresponding Scx_Spec ghost
-- expression function. The loop invariant states that the ghost
-- function's value at the original position equals its value at the
-- current scan position — so early returns can conclude the post
-- directly via a single ghost unfolding step.
---------------------------------------------------------------------------
function R_Skip_Tok_Spaces
(Source : Byte_Array;
Pos : Positive) return Natural
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => R_Skip_Tok_Spaces'Result
= Scx_Spec.Skip_Tok_Spaces (Source, Pos);
function R_Token_Length
(Source : Byte_Array;
Pos : Positive) return Natural
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => R_Token_Length'Result = Scx_Spec.Token_Length (Source, Pos);
function R_Token_End
(Source : Byte_Array;
Pos : Positive) return Positive
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Post => R_Token_End'Result = Scx_Spec.Token_End (Source, Pos)
and then R_Token_End'Result in Pos .. Source'Last + 1;
---------------------------------------------------------------------------
-- R_Skip_Tok_Spaces body
---------------------------------------------------------------------------
function R_Skip_Tok_Spaces
(Source : Byte_Array;
Pos : Positive) return Natural
is
P : Positive := Pos;
begin
loop
pragma Loop_Invariant (P in Pos .. Source'Last);
pragma Loop_Invariant
(Scx_Spec.Skip_Tok_Spaces (Source, Pos)
= Scx_Spec.Skip_Tok_Spaces (Source, P));
pragma Loop_Variant (Decreases => Source'Last - P);
if Is_Line_End (Source (P)) then
return 0;
elsif Source (P) = Hash_Byte then
return 0;
elsif not Is_Field_Space (Source (P)) then
return P;
elsif P = Source'Last then
return 0;
end if;
P := P + 1;
end loop;
end R_Skip_Tok_Spaces;
---------------------------------------------------------------------------
-- R_Token_Length body
--
-- Invariant: Token_Length(Source, Pos) = Len + Token_Length(Source, P).
-- At loop entry, Len = 0, P = Pos — trivially true. Each iteration
-- advances both by 1 in lock-step, matching the ghost function's
-- "1 + Token_Length(Source, Pos + 1)" recursive step.
---------------------------------------------------------------------------
function R_Token_Length
(Source : Byte_Array;
Pos : Positive) return Natural
is
P : Positive := Pos;
Len : Natural := 0;
begin
loop
pragma Loop_Invariant (P in Pos .. Source'Last);
pragma Loop_Invariant (Len = P - Pos);
pragma Loop_Invariant
(Scx_Spec.Token_Length (Source, Pos)
= Len + Scx_Spec.Token_Length (Source, P));
pragma Loop_Variant (Decreases => Source'Last - P);
-- Inline Scx_Spec.Is_Token_End (a ghost function) with its body:
-- Is_Field_Space OR Is_Line_End OR Hash_Byte.
if Is_Field_Space (Source (P))
or else Is_Line_End (Source (P))
or else Source (P) = Hash_Byte
then
-- Token_Length(Source, P) = 0
return Len;
elsif P = Source'Last then
-- Token_Length(Source, P) = 1
return Len + 1;
end if;
Len := Len + 1;
P := P + 1;
end loop;
end R_Token_Length;
---------------------------------------------------------------------------
-- R_Token_End body
--
-- Invariant: Token_End(Source, Pos) = Token_End(Source, P). The ghost
-- function recurses past all non-terminator bytes and returns Pos at
-- the first terminator, or Source'Last + 1 at end-of-source.
---------------------------------------------------------------------------
function R_Token_End
(Source : Byte_Array;
Pos : Positive) return Positive
is
P : Positive := Pos;
begin
loop
pragma Loop_Invariant (P in Pos .. Source'Last);
pragma Loop_Invariant
(Scx_Spec.Token_End (Source, Pos) = Scx_Spec.Token_End (Source, P));
pragma Loop_Variant (Decreases => Source'Last - P);
if Is_Field_Space (Source (P))
or else Is_Line_End (Source (P))
or else Source (P) = Hash_Byte
then
-- Token_End(Source, P) = P
return P;
elsif P = Source'Last then
-- Token_End(Source, P) = Source'Last + 1
return Source'Last + 1;
end if;
P := P + 1;
end loop;
end R_Token_End;
---------------------------------------------------------------------------
-- Layer 2a: Cross-buffer byte equality
--
-- Mirrors Scx_Spec.Two_Buf_Bytes_Equal. The invariant peels the
-- prefix of compared bytes out of the recursive ghost function and
-- leaves the suffix tail — matching the left-to-right structure of
-- the recursion.
---------------------------------------------------------------------------
function R_Two_Buf_Equal
(Src_A : Byte_Array;
AF : Positive;
Src_B : Byte_Array;
BF : Positive;
Len : Natural) return Boolean
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),
Post => R_Two_Buf_Equal'Result
= Scx_Spec.Two_Buf_Bytes_Equal (Src_A, AF, Src_B, BF, Len);
function R_Two_Buf_Equal
(Src_A : Byte_Array;
AF : Positive;
Src_B : Byte_Array;
BF : Positive;
Len : Natural) return Boolean
is
K : Natural := 0;
begin
if Len = 0 then
return True;
end if;
loop
pragma Loop_Invariant (K in 0 .. Len - 1);
pragma Loop_Invariant
(Scx_Spec.Two_Buf_Bytes_Equal (Src_A, AF, Src_B, BF, Len)
= Scx_Spec.Two_Buf_Bytes_Equal
(Src_A, AF + K, Src_B, BF + K, Len - K));
pragma Loop_Variant (Decreases => Len - K);
if Src_A (AF + K) /= Src_B (BF + K) then
return False;
end if;
if K = Len - 1 then
return True;
end if;
K := K + 1;
end loop;
end R_Two_Buf_Equal;
---------------------------------------------------------------------------
-- Layer 2b: Token matches a specific Script_Names entry
--
-- Mirrors Scx_Spec.Ghost_Token_Matches byte-for-byte. The post links
-- the runtime answer to the ghost function directly.
---------------------------------------------------------------------------
function Token_Matches_Name
(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
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),
Post => Token_Matches_Name'Result
= Scx_Spec.Ghost_Token_Matches
(Scx_Src, Tok_First, Tok_Len,
Script_Src, Script_Names, I);
function Token_Matches_Name
(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
Name : constant UCD_Parser.Value_Name := Script_Names (I);
begin
if Tok_Len = 0 then
return False;
end if;
if Name.Last < Name.First then
return False;
end if;
if Name.First not in Script_Src'Range then
return False;
end if;
if Name.Last not in Script_Src'Range then
return False;
end if;
if Name.Last - Name.First + 1 /= Tok_Len then
return False;
end if;
return R_Two_Buf_Equal
(Scx_Src, Tok_First,
Script_Src, Name.First,
Tok_Len);
end Token_Matches_Name;
---------------------------------------------------------------------------
-- Layer 2c: Does the value field at VS list Script_Names(Script_Idx)?
--
-- Runtime walker mirroring Scx_Spec.Ghost_Value_Has_Script for a
-- fixed Script_Idx. Loop invariant: the ghost answer from VS equals
-- the ghost answer from the current token position Cur.
---------------------------------------------------------------------------
function R_Value_Has_Script
(Scx_Src : Byte_Array;
VS : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Idx : UCD_Parser.Property_Index) return Boolean
with Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then VS 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,
Post => R_Value_Has_Script'Result
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, Script_Idx);
function R_Value_Has_Script
(Scx_Src : Byte_Array;
VS : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Idx : UCD_Parser.Property_Index) return Boolean
is
Cur : Positive := VS;
begin
loop
pragma Loop_Invariant (Cur in VS .. Scx_Src'Last);
pragma Loop_Invariant
(Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, Script_Idx)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, Cur, Script_Src, Script_Names, Script_Idx));
pragma Loop_Variant (Decreases => Scx_Src'Last - Cur);
declare
Tok_Start : constant Natural :=
R_Skip_Tok_Spaces (Scx_Src, Cur);
begin
if Tok_Start = 0 then
-- Ghost_Value_Has_Script (Cur, ...) = False by its body
-- (Skip_Tok_Spaces = 0 ⇒ the first branch returns False).
return False;
end if;
declare
TL : constant Natural :=
R_Token_Length (Scx_Src, Tok_Start);
Next : constant Positive :=
R_Token_End (Scx_Src, Tok_Start);
begin
if TL = 0 then
return False;
end if;
if Token_Matches_Name
(Scx_Src, Tok_Start, TL,
Script_Src, Script_Names, Script_Idx)
then
return True;
end if;
if Next > Scx_Src'Last then
return False;
end if;
Cur := Next;
end;
end;
end loop;
end R_Value_Has_Script;
---------------------------------------------------------------------------
-- Layer 3: Build per-line Script_Set
--
-- For a data line whose value field starts at VS, construct a
-- Script_Set listing exactly the script indices S in 1..Script_Count
-- for which Scx_Spec.Ghost_Value_Has_Script holds.
--
-- Strategy: iterate S from 1..Script_Count, calling R_Value_Has_Script
-- once per index, and add matching indices to the set. The outer-loop
-- invariant assembles the Set_Has postcondition one index at a time.
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Ghost helper lemma: appending a new item X at position Count+1
-- doesn't change Set_Has_From membership for any Idx /= X.
--
-- This is the structural fact needed to carry Build_Line_Set's
-- "Set_Has = Ghost_Value_Has_Script" invariant across an iteration
-- that appends a fresh element. Inductive on From, variant
-- Max_Scx_Size - From.
---------------------------------------------------------------------------
procedure Lemma_Set_Has_From_Append_Ne
(S_Old : Script_Set;
S_New : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => Max_Scx_Size - From),
Pre => From in 1 .. Max_Scx_Size
and then S_Old.Count in 0 .. Max_Scx_Size - 1
and then S_New.Count = S_Old.Count + 1
and then (for all K in 1 .. S_Old.Count =>
S_New.Items (K) = S_Old.Items (K))
and then S_New.Items (S_New.Count) /= Idx,
Post => Set_Has_From (S_New, Idx, From)
= Set_Has_From (S_Old, Idx, From);
procedure Lemma_Set_Has_From_Append_Ne
(S_Old : Script_Set;
S_New : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
is
begin
if From < Max_Scx_Size then
Lemma_Set_Has_From_Append_Ne (S_Old, S_New, Idx, From + 1);
end if;
end Lemma_Set_Has_From_Append_Ne;
---------------------------------------------------------------------------
-- Ghost helper lemma: appending a new item X (at Count+1) preserves
-- Set_Has membership for any Idx /= X.
--
-- This is the Set_Has-level wrapper around Lemma_Set_Has_From_Append_Ne.
-- It internally calls the From-level lemma and then handles the
-- Count >= 1 case split that bridges Set_Has_From to Set_Has.
---------------------------------------------------------------------------
procedure Lemma_Append_Preserves_Set_Has
(S_Old : Script_Set;
S_New : Script_Set;
Idx : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
Pre => S_Old.Count in 0 .. Max_Scx_Size - 1
and then S_New.Count = S_Old.Count + 1
and then (for all K in 1 .. S_Old.Count =>
S_New.Items (K) = S_Old.Items (K))
and then S_New.Items (S_New.Count) /= Idx,
Post => Set_Has (S_New, Idx) = Set_Has (S_Old, Idx);
procedure Lemma_Append_Preserves_Set_Has
(S_Old : Script_Set;
S_New : Script_Set;
Idx : UCD_Parser.Property_Index)
is
begin
Lemma_Set_Has_From_Append_Ne (S_Old, S_New, Idx, 1);
-- Now: Set_Has_From (S_New, Idx, 1) = Set_Has_From (S_Old, Idx, 1).
-- Set_Has (S_New, Idx) = True AND Set_Has_From (S_New, Idx, 1)
-- = Set_Has_From (S_Old, Idx, 1).
-- Set_Has (S_Old, Idx) = (Old.Count >= 1) AND Set_Has_From (...).
-- Case Old.Count = 0: both Set_Has_From = False, both Set_Has = False.
-- Case Old.Count >= 1: both Set_Has = Set_Has_From. QED.
end Lemma_Append_Preserves_Set_Has;
---------------------------------------------------------------------------
-- Ghost helper lemma: if Items(Count) = Idx, then
-- Set_Has_From (S, Idx, From) for any From in 1..Count.
--
-- Inductive from From up to Count. At Count the base case is
-- trivially true; each step follows from the IH via the OR branch
-- of Set_Has_From's definition.
---------------------------------------------------------------------------
procedure Lemma_Set_Has_From_At
(S : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => S.Count - From),
Pre => From in 1 .. Max_Scx_Size
and then S.Count in From .. Max_Scx_Size
and then S.Items (S.Count) = Idx,
Post => Set_Has_From (S, Idx, From);
procedure Lemma_Set_Has_From_At
(S : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
is
begin
if From < S.Count then
Lemma_Set_Has_From_At (S, Idx, From + 1);
end if;
end Lemma_Set_Has_From_At;
---------------------------------------------------------------------------
-- Ghost helper lemma: if no item in positions From..Count equals Idx,
-- then Set_Has_From (S, Idx, From) is False.
--
-- Inductive from From upwards. At From > Count the base is trivially
-- False. Each step unfolds the definition: Items(From) /= Idx, and
-- the OR branch is False by IH.
---------------------------------------------------------------------------
procedure Lemma_Set_Has_From_Bound
(S : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => Max_Scx_Size - From),
Pre => From in 1 .. Max_Scx_Size
and then S.Count in 0 .. Max_Scx_Size
and then (for all K in From .. S.Count =>
S.Items (K) /= Idx),
Post => not Set_Has_From (S, Idx, From);
procedure Lemma_Set_Has_From_Bound
(S : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
is
begin
if From <= S.Count and then From < Max_Scx_Size then
Lemma_Set_Has_From_Bound (S, Idx, From + 1);
end if;
end Lemma_Set_Has_From_Bound;
---------------------------------------------------------------------------
-- Ghost lemma: structurally equal Script_Sets yield equal Set_Has_From.
--
-- If A.Count = B.Count and A.Items (1 .. Count) = B.Items (1 .. Count),
-- then Set_Has_From (A, Idx, From) = Set_Has_From (B, Idx, From).
-- This bridges Pool_Find_Or_Insert's Sets_Equal postcondition to
-- Set_Has (and hence Pool_Has) equality.
---------------------------------------------------------------------------
procedure Lemma_Sets_Equal_Set_Has_From
(A : Script_Set;
B : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => Max_Scx_Size - From),
Pre => From in 1 .. Max_Scx_Size
and then A.Count in 0 .. Max_Scx_Size
and then A.Count = B.Count
and then (for all K in 1 .. A.Count =>
A.Items (K) = B.Items (K)),
Post => Set_Has_From (A, Idx, From)
= Set_Has_From (B, Idx, From);
procedure Lemma_Sets_Equal_Set_Has_From
(A : Script_Set;
B : Script_Set;
Idx : UCD_Parser.Property_Index;
From : Positive)
is
begin
if From <= A.Count and then From < Max_Scx_Size then
Lemma_Sets_Equal_Set_Has_From (A, B, Idx, From + 1);
end if;
end Lemma_Sets_Equal_Set_Has_From;
---------------------------------------------------------------------------
-- Ghost lemma: structurally equal Script_Sets have equal Set_Has for
-- every script index in 1 .. N.
--
-- This is the universally quantified wrapper around
-- Lemma_Sets_Equal_Set_Has_From. One call replaces a for-loop of
-- per-index calls, avoiding inner loop cut points.
---------------------------------------------------------------------------
procedure Lemma_Sets_Equal_Set_Has_All
(A : Script_Set;
B : Script_Set;
N : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => N),
Pre => A.Count in 0 .. Max_Scx_Size
and then A.Count = B.Count
and then (for all K in 1 .. A.Count =>
A.Items (K) = B.Items (K)),
Post => (for all Idx in UCD_Parser.Property_Index range 1 .. N =>
Set_Has (A, Idx) = Set_Has (B, Idx));
procedure Lemma_Sets_Equal_Set_Has_All
(A : Script_Set;
B : Script_Set;
N : UCD_Parser.Property_Index)
is
begin
Lemma_Sets_Equal_Set_Has_From (A, B, N, 1);
if N > 1 then
Lemma_Sets_Equal_Set_Has_All (A, B, N - 1);
end if;
end Lemma_Sets_Equal_Set_Has_All;
---------------------------------------------------------------------------
-- Ghost lemma: after appending script index S to the set, the
-- Set_Has = Ghost_Value_Has_Script invariant extends from 1..S-1
-- to 1..S.
--
-- The critical insight is that the old invariant (for TT in 1..S-1)
-- is a PRECONDITION (axiom) of this procedure, so it survives the
-- inner loop's cut point — unlike an outer loop invariant that
-- would be lost.
---------------------------------------------------------------------------
procedure Lemma_Build_Line_Set_Extend
(Old_R : Script_Set;
New_R : Script_Set;
S : UCD_Parser.Property_Index;
Scx_Src : Byte_Array;
VS : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array)
with Ghost,
Always_Terminates,
Pre => S in 1 .. Max_Scx_Size
and then Old_R.Count in 0 .. Max_Scx_Size - 1
and then New_R.Count = Old_R.Count + 1
and then (for all K in 1 .. Old_R.Count =>
New_R.Items (K) = Old_R.Items (K))
and then New_R.Items (New_R.Count) = S
and then Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then VS in Scx_Src'Range
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, S)
and then (for all TT in UCD_Parser.Property_Index
range 1 .. S - 1 =>
Set_Has (Old_R, TT)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src,
Script_Names, TT)),
Post => (for all TT in UCD_Parser.Property_Index
range 1 .. S =>
Set_Has (New_R, TT)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, TT));
procedure Lemma_Build_Line_Set_Extend
(Old_R : Script_Set;
New_R : Script_Set;
S : UCD_Parser.Property_Index;
Scx_Src : Byte_Array;
VS : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array)
is
begin
-- S is now in the set:
Lemma_Set_Has_From_At (New_R, S, 1);
-- For TT < S, membership is preserved (appended S /= TT).
-- The precondition axiom gives Set_Has(Old_R, TT) = GVHS(TT),
-- so after chaining: Set_Has(New_R, TT) = GVHS(TT).
for SS in UCD_Parser.Property_Index range 1 .. S - 1 loop
pragma Loop_Invariant
(Old_R.Count in 0 .. Max_Scx_Size - 1);
pragma Loop_Invariant
(New_R.Count = Old_R.Count + 1);
pragma Loop_Invariant
(New_R.Items (New_R.Count) = S);
pragma Loop_Invariant
(for all K in 1 .. Old_R.Count =>
New_R.Items (K) = Old_R.Items (K));
pragma Loop_Invariant
(Set_Has (New_R, S));
pragma Loop_Invariant
(for all TT in UCD_Parser.Property_Index
range 1 .. SS - 1 =>
Set_Has (New_R, TT)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, TT));
-- Instantiate the precondition's quantifier for SS:
pragma Assert
(Set_Has (Old_R, SS)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, SS));
Lemma_Append_Preserves_Set_Has (Old_R, New_R, SS);
-- Chain: Set_Has(New_R, SS) = Set_Has(Old_R, SS) = GVHS(SS)
pragma Assert
(Set_Has (New_R, SS)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, SS));
end loop;
end Lemma_Build_Line_Set_Extend;
procedure Build_Line_Set
(Scx_Src : Byte_Array;
VS : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index;
Result : out Script_Set)
with Pre => Scx_Src'First = 1
and then Scx_Src'Last < Positive'Last
and then VS in Scx_Src'Range
and then Script_Src'First = 1
and then Script_Src'Last < Positive'Last
and then Script_Count in 1 .. UCD_Parser.Max_Value_Names
and then Script_Count <= Max_Scx_Size,
Post => Result.Count in 0 .. Max_Scx_Size
and then Result.Count <= Script_Count
and then
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Set_Has (Result, S)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, S));
procedure Build_Line_Set
(Scx_Src : Byte_Array;
VS : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index;
Result : out Script_Set)
is
begin
Result := (Count => 0, Items => [others => 0]);
for S in UCD_Parser.Property_Index range 1 .. Script_Count loop
pragma Loop_Invariant (Result.Count in 0 .. S - 1);
pragma Loop_Invariant (Result.Count <= Max_Scx_Size);
pragma Loop_Invariant
(for all SS in UCD_Parser.Property_Index range 1 .. S - 1 =>
Set_Has (Result, SS)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, SS));
pragma Loop_Invariant
(for all K in 1 .. Result.Count =>
Result.Items (K) in 1 .. S - 1);
declare
Old_Result : constant Script_Set := Result
with Ghost;
Hit : constant Boolean :=
R_Value_Has_Script
(Scx_Src, VS, Script_Src, Script_Names, S);
begin
if Hit then
Result.Count := Result.Count + 1;
Result.Items (Result.Count) := S;
Lemma_Build_Line_Set_Extend
(Old_R => Old_Result,
New_R => Result,
S => S,
Scx_Src => Scx_Src,
VS => VS,
Script_Src => Script_Src,
Script_Names => Script_Names);
else
Lemma_Set_Has_From_Bound (Result, S, 1);
end if;
end;
end loop;
end Build_Line_Set;
---------------------------------------------------------------------------
-- Layer 4: Pool find-or-insert
--
-- Structural equality between two Script_Sets, followed by a linear
-- scan over the existing pool. If no matching set is found, append
-- the candidate. On overflow (Pool_End already at Max_Unique_Scx and
-- no match), signal Full := True so the caller can fail cleanly.
---------------------------------------------------------------------------
function Sets_Equal (A, B : Script_Set) return Boolean
with Post => Sets_Equal'Result =
(A.Count = B.Count
and then (for all K in 1 .. A.Count =>
A.Items (K) = B.Items (K)));
function Sets_Equal (A, B : Script_Set) return Boolean is
begin
if A.Count /= B.Count then
return False;
end if;
for K in 1 .. A.Count loop
pragma Loop_Invariant
(for all J in 1 .. K - 1 => A.Items (J) = B.Items (J));
if A.Items (K) /= B.Items (K) then
return False;
end if;
end loop;
return True;
end Sets_Equal;
---------------------------------------------------------------------------
-- Ghost lemma: Pool_Has is preserved when pool entries are unchanged.
--
-- If Pool_Old(P) = Pool_New(P) for some P, and P <= Old_End <= New_End,
-- then Pool_Has (Pool_New, New_End, P, S) = Pool_Has (Pool_Old, Old_End, P, S).
--
-- This bridges Pool_Find_Or_Insert's frame postcondition to the inner
-- loop's first-iteration check, where the solver needs to carry
-- Pool_Has through a pool mutation for already-assigned CPs.
---------------------------------------------------------------------------
procedure Lemma_Pool_Has_Frame
(Pool_Old : Scx_Pool_Array;
Pool_New : Scx_Pool_Array;
Old_End : Natural;
New_End : Natural;
P : Scx_Pool_Id;
S : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
Pre => Old_End in 0 .. Max_Unique_Scx
and then New_End in Old_End .. Max_Unique_Scx
and then P in 0 .. Old_End
and then (for all Q in 1 .. Old_End =>
Pool_New (Q) = Pool_Old (Q)),
Post => Pool_Has (Pool_New, New_End, P, S)
= Pool_Has (Pool_Old, Old_End, P, S);
procedure Lemma_Pool_Has_Frame
(Pool_Old : Scx_Pool_Array;
Pool_New : Scx_Pool_Array;
Old_End : Natural;
New_End : Natural;
P : Scx_Pool_Id;
S : UCD_Parser.Property_Index)
is
begin
null;
-- Pool_Has postcondition expands to:
-- result = (P >= 1 and P <= End and P <= Max and Set_Has(Pool(P), S))
-- Since Pool_New(P) = Pool_Old(P) (from frame, P <= Old_End),
-- and P <= Old_End <= New_End, the result is identical.
end Lemma_Pool_Has_Frame;
---------------------------------------------------------------------------
-- Ghost lemma: universally quantified Pool_Has frame.
--
-- Carries the entire Part A invariant through a pool mutation:
-- for all CPs where Table(CP) in 1..Old_End, and for all S in 1..N,
-- Pool_Has(New, New_End, Table(CP), S) = Pool_Has(Old, Old_End, Table(CP), S).
--
-- The body loops over all (CP, S) pairs calling Lemma_Pool_Has_Frame.
---------------------------------------------------------------------------
procedure Lemma_Pool_Has_Frame_All
(Pool_Old : Scx_Pool_Array;
Pool_New : Scx_Pool_Array;
Old_End : Natural;
New_End : Natural;
Table : Scx_Table_Array;
N : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
Pre => Old_End in 0 .. Max_Unique_Scx
and then New_End in Old_End .. Max_Unique_Scx
and then (for all CP in Codepoint =>
Table (CP) in 0 .. Old_End)
and then (for all Q in 1 .. Old_End =>
Pool_New (Q) = Pool_Old (Q))
and then N in 1 .. UCD_Parser.Max_Value_Names,
Post => (for all CP in Codepoint =>
(if Table (CP) /= 0 then
(for all S in UCD_Parser.Property_Index
range 1 .. N =>
Pool_Has (Pool_New, New_End, Table (CP), S)
= Pool_Has (Pool_Old, Old_End, Table (CP), S))));
procedure Lemma_Pool_Has_Frame_All
(Pool_Old : Scx_Pool_Array;
Pool_New : Scx_Pool_Array;
Old_End : Natural;
New_End : Natural;
Table : Scx_Table_Array;
N : UCD_Parser.Property_Index)
is
begin
for CP in Codepoint loop
if Table (CP) /= 0 then
for S in UCD_Parser.Property_Index range 1 .. N loop
Lemma_Pool_Has_Frame
(Pool_Old, Pool_New, Old_End, New_End, Table (CP), S);
pragma Loop_Invariant
(for all SS in UCD_Parser.Property_Index range 1 .. S =>
Pool_Has (Pool_New, New_End, Table (CP), SS)
= Pool_Has (Pool_Old, Old_End, Table (CP), SS));
end loop;
end if;
pragma Loop_Invariant
(for all CC in Codepoint range 0 .. CP =>
(if Table (CC) /= 0 then
(for all S in UCD_Parser.Property_Index
range 1 .. N =>
Pool_Has (Pool_New, New_End, Table (CC), S)
= Pool_Has (Pool_Old, Old_End, Table (CC), S))));
end loop;
end Lemma_Pool_Has_Frame_All;
procedure Pool_Find_Or_Insert
(Pool : in out Scx_Pool_Array;
Pool_End : in out Natural;
Cand : Script_Set;
Id : out Scx_Pool_Id;
Full : out Boolean)
with Pre => Pool_End in 0 .. Max_Unique_Scx
and then Cand.Count in 0 .. Max_Scx_Size
and then (for all P in 1 .. Pool_End =>
P in 1 .. Max_Unique_Scx
and then Pool (P).Count in 0 .. Max_Scx_Size),
Post => Pool_End in Pool_End'Old .. Max_Unique_Scx
and then (for all P in 1 .. Pool_End =>
P in 1 .. Max_Unique_Scx
and then Pool (P).Count in 0 .. Max_Scx_Size)
and then (for all P in 1 .. Pool_End'Old =>
Pool (P) = Pool'Old (P))
and then (if not Full then
Id in 1 .. Pool_End
and then Id in 1 .. Max_Unique_Scx
and then Sets_Equal (Pool (Id), Cand))
and then (if Full then Id = 0);
procedure Pool_Find_Or_Insert
(Pool : in out Scx_Pool_Array;
Pool_End : in out Natural;
Cand : Script_Set;
Id : out Scx_Pool_Id;
Full : out Boolean)
is
begin
Full := False;
-- Linear scan for an existing equal set.
for P in 1 .. Pool_End loop
pragma Loop_Invariant (Pool_End = Pool_End'Loop_Entry);
pragma Loop_Invariant
(for all Q in 1 .. Pool_End =>
Pool (Q) = Pool'Loop_Entry (Q));
if Sets_Equal (Pool (P), Cand) then
Id := P;
return;
end if;
end loop;
-- No match — try to append.
if Pool_End = Max_Unique_Scx then
Full := True;
Id := 0;
return;
end if;
Pool_End := Pool_End + 1;
Pool (Pool_End) := Cand;
Id := Pool_End;
end Pool_Find_Or_Insert;
---------------------------------------------------------------------------
-- Layer 6: Ghost lemmas advancing Expected_Scx_Has_From
--
-- These lemmas discharge the forward-unfolding equations needed to
-- carry the two-part loop invariant of Parse_Script_Extensions over
-- a single iteration. Each is a one-step unfolding of the
-- Expected_Scx_Has expression function; the prover discharges them
-- automatically via expression-function auto-unfolding.
---------------------------------------------------------------------------
-- No line at Pos claims any codepoint (either not a data line, or a
-- data line whose [First_CP..Last_CP] range lies entirely outside
-- the Codepoint subtype). In that case, for every CP, S pair the
-- Expected_Scx_Has_From answer from Pos equals the answer from the
-- next line.
procedure Lemma_Advance_No_Cover
(Scx_Src : Byte_Array;
Pos : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
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_Count in 1 .. UCD_Parser.Max_Value_Names
and then
(for all CP in Codepoint =>
not (UCD_Format_Spec.Is_Data_Line (Scx_Src, Pos)
and then UCD_Format_Spec.Line_Covers_CP
(Scx_Src, Pos, CP))),
Post =>
(for all CP in Codepoint =>
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Scx_Spec.Expected_Scx_Has_From
(Scx_Src, Pos, CP, Script_Src, Script_Names, S)
= Scx_Spec.Expected_Scx_Has_From
(Scx_Src,
UCD_Format_Spec.Next_Line_Start (Scx_Src, Pos),
CP, Script_Src, Script_Names, S)));
procedure Lemma_Advance_No_Cover
(Scx_Src : Byte_Array;
Pos : Positive;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
is
pragma Unreferenced (Scx_Src, Pos, Script_Src, Script_Names);
pragma Unreferenced (Script_Count);
begin
null;
end Lemma_Advance_No_Cover;
-- Data line at Pos covers only codepoints in the range [CP1..CP2]
-- (after Max_Codepoint capping). For every CP strictly outside
-- that range, the line does not cover CP, so the Expected_Scx_Has_From
-- answer unfolds to the next line.
procedure Lemma_Frame_Data_Line
(Scx_Src : Byte_Array;
Pos : Positive;
CP1 : Codepoint;
CP2 : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
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_Count in 1 .. UCD_Parser.Max_Value_Names
and then UCD_Format_Spec.Is_Data_Line (Scx_Src, Pos)
and then
(for all CP in Codepoint =>
(if CP < CP1 or else CP > CP2 then
not UCD_Format_Spec.Line_Covers_CP
(Scx_Src, Pos, CP))),
Post =>
(for all CP in Codepoint =>
(if CP < CP1 or else CP > CP2 then
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Scx_Spec.Expected_Scx_Has_From
(Scx_Src, Pos, CP, Script_Src, Script_Names, S)
= Scx_Spec.Expected_Scx_Has_From
(Scx_Src,
UCD_Format_Spec.Next_Line_Start (Scx_Src, Pos),
CP, Script_Src, Script_Names, S))));
procedure Lemma_Frame_Data_Line
(Scx_Src : Byte_Array;
Pos : Positive;
CP1 : Codepoint;
CP2 : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
is
pragma Unreferenced (Scx_Src, Pos, CP1, CP2, Script_Src);
pragma Unreferenced (Script_Names, Script_Count);
begin
null;
end Lemma_Frame_Data_Line;
-- Data line at Pos covers CP and has a non-empty value field at VS.
-- Then Expected_Scx_Has_From folds to Ghost_Value_Has_Script at VS
-- for every script index S.
procedure Lemma_Covering_Folds
(Scx_Src : Byte_Array;
Pos : Positive;
CP : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
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_Count in 1 .. UCD_Parser.Max_Value_Names
and then UCD_Format_Spec.Is_Data_Line (Scx_Src, Pos)
and then UCD_Format_Spec.Line_Covers_CP (Scx_Src, Pos, CP)
and then UCD_Format_Spec.Value_Start (Scx_Src, Pos) > 0,
Post =>
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Scx_Spec.Expected_Scx_Has_From
(Scx_Src, Pos, CP, Script_Src, Script_Names, S)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src,
UCD_Format_Spec.Value_Start (Scx_Src, Pos),
Script_Src, Script_Names, S));
procedure Lemma_Covering_Folds
(Scx_Src : Byte_Array;
Pos : Positive;
CP : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
is
pragma Unreferenced (Scx_Src, Pos, CP, Script_Src, Script_Names);
pragma Unreferenced (Script_Count);
begin
null;
end Lemma_Covering_Folds;
-- Recursive variant of Lemma_Covering_Folds covering all CPs in
-- CP1 .. CP2. Uses recursion instead of a loop to avoid cut points.
--
-- Precondition: Is_Range_Line and CP1..CP2 within [First_CP..Last_CP].
procedure Lemma_Covering_Folds_Range
(Scx_Src : Byte_Array;
Pos : Positive;
CP1 : Codepoint;
CP2 : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
with Ghost,
Always_Terminates,
Subprogram_Variant => (Decreases => CP2 - CP1),
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_Count in 1 .. UCD_Parser.Max_Value_Names
and then UCD_Format_Spec.Is_Data_Line (Scx_Src, Pos)
and then UCD_Format_Spec.Value_Start (Scx_Src, Pos) > 0
and then CP1 <= CP2
and then UCD_Format_Spec.Is_Range_Line (Scx_Src, Pos)
and then UCD_Format_Spec.Line_First_CP (Scx_Src, Pos)
<= Natural (CP1)
and then Natural (CP2)
<= UCD_Format_Spec.Line_Last_CP (Scx_Src, Pos),
Post =>
(for all C in Codepoint range CP1 .. CP2 =>
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Scx_Spec.Expected_Scx_Has_From
(Scx_Src, Pos, C, Script_Src, Script_Names, S)
= Scx_Spec.Ghost_Value_Has_Script
(Scx_Src,
UCD_Format_Spec.Value_Start (Scx_Src, Pos),
Script_Src, Script_Names, S)));
procedure Lemma_Covering_Folds_Range
(Scx_Src : Byte_Array;
Pos : Positive;
CP1 : Codepoint;
CP2 : Codepoint;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index)
is
begin
-- CP2 is in [First_CP..Last_CP] and Is_Range_Line holds,
-- so Line_Covers_CP holds for CP2.
Lemma_Covering_Folds
(Scx_Src, Pos, CP2, Script_Src, Script_Names, Script_Count);
if CP1 < CP2 then
Lemma_Covering_Folds_Range
(Scx_Src, Pos, CP1, CP2 - 1,
Script_Src, Script_Names, Script_Count);
end if;
end Lemma_Covering_Folds_Range;
-- (Handle_Data_Line_CPs removed: inlined at the call site to avoid
-- expression-function auto-inlining issues at procedure boundaries.
-- The per-CP loop now lives directly inside Parse_Script_Extensions.)
---------------------------------------------------------------------------
-- Layer 7: Parse_Script_Extensions
--
-- Outer loop walks the source line by line, invoking the proven
-- UCD_Parser line-scanning helpers to establish Is_Data_Line and
-- locate the value field. For each covered codepoint the parser
-- applies first-match-wins semantics: only lines whose Table entry
-- is still 0 are updated.
--
-- The two-part loop invariant tracks:
-- Part A: for every already-assigned CP (Table(CP) /= 0), the
-- parsed Pool_Has answer matches Expected_Scx_Has_From from
-- position 1.
-- Part B: for every still-unassigned CP (Table(CP) = 0), the
-- Expected_Scx_Has_From answer from 1 equals the answer
-- from the current Line_Pos — i.e., no earlier line has
-- claimed CP.
---------------------------------------------------------------------------
procedure Parse_Script_Extensions
(Scx_Src : Byte_Array;
Script_Src : Byte_Array;
Script_Names : UCD_Parser.Value_Name_Array;
Script_Count : UCD_Parser.Property_Index;
Pool : out Scx_Pool_Array;
Pool_End : out Natural;
Table : out Scx_Table_Array;
Success : out Boolean)
is
Line_Pos : Positive := 1;
begin
Pool := [others => (Count => 0, Items => [others => 0])];
Pool_End := 0;
Table := [others => 0];
Success := True;
while Line_Pos <= Scx_Src'Last loop
pragma Loop_Invariant (Line_Pos in 1 .. Scx_Src'Last);
pragma Loop_Invariant (Pool_End in 0 .. Max_Unique_Scx);
pragma Loop_Invariant
(for all CP in Codepoint => Table (CP) in 0 .. Pool_End);
pragma Loop_Invariant
(for all P in 1 .. Pool_End =>
(P in 1 .. Max_Unique_Scx
and then Pool (P).Count in 0 .. Max_Scx_Size));
-- Part A: every assigned CP already holds the final answer
pragma Loop_Invariant
(if Success then
(for all CP in Codepoint =>
(if Table (CP) /= 0 then
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Pool_Has (Pool, Pool_End, Table (CP), S)
= Scx_Spec.Expected_Scx_Has_From
(Scx_Src, 1, CP,
Script_Src, Script_Names, S)))));
-- Part B: every unassigned CP still has its "from 1" answer
-- equal to its "from Line_Pos" answer.
pragma Loop_Invariant
(if Success then
(for all CP in Codepoint =>
(if Table (CP) = 0 then
(for all S in UCD_Parser.Property_Index
range 1 .. Script_Count =>
Scx_Spec.Expected_Scx_Has_From
(Scx_Src, 1, CP,
Script_Src, Script_Names, S)
= Scx_Spec.Expected_Scx_Has_From
(Scx_Src, Line_Pos, CP,
Script_Src, Script_Names, S)))));
pragma Loop_Variant (Decreases => Scx_Src'Last - Line_Pos);
declare
F0 : constant Natural := UCD_Parser.Skip_WS (Scx_Src, Line_Pos);
NL : constant Positive :=
UCD_Parser.Next_Line (Scx_Src, Line_Pos);
Semi : Natural;
begin
-- Non-data case 1: no non-space before line-end, or first
-- non-space is not a hex digit → Is_Data_Line is False.
if F0 = 0 or else not Is_Hex_Digit (Scx_Src (F0)) then
pragma Assert
(not UCD_Format_Spec.Is_Data_Line (Scx_Src, Line_Pos));
Lemma_Advance_No_Cover
(Scx_Src, Line_Pos, Script_Src, Script_Names, Script_Count);
Line_Pos := NL;
else
Semi := UCD_Parser.Find_Semi (Scx_Src, Line_Pos);
if Semi = 0 then
-- Non-data case 2: no semicolon.
pragma Assert
(not UCD_Format_Spec.Is_Data_Line (Scx_Src, Line_Pos));
Lemma_Advance_No_Cover
(Scx_Src, Line_Pos, Script_Src, Script_Names,
Script_Count);
Line_Pos := NL;
else
declare
CP1_N : Natural;
Hex_Len : Natural;
begin
UCD_Parser.Parse_CP (Scx_Src, F0, CP1_N, Hex_Len);
if Hex_Len < 4
or else (F0 + Hex_Len <= Scx_Src'Last
and then Is_Hex_Digit
(Scx_Src (F0 + Hex_Len)))
then
-- Non-data case 3: HDC < 4 or HDC > 6
-- → Is_Data_Line False.
if Hex_Len = 0 then
null; -- already not Is_Hex_Digit (impossible branch)
elsif Hex_Len <= 3 then
UCD_Parser.Lemma_Hex_Digit_Count
(Scx_Src, F0, Hex_Len);
else
-- Hex_Len = 4, 5, or 6 with a hex digit
-- immediately after.
if Hex_Len = 6 then
pragma Assert
(F0 + Hex_Len <= Scx_Src'Last);
pragma Assert
(Is_Hex_Digit (Scx_Src (F0 + Hex_Len)));
UCD_Parser.Lemma_HDC_GT_6 (Scx_Src, F0);
else
-- Hex_Len = 4 or 5: Lemma_Hex_Digit_Count
-- requires "no hex digit after", but we have
-- one — so we use it for the OPPOSITE
-- conclusion by contradiction. Simpler:
-- show HDC > Hex_Len via direct unfolding,
-- then HDC >= Hex_Len + 1 means HDC > 6
-- only if Hex_Len = 6. For Hex_Len < 6
-- with trailing hex, HDC might be 5 or 6
-- (still in 4..6) — which WOULD make this
-- a valid data line! So this case should
-- actually not mark as non-data.
--
-- Re-examine: if Hex_Len = 4 and there's a
-- hex digit at F0+4, then Parse_CP returned
-- early — but Parse_CP reads up to 6 digits.
-- So Hex_Len = 4 with hex at F0+4 should not
-- happen: Parse_CP would have continued to
-- Hex_Len = 5. Similarly Hex_Len = 5 with
-- hex at F0+5 would be Hex_Len = 6.
-- Therefore Hex_Len in {4,5} with trailing
-- hex is impossible by Parse_CP's post.
pragma Assert (False);
end if;
end if;
pragma Assert
(not UCD_Format_Spec.Is_Data_Line
(Scx_Src, Line_Pos));
Lemma_Advance_No_Cover
(Scx_Src, Line_Pos, Script_Src, Script_Names,
Script_Count);
Line_Pos := NL;
else
-- Hex_Len in 4..6 and no trailing hex.
-- Establish Is_Data_Line via Lemma_Hex_Digit_Count.
UCD_Parser.Lemma_Hex_Digit_Count
(Scx_Src, F0, Hex_Len);
pragma Assert
(UCD_Format_Spec.Is_Data_Line (Scx_Src, Line_Pos));
if CP1_N > Max_Codepoint then
-- Line_First_CP > Max_Codepoint, so
-- Line_Covers_CP is False for every Codepoint.
pragma Assert
(CP1_N = UCD_Format_Spec.Line_First_CP
(Scx_Src, Line_Pos));
Lemma_Advance_No_Cover
(Scx_Src, Line_Pos, Script_Src, Script_Names,
Script_Count);
Line_Pos := NL;
else
-- CP1_N in 0 .. Max_Codepoint.
-- Determine whether this is a range line and
-- compute CP2_N (defaults to CP1_N for single).
declare
CP2_N : Natural := CP1_N;
Hex_Len2 : Natural;
Last_N : Natural;
CP1 : constant Codepoint :=
Codepoint (CP1_N);
CP2 : Codepoint;
VS_Run : Natural;
Line_Set : Script_Set;
Id : Scx_Pool_Id;
Full : Boolean;
begin
if Scx_Src'Last - F0 >= Hex_Len + 2
and then Scx_Src (F0 + Hex_Len) = Dot_Byte
and then Scx_Src (F0 + Hex_Len + 1)
= Dot_Byte
and then Is_Hex_Digit
(Scx_Src (F0 + Hex_Len + 2))
then
UCD_Parser.Parse_CP
(Scx_Src, F0 + Hex_Len + 2,
CP2_N, Hex_Len2);
if Hex_Len2 in 4 .. 6
and then
(Scx_Src'Last - F0 < Hex_Len + 2 + Hex_Len2
or else not Is_Hex_Digit
(Scx_Src
(F0 + Hex_Len + 2
+ Hex_Len2)))
then
UCD_Parser.Lemma_Hex_Digit_Count
(Scx_Src, F0 + Hex_Len + 2, Hex_Len2);
else
CP2_N := CP1_N;
end if;
end if;
-- Clamp the last CP to Max_Codepoint.
if CP2_N < CP1_N then
-- Ill-formed (shouldn't happen for a
-- valid UCD file); treat as non-covering.
Success := False;
Line_Pos := NL;
else
if CP2_N > Max_Codepoint then
Last_N := Max_Codepoint;
else
Last_N := CP2_N;
end if;
CP2 := Codepoint (Last_N);
-- Compute Value_Start matching the ghost
-- definition exactly.
if Semi >= Scx_Src'Last then
VS_Run := 0;
else
VS_Run :=
UCD_Parser.Skip_WS
(Scx_Src, Semi + 1);
end if;
if VS_Run = 0 then
-- Empty value field — the line asserts
-- no scripts for the covered CPs. The
-- "empty set" interning path is
-- handled by Build_Line_Set returning
-- Count = 0, but we still need
-- VS in Scx_Src'Range to call it.
-- Mark Success := False for this rare
-- case; the UCD file never exercises
-- it in practice.
Success := False;
Line_Pos := NL;
else
Build_Line_Set
(Scx_Src, VS_Run, Script_Src,
Script_Names, Script_Count,
Line_Set);
declare
Pool_Snap : constant Scx_Pool_Array
:= Pool with Ghost;
PE_Snap : constant Natural
:= Pool_End with Ghost;
begin
Pool_Find_Or_Insert
(Pool, Pool_End, Line_Set, Id, Full);
if Full then
Success := False;
Line_Pos := NL;
elsif not Success then
-- Prior iteration failed: Part A/B
-- are vacuously true, skip proving.
Line_Pos := NL;
else
-- Carry outer Part A through
-- the Pool_Find_Or_Insert
-- mutation. Pool_Has is opaque,
-- so the solver needs an explicit
-- frame lemma to re-establish
-- Pool_Has for all already-
-- assigned CPs.
Lemma_Pool_Has_Frame_All
(Pool_Snap, Pool, PE_Snap,
Pool_End, Table, Script_Count);
-- Build "Covering folded"
-- precondition fact:
-- Pool_Has(Id, S) =
-- Expected_Scx_Has_From(
-- Line_Pos, C, S)
-- for all C in CP1..CP2, all S.
--
-- (a) VS_Run = Value_Start
pragma Assert
(VS_Run = UCD_Format_Spec.Value_Start
(Scx_Src, Line_Pos));
-- (b) Sets_Equal → Set_Has equality
Lemma_Sets_Equal_Set_Has_All
(Pool (Id), Line_Set,
Script_Count);
-- (c) Covering_Folds:
-- Establish Line_Covers_CP
-- structurally from computed CPs.
pragma Assert
(Natural (CP1)
= UCD_Format_Spec.Line_First_CP
(Scx_Src, Line_Pos));
pragma Assert
(if UCD_Format_Spec.Is_Range_Line
(Scx_Src, Line_Pos)
then UCD_Format_Spec.Line_First_CP
(Scx_Src, Line_Pos)
<= UCD_Format_Spec.Line_Last_CP
(Scx_Src, Line_Pos));
if CP1 = CP2 then
Lemma_Covering_Folds
(Scx_Src, Line_Pos, CP1,
Script_Src, Script_Names,
Script_Count);
else
-- Range line: CP1 < CP2.
-- Reinstantiate Covering_Folds
-- for all CPs by recursion.
pragma Assert
(Natural (CP2)
<= UCD_Format_Spec.Line_Last_CP
(Scx_Src, Line_Pos));
Lemma_Covering_Folds_Range
(Scx_Src, Line_Pos, CP1, CP2,
Script_Src, Script_Names,
Script_Count);
end if;
-- Bridge: combine Sets_Equal
-- + Build_Line_Set to get
-- Pool_Has(Id, S) = GVHS(VS, S),
-- which chains with Covering_Folds
-- to give the "Covering folded"
-- precondition.
pragma Assert
(for all C in
Codepoint range CP1 .. CP2 =>
(for all S in
UCD_Parser.Property_Index
range 1 .. Script_Count =>
Pool_Has
(Pool, Pool_End, Id, S)
= Scx_Spec.Expected_Scx_Has_From
(Scx_Src, Line_Pos, C,
Script_Src,
Script_Names, S)));
-- Re-assert outer Part A with
-- current Pool/Pool_End.
-- Pool_Find_Or_Insert preserves
-- existing entries, so Pool_Has
-- values for already-assigned CPs
-- are unchanged.
pragma Assert
(if Success then
(for all CP in Codepoint =>
(if Table (CP) /= 0 then
(for all S in
UCD_Parser.Property_Index
range 1 ..
Script_Count =>
Pool_Has
(Pool, Pool_End,
Table (CP), S)
= Scx_Spec
.Expected_Scx_Has_From
(Scx_Src, 1, CP,
Script_Src,
Script_Names,
S)))));
-- Per-CP assignment loop (inlined
-- from Handle_Data_Line_CPs to keep
-- the bridging assertion locally
-- available without crossing a
-- procedure boundary).
for C in Codepoint range CP1 .. CP2 loop
pragma Loop_Invariant
(for all CP in Codepoint =>
Table (CP) in 0 .. Pool_End);
pragma Loop_Invariant
(for all P in 1 .. Pool_End =>
(P in 1 .. Max_Unique_Scx
and then
Pool (P).Count
in 0 .. Max_Scx_Size));
pragma Loop_Invariant
(for all Prev in
Codepoint range CP1 .. C - 1 =>
Table (Prev) /= 0);
-- Part A (inner): assigned CPs
-- hold final answer.
pragma Loop_Invariant
(if Success then
(for all CP in Codepoint =>
(if Table (CP) /= 0 then
(for all S in
UCD_Parser.Property_Index
range 1 ..
Script_Count =>
Pool_Has
(Pool, Pool_End,
Table (CP), S)
= Scx_Spec
.Expected_Scx_Has_From
(Scx_Src, 1, CP,
Script_Src,
Script_Names,
S)))));
-- Part B (inner): unassigned CPs
-- have from-1 = from-Line_Pos.
pragma Loop_Invariant
(if Success then
(for all CP in Codepoint =>
(if Table (CP) = 0 then
(for all S in
UCD_Parser.Property_Index
range 1 ..
Script_Count =>
Scx_Spec
.Expected_Scx_Has_From
(Scx_Src, 1, CP,
Script_Src,
Script_Names, S)
= Scx_Spec
.Expected_Scx_Has_From
(Scx_Src,
Line_Pos, CP,
Script_Src,
Script_Names,
S)))));
if Table (C) = 0 then
Table (C) := Id;
end if;
end loop;
-- Advance Part B from
-- Line_Pos to NL for CPs
-- outside [CP1..CP2].
-- The inner loop above
-- guarantees all CPs in
-- CP1..CP2 are assigned,
-- so only outside-range
-- CPs have Table(CP) = 0.
Lemma_Frame_Data_Line
(Scx_Src, Line_Pos,
CP1, CP2, Script_Src,
Script_Names,
Script_Count);
Line_Pos := NL;
end if;
end; -- declare Pool_Snap
end if;
end if;
end;
end if;
end if;
end;
end if;
end if;
end;
end loop;
end Parse_Script_Extensions;
end Lingenic_Text.Scx_Parser;