that constraint instead, and a fifth role fails until someone says whether it

reads.

Amended 2026-08-23 (issue #185): the one instance of that residue is closed.

`OpenAgents.DataRights.AccountExport`'s push-receipt and deployment joins used

to select a repository's `owner` and `name` with no predicate at all, so an

export named the current owner and name of a private repository the account had

been removed from, or of one renamed after they left. All three now join the

same `readable_by/2` subquery the module's `repository_work_export/1` composes,

and the module states one rule for all four collections that render a path: a

repository's current owner and name travel only where the predicate admits the

repository to that account. What the rule does to the record differs by family

and is stated rather than left to each query — an account-keyed record survives

with a null repository, because a push receipt is the account's own evidence

under `EXIT-005`, and a repository-keyed record under `repository_work` is

withheld entirely, because it has no meaning apart from its repository.

`OpenAgents.DataRights.AccountExportTest` proves both halves for each

collection.

What is still not enumerated: a listing that applies no predicate at all names

no term and calls no resolver, so it passes every test above.

`OpenAgents.DataRights.AccountExport`'s push-receipt and deployment joins are

that shape — each is scoped to the acting account's own rows, and each selects

a repository's `owner` and `name` without the predicate, which the same

module's `repository_work_export/1` explicitly applies.

no term and calls no resolver, so it passes every test above. Closing the one

instance does not close the class — a predicate-free listing added tomorrow

would still pass every test here, and only a reader would catch it.

`docs/2026-08-23-invariant-proof-audit.md` records the residue.

Reading across repositories obeys the same rule as reading one: the

this account can read never appear. Dropping the `readable_by` join turns the

first red while every other assertion still passes.

Amended 2026-08-23 (issue #185): a repository's current owner and name are the

repository's rather than the account's, and the export applies one rule to all

four collections that render a path. `push_receipt`, `deployment` request, and

`deployment` approval are keyed on the account, so the record comes back

whatever the repository says now — with `"repository": null` where

`readable_by/2` no longer admits it, keeping the `storage_key`, `wal_seq`, and

refs an `EXIT-005` chain link needs. `repository_work` withholds the record

instead, because a pull request separated from its repository is not a record

an account can use. Nothing moves off `portable`: an account still gets every

record it authored, and what it stops getting is a name that was never its

own. The document says so in its own `not_included` section under the family

`repository_identity`, so a recipient reading the file offline is not left to

infer why a receipt names no repository.

Ownership of a migrated forum post is decided, not guessed. Two identities

resolve to an account and no third: `user:<account-id>`, which every topic and

post written on this surface carries, and any `actor_ref` the account holds a

| STATUS-001 | `test/openagents/network_status_test.exs`, `test/openagents_web/live/network_status_live_test.exs` |

| CAPACITY-001 | `test/openagents/capacity_test.exs` |

| TRANSPARENCY-001 | `test/openagents/forge/visibility_test.exs`, `test/openagents/forge/browse_test.exs`, `test/openagents_web/live/code_live_test.exs`, `test/openagents_web/transparency_surface_test.exs` |

| REPOSITORY-001 | `test/openagents/repositories/visibility_join_test.exs`, `test/openagents_web/live/computers_repository_access_test.exs`, `test/openagents/repository_lifecycle_test.exs`, `test/openagents/repositories/provisioner_test.exs`, `test/openagents_web/controllers/repository_controller_test.exs`, `test/openagents/issues_workspace_test.exs`, `test/openagents_web/live/issue_workspace_live_test.exs`, `test/openagents_web/live/project_workspace_live_test.exs`, `test/openagents/forge/git_http_test.exs` |

| REPOSITORY-001 | `test/openagents/repositories/visibility_join_test.exs`, `test/openagents/data_rights/account_export_test.exs`, `test/openagents_web/live/computers_repository_access_test.exs`, `test/openagents/repository_lifecycle_test.exs`, `test/openagents/repositories/provisioner_test.exs`, `test/openagents_web/controllers/repository_controller_test.exs`, `test/openagents/issues_workspace_test.exs`, `test/openagents_web/live/issue_workspace_live_test.exs`, `test/openagents_web/live/project_workspace_live_test.exs`, `test/openagents/forge/git_http_test.exs` |

| API-001 | `test/openagents_web/controllers/api_extension_governance_test.exs`, `test/openagents/issue_progress_test.exs` |

| CONTRIBUTION-001 | `test/openagents_web/contribution_contract_test.exs` |

| REPOSITORY-002 | `ops/ci/push-remote-check.sh`, `ops/dev/install-push-guard.sh`, `test/openagents/push_remote_contract_test.exs` |

**What is left.** A listing that applies no predicate at all names no term and

calls no resolver. `OpenAgents.DataRights.AccountExport`'s push-receipt and

deployment joins are that shape; each is scoped to the acting account's own

rows and selects a repository's `owner` and `name` without the predicate the

same module applies elsewhere. `REPOSITORY-001` records it.

deployment joins were that shape; each was scoped to the acting account's own

rows and selected a repository's `owner` and `name` without the predicate the

same module applies elsewhere. Issue #185 closed that instance: all three joins

now compose `readable_by/2`, the module states one disclosure rule for every

collection that renders a path, and

`test/openagents/data_rights/account_export_test.exs` reddens on each of them

when the predicate is dropped. The class stays open — a predicate-free listing

added tomorrow would still name no term and call no resolver — and

`REPOSITORY-001` records it.

### `RELEASE-004` — no hosted CI

  inside the document — a post to its topic, a tip to its post, an event to its

  thread — resolves inside the document itself.

  ## Repository names

  A repository's current owner and name are the repository's, not the

  account's. They travel in this document only where

  `OpenAgents.Repositories.readable_by/2` admits the repository to this

  account, and every collection that renders `owner/name` applies that one

  rule: push receipts, deployment requests, deployment approvals, and the

  four families under `"repository_work"`. A private repository the account

  was removed from, or one renamed after they left, does not tell them what it

  is called now.

  What the rule does to the record differs by family, and the difference is

  stated rather than left to each query. An account-keyed record survives with

  `"repository": null`: a push receipt is the account's own evidence — the WAL

  sequence and ref map a clone does not carry — and withholding it would cost

  the account its own history to protect a name it no longer has. A

  repository-keyed record under `"repository_work"` is withheld entirely,

  because a pull request separated from its repository is not a record the

  account can use.

  ## Repository-keyed work

  Pull requests, stacks, and issue dependencies key on a repository rather than

  # `forge_pushes.principal` is `user:<account-id>` for a person's push and an

  # operator or assignment string otherwise, so the account's own pushes are an

  # exact match rather than a guess.

  #

  # The receipt is the account's own and comes back whatever the repository

  # says now. The repository's current owner and name are not, so the join

  # goes through `readable_repositories/1` rather than straight at the table:

  # a receipt for a repository this account can no longer read arrives with

  # `"repository": null` and keeps its `storage_key`, `wal_seq`, and refs.

  defp push_receipts_export(user) do

    principal = account_actor_ref(user)

    readable = readable_repositories(user)

    receipts =

      Repo.all(

        from receipt in PushReceipt,

          left_join: repository in Repository,

          left_join: repository in subquery(readable),

          on: repository.storage_key == receipt.repo,

          where: receipt.principal == ^principal,

          order_by: [asc: receipt.inserted_at, asc: receipt.id],

  ## ── deployments ────────────────────────────────────────────────────────

  # Both reads are keyed on the account — the requester of a deployment and the

  # approver of one — so both records survive a lost membership. Both join

  # `readable_repositories/1` for the same reason the push receipts do: the

  # request is the account's, the repository's current name is not.

  defp deployments_export(user) do

    readable = readable_repositories(user)

    requests =

      Repo.all(

        from request in Request,

          left_join: repository in Repository,

          left_join: repository in subquery(readable),

          on: repository.id == request.repository_id,

          where: request.requested_by_user_id == ^user.id,

          order_by: [asc: request.requested_at, asc: request.id],

    approvals =

      Repo.all(

        from approval in Approval,

          left_join: repository in Repository,

          left_join: repository in subquery(readable),

          on: repository.id == approval.repository_id,

          where: approval.approver_user_id == ^user.id,

          order_by: [asc: approval.decided_at, asc: approval.id],

  end

  # A repository's identity comes back with the predicate rather than beside

  # it, so a caller cannot name a repository this query did not admit.

  # it, so a caller cannot name a repository this query did not admit. Every

  # collection that renders `owner/name` joins this one query — the four

  # repository-keyed families here, and the account-keyed push receipts and

  # deployments above — so the module cannot state one disclosure rule and

  # apply two. `storage_key` rides along because a push receipt names its

  # repository by that key rather than by `repository_id`.

  defp readable_repositories(user) do

    from repository in Repositories.readable_by(Repository, user),

      select: %{id: repository.id, owner: repository.owner, name: repository.name}

      select: %{

        id: repository.id,

        owner: repository.owner,

        name: repository.name,

        storage_key: repository.storage_key

      }

  end

  defp pull_requests_export(user, readable) do

        "mechanism" => "git clone with an oa_pat_ token",

        "issue" => nil

      },

      %{

        "family" => "repository_identity",

        "reason" =>

          "A repository's current owner and name appear only where the account can still read " <>

            "the repository. A push receipt, deployment request, or approval for a repository " <>

            "the account was removed from arrives with a null repository and keeps every field " <>

            "that is the account's own; a record under repository_work is withheld instead, " <>

            "because it has no meaning apart from its repository.",

        "mechanism" => "OpenAgents.Repositories.readable_by/2",

        "issue" => nil

      },

      %{

        "family" => "forum",

        "reason" =>

  import Ecto.Query

  alias OpenAgents.DataRights.AccountExport

  alias OpenAgents.Deployments.Approval

  alias OpenAgents.Deployments.Request

  alias OpenAgents.DeploymentsFixtures

  alias OpenAgents.Forum

  alias OpenAgents.Forum.{Post, TipDestination, Topic}

  alias OpenAgents.Forum.Forum, as: Board

  alias OpenAgents.PullRequests.PullRequest

  alias OpenAgents.Repo

  alias OpenAgents.Repositories

  alias OpenAgents.Repositories.Membership

  alias OpenAgents.Reputation

  alias OpenAgents.Stacks

  alias OpenAgents.Threads

    end

  end

  # The repository's current owner and name are the repository's, not the

  # account's, and `readable_by/2` is the only thing withholding them here:

  # each account gets these records back through a column naming it, so no

  # other gate stands between the export and the path. Replacing the

  # `readable_repositories/1` subquery with the repositories table turns every

  # assertion in this block red and nothing else in this file.

  describe "a repository the account can no longer read" do

    test "a push receipt keeps every field that is the account's own and loses the path" do

      user = github_user("account-export-push-gone", "export-push-gone")

      owner = github_user("account-export-push-owner", "export-push-owner")

      repository = private_repository_with_member("export-push-private", owner)

      {:ok, _membership} = Repositories.add_member(repository, user, "contributor")

      refs = %{"refs/heads/main" => String.duplicate("b", 40)}

      Repo.insert!(%PushReceipt{

        repo: repository.storage_key,

        wal_seq: 9,

        principal: "user:" <> user.id,

        refs: refs,

        duration_ms: 31

      })

      # While the account is still a member, the document names the repository.

      assert {:ok, before_removal} = AccountExport.build(user)

      assert [named] = before_removal["push_receipts"]["records"]

      assert named["repository"] == repository.owner <> "/" <> repository.name

      drop_membership!(repository, user)

      refute Repositories.member?(repository, user)

      assert {:ok, export} = AccountExport.build(user)

      assert [receipt] = export["push_receipts"]["records"]

      assert receipt["repository"] == nil

      assert receipt["storage_key"] == repository.storage_key

      assert receipt["wal_seq"] == 9

      assert receipt["refs"] == refs

      assert receipt["duration_ms"] == 31

    end

    test "a deployment request and an approval keep the record and lose the path" do

      user = github_user("account-export-deploy-gone", "export-deploy-gone")

      owner = github_user("account-export-deploy-owner", "export-deploy-owner")

      repository = private_repository_with_member("export-deploy-private", owner)

      {:ok, _membership} = Repositories.add_member(repository, user, "maintainer")

      _environment = DeploymentsFixtures.environment_fixture(repository, user)

      run = DeploymentsFixtures.run_fixture(repository, user)

      request = Repo.get!(Request, run.deployment_request_id)

      Repo.insert!(%Approval{

        repository_id: repository.id,

        deployment_run_id: run.id,

        approver_user_id: user.id,

        decision: "approved",

        rule: "manual",

        request_digest: request.request_digest,

        decided_at: DateTime.utc_now()

      })

      drop_membership!(repository, user)

      refute Repositories.member?(repository, user)

      assert {:ok, export} = AccountExport.build(user)

      assert [exported_request] = export["deployments"]["requests"]

      assert exported_request["repository"] == nil

      assert exported_request["commit_sha"] == DeploymentsFixtures.commit_sha()

      assert exported_request["request_digest"] == request.request_digest

      assert [exported_approval] = export["deployments"]["approvals"]

      assert exported_approval["repository"] == nil

      assert exported_approval["decision"] == "approved"

      assert exported_approval["request_digest"] == request.request_digest

    end

    test "the document names the rule it applies to a repository it will not name" do

      user = github_user("account-export-disclosure", "export-disclosure")

      assert {:ok, export} = AccountExport.build(user)

      assert gap =

               Enum.find(export["not_included"], &(&1["family"] == "repository_identity"))

      assert gap["mechanism"] == "OpenAgents.Repositories.readable_by/2"

      assert gap["reason"] =~ "null repository"

    end

  end

  describe "who a legacy forum post belongs to" do

    test "an unclaimed legacy identity does not export", %{board: board} do

      user = github_user("account-export-unclaimed", "export-unclaimed")

    }

  end

  # Membership is what `readable_by/2` reads for a private repository, so the

  # row goes rather than the repository: the account really did the work and

  # really cannot read where it landed.

  defp drop_membership!(repository, user) do

    {1, nil} =

      Repo.delete_all(

        from membership in Membership,

          where: membership.repository_id == ^repository.id and membership.user_id == ^user.id

      )

    :ok

  end

  defp private_repository_with_member(name, user) do

    repository =

      OpenAgents.AccountsFixtures.repository_fixture(%{name: name, visibility: "private"})