A retained name owes a population, and the population must be established from

something that cannot lie rather than from a reading of the call sites. The

retired AAD `sarah.machine_token.v1` had none — nothing seals a version-1 blob

and a sealed pairing token cannot outlive its bounded window — so the token

vault carries one version and one AAD. The audit actor kind `machine` looked

and a sealed pairing token cannot outlive its bounded window, which

IDENTITY-011 now enforces rather than assumes — so the token vault carries one

version and one AAD. The audit actor kind `machine` looked

the same and is not: a paired computer authenticating to the Git plane pushes

under `{:machine, id}`, from a variable that no source scan for a literal

finds. It stays, and the proof asserts that every principal kind

`test/openagents_web/controllers/computer_control_api_test.exs`, and

`test/openagents/inference/computer_revocation_test.exs`.

### IDENTITY-011 — A pairing window closes on its own clock

Status: Current

A computer pairing is a bounded window: the CLI registers it, the account owner

approves it in the browser, and the CLI claims the computer token exactly once.

`OpenAgents.Machines` seals that token at rest for the claim window alone, and

`OpenAgents.Machines.TokenVault` carries one version and one AAD on the

strength of that bound — CANON-002 states it as settled.

Nothing enforced it. `claim_pairing/2` expired an elapsed pairing, and that was

the only thing that ever did, so the window closed only when someone knocked on

it. A pairing the CLI stopped polling — killed, disconnected, or abandoned

after approval — stayed `approved` indefinitely: `token_ciphertext` held a

sealed, openable `smct_` token long past the window, and the computer the

approval created stayed `active`, counting against the owner's capacity and

issuing operator-approval receipts for a computer that never connected.

`machine_pairings.expires_at` recorded the deadline and nothing read it, which

is why `machine_pairings_expires_at_index` had no reader.

`OpenAgents.Machines.expire_elapsed_pairings/0` is that reader, and

`OpenAgents.Machines.PairingExpiry` runs it on the same interval and shape as

`OpenAgents.Forge.AssignmentExpiry`. It applies `claim_pairing/2`'s own expiry

rather than a second, weaker one: each row is re-read under `FOR UPDATE`, the

status moves to `expired`, `token_ciphertext` is nulled, and any computer the

pairing created is revoked together with the inference grants it holds. That

last step inherits IDENTITY-008 unchanged, because it is the same call inside

the same lock. A sweep and a late claim racing the same row therefore have one

winner, and the loser finds a status it no longer acts on. The revocation is

announced on the computer's topic, which this path had never done because until

now nothing ran it without a bearer.

The selection is proved separately from the outcomes, and the split is the

point. `expire_elapsed_pairing/1` refuses anything terminal or still fresh on

its own re-read, so widening the outer predicate changes no row and no return

value — every outcome test stays green while the sweep silently stops using the

index and starts scanning the table each minute, which is the defect this entry

closes. `OpenAgents.Machines.elapsed_pairing_query/1` is therefore public and

asserted twice: on exactly which rows it names, and on `EXPLAIN` of that same

query naming `machine_pairings_expires_at_index` with sequential scans priced

out.

Evidence: `OpenAgents.Machines.expire_elapsed_pairings/0`,

`OpenAgents.Machines.elapsed_pairing_query/1`,

`OpenAgents.Machines.PairingExpiry`, `OpenAgents.Machines.TokenVault`, and

`test/openagents/machines/pairing_expiry_test.exs`.

### IDENTITY-009 — Unified delegation preserves substrate authority

Status: Current

| IDENTITY-008 | `test/openagents_web/controllers/computer_control_api_test.exs`, `test/openagents/inference/computer_revocation_test.exs` |

| IDENTITY-009 | `test/openagents_web/controllers/delegations_controller_test.exs` |

| IDENTITY-010 | `test/openagents/forge/assignment_test.exs`, `test/openagents/forge/assignment_credential_reach_test.exs` |

| IDENTITY-011 | `test/openagents/machines/pairing_expiry_test.exs` |

