Invariant conformance

SYNAPSE CHANNEL maintains a machine-checked conformance registry for six coordination boundaries. It is a proof map, not a certification badge: each row names its exact normative invariants, implementation files, executable evidence, scope, and residual limitations.

The current programme status is partial. Two bounded guarantees conform and four remain partial. The generated invariant_conformance.json is suitable for automation; tools/invariant_conformance.toml is its canonical source.

Boundary	Status	Current truth
Single authority	Conformant	One hub authority domain prevents overlapping ownership; federation does not merge authority.
Immediate-effect fencing	Partial	Hub-mediated epochs and versions fence stale mutations, but direct external effects are outside that boundary.
Atomic operation truth	Partial	Claim-family operations commit before publication and apply once; this is not yet universal.
Content-bound global event identity	Conformant	A federated identity binds one fingerprint; equivocation quarantines before publication.
Causal conflict handling	Partial	Equivocation fails closed and divergent task snapshots produce payload-free unresolved conflict objects, but task events do not carry causal parents.
Evidence completeness	Partial	Defined journal, receipt, AEF, and quarantine evidence exists, but coverage is not universal.

python tools/invariant_conformance.py --check validates the schema, exact six-row set, cited invariant identifiers, public evidence paths, and generated output. This freshness check runs before commit and in reserved release preflight. --enforce is intentionally red until every row is truthfully conformant; it prints every incomplete boundary and exits non-zero.

Ordinary line or branch coverage cannot close a boundary by itself. The registry links state-machine exploration, kill-point fault injection, multi-process races, restart and concurrency probes, adversarial inputs, and receipt/replay tests where those modes apply. A status changes only when both the normative guarantee and its hostile executable evidence change together.

The single-authority race evidence includes two independent Python client processes released through an on-disk barrier against one live hub. Concurrent takeovers must produce exactly one 4010-superseded process, one surviving process, and one final socket-to-identity binding.

Partition evidence is similarly explicit. A contested namespace refuses local grants; partition and verified-heal transitions are durable; failed or partial poll rounds retain suspicion; restart restores the last proven contest; and an observed release heals only after a successful round. These tests prove safe partition containment and recovery, not causal ordering of the display fold.

The observed task-board fold also retains the latest snapshot from each authoring hub. If those complete records diverge, JSON and text surfaces expose one bounded, payload-free conflict object with each contender's hub, sequence, timestamp, and record fingerprint. Equal snapshots converge without a conflict, and later equal snapshots clear the divergence. This makes disagreement visible without leaking the losing task record or choosing an authoritative winner. It is not a claim that the snapshots were concurrent: task events do not yet carry a causal parent or vector clock, so the boundary remains partial.

The randomized state machine is complemented by python tools/exhaustive_coordination_model.py --depth 4. That deterministic bounded explorer enumerates every trace over thirteen real claim, overlap, cross-worktree, renewal, handoff, release, stale-fence, update, and expiry actions. It drives SynapseState directly and checks the named mutual-exclusion, epoch, lease, version, and handoff invariants after every transition. Its result is bounded evidence, not a claim about unbounded state space.