3.7. Proof Engineering Patterns🔗

Several patterns emerged during the verification effort:

• Decomposition — large functions are decomposed into validation (error guards), state transformation (pure updates), and emission (token output) phases, each proved independently then composed.

• Append-only invariant — the switch from insertAt to placeholder reservation slots with setIfInBounds backpatching eliminated the hardest class of proof obligations (index shifting).

• Monotonic progress — proving offset_lt (strict increase) for every scanner operation provides termination and guarantees no infinite loops.

• Well-formedness threading — a WellFormed predicate on scanner state is threaded through every operation, establishing that invariants are maintained from scannerInit through scanNextToken to stream completion.

• Anchor monotonicity — the AnchorsGrow relation is proved transitively across all 14 mutually recursive parser functions, establishing that anchors accumulate but are never dropped.

• Fuel-based termination — the parser's 14 mutual functions use fuel : Nat as a decreasing argument. Initial fuel is set to 4 * tokens.size + 4, large enough for any valid input.