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, 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).
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."
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.
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.