/declaring-invariants

name: declaring-invariants
description: Find tests that enumerate a domain by copying it, and declare the invariants a codebase depends on. Reports where a parametrize list, for-loop, or it.each iterates a hand-written subset of a dict/set/tuple/Enum that exists in the source, and names the members nothing covers. Use when reviewing tests, when a module gains a name-to-thing table, registry, enum, or dispatch map, before trusting a green suite as evidence a domain is covered, or when asked "is this test actually total", "does anything cover X", "what does this repo guarantee", "which invariants do we declare". Also for vacuous tests that pass over an empty collection, for a domain that has silently NARROWED (an enumeration cannot see that), and for recording the refutation that proves a claim can fail.
metadata:
  version: 0.2.3

declaring-invariants

Two scripts over one idea: **a test that enumerates a domain must loop the registry rather than a copy of it.** Someone also has to say which domains matter in the first place.

python3 scripts/totality_lint.py <repo>   # tests that copy a domain
python3 scripts/claims.py <repo>          # what the repo declares, and what backs it

Python only, stdlib `ast` only: no install, no config file, no network.

The failure it catches

A test that loops a hand-written list passes its runner and proves nothing about completeness. When the same members also exist as a registry in the source, the list is a copy, and the copy drifts the moment someone adds a member to the registry and not to the test. Nothing goes red.

Measured on `oaustegard/remex`, 2026-08-24: adding a fourth member to `ROTATION_CODES` with no construction behind it left the **entire 267-test suite green**. Four separate tests looked total; each parametrized `["haar", "rht"]` against a three-member registry. Only a test that looped the registry itself caught it.

Adapted from the meta-oracle in [`daniloc/coherence`](https://github.com/daniloc/coherence) (`src/oracle-domain.ts`), which classifies an oracle's iteration root as LIVE or LITERAL by parsing the oracle's own AST. That harness needs spec files, a claim grammar, a ledger and Node; the check does not.

`totality_lint.py` — tests that copy a domain

| finding | meaning | |---|---| | `sampled-domain` | a `parametrize` or `for` over a literal whose members are a strict subset of a source registry. The uncovered members are named. | | `ratchet-broken` | a hand-list marked `ratchet` names a member the registry no longer contains. Detected statically, without running anything. | | `unratcheted` | a registry enumerated live with nothing pinning its membership. Suppressed when `no-floor` already claimed the same line. | | `no-floor` | a test iterates a live registry with no `len(...) >= n` assertion in the file, so an emptied registry passes vacuously. | | `stale-ack` | an acknowledgement on a test that now covers the whole domain. |

python3 scripts/totality_lint.py <repo>            # the report
python3 scripts/totality_lint.py <repo> --json
python3 scripts/totality_lint.py <repo> --strict   # exit 1 if any finding
python3 scripts/totality_lint.py --selftest        # fixtures, no repo

A partial domain is often correct. Say so on the test and it stops being a finding:

# totality: partial — mojo has no construction for "none"
@pytest.mark.parametrize("rotation", ["haar", "rht"])
def test_save_params_accepts_every_mojo_rotation(rotation): ...

The marker also works as `totality: partial — <why>` inside the docstring. An acknowledgement on a test that later covers the whole domain is reported as `stale-ack`, so a suppression cannot become a silence.

Why a hand-list is the second form

An enumeration loops **whatever the domain currently holds**, so it is structurally blind to the domain narrowing. Remove a member and the loop simply ranges over fewer of them, green. Raised by Yep, 2026-08-24; reproduced on `oaustegard/remex` before being believed:

| perturbation of `ROTATION_CODES` | domain floor | enumeration | parity | hand-list | |---|---|---|---|---| | grow — add `"hadamard2"` | pass | **RED** | **RED** | pass | | shrink — drop `"none"` | **RED** | pass | RED\* | pass | | substitute — `"none"` → `"xyz"` in both spellings | pass | pass | pass | pass |

\* only because the *other* spelling of the domain did not shrink, which is incidental to that repository.

In the substitution row cardinality holds, both spellings agree, and five green tests cover a registry that quietly stopped supporting a rotation every index on disk was written with. The floor is a **cardinality** check; it cannot see a member swapped for another.

The second form is a **ratchet**: a hand-list asserting the domain keeps containing it. Mark it and the linter checks the pin rather than taking the marker's word for it.

# totality: ratchet — these three shipped; one leaving is a compatibility break
def test_no_shipped_rotation_is_ever_removed():
    for shipped in ("haar", "rht", "none"):
        assert shipped in ROTATION_CODES

Under that same substitution the linter reports `ratchet-broken` naming `'none'` **statically, before any test runs**, and the test itself goes red while the other five pass.

So: an enumeration proves every current member is handled, and a ratchet proves no member left without a decision. `unratcheted` names a registry that has the first and not the second. Neither half alone is the answer.

**A ratchet covers shrink only.** Over a strict subset it still reports `sampled-domain` for the members it never listed, because pinning two of three says nothing about the third. Suppressing that would make the marker a laundering channel — the escape hatch these notes criticise `via guard` for being in coherence. It was one: until 2026-08-25, `# totality: ratchet` over two of three members silenced the report entirely and checked nothing about the third. Caught by an adversa