CHANGELOG⤓ .md 2026-07-15T070725.000 000000000031424 - 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..NumCPs appears in the Order array). A nested ghost procedure `ProveSurjective provides explicit existential witnesses via a loop invariant, resolving the VC that SMT solvers could not discharge automatically. - **Ghost sos/eos specification** (bidispec.ads`, `bidi.adb`). `GhostSos and GhostEos` 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 `GhostEffectiveLevel` (backward walk for preceding level) and `GhostNextNonX9Level` (forward scan for following level) encode the X9-aware level lookup rules. Two ghost lemma procedures (`LemmaEffectiveLevelMatches, LemmaNextNonX9LevelMatches`) prove by structural recursion that the runtime functions match the ghost specification. The X10 sos/eos computation is now proved, not assumed. - **EmbedLevels 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).