Declaring Invariants

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 (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

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:

* 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 adversarial pass on this skill, not by its own tests.

claims.py — what the repo declares

totality_lint asks whether a test's domain is complete. It presumes a test exists. This asks the prior question, the one coherence's own Known Limits concedes it does not answer: nothing enforces exists ⇒ declared.

A claim is a test whose docstring opens with invariant:. No new file format, and the claim inherits its test's pass/fail:

def test_every_skipped_directory_is_actually_skipped(self):
    """invariant: every name in SKIP_DIRS is excluded from the walk.

    refuted: replaced the walk's `part in SKIP_DIRS` check with
    `part in {"node_modules"}` -> this test went red naming `.coherence`,
    while the other 25 tests in this file stayed green.
    """

A claim whose test carries a ratchet marker is reported as pinning its registries rather than copying them, and a ratcheted registry is not unanchored.

python3 scripts/claims.py <repo> [--json] [--strict] [--selftest]

Write the refutation from what you observed

refuted: is the half that costs something. Break the chokepoint, watch the claim go red by name, restore, and record what you saw. A green test and an unfalsifiable one look identical from outside; the refutation is what separates them.

Never write a refutation you have not run. The first refutation authored for the SKIP_DIRS invariant above asserted a failure that did not occur — the fixture placed the registry outside the test's reachability, so the test passed under perturbation for an unrelated reason. A vacuous claim, written while building the tool that catches vacuous claims, and caught only by running the perturbation instead of trusting the sentence.

Procedure, in order:

1. Break the chokepoint the claim names, with one edit in the source rather than in the test.
2. Run the claiming test. Read the failure text. Note the member it named.
3. Run the rest of the file. Confirm the others stay green — if everything goes red, the claim is not localised and the refutation says nothing.
4. Restore the source.
5. Write refuted: <the edit> -> <what went red, by name>.

Wiring it into a commit gate

The reference wiring lives in oaustegard/claude-workspace (scripts/tdd_hook.py): a commit where a registry gained a member and no invariant: test iterates it live is denied, naming the registry and what it gained. Override with no-invariant: <why> in the commit body.

Registry shrink is gated the same way, and needs a ratchet rather than an enumeration to clear it. A new function or a new branch is behavioural growth too, but neither is diffable without guessing, and a gate that guesses stops being consulted. A brand-new registry is not gated. Declaring one is a judgement call; growing one has already made it.

Where the two filters came from

Both filters exist because the unfiltered version was noise. Reproduce either by removing the filter and re-running against a real repo.

• no-floor fires only on a name independently recognised as a registry. Firing on every for x in <local> produced 27 findings on remex, all noise: numpy arrays, query matrices, loop counters.
• A literal matches a registry only when reachable — the test imports its module or package, shares its top-level directory, or is its paired tests/test_<mod>.py. Matching against any registry in the tree joined a test in discrepancy/ to registries in kb-k-sweep/ and remex-vs-higgs-ablation/ on a monorepo, because small integer sets collide by chance. Four findings became one, and the survivor was real.

The join key is membership, not names: [1, 2, 3, 4, 8] and SUPPORTED_BITS share no token, so containment is what ties them together. No naming convention is assumed, and none is required.