| CAPACITY-002 | `test/openagents/box_fanout_test.exs` |

| CAPACITY-003 | `test/openagents/box_reconciler_test.exs` |

| WORK-002 | `test/openagents/box_runs_test.exs` |

        OpenAgents.BoxRunRecovery,

        OpenAgents.Box.Reconciler,

        OpenAgents.Forge.AssignmentExpiry,

        OpenAgents.Forge.AssignmentCredentialVault

        OpenAgents.Forge.AssignmentCredentialVault,

        OpenAgents.Machines.PairingExpiry

      ] ++ analytics_children() ++ [OpenAgentsWeb.Endpoint]

    # See https://elixir.hexdocs.pm/Supervisor.html

    end

  end

  @doc """

  Expire every pairing whose window has closed, without waiting for a poll.

  `claim_pairing/2` already expires an elapsed pairing, and that was the only

  thing that ever did. A pairing the CLI stops polling — killed, disconnected,

  or simply abandoned after the owner approved it — therefore stayed `approved`

  forever, holding the sealed computer token `TokenVault` promises lives only

  for the claim window, and leaving the computer it created `active` with a

  token nobody ever received.

  This is the same transition without a bearer. It reads

  `machine_pairings.expires_at`, which is what

  `machine_pairings_expires_at_index` exists for and what nothing read, then

  applies `claim_pairing/2`'s own expiry to each row under that row's lock: the

  status moves to `expired`, `token_ciphertext` is nulled, and any computer the

  pairing created is revoked along with the inference grants it holds

  (IDENTITY-008, IDENTITY-011).

  """

  @spec expire_elapsed_pairings() :: non_neg_integer()

  def expire_elapsed_pairings do

    DateTime.utc_now()

    |> elapsed_pairing_ids()

    |> Enum.count(&(expire_elapsed_pairing(&1) == :ok))

  end

  @doc """

  The rows `expire_elapsed_pairings/0` will act on, as of `now`.

  This is a separate function because it is the only thing in the release that

  reads `machine_pairings.expires_at`, and therefore the only reader

  `machine_pairings_expires_at_index` has. `expire_elapsed_pairing/1` re-reads

  each row under its own lock and refuses anything terminal or still fresh, so

  a widened predicate here changes no outcome and no result — it only makes the

  sweep read rows it will not touch, and stops using the index, invisibly. The

  selection is proved on its own for that reason.

  """

  @spec elapsed_pairing_ids(DateTime.t()) :: [Ecto.UUID.t()]

  def elapsed_pairing_ids(%DateTime{} = now), do: now |> elapsed_pairing_query() |> Repo.all()

  @doc "The selection above, unexecuted, so a proof can read its plan."

  @spec elapsed_pairing_query(DateTime.t()) :: Ecto.Query.t()

  def elapsed_pairing_query(%DateTime{} = now) do

    Pairing

    |> where([p], p.status in ["pending", "approved"] and p.expires_at <= ^now)

    |> select([p], p.id)

  end

  # One transaction per row. The re-read under `FOR UPDATE` is what makes the

  # sweep safe next to a claim arriving at the same moment: whichever takes the

  # lock first moves the row, and the other finds a status it no longer acts on.

  defp expire_elapsed_pairing(pairing_id) do

    Repo.transaction(fn ->

      case Repo.one(from(p in Pairing, where: p.id == ^pairing_id, lock: "FOR UPDATE")) do

        %Pairing{status: status} = pairing when status in ["pending", "approved"] ->

          if expired?(pairing), do: expire_locked_pairing(pairing), else: :fresh

        _consumed ->

          :consumed

      end

    end)

    |> case do

      {:ok, :ok} -> :ok

      _unchanged -> :unchanged

    end

  end

  defp verify_capacity(user_id) do

    now = DateTime.utc_now()

    |> Repo.update!()

    if pairing.machine_id do

      from(machine in Machine,

        where: machine.id == ^pairing.machine_id and machine.status == "active"

      )

      |> Repo.update_all(set: [status: "revoked", revoked_at: now, updated_at: now])

      {revoked, _returned} =

        from(machine in Machine,

          where: machine.id == ^pairing.machine_id and machine.status == "active"

        )

        |> Repo.update_all(set: [status: "revoked", revoked_at: now, updated_at: now])

      # The other revocation path, and it owes the same thing: this runs inside

      # the claim transaction, after the update has taken the computer row's

      # lock, so an interleaved mint cannot slip a live grant past it.

      _ = OpenAgents.Inference.revoke_active_for_machine(pairing.machine_id)

      # `revoke_machine/2` announces its revocation so the computer's channel

      # closes and an open /computers stops showing the card as live. This path

      # revokes too, and until the sweep existed nothing ever ran it headlessly.

      if revoked > 0 do

        Phoenix.PubSub.broadcast(

          OpenAgents.PubSub,

          "machine:#{pairing.machine_id}",

          {:machine_revoked, pairing.machine_id}

        )

      end

    end

    :ok

