Report the gap between a proven invariant and a deployed one #246

Closed AtlantisPleb opened this 5d ago 1 comment

Evidence

Shipped in the release at 0bf2706, promoted 2026-08-27.

1 pushes receipt

What happened

#187 was one cause behind six separate live failures: main held the EXIT-001 account export, the EXIT-004 graft reconciliation, the EXIT-005 chain, and the EXIT-006 disclosure, and the deployed revision did not. Every invariant was green the whole time, because an invariant reads the compiled modules of the node running the test suite, not the ones running the forge.

The gap was found by a person performing #180's rehearsals by hand and checking six surfaces one at a time. Nothing reported it. The release that closed #187 removes today's gap; it does not remove the next one.

What to build

Something that reports the distance between the revision the invariants were proven against and the revision the forge is serving, without anyone rehearsing to find it.

The forge hosts its own repository, so the comparison needs no outside service: OpenAgents.BuildInfo.revision/0 is the running revision, and the bare projection for OpenAgentsInc/openagents.com holds the head of refs/heads/main that the same forge serves.

What makes this harder than it looks

EXIT-006 is the obvious home and its proof forbids the obvious payload. The disclosure publishes counts, booleans, family names, issue numbers, and one document path, and test/openagents/forge/independence_disclosure_test.exs turns red when a repository path, an account id, a node name, or a commit sha reaches the projection. One of the six mutations that proof was confirmed against was adding the forge's repository name. A distance is a number and fits; the two revisions it is a distance between do not.

STATUS-001 also treats the published key set as a decision to be asked for rather than an accident, so adding a section to independence is a ledger amendment, not an implementation detail.

Acceptance criteria

A gap between the proven revision and the deployed revision is reported somewhere a person or a check reads without performing a rehearsal.
The report is derived from the running node rather than restated, in the way every other claim in OpenAgents.Forge.Independence is derived.
Whatever surface carries it names its bound: a forge that will not serve its own repository reports nothing here either, and that is the same withholding EXIT-005 and EXIT-006 already decline to detect.
The ledger entry and the proof move with the published key set.

Found by: #187's close, docs/forge-exit-rehearsals.md.

AtlantisPleb opened this issue 5d ago
AtlantisPleb closed this as completed in 0aa6cde 5d ago
A AtlantisPleb Author 5d ago

Landed as 0aa6cde on main.

OpenAgents.Forge.Independence now publishes its own distance from the revision its proofs ran against. /api/status and /status carry independence.deployment: proven_ref (refs/heads/main), known, and behind — the number of commits on the head this node serves that the running revision does not carry. The status page renders it in words, so a person reads "26 commits behind refs/heads/main; an invariant proven there is not proven here" without rehearsing a single exit surface.

Why EXIT-006 did not have to move to accommodate it. The proof forbids a commit sha reaching this projection, and adding the forge's repository name was one of the six mutations it was confirmed against. That rule is untouched. A distance is a count and fits under it; the two revisions it lies between do not, and they are not published. Three further mutations were confirmed and reverted: publishing the running revision beside its distance (caught by the vocabulary assertion and both STATUS-001 key-set assertions), hardcoding the distance to zero (caught by the seeded-repository counts and, independently, by the compiled-import-table read), and dropping the section (caught by STATUS-001's stale-key assertion).

Derived, not restated. The running revision is the one /api/status already publishes for this node. The proven revision is refs/heads/main in the bare projection this forge serves of its own repository — RELEASE-004 binds the proof matrix to the exact candidate sha and .githooks/pre-push refuses a push without it, which is what makes that head the newest proven revision. The distance is git rev-list --count over objects already on disk. No outside service is asked.

Its bound, named. The claim is not "how far behind main this forge is": nothing on this node can see a main it declines to serve. A forge that will not serve its own repository, an empty bare projection, and a release built from a revision this forge never accepted all report known: false and no distance at all — the same withholding EXIT-005 and EXIT-006 already decline to detect. Being behind is also not an axis of degraded?, and that is deliberate and recorded: a node one commit behind is not less independent, and folding ordinary deploy lag into the independence verdict would make that verdict mean nothing on the day it mattered. The distance is published beside the verdict, as its margin of error.

STATUS-001 and EXIT-006 record the decision, and the published key set moved with the claim as STATUS-001 requires. docs/forge-operator-independence.md and docs/forge-exit-rehearsals.md record what it still does not do.

What it does not do, and what is true right now. It reports; it does not act. Nothing raises an incident when the distance grows — a reader or a check has to look. And the live forge is still serving 46cf8a5a, 26 commits behind this commit, so it does not carry this section yet; promotion is an operator act. The first thing this section will say when it is promoted is how far behind the node that runs it was.