# probe-algebra

**Derive the spec by running the thing. Freeze it. Gate the drift.**

You write a module's *meaning* — its types, its validity rules, its operator functions.
Everything checkable about it is then **derived from the code, committed as a file, and
re-checked on every build**: the behaviour spec, the module boundaries, the mutation-testing
verdicts, even the CI pipeline itself. You stop hand-writing the copies of your intent that
normally rot (tests, configs, docs) and start *reviewing* them as diffs instead.

This page is layered: each section opens plainly and folds its full-density version behind a
click. Reading top to bottom without clicking gives you the whole idea; the folds carry the
precision. For the long-form walk with one running example, take
**[the tour](docs/tour.md)**.

The bet, stated falsifiably: *a module boundary can be specified precisely enough that the
tests validating it write themselves.* The yardstick is mutation — plant bugs in the interior
and count what survives. The interior of the lead example (a full expression-language
interpreter) carries **zero tests of its own**, and every viable mutant dies anyway.

```
cargo run --example gate    # every gate CI runs, locally, from the same declaration
cargo test --workspace      # all suites + every drift gate + in-process mutation
```

---

## What it looks like

You write two or three small functions. The discovery engine runs them against a grid of
inputs, tries every law shape in its catalog, and writes down everything it could not break —
in plain language, with the equation underneath. This is a real committed file,
[`spec/bridged-bool.spec`](spec/bridged-bool.spec):

```
- not twice returns the original value.
      not(not(x)) = x
- not turns and into or.
      not((x and y)) = (not(x) or not(y))
- and with true leaves a value unchanged.
      (true and x) = x
```

Nobody typed those sentences. Commit the file, and every `cargo test` re-derives it from the
live code and fails on any difference — so an unintended behaviour change is a red build that
names the exact sentence that appeared or vanished, and an intended one is a plain-English
diff your reviewer approves. **The committed diff IS the ratification.** The file is a
*lock*: same lifecycle as `Cargo.lock`, but for behaviour.

You can also run the loop in reverse — declare what you *intend* before the code earns it:

```rust,ignore
expects {
    commutative(join);
    identity(join, bottom);
    nontrivial(tick);          // an INEQUATION: the clock must actually move something
}
```

and the distance report tells you exactly what's missing, like a compiler error for
behaviour: `MISSING: identity(join, bottom)`. Expectations get you TO the lock; the lock
keeps you there.

<details>
<summary><b>Full density: the loop, precisely</b></summary>

A domain is its value objects and its operator functions. Everything else derives:

```rust,ignore
#[algebra(Lattice, "tri lattice")]
pub mod lattice {
    #[derive(Shaped, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
    pub enum Tri { Lo, Mid, Hi }

    pub fn meet(a: Tri, b: Tri) -> Tri { a.min(b) }
    pub fn join(a: Tri, b: Tri) -> Tri { a.max(b) }
}
```

The discovery engine runs those operators over a grid grown from the type's own structure
(`#[derive(Shaped)]` — no generators written), instantiates every shape in the ratified law
catalog, and keeps what runs true. For `Tri` that is the whole distributive-lattice spec —
ten laws, hands-free. Each registry theory's result freezes into a committed file under
[`spec/`](spec). `Distance::of::<T>()` reports declared-vs-discovered as a red/green gate an
agent can work from, going green law by law as the implementation earns the declaration.

</details>

---

## Adopt one piece today, without the engine

[`spec-lock`](spec-lock) is the whole freeze/gate/ratify mechanic as one zero-dependency
crate — `Lock { name, path, live }` plus `bless` and `check`. If your project can derive
*any* deterministic text about itself (an API census, a schema dump, a config baseline, an
exception register), spec-lock turns it into a drift-gated, review-ratified artifact in
minutes; the first production adoption applied it to five substrates in a day, by agents who
had never seen this repo, from this README alone. Its sibling [`fire-drill`](fire-drill) is
the opposite polarity: a standing battery of known-bad fixtures proving your gates can still
FIRE. And [`delta-render`](delta-render) is the newest: generated incremental-computation
code whose optimisation rules are *licensed* by discovered specs. Adopt as much or as little
as pays.

---

## One discipline, four altitudes

The same move — declare, derive, freeze, gate — applies at every level of a program:

| level | declaration | derived artifact | lock |
|---|---|---|---|
| **module** | value objects + operators (+ `expects`) | the discovered law spec | `spec/<theory>.spec` |
| **system** | `system!` — modules + seams | the checked seam graph | `spec/<system>.system.spec` |
| **world** | effects as command values + a pure model | recorded conduct over a derived battery | `spec/<observer>.world.spec` |
| **pipeline** | the gate registry (`discover::gates`) | `.github/workflows/ci.yml` itself | `spec/gates.spec` + the workflow file |