defmodule OpenAgents.Machines.PairingExpiry do

  @moduledoc """

  Periodically expires pairings whose windows have closed.

  Without it the only thing that expired a pairing was the CLI polling for its

  token, so an abandoned pairing kept a sealed computer token and a live

  computer indefinitely. See `INVARIANTS.md`, IDENTITY-011.

  """

  use GenServer

  @interval_ms 60_000

  @spec start_link(keyword()) :: GenServer.on_start()

  def start_link(options \\ []) do

    GenServer.start_link(__MODULE__, options, name: __MODULE__)

  end

  @impl true

  def init(options) do

    interval_ms = Keyword.get(options, :interval_ms, @interval_ms)

    schedule(interval_ms)

    {:ok, interval_ms}

  end

  @impl true

  def handle_info(:expire, interval_ms) do

    _ = OpenAgents.Machines.expire_elapsed_pairings()

    schedule(interval_ms)

    {:noreply, interval_ms}

  end

  defp schedule(interval_ms), do: Process.send_after(self(), :expire, interval_ms)

end

  `OpenAgents.Machines` `@pairing_lifetime_seconds`, and both terminal

  transitions — claim and expiry — null `token_ciphertext` on the way out. A

  compatibility branch with an empty population is a name and a claim that

  nothing tests. See `INVARIANTS.md`, CANON-002.

  nothing tests. That bound is enforced by

  `OpenAgents.Machines.expire_elapsed_pairings/0`; before it existed, expiry

  ran only when the CLI polled, so an abandoned pairing held its sealed token

  indefinitely. See `INVARIANTS.md`, CANON-002 and IDENTITY-011.

  The `openagents.machine_token.v2` AAD keeps its `machine` spelling for the

  opposite reason: it is bound into ciphertext this release did not write.

