Record forge operator-independence and exit invariants #94

Open AtlantisPleb opened this 23h ago 1 comment

Outcome

State the forge's current single-operator trust boundary and add executable invariants for export, independent verification, mirror recovery, and operator exit.

Current behavior

The forge is canonical and MirrorWatch maintains GitHub as a read-only mirror, but the path from one operator to independently recoverable source and receipt history remains partly operational knowledge. Episode 267 records the same honest caveat for the relay.

Source: docs/episode-triage.md, episodes 266, 267, and 272.

Contract

Document which operator can accept pushes, promote deployments, issue credentials, and publish receipts.
Define export formats for repositories, issues, projects, attachments, identities where portable, and all receipt families.
Let an independent verifier check push, build, release, deployment, and accepted-outcome receipts without production database access.
Define restoration from the durable forge WAL and exported metadata on a clean operator environment.
Preserve GitHub as a mirror, never as hidden authority.
Define key rotation, operator loss, mirror divergence, and partial-export behavior.
Add invariant IDs and executable proofs to INVARIANTS.md.

Acceptance criteria

A documented rehearsal restores one repository and its bounded work history from exported artifacts.
An independent process detects a forged, missing, reordered, or mismatched receipt.
Operator loss does not require treating GitHub as canonical.
Private repository exports remain encrypted and access controlled.
Status and incident surfaces disclose degraded independence honestly.

Verification

Run export, clean restore, signature verification, mirror divergence, key rotation, private-data, and partial-failure rehearsals. Add the proofs to the documentation gate and run mix precommit.

Dependencies

Coordinate current forge WAL, MirrorWatch, deployment receipt, and project 3 linkage work.

AtlantisPleb opened this issue 23h ago

A AtlantisPleb Author 5h ago

Landed in 0fd32dd. Leaving this open: four invariants are in, and several acceptance criteria on this issue are not met, so closing it would overstate what holds.

What landed

docs/forge-operator-independence.md states the single-operator trust boundary without softening it. In summary: operator identity is an allowlist of GitHub numeric IDs, one hardcoded and the rest from an environment variable, with no role table, no scoped operator, and no separation of duties. A single static forge operator token authorizes read and write on every configured repository with no membership check and no protected-branch check, and pushes made with it record the principal operator:forge-token, so they are not attributable to a person. OpenAgentsWeb.AdminRecordingController unseals and streams any account's call recording. There are no encrypted Ecto column types anywhere: issue bodies, comments, messages, repository metadata, and every receipt family are plaintext in PostgreSQL, and the three hand-rolled vaults take their keys from the operator's own environment. Git objects are unencrypted on the node partition and in the WAL. No operator read is audited. Nothing in this codebase constrains the operator from the users of their own forge; what the invariants add is the ability to find out, not a constraint.

Invariants

ID	Property	Proof
`EXIT-001`	The export ledger matches the surface in both directions	`test/openagents/data_rights/export_inventory_test.exs`
`EXIT-002`	Served state is checkable against the WAL with no database	`test/openagents/forge/independence_test.exs`
`EXIT-003`	Recovery comes from the WAL; the mirror is strictly lossy and never an input	`test/openagents/forge/independence_test.exs`
`EXIT-004`	A clone is complete and self-hosting	`test/openagents/forge/independence_test.exs`

EXIT-001 is a ledger rather than a portability claim, because export is materially incomplete and an invariant asserting otherwise would pass vacuously. OpenAgents.DataRights.ExportInventory derives its coverage from OpenAgentsWeb.ApiRouteAuthority.families/0, so a new resource family cannot reach /api/v3 without someone deciding whether a user can export it. It proved that immediately: a rebase brought in the fleet_target family and the proof went red until it was classified.

Fourteen mutations, each confirmed to fail the intended test

Dropping the extra-ref direction of the ref comparison; skipping the entry digest comparison; disabling the sequence check; making the verifier query PostgreSQL; widening exportable_refs/1 to withhold nothing; adding a mirror call to the rebuild path; making reconcile_receipts/1 stop deriving from the WAL; copying the WAL alongside the mirror push; hiding a branch from clones; four ledger edits (a false portable claim, a false blocked claim, a dropped family, a portable claim with no proof); and one real surface change — widening Issues.get_issue_by_path!/3 to reach private repositories, which turned the ledger red with comment: the ledger records :blocked but the surface is :portable.

What is not true, and is now recorded

Export is incomplete. Six families — comment, label, milestone, assignee, issue_label, issue_assignee — resolve the repository through a public-only query, so a private repository's own owner gets 404 and a bearer token does not widen it. #142.
No account-scoped export exists for forge-owned or forum-owned data. Forum posts, deployments, agent links, Box leases, paired computers, and every receipt family have no export artifact, and push receipts have no published route at all. There is also no cross-repository read anywhere. #143.
Verification is tamper-evident, not tamper-proof. WAL entries are unsigned and the index is anchored nowhere outside operator storage, so a consistent rewrite of an entry, its key, and the index verifies clean. #151.
ADMIN-001 understates the operator surface. It states that no routed controller returns recording audio, and OpenAgentsWeb.AdminRecordingController is routed at GET /admin/recordings/:id/audio. It also frames the forge promote as the one operator write, and several others exist. #146.

Acceptance criteria still open on this issue

Private repository exports are not encrypted; the export paths that exist are plain JSON over an authenticated route, and repository content is not encrypted at rest by the application. Stated in the document rather than claimed.
Status and incident surfaces do not disclose degraded independence. OpenAgents.Forge.MirrorWatch publishes mirror freshness, and nothing surfaces the verification state or the export gaps.
Key rotation, operator loss, and partial-export rehearsals are undocumented. EXIT-003 covers recovery from the WAL and what the mirror cannot give back; it is not a rehearsal runbook.
No documented rehearsal restores a repository and its bounded work history from exported artifacts on a clean operator environment. EXIT-004 proves a clone re-serves with the forge deleted, which is the source half only.

POOL_SIZE=8 MIX_TEST_PARTITION=lane94 mix precommit passed: 3357 tests, documentation check on 92 files, reference check clean.