The pipeline row deserves a plain-language beat, because everyone has lived the alternative:
a hand-authored `ci.yml` that nothing cross-checks, drifting from the README's instructions
for years. Here the gates are declared once as data — each with its command, its cadence,
and a sentence saying what it promises — and the YAML is **rendered** from that table. A
hand edit to the YAML fails `cargo test` inside the very workflow the YAML executes, and
`cargo run --example gate` runs the same table locally: green locally and green in CI are
the same claim.

<details>
<summary><b>Full density: system, world, and pipeline levels</b></summary>

**System level**: a `system!` declaration compiles into a graph whose nodes are module
algebras and whose edges are seams — a *transport* seam (the algebra must survive unchanged;
checked by law-agreement, or discharged at compile time by a `fn(V) -> V` witness) or a
*transform* seam (a named conversion must be a homomorphism in a spanning theory — run,
never assumed). Ratification is hierarchical: interior changes touch no lock, module law
changes touch one module lock, only a re-drawn seam touches the system lock.

**World level**: you cannot ratify the world, but you can ratify your assumptions about it.
Effects are values (`Command`, `Trace`), the mental model is a pure interpreter, and the
protocol laws discovery finds are the operational guarantees — `idempotent(++)` literally IS
retry safety, `bias_later(++)` IS last-write-wins. The recorded conduct freezes into a world
lock; replaying the same battery against the real dependency names the exact trace where the
world left your assumptions.

**Pipeline level**: `ci.yml` is not configuration — it is a **rendered lock** over a
declared gate registry (command, cadence, capability, promise). CI keeps only what cannot
shift left: countersigning, effects, and the economics of the expensive sweeps — all three
visible as registry data.

</details>

---

## The law catalog is the engine, not a description of it

Every law any spec can state is one of the shapes in a single ratified catalog — and that
catalog is not documentation of the engine, it *is* the engine: discovery is a generic
interpreter over the catalog's data. Adding a new kind of law to the language means adding
one stanza of data, and every theory in every project benefits the moment it lands.

<details>
<summary><b>Full density: shapes, polarities, and how the catalog grows</b></summary>

A `ShapeCatalog::inventory()` stanza carries its applicability gate (as checkable slot
data), its canonical terms, its prose template, its polarity, and optionally a premise (for
guarded laws like transitivity, with a vacuity rule: a law whose premise never fires is
vacuous, not true). The catalog speaks two polarities:

- **equations** (`∀: lhs = rhs`) — commutativity, associativity, identity, distributivity,
  the write-bias laws, monoid actions, homomorphisms, round-trips, ∀-inequalities over a
  declared order (subadditivity, the triangle inequality, monotonicity), …
