Changelog

[1.2.0] - 2026-07-15

Added

• Proved BidiBrackets parser (bidi_brackets_spec.ads/.adb, bidi_brackets_parser.ads/.adb). The BidiBrackets.txt parser is now a fully verified SPARK module with a Platinum postcondition: for every codepoint, each output table entry matches a recursive ghost specification encoding the BidiBrackets.txt file format. This eliminates the last unproved data parser in the codebase.
• Ghost specification for BidiBrackets.txt (bidi_brackets_spec.ads/.adb). Six-layer expression function hierarchy encoding field scanning, line predicates, and expected-output recursion, with opaque wrapper functions preventing cascading auto-inlining in loop invariant VCs.
• Surjectivity proof for Reorder (bidi.adb). The Reorder procedure's postcondition now fully proves that the output ordering is a permutation (surjectivity: every value in 1..Num_CPs appears in the Order array). A nested ghost procedure Prove_Surjective provides explicit existential witnesses via a loop invariant, resolving the VC that SMT solvers could not discharge automatically.
• Ghost sos/eos specification (bidi_spec.ads, bidi.adb). Ghost_Sos and Ghost_Eos expression functions encode the X10 rule for start-of-sequence and end-of-sequence direction computation, including the unmatched isolate initiator exception. Supporting ghost functions Ghost_Effective_Level (backward walk for preceding level) and Ghost_Next_Non_X9_Level (forward scan for following level) encode the X9-aware level lookup rules. Two ghost lemma procedures (Lemma_Effective_Level_Matches, Lemma_Next_Non_X9_Level_Matches) prove by structural recursion that the runtime functions match the ghost specification. The X10 sos/eos computation is now proved, not assumed.
• Embed_Levels linking postcondition (bidi.adb). Extracted the Embed_Levels(I) := Work_Levels(I) copy into a named procedure Copy_Embed_Levels with a postcondition proving Embed_Levels(I) = Work_Levels(I) for all I. The phase composition from Resolve_Explicit_Levels → copy → Process_Run_Sequences is now contract-verified.
• Lower_O_Byte and Lower_C_Byte byte constants in the root package (lingenic_text.ads).

Changed

• Bidi.Initialize refactored (bidi.adb). Replaced the 160-line SPARK_Mode => Off hand-rolled BidiBrackets.txt parser with a 15-line call to the proved Bidi_Brackets_Parser.Parse_Brackets_File. The bracket table types are now subtypes of the parser's types, eliminating a copy step.
• Vacuous guards removed from bidi postconditions (bidi.adb). Postconditions of Apply_W1, Apply_W2, Apply_W4, Apply_W5, Apply_W6, Apply_W7, Apply_N1_N2, and Apply_I1_I2 contained guards (if Seq(S) >= 1 and then Seq(S) <= Max_Paragraph_CPs then ...) that were always true under the Seq_Unique precondition, making the consequents trivially satisfiable. Guards removed; postconditions are now unconditional and strictly stronger. Corresponding vacuous guards in Apply_N0 runtime code replaced with pragma Assert or removed.
• Effective_Level rewritten as recursive expression function (bidi.adb). The original iterative reverse-loop body was opaque to the solver. As a recursive expression function mirroring Ghost_Effective_Level, the solver can unfold both in lockstep for proof. Next_Non_X9_Level similarly extracted as a recursive expression function replacing the inline forward scan loop.

Verification

• 9,640 verification conditions discharged at Level 4 (up from 9,214 in v1.1.0).
• Zero pragma Assume. Zero Annotate(GNATprove, ...).
• 504,634 conformance test cases passed (unchanged).
• 91,707/91,707 BidiCharacterTest.txt cases passed.

[1.1.0] - 2026-07-08

Initial public release. 14 algorithm modules, 53 source files, ~30,500 lines. 9,214 verification conditions proved at Level 4. 504,634 conformance test cases passed.