FORMAL VERIFICATION
===================
This document describes the formal verification approach, proof patterns,
and ghost code architecture used throughout Lingenic-Text.
VERIFICATION TOOL
-----------------
GNATprove is the SPARK formal verification tool. It uses the Why3
intermediate verification framework and calls SMT solvers (CVC5, Z3,
Alt-Ergo) to discharge verification conditions.
Settings (from lingenic_text.gpr):
--level=4 Highest proof effort
--timeout=60 60-second timeout per verification condition
--steps=0 No step limit (timeout governs)
--counterexamples=on Show counterexamples for failed proofs
--proof=progressive Progressive proof strategy (try simple first,
escalate to full effort only for hard VCs)
Command:
gnatprove -P lingenic_text.gpr -XMODE=prove -j0
WHAT IS PROVED
--------------
Every subprogram in the library carries contracts. GNATprove proves:
1. ABSENCE OF RUNTIME ERRORS
- Array index out of bounds: every index is proved in range
- Arithmetic overflow: every operation is proved within bounds
- Division by zero: every divisor is proved nonzero
- Range check failure: every assignment is proved within type range
2. FUNCTIONAL CORRECTNESS
- Postconditions: the output of every subprogram matches its
specification. For segmentation modules, this means the byte
position returned equals the recursive ghost function. For
transforms, this means the output satisfies the ghost predicate.
- Loop invariants: every loop maintains its stated invariants.
- Subprogram variants: every recursive function terminates.
3. GLOBAL DATA CONTRACTS
- Global annotations: every subprogram declares which global state
it reads and writes.
- Depends annotations: output dependencies are declared and verified.
4. PRECONDITION VERIFICATION
- Every call site is proved to satisfy the callee's preconditions.
- Every Initialize procedure's postcondition establishes the
Initialized predicate, which is a precondition on all accessors.
NO PRAGMA ASSUME
----------------
Lingenic-Text uses no pragma Assume anywhere. Every verification
condition is discharged by the prover. There are no hand-waved
obligations, no "structural limitations" excuses, no suppressions.
If a VC does not discharge, the code does not build. The proof is
the product.
GHOST CODE
----------
Ghost code is erased completely at compile time -- zero runtime cost,
zero code size impact. Lingenic-Text uses ghost code extensively:
Ghost Packages:
Packages with the Ghost aspect or all-ghost contents are erased.
Examples: UTF8_Spec, UCD_Format_Spec, Graphemes_Spec, Words_Spec,
Sentences_Spec, Line_Break_Spec, Normalization_Spec, Case_Mapping_Spec,
Collation_Spec, Bidi_Spec, Bidi_Brackets_Spec, EAW_Spec, Emoji_Spec,
IDNA_Spec, Properties_Spec.
Ghost Expression Functions:
Expression functions with Ghost aspect are unfolded by the solver
directly into proof contexts. The solver sees the function body,
not a call -- this is why expression functions are preferred for
proof over regular functions.
Examples: Is_Grapheme_Break, Well_Formed_At, Decoded_At, Ghost_CP,
Ghost_GBP, Ghost_Break, Updated_State, Initial_State, Cell_Width.
Ghost Recursive Functions:
Recursive ghost functions specify complete algorithms. They have
Subprogram_Variant annotations proving termination. The solver
can unfold one recursive step to match the loop body.
Examples: Next_GCB, Next_WB, Next_SB, Next_LB, Ghost_Scan,
Ghost_Upper_Out, Ghost_Lower_Out, Ghost_Title_Scan, Ghost_Is_NFD_From,
Ghost_Is_NFC_From, Ghost_Norm_Out, Expected_Value.
Ghost Predicates:
Used as loop invariants and preconditions.
Examples: Partial_Valid (in Text_Transform generic), Ghost_Is_NFD,
Ghost_Is_NFC, Data_All_Terminal.
Ghost Lemmas:
Procedural proofs that establish relationships between different
ghost specifications. The body is typically null (the property
follows by structural identity of the expression function bodies).
Examples: Lemma_NFC_Matches_UTF8_Spec (anchors duplicated UTF-8
helpers to UTF8_Spec), Lemma_Hex_Digit_Count (links runtime
Parse_CP to ghost Hex_Digit_Count), Lemma_Invariant_Step_Open
(one-step advance of BidiBrackets parser invariant),
Prove_Surjective (existential witness instantiation for Reorder
permutation proof), Lemma_Effective_Level_Matches and
Lemma_Next_Non_X9_Level_Matches (bridge runtime recursive
functions to ghost specification functions by structural
induction).
PROOF PATTERNS
--------------
Pattern 1: Recursive Ghost Function vs Forward Loop
Used by: Graphemes, Words, Sentences, Line_Break, Emoji
The algorithm is specified as a recursive ghost function:
function Next_GCB(Text, Cur, St) return Positive is
(if Cur not in Text'Range then ...
elsif Ghost_Break(St, Text, Cur) then Cur
else Next_GCB(Text, Cur + Step, Updated_State(St, Text, Cur)))
with Subprogram_Variant => (Decreases => Text'Last - Cur + 1);
The implementation is a forward loop:
Cur := Pos + Step;
while Cur <= Text'Last loop
if break_condition then exit;
State := update(State);
Cur := Cur + Step;
end loop;
Loop invariant: "if the ghost function were called with the current
state and position, it would return the same result as the full
recursive computation starting from Pos."
The prover matches one loop iteration to one recursive unfolding step.
Pattern 2: Ghost Predicate Maintained by Generic Callback
Used by: Normalization, Case_Mapping (via Text_Transform)
The generic Text_Transform carries Partial_Valid as its loop invariant.
On_Codepoint's postcondition preserves Partial_Valid.
On_Finish's postcondition bridges from Partial_Valid to Output_Valid.
The generic's postcondition asserts Output_Valid on success.
This separates the "scan and decode" proof (in the generic) from the
"this transform is correct" proof (in On_Codepoint/On_Finish).
Pattern 3: Recursive Ghost for Output Byte Count
Used by: Case_Mapping (Ghost_Upper_Out, Ghost_Lower_Out, etc.)
The postcondition proves the exact output byte count:
Last - Output'First + 1 = Ghost_Upper_Total(Input)
Ghost_Upper_Total is a recursive function summing Ghost_Upper_Out_Bytes
for each input codepoint. The loop invariant tracks the accumulated
byte count and proves it matches the partial sum.
Pattern 4: Recursive Ghost Predicate for Output Structure
Used by: Normalization (Ghost_Is_NFD_From, Ghost_Is_NFC_From)
The postcondition asserts a structural property of the output:
Ghost_Is_NFD(Output, Output'First, Last)
This recursive predicate walks the output checking well-formedness,
full decomposition, and CCC ordering at every position. The loop
invariant maintains Ghost_Is_NFD_From for the output written so far.
Pattern 5: Flat Array Correctness
Used by: UCD_Parser
The parser's postcondition proves:
for all CP => Table(CP) = Expected_Value(Source, 1, CP, Names, Num)
Expected_Value is a recursive ghost function that processes the file
line by line, applying last-writer-wins semantics. The loop invariant
states: "for all CP, Table(CP) equals what Expected_Value would return
if we started scanning from the current line position."
Pattern 6: Opaque Wrapper Functions
Used by: Bidi_Brackets_Parser (via Bidi_Brackets_Spec)
Recursive ghost expression functions auto-unfold in proof contexts.
When referenced in loop invariants, this can cause cascading
expansion and solver timeout.
Solution: declare non-expression-function wrappers (in a .adb body)
with postconditions equating to the expression function. The solver
treats the wrapper as opaque and uses only the postcondition, without
unfolding the recursive body.
function Expected_Open_From(S, Pos, CP) return Natural
with Post => Result = (if Pos > S'Last then 0
else Expected_Open_Mapping(S, Pos, CP));
Loop invariants reference the opaque wrapper; lemma procedures
unfold one level when needed.
Pattern 7: Existential Witness via Ghost Procedure
Used by: Bidi.Reorder (Prove_Surjective)
SMT solvers cannot automatically instantiate existential quantifiers
when the witness involves array indexing. Given Order(Inv(V)) = V
with Inv(V) in range, the solver cannot infer that Inv(V) is a
valid witness for "for some I => Order(I) = V".
Solution: a nested ghost procedure with a loop that instantiates the
witness one value at a time:
procedure Prove_Surjective with Ghost,
Pre => Is_Perm,
Post => (for all V in 1..N => (for some I in 1..N => Order(I) = V));
procedure Prove_Surjective is
begin
for V in 1 .. N loop
pragma Assert (Order (Inv (V)) = V);
pragma Loop_Invariant
(for all W in 1 .. V =>
(for some I in 1 .. N => Order (I) = W));
end loop;
end Prove_Surjective;
Each iteration is single-step reasoning. The loop invariant
accumulates the proved existentials. The procedure is Ghost --
zero runtime cost.
Pattern 8: Recursive Lemma for Runtime/Ghost Array Bridging
Used by: Bidi (sos/eos proof)
When a runtime function reads from runtime arrays (Orig_Types,
Embed_Levels) and a ghost specification function reads from ghost
arrays (Ghost_BC_Array, Ghost_Level_Array), the solver cannot
connect them even if the ghost arrays are element-wise equal.
The gap has two components: (a) the solver must instantiate the
element-wise equality at the specific index, and (b) the recursive
functions must be unfolded to arbitrary depth.
Solution: write a recursive ghost lemma procedure that mirrors
the structure of both functions. The lemma takes the ghost arrays
as parameters with a precondition asserting element-wise equality,
and proves the runtime function equals the ghost function:
procedure Lemma_Effective_Level_Matches
(Idx : Para_Index; OT_G : Ghost_BC_Array; EL_G : Ghost_Level_Array)
with Ghost,
Pre => (for all I => OT_G(I) = Orig_Types(I))
and then (for all I => EL_G(I) = Embed_Levels(I)),
Post => Effective_Level(Idx) =
Ghost_Effective_Level(OT_G, EL_G, Idx, PL),
Subprogram_Variant => (Decreases => Idx);
procedure Lemma_Effective_Level_Matches (...) is
begin
pragma Assert (OT_G(Idx) = Orig_Types(Idx));
pragma Assert (EL_G(Idx) = Embed_Levels(Idx));
if not Is_X9_Removed(Orig_Types(Idx)) then null;
elsif Idx = 1 then null;
else Lemma_Effective_Level_Matches(Idx - 1, OT_G, EL_G);
end if;
end;
Each recursive step: the pragma Assert instantiates the universal
quantifier at the current index; one-step unfolding of both
expression functions produces identical results; the recursive
call establishes the inductive hypothesis.
The runtime function must also be an expression function (not a
loop-based function) so the solver can unfold it. If the original
runtime function uses a loop, rewrite it as a recursive expression
function mirroring the ghost function. The conversion functions
(To_GBC_Outer, To_Ghost_Levels) are passed directly as procedure
arguments at the call site, avoiding the GNAT 15 limitation on
non-scalar object declarations inside loops with loop invariants.
TERMINATION
-----------
All recursive ghost functions have Subprogram_Variant annotations:
Subprogram_Variant => (Decreases => Text'Last - Cur + 1)
This proves termination because Ghost_Step_Length >= 1, so Cur strictly
increases on each recursive call, and Text'Last is fixed.
All procedures with loops have Always_Terminates annotations where
required by the SPARK standard.
COMPILER CONFIGURATION
----------------------
Build mode (build.adc):
pragma SPARK_Mode (On);
pragma Assertion_Policy (Ignore);
Assertions are not checked at runtime because the prover has already
verified them. This is safe because the proofs are total: they cover
all inputs, not just tested ones.
Runtime checks are also suppressed (-gnatp) because GNATprove has
proved the absence of all runtime errors.
Prove mode (gnatprove.adc):
pragma SPARK_Mode (On);
pragma Assertion_Policy (Check);
During proving, assertions are active so the prover can see them.
SPARK_MODE BOUNDARY
-------------------
The entire library is SPARK_Mode(On) except:
File_IO.Read_File Reads bytes from disk. The trust boundary.
Initialize bodies Call File_IO, then proved parsers. All data
parsers (UCD_Parser, Scx_Parser,
Bidi_Brackets_Parser) are proved SPARK.
Once bytes are in memory, all processing is machine-checked SPARK.
The Initialize postconditions (Initialized, Data_All_Terminal) bridge
the trust boundary: the non-SPARK code establishes the preconditions
that all downstream SPARK code relies on.
DOUBLE PROOF CHAIN
------------------
Two independent evidence chains establish end-to-end correctness:
Chain 1 (Formal Proof):
Implementation matches ghost specification for ALL inputs.
Evidence: GNATprove discharges every VC at Level 4.
Strength: Universal (covers all inputs, not just test cases).
Limitation: Only as correct as the ghost specification.
Chain 2 (Conformance Tests):
Ghost specification matches the Unicode standard.
Evidence: Official Unicode test suites pass 100%.
Strength: Tests are authored by the Unicode Consortium.
Limitation: Tests are finite (cannot cover all inputs).
Together: Implementation = Specification (by proof),
Specification = Standard (by test).
No gap between the implementation and the standard.