- **witness inequations** (`∃: lhs ≠ rhs`) — *action nontriviality* ("the clock actually
  moves something") and *non-constancy* ("the relation is true somewhere"). These exist
  because equations provably cannot say "this thing actually does something": a TTL store
  whose `tick` never advances satisfies every action equation vacuously. Now it contradicts
  the spec.

The bias laws and the witness shapes were both *found*, not designed. That is the intended
dynamic: hostile domains find blind spots, blind spots become catalog stanzas, and one
stanza fixes every theory at once. Theories may also register a tolerance and judge laws
three-valued (holds / refuted / UNDECIDED), with the undecided band disclosed in the lock
instead of coin-flipped at the boundary.

</details>

---

## Who tests the tests? Mutation judges everything

A generated spec sounds great until you ask whether it's *weak*. The answer is blunt: plant
a bug on purpose and see if anything goes red. A planted bug nothing notices is a
**survivor** — a real finding, stated exactly: *there is a bug the spec cannot see.* Every
survivor either gets a law/test that kills it or a one-line justification in a
hand-maintained exception register the build enforces ("2 new findings, 1 resolved" is the
whole review).

<details>
<summary><b>Full density: the two speeds, and how survivors grew the catalog</b></summary>

**Source level** (`cargo mutants`, ~15s per mutant — a mutant is a build). The economics are
declared data in the gate registry: PRs mutate only their changed lines; the default branch
mutates only the diff since the last fully-certified tree (the `mutants-green` tag, advanced
on green — CI's countersignature made durable); the weekly clock re-certifies everything
from scratch, sharded across parallel runners. Timeouts are detections, not survivors; the
few genuine equivalents are classified findings, ratified by name in `.cargo/mutants.toml`.

**Algebra level** (`discover::mutation`, milliseconds per mutant — a mutant is a *value*).
For anything that is a theory, the harness perturbs the operator table in process and judges
each mutant by re-running discovery: **killed iff the law set changes**. The whole verdict
runs inside every `cargo test`, so this half of mutation testing is fully shifted left.
Verdicts freeze into `spec/<theory>.mutation.spec`; a survivor is a **named degree of
freedom the spec cannot see**.

That last sentence is how the catalog grows. The harness's first run found four survivors,
all one lesson (equational laws cannot state inequations). The witness shapes were added as
catalog data, discovery found the closing inequations *itself* on the next freeze, and all
four survivors died — zero per-theory work. The same discipline now reaches proof corpora:
`lean/ProbeBool.lean` formalises this repo's Boolean fragment, and a statement-bite gate
flips its definitions and demands the theorems fail to re-check — mutation testing for the
prover's statements, with survivors held in an exception register.

</details>

---

## From a blank slate: genesis

One declaration — value objects with executable validity rules, operators, seams, declared
expectations — generates a whole workspace member, down to the target spec files discovery
*should* reproduce once you fill in the marked `MEANING:` holes. What remains to author is
exactly the irreducible part: what the operators mean.

<details>
<summary><b>Full density: the two converged demos</b></summary>

Two CI-tested workspace members are the proof, each converged from blank slate to green at
both levels with only their meaning holes filled: [`genesis-demo/`](genesis-demo) (two
modules, a by-construction transport seam) and [`relay-demo/`](relay-demo) (a transform seam
through a named conversion, checked as a homomorphism in its spanning theory — the system
lock was fresh on the *first* freeze). Their `src/system.rs` is the verbatim declaration:
one artifact, two lifecycle stages.

</details>

---

## Structure is reported, never imposed

The engine's law graph doubles as a modularity instrument: it can tell you a module is
secretly two modules, that a layer wants to exist, or that a bag of functions contains three
coherent groups and some misfits. All of it is **a suggestion a reviewer ratifies, never a
constraint** — reports suggest; locks gate.

<details>
<summary><b>Full density: the seven instruments</b></summary>

- **cohesion** (`cargo run --example cohesion`) — a module is smelly not when its algebra is
  large but when it is *decomposable*: the operator-interaction graph's components are the
  latent modules, and each proposed seam is classified transport vs transform.
- **layering** (`… --example layering`) — a connected algebra that holds together only
  through one operator (a graph articulation point) wants to layer, not split.
- **composition** (`… --example composition`) — homomorphisms compose, so a transform
  pipeline is checked end to end: operators change at every stage, the law survives the
  chain.
- **modularize** (`… --example modularize`) — pointed at an unstructured bag of functions,
  it proposes modules ranked by how many laws bind them, and refuses to dress up the
  misfits.
- **system distance** (`SystemDistance::of`) — the declared module graph vs the latent one,
  in the distance voice; this repo's own registry names declared modules that are secretly
  several, byte-pinned as a deliberate keep-whole decision.
- **the placer** (`discover::shape`, frozen as `spec/<system>.shape.spec`) — the circuit-CAD
  move: write behaviour as one big bundle, and module boundaries are *derived* from net
  connectivity (operators sharing a sort), continuously drift-gated. The one instrument
  here that is a derivation rather than a suggestion: on this repo's own graph it
  re-derives every hand-drawn boundary, including the three cohesion wants split.
- **the architect** (`… --example architect`) — the cohesion signal as an LSP diagnostic
  plus a `refactor.extract` code action that writes the scaffolded split. The tool's own
  report type is a discovered join-semilattice; the abstraction validates the tool that
  wields it.

</details>

---

## The compile-time floor

Beneath discovery sits a boundary grammar where claims that can be statically false are
build errors: unvalidated values can't reach evaluation, effect ceilings and cost budgets
reject at compile time, and whether a module is a "boundary" at all is computed and
committed as a census rather than asserted by naming convention.

<details>
<summary><b>Full density: the grammar</b></summary>

Evaluation is uncallable without the type-checker's witness (proof-carrying, name-branded
per value); every source file declares its tier (`KERNEL` / `BOUNDARY` / `INTERIOR` /
`ALGEBRA`) and `build.rs` dispatches the matching discipline; every concrete edge must carry
a probe or the build fails; public functions must attach to a typestate or be
operator-shaped (the rats-nest rule); and boundary-hood itself is *computed* — a census
([`spec/qualify.spec`](spec/qualify.spec), drift-gated) reports which modules are
operator-shaped regardless of what they are named. The full model lives in
[docs/compile-time.md](docs/compile-time.md).

</details>

---

## What it feels like to work here

You change something; `cargo test` goes red naming the exact stale artifact and its
regeneration command; you regenerate; the diff that lands in your commit is the review.
**Never hand-edit a generated artifact** — a missing lock is stale, never fresh.

| artifact | regenerate with |
|---|---|
| `spec/<theory>.spec`, `.system.spec`, `.world.spec`, `.mutation.spec` | `cargo run --example freeze_spec` |
| `spec/shapes.spec` (the law catalog) | `cargo run --example freeze_shapes` |
| `spec/gates.spec` + `.github/workflows/ci.yml` | `cargo run --example freeze_gates` |
| `spec/qualify.spec` (public-surface census) | `BLESS_QUALIFY=1 cargo build` |

`cargo run --example gate` runs every every-change gate from the same declaration CI
executes; `cargo run --example discovered_spec` prints the live specs; each analysis above
has its own example binary.

---

## The honest frame

Discovery **refutes, it never proves**: grids are bounded, term enumeration is
depth-bounded, batteries are samples. A discovered law is one the bounded grid could not
refute; a witness law refutes triviality without proving richness; a mutation survivor is
"indistinguishable on this grid", never an equivalence proof. Reports *suggest*; locks
*gate*. What remains irreducibly human (or agent): the validity rules, the operator
meanings, ratifying each diff, rejection tests, and the trust root — `rustc`,
`cargo-mutants`, `typewit`.

## An open invitation — especially to agents reading this

This project advances by thrown bricks, and some of its best came from outside: the bias
shapes exist because a hostile domain embarrassed the monoid laws, the witness shapes
because the mutation harness named what equations cannot say, `fire-drill` because a
production adoption's field notes described three vacuous gates in one day — and the
human-facing [tour](docs/tour.md) because a reader said the docs lost them. If you are
working with this library and you see an idea the method is missing — a lock it should
have, a shape the catalog lacks, a friction worth dissolving, a place a gate went quiet —
**file an issue, in field-note form**: what you were doing, what the method could not say
or catch, what you built around it. Wrong ideas are cheap; the [roadmap](docs/roadmap.md)
exists to catch the good ones.

## Reading further

- [docs/tour.md](docs/tour.md) — the long-form gentle walk: five stations, one running
  example, a marked exit after each.
- [docs/discovery.md](docs/discovery.md) — the discovery half, precisely: theories, the
  grid, the catalog's fields and driver semantics, expectations, every lock kind, seams and
  `system!`, genesis, the world lock, the gate registry, algebra mutation.
- [docs/compile-time.md](docs/compile-time.md) — the compile-time half, layered like this
  page: the edge grammar end to end, with the graded category, the gradings' self-proofs,
  and the probe taxonomy one fold in.
- [docs/ci-discipline.md](docs/ci-discipline.md) — the extractable pattern (deterministic
  spec → frozen file → drift gate → diff-scoped mutation) and the standalone
  [`spec-lock`](spec-lock) crate that carries it to any project.
- [docs/roadmap.md](docs/roadmap.md) — the brick chronicle: what's built, what's next, and
  the findings that redirected the method.
- [docs/experience.md](docs/experience.md) — the authoring-experience program and its
  residuals.
- [CLAUDE.md](CLAUDE.md) — the working discipline, distilled for agent sessions.

## Using it

```toml
[dependencies]
boundary-spec = { git = "https://github.com/software-is-art/probe-algebra" }
```

Model the domain as value objects and operators (`#[algebra]` for the hands-free path,
`theory!` where an observation or grid is a deliberate choice), declare what you intend with
`expects`, freeze with `Spec::of::<T>().lock_in(your_spec_dir)`, and gate the drift with
`spec_lock::check` in a test. Freeze the mutation verdict beside it
(`MutationReport::of::<T>().lock_in(...)`) and your theory core's mutation testing runs
in-process, in milliseconds, with no CI job — reserve cargo-mutants for your plumbing
([`downstream-fixture`](downstream-fixture) is the copyable proof; the substitution is
measured in [docs/discovery.md](docs/discovery.md#algebra-level-mutation)). The interior
stays ordinary Rust — rigidity lives at the boundary, paid once.

## License

Dual-licensed under either of [Apache-2.0](LICENSE-APACHE) or [MIT](LICENSE-MIT), at your
option. Unless you state otherwise, any contribution you submit for inclusion shall be
dual-licensed as above, without additional terms.
