docs/verification-theory.md
Verification Theory
Repository-independent. Derived from the failure record of a single investigation, but stated without reference to it. Conditions are numbered as requirements; each was purchased with a distinct measured failure, and none was added for symmetry.
0. The Enumeration Lemma
A search space derived from observed instances is a subset of the observed. A subset provides no bound on its complement. Therefore a methodology whose search space is content-derived cannot support a completeness claim, regardless of how many instances it finds.
This is the whole theory in one line. Everything below is its consequences.
The lemma is near-tautological, which is precisely why it is dangerous: a content-derived search feels thorough in proportion to how much it finds, and finding more is evidence of nothing.
1. The formal object space
Enumerate positions, not meanings.
The object space is the set of syntactic positions in the artifact at which a value can reach the observable output. For a renderer: every attribute binding in every output-producing construct. For a compiler: every emitted instruction slot. For a serializer: every field write.
The space must be decidable without knowing what any value means. Semantic categories — "visual properties", "colours", "state-derived values" — are inadmissible as the object space, because they are exactly what gets discovered late. A category discovered on pass n was absent from the space on pass n−1.
2. The grammar
The search space is generated by a parser over the artifact's language, never by pattern-matching over its text.
Regex over source is a sampling method, not an enumeration method: it returns only the syntactic forms the author anticipated. Every sampling method inherits the Enumeration Lemma.
The grammar supplies the space; the artifact supplies the population; neither is supplied by the investigator's expectation.
3. Completeness criterion
A methodology is complete iff classification over the object space is:
- total — every element receives a class; and
- functional — no element receives two;
and the enumerated population is provably equal to the grammar-generated one, by cardinality or by construction.
Completeness is a property of the enumeration. It is never a property of the findings.
4. Soundness criterion
Every class must map to a rule capable of rejecting.
A class with no rejecting rule is a category, not a check — it partitions the space without constraining it, and produces confidence proportional to nothing.
The rule must be stated independently of the instances that motivated it. A rule fitted to its discovery set cannot reject anything the discovery set did not contain.
5. Coverage criterion
Every rule must have an executable test whose observation surface is identical to the rule's subject.
This is the condition most often violated invisibly, because a test that names the right rule while observing the wrong object appears to cover it. Testing an intermediate representation does not cover a rule about final output. The test passes; the rule is violated; nothing detects the difference.
Coverage is a relation between three things — rule, subject, observation surface — and requires the last two to be equal, not merely related.
6. Falsification criterion
Every test must have been observed failing against a reproduction of the violation it defends — and, separately, the enumerator itself must be mutation-tested.
The first half is standard and sufficient for implementation defects. The second half is not standard and is required by the Enumeration Lemma: a mutation that introduces an element the enumerator cannot classify must cause failure. Without it, the enumeration can silently become incomplete as the artifact grows, and no test will notice, because every test operates on the enumerated set.
7. Stopping criterion
Completeness may be asserted only when all of the following hold simultaneously:
- the object space is grammar-derived (§1, §2);
- the enumerated population is verified equal to the generated one (§3);
- classification is total and functional (§3);
- every class has a rejecting rule stated independently of its discovery set (§4);
- every rule has a test whose observation surface equals its subject (§5);
- every test has been observed failing (§6);
- a mutation introducing an unclassifiable element fails the enumerator (§6).
Absence of findings is never a stopping criterion. A search that stops because it found nothing has measured its own exhaustion, not the space.
8. Assumptions
| Class | Assumption |
|---|---|
| Proven | The Enumeration Lemma: a subset bounds nothing about its complement. |
| Proven | Alpern–Schneider (1985); Clarkson–Schneider (2010) — where trace/hyperproperty decomposition is used. |
| Measured | Content-derived enumeration fails repeatedly and in the same shape: three consecutive passes, each correcting the last, each reproducing the identical bias. |
| Measured | A test observing the wrong surface passes while its named rule is violated. |
| Measured | Rules can exist with zero executable coverage while appearing covered, because tests cite article numbers rather than observing subjects. |
| Assumed | The artifact's language has a decidable grammar and an available parser. |
| Assumed | Output-producing constructs are identifiable from that grammar. |
| Assumed | Finite classification is possible — the population admits a finite class set. |
| Unverifiable | That the rule set is itself complete. Establishable only from outside the system. |
| Unverifiable | That the rules faithfully capture intent. |
| Unverifiable | That a class boundary is correct rather than merely consistent. |
The three unverifiable assumptions are the permanent ceiling. A methodology satisfying §1–§7 establishes that the artifact conforms to its rules — never that its rules are right.
9. Why omitting any condition is structurally fatal
Each omission is independently fatal, and each has a distinct observed instance. None is included for completeness of the list.
| Omit | Consequence | Failure mode |
|---|---|---|
| §1 object space | "Complete" has no referent | vacuous claim |
| §2 grammar | Space is content-derived; Enumeration Lemma applies | enumerated 16% of the population and asserted completeness |
| §3 completeness | Unclassified elements exist and are invisible | a class discovered on a later pass was absent from the space on the earlier one |
| §4 soundness | Classes that cannot reject produce confidence from nothing | a class justified by the investigator's own interpretation |
| §5 coverage | Rule violated, test green, no signal | verification against an intermediate object while the rule governed the output |
| §6 falsification | Tests that cannot fail certify nothing | a guard that survived its own deletion; a fixture that never executed the path it asserted |
| §7 stopping | Reasoning from absence of findings | four successive completeness claims, each falsified by the next pass |
The pattern across §2, §3 and §7 is one mechanism seen three ways: the investigator enumerates the shape of the thing most recently found and mistakes that for enumerating the space. Conditions §1–§3 exist to remove the investigator from the definition of the search space; §5–§6 exist to remove them from the definition of success.
10. Generalization
These conditions are not renderer-specific. Nothing in §1–§7 references rendering, visualization, or geometry. They reference an artifact with a grammar, an observable output surface, a rule set, and tests.
They apply to verification of any transducer — any system mapping structured input to observable output where the claim is that every output element traces to input. Renderers, compilers, serializers, query planners, report generators, and API response builders are the same problem with different grammars. Only §1's instantiation changes: JSX attribute bindings, emitted instructions, field writes, response keys.
The honest boundary. §2 requires the output positions to be statically
enumerable from grammar. A system whose output positions are computed at runtime
— reflection-driven emission, eval, fully dynamic dispatch — violates that
precondition, and for such a system no completeness claim of this kind is
available at all. That is a real limit, not a gap to be patched: the object space
is not decidable, so §3 has nothing to range over.
Within that boundary the conditions are necessary and jointly sufficient. Necessary, because §9 exhibits an independent fatal failure for each omission. Sufficient for conformance, because §1–§3 fix the space, §4 makes each class rejecting, §5 binds each rule to an observation of its own subject, §6 proves each binding can fail, and §7 forbids the one inference — from absence — that none of the others rule out.
Sufficient for conformance. Never sufficient for correctness: that remains bounded by the three unverifiable assumptions in §8.
11. Adversarial review — the framework does not survive as stated
Four attacks. Three succeed. The framework is revised, not defended.
Attack 1 — satisfies all seven, permits an invalid claim: SUCCEEDS
Construct a renderer verification that satisfies every condition: positions enumerated from the grammar, population verified equal, classification total and functional, every class rejecting, every test observing rendered output, every test observed failing, enumerator mutation-tested.
It still admits an invalid completeness claim, because output-contributing positions need not be syntactic bindings.
In SVG, fill and stroke are inherited presentation attributes. A <path>
carrying no fill attribute renders with its parent <g>'s fill. Grammar
enumeration over attribute bindings finds nothing at that position, and the
pixel nevertheless has a colour. The same holds for any external contributor:
stylesheets, <style> blocks, CSS custom properties, theme providers, user-agent
defaults.
The seven conditions are stated relative to a chosen artifact. They say nothing about whether the artifact set is closed under output-contribution — and condition 1 silently presupposes it, since "positions in the artifact" is circular unless the contributing artifacts can themselves be enumerated.
Attack 2 — violates a condition, establishes completeness legitimately: SUCCEEDS
Two independent constructions.
Exhaustive output enumeration. A status indicator with three possible renderings — red, amber, green. Enumerate the output space directly, test all three, and completeness follows by exhaustion. Conditions 1 and 2 are violated: no position enumeration, no parser. The claim is nonetheless valid.
Proof in place of enumeration. If the output function is proved total over a characterised range, completeness follows from the proof. Again no position enumeration is required.
Both show conditions 1–2 are necessary only when direct output enumeration or proof is infeasible. As stated, they are over-claimed as universal.
Attack 3 — an independent eighth condition: SUCCEEDS
§8. Closure of the artifact set. It must be established that no artifact outside the enumerated set can contribute to the observable output.
Independent in both directions: Attack 1 satisfies §§1–7 and violates closure; closure is trivially satisfiable while violating any of §§1–7. Neither implies the other, and §3's "provably equal to the grammar-generated set" does not catch it, because the equality ranges over the grammar of the enumerated artifacts.
A ninth was sought and not found. The candidates reduce: temporal closure (the artifact changes) reduces to §6's enumerator mutation-testing; verifier-of-the-verifier is an infinite regress belonging in §8's unverifiable class, not a condition.
Attack 4 — counterexample to the Enumeration Lemma: PARTIALLY SUCCEEDS
The lemma as stated — a subset provides no bound on its complement — is too strong. Two counterexamples:
- Capture–recapture. Two samples from a population bound its total size. A subset does bound its complement, probabilistically.
- Spanning sets. Observing a basis bounds the entire space exactly.
Both work for the same reason: they reason from subset plus independent structural knowledge, not from the subset alone. The lemma's real content survives once qualified:
A search space derived from observed instances provides no bound on its complement absent independent knowledge of the space's structure.
That qualifier is not a weakening — it is the justification for §2. The grammar is the independent structural knowledge, which is precisely why grammar-derived enumeration escapes the lemma while pattern-matching does not.
12. Revised framework
Eight conditions, with §§1–2 correctly scoped:
- §1–2 apply when direct output enumeration or proof is infeasible. Where the output space is finite and enumerable, or the output function is proved total over a characterised range, position enumeration is unnecessary.
- §8 Closure — no artifact outside the enumerated set contributes to output.
- §§3–7 unchanged.
The Enumeration Lemma carries its qualifier.
What the review establishes. The framework was not merely restated; three of its claims were wrong. Conditions 1–2 were over-scoped, a necessary condition was missing, and the central lemma was too strong. What survived is the part that was purchased with measured failures — §§3–7 — while the parts derived by reasoning about the general case are exactly the parts that broke.
That asymmetry is itself the most reliable finding here.