L4YAML

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.

  • Invariant-preservation certificates — a recursion can be structurally complete (every constructor of its output is liftable from the available pieces) and still not be runnable: the proof that each recursive call's input satisfies the recursion's precondition is a distinct obligation from the assembly lemmas, the structural analogue of a loop invariant's inductive step. In the flow-subrange locate recursion this is the ADVANCE-step certificate advanceTail_invariant — given a balanced window and a depth-0 entry separator at index m, the tail [m+1, hi) is itself a balanced window and re-bases onto the moving origin, so the recursive call is well-posed. The certificate is phrased over bracket balance alone (no collection-specific deliverable type), so a single lemma serves both the sequence and mapping recursions.

  • 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.