Proof and analysis

Proof and Analysis

Purpose

Tests check the inputs you thought of; analysis covers the inputs you didn't. This skill is the paper-and-pencil discipline of engineering: name the invariants, enumerate the input space exhaustively, compute the complexity of the actual loops, estimate scale with powers of ten, and reason about interleavings — then write the argument down so someone can attack it.

Metadata

• Prerequisites: none (loadable standalone).
• Related Skills: validation-and-testing (a proof covers all inputs, a test proves the environment works — you usually want both), performance-engineering (consumes this skill's estimation; owns empirical measurement), system-design (consumes capacity arithmetic in step 6), debugging-playbook (hypothesis discipline is shared), refactoring-playbook (consumes behavior-preservation arguments).
• Owns: invariants and pre/postconditions; exhaustive case analysis; complexity analysis; back-of-envelope estimation; concurrency interleaving reasoning.

When to Use / When NOT to Use

Use when:

• Deciding whether a function/algorithm is correct for ALL inputs, not just tested ones.
• Analyzing complexity ("will this loop survive 100× the data?").
• Estimating capacity/cost/load before building (feeds system-design).
• Reasoning about shared state, races, and interleavings.
• Arguing a refactor is behavior-preserving (feeds refactoring-playbook).
• Reviewing logic-dense code where testing every path is impractical.

Do NOT use (load the sibling instead):

• The question is answerable by MEASURING a running system → performance-engineering (analysis predicts; measurement decides).
• The unknown is an external fact (how a library behaves, what an API returns) → research-methodology (go read the source; don't derive what you can look up).
• The code is misbehaving NOW → debugging-playbook (analysis generates hypotheses for it, not replacements for reproduction).
• The logic is trivial (no branches, no loops) → don't ceremonialize it (engineering-minimalism).

Definitions & Mental Model

• Invariant: a property that holds at every observable point ("the list is always sorted between operations"; "balance never goes negative").
• Precondition / postcondition: what a function assumes on entry / guarantees on exit. Together with invariants, they are the contract logic is judged against.
• Case analysis: partitioning the input space into exhaustive, disjoint classes and arguing each class separately.
• Back-of-envelope estimation: order-of-magnitude arithmetic with explicit assumptions — the goal is catching factor-of-100 surprises, not three significant figures.
• Interleaving: one possible ordering of operations from concurrent actors; correctness under concurrency means correctness under EVERY interleaving.

Mental model: an informal proof is an argument written so a hostile reader can attack it. That definition does all the work: it forces the claim to be explicit (state the invariant), the coverage to be total (which case does input X fall in? — if the cases aren't exhaustive, the hostile reader wins instantly), and the assumptions to be visible (each one is an attack surface — and that is good, because an attacked-and-defended assumption is knowledge, while a hidden one is a bug's hiding place). The complement discipline: an estimate is a proof about magnitude — same rules, coarser numbers.

Core Methodology

1. State the claim precisely. "This function is correct" is not analyzable. "For any list of ≥0 integers, this returns the maximum, and raises ValueError on empty input" is. The claim names the input domain, the guaranteed output, and the error contract. If you cannot state the claim, that is the finding — the code has no specification to be correct against.
2. Name the invariants and pre/postconditions. For loops: what is true before, preserved by each iteration, and — combined with the exit condition — implies the postcondition? (The loop-invariant argument is the workhorse of informal proof.) For data structures: what property do all operations preserve? Write them as comments or in the analysis note — an invariant that lives only in your head dies with the context.
3. Enumerate the input space exhaustively. The standard partition, applied to every analyzed input:

For each input, argue these classes (or state why a class is impossible):
├─ EMPTY        (zero items, empty string, null/None, missing field)
├─ ONE          (single element — boundary between empty and many)
├─ MANY         (the "normal" case)
├─ MAXIMUM      (largest allowed / overflow-adjacent / limit-sized)
├─ MALFORMED    (wrong type, wrong encoding, violates the precondition)
├─ DUPLICATES / TIES  (equal keys, repeated values — breaks naive assumptions)
├─ BOUNDARY     (off-by-one candidates: first, last, exactly-at-limit)
└─ ADVERSARIAL  (if the input crosses a trust boundary —
                 route the consequences to security-review-playbook)

The classes must be exhaustive (every input falls somewhere) and each class's argument must be short. A class you can't argue is where the bug is. 4. Compute complexity from the actual code, not vibes. Count the loops as written: a loop over n containing a lookup that scans n is O(n²) no matter what the function name promises. Standard traps: hidden linear operations inside loops (in on a list, string concatenation in a loop, per-item queries — the N+1 pattern), sorting inside a loop, recursion without memoization. State the result with its variable ("O(n·m) where n=orders, m=lines/order") and the practical verdict at expected scale — O(n²) at n=200 is fine; at n=200,000 it is an outage. Hand measured confirmation to performance-engineering. 5. Estimate with powers of ten and written assumptions. The procedure: (a) write every assumption as a number ("~5k orders/day", "~200 bytes/record"); (b) multiply with aggressive rounding (powers of 10, 2, and 5 are enough); (c) sanity-check the result against a known anchor (disk sizes, requests/sec a single process handles, tokens per page); (d) state the conclusion WITH its assumptions so an attacker can find the wrong one. The deliverable is "this fits in memory for a decade" or "this is 400GB/month — redesign", never false precision. 6. Reason about concurrency by enumerating interleavings on the smallest case. Two actors and one shared thing expose most races:

• Inventory what is actually shared (variables, rows, files, counters) — unshared state cannot race.
• For each shared thing, write the smallest dangerous interleaving as a two-column timeline (A reads… B reads… A writes… B writes — the lost update).
• Check the fix claims: is the compound operation actually atomic, or just short? Does the lock cover the read AND the write? Check-then-act (if exists: use) is the classic non-atomic compound.
• If more than two actors or two shared objects are essential to the argument, the design is too clever to verify by hand — simplify the design rather than lengthening the proof (engineering-minimalism).

7. For refactors: argue behavior preservation by partition + spot execution. Partition the input space (step 3); argue old and new code compute the same result per class; then hand-execute both on one representative of the trickiest class. This argument plus characterization tests is refactoring-playbook's proof obligation, discharged.
8. Write the argument down and invite attack. A paragraph in the PR description, a comment block, or an analysis note: claim, invariants, cases, verdict, assumptions. Then the crucial move — hand it to someone (or something) incentivized to break it. An argument that survives attack is a proof for engineering purposes; an argument nobody saw is a hunch with formatting.
9. Know the limits: proof and test are complements. The proof covers all inputs but assumes the platform behaves (the compiler, the library, the database). The test covers few inputs but exercises the real platform. High-stakes logic gets both: the argument for coverage, the test for reality (validation-and-testing turns the trickiest analyzed classes into the test cases — the partition IS the test plan).

Analysis checklist

• Claim stated with input domain, output guarantee, and error contract
• Invariants / pre / postconditions named and written down
• Input space partitioned exhaustively; every class argued or ruled impossible
• Complexity computed from actual loops, stated with variables and scale verdict
• Estimates: assumptions written as numbers, rounded arithmetic shown, anchored
• Concurrency: shared-state inventory + smallest dangerous interleaving examined
• The argument is written where a reviewer can attack it
• Trickiest classes handed to validation-and-testing as test cases

Discovery & Audit Commands

This domain is judgment-driven; the commands that apply locate the analysis targets:

# Find the logic-dense code that deserves analysis (nesting, branches)
grep -rn -E "for .*for |while .*while" --include="*.py" . | grep -v node_modules | head    # nested-loop candidates (O(n²) suspects)
grep -rc "if \|elif \|else" --include="*.py" . 2>/dev/null | sort -t: -k2 -rn | head      # branchiest files

# Hidden-linear-inside-loop suspects
grep -rn -B2 " in " --include="*.py" . | grep -A2 "for " | head -20                        # `x in list` inside loops
grep -rn -iE "for .*:" --include="*.py" . | grep -iE "query|select|fetch|get\(" | head     # N+1 query candidates

# Shared-state inventory for concurrency analysis
grep -rn -E "global |threading|multiprocessing|asyncio|Lock|Semaphore" --include="*.py" . | grep -v node_modules | head
grep -rn -E "async |await " --include="*.py" --include="*.ts" . | grep -v node_modules | head -10

# Existing invariants/contracts already written down
grep -rn -iE "invariant|precondition|postcondition|assert " --include="*.py" . | grep -v node_modules | head

Failure Modes & Anti-patterns

Symptom	Mistake	Correction
"Obviously correct" code fails on empty input	Case analysis skipped the trivial classes	The exhaustive partition, every time — EMPTY and ONE first (step 3)
Works at n=1k, dies at n=100k	Complexity judged by function names, not loops	Count the loops as written; hidden linears hunted (step 4)
Design approved, storage bill 100× estimate	No estimate, or unstated assumptions	Powers-of-ten arithmetic with written, attackable assumptions (step 5)
Race appears only under production load	"It's fast, it won't collide"	Enumerate the smallest dangerous interleaving; speed is not atomicity (step 6)
Check-then-act bug behind a lock that covers only the write	Lock scope not analyzed	The lock must span the read AND the write of the compound (step 6)
Proof exists, code still fails in prod	Proof treated as replacing tests	Complements: argument for coverage, test for platform reality (step 9)
Analysis convinced its author, wrong anyway	Argument never exposed to attack	Write it down; hand it to a hostile reader (step 8)
Three-page proof for a two-line function	Ceremony where none is due	Analysis effort proportional to logic density (When NOT)
Ties/duplicates break the "sorted" assumption	Equality class forgotten	DUPLICATES/TIES is a first-class partition member (step 3)
Estimate with 4 significant figures, wrong by 50×	False precision hiding a wrong assumption	Round hard; the assumptions are the answer (step 5)

Worked Example

Task: verify a de-duplication function before it ships: "given a list of customer records, return one record per email, keeping the most recent."

1. Claim: for any list of records with (email, timestamp) fields, returns exactly one record per distinct email — the one with the maximum timestamp — preserving no particular order; raises nothing (empty list → empty list).
2. Invariant (loop): after processing k records, the accumulator maps each seen email to the max-timestamp record among the first k. Preserved per iteration (compare-and-replace); at exit, implies the postcondition.
3. Case analysis: EMPTY → empty dict → empty list ✓. ONE → that record ✓. MANY, all distinct → identity ✓. DUPLICATES → covered by the invariant ✓. TIES — two records, same email, same timestamp: the code keeps the first encountered (uses > not >=). The claim said "the most recent" — with a tie, which one? The claim is underspecified: finding #1, resolved by amending the claim ("ties keep the first occurrence") and documenting it. MALFORMED — record missing email: KeyError propagates; claim amended to state the precondition, and the caller (a trust boundary) gains validation. BOUNDARY — timestamps at equal microseconds are the tie case, already handled.
4. Complexity: one pass, dict operations O(1) amortized → O(n). At the expected n≈50k: trivial. (The rejected first draft used record in seen_list — O(n²), caught by the hidden-linear hunt.)
5. Handoff: the TIES and MALFORMED classes become the two new test cases (validation-and-testing); the argument lands in the PR description, where a reviewer promptly attacks the timezone assumption behind "most recent" — a fourth finding the tests would never have surfaced.

Repository Examples

Repo facts below are point-in-time illustrations (as of 2026-07-04) — examples, never assumptions about your system.

• agentix (~/agentix) — case analysis reified as tests: the JSON-extraction tests cover plain / fenced / embedded / nested / malformed inputs — an input-space partition of exactly this skill's shape, executed as a suite. The balanced-brace scanner respects string escapes — the analysis insight that } inside "..." doesn't close a brace is a case-analysis finding (the MALFORMED/BOUNDARY classes) baked into code.
• prism (~/prism) — bounded-resource reasoning in the design: MAX_LINES_PER_CHUNK=120, MAX_FILES_PER_PR=10, and Semaphore(5) are the artifacts of capacity reasoning — each cap answers "what bounds the work?" on paper before the system ran.
• ragit (~/ragit) — estimation shaping a design: batching embeddings 64 at a time reflects the arithmetic that per-chunk calls to a remote service dominate cost — the batching decision is an estimate's conclusion in code form.

Validation Exercise (any repository): pick one non-trivial function; write its claim (domain, guarantee, error contract), run the 8-class partition, and compute its complexity from the loops. Any class you cannot argue in two sentences is either a latent bug or a missing precondition — both are findings.

Validation Criteria

You applied this skill correctly when:

1. The claim is written and names the input domain, guarantee, and error contract.
2. The partition is exhaustive — a reviewer cannot name an input that falls in no class — and each class has an argument.
3. The complexity statement points at the specific loops/operations, and the scale verdict uses expected numbers.
4. Estimates show their assumptions as numbers a reviewer can individually attack.
5. Concurrency claims come with the shared-state inventory and at least one examined interleaving.
6. The trickiest classes exist as test cases, and the written argument survived at least one hostile read.

Provenance & Maintenance

• Sources: ~/agentix, ~/prism, ~/ragit — investigated 2026-07-04. The methodology (loop invariants, case partition, back-of-envelope) is timeless engineering practice, not repo-derived. Skill authored 2026-07-06.
• Assumptions: repo constants (batch=64, chunk=120, semaphore=5) are point-in-time; the inference that they encode capacity reasoning is Candidate (consistent with the code, not documented by its author).
• Re-verification commands:

  grep -rn "fenced\|balanced\|malformed" ~/agentix/tests | head
  grep -rn "MAX_LINES_PER_CHUNK\|Semaphore" ~/prism/prism ~/prism/.env.example
  grep -n "batch" ~/ragit/ragit/indexer.py | head
  

• Likely to drift: the example constants; nothing else — the core method does not age.
• Maintenance checklist:
  • Re-run re-verification; re-stamp Repository Examples.
  • Confirm cross-referenced skills still exist under their directory names.