a checker for the deprovision spec, and the trap that makes it pass for free

scripts/assert-uid-free.sh is the verification half of docs/deprovision-os-account.md, written
outside the implementation on purpose: a checker the function calls is a restatement of its own
beliefs rather than an audit. Nine checks — passwd entry, uid reuse, both subid files, linger,
runtime dir, live processes, files owned by the uid, and files owned anywhere in the freed
subuid range.

Two modes, because the range has to be captured BEFORE deletion. userdel removes the
/etc/subuid entry along with the account, and after that there is no way to ask what range it
held — so a checker that only runs afterwards silently drops the half most likely to be wrong.

Exercised against green while fully provisioned: eight of nine checks fail, exit 1. A checker
that has never been seen to fail is not evidence.

And the trap worth knowing before anyone trusts a green result: the subuid check passes
vacuously on most accounts. Files get a mapped owner only when a process inside a container runs
as a NON-root user; an image whose files are root-owned maps to the member's own uid and leaves
the range empty. Measured on green after a night of real use — claude installed, an image
pulled, transcripts written — the range check found zero files and passed without testing
anything. The spec now says how to build a specimen that actually exercises it, and to watch the
check fail on that tree before trusting it to pass on a cleaned one.

Docs and a script only; no behaviour change. On a branch, for whoever merges it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

docs/deprovision-os-account.md

@@ -146,8 +146,28 @@ All of these must hold for the freed uid *and* its freed subuid range:
 - `/run/user/<uid>` absent
 - no processes owned by the uid
 
-Worth extracting as `assertUidFree(uid, subuidRange)` and reusing it as the post-condition of the function and
-as a test.
+`scripts/assert-uid-free.sh` implements exactly this, deliberately **outside** the function: a checker the
+implementation calls is a restatement of its own beliefs, not an audit. Two modes, and the split matters —
+
+```
+./scripts/assert-uid-free.sh --capture green                    # BEFORE: prints "green 1001 165536 65536"
+sudo ./scripts/assert-uid-free.sh --check green 1001 165536 65536   # AFTER: exit 1 unless clean
+```
+
+The range has to be captured **before** deletion, because `userdel` removes the `/etc/subuid` entry with the
+account. After that there is no way to ask what range it held — and a check that silently skips that half is
+the exact failure this section exists to prevent.
+
+**The subuid check passes vacuously on most accounts, and that is a trap.** Container files are owned by a
+mapped id only when a process inside the container runs as a NON-root user; an image whose files are root-owned
+maps to the member's own uid and leaves nothing in the range. Measured on green after a night of real use —
+`claude` installed, images pulled, transcripts written — the range check found **zero** files and passed
+without testing anything.
+
+To build a specimen that actually exercises it, run a container whose process writes as a non-root user. The
+`postgres:18-alpine` case from the same night is the natural one: its entrypoint drops to uid 70, and the data
+directory came out owned by `subuid_start + 70` on the host. Verify the range check *fails* on that tree before
+trusting it to pass on a cleaned one.
 
 **Trap for the verifier:** do not use `sudo -u <user> …` to check anything after step 2. Creating a session
 starts a user manager and recreates `/run/user/<uid>`, so the check would undo the step it is verifying.

scripts/assert-uid-free.sh

@@ -0,0 +1,69 @@
+#!/usr/bin/env bash
+# Verify that a deprovisioned account has genuinely released its uid.
+#
+# Written as the verification half of `docs/deprovision-os-account.md`, deliberately OUTSIDE the
+# implementation: if the function under test calls its own checker, the check is a restatement rather than
+# an audit. This runs against the machine and knows nothing about the code that was supposed to clean it.
+#
+# The subuid range must be captured BEFORE the account is deleted, because `userdel` removes the
+# /etc/subuid entry along with the account — after which there is no way to ask what range it held, and a
+# check that silently skips that half is the failure mode this whole file exists to prevent.
+#
+#   ./assert-uid-free.sh --capture green            # before: prints "green 1001 165536 65536"
+#   ./assert-uid-free.sh --check green 1001 165536 65536   # after: exits non-zero unless clean
+#
+set -uo pipefail
+
+DATA_PATH="${DATA_PATH:-/home/pastilhas/officerdev/data}"
+SEARCH_ROOTS=("$DATA_PATH" /home)
+
+usage() { echo "usage: $0 --capture <user> | --check <user> <uid> <subuid_start> <subuid_count>" >&2; exit 2; }
+
+if [[ "${1:-}" == "--capture" ]]; then
+  user="${2:?user required}"
+  uid="$(id -u "$user" 2>/dev/null)" || { echo "no such account: $user" >&2; exit 1; }
+  range="$(awk -F: -v u="$user" '$1==u {print $2" "$3; exit}' /etc/subuid)"
+  [[ -n "$range" ]] || { echo "no /etc/subuid entry for $user — capture it another way or it is unverifiable" >&2; exit 1; }
+  echo "$user $uid $range"
+  exit 0
+fi
+
+[[ "${1:-}" == "--check" ]] || usage
+user="${2:?}"; uid="${3:?}"; sub_start="${4:?}"; sub_count="${5:?}"
+sub_end=$(( sub_start + sub_count - 1 ))
+
+fails=0
+ok()   { printf '  ok    %s\n' "$1"; }
+bad()  { printf '  FAIL  %s\n' "$1"; fails=$((fails+1)); }
+
+echo "checking $user (uid $uid, subuids $sub_start-$sub_end)"
+
+getent passwd "$user" >/dev/null 2>&1 && bad "passwd entry still exists" || ok "no passwd entry"
+getent passwd "$uid" >/dev/null 2>&1 && bad "uid $uid reassigned or still present" || ok "uid $uid unused"
+
+grep -q "^$user:" /etc/subuid 2>/dev/null && bad "/etc/subuid entry remains" || ok "no /etc/subuid entry"
+grep -q "^$user:" /etc/subgid 2>/dev/null && bad "/etc/subgid entry remains" || ok "no /etc/subgid entry"
+
+[[ -e "/var/lib/systemd/linger/$user" ]] && bad "linger marker remains" || ok "no linger marker"
+[[ -d "/run/user/$uid" ]] && bad "/run/user/$uid remains" || ok "no runtime directory"
+
+procs="$(pgrep -u "$uid" 2>/dev/null | wc -l)"
+[[ "$procs" -eq 0 ]] && ok "no processes" || bad "$procs process(es) still owned by uid $uid"
+
+# The uid half.
+owned="$(find "${SEARCH_ROOTS[@]}" -uid "$uid" -print -quit 2>/dev/null)"
+[[ -z "$owned" ]] && ok "no files owned by uid $uid" || bad "files owned by uid $uid (e.g. $owned)"
+
+# The subuid half — the one a uid-only check passes straight through. Container processes running as a
+# non-root user inside their namespace write files owned by a MAPPED id, not by the member's uid, and
+# `userdel` frees the whole range for reallocation.
+mapped="$(find "${SEARCH_ROOTS[@]}" -uid +"$((sub_start-1))" ! -uid +"$sub_end" -print -quit 2>/dev/null)"
+[[ -z "$mapped" ]] && ok "no files in the freed subuid range" || bad "files owned by the freed subuid range (e.g. $mapped)"
+
+echo
+if [[ "$fails" -eq 0 ]]; then
+  echo "CLEAN — uid $uid and its subuid range are safe to reissue"
+  exit 0
+fi
+echo "NOT CLEAN — $fails check(s) failed; do not reissue this uid"
+exit 1