defmodule OpenAgents.Machines.PairingExpiryTest do

  @moduledoc """

  IDENTITY-011: a pairing window closes on its own clock.

  Before the sweep, `claim_pairing/2` was the only thing that expired a

  pairing, so every property here failed for the same reason: nobody polled.

  """

  use OpenAgents.DataCase, async: true

  alias OpenAgents.Inference

  alias OpenAgents.Machines

  alias OpenAgents.Machines.{Machine, Pairing, TokenVault}

  alias OpenAgents.Repo

  defp user(key) do

    {:ok, user} =

      OpenAgents.Accounts.upsert_github_user(%{

        github_id: :erlang.phash2({__MODULE__, key}),

        github_login: "pairing-expiry-#{key}",

        github_avatar_url: "https://avatars.githubusercontent.com/u/1?v=4"

      })

    user

  end

  defp start_pairing do

    {:ok, started} = Machines.start_pairing(%{"name" => "box", "tier" => "probe"})

    started

  end

  defp close_window(pairing_id) do

    Pairing

    |> Repo.get!(pairing_id)

    |> Ecto.Changeset.change(expires_at: DateTime.add(DateTime.utc_now(), -3_600, :second))

    |> Repo.update!()

  end

  test "an approved pairing nobody claims loses its sealed token" do

    %{pairing: pairing, code: code} = start_pairing()

    {:ok, _machine} = Machines.approve_pairing(user("sealed"), code)

    assert is_binary(Repo.get!(Pairing, pairing.id).token_ciphertext),

           "the fixture must actually hold a sealed token"

    close_window(pairing.id)

    assert Machines.expire_elapsed_pairings() == 1

    swept = Repo.get!(Pairing, pairing.id)

    assert swept.status == "expired"

    assert is_nil(swept.token_ciphertext)

  end

  test "the computer an unclaimed pairing created is revoked" do

    %{pairing: pairing, code: code} = start_pairing()

    {:ok, machine} = Machines.approve_pairing(user("computer"), code)

    close_window(pairing.id)

    assert Machines.expire_elapsed_pairings() == 1

    revoked = Repo.get!(Machine, machine.id)

    assert revoked.status == "revoked"

    assert revoked.revoked_at

  end

  test "the revoked computer's inference grants close with it" do

    %{pairing: pairing, code: code} = start_pairing()

    owner = user("grants")

    {:ok, machine} = Machines.approve_pairing(owner, code)

    {:ok, conversation} = OpenAgents.Conversations.ensure_conversation(owner)

    {:ok, grant, _token} =

      Inference.mint(%{

        owner_visitor_id: conversation.visitor_id,

        conversation_id: conversation.id,

        machine_id: machine.id

      })

    assert grant.status == "active"

    close_window(pairing.id)

    assert Machines.expire_elapsed_pairings() == 1

    assert Repo.reload!(grant).status == "revoked"

  end

  test "the sweep announces the revocation so an open channel closes" do

    %{pairing: pairing, code: code} = start_pairing()

    {:ok, machine} = Machines.approve_pairing(user("broadcast"), code)

    :ok = Phoenix.PubSub.subscribe(OpenAgents.PubSub, "machine:#{machine.id}")

    close_window(pairing.id)

    assert Machines.expire_elapsed_pairings() == 1

    machine_id = machine.id

    assert_receive {:machine_revoked, ^machine_id}

  end

  test "a pending pairing nobody approves expires too" do

    %{pairing: pairing} = start_pairing()

    close_window(pairing.id)

    assert Machines.expire_elapsed_pairings() == 1

    assert Repo.get!(Pairing, pairing.id).status == "expired"

  end

  test "a pairing still inside its window is left alone" do

    %{pairing: pairing, code: code} = start_pairing()

    {:ok, machine} = Machines.approve_pairing(user("fresh"), code)

    assert Machines.expire_elapsed_pairings() == 0

    assert Repo.get!(Pairing, pairing.id).status == "approved"

    assert Repo.get!(Machine, machine.id).status == "active"

  end

  test "a claimed pairing is never swept, and its computer keeps working" do

    %{pairing: pairing, code: code, poll_secret: poll_secret} = start_pairing()

    {:ok, machine} = Machines.approve_pairing(user("claimed"), code)

    {:ok, %{token: token}} = Machines.claim_pairing(pairing.id, poll_secret)

    close_window(pairing.id)

    assert Machines.expire_elapsed_pairings() == 0

    assert Repo.get!(Pairing, pairing.id).status == "claimed"

    assert {:ok, %Machine{id: id}} = Machines.authenticate_token(token)

    assert id == machine.id

  end

  test "the sweep is idempotent" do

    %{pairing: pairing, code: code} = start_pairing()

    {:ok, _machine} = Machines.approve_pairing(user("idempotent"), code)

    close_window(pairing.id)

    assert Machines.expire_elapsed_pairings() == 1

    assert Machines.expire_elapsed_pairings() == 0

  end

  # The claim path and the sweep must reach the same state, or the sweep would

  # be a second, weaker expiry rather than the same one on a clock.

  test "the sweep leaves the row where a late claim would have left it" do

    %{pairing: swept, code: swept_code} = start_pairing()

    {:ok, _} = Machines.approve_pairing(user("parity-a"), swept_code)

    close_window(swept.id)

    assert Machines.expire_elapsed_pairings() == 1

    %{pairing: claimed, code: claimed_code, poll_secret: secret} = start_pairing()

    {:ok, _} = Machines.approve_pairing(user("parity-b"), claimed_code)

    close_window(claimed.id)

    assert {:error, :pairing_expired} = Machines.claim_pairing(claimed.id, secret)

    fields = fn id ->

      row = Repo.get!(Pairing, id)

      {row.status, row.token_ciphertext, Repo.get!(Machine, row.machine_id).status}

    end

    assert fields.(swept.id) == fields.(claimed.id)

  end

  # The sweep's selection is the only reader `machine_pairings_expires_at_index`

  # has, and it is invisible to every outcome above: `expire_elapsed_pairing/1`

  # re-reads each row under `FOR UPDATE` and refuses anything terminal or still

  # fresh, so widening the predicate leaves all of those tests green while the

  # index quietly stops being used. It is proved directly for that reason.

  describe "the sweep's selection" do

    test "names elapsed pending and approved pairings and nothing else" do

      %{pairing: elapsed_pending} = start_pairing()

      close_window(elapsed_pending.id)

      %{pairing: elapsed_approved, code: approved_code} = start_pairing()

      {:ok, _} = Machines.approve_pairing(user("select-approved"), approved_code)

      close_window(elapsed_approved.id)

      %{pairing: elapsed_claimed, code: claimed_code, poll_secret: secret} = start_pairing()

      {:ok, _} = Machines.approve_pairing(user("select-claimed"), claimed_code)

      {:ok, _} = Machines.claim_pairing(elapsed_claimed.id, secret)

      close_window(elapsed_claimed.id)

      %{pairing: fresh} = start_pairing()

      selected = Machines.elapsed_pairing_ids(DateTime.utc_now())

      assert Enum.sort(selected) == Enum.sort([elapsed_pending.id, elapsed_approved.id])

      refute elapsed_claimed.id in selected

      refute fresh.id in selected

    end

    test "the predicate is served by machine_pairings_expires_at_index" do

      # A cold table is small enough that a sequential scan is the cheaper plan,

      # so the planner is asked which index it would use, not whether it bothers.

      # `SET LOCAL` so the choice dies with the sandbox's transaction and cannot

      # follow this connection back into the pool.

      Repo.query!("SET LOCAL enable_seqscan = off")

      # The production query itself, not a copy of it, so a predicate that stops

      # naming `expires_at` fails here as well as above.

      {sql, params} =

        Ecto.Adapters.SQL.to_sql(

          :all,

          Repo,

          Machines.elapsed_pairing_query(DateTime.utc_now())

        )

      plan =

        Repo.query!("EXPLAIN " <> sql, params).rows

        |> Enum.map_join("\n", &hd/1)

      assert plan =~ "machine_pairings_expires_at_index", plan

    end

  end

  # TokenVault carries exactly one AAD on the strength of this bound, and

  # CANON-002 states it as settled. It was not: nothing enforced it.

  test "no sealed ciphertext survives a closed window" do

    for key <- ["survivor-a", "survivor-b"] do

      %{pairing: pairing, code: code} = start_pairing()

      {:ok, _} = Machines.approve_pairing(user(key), code)

      close_window(pairing.id)

    end

    _swept = Machines.expire_elapsed_pairings()

    stale =

      Repo.all(

        from p in Pairing,

          where: not is_nil(p.token_ciphertext) and p.expires_at <= ^DateTime.utc_now(),

          select: p.token_ciphertext

      )

    assert stale == [],

           "sealed tokens outlived their window: #{inspect(Enum.map(stale, &TokenVault.open/1))}"

  end

end