-- 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
--
-- BidiBrackets.txt ghost specification.
--
-- Encodes the BidiBrackets.txt file format as expression functions:
--
-- HHHH; HHHH; o/c # comment
--
-- Field 0: codepoint (4-6 uppercase hex digits)
-- Field 1: paired bracket codepoint (4-6 uppercase hex digits)
-- Field 2: bracket type ('o' = open, 'c' = close)
--
-- Lines starting with '#' are comments. Blank lines are skipped.
--
-- Reuses the lower layers of UCD_Format_Spec (hex scanning, line
-- scanning, Is_Data_Line, Line_First_CP) and adds BidiBrackets-specific
-- field extraction and expected-output recursive functions.
--
-- Every function here is Ghost — erased at compile time, zero runtime cost.
-- The parser's postconditions reference these ghost functions to establish
-- that the parsed tables match what the BidiBrackets file specifies.
-------------------------------------------------------------------------------
with Lingenic_Text.UCD_Format_Spec;
package Lingenic_Text.Bidi_Brackets_Spec
with SPARK_Mode, Ghost, Pure
is
use UCD_Format_Spec;
---------------------------------------------------------------------------
-- Layer 1: Field 1 scanning
--
-- Field 1 is the paired bracket codepoint, located after the first
-- semicolon. We find the first semicolon (from UCD_Format_Spec),
-- skip whitespace past it, and expect 4-6 hex digits.
---------------------------------------------------------------------------
-- Position of the first non-space byte after the first semicolon.
-- Returns 0 if the first semicolon is at end of source or if only
-- whitespace follows it before line-end.
function Field1_Start
(Source : Byte_Array;
Line_Start : Positive) return Natural
is (declare
Semi1 : constant Natural :=
Find_Semicolon (Source, Line_Start);
begin
(if Semi1 = 0 or else Semi1 >= Source'Last then 0
else Skip_Spaces (Source, Semi1 + 1)))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range
and then Is_Data_Line (Source, Line_Start),
Post => (if Field1_Start'Result > 0 then
Field1_Start'Result in 1 .. Source'Last);
-- Hex digit count at Field1_Start.
-- Returns 0 when Field1_Start is 0 or when the byte at Field1_Start
-- is not a hex digit.
function Field1_Hex_Count
(Source : Byte_Array;
Line_Start : Positive) return Natural
is (declare
F1 : constant Natural := Field1_Start (Source, Line_Start);
begin
(if F1 = 0 then 0
else Hex_Digit_Count (Source, F1)))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range
and then Is_Data_Line (Source, Line_Start);
---------------------------------------------------------------------------
-- Layer 2: Second semicolon and type field
--
-- After field 1 (the paired codepoint hex), we find the second
-- semicolon, skip whitespace past it, and expect 'o' or 'c'.
---------------------------------------------------------------------------
-- Position of the second semicolon on the line.
-- Searches from Field1_Start + Field1_Hex_Count forward.
-- Returns 0 if field 1 doesn't have valid hex or no second semicolon.
function Find_Second_Semi
(Source : Byte_Array;
Line_Start : Positive) return Natural
is (declare
F1 : constant Natural := Field1_Start (Source, Line_Start);
HC : constant Natural := Field1_Hex_Count (Source, Line_Start);
begin
(if F1 = 0 or else HC = 0
or else Source'Last - F1 < HC
then 0
else Find_Semicolon (Source, F1 + HC)))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range
and then Is_Data_Line (Source, Line_Start);
-- Position of the first non-space byte after the second semicolon
-- (start of the bracket type field).
-- Returns 0 when there is no second semicolon, or when only whitespace
-- follows it before line-end.
function Type_Field_Pos
(Source : Byte_Array;
Line_Start : Positive) return Natural
is (declare
Semi2 : constant Natural := Find_Second_Semi (Source, Line_Start);
begin
(if Semi2 = 0 or else Semi2 >= Source'Last then 0
else Skip_Spaces (Source, Semi2 + 1)))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range
and then Is_Data_Line (Source, Line_Start),
Post => (if Type_Field_Pos'Result > 0 then
Type_Field_Pos'Result in 1 .. Source'Last);
---------------------------------------------------------------------------
-- Layer 3: BidiBrackets data line predicate
--
-- A valid BidiBrackets data line is a standard UCD data line (field 0
-- has 4-6 hex digits + semicolon) that additionally has:
-- - Field 1: 4-6 hex digits for the paired codepoint
-- - A second semicolon after field 1
-- - A type field byte that is 'o' or 'c'
---------------------------------------------------------------------------
function Is_Bracket_Data_Line
(Source : Byte_Array;
Line_Start : Positive) return Boolean
is (Is_Data_Line (Source, Line_Start)
and then Field1_Hex_Count (Source, Line_Start) in 4 .. 6
and then Type_Field_Pos (Source, Line_Start) > 0
and then (Source (Type_Field_Pos (Source, Line_Start)) = Lower_O_Byte
or else
Source (Type_Field_Pos (Source, Line_Start)) = Lower_C_Byte))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range;
---------------------------------------------------------------------------
-- Layer 4: Field extraction from a valid bracket data line
---------------------------------------------------------------------------
-- Parse the paired codepoint from field 1.
function Line_Paired_CP
(Source : Byte_Array;
Line_Start : Positive) return Natural
is (Parse_Hex (Source,
Field1_Start (Source, Line_Start),
Field1_Hex_Count (Source, Line_Start)))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range
and then Is_Bracket_Data_Line (Source, Line_Start);
-- The bracket type byte ('o' or 'c').
function Line_Bracket_Type
(Source : Byte_Array;
Line_Start : Positive) return Byte
is (Source (Type_Field_Pos (Source, Line_Start)))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range
and then Is_Bracket_Data_Line (Source, Line_Start);
-- Is this an open-bracket line?
function Is_Open_Line
(Source : Byte_Array;
Line_Start : Positive) return Boolean
is (Is_Bracket_Data_Line (Source, Line_Start)
and then Line_Bracket_Type (Source, Line_Start) = Lower_O_Byte)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range;
-- Is this a close-bracket line?
function Is_Close_Line
(Source : Byte_Array;
Line_Start : Positive) return Boolean
is (Is_Bracket_Data_Line (Source, Line_Start)
and then Line_Bracket_Type (Source, Line_Start) = Lower_C_Byte)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range;
-- Does the bracket data line at Line_Start cover codepoint CP?
-- BidiBrackets has no ranges — each line covers a single codepoint.
function Bracket_Line_Covers_CP
(Source : Byte_Array;
Line_Start : Positive;
CP : Codepoint) return Boolean
is (Is_Bracket_Data_Line (Source, Line_Start)
and then Line_First_CP (Source, Line_Start) = CP)
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Line_Start in Source'Range;
---------------------------------------------------------------------------
-- Layer 5: Expected output table functions (file-level recursion)
--
-- These define what each output table should contain after processing
-- all lines from position Pos forward. Last-writer-wins semantics
-- (consistent with UCD_Parser), though in practice each codepoint
-- appears at most once in BidiBrackets.txt.
--
-- Expected_Open_Mapping(S, Pos, CP):
-- Scan lines from Pos. If a bracket data line covers CP and is an
-- open-bracket line, the value is Line_Paired_CP. Default is 0.
--
-- Expected_Close_Mapping(S, Pos, CP):
-- Same, for close-bracket lines → Bracket_Close_Table.
--
-- Expected_Is_Open(S, Pos, CP):
-- True if any open-bracket line from Pos forward covers CP.
--
-- Expected_Is_Close(S, Pos, CP):
-- True if any close-bracket line from Pos forward covers CP.
---------------------------------------------------------------------------
function Expected_Open_Mapping
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Natural
is (if Pos > Source'Last then 0
elsif Is_Open_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
and then Line_Paired_CP (Source, Pos) <= Max_Codepoint
then
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
Rest : constant Natural :=
(if NL > Source'Last then 0
else Expected_Open_Mapping (Source, NL, CP));
begin
(if Rest /= 0 then Rest
else Line_Paired_CP (Source, Pos)))
else
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
(if NL > Source'Last then 0
else Expected_Open_Mapping (Source, NL, CP))))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Subprogram_Variant => (Decreases => Source'Last - Pos),
Post => Expected_Open_Mapping'Result <= Max_Codepoint;
function Expected_Close_Mapping
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Natural
is (if Pos > Source'Last then 0
elsif Is_Close_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
and then Line_Paired_CP (Source, Pos) <= Max_Codepoint
then
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
Rest : constant Natural :=
(if NL > Source'Last then 0
else Expected_Close_Mapping (Source, NL, CP));
begin
(if Rest /= 0 then Rest
else Line_Paired_CP (Source, Pos)))
else
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
(if NL > Source'Last then 0
else Expected_Close_Mapping (Source, NL, CP))))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Subprogram_Variant => (Decreases => Source'Last - Pos),
Post => Expected_Close_Mapping'Result <= Max_Codepoint;
function Expected_Is_Open
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
is (if Pos > Source'Last then False
elsif Is_Open_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
then True
else
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
(if NL > Source'Last then False
else Expected_Is_Open (Source, NL, CP))))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Subprogram_Variant => (Decreases => Source'Last - Pos);
function Expected_Is_Close
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
is (if Pos > Source'Last then False
elsif Is_Close_Line (Source, Pos)
and then Line_First_CP (Source, Pos) = CP
then True
else
(declare
NL : constant Positive := Next_Line_Start (Source, Pos);
begin
(if NL > Source'Last then False
else Expected_Is_Close (Source, NL, CP))))
with Pre => Source'First = 1
and then Source'Last < Positive'Last
and then Pos in Source'Range,
Subprogram_Variant => (Decreases => Source'Last - Pos);
---------------------------------------------------------------------------
-- Layer 6: Boundary-safe wrappers (opaque)
--
-- These are deliberately NOT expression functions. The solver treats
-- them as opaque and uses the postcondition only. This prevents
-- cascading recursive expansion in loop invariant VCs.
-- Bodies are in bidi_brackets_spec.adb.
---------------------------------------------------------------------------
function Expected_Open_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Natural
with Pre => Source'First = 1
and then Source'Last < Positive'Last,
Post => Expected_Open_From'Result <= Max_Codepoint
and then Expected_Open_From'Result =
(if Pos > Source'Last then 0
else Expected_Open_Mapping (Source, Pos, CP));
function Expected_Close_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Natural
with Pre => Source'First = 1
and then Source'Last < Positive'Last,
Post => Expected_Close_From'Result <= Max_Codepoint
and then Expected_Close_From'Result =
(if Pos > Source'Last then 0
else Expected_Close_Mapping (Source, Pos, CP));
function Expected_Is_Open_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
with Pre => Source'First = 1
and then Source'Last < Positive'Last,
Post => Expected_Is_Open_From'Result =
(if Pos > Source'Last then False
else Expected_Is_Open (Source, Pos, CP));
function Expected_Is_Close_From
(Source : Byte_Array;
Pos : Positive;
CP : Codepoint) return Boolean
with Pre => Source'First = 1
and then Source'Last < Positive'Last,
Post => Expected_Is_Close_From'Result =
(if Pos > Source'Last then False
else Expected_Is_Close (Source, Pos, CP));
end Lingenic_Text.Bidi_Brackets_Spec;