308 lines
18 KiB
Markdown
308 lines
18 KiB
Markdown
---
|
||
name: invariant-guard
|
||
description: "Correctness-first: forces writing the function contract, loop invariant, termination argument, and edge cases BEFORE code. Catches Boyer-Moore, leftmost binary search, QuickSelect traps."
|
||
risk: safe
|
||
source: community
|
||
source_repo: morsechimwai/lemmaly
|
||
source_type: community
|
||
date_added: "2026-05-26"
|
||
author: morsechimwai
|
||
tags: [algorithms, correctness, loop-invariants, contracts, edge-cases, verification]
|
||
tools: [claude-code, antigravity, cursor, gemini-cli, codex-cli]
|
||
license: "Apache-2.0"
|
||
license_source: "https://github.com/morsechimwai/lemmaly/blob/main/LICENSE"
|
||
---
|
||
|
||
# invariant-guard — Correctness-First Coding
|
||
|
||
The model knows what a loop invariant is. It knows recursion needs a base case. It knows about empty lists, integer overflow, and the difference between `<` and `≤`. It just does not write these down before producing code, so it ships subtle correctness bugs that tests do not catch.
|
||
|
||
invariant-guard fixes the behavior. State the invariants. State the base case. State the termination argument. State the edge cases. Then write the code — and verify that the code maintains what you stated.
|
||
|
||
**Violating the letter of these rules is violating the spirit of the skill.** "I know this algorithm" is the exact rationalization that ships off-by-one and missing-postcondition bugs.
|
||
|
||
## When to Use This Skill
|
||
|
||
Use **invariant-guard** when writing or reviewing algorithms where the obvious implementation is subtly wrong:
|
||
|
||
- Postcondition stronger than the loop's natural invariant: Boyer–Moore majority, Floyd's cycle detection, leftmost vs any binary search, QuickSelect partition.
|
||
- In-place mutation with read+write pointers: dedup-in-place, partition, rotate.
|
||
- Recursion with multiple parameters or accumulator state.
|
||
- Off-by-one suspects with duplicates, empty inputs, boundary values.
|
||
- Iterative refinements that must terminate: fixed-point, Newton, EM.
|
||
- Any function where you catch yourself thinking "I know this algorithm" — the trap is usually in the contract, not the loop body.
|
||
|
||
Pairs with `lemmaly` (picks the algorithm) and `mathguard` (picks the math). Load `invariant-guard` *after* the algorithm has been chosen and *before* the loop body is written.
|
||
|
||
## The Iron Law
|
||
|
||
```text
|
||
NO LOOP OR RECURSION WITHOUT A WRITTEN INVARIANT AND TERMINATION ARGUMENT
|
||
```
|
||
|
||
If you cannot write the invariant in one sentence, you have not designed the loop. Write code anyway and you are coding by guess — and the bug will be in the case you did not enumerate.
|
||
|
||
## Non-negotiable rules
|
||
|
||
1. **Every loop gets a one-line invariant.** Before writing any loop, state in one sentence what is true at the top of every iteration. Examples:
|
||
- "At loop top: `result` contains the sum of `a[0..i)`."
|
||
- "At loop top: `lo ≤ target_position ≤ hi`."
|
||
- "At loop top: `seen` contains every element processed so far; `dups` contains every element that appeared at least twice."
|
||
|
||
If you cannot write the invariant in one sentence, you have not designed the loop yet.
|
||
|
||
2. **Every loop gets a one-line termination argument.** Name the quantity that strictly decreases (or strictly increases toward a bound) on every iteration. Examples:
|
||
- "`hi − lo` strictly decreases each iteration."
|
||
- "`i` increases by 1 and is bounded above by `n`."
|
||
- "`stack.length` strictly decreases each pop; nothing pushes inside this branch."
|
||
|
||
No termination argument, no loop.
|
||
|
||
3. **Every recursion gets an explicit base case and a measure.** Before writing a recursive function, state:
|
||
- The base case(s) — the smallest inputs that return without recursing.
|
||
- The measure — a non-negative integer that strictly decreases on every recursive call (e.g. `len(xs)`, `hi − lo`, `depth`, `n`).
|
||
- The combination — how the recursive results combine into the answer.
|
||
|
||
No base case + measure, no recursion. (Mutual recursion: state the measure across the cycle.)
|
||
|
||
4. **List edge cases before writing, not after.** For every function operating on a collection or number, list which of these apply and how they behave:
|
||
- Empty input (`[]`, `""`, `null`, `undefined`, `None`).
|
||
- Singleton (`[x]`).
|
||
- All-equal elements.
|
||
- Already-sorted / reverse-sorted input.
|
||
- Duplicates (when uniqueness is assumed).
|
||
- Negative numbers, zero, exactly the boundary value.
|
||
- Integer overflow / underflow at the type max/min.
|
||
- NaN, ±Infinity, `-0`, denormals (for floats).
|
||
- Off-by-one boundaries: index 0, index n−1, index n, length 0, length 1.
|
||
- Concurrent modification while iterating.
|
||
|
||
The cases that apply must each have a one-phrase expected behavior written down.
|
||
|
||
5. **Make illegal states unreachable, not just unhandled.** Prefer encoding constraints in types and structure so the wrong state cannot be constructed:
|
||
- Sum type over boolean flag soup (`Loading | Loaded(data) | Error(msg)` not `{loading, data, error}`).
|
||
- Newtype for IDs that must not be swapped (`UserId` vs `OrderId`).
|
||
- Non-empty list type when the function requires at least one element.
|
||
- Parsed value at the boundary, not validated repeatedly downstream (parse-don't-validate).
|
||
|
||
If the language cannot encode it, write the invariant as a comment and assert it at the boundary.
|
||
|
||
## The pre-write protocol
|
||
|
||
Before producing non-trivial code that has loops, recursion, or non-trivial state, your message must contain — in this order:
|
||
|
||
1. **Function contract** — preconditions, postconditions, and what the function returns. One line each.
|
||
2. **Loop invariants** — one per loop. (Rule 1.)
|
||
3. **Termination arguments** — one per loop or recursion. (Rules 2, 3.)
|
||
4. **Base cases and measure** — for recursion. (Rule 3.)
|
||
5. **Edge case table** — bullets, one per applicable case, with expected behavior. (Rule 4.)
|
||
6. **Illegal states made unrepresentable** — name the types or asserts that enforce invariants. (Rule 5.)
|
||
7. **The code.**
|
||
8. **Self-check** — one line per loop confirming the invariant holds at top, body preserves it, and exit implies postcondition.
|
||
|
||
If any of 1–6 is missing, do not emit code.
|
||
|
||
## Worked trap — Boyer–Moore majority vote
|
||
|
||
This is the canonical "the trap is in the contract, not the loop body" case.
|
||
|
||
**Naive baseline (what gets shipped without the skill):**
|
||
|
||
```typescript
|
||
function findMajority(arr: number[]): number | null {
|
||
if (arr.length === 0) return null;
|
||
let candidate = arr[0], count = 0;
|
||
for (const x of arr) {
|
||
if (count === 0) candidate = x;
|
||
if (x === candidate) count++; else count--;
|
||
}
|
||
return candidate; // BUG: returns the candidate even when no majority exists
|
||
}
|
||
```
|
||
|
||
This implementation fails on `[1,2,3]` (returns `3`, expected `null`) and `[2,2,1,1]` (returns `1`, expected `null`). The voting loop is correct; the postcondition is wrong.
|
||
|
||
**Why the protocol catches it.** Writing **step 1 (function contract)** forces the postcondition in plain language:
|
||
|
||
> Returns `x` iff `count(x, arr) > arr.length / 2`; else `null`.
|
||
|
||
Then writing **step 2 (loop invariant)** forces the invariant of the voting pass:
|
||
|
||
> If a strict majority element exists in `arr`, it equals `candidate` when the loop exits.
|
||
|
||
These two statements are not equivalent. The loop invariant guarantees "if a majority exists, it is the candidate" — not "the candidate is a majority." Once you write both down, the gap is visible: you need a second pass to verify, or the postcondition is unmet.
|
||
|
||
**Correct implementation that survives the protocol:**
|
||
|
||
```typescript
|
||
function findMajority(arr: number[]): number | null {
|
||
if (arr.length === 0) return null;
|
||
// Pass 1: vote.
|
||
let candidate = arr[0], count = 0;
|
||
// inv: if a strict majority exists in arr, it equals candidate at every count===0 reset.
|
||
for (const x of arr) {
|
||
if (count === 0) candidate = x;
|
||
if (x === candidate) count++; else count--;
|
||
}
|
||
// Pass 2: verify — the voting invariant is strictly weaker than the postcondition.
|
||
let tally = 0;
|
||
// inv: tally = count of candidate in arr[0..i).
|
||
for (const x of arr) if (x === candidate) tally++;
|
||
return tally * 2 > arr.length ? candidate : null;
|
||
}
|
||
```
|
||
|
||
**Pattern to generalize.** The same trap appears in:
|
||
|
||
- **Floyd's cycle detection** — finding the meeting point tells you a cycle exists, *not* where it starts. You need a second walk.
|
||
- **Two-pointer "find any"** vs **"find leftmost"** — the loop invariant for one does not satisfy the postcondition of the other.
|
||
- **QuickSelect partition** — the loop returns a position; the postcondition is that the element at that position is the k-th smallest. Off by one in the partition invariant silently breaks it.
|
||
- **DP with reconstruction** — the table tells you the optimum value; reconstructing the optimum path needs separate invariants on the choice array.
|
||
|
||
In every case: **write the postcondition first; write the loop invariant second; check that the second implies the first. If not, you are missing a pass, a check, or an auxiliary state.**
|
||
|
||
## Canonical example — binary search for the leftmost match
|
||
|
||
Most "I know binary search" implementations are written for "find any match." The trap is the postcondition.
|
||
|
||
**Problem.** Given a sorted array with duplicates, return the index of the **leftmost** occurrence of `target`, or `-1`.
|
||
|
||
### Without the protocol — returns any match
|
||
|
||
```ts
|
||
function leftmost(a: number[], target: number): number {
|
||
let lo = 0, hi = a.length - 1;
|
||
while (lo <= hi) {
|
||
const mid = (lo + hi) >> 1;
|
||
if (a[mid] === target) return mid; // returns ANY occurrence
|
||
if (a[mid] < target) lo = mid + 1; else hi = mid - 1;
|
||
}
|
||
return -1;
|
||
}
|
||
// leftmost([1,2,2,2,3], 2) → may return 2, not 1
|
||
```
|
||
|
||
The loop invariant ("target lies in `a[lo..hi]` if anywhere") is satisfied. But the postcondition ("returned index is the *smallest* `i` with `a[i] === target`") is strictly stronger. The loop body's early return abandons the search before reaching the leftmost.
|
||
|
||
### With the protocol — contract-driven leftmost
|
||
|
||
```ts
|
||
function leftmost(a: number[], target: number): number {
|
||
// contract:
|
||
// pre: a is sorted ascending
|
||
// post: returns smallest i with a[i] === target, or -1 if absent
|
||
let lo = 0, hi = a.length; // half-open [lo, hi)
|
||
// inv: every index < lo has a[i] < target; every index ≥ hi has a[i] > target OR is past leftmost match
|
||
// term: hi - lo strictly halves each iteration
|
||
while (lo < hi) {
|
||
const mid = (lo + hi) >> 1;
|
||
if (a[mid] < target) lo = mid + 1; else hi = mid;
|
||
}
|
||
// exit: lo === hi, and by invariant lo is the leftmost index where a[lo] >= target
|
||
return lo < a.length && a[lo] === target ? lo : -1;
|
||
}
|
||
```
|
||
|
||
Same loop shape. The difference is the contract was written first — and the loop body was chosen to maintain an invariant that *implies* the postcondition.
|
||
|
||
## Common invariant patterns to reach for
|
||
|
||
| Loop / algorithm shape | Canonical invariant | Termination |
|
||
|---|---|---|
|
||
| Linear scan accumulating | `acc = f(a[0..i))` at top | `i` increases by 1, bounded by `n` |
|
||
| Two-pointer (sorted) | `target (if any) lies in a[lo..hi]` | `hi − lo` strictly decreases |
|
||
| Binary search | `target (if present) ∈ a[lo..hi]` and `a[lo..hi]` non-empty | `hi − lo` strictly halves |
|
||
| Sliding window | window `[l..r)` satisfies the constraint; answer ≥ best so far | `r` advances at least once per outer iter |
|
||
| BFS | every node at distance < d has been popped; queue contains some at distance d | strict node count decrease per pop |
|
||
| DFS / recursion on tree | result for subtree rooted at v = combine(children results) | depth (or remaining nodes) strictly decreases |
|
||
| Divide and conquer | result on `a[lo..hi]` = combine(results on the two halves) | `hi − lo` strictly halves |
|
||
| Greedy with priority queue | extracted item is globally optimal for the remaining problem | heap size strictly decreases per extract |
|
||
| Union-Find op | `find(x)` always returns the canonical root of x's component | tree height bounded by O(log n) (with rank) |
|
||
| In-place partition | `a[0..i)` < pivot; `a[i..j)` ≥ pivot; `a[j..n)` unseen | `n − j` strictly decreases |
|
||
|
||
## Edge case table — defaults to consider
|
||
|
||
| Input shape | Cases to check |
|
||
|---|---|
|
||
| Array / list | empty, singleton, all-equal, sorted, reversed, with duplicates |
|
||
| String | empty, single char, all whitespace, unicode (surrogates, combining), bytes vs code points |
|
||
| Integer | 0, 1, −1, MIN, MAX, MAX − 1, near overflow in arithmetic, division by 0 |
|
||
| Float | 0.0, −0.0, NaN, ±Inf, denormal, exact comparison should be ε-based |
|
||
| Map / dict | empty, missing key (default vs error), key collision semantics |
|
||
| Tree / graph | empty, single node, cycle (if undirected), self-loop, multigraph, disconnected |
|
||
| Stream / iterator | empty, infinite, single yield, exception mid-iteration |
|
||
| Time / date | DST transition, leap second/day, timezone offset, epoch boundary |
|
||
| Concurrent | empty contention, single thread, max contention, cancellation mid-op |
|
||
|
||
## Output discipline
|
||
|
||
Code you emit must:
|
||
|
||
- Have one comment per loop stating the invariant (use `// inv:` or `# inv:`).
|
||
- Have one comment per recursion stating the base case and measure.
|
||
- Handle every edge case you listed in step 5, or explicitly delegate ("throws on empty — caller responsibility").
|
||
- Assert preconditions at function entry when the language supports it cheaply.
|
||
- Use types (sum types, newtypes, non-empty, non-null) over runtime checks where the language allows.
|
||
|
||
## When to escalate or redirect
|
||
|
||
- The function is performance-critical and you have not picked the algorithm — go back to **`lemmaly`** first; pick the algorithm, then state its invariants here.
|
||
- The technique is mathematical (probabilistic, FFT, geometry) — load **`mathguard`**; invariants for approximate algorithms include ε-bounds, not equality.
|
||
- The code is concurrent — invariants must account for interleaving; explicitly state "single-threaded only" if that is the assumption.
|
||
|
||
## Rationalizations to watch for
|
||
|
||
| Excuse | Reality |
|
||
| --- | --- |
|
||
| "I know this algorithm — single pass, done." | Knowing the loop ≠ knowing the contract. The trap usually lives in the postcondition the loop does not enforce. |
|
||
| "I traced it in my head, it works." | Mental tracing skips edge cases. Write the invariant; check it implies the postcondition. |
|
||
| "Edge cases are obvious." | Then write them down in 30 seconds. If they are obvious, the table is cheap. If they are not, the table just saved you. |
|
||
| "Tests will catch it." | Tests catch the examples you thought of. The trap is the example you did not. Postconditions catch all examples. |
|
||
| "The postcondition is implied." | If it were, the natural loop invariant would equal it. When they differ (Boyer–Moore, leftmost search, QuickSelect), you need a second pass, an extra check, or auxiliary state. |
|
||
| "Adding a verification pass feels redundant." | Boyer–Moore voting + verification is still O(n). "Feels redundant" is the rationalization that ships the bug. |
|
||
|
||
## Red flags — STOP and write the invariant first
|
||
|
||
- About to write `while (...)` without having stated what is true on entry.
|
||
- About to write `if (i === n − 1)` or `if (i === n)` — boundary suspicious, restate the invariant.
|
||
- About to recurse without naming the base case in this message.
|
||
- About to write `// TODO: handle empty` — handle it now or change the type so empty is impossible.
|
||
- About to use `==` on floats.
|
||
- About to compare across signed/unsigned or across types where overflow rolls.
|
||
- About to silently swallow an error in the middle of a loop ("just continue").
|
||
- Tests pass but you did not actually state what the function guarantees.
|
||
- "It works on the examples I tried."
|
||
|
||
## Verification checklist
|
||
|
||
Before claiming the function is correct:
|
||
|
||
- [ ] Every loop has a one-line `// inv:` comment in code.
|
||
- [ ] Every loop has a termination argument written down (in comment or PR description).
|
||
- [ ] Every recursion names its base case and measure in code.
|
||
- [ ] The function's postcondition is written and is implied by the exit state of the last loop.
|
||
- [ ] Every applicable edge case from the table has a test or an explicit "delegated to caller" note.
|
||
- [ ] At least one test exercises each non-trivial boundary (empty, singleton, max, off-by-one).
|
||
- [ ] Illegal states the function rejects are either unrepresentable in the type, or asserted at entry.
|
||
- [ ] For approximate/randomized algorithms (escalated to mathguard): ε-bounds are part of the postcondition, not equality.
|
||
|
||
Cannot check every box? The code is example-correct, not behavior-correct. Either fill the gap or downgrade the function's claimed contract.
|
||
|
||
## Limitations
|
||
|
||
- **Not an automated prover.** invariant-guard requires the author to *write* invariants; it does not mechanically check them. Pair with property-based tests for stronger evidence.
|
||
- **Concurrency is out of scope by default.** Stated invariants assume single-threaded execution unless explicitly extended; multi-threaded reasoning needs additional happens-before / linearizability arguments.
|
||
- **Float and overflow edge cases are language-specific.** The edge-case table is a checklist, not a substitute for understanding your language's numeric semantics.
|
||
- **Will slow down trivial code.** For one-liners that obviously cannot fail, the protocol is overhead; reserve it for non-trivial loops, recursion, and in-place mutation.
|
||
- **Documentation is the only enforcement.** If the author skips writing the invariants, this skill cannot detect that — pair with code review or a PR template that asks for the contract.
|
||
|
||
## The thesis, in one line
|
||
|
||
> **Tests verify examples. Invariants verify behavior. AI assistants ship example-correct, behavior-wrong code by default. invariant-guard makes them reason about behavior first.**
|
||
|
||
## Related Skills
|
||
|
||
- `lemmaly` — algorithm choice must be settled before invariants; load lemmaly first if the algorithm family is unclear.
|
||
- `mathguard` — ε-bounded postconditions for approximate / randomized algorithms.
|
||
- `complexity-cuts` — if 3+ optimization transformations have failed tests, the bug is a missing contract, not a missing optimization — escalate here.
|