From 3ded67d81ccd5285c58a2a3ac2dd39ac8800c987 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 12 Nov 2026 02:00:05 +0000 Subject: [PATCH 1/9] fix(skills): check the agent-tty socket dir before launch uses it MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit agent-tty keeps every session socket under the fixed dir /tmp/agent-tty, whatever TMPDIR says, and never checks who owns it. Reproduced on main in a bwrap user namespace that this user owns, with /tmp/agent-tty a host-root-owned 1777 dir (it shows as owned by nobody and this user can still write in it): agent-tty create made its per-home dir and socket inside it without complaint. The agent-tty client connects to the path and accepts any answer that echoes the request id, so a party that can rename entries in that dir can move the per-home dir away, listen on a socket of the same name, and agent-tty snapshot prints what it answers (the repro printed FORGED-BY-SQUATTER). Launch now makes /tmp/agent-tty with mode 0700 when it is missing and refuses one that is a symlink, is owned by another user or is group- or world-writable, through the check that already covers VERIFY_OUT (unsafe_dir). The check runs before launch makes the state dir, so a refusal leaves nothing behind. Proof: five cases in proof-launch-refusals.sh in a bwrap sandbox with a /tmp of its own (att-root-foreign, att-root-loose, att-root-link refuse; att-root-made and att-root-own-755 accept). The tmp-link-foreign case shares its sandbox setup with them. SKILL.md says what launch does, and that root is fine above the state dir. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_ --- .../skills/verify-claudecode-nvim/SKILL.md | 4 +- .../scripts/proof-launch-refusals.sh | 80 +++++++++++++++---- .../verify-claudecode-nvim/scripts/vcn.sh | 12 +++ 3 files changed, 79 insertions(+), 17 deletions(-) diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md index c271b6fc5..e0486786d 100644 --- a/.agents/skills/verify-claudecode-nvim/SKILL.md +++ b/.agents/skills/verify-claudecode-nvim/SKILL.md @@ -52,7 +52,7 @@ Launch first runs `agent-tty doctor` and saves it to `$OUT/agent-tty-doctor.json - CI does not run the harness, on 0.8 or any other version. A run needs `agent-tty` from npm and Playwright Chromium (about 400 MB unpacked), and CI installs neither. Node is not the obstacle: the `unit-tests` job already gets the repo's Node 26 from mise. The two would add minutes and two more downloads to every PR. CI's `integration-tests (v0.8.0)` job already runs the plugin's integration tests on Neovim 0.8. After a change to `vcn.sh`, check the 0.8 path by hand: do the full run at the end of this file, with `VCN_NVIM=<0.8 nvim> $V launch` as its launch step. - `VCN_RTP=[:...]` adds plugin dirs to `runtimepath` after this checkout. A `terminal.provider = "snacks"` run needs a snacks.nvim clone there, because the harness installs no plugin. Pin the clone as [features/send-at-mention.md](features/send-at-mention.md) shows. A relative entry resolves against the directory you launch from, because nvim runs in `$WORK`, and symlinks are followed. Launch exits 1 for an entry that is not a directory, so a typo cannot pass as a snacks run on a native terminal. A float run is in [features/terminal-float-diff.md](features/terminal-float-diff.md). - `VCN_INIT_JSONRPC=` sets the `jsonrpc` field of the `initialize` request (default `2.0`). Only `scripts/proof-launch-refusals.sh` sets it, to get an error answer from the plugin. -- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`) (the dashboard command below runs `agent-tty` itself, with your `TMPDIR`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the five `journey-*.sh` scripts and the dashboard command source it without this check): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`. +- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`) (the dashboard command below runs `agent-tty` itself, with your `TMPDIR`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. `agent-tty` keeps every socket in the fixed dir `/tmp/agent-tty`, whatever `TMPDIR` says, and does not check who owns it, so another user who owns that dir or can rename entries in it could swap the socket dir of a run and answer every command. Launch makes `/tmp/agent-tty` with mode `0700` when it is missing, and refuses one that is a symlink, is owned by another user or is group- or world-writable (a `0755` dir of yours is fine). Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the five `journey-*.sh` scripts and the dashboard command source it without this check): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`. - `VCN_SETUP=''` is deep-merged into `require("claudecode").setup()` over the base `{ terminal = { provider = "none" } }`. Example: `VCN_SETUP='{"diff_opts":{"layout":"unified"}}' $V launch`. - For a `log_level = "debug"` run, launch with `VCN_SETUP='{"log_level":"debug"}' $V launch --cmd 'set messagesopt=wait:0,history:10000' hello.txt`. Without it, one openDiff call at debug level parks Neovim at `Press ENTER`, and RPC stops answering. Launch arguments replace the default file, so name `hello.txt`. Neovim 0.8 has no `messagesopt`, so plain `set` fails launch with E518. Use `--cmd 'silent! set messagesopt=wait:0,history:10000'` there. Launch then works, but debug echoes still stop at `Press ENTER` (see Doctor). @@ -130,7 +130,7 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul - `scripts/vcn.sh` is the harness. `$V help` lists its subcommands. - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`. - `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (the proof reads the source), a `run.env` without `JQ_BIN` still runs `jq`, a doc that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` in a code block (or in inline code) sets it in the same block (or the same doc, for inline code), because a fresh shell has none of them (`doc-vars`), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, and a command run with a `TMPDIR` that does not exist still works, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1. -- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one). It also proves that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes about 60 s. +- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes about 60 s. - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`. - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`. - The `race` case puts a `mkdir` shim first on `PATH`. The shim plays another launch that makes the dir above `VERIFY_OUT` first, group-writable. Launch must refuse that dir in the check after `mkdir` and leave it in place. diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh index d6325f1df..de185cce9 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh @@ -151,23 +151,20 @@ mkdir -m 700 "$TMP/lnk-safe" ln -s "$TMP/lnk-safe" "$TMP/lnk-loose/t" refused tmp-link-loose "refusing TMPDIR: $TMP/lnk-loose, above the state dir, is writable by others and not sticky" \ TMPDIR="$TMP/lnk-loose/t" VERIFY_OUT="$TMP/tmp-out" -# bwrap makes a user namespace that this user owns (no sudo, no second account). Root's inodes show as another user there: -# /var/run is a root-owned symlink to /run, and `--dir /run` makes the target this user's, so only the owner of the symlink -# can refuse it. The tools that launch resolves before the TMPDIR check are bound read-only under their own paths. -tmp_link_foreign_case() { - local name=tmp-link-foreign tool exe root repo out rc=0 paths="" binds=() +# bwrap makes a user namespace that this user owns (no sudo, no second account). Root's inodes show as another user there. +# sandbox_base sets sb to the bwrap arguments that the sandboxed launches below share, or prints SKIP and fails. The tools +# that launch resolves before its checks are bound read-only under their own paths, the repo is at /w, and /tmp is a tmpfs of +# its own, so no case touches the host's /tmp. +sandbox_base() { + local name=$1 tool exe root repo paths="" binds=() command -v bwrap >/dev/null || { echo "SKIP $name: bwrap is not installed" - return 0 - } - [[ -L /var/run && $(stat -c %u /var/run) == 0 && $(realpath /var/run) == /run ]] || { - echo "SKIP $name: /var/run is not a root-owned symlink to /run" - return 0 + return 1 } for tool in nvim node jq; do exe=$(mise which "$tool" 2>/dev/null || command -v "$tool") || { echo "SKIP $name: $tool not found" - return 0 + return 1 } exe=$(realpath -- "$exe") # nvim needs the runtime beside its bin dir. @@ -176,14 +173,25 @@ tmp_link_foreign_case() { paths+=$(dirname -- "$exe"): done repo=$(cd "$(dirname "$V")/../../../.." && pwd) - local args=(--unshare-user --uid 0 --gid 0 --ro-bind /usr /usr --symlink usr/bin /bin --symlink usr/lib /lib + sb=(--unshare-user --uid 0 --gid 0 --ro-bind /usr /usr --symlink usr/bin /bin --symlink usr/lib /lib --symlink usr/lib64 /lib64 --unshare-pid --dev /dev --proc /proc --perms 01777 --tmpfs /tmp "${binds[@]}" - --ro-bind /var /var --dir /run --ro-bind "$repo" /w --setenv PATH "$paths/usr/bin:/bin" --setenv HOME /tmp - --setenv VCN_AGENT_TTY /usr/bin/true --setenv VERIFY_OUT /tmp/out --setenv TMPDIR /var/run) - bwrap "${args[@]}" /usr/bin/true 2>/dev/null || { + --ro-bind "$repo" /w --setenv PATH "$paths/usr/bin:/bin" --setenv HOME /tmp --setenv VERIFY_OUT /tmp/out) + bwrap "${sb[@]}" /usr/bin/true 2>/dev/null || { echo "SKIP $name: bwrap cannot make a user namespace here" + return 1 + } +} + +# /var/run is a root-owned symlink to /run, and `--dir /run` makes the target this user's, so only the owner of the symlink +# can refuse it. +tmp_link_foreign_case() { + local name=tmp-link-foreign out rc=0 + [[ -L /var/run && $(stat -c %u /var/run) == 0 && $(realpath /var/run) == /run ]] || { + echo "SKIP $name: /var/run is not a root-owned symlink to /run" return 0 } + sandbox_base "$name" || return 0 + local args=("${sb[@]}" --ro-bind /var /var --dir /run --setenv VCN_AGENT_TTY /usr/bin/true --setenv TMPDIR /var/run) out=$(bwrap "${args[@]}" /usr/bin/bash -c '[[ $(stat -c %u /var/run) != "$EUID" && $(stat -c %u /run) == "$EUID" ]] || echo SETUP-WRONG-OWNERS /w/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh launch; echo "rc=$?"' 2>&1) || rc=$? [[ $out != *SETUP-WRONG-OWNERS* ]] || fail "$name: the symlink is not another user's or its target is not this user's, so the case proves nothing: $out" @@ -192,6 +200,48 @@ tmp_link_foreign_case() { echo "PASS $name: TMPDIR=/var/run, a symlink that another user owns, was refused before launch made anything" } tmp_link_foreign_case + +# agent-tty keeps every socket under the fixed dir /tmp/agent-tty and never checks who owns it. Another user who owns it, or who +# can rename entries in it, could swap the socket dir of a run and answer every command. Launch makes the dir 0700 when it is +# missing and refuses one that is not this user's alone. +# att_root_case [bwrap args]: launch in a sandbox after the planting shell ran. is +# the text of a refusal, which must leave nothing behind, or empty when launch must get past the check (it stops later, +# because no agent-tty passes doctor) and leave /tmp/agent-tty with and this user as its owner. +att_root_case() { + local name=$1 plant=$2 want=$3 mode=$4 out rc=0 + shift 4 + sandbox_base "$name" || return 0 + local args=("${sb[@]}" "$@" --setenv VCN_AGENT_TTY /usr/bin/false) + out=$(bwrap "${args[@]}" /usr/bin/bash -c "$plant"' + /w/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh launch; echo "rc=$?" + [[ ! -e /tmp/out && -z $(ls -d /tmp/vcn.* 2>/dev/null) ]] || echo LEFT-BEHIND + stat -c "ROOT %a %u" /tmp/agent-tty 2>&1' 2>&1) || rc=$? + if [[ -n $want ]]; then + [[ $out == *"refusing the agent-tty socket dir: $want"* && $out == *"rc=1"* && $out != *VCN_STATE=* && $out != *LEFT-BEHIND* ]] || + fail "$name: launch did not refuse /tmp/agent-tty with '$want', exit 1 and nothing left behind: $out" + echo "PASS $name: $want, and launch refused it before it made anything" + else + [[ $out != *"refusing the agent-tty socket dir"* && $out == *"rc=1"* && $out == *"ROOT $mode 0"* ]] || + fail "$name: launch refused /tmp/agent-tty or did not leave it with mode $mode and this user as owner: $out" + echo "PASS $name: launch accepted /tmp/agent-tty and left it with mode $mode" + fi +} +host_root_dir="" +for cand in /srv /opt /usr /etc; do + [[ $(stat -c '%u %a' -- "$cand" 2>/dev/null) == "0 755" ]] && { + host_root_dir=$cand + break + } +done +if [[ -n $host_root_dir ]]; then + att_root_case att-root-foreign : "/tmp/agent-tty is owned by another user" "" --ro-bind "$host_root_dir" /tmp/agent-tty +else + echo "SKIP att-root-foreign: no host-root-owned 0755 dir to bind" +fi +att_root_case att-root-loose 'mkdir -m 777 /tmp/agent-tty' "/tmp/agent-tty is group- or world-writable" "" +att_root_case att-root-link 'ln -s /tmp /tmp/agent-tty' "/tmp/agent-tty is a symlink" "" +att_root_case att-root-made : "" 700 +att_root_case att-root-own-755 'mkdir -m 755 /tmp/agent-tty' "" 755 # A newline at the end of a name is cut by a command substitution. The resolved TMPDIR is a dir with a newline at the end of its # name and mode 777, and a twin symlink without the newline leads to a safe dir: a launch that cuts the newline would take the twin. mkdir -m 700 "$TMP/nl" "$TMP/nl/safe" diff --git a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh index 5417f1d07..a9559161f 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh @@ -385,6 +385,17 @@ unsafe_above() { [[ -z $why ]] || echo "$why" } +# agent-tty keeps every socket under the fixed dir /tmp/agent-tty, whatever TMPDIR says, and never checks who owns it. Another +# user who owns that dir, or who can rename entries in it, could swap the socket dir of a run and answer every command. +# Make it 0700 when it is missing, and refuse one that is not this user's alone. +ensure_att_root() { + local why + [[ -e /tmp/agent-tty || -L /tmp/agent-tty ]] || mkdir -m 700 -- /tmp/agent-tty 2>/dev/null || true + why=$(unsafe_dir /tmp/agent-tty) + [[ -z $why ]] || die "refusing the agent-tty socket dir: $why; agent-tty keeps its sockets in /tmp/agent-tty and does not check who owns it" + [[ -d /tmp/agent-tty ]] || die "cannot make /tmp/agent-tty, where agent-tty keeps its sockets" +} + # stat prints one record per dir, mode, owner and type and no name, so no path is ever read back from a line of text: # a name with a trailing space, a tab or a newline would be cut, and a twin symlink with the shorter name tested in its # place. The type is the raw mode in hex (%f): GNU stat translates the label that %F prints. @@ -528,6 +539,7 @@ cmd_launch() { # symlinks of that path after launch has resolved them (agent-tty gets $VCN_STATE/tmp), so it no longer guards a later call. why=$(unsafe_walk "$given" "the state dir") [[ -z $why ]] || die "refusing TMPDIR: $why; set TMPDIR to a dir only you can write" + ensure_att_root # Short /tmp path: the nvim RPC socket path must stay under 108 bytes. # A signal while mktemp runs is recorded and acted on once the state dir exists. mktemp ignores signals, so it cannot # die between making the dir and printing its name. From 18671502e474b3929fc95d1eee6647c4d9d73c01 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 12 Nov 2026 02:19:25 +0000 Subject: [PATCH 2/9] test(skills): prove that att() makes $VCN_STATE/tmp for a run that has none MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-5 verifiers of #506 (F1): deleting `[[ -d $VCN_STATE/tmp ]] || mkdir -m 700 ...` from att() left the refusal proof at 34 PASS and the resolution proof at CASES 45. The line decides whether `record` works on a run that an older vcn.sh started, because that run has no tmp dir and agent-tty needs one for its WebM export. tmp-removed launches, removes $VCN_STATE/tmp, and requires `record` to exit 0 with a non-empty r2.webm and tmp back at mode 0700. Without the mkdir in att() the case fails: record exits 1 (agent-tty EXPORT_ERROR). _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_ --- .../scripts/proof-agent-tty-resolution.sh | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh index b0eadd00b..3fcf077fd 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh @@ -29,6 +29,7 @@ # can write: launch accepts it, and after another user repoints the second symlink, `record` still # writes no byte of theirs into the evidence dir, because no agent-tty call of vcn.sh reads the caller's TMPDIR # tmp-later-tmpdir a command run with a TMPDIR that does not exist works: agent-tty makes its staging dirs in the state dir +# tmp-removed a run without $VCN_STATE/tmp, as an older vcn.sh left it, works: `record` makes the dir (0700) and writes a WebM # state-count a stat that answers for one dir fewer than the walk asked for (a shim drops the record of the loose # dir above the state dir) makes the walk refuse, not pass # state-newline a state dir whose name ends in a newline is accepted: the check reads its resolved path whole @@ -1115,6 +1116,24 @@ tmp_later_case() { cases=$((cases + 1)) } +# A run that an older vcn.sh started has no $VCN_STATE/tmp. att() must make it, mode 0700, before it gives agent-tty that TMPDIR, +# or the WebM export of record fails. The case removes the dir that launch made to look like such a run. +tmp_removed_case() { + local name=tmp-removed r=0 mode + launch "$name" "$good_path" + ((rc == 0)) || fail "$name" "launch exited $rc: $out" + [[ $state == "$priv"/vcn.?????? ]] || fail "$name" "launch printed a state dir outside the proof's private dir: $state" + rm -rf -- "$state/tmp" + env PATH="$good_path" VCN_STATE="$state" "$V" record r2 >"$TMP/$name-record.txt" 2>&1 || r=$? + mode=$(stat -c %a -- "$state/tmp" 2>/dev/null || echo missing) + stop "$good_path" + ((r == 0)) || fail "$name" "record without $state/tmp exited $r: $(tail -n 2 "$TMP/$name-record.txt")" + [[ -s $TMP/out-$name/r2.webm ]] || fail "$name" "record wrote no r2.webm" + [[ $mode == 700 ]] || fail "$name" "record left $state/tmp with mode $mode, not 700" + echo "ok $name: record made $state/tmp again with mode 0700 and wrote a WebM" + cases=$((cases + 1)) +} + signal_symlink_case() { local name=signal-symlink gate=$TMP/gate-signal-symlink sockdir ln -s "$priv" "$TMP/priv-link" @@ -1176,6 +1195,7 @@ state_owner_case state_ancestor_case tmp_multihop_case tmp_later_case +tmp_removed_case signal_symlink_case sigterm_case echo "CASES $cases" From caeefd3bdcece0836832f9331630887859d0ff36 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 12 Nov 2026 03:26:49 +0000 Subject: [PATCH 3/9] feat(skills): read a run's values through vcn.sh get, guard NODE_DIR, run the static proofs in CI MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up of #506 and #508 (their verifiers' index items N3, m1-m5, F1 and F2). get and dashboard. The five journey-*.sh scripts and the dashboard command still ran `source "$VCN_STATE/run.env"` in the caller's own shell, with no check of the state dir. `vcn.sh get [-z] ` answers one value of run.env after load's check, and only a name that run.env holds. A journey reads OUT and WORK through it (`-z` keeps a newline at the end of a path), so a stale exported OUT cannot redirect its evidence, and `vcn.sh dashboard` runs the agent-tty dashboard through att(). Nothing parses printed text, which the #508 round-5 verifier showed to be forgeable. NODE_DIR. att() puts NODE_DIR in front of PATH. load and launch now refuse an empty or relative NODE_DIR (the current dir would go on PATH) and one with a colon (a second dir). A dir that lost its node is not refused, so cleanup still runs. Static proofs. proof-static.sh holds no-bare-tools and doc-vars, moved out of the resolution proof, and `mise run check` runs it, so CI does. It closes the gaps of the #508 round-6 index: indented and ~~~ fences (m1), a comment that names `source run.env` (m2), a self-test that checked a copy of the set pattern (m3), and `"${JQ_BIN:-jq}"` (m4). A new case, no-source-run-env, fails when any script or recipe of the skill sources a run.env except load. Proof cases: get-values, get-state, journey-out (VERIFY_OUT with ` OUT=` in it, a newline in it and at its end, and a stale exported OUT), dashboard, node-dir in the resolution proof, node-relative in the refusal proof. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_ --- .../skills/verify-claudecode-nvim/SKILL.md | 11 +- .../verify-claudecode-nvim/features/README.md | 2 +- .../scripts/journey-diff-close-save.sh | 6 +- .../scripts/journey-new-tab-diff-mode.sh | 6 +- .../scripts/journey-opendiff-accept.sh | 6 +- .../scripts/journey-snacks-float-diff.sh | 6 +- .../scripts/journey-snacks-float-reload.sh | 6 +- .../scripts/proof-agent-tty-resolution.sh | 257 +++++++++++------- .../scripts/proof-launch-refusals.sh | 14 +- .../scripts/proof-static.sh | 208 ++++++++++++++ .../verify-claudecode-nvim/scripts/vcn.sh | 42 ++- mise.toml | 4 +- 12 files changed, 450 insertions(+), 118 deletions(-) create mode 100755 .agents/skills/verify-claudecode-nvim/scripts/proof-static.sh diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md index e0486786d..ee7a6eaa6 100644 --- a/.agents/skills/verify-claudecode-nvim/SKILL.md +++ b/.agents/skills/verify-claudecode-nvim/SKILL.md @@ -36,7 +36,7 @@ VCN_STATE=/tmp/vcn.AbC123 OUT=/home/coder/.xum/sessions//scratch/verify-claudecode-nvim/20261031T120000Z-AbC123 ``` -Every bash call is a fresh shell. Start each later call with the two values launch printed, each in single quotes because a path can hold a space or an apostrophe (`TMPDIR` and `VERIFY_OUT` allow both): `export VCN_STATE='/tmp/vcn.AbC123' OUT=''`. Inside the quotes, write each `'` of the path as `'\''`. Use a new request id for every `rpc` or `tool` call, because the harness refuses an id the run already used. Do not `source` `$VCN_STATE/run.env` or `$OUT/run.env` in your own calls: bash runs every line of a file it sources, as you. `launch` appends version lines such as `agent-tty 0.5.0` to `$OUT/run.env`, and bash would run those as commands. The five `journey-*.sh` scripts and the dashboard command below still `source` `$VCN_STATE/run.env`. `vcn.sh` checks `$VCN_STATE` before it sources `run.env` (it must be its own resolved path and a directory that this user owns, with no group or other write, and no dir above it may be owned by another user or writable by others without the sticky bit), but only in its own commands. Those scripts and that command do not make the check. Export a `VCN_STATE` that your own `launch` printed, never one from an earlier or another session. Get the other values from the run: +Every bash call is a fresh shell. Start each later call with the `VCN_STATE` value that launch printed, in single quotes because a path can hold a space or an apostrophe (`TMPDIR` and `VERIFY_OUT` allow both): `export VCN_STATE='/tmp/vcn.AbC123'`. Inside the quotes, write each `'` of the path as `'\''`. A path can hold a newline too, and launch then prints it over two lines: copy all of it, inside the quotes. Use a new request id for every `rpc` or `tool` call, because the harness refuses an id the run already used. Do not `source` `$VCN_STATE/run.env` or `$OUT/run.env` in your own calls: bash runs every line of a file it sources, as you. `launch` appends version lines such as `agent-tty 0.5.0` to `$OUT/run.env`, and bash would run those as commands. Read any other value of the run with `$V get `, for example `OUT=$($V get OUT)`. A command substitution cuts the newlines at the end of a value, so a script that needs a path whole reads `IFS= read -r -d '' OUT < <($V get -z OUT)`. `get` answers only a name that `run.env` holds, parses no printed text, and runs the check that every `vcn.sh` command makes of `$VCN_STATE` before it sources `run.env` (it must be its own resolved path and a directory that this user owns, with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit). The five `journey-*.sh` scripts read `OUT` and `WORK` through `get`, so they make that check too, and an `OUT` that you exported does not change where they write. Export a `VCN_STATE` that your own `launch` printed, never one from an earlier or another session. Get the other values from the run: - `WORK` is `$VCN_STATE/work`, where `hello.txt` and `other.txt` live. - `$V doctor` prints the agent-tty session id (`SID`) in its `agent-tty session is running` line and the port of the plugin server (`PORT`) in its `plugin server is running on lock port ` line. The port is also the name of the lock file, `$VCN_STATE/claude/ide/.lock`, so `PORT=$(basename "$VCN_STATE"/claude/ide/*.lock .lock)` gives it while the server runs. @@ -52,7 +52,7 @@ Launch first runs `agent-tty doctor` and saves it to `$OUT/agent-tty-doctor.json - CI does not run the harness, on 0.8 or any other version. A run needs `agent-tty` from npm and Playwright Chromium (about 400 MB unpacked), and CI installs neither. Node is not the obstacle: the `unit-tests` job already gets the repo's Node 26 from mise. The two would add minutes and two more downloads to every PR. CI's `integration-tests (v0.8.0)` job already runs the plugin's integration tests on Neovim 0.8. After a change to `vcn.sh`, check the 0.8 path by hand: do the full run at the end of this file, with `VCN_NVIM=<0.8 nvim> $V launch` as its launch step. - `VCN_RTP=[:...]` adds plugin dirs to `runtimepath` after this checkout. A `terminal.provider = "snacks"` run needs a snacks.nvim clone there, because the harness installs no plugin. Pin the clone as [features/send-at-mention.md](features/send-at-mention.md) shows. A relative entry resolves against the directory you launch from, because nvim runs in `$WORK`, and symlinks are followed. Launch exits 1 for an entry that is not a directory, so a typo cannot pass as a snacks run on a native terminal. A float run is in [features/terminal-float-diff.md](features/terminal-float-diff.md). - `VCN_INIT_JSONRPC=` sets the `jsonrpc` field of the `initialize` request (default `2.0`). Only `scripts/proof-launch-refusals.sh` sets it, to get an error answer from the plugin. -- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`) (the dashboard command below runs `agent-tty` itself, with your `TMPDIR`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. `agent-tty` keeps every socket in the fixed dir `/tmp/agent-tty`, whatever `TMPDIR` says, and does not check who owns it, so another user who owns that dir or can rename entries in it could swap the socket dir of a run and answer every command. Launch makes `/tmp/agent-tty` with mode `0700` when it is missing, and refuses one that is a symlink, is owned by another user or is group- or world-writable (a `0755` dir of yours is fine). Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the five `journey-*.sh` scripts and the dashboard command source it without this check): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`. +- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`) (the dashboard command below runs `agent-tty` itself, with your `TMPDIR`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. `agent-tty` keeps every socket in the fixed dir `/tmp/agent-tty`, whatever `TMPDIR` says, and does not check who owns it, so another user who owns that dir or can rename entries in it could swap the socket dir of a run and answer every command. Launch makes `/tmp/agent-tty` with mode `0700` when it is missing, and refuses one that is a symlink, is owned by another user or is group- or world-writable (a `0755` dir of yours is fine). Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the journeys read through `get`, so they check it too): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`. - `VCN_SETUP=''` is deep-merged into `require("claudecode").setup()` over the base `{ terminal = { provider = "none" } }`. Example: `VCN_SETUP='{"diff_opts":{"layout":"unified"}}' $V launch`. - For a `log_level = "debug"` run, launch with `VCN_SETUP='{"log_level":"debug"}' $V launch --cmd 'set messagesopt=wait:0,history:10000' hello.txt`. Without it, one openDiff call at debug level parks Neovim at `Press ENTER`, and RPC stops answering. Launch arguments replace the default file, so name `hello.txt`. Neovim 0.8 has no `messagesopt`, so plain `set` fails launch with E518. Use `--cmd 'silent! set messagesopt=wait:0,history:10000'` there. Launch then works, but debug echoes still stop at `Press ENTER` (see Doctor). @@ -94,7 +94,7 @@ Rules: - After `Escape`, wait for `$V until 'mode()' n` before typing a `:` command. - After `FILE_SAVED`, Claude writes the file itself: write `result.content[1].text` to disk, then call `close_tab`. The plugin never writes it. - `$V until` confirms nvim state, not the screen. Use `$V capture` or `$V screenshot`, which wait for the screen, when the evidence is what the user sees. -- To watch live, a human runs `source "$VCN_STATE/run.env"; PATH="$NODE_DIR:$PATH" "$ATT_BIN" --home "$ATT_HOME" dashboard --session "$SID"` in a terminal. The dashboard is read-only and leaves the session size alone. +- To watch live, a human runs `$V dashboard` in a terminal, with `VCN_STATE` exported. The dashboard is read-only and leaves the session size alone. - agent-tty answers no DA1 (`ESC[c`) query. Neovim 0.12's TUI stops a `:suspend` only when the terminal answers its DA1 query, so in this harness `:suspend` and Ctrl-Z fire `VimSuspend` and detach the UI, but the TUI process never stops (state `S`, not `T`) and the screen stops updating while nvim keeps taking keys. Count `VimSuspend` events, and read buffer text through `$V expr`, instead of watching the process state or the screen. ## Evidence @@ -129,8 +129,9 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul - `scripts/vcn.sh` is the harness. `$V help` lists its subcommands. - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`. -- `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (the proof reads the source), a `run.env` without `JQ_BIN` still runs `jq`, a doc that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` in a code block (or in inline code) sets it in the same block (or the same doc, for inline code), because a fresh shell has none of them (`doc-vars`), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, and a command run with a `TMPDIR` that does not exist still works, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1. -- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes about 60 s. +- `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused (an absolute `NODE_DIR` that holds no node is not, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1. +- `scripts/proof-static.sh` proves two things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), and every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them. A code block is a fence of three or more backticks or tildes with any indent. A block or span that sources a `run.env` is left out of that check, and a comment that names such a source does not count. It also proves that no script and no recipe sources a `run.env` except `load` in `vcn.sh`. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `. +- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes about 60 s. - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`. - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`. - The `race` case puts a `mkdir` shim first on `PATH`. The shim plays another launch that makes the dir above `VERIFY_OUT` first, group-writable. Launch must refuse that dir in the check after `mkdir` and leave it in place. diff --git a/.agents/skills/verify-claudecode-nvim/features/README.md b/.agents/skills/verify-claudecode-nvim/features/README.md index 849376544..7936ce5e1 100644 --- a/.agents/skills/verify-claudecode-nvim/features/README.md +++ b/.agents/skills/verify-claudecode-nvim/features/README.md @@ -5,7 +5,7 @@ This directory is the maintained source for verifying the user-facing behavior o ## Baseline preconditions - Launch a fresh run with `.agents/skills/verify-claudecode-nvim/scripts/vcn.sh launch`. It opens `hello.txt` with the default config plus `terminal.provider = "none"`. -- Start every bash call with `export VCN_STATE='' OUT=''` (quoted as SKILL.md says); `WORK=$VCN_STATE/work; V=.agents/skills/verify-claudecode-nvim/scripts/vcn.sh`. Do not `source` a `run.env` in these calls (see SKILL.md). +- Start every bash call with `export VCN_STATE=''` (quoted as SKILL.md says); `V=.agents/skills/verify-claudecode-nvim/scripts/vcn.sh; OUT=$($V get OUT); WORK=$($V get WORK)`. Do not `source` a `run.env` in these calls (see SKILL.md). - `$WORK/hello.txt` is `alpha`, `beta`, `gamma` and `$WORK/other.txt` is `one`, `two`, `three`, `four`. - `$V doctor` reports nine `ok` lines, including `a client finished the WebSocket handshake`. - Never drive an nvim, agent-tty session, or lock file that this run did not start. diff --git a/.agents/skills/verify-claudecode-nvim/scripts/journey-diff-close-save.sh b/.agents/skills/verify-claudecode-nvim/scripts/journey-diff-close-save.sh index ada00de66..beaefd1bc 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/journey-diff-close-save.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/journey-diff-close-save.sh @@ -9,8 +9,10 @@ # `PASS` or `FAIL: of checks failed` last. Evidence lands in $OUT as diff-close-save-*. set -euo pipefail V="$(dirname "${BASH_SOURCE[0]}")/vcn.sh" -# shellcheck source=/dev/null -source "$VCN_STATE/run.env" +# Read OUT and WORK through vcn.sh get, which checks $VCN_STATE first. -z keeps a newline at the end of a path. +get() { IFS= read -r -d "" "$1" < <("$V" get -z "$1"); } +get OUT +get WORK target=${1:-existing} [[ $target == existing || $target == new ]] || { echo "usage: journey-diff-close-save.sh [existing|new]" >&2 diff --git a/.agents/skills/verify-claudecode-nvim/scripts/journey-new-tab-diff-mode.sh b/.agents/skills/verify-claudecode-nvim/scripts/journey-new-tab-diff-mode.sh index c2adca0e2..1e097313f 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/journey-new-tab-diff-mode.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/journey-new-tab-diff-mode.sh @@ -5,8 +5,10 @@ # Add "layout":"unified" to diff_opts for the unified layout. Evidence lands in $OUT as new-tab-diff-mode-*. set -euo pipefail V="$(dirname "${BASH_SOURCE[0]}")/vcn.sh" -# shellcheck source=/dev/null -source "$VCN_STATE/run.env" +# Read OUT and WORK through vcn.sh get, which checks $VCN_STATE first. -z keeps a newline at the end of a path. +get() { IFS= read -r -d "" "$1" < <("$V" get -z "$1"); } +get OUT +get WORK fail() { echo "FAIL: $*" >&2 diff --git a/.agents/skills/verify-claudecode-nvim/scripts/journey-opendiff-accept.sh b/.agents/skills/verify-claudecode-nvim/scripts/journey-opendiff-accept.sh index e9c1786b8..a6d62f89f 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/journey-opendiff-accept.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/journey-opendiff-accept.sh @@ -3,8 +3,10 @@ # Evidence lands in $OUT as opendiff-accept-*. set -euo pipefail V="$(dirname "${BASH_SOURCE[0]}")/vcn.sh" -# shellcheck source=/dev/null -source "$VCN_STATE/run.env" +# Read OUT and WORK through vcn.sh get, which checks $VCN_STATE first. -z keeps a newline at the end of a path. +get() { IFS= read -r -d "" "$1" < <("$V" get -z "$1"); } +get OUT +get WORK FILE="$WORK/hello.txt" TAB="✻ [Claude Code] hello.txt (vcn) ⧉" PROPOSED=$'alpha\nBETA\ngamma\n' diff --git a/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-diff.sh b/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-diff.sh index b9eaa95b4..cce7a620f 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-diff.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-diff.sh @@ -3,8 +3,10 @@ set -euo pipefail SCRIPTS="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" V="$SCRIPTS/vcn.sh" OBSERVE="$SCRIPTS/observe-windows.lua" -# shellcheck source=/dev/null -source "$VCN_STATE/run.env" +# Read OUT and WORK through vcn.sh get, which checks $VCN_STATE first. -z keeps a newline at the end of a path. +get() { IFS= read -r -d "" "$1" < <("$V" get -z "$1"); } +get OUT +get WORK TAB="✻ [Claude Code] hello.txt (float) ⧉" fail() { diff --git a/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-reload.sh b/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-reload.sh index 38ca49cea..9bf16be45 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-reload.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/journey-snacks-float-reload.sh @@ -7,8 +7,10 @@ set -euo pipefail SCRIPTS="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" V="$SCRIPTS/vcn.sh" OBSERVE="$SCRIPTS/observe-windows.lua" -# shellcheck source=/dev/null -source "$VCN_STATE/run.env" +# Read OUT and WORK through vcn.sh get, which checks $VCN_STATE first. -z keeps a newline at the end of a path. +get() { IFS= read -r -d "" "$1" < <("$V" get -z "$1"); } +get OUT +get WORK TAB="✻ [Claude Code] hello.txt (float-reload) ⧉" fail() { diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh index 3fcf077fd..594282dcd 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh @@ -9,12 +9,9 @@ # setsid-resolved a failing setsid on PATH and a working one that only `mise which setsid` names: a launch that # fails by itself still saves its failure screen and the final evidence, and runs `agent-tty home # forget`, all through the setsid that mise names -# no-bare-tools vcn.sh has no jq or setsid command except through $JQ_BIN and $SETSID_BIN (reads the source, so it -# reaches every call site, which the two cases above do not) -# doc-vars a code block, or the inline code of a doc, that expands PORT, SID, NVIM_PID or NODE_DIR sets it in -# the same block (or the same doc, for inline code), because a fresh shell has none of them. Prose -# that names an assignment sets nothing. # jq-old-run a run.env without JQ_BIN, as an older vcn.sh wrote it: a command resolves jq again +# node-dir a run.env whose NODE_DIR is empty, relative or has a colon is refused (att() would put the current dir, or +# a second dir, on PATH), and one whose NODE_DIR is an absolute dir without a node is not # state-resolved a VCN_STATE with a . or .. part, a symlink in its path, or a symlink as its last part is refused, not # sourced # state-slash a VCN_STATE with a trailing /, /. or //, or a .. after a symlink, is refused, not sourced @@ -29,6 +26,12 @@ # can write: launch accepts it, and after another user repoints the second symlink, `record` still # writes no byte of theirs into the evidence dir, because no agent-tty call of vcn.sh reads the caller's TMPDIR # tmp-later-tmpdir a command run with a TMPDIR that does not exist works: agent-tty makes its staging dirs in the state dir +# get-values `vcn.sh get` answers the values of a hand-made run.env exactly (a path with a space, an equals sign, quotes +# and a newline, also at its end with -z), and answers no name that run.env does not hold +# get-state `get` and each of the five journeys refuse a state dir that others can write, before they source its run.env +# journey-out journey-opendiff-accept.sh writes all its evidence into the OUT of its run, whatever VERIFY_OUT looks like +# (` OUT=` in the name, a newline in it or at its end) and whatever OUT the caller exported +# dashboard `vcn.sh dashboard` shows the running session in a terminal (script(1) stands in for one) # tmp-removed a run without $VCN_STATE/tmp, as an older vcn.sh left it, works: `record` makes the dir (0700) and writes a WebM # state-count a stat that answers for one dir fewer than the walk asked for (a shim drops the record of the loose # dir above the state dir) makes the walk refuse, not pass @@ -715,98 +718,6 @@ setsid_resolved_case() { cases=$((cases + 1)) } -# jq-resolved and setsid-resolved reach only the calls that a launch makes. This case reads the source: any word jq or -# setsid in a code line, except the two resolutions (`=$(bin jq)`, `=$(bin setsid)`), is a bare call and fails it. -bare_tools_case() { - local name=no-bare-tools hits site bare sites=0 word_re='(^|[^[:alnum:]_$-])(jq|setsid)($|[^[:alnum:]_-])' form - local strip_re='(JQ_BIN|SETSID_BIN)=\$\(bin (jq|setsid)\)' - local jq_ref='"$JQ_BIN"' setsid_ref='"$SETSID_BIN"' - while IFS= read -r site; do - for form in "" /usr/bin/ ./; do - bare=${site//"$jq_ref"/${form}jq} - bare=${bare//"$setsid_ref"/${form}setsid} - grep -qE "$word_re" <<<"$bare" || fail "$name" "the pattern misses this call written as a bare or path-qualified call: $bare" - done - sites=$((sites + 1)) - done < <(grep -E '"\$(JQ_BIN|SETSID_BIN)"' "$V" | grep -v 'env_line JQ_BIN') - ((sites > 0)) || fail "$name" "vcn.sh has no call through \$JQ_BIN or \$SETSID_BIN to check the pattern against" - sed -E "s/$strip_re//" <<<'jq --version; JQ_BIN=$(bin jq)' | grep -qE "$word_re" || fail "$name" "a bare jq on a line that ends with the resolution would pass" - hits=$(grep -n '' "$V" | grep -vE '^[0-9]+:[[:space:]]*#' | sed -E "s/$strip_re//" | grep -E "$word_re" || true) - [[ -z $hits ]] || fail "$name" "vcn.sh runs a bare or path-qualified jq or setsid: $(tr '\n' ' ' <<<"$hits")" - echo "ok $name: vcn.sh runs jq and setsid only through \$JQ_BIN and \$SETSID_BIN" - cases=$((cases + 1)) -} - -# A caller used to get PORT, SID, NVIM_PID and NODE_DIR from `source run.env`. A recipe that expands one of them must set -# it with `VAR=$(`, because a fresh shell has none. A recipe is a fenced code block (checked on its own) or an inline code -# span (all of them in a doc are checked together, because a bullet cites one assignment for the steps below it). Prose -# outside the backticks is not a recipe: it can name an assignment that no recipe runs. -# code_units : prints each fenced block, then the inline code spans outside the blocks, each unit ended by a line -# that holds only %%unit%%. A block or a span that sources a run.env sets every variable of the run by itself, so it is left -# out: it needs no `VAR=$(`, and it gives none to the other recipes. -code_units() { - awk 'function sources(text) { return text ~ /(^|[^A-Za-z0-9_.-])(source|\.)[ \t]+[^;#]*run\.env/ } - /^```/ { if (fenced) { if (!sources(block)) printf "%s", block; print "%%unit%%"; block = "" } fenced = !fenced; next } - fenced { block = block $0 "\n"; next } - { line = $0 - while (match(line, /`[^`]+`/)) { - span = substr(line, RSTART + 1, RLENGTH - 2) - if (!sources(span)) spans = spans span "\n" - line = substr(line, RSTART + RLENGTH) - } } - END { if (fenced) { if (!sources(block)) printf "%s", block; print "%%unit%%" } printf "%s%%%%unit%%%%\n", spans }' "$1" -} - -# units_missing : succeeds when a unit of the file expands and does not set it. -units_missing() { - local line unit="" uses_re='\$\{?'$2'([^A-Za-z0-9_]|$)' sets_re='(^|[^A-Za-z0-9_$])'$2'=\$\(' - while IFS= read -r line; do - if [[ $line != "%%unit%%" ]]; then - unit+=$line$'\n' - continue - fi - if grep -qE "$uses_re" <<<"$unit" && ! grep -qE "$sets_re" <<<"$unit"; then - return 0 - fi - unit="" - done < <(code_units "$1") - return 1 -} - -doc_vars_case() { - local name=doc-vars skill file var uses_re sets_re sample missing="" - skill=$(dirname "$V")/.. - sample=$TMP/doc-vars-sample.md - for var in PORT SID NVIM_PID NODE_DIR; do - uses_re='\$\{?'$var'([^A-Za-z0-9_]|$)' - sets_re='(^|[^A-Za-z0-9_$])'$var'=\$\(' - grep -qE "$uses_re" <<<"see \"\$$var.lock\" and \${$var}" || fail "$name" "the use pattern misses \$$var" - ! grep -qE "$uses_re" <<<"echo $var=\$CLAUDE_CODE_SSE_$var" || fail "$name" "the use pattern matches a longer name" - grep -qE "$sets_re" <<<"$var=\$(basename \"\$L\"/*.lock .lock)" || fail "$name" "the set pattern misses an assignment of $var" - ! grep -qE "$sets_re" <<<"echo $var=\$CLAUDE_CODE_SSE_$var" || fail "$name" "the set pattern matches text that sets nothing" - # Prose that names the assignment must not satisfy a block that uses the variable, and a block that sets it must. - printf 'Set it with %s=$(x) before.\n\n```bash\necho "$%s"\n```\n' "$var" "$var" >"$sample" - units_missing "$sample" "$var" || fail "$name" "a block that expands $var and sets it only in prose passed" - printf 'Prose.\n\n```bash\n%s=$(x)\necho "$%s"\n```\n' "$var" "$var" >"$sample" - ! units_missing "$sample" "$var" || fail "$name" "a block that sets $var before it expands it was flagged" - printf 'Set `%s=$(x)` first, then `echo "$%s"`.\n' "$var" "$var" >"$sample" - ! units_missing "$sample" "$var" || fail "$name" "inline code that sets $var for inline code that expands it was flagged" - printf 'Run `source "$VCN_STATE/run.env"; echo "$%s"`.\n\n```bash\n. "$VCN_STATE/run.env"\necho "$%s"\n```\n' "$var" "$var" >"$sample" - ! units_missing "$sample" "$var" || fail "$name" "a recipe that sources a run.env was flagged for $var" - printf 'Run `echo "$%s"`, as in `grep run.env x`.\n' "$var" >"$sample" - units_missing "$sample" "$var" || fail "$name" "a recipe that only names a run.env passed for $var" - printf 'Run `source "$VCN_STATE/run.env"` first, then `echo "$%s"`.\n' "$var" >"$sample" - units_missing "$sample" "$var" || fail "$name" "a source in one inline recipe set $var for another recipe" - for file in "$skill"/SKILL.md "$skill"/features/*.md; do - ! units_missing "$file" "$var" || missing+=" ${file#"$skill"/}:$var" - done - done - rm -f -- "$sample" - [[ -z $missing ]] || fail "$name" "a recipe expands a variable that it does not set:$missing" - echo "ok $name: every recipe that expands PORT, SID, NVIM_PID or NODE_DIR sets it" - cases=$((cases + 1)) -} - # The run.env of a run that an older vcn.sh started has no JQ_BIN. A command that needs jq must resolve it again. jq_old_run_case() { local name=jq-old-run dir out rc=0 @@ -821,6 +732,151 @@ jq_old_run_case() { cases=$((cases + 1)) } +# att() puts NODE_DIR in front of PATH. A command must refuse a run.env whose NODE_DIR would put the current dir (empty, relative) +# or a second dir (a colon) on PATH, and must not refuse an absolute dir that has lost its node, because cleanup has to run. +node_dir_case() { + local name=node-dir dir out rc val want + for val in "|it is not an absolute path" "bin|it is not an absolute path" "/usr/bin:/tmp|it has a colon, which PATH would split"; do + want=${val#*|} + val=${val%%|*} + dir=$(mktemp -d "$priv/vcn.XXXXXX") + printf 'VCN_STATE=%q\nOUT=%q\nNODE_DIR=%q\n' "$dir" "$TMP/out-$name" "$val" >"$dir/run.env" + rc=0 + out=$(env PATH="$base" VCN_STATE="$dir" "$V" doctor 2>&1) || rc=$? + ((rc == 1)) && [[ $out == *"NODE_DIR=$val in $dir/run.env is not usable: $want"* ]] || + fail "$name" "doctor with NODE_DIR='$val' exited $rc, wanted 1 with '$want': $out" + rm -rf -- "$dir" + done + mkdir "$TMP/no-node" + dir=$(mktemp -d "$priv/vcn.XXXXXX") + printf 'VCN_STATE=%q\nOUT=%q\nNODE_DIR=%q\n' "$dir" "$TMP/out-$name" "$TMP/no-node" >"$dir/run.env" + rc=0 + out=$(env PATH="$base" VCN_STATE="$dir" "$V" doctor 2>&1) || rc=$? + [[ $out != *"NODE_DIR="* ]] || fail "$name" "doctor refused an absolute NODE_DIR that holds no node: $out" + rm -rf -- "$dir" "$TMP/no-node" + echo "ok $name: an empty, relative or colon NODE_DIR was refused, and an absolute dir without a node was not" + cases=$((cases + 1)) +} + +# `vcn.sh get` reads a value of run.env after the check that every command makes, and the journeys use it in place of a source. +# The run.env of get_run_dir is hand-made, and its OUT holds a space, an equals sign, a tab, quotes and a newline (also at its end). +get_run_dir() { # : makes a state dir under $priv that holds NODE_DIR, WORK and the weird OUT + mkdir -p "$TMP/no-node" + printf 'VCN_STATE=%q\nOUT=%q\nWORK=%q\nNODE_DIR=%q\n' "$2" "$weird_out" "$2/work" "$TMP/no-node" >"$2/run.env" +} +get_values_case() { + local name=get-values dir got out rc + weird_out=$'/tmp/a b OUT=/x\t\'q"\nline2\n' + dir=$(mktemp -d "$priv/vcn.XXXXXX") + get_run_dir "$name" "$dir" + got=$(env PATH="$good_path" VCN_STATE="$dir" "$V" get WORK) || fail "$name" "get WORK failed" + [[ $got == "$dir/work" ]] || fail "$name" "get WORK printed '$got', not $dir/work" + got="" + IFS= read -r -d "" got < <(env PATH="$good_path" VCN_STATE="$dir" "$V" get -z OUT) || fail "$name" "get -z OUT printed no NUL end" + [[ $got == "$weird_out" ]] || fail "$name" "get -z OUT printed '$got', not the whole OUT" + got=$(env PATH="$good_path" VCN_STATE="$dir" "$V" get OUT) + [[ $got == "${weird_out%$'\n'}" ]] || fail "$name" "get OUT in a command substitution printed '$got'" + for got in PATH SID "a b" "" "OUT; touch $TMP/marker-$name"; do + rc=0 + out=$(env PATH="$good_path" VCN_STATE="$dir" "$V" get "$got" 2>&1) || rc=$? + ((rc == 1)) && [[ $out == "vcn: get: "* ]] || fail "$name" "get '$got' exited $rc with '$out', wanted 1 and a get: refusal" + done + [[ ! -e $TMP/marker-$name ]] || fail "$name" "get ran a name that it was given" + rc=0 + out=$(env PATH="$good_path" VCN_STATE="$dir" "$V" get 2>&1) || rc=$? + ((rc == 1)) || fail "$name" "get without a name exited $rc: $out" + rm -rf -- "$dir" "$TMP/no-node" + echo "ok $name: get printed WORK, OUT with -z whole, and refused PATH, a name that run.env lacks, a bad name and no name" + cases=$((cases + 1)) +} + +# A stale or foreign VCN_STATE is the input that the check exists for. A journey that sourced run.env ran it unchecked. get +# and every journey must stop at the check: the marker that the run.env touches stays away. +get_state_case() { + local name=get-state dir out rc journey cmd + weird_out=/tmp/x + dir=$(mktemp -d "$priv/vcn.XXXXXX") + get_run_dir "$name" "$dir" + printf 'touch %s\n' "$TMP/marker-$name" >>"$dir/run.env" + chmod 770 "$dir" + for journey in get "$(dirname "$V")"/journey-*.sh; do + if [[ $journey == get ]]; then cmd=("$V" get OUT); else cmd=("$journey"); fi + rc=0 + out=$(env PATH="$good_path" VCN_STATE="$dir" "${cmd[@]}" 2>&1) || rc=$? + [[ ! -e $TMP/marker-$name ]] || fail "$name" "${journey##*/} sourced the run.env of $dir" + ((rc == 1)) && [[ $out == *"refusing state dir $dir: it is group- or world-writable"* ]] || + fail "$name" "${journey##*/} exited $rc, wanted 1 with the refusal of $dir: $out" + done + rm -rf -- "$dir" "$TMP/no-node" + echo "ok $name: get and the five journeys refused a state dir that others can write, and its run.env was not sourced" + cases=$((cases + 1)) +} + +# journey-opendiff-accept.sh writes opendiff-accept-* files into OUT. A caller can export a stale OUT, and VERIFY_OUT can be a path +# that a parse of printed text gets wrong: ` OUT=` inside the name, a newline in it, or a newline at its end (a command +# substitution cuts that one). Each shape must end with every file in the OUT of its run and none in the other dirs. +journey_out_case() { + local name=journey-out shape want real jout n m stale=$TMP/stale-out else=$TMP/jo-else r + mkdir "$stale" "$else" + for shape in a1 newline nlend; do + case $shape in + a1) want="$TMP/jo-a1/run OUT=$else" ;; + newline) want="$TMP/jo-nl/first"$'\n'"second" ;; + nlend) want="$TMP/jo-nlend/dir"$'\n' ;; + esac + rc=0 + out=$(env -u XUM_SCRATCH_DIR -u VCN_AGENT_TTY PATH="$good_path" VERIFY_OUT="$want" TMPDIR="$priv" "$V" launch 2>&1) || rc=$? + state=$(sed -n 's/^VCN_STATE=//p' <<<"$out" | head -n 1) + ((rc == 0)) && [[ $state == "$priv"/vcn.?????? ]] || fail "$name" "launch with the $shape VERIFY_OUT exited $rc: $out" + live_state=$state live_path=$good_path + real="" + IFS= read -r -d "" real < <(env VCN_STATE="$state" "$V" get -z OUT) || true + [[ $real == "$want" ]] || fail "$name" "get OUT is not the VERIFY_OUT of the $shape launch" + r=0 + jout=$(env PATH="$good_path" VCN_STATE="$state" OUT="$stale" "$(dirname "$V")/journey-opendiff-accept.sh" 2>&1) || r=$? + n=$(find "$real" -maxdepth 1 -name 'opendiff-accept-*' -print0 | tr -cd '\0' | wc -c) + m=$(find "$else" "$stale" -type f -print0 | tr -cd '\0' | wc -c) + stop "$good_path" + ((r == 0 && n > 0 && m == 0)) || + fail "$name" "$shape: the journey exited $r with $n files in its OUT and $m in the other dirs: $(tail -n 3 <<<"$jout")" + find "$else" "$stale" -mindepth 1 -delete + done + echo "ok $name: the journey wrote its files into the OUT of the run for a VERIFY_OUT with OUT= in it, with a newline in it and at its end, and an exported stale OUT" + cases=$((cases + 1)) +} + +# The dashboard is a terminal program. script(1) gives it one, and the case checks that the running session (hello.txt) shows. +dashboard_case() { + local name=dashboard raw=$TMP/dashboard.raw spid kids k r=0 + command -v script >/dev/null || { + echo "SKIP $name: script(1) is not installed" + return 0 + } + launch "$name" "$good_path" + ((rc == 0)) || fail "$name" "launch exited $rc: $out" + env PATH="$good_path" VCN_STATE="$state" script -qfec "stty cols 160 rows 40; $V dashboard" /dev/null >"$raw" 2>&1 /dev/null || true + sleep 1 + for k in $kids; do + if [[ -d /proc/$k ]] && tr '\0' ' ' <"/proc/$k/cmdline" | grep -q 'dashboard'; then + kill "$k" + r=1 + fi + done + stop "$good_path" + sed 's/\x1b\[[0-9;?]*[A-Za-z]//g; s/\x1b[()][A-Z0-9]//g' "$raw" | tr -d '\r' >"$raw.txt" + if ! grep -q alpha "$raw.txt" || ! grep -q gamma "$raw.txt"; then + fail "$name" "the dashboard did not show the text of hello.txt: $(head -c 300 "$raw.txt")" + fi + ((r == 0)) || fail "$name" "a dashboard process was still alive after its terminal ended (stopped now)" + echo "ok $name: vcn.sh dashboard showed the running session in a terminal and left no process" + cases=$((cases + 1)) +} + # refuses_state [wrapper...]: `vcn.sh cleanup`, run through the wrapper, must exit 1 with # and must not source the run.env in , which touches $TMP/marker-. refuses_state() { @@ -1178,9 +1234,8 @@ signal_failed_case signal_gap_case cleanup_no_agent_tty_case setsid_resolved_case -bare_tools_case -doc_vars_case jq_old_run_case +node_dir_case state_resolved_case state_slash_case state_mode_case @@ -1196,6 +1251,10 @@ state_ancestor_case tmp_multihop_case tmp_later_case tmp_removed_case +get_values_case +get_state_case +journey_out_case +dashboard_case signal_symlink_case sigterm_case echo "CASES $cases" diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh index de185cce9..d47c6118f 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh @@ -23,6 +23,7 @@ # leads to a safe dir: the resolved path is read with its newline # tmp-load-refused mktemp answers with a path that is not its own resolved path (a // in it): load refuses the new state dir, # and launch leaves no state dir and no evidence dir +# node-relative node is found through a relative PATH entry (no mise): its dir would go on PATH in every agent-tty call # tmp-root TMPDIR is /: launch gives mktemp /vcn.XXXXXX, not //vcn.XXXXXX (a mktemp shim stops launch and prints it) # tmp-space a dir above TMPDIR that others can write has a name that ends in a space # out-space the same above VERIFY_OUT @@ -50,7 +51,7 @@ # Prints PASS per case, or FAIL: and exits 1. The init case's evidence dir is # deleted when every case passes, and kept with its path printed when one fails. set -euo pipefail -V="$(dirname "${BASH_SOURCE[0]}")/vcn.sh" +V="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)/vcn.sh" # Resolved, because launch prints the state dir under the resolved path of TMPDIR. TMP=$(realpath -- "$(mktemp -d)") init_out="" @@ -143,6 +144,17 @@ refused tmp-dot "TMPDIR=$TMP/dd/./y has a . or .. part" TMPDIR="$TMP/dd/./y" VER mkdir "$TMP/mktemp-bin" printf '#!/bin/sh\necho "mktemp shim: template=$2" >&2\nexit 1\n' >"$TMP/mktemp-bin/mktemp" chmod +x "$TMP/mktemp-bin/mktemp" +# launch resolves node itself. Without mise, `command -v node` prints a relative path for a relative PATH entry, and the dir of that +# path would go in front of PATH in every agent-tty call. Launch refuses before it makes anything. +mkdir -m 700 "$TMP/relnode" "$TMP/relnode/nb" "$TMP/relnode/t" +printf '#!/bin/sh\nexit 0\n' >"$TMP/relnode/nb/node" +chmod +x "$TMP/relnode/nb/node" +nvim_dir=$(dirname -- "$(mise which nvim 2>/dev/null || command -v nvim)") +( + cd "$TMP/relnode" + refused node-relative "node is at ./nb/node, and its dir is not usable: it is not an absolute path" \ + PATH="./nb:$nvim_dir:/usr/bin:/bin" VCN_AGENT_TTY=/usr/bin/true TMPDIR="$TMP/relnode/t" VERIFY_OUT="$TMP/relnode/o" +) refused tmp-root "mktemp shim: template=/vcn.XXXXXX" PATH="$TMP/mktemp-bin:$PATH" TMPDIR=/ VERIFY_OUT="$TMP/tmp-out" # mktemp gets the resolved path. The path as given must pass the same walk, which is main's rule: the symlink itself, its # owner and the dirs above it. diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh new file mode 100755 index 000000000..edc11ea9f --- /dev/null +++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh @@ -0,0 +1,208 @@ +#!/usr/bin/env bash +# Static proofs of the verify-claudecode-nvim skill. They read the skill's own files and start no run, no agent-tty and no nvim, +# so `mise run check` runs them in CI: +# no-bare-tools vcn.sh has no jq or setsid command except through $JQ_BIN and $SETSID_BIN, not even as the default of a +# parameter expansion (reads the source, so it reaches every call site, which a run of launch does not) +# doc-vars a code block, or the inline code of a doc, that expands PORT, SID, NVIM_PID or NODE_DIR sets it in the same +# block (or the same doc, for inline code), because a fresh shell has none of them. Prose that names an +# assignment sets nothing, and neither does a comment +# no-source-run-env no script of the skill, and no recipe in its docs, sources a run.env, except `load` in vcn.sh, which checks the +# state dir first (the callers read a value through `vcn.sh get`) +# Prints one `ok ` per case, or `FAIL : ` and exits 1, and ends with `CASES `. +set -euo pipefail +V="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)/vcn.sh" +TMP=$(mktemp -d) +trap 'rm -rf "$TMP"' EXIT +cases=0 + +fail() { + echo "FAIL $1: $2" >&2 + exit 1 +} + +# jq-resolved and setsid-resolved reach only the calls that a launch makes. This case reads the source: any word jq or setsid +# in a code line, except the two resolutions (`=$(bin jq)`, `=$(bin setsid)`), is a bare call and fails it. A default in a +# parameter expansion (`${JQ_BIN:-jq}`) names the tool as bare as a call does, and the word pattern skips it on purpose, because +# a name with a hyphen before it (`mise-jq`) is not a call. +bare_tools_case() { + local name=no-bare-tools hits site bare sites=0 word_re='(^|[^[:alnum:]_$-])(jq|setsid)($|[^[:alnum:]_-])' form + local default_re='\$\{[A-Za-z_][A-Za-z0-9_]*:?[-=+?](jq|setsid)\}' + local strip_re='(JQ_BIN|SETSID_BIN)=\$\(bin (jq|setsid)\)' + local jq_ref='"$JQ_BIN"' setsid_ref='"$SETSID_BIN"' + while IFS= read -r site; do + for form in "" /usr/bin/ ./; do + bare=${site//"$jq_ref"/${form}jq} + bare=${bare//"$setsid_ref"/${form}setsid} + grep -qE "$word_re" <<<"$bare" || fail "$name" "the pattern misses this call written as a bare or path-qualified call: $bare" + done + sites=$((sites + 1)) + done < <(grep -E '"\$(JQ_BIN|SETSID_BIN)"' "$V" | grep -v 'env_line JQ_BIN') + ((sites > 0)) || fail "$name" "vcn.sh has no call through \$JQ_BIN or \$SETSID_BIN to check the pattern against" + sed -E "s/$strip_re//" <<<'jq --version; JQ_BIN=$(bin jq)' | grep -qE "$word_re" || fail "$name" "a bare jq on a line that ends with the resolution would pass" + for bare in '"${JQ_BIN:-jq}" -n 1' 'x=${SETSID_BIN=setsid}' '${JQ_BIN-jq}'; do + grep -qE "$default_re" <<<"$bare" || fail "$name" "the default pattern misses $bare" + done + ! grep -qE "$default_re" <<<'"$JQ_BIN" -n "${JQ_BIN:-x}"' || fail "$name" "the default pattern matches a call through \$JQ_BIN" + hits=$(grep -n '' "$V" | grep -vE '^[0-9]+:[[:space:]]*#' | sed -E "s/$strip_re//" | grep -E "$word_re|$default_re" || true) + [[ -z $hits ]] || fail "$name" "vcn.sh runs a bare or path-qualified jq or setsid: $(tr '\n' ' ' <<<"$hits")" + echo "ok $name: vcn.sh runs jq and setsid only through \$JQ_BIN and \$SETSID_BIN" + cases=$((cases + 1)) +} + +# A caller used to get PORT, SID, NVIM_PID and NODE_DIR from `source run.env`. A recipe that expands one of them must set it with +# `VAR=$(`, because a fresh shell has none. A recipe is a fenced code block (checked on its own) or an inline code span (all of +# them in a doc are checked together, because a bullet cites one assignment for the steps below it). Prose outside the backticks +# is not a recipe: it can name an assignment that no recipe runs. +# A fence is three or more backticks or tildes with any indent, closed by a line of the same character, at least as long. +# code_units [1]: prints each fenced block, then the inline code spans outside the blocks, each unit ended by a line that +# holds only %%unit%%. A block or a span that sources a run.env sets every variable of the run by itself, so it is left out: it +# needs no `VAR=$(`, and it gives none to the other recipes. With a 1, it prints only those units that source. A comment that +# names such a source is no source. +code_units() { + awk -v want="${2:-0}" 'function emit(text) { if ((sources(text) ? 1 : 0) == want) printf "%s", text } + function run_len(t, ch, n) { n = 0; while (substr(t, n + 1, 1) == ch) n++; return n } + function sources(text, n, i, rows, row) { + n = split(text, rows, "\n") + for (i = 1; i <= n; i++) { + row = rows[i] + sub(/^[ \t]*#.*/, "", row) + sub(/[ \t]#.*$/, "", row) + if (row ~ /(^|[^A-Za-z0-9_.-])(source|\.)[ \t]+[^;#]*run\.env/) return 1 + } + return 0 + } + { t = $0; sub(/^[ \t]+/, "", t) } + fenced { + n = run_len(t, fch) + if (n >= flen && substr(t, n + 1) ~ /^[ \t]*$/) { + emit(block) + print "%%unit%%" + block = "" + fenced = 0 + next + } + block = block $0 "\n" + next + } + { c = substr(t, 1, 1) } + (c == "`" || c == "~") && run_len(t, c) >= 3 { fenced = 1; fch = c; flen = run_len(t, c); next } + { line = $0 + while (match(line, /`[^`]+`/)) { + span = substr(line, RSTART + 1, RLENGTH - 2) + if ((sources(span) ? 1 : 0) == want) spans = spans span "\n" + line = substr(line, RSTART + RLENGTH) + } } + END { if (fenced) { emit(block); print "%%unit%%" } printf "%s%%%%unit%%%%\n", spans }' "$1" +} + +# The two patterns that decide whether a unit expands a variable and whether it sets it. units_missing and the self-test below +# both call these, so a change to one is a change to what the self-test checks. +var_uses_re() { printf '%s' '\$\{?'"$1"'([^A-Za-z0-9_]|$)'; } +var_sets_re() { printf '%s' '(^|[^A-Za-z0-9_$])'"$1"'=\$\('; } + +# units_missing : succeeds when a unit of the file expands and does not set it. +units_missing() { + local line unit="" uses_re sets_re + uses_re=$(var_uses_re "$2") + sets_re=$(var_sets_re "$2") + while IFS= read -r line; do + if [[ $line != "%%unit%%" ]]; then + unit+=$line$'\n' + continue + fi + if grep -qE "$uses_re" <<<"$unit" && ! grep -qE "$sets_re" <<<"$unit"; then + return 0 + fi + unit="" + done < <(code_units "$1") + return 1 +} + +doc_vars_case() { + local name=doc-vars skill file var uses_re sets_re sample missing="" fence + skill=$(dirname "$V")/.. + sample=$TMP/doc-vars-sample.md + for var in PORT SID NVIM_PID NODE_DIR; do + uses_re=$(var_uses_re "$var") + sets_re=$(var_sets_re "$var") + grep -qE "$uses_re" <<<"see \"\$$var.lock\" and \${$var}" || fail "$name" "the use pattern misses \$$var" + ! grep -qE "$uses_re" <<<"echo $var=\$CLAUDE_CODE_SSE_$var" || fail "$name" "the use pattern matches a longer name" + grep -qE "$sets_re" <<<"$var=\$(basename \"\$L\"/*.lock .lock)" || fail "$name" "the set pattern misses an assignment of $var" + grep -qE "$sets_re" <<<"export $var=\$(x)" || fail "$name" "the set pattern misses an exported assignment of $var" + ! grep -qE "$sets_re" <<<"echo $var=\$CLAUDE_CODE_SSE_$var" || fail "$name" "the set pattern matches text that sets nothing" + ! grep -qE "$sets_re" <<<"X_$var=\$(x)" || fail "$name" "the set pattern matches an assignment of a longer name" + ! grep -qE "$sets_re" <<<"$var=literal" || fail "$name" "the set pattern matches an assignment that runs nothing" + # Prose that names the assignment must not satisfy a block that uses the variable, and a block that sets it must. + printf 'Set it with %s=$(x) before.\n\n```bash\necho "$%s"\n```\n' "$var" "$var" >"$sample" + units_missing "$sample" "$var" || fail "$name" "a block that expands $var and sets it only in prose passed" + printf 'Prose.\n\n```bash\n%s=$(x)\necho "$%s"\n```\n' "$var" "$var" >"$sample" + ! units_missing "$sample" "$var" || fail "$name" "a block that sets $var before it expands it was flagged" + printf '```bash\n%s=literal\nX_%s=$(x)\necho "$%s"\n```\n' "$var" "$var" "$var" >"$sample" + units_missing "$sample" "$var" || fail "$name" "a block that sets $var to a literal, or sets a longer name, passed as a block that sets $var" + # Every spelling of a fence is a block: indented, tildes, and four backticks around a block that holds three. + for fence in '```' ' ```bash' '~~~' ' ~~~sh' '````'; do + printf 'Prose.\n\n%s\necho "$%s"\n%s\n' "$fence" "$var" "${fence//[^\`~]/}" >"$sample" + units_missing "$sample" "$var" || fail "$name" "a block opened by '$fence' that expands $var and sets nothing passed" + printf 'Prose.\n\n%s\n%s=$(x)\necho "$%s"\n%s\n' "$fence" "$var" "$var" "${fence//[^\`~]/}" >"$sample" + ! units_missing "$sample" "$var" || fail "$name" "a block opened by '$fence' that sets $var was flagged" + done + printf 'Prose.\n\n````\n```\necho "$%s"\n```\n````\n' "$var" >"$sample" + units_missing "$sample" "$var" || fail "$name" "three backticks inside a four-backtick block closed it, so the use of $var passed" + printf 'Set `%s=$(x)` first, then `echo "$%s"`.\n' "$var" "$var" >"$sample" + ! units_missing "$sample" "$var" || fail "$name" "inline code that sets $var for inline code that expands it was flagged" + printf 'Run `source "$VCN_STATE/run.env"; echo "$%s"`.\n\n```bash\n. "$VCN_STATE/run.env"\necho "$%s"\n```\n' "$var" "$var" >"$sample" + ! units_missing "$sample" "$var" || fail "$name" "a recipe that sources a run.env was flagged for $var" + printf 'Run `echo "$%s"`, as in `grep run.env x`.\n' "$var" >"$sample" + units_missing "$sample" "$var" || fail "$name" "a recipe that only names a run.env passed for $var" + printf '```bash\n# source "$VCN_STATE/run.env" first\necho "$%s"\n```\n' "$var" >"$sample" + units_missing "$sample" "$var" || fail "$name" "a comment that names a source of run.env exempted a block that expands $var" + printf '```bash\necho "$%s" # source run.env\n```\n' "$var" >"$sample" + units_missing "$sample" "$var" || fail "$name" "a trailing comment that names a source of run.env exempted a block that expands $var" + printf 'Run `source "$VCN_STATE/run.env"` first, then `echo "$%s"`.\n' "$var" >"$sample" + units_missing "$sample" "$var" || fail "$name" "a source in one inline recipe set $var for another recipe" + for file in "$skill"/SKILL.md "$skill"/features/*.md; do + ! units_missing "$file" "$var" || missing+=" ${file#"$skill"/}:$var" + done + done + rm -f -- "$sample" + [[ -z $missing ]] || fail "$name" "a recipe expands a variable that it does not set:$missing" + echo "ok $name: every recipe that expands PORT, SID, NVIM_PID or NODE_DIR sets it" + cases=$((cases + 1)) +} + +# sourcing_units : the units of the file that source a run.env. +sourcing_units() { code_units "$1" 1 | grep -v '^%%unit%%$' || true; } + +# The callers of a run moved to `vcn.sh get` and `vcn.sh dashboard`. A source of run.env in the skill's own scripts runs every +# line of the file with no check of the state dir, and one in a doc teaches a caller to do it. Only `load` in vcn.sh sources it. +no_source_case() { + local name=no-source-run-env skill file hits sample=$TMP/no-source.md src_re='(^|[;&|({])[[:space:]]*(source|\.)[[:space:]]+[^;#`]*run\.env' n + skill=$(dirname "$V")/.. + printf 'Run:\n\n```bash\nsource "$VCN_STATE/run.env"\n```\n' >"$sample" + [[ -n $(sourcing_units "$sample") ]] || fail "$name" "a fenced block that sources a run.env was not found" + printf 'Run:\n\n ~~~\n. "$OUT/run.env"\n ~~~\n' >"$sample" + [[ -n $(sourcing_units "$sample") ]] || fail "$name" "an indented ~~~ block that sources a run.env was not found" + printf 'Run `source "$VCN_STATE/run.env"; echo`.\n' >"$sample" + [[ -n $(sourcing_units "$sample") ]] || fail "$name" "an inline span that sources a run.env was not found" + printf 'Do not `source` `$VCN_STATE/run.env`.\n\n```bash\n# source run.env\necho x\n```\n' >"$sample" + [[ -z $(sourcing_units "$sample") ]] || fail "$name" "prose or a comment that names a source was taken for one" + rm -f -- "$sample" + for file in "$skill"/SKILL.md "$skill"/features/*.md; do + hits=$(sourcing_units "$file") + [[ -z $hits ]] || fail "$name" "${file#"$skill"/} has a recipe that sources a run.env: $(tr '\n' ' ' <<<"$hits")" + done + for file in "$skill"/scripts/*.sh; do + [[ ${file##*/} != vcn.sh ]] || continue + hits=$(grep -nE "$src_re" "$file" | grep -vE '^[0-9]+:[[:space:]]*#' || true) + [[ -z $hits ]] || fail "$name" "${file#"$skill"/} sources a run.env: $(tr '\n' ' ' <<<"$hits")" + done + n=$(grep -E "$src_re" "$V" | grep -cvE '^[[:space:]]*#' || true) + ((n == 1)) || fail "$name" "vcn.sh sources a run.env in $n places, wanted one (load)" + echo "ok $name: only load in vcn.sh sources a run.env; no script and no recipe does" + cases=$((cases + 1)) +} + +bare_tools_case +doc_vars_case +no_source_case +echo "CASES $cases" diff --git a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh index a9559161f..97b3864c3 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh @@ -15,6 +15,9 @@ # record save a WebM of the session so far to $OUT/.webm and print its path # connect start one more client, named by VCN_CLIENT, and finish its handshake # disconnect kill the client VCN_CLIENT names (unset: the launch client) +# get [-z] print one value of run.env (OUT, WORK, SID, PORT, ...) after the check that every command makes; -z +# ends it with a NUL, so `read -r -d ""` keeps a newline at its end +# dashboard show the session live (agent-tty dashboard): run it in a terminal # cleanup stop everything this run started, delete VCN_STATE, keep $OUT # VCN_CLIENT= makes rpc, tool, await, connect and disconnect act as that client. # VCN_AGENT_TTY= makes launch run that agent-tty (default: the first agent-tty on PATH, then mise's, that @@ -74,6 +77,16 @@ unsafe_state() { fi } +# att() puts NODE_DIR in front of PATH. An empty or relative one puts the current dir on PATH, and a colon adds a second entry. A +# dir that has lost its node since launch is not refused here: cleanup must still run. Prints why is no good, or nothing. +bad_node_dir() { + if [[ $1 != /* ]]; then + echo "it is not an absolute path" + elif [[ $1 == *:* ]]; then + echo "it has a colon, which PATH would split" + fi +} + load() { local why [[ -n ${VCN_STATE-} ]] || die "VCN_STATE is not set (launch prints it)" @@ -87,6 +100,8 @@ load() { [[ -z ${VCN_CLIENT-} || $VCN_CLIENT =~ ^[a-z0-9]+$ ]] || die "VCN_CLIENT must match [a-z0-9]+" # shellcheck source=/dev/null source "$VCN_STATE/run.env" + why=$(bad_node_dir "${NODE_DIR-}") + [[ -z $why ]] || die "NODE_DIR=${NODE_DIR-} in $VCN_STATE/run.env is not usable: $why" # A run that an older vcn.sh started has no JQ_BIN. [[ -n ${JQ_BIN-} ]] || JQ_BIN=$(bin jq) } @@ -477,6 +492,27 @@ cmd_connect() { echo "client $VCN_CLIENT connected; its messages are in $OUT/ws-out$(chan).jsonl and $OUT/ws-in$(chan).jsonl" } +# A caller that sources run.env runs every line of it in its own shell, with no check of $VCN_STATE. A value read through get +# comes from the run.env that load has checked, and the caller parses no printed text: a path can hold a space, an equals sign or +# a newline. Only a name that run.env holds is answered, so get cannot be used to read the rest of the environment. +cmd_get() { + local nul="" name + if [[ ${1-} == -z ]]; then + nul=1 + shift + fi + (($# == 1)) || die "get needs one name: get [-z] " + name=$1 + [[ $name =~ ^[A-Za-z][A-Za-z0-9_]*$ ]] || die "get: $name is not the name of a value of run.env" + grep -q -- "^$name=" "$VCN_STATE/run.env" || die "get: run.env of this run holds no $name" + if [[ -n $nul ]]; then printf '%s\0' "${!name}"; else printf '%s\n' "${!name}"; fi +} + +cmd_dashboard() { + [[ -n ${SID-} ]] || die "this run has no agent-tty session" + att dashboard --session "$SID" +} + # Kill a client by its recorded PID, the way a Claude CLI that exits drops its socket. cmd_disconnect() { local var @@ -502,6 +538,8 @@ cmd_launch() { mapfile -t att_cands <<<"$att_cands" VCN_RTP=$(rtp_dirs) node_exe=$(bin node) + why=$(bad_node_dir "$(dirname -- "$node_exe")") + [[ -z $why ]] || die "node is at $node_exe, and its dir is not usable: $why" # Every call runs these paths, not the bare names: another setsid or jq earlier on PATH could differ or fail. SETSID_BIN=$(bin setsid) JQ_BIN=$(bin jq) @@ -688,7 +726,7 @@ launch) cmd_launch "$@" ;; cleanup) cmd_cleanup ;; -doctor | keys | expr | until | rpc | tool | await | capture | screenshot | record | connect | disconnect) +doctor | keys | expr | until | rpc | tool | await | capture | screenshot | record | connect | disconnect | get | dashboard) load c=$1 shift @@ -708,6 +746,8 @@ doctor | keys | expr | until | rpc | tool | await | capture | screenshot | recor record) cmd_record "$1" ;; connect) cmd_connect ;; disconnect) cmd_disconnect ;; + get) cmd_get "$@" ;; + dashboard) cmd_dashboard ;; esac ;; help | -h | --help) diff --git a/mise.toml b/mise.toml index 89c46d142..6bde116a3 100644 --- a/mise.toml +++ b/mise.toml @@ -102,7 +102,7 @@ done ''' [tasks.check] -description = "Check Lua syntax and run luacheck" +description = "Check Lua syntax, run luacheck, and run the static proofs of the verify skill" depends = ["setup"] run = ''' echo "Checking Lua files for syntax errors..." @@ -111,6 +111,8 @@ echo "Checking Lua files for syntax errors..." find lua -name "*.lua" -type f -print0 | xargs -0 -I{} luajit -e "assert(loadfile('{}'))" echo "Running luacheck..." ./.luarocks/bin/luacheck lua/ tests/ --no-unused-args --no-max-line-length +echo "Running the static proofs of the verify-claudecode-nvim skill..." +bash .agents/skills/verify-claudecode-nvim/scripts/proof-static.sh ''' [tasks.test] From cee2881113d7397df39247a73d08980d90a55e47 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 12 Nov 2026 03:46:20 +0000 Subject: [PATCH 4/9] fix(skills): check NODE_DIR only where it is set, and tighten the new checks MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An independent review of the previous commit found, by reading, that load refused a run.env that has no NODE_DIR at all. The hand-made run.env files of cleanup-no-agent-tty and jq-old-run have none, so a full run of the resolution proof stopped at the first of them. load now checks NODE_DIR when it is set (an empty value is set, and refused). A run.env that launch left half written stays cleanable, and nothing runs agent-tty for it, because SID and ATT_BIN are written after NODE_DIR. - SKILL.md no longer says that the dashboard command runs agent-tty with the caller's TMPDIR: it goes through att(). It counts three proofs in proof-static.sh, not two. - unsafe_dir takes the label for the dirs above, so a /tmp that others can write says "above the agent-tty socket dir". The refusal names `chmod go-w /tmp/agent-tty` for a mode that agent-tty made under umask 002. - no-source-run-env finds a source after if, then, do, else, elif, while, until and !, not only after ; & | ( {. A self-test holds lines that must and must not match. - no-bare-tools runs the scan of a file (bare_hits) on a sample, so dropping the default pattern from the scan fails the case, not only a pattern test. - node-relative puts a failing mise first on PATH: a mise in /usr/bin would otherwise answer with an absolute path and the case would not reach its refusal. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_ --- .../skills/verify-claudecode-nvim/SKILL.md | 4 +-- .../scripts/proof-launch-refusals.sh | 12 ++++--- .../scripts/proof-static.sh | 34 +++++++++++++++---- .../verify-claudecode-nvim/scripts/vcn.sh | 13 ++++--- 4 files changed, 45 insertions(+), 18 deletions(-) diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md index ee7a6eaa6..fbdfcc982 100644 --- a/.agents/skills/verify-claudecode-nvim/SKILL.md +++ b/.agents/skills/verify-claudecode-nvim/SKILL.md @@ -52,7 +52,7 @@ Launch first runs `agent-tty doctor` and saves it to `$OUT/agent-tty-doctor.json - CI does not run the harness, on 0.8 or any other version. A run needs `agent-tty` from npm and Playwright Chromium (about 400 MB unpacked), and CI installs neither. Node is not the obstacle: the `unit-tests` job already gets the repo's Node 26 from mise. The two would add minutes and two more downloads to every PR. CI's `integration-tests (v0.8.0)` job already runs the plugin's integration tests on Neovim 0.8. After a change to `vcn.sh`, check the 0.8 path by hand: do the full run at the end of this file, with `VCN_NVIM=<0.8 nvim> $V launch` as its launch step. - `VCN_RTP=[:...]` adds plugin dirs to `runtimepath` after this checkout. A `terminal.provider = "snacks"` run needs a snacks.nvim clone there, because the harness installs no plugin. Pin the clone as [features/send-at-mention.md](features/send-at-mention.md) shows. A relative entry resolves against the directory you launch from, because nvim runs in `$WORK`, and symlinks are followed. Launch exits 1 for an entry that is not a directory, so a typo cannot pass as a snacks run on a native terminal. A float run is in [features/terminal-float-diff.md](features/terminal-float-diff.md). - `VCN_INIT_JSONRPC=` sets the `jsonrpc` field of the `initialize` request (default `2.0`). Only `scripts/proof-launch-refusals.sh` sets it, to get an error answer from the plugin. -- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`) (the dashboard command below runs `agent-tty` itself, with your `TMPDIR`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. `agent-tty` keeps every socket in the fixed dir `/tmp/agent-tty`, whatever `TMPDIR` says, and does not check who owns it, so another user who owns that dir or can rename entries in it could swap the socket dir of a run and answer every command. Launch makes `/tmp/agent-tty` with mode `0700` when it is missing, and refuses one that is a symlink, is owned by another user or is group- or world-writable (a `0755` dir of yours is fine). Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the journeys read through `get`, so they check it too): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`. +- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. `agent-tty` keeps every socket in the fixed dir `/tmp/agent-tty`, whatever `TMPDIR` says, and does not check who owns it, so another user who owns that dir or can rename entries in it could swap the socket dir of a run and answer every command. Launch makes `/tmp/agent-tty` with mode `0700` when it is missing, and refuses one that is a symlink, is owned by another user or is group- or world-writable (a `0755` dir of yours is fine). Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the journeys read through `get`, so they check it too): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`. - `VCN_SETUP=''` is deep-merged into `require("claudecode").setup()` over the base `{ terminal = { provider = "none" } }`. Example: `VCN_SETUP='{"diff_opts":{"layout":"unified"}}' $V launch`. - For a `log_level = "debug"` run, launch with `VCN_SETUP='{"log_level":"debug"}' $V launch --cmd 'set messagesopt=wait:0,history:10000' hello.txt`. Without it, one openDiff call at debug level parks Neovim at `Press ENTER`, and RPC stops answering. Launch arguments replace the default file, so name `hello.txt`. Neovim 0.8 has no `messagesopt`, so plain `set` fails launch with E518. Use `--cmd 'silent! set messagesopt=wait:0,history:10000'` there. Launch then works, but debug echoes still stop at `Press ENTER` (see Doctor). @@ -130,7 +130,7 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul - `scripts/vcn.sh` is the harness. `$V help` lists its subcommands. - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`. - `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused (an absolute `NODE_DIR` that holds no node is not, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1. -- `scripts/proof-static.sh` proves two things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), and every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them. A code block is a fence of three or more backticks or tildes with any indent. A block or span that sources a `run.env` is left out of that check, and a comment that names such a source does not count. It also proves that no script and no recipe sources a `run.env` except `load` in `vcn.sh`. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `. +- `scripts/proof-static.sh` proves three things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), and every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them. A code block is a fence of three or more backticks or tildes with any indent. A block or span that sources a `run.env` is left out of that check, and a comment that names such a source does not count. It also proves that no script and no recipe sources a `run.env` except `load` in `vcn.sh`. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `. - `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes about 60 s. - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`. - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`. diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh index d47c6118f..33a98eba6 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh @@ -144,16 +144,18 @@ refused tmp-dot "TMPDIR=$TMP/dd/./y has a . or .. part" TMPDIR="$TMP/dd/./y" VER mkdir "$TMP/mktemp-bin" printf '#!/bin/sh\necho "mktemp shim: template=$2" >&2\nexit 1\n' >"$TMP/mktemp-bin/mktemp" chmod +x "$TMP/mktemp-bin/mktemp" -# launch resolves node itself. Without mise, `command -v node` prints a relative path for a relative PATH entry, and the dir of that -# path would go in front of PATH in every agent-tty call. Launch refuses before it makes anything. -mkdir -m 700 "$TMP/relnode" "$TMP/relnode/nb" "$TMP/relnode/t" +# launch resolves node itself. Without mise (a shim that fails stands in, whatever /usr/bin holds), `command -v node` prints a +# relative path for a relative PATH entry, and the dir of that path would go in front of PATH in every agent-tty call. Launch +# refuses before it makes anything. +mkdir -m 700 "$TMP/relnode" "$TMP/relnode/nb" "$TMP/relnode/t" "$TMP/relnode/nomise" printf '#!/bin/sh\nexit 0\n' >"$TMP/relnode/nb/node" -chmod +x "$TMP/relnode/nb/node" +printf '#!/bin/sh\nexit 1\n' >"$TMP/relnode/nomise/mise" +chmod +x "$TMP/relnode/nb/node" "$TMP/relnode/nomise/mise" nvim_dir=$(dirname -- "$(mise which nvim 2>/dev/null || command -v nvim)") ( cd "$TMP/relnode" refused node-relative "node is at ./nb/node, and its dir is not usable: it is not an absolute path" \ - PATH="./nb:$nvim_dir:/usr/bin:/bin" VCN_AGENT_TTY=/usr/bin/true TMPDIR="$TMP/relnode/t" VERIFY_OUT="$TMP/relnode/o" + PATH="./nb:$TMP/relnode/nomise:$nvim_dir:/usr/bin:/bin" VCN_AGENT_TTY=/usr/bin/true TMPDIR="$TMP/relnode/t" VERIFY_OUT="$TMP/relnode/o" ) refused tmp-root "mktemp shim: template=/vcn.XXXXXX" PATH="$TMP/mktemp-bin:$PATH" TMPDIR=/ VERIFY_OUT="$TMP/tmp-out" # mktemp gets the resolved path. The path as given must pass the same walk, which is main's rule: the symlink itself, its diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh index edc11ea9f..d2f04ff27 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh @@ -24,10 +24,18 @@ fail() { # in a code line, except the two resolutions (`=$(bin jq)`, `=$(bin setsid)`), is a bare call and fails it. A default in a # parameter expansion (`${JQ_BIN:-jq}`) names the tool as bare as a call does, and the word pattern skips it on purpose, because # a name with a hyphen before it (`mise-jq`) is not a call. +word_re='(^|[^[:alnum:]_$-])(jq|setsid)($|[^[:alnum:]_-])' +default_re='\$\{[A-Za-z_][A-Za-z0-9_]*:?[-=+?](jq|setsid)\}' +strip_re='(JQ_BIN|SETSID_BIN)=\$\(bin (jq|setsid)\)' + +# bare_hits : the numbered code lines of the file that name jq or setsid as a bare call or as a default, except the two +# resolutions. +bare_hits() { + grep -n '' "$1" | grep -vE '^[0-9]+:[[:space:]]*#' | sed -E "s/$strip_re//" | grep -E "$word_re|$default_re" || true +} + bare_tools_case() { - local name=no-bare-tools hits site bare sites=0 word_re='(^|[^[:alnum:]_$-])(jq|setsid)($|[^[:alnum:]_-])' form - local default_re='\$\{[A-Za-z_][A-Za-z0-9_]*:?[-=+?](jq|setsid)\}' - local strip_re='(JQ_BIN|SETSID_BIN)=\$\(bin (jq|setsid)\)' + local name=no-bare-tools hits site bare sites=0 form local jq_ref='"$JQ_BIN"' setsid_ref='"$SETSID_BIN"' while IFS= read -r site; do for form in "" /usr/bin/ ./; do @@ -43,7 +51,11 @@ bare_tools_case() { grep -qE "$default_re" <<<"$bare" || fail "$name" "the default pattern misses $bare" done ! grep -qE "$default_re" <<<'"$JQ_BIN" -n "${JQ_BIN:-x}"' || fail "$name" "the default pattern matches a call through \$JQ_BIN" - hits=$(grep -n '' "$V" | grep -vE '^[0-9]+:[[:space:]]*#' | sed -E "s/$strip_re//" | grep -E "$word_re|$default_re" || true) + printf 'f() {\n # jq here is a comment\n x=$("${JQ_BIN:-jq}" -n 1)\n}\n' >"$TMP/bare-sample" + [[ $(bare_hits "$TMP/bare-sample") == "3:"* ]] || fail "$name" "the scan of a file missed a default in a parameter expansion: $(bare_hits "$TMP/bare-sample")" + printf 'f() {\n x=$("$JQ_BIN" -n 1)\n JQ_BIN=$(bin jq)\n}\n' >"$TMP/bare-sample" + [[ -z $(bare_hits "$TMP/bare-sample") ]] || fail "$name" "the scan of a file took a call through \$JQ_BIN or the resolution for a bare call" + hits=$(bare_hits "$V") [[ -z $hits ]] || fail "$name" "vcn.sh runs a bare or path-qualified jq or setsid: $(tr '\n' ' ' <<<"$hits")" echo "ok $name: vcn.sh runs jq and setsid only through \$JQ_BIN and \$SETSID_BIN" cases=$((cases + 1)) @@ -176,7 +188,16 @@ sourcing_units() { code_units "$1" 1 | grep -v '^%%unit%%$' || true; } # The callers of a run moved to `vcn.sh get` and `vcn.sh dashboard`. A source of run.env in the skill's own scripts runs every # line of the file with no check of the state dir, and one in a doc teaches a caller to do it. Only `load` in vcn.sh sources it. no_source_case() { - local name=no-source-run-env skill file hits sample=$TMP/no-source.md src_re='(^|[;&|({])[[:space:]]*(source|\.)[[:space:]]+[^;#`]*run\.env' n + local name=no-source-run-env skill file hits sample=$TMP/no-source.md n line + # A source is a command: at the start of a line or after ; & | ( { ! or a keyword. The words in an echo are not. + local src_re='(^|[;&|({!]|(^|[[:space:]])(if|then|do|else|elif|while|until)[[:space:]])[[:space:]]*(source|\.)[[:space:]]+[^;#`]*run\.env' + for line in 'source "$VCN_STATE/run.env"' ' . "$OUT/run.env"' 'if source "$S/run.env"; then' 'x && source run.env' 'then source "$S/run.env"' \ + '! source "$S/run.env"' 'while . ./run.env; do' 'f() { . "$S/run.env"; }'; do + grep -qE "$src_re" <<<"$line" || fail "$name" "the script pattern misses: $line" + done + for line in 'echo "a state dir was refused and its run.env not sourced"' 'echo "named through a . or .. part, its run.env"' 'echo "did not source its run.env"'; do + ! grep -qE "$src_re" <<<"$line" || fail "$name" "the script pattern takes words of an echo for a source: $line" + done skill=$(dirname "$V")/.. printf 'Run:\n\n```bash\nsource "$VCN_STATE/run.env"\n```\n' >"$sample" [[ -n $(sourcing_units "$sample") ]] || fail "$name" "a fenced block that sources a run.env was not found" @@ -192,7 +213,8 @@ no_source_case() { [[ -z $hits ]] || fail "$name" "${file#"$skill"/} has a recipe that sources a run.env: $(tr '\n' ' ' <<<"$hits")" done for file in "$skill"/scripts/*.sh; do - [[ ${file##*/} != vcn.sh ]] || continue + # vcn.sh is the one place that sources it, and this script holds the samples of the patterns. + [[ ${file##*/} != vcn.sh && ${file##*/} != proof-static.sh ]] || continue hits=$(grep -nE "$src_re" "$file" | grep -vE '^[0-9]+:[[:space:]]*#' || true) [[ -z $hits ]] || fail "$name" "${file#"$skill"/} sources a run.env: $(tr '\n' ' ' <<<"$hits")" done diff --git a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh index 97b3864c3..36f4a7959 100755 --- a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh +++ b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh @@ -100,8 +100,11 @@ load() { [[ -z ${VCN_CLIENT-} || $VCN_CLIENT =~ ^[a-z0-9]+$ ]] || die "VCN_CLIENT must match [a-z0-9]+" # shellcheck source=/dev/null source "$VCN_STATE/run.env" - why=$(bad_node_dir "${NODE_DIR-}") - [[ -z $why ]] || die "NODE_DIR=${NODE_DIR-} in $VCN_STATE/run.env is not usable: $why" + # A run.env that has no NODE_DIR yet (launch stopped while it wrote the file) is left to cleanup: nothing runs agent-tty for it. + if [[ -n ${NODE_DIR+x} ]]; then + why=$(bad_node_dir "$NODE_DIR") + [[ -z $why ]] || die "NODE_DIR=$NODE_DIR in $VCN_STATE/run.env is not usable: $why" + fi # A run that an older vcn.sh started has no JQ_BIN. [[ -n ${JQ_BIN-} ]] || JQ_BIN=$(bin jq) } @@ -384,7 +387,7 @@ unsafe_dir() { elif [[ -e $1 ]] && (((8#$(stat -c %a "$1") & 8#022) != 0)); then echo "$1 is group- or world-writable" else - unsafe_above "$1" + unsafe_above "$1" "${2-the evidence dir}" fi } @@ -406,8 +409,8 @@ unsafe_above() { ensure_att_root() { local why [[ -e /tmp/agent-tty || -L /tmp/agent-tty ]] || mkdir -m 700 -- /tmp/agent-tty 2>/dev/null || true - why=$(unsafe_dir /tmp/agent-tty) - [[ -z $why ]] || die "refusing the agent-tty socket dir: $why; agent-tty keeps its sockets in /tmp/agent-tty and does not check who owns it" + why=$(unsafe_dir /tmp/agent-tty "the agent-tty socket dir") + [[ -z $why ]] || die "refusing the agent-tty socket dir: $why; agent-tty keeps its sockets in /tmp/agent-tty and does not check who owns it. If the dir is yours and only its mode is wrong, run: chmod go-w /tmp/agent-tty" [[ -d /tmp/agent-tty ]] || die "cannot make /tmp/agent-tty, where agent-tty keeps its sockets" } From 6258438158e3940fb1337f8f75fc5dd9d6c7652c Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 12 Nov 2026 03:52:22 +0000 Subject: [PATCH 5/9] docs(skills): give the measured time of the refusal proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-5 verifier of #506 (F2): SKILL.md said that proof-launch-refusals.sh takes about 60 s. It ran for 163 s (the last gate on #506), about 190 s (a verifier) and 287 s (this branch, with 40 PASS lines, on a host at a load of about 20), because most cases start a launch. The sentence now says 3 to 5 minutes and why. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_ --- .agents/skills/verify-claudecode-nvim/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md index fbdfcc982..f95041b79 100644 --- a/.agents/skills/verify-claudecode-nvim/SKILL.md +++ b/.agents/skills/verify-claudecode-nvim/SKILL.md @@ -131,7 +131,7 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`. - `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused (an absolute `NODE_DIR` that holds no node is not, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1. - `scripts/proof-static.sh` proves three things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), and every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them. A code block is a fence of three or more backticks or tildes with any indent. A block or span that sources a `run.env` is left out of that check, and a comment that names such a source does not count. It also proves that no script and no recipe sources a `run.env` except `load` in `vcn.sh`. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `. -- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes about 60 s. +- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 3 to 5 minutes (163 s to 287 s measured, depending on the load of the host), because most cases start a launch. - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`. - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`. - The `race` case puts a `mkdir` shim first on `PATH`. The shim plays another launch that makes the dir above `VERIFY_OUT` first, group-writable. Launch must refuse that dir in the check after `mkdir` and leave it in place. From 6757eca3294c07a9c69ee785e3a47efe45a61b28 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 12 Nov 2026 04:34:18 +0000 Subject: [PATCH 6/9] docs(skills): widen the measured time of the refusal proof MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The final gate of this branch ran proof-launch-refusals.sh in 338 s (40 PASS lines) on a host at a load of 35. SKILL.md now says 3 to 6 minutes, from 163 s to 338 s. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_ --- .agents/skills/verify-claudecode-nvim/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md index f95041b79..73d5c4d6e 100644 --- a/.agents/skills/verify-claudecode-nvim/SKILL.md +++ b/.agents/skills/verify-claudecode-nvim/SKILL.md @@ -131,7 +131,7 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`. - `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused (an absolute `NODE_DIR` that holds no node is not, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1. - `scripts/proof-static.sh` proves three things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), and every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them. A code block is a fence of three or more backticks or tildes with any indent. A block or span that sources a `run.env` is left out of that check, and a comment that names such a source does not count. It also proves that no script and no recipe sources a `run.env` except `load` in `vcn.sh`. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `. -- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 3 to 5 minutes (163 s to 287 s measured, depending on the load of the host), because most cases start a launch. +- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 3 to 6 minutes (163 s to 338 s measured, depending on the load of the host), because most cases start a launch. - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`. - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`. - The `race` case puts a `mkdir` shim first on `PATH`. The shim plays another launch that makes the dir above `VERIFY_OUT` first, group-writable. Launch must refuse that dir in the check after `mkdir` and leave it in place. From 30e86876a442b4a696787fcafdf6e78afd86e56a Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 12 Nov 2026 06:08:40 +0000 Subject: [PATCH 7/9] fix(skills): read OUT and WORK whole in the docs, and harden the checks that guard them MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round 1 of the verifiers of #545 (Opus F3 to F12, gpt A and B). features/README.md read OUT as `OUT=$($V get OUT)`. A command substitution cuts a newline at the end of the value, and VERIFY_OUT may end in one, so the next documented write went to the twin of the evidence dir. SKILL.md and the README now give one recipe, `getz() { IFS= read -r -d '' "$1" < <($V get -z "$1"); }; getz OUT; getz WORK`, and the full-run block of SKILL.md no longer exports OUT. proof-static.sh gets two cases: doc-get-exact (no recipe reads a path through `$(... get NAME)`) and doc-recipe (the documented line runs on a hand-made run.env with a trailing newline in OUT and WORK, with a control that shows a command substitution cuts it). proof-static.sh, the points of Opus F3 to F6: a comment sets and sources nothing, so `# PORT=$(x)` no longer satisfies doc-vars and `echo x # source run.env` no longer exempts a block. A source after `builtin`, `command` or `eval`, in backticks or in quotes, is found, and so is a span that a line break splits. `$((PORT + 1))` is a use. A missing SKILL.md or features/*.md fails. The header says what the checks do not see (an indented code block, 
, a command that a variable holds, a source in a .lua,
.py or .mjs file). Each change has a sample in the case and a mutant that turns it red.

proof-launch-refusals.sh, gpt B and Opus F7: a case that accepts /tmp/agent-tty
requires the launch to go on to `agent-tty doctor`, so a guard that refuses a safe dir
with any message fails it (the strict-0700 mutant with another message was green). New
cases: att-root-own-700 and att-root-nosticky (a 0700 dir under a /tmp that is
world-writable without the sticky bit: only the walk above the dir can refuse it).

Opus F9: load names the manual cleanup for a run whose NODE_DIR it refuses: stop the
nvim and agent-tty processes and `rm -rf` the state dir. cleanup refuses too, because it
would run agent-tty with that PATH. node-dir tests the hint and that the dir stays.
Opus F8: get keeps both name checks, and get-values holds a name (`O.T`) that only the
pattern check refuses. SKILL.md says that a 0775 /tmp/agent-tty (umask 002) is refused
and that the message names `chmod go-w`.

_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
---
 .../skills/verify-claudecode-nvim/SKILL.md    |  12 +-
 .../verify-claudecode-nvim/features/README.md |   2 +-
 .../scripts/proof-agent-tty-resolution.sh     |  13 +-
 .../scripts/proof-launch-refusals.sh          |  20 ++-
 .../scripts/proof-static.sh                   | 147 +++++++++++++++---
 .../verify-claudecode-nvim/scripts/vcn.sh     |   2 +-
 6 files changed, 157 insertions(+), 39 deletions(-)

diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md
index 73d5c4d6e..c3874a228 100644
--- a/.agents/skills/verify-claudecode-nvim/SKILL.md
+++ b/.agents/skills/verify-claudecode-nvim/SKILL.md
@@ -36,7 +36,7 @@ VCN_STATE=/tmp/vcn.AbC123
 OUT=/home/coder/.xum/sessions//scratch/verify-claudecode-nvim/20261031T120000Z-AbC123
 ```
 
-Every bash call is a fresh shell. Start each later call with the `VCN_STATE` value that launch printed, in single quotes because a path can hold a space or an apostrophe (`TMPDIR` and `VERIFY_OUT` allow both): `export VCN_STATE='/tmp/vcn.AbC123'`. Inside the quotes, write each `'` of the path as `'\''`. A path can hold a newline too, and launch then prints it over two lines: copy all of it, inside the quotes. Use a new request id for every `rpc` or `tool` call, because the harness refuses an id the run already used. Do not `source` `$VCN_STATE/run.env` or `$OUT/run.env` in your own calls: bash runs every line of a file it sources, as you. `launch` appends version lines such as `agent-tty 0.5.0` to `$OUT/run.env`, and bash would run those as commands. Read any other value of the run with `$V get `, for example `OUT=$($V get OUT)`. A command substitution cuts the newlines at the end of a value, so a script that needs a path whole reads `IFS= read -r -d '' OUT < <($V get -z OUT)`. `get` answers only a name that `run.env` holds, parses no printed text, and runs the check that every `vcn.sh` command makes of `$VCN_STATE` before it sources `run.env` (it must be its own resolved path and a directory that this user owns, with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit). The five `journey-*.sh` scripts read `OUT` and `WORK` through `get`, so they make that check too, and an `OUT` that you exported does not change where they write. Export a `VCN_STATE` that your own `launch` printed, never one from an earlier or another session. Get the other values from the run:
+Every bash call is a fresh shell. Start each later call with the `VCN_STATE` value that launch printed, in single quotes because a path can hold a space or an apostrophe (`TMPDIR` and `VERIFY_OUT` allow both): `export VCN_STATE='/tmp/vcn.AbC123'`. Inside the quotes, write each `'` of the path as `'\''`. A path can hold a newline too, and launch then prints it over two lines: copy all of it, inside the quotes. Use a new request id for every `rpc` or `tool` call, because the harness refuses an id the run already used. Do not `source` `$VCN_STATE/run.env` or `$OUT/run.env` in your own calls: bash runs every line of a file it sources, as you. `launch` appends version lines such as `agent-tty 0.5.0` to `$OUT/run.env`, and bash would run those as commands. Read a path of the run with `get -z`, which keeps a newline at the end of the path that a command substitution would cut: `getz() { IFS= read -r -d '' "$1" < <($V get -z "$1"); }; getz OUT; getz WORK`. A value that holds no newline, such as `PORT` or `SID`, can be read through `$($V get PORT)`. `get` answers only a name that `run.env` holds, parses no printed text, and runs the check that every `vcn.sh` command makes of `$VCN_STATE` before it sources `run.env` (it must be its own resolved path and a directory that this user owns, with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit). The five `journey-*.sh` scripts read `OUT` and `WORK` through `get`, so they make that check too, and an `OUT` that you exported does not change where they write. Export a `VCN_STATE` that your own `launch` printed, never one from an earlier or another session. Get the other values from the run:
 
 - `WORK` is `$VCN_STATE/work`, where `hello.txt` and `other.txt` live.
 - `$V doctor` prints the agent-tty session id (`SID`) in its `agent-tty session  is running` line and the port of the plugin server (`PORT`) in its `plugin server is running on lock port ` line. The port is also the name of the lock file, `$VCN_STATE/claude/ide/.lock`, so `PORT=$(basename "$VCN_STATE"/claude/ide/*.lock .lock)` gives it while the server runs.
@@ -52,7 +52,7 @@ Launch first runs `agent-tty doctor` and saves it to `$OUT/agent-tty-doctor.json
   - CI does not run the harness, on 0.8 or any other version. A run needs `agent-tty` from npm and Playwright Chromium (about 400 MB unpacked), and CI installs neither. Node is not the obstacle: the `unit-tests` job already gets the repo's Node 26 from mise. The two would add minutes and two more downloads to every PR. CI's `integration-tests (v0.8.0)` job already runs the plugin's integration tests on Neovim 0.8. After a change to `vcn.sh`, check the 0.8 path by hand: do the full run at the end of this file, with `VCN_NVIM=<0.8 nvim> $V launch` as its launch step.
 - `VCN_RTP=[:...]` adds plugin dirs to `runtimepath` after this checkout. A `terminal.provider = "snacks"` run needs a snacks.nvim clone there, because the harness installs no plugin. Pin the clone as [features/send-at-mention.md](features/send-at-mention.md) shows. A relative entry resolves against the directory you launch from, because nvim runs in `$WORK`, and symlinks are followed. Launch exits 1 for an entry that is not a directory, so a typo cannot pass as a snacks run on a native terminal. A float run is in [features/terminal-float-diff.md](features/terminal-float-diff.md).
 - `VCN_INIT_JSONRPC=` sets the `jsonrpc` field of the `initialize` request (default `2.0`). Only `scripts/proof-launch-refusals.sh` sets it, to get an error answer from the plugin.
-- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. `agent-tty` keeps every socket in the fixed dir `/tmp/agent-tty`, whatever `TMPDIR` says, and does not check who owns it, so another user who owns that dir or can rename entries in it could swap the socket dir of a run and answer every command. Launch makes `/tmp/agent-tty` with mode `0700` when it is missing, and refuses one that is a symlink, is owned by another user or is group- or world-writable (a `0755` dir of yours is fine). Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the journeys read through `get`, so they check it too): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`.
+- `TMPDIR=` makes launch put its state dir, `vcn.XXXXXX`, in `` instead of `/tmp`. The path must be absolute, name an existing directory (a missing one could be made by another user after the checks) and have no `.` or `..` part (one after a symlink would hide the symlink from the checks). Launch resolves it once, with `realpath -e`, and gives `mktemp` only the result, so `VCN_STATE` has no symlink in it. Launch refuses a `TMPDIR` that another user could write, and it checks two paths: the path as you give it (the symlink itself, if it is one, and every dir above it) and the resolved path. In each, it refuses a dir or symlink that another user owns (root is fine) and a dir that is group- or world-writable without the sticky bit. The check of the path as given is the rule that main applied. `vcn.sh` never gives `agent-tty` your `TMPDIR`: every `agent-tty` call that `vcn.sh` makes runs with `TMPDIR=$VCN_STATE/tmp`, a dir that launch makes in the state dir (mode `0700`), so a symlink in your `TMPDIR` that another user repoints after the launch cannot redirect a WebM export or a screenshot, and a command can run with any `TMPDIR`. A `TMPDIR` that is a symlink to a second symlink is accepted when both paths pass, because nothing follows the symlinks after launch has resolved them: `mktemp` gets the resolved path. `/tmp` is sticky, so the default passes. `agent-tty` keeps every socket in the fixed dir `/tmp/agent-tty`, whatever `TMPDIR` says, and does not check who owns it, so another user who owns that dir or can rename entries in it could swap the socket dir of a run and answer every command. Launch makes `/tmp/agent-tty` with mode `0700` when it is missing, and refuses one that is a symlink, is owned by another user or is group- or world-writable (a `0755` dir of yours is fine, and a `0775` dir that a plain `agent-tty` run made under `umask 002` is refused: the message names `chmod go-w /tmp/agent-tty`). Keep it short: nvim's socket, `nvim.sock`, lives in the state dir, and a Unix socket path is limited to 108 bytes. Neovim 0.12.3 accepts a longer path. Older versions are untested. `cleanup` accepts a state dir from any `TMPDIR`: an absolute path that ends in `/vcn.` and six letters or digits. Every `vcn.sh` command that reads a run first checks `$VCN_STATE`, because it sources `run.env` from it (the journeys read through `get`, so they check it too): `$VCN_STATE` must be its own resolved path (no symlink, `.` or `..` part, as launch prints it) and a directory that this user owns with no group or other write, and no dir above it may be owned by another user (root is fine) or writable by others without the sticky bit. A dir or symlink that another user made at the name of a cleaned-up run fails that check. There is no separate check of the file: after the check of the dir, no other user can swap it or anything in it. A run that an older `vcn.sh` started has no `JQ_BIN` in `run.env`, so the command resolves `jq` again. `scripts/proof-agent-tty-resolution.sh` runs every launch with a private `TMPDIR`.
 - `VCN_SETUP=''` is deep-merged into `require("claudecode").setup()` over the base `{ terminal = { provider = "none" } }`. Example: `VCN_SETUP='{"diff_opts":{"layout":"unified"}}' $V launch`.
 - For a `log_level = "debug"` run, launch with `VCN_SETUP='{"log_level":"debug"}' $V launch --cmd 'set messagesopt=wait:0,history:10000' hello.txt`. Without it, one openDiff call at debug level parks Neovim at `Press ENTER`, and RPC stops answering. Launch arguments replace the default file, so name `hello.txt`. Neovim 0.8 has no `messagesopt`, so plain `set` fails launch with E518. Use `--cmd 'silent! set messagesopt=wait:0,history:10000'` there. Launch then works, but debug echoes still stop at `Press ENTER` (see Doctor).
 
@@ -129,9 +129,9 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul
 
 - `scripts/vcn.sh` is the harness. `$V help` lists its subcommands.
 - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`.
-- `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused (an absolute `NODE_DIR` that holds no node is not, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1.
-- `scripts/proof-static.sh` proves three things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), and every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them. A code block is a fence of three or more backticks or tildes with any indent. A block or span that sources a `run.env` is left out of that check, and a comment that names such a source does not count. It also proves that no script and no recipe sources a `run.env` except `load` in `vcn.sh`. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `.
-- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0755`, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 3 to 6 minutes (163 s to 338 s measured, depending on the load of the host), because most cases start a launch.
+- `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused, `cleanup` included, which names the `rm -rf` of the state dir for stopping the run by hand (an absolute `NODE_DIR` that holds no node is not refused, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1.
+- `scripts/proof-static.sh` proves five things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` (also in `$(( ))`) sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them, no script and no recipe sources a `run.env` except `load` in `vcn.sh`, no recipe reads a path of the run (`OUT`, `WORK`) through `$(... get NAME)`, which cuts a newline at its end, and the recipe that `features/README.md` and this file give for reading `OUT` and `WORK` returns both whole for a `VERIFY_OUT` that ends in a newline (the case runs the documented line on a hand-made `run.env`). A code block is a fence of three or more backticks or tildes with any indent, and an inline span that a line break splits is one span. A comment sets and sources nothing, and an assignment or a source in one does not count. A source after `builtin`, `command` or `eval`, in backticks or in quotes, is found. The checks do not see an indented code block, `
`, a command that a variable holds, or a source in a `.lua`, `.py` or `.mjs` file. A missing `SKILL.md` or `features/*.md` fails them. A block or span that sources a `run.env` is left out of the first two checks. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `.
+- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0700` or `0755`: each such case requires the launch to go on to `agent-tty doctor`, so a guard that refuses a safe dir with any message fails it, and that launch refuses your `0700` dir when `/tmp` is world-writable without the sticky bit, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 3 to 6 minutes (163 s to 338 s measured, depending on the load of the host), because most cases start a launch.
   - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`.
   - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`.
   - The `race` case puts a `mkdir` shim first on `PATH`. The shim plays another launch that makes the dir above `VERIFY_OUT` first, group-writable. Launch must refuse that dir in the check after `mkdir` and leave it in place.
@@ -151,7 +151,7 @@ A full run, with the `VCN_STATE` value from launch:
 ```bash
 V=.agents/skills/verify-claudecode-nvim/scripts/vcn.sh
 $V launch
-export VCN_STATE='/tmp/vcn.AbC123' OUT=''
+export VCN_STATE='/tmp/vcn.AbC123'
 $V doctor
 .agents/skills/verify-claudecode-nvim/scripts/journey-opendiff-accept.sh
 $V cleanup
diff --git a/.agents/skills/verify-claudecode-nvim/features/README.md b/.agents/skills/verify-claudecode-nvim/features/README.md
index 7936ce5e1..8a5302894 100644
--- a/.agents/skills/verify-claudecode-nvim/features/README.md
+++ b/.agents/skills/verify-claudecode-nvim/features/README.md
@@ -5,7 +5,7 @@ This directory is the maintained source for verifying the user-facing behavior o
 ## Baseline preconditions
 
 - Launch a fresh run with `.agents/skills/verify-claudecode-nvim/scripts/vcn.sh launch`. It opens `hello.txt` with the default config plus `terminal.provider = "none"`.
-- Start every bash call with `export VCN_STATE=''` (quoted as SKILL.md says); `V=.agents/skills/verify-claudecode-nvim/scripts/vcn.sh; OUT=$($V get OUT); WORK=$($V get WORK)`. Do not `source` a `run.env` in these calls (see SKILL.md).
+- Start every bash call with `export VCN_STATE=''` (quoted as SKILL.md says); `V=.agents/skills/verify-claudecode-nvim/scripts/vcn.sh; getz() { IFS= read -r -d '' "$1" < <($V get -z "$1"); }; getz OUT; getz WORK`, which keeps a newline at the end of a path, as a command substitution would not. Do not `source` a `run.env` in these calls (see SKILL.md).
 - `$WORK/hello.txt` is `alpha`, `beta`, `gamma` and `$WORK/other.txt` is `one`, `two`, `three`, `four`.
 - `$V doctor` reports nine `ok` lines, including `a client finished the WebSocket handshake`.
 - Never drive an nvim, agent-tty session, or lock file that this run did not start.
diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh
index 594282dcd..91aa99662 100755
--- a/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh
+++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-agent-tty-resolution.sh
@@ -10,8 +10,9 @@
 #                     fails by itself still saves its failure screen and the final evidence, and runs `agent-tty home
 #                     forget`, all through the setsid that mise names
 #   jq-old-run        a run.env without JQ_BIN, as an older vcn.sh wrote it: a command resolves jq again
-#   node-dir          a run.env whose NODE_DIR is empty, relative or has a colon is refused (att() would put the current dir, or
-#                     a second dir, on PATH), and one whose NODE_DIR is an absolute dir without a node is not
+#   node-dir          a run.env whose NODE_DIR is empty, relative or has a colon is refused, by cleanup too, which names the
+#                     rm -rf for the state dir (att() would put the current dir, or a second dir, on PATH), and one whose NODE_DIR
+#                     is an absolute dir without a node is not
 #   state-resolved    a VCN_STATE with a . or .. part, a symlink in its path, or a symlink as its last part is refused, not
 #                     sourced
 #   state-slash       a VCN_STATE with a trailing /, /. or //, or a .. after a symlink, is refused, not sourced
@@ -745,6 +746,12 @@ node_dir_case() {
     out=$(env PATH="$base" VCN_STATE="$dir" "$V" doctor 2>&1) || rc=$?
     ((rc == 1)) && [[ $out == *"NODE_DIR=$val in $dir/run.env is not usable: $want"* ]] ||
       fail "$name" "doctor with NODE_DIR='$val' exited $rc, wanted 1 with '$want': $out"
+    # cleanup refuses too, because it would run agent-tty with that PATH. It must say how to stop the run by hand, and it must
+    # leave the state dir for that.
+    rc=0
+    out=$(env PATH="$base" VCN_STATE="$dir" "$V" cleanup 2>&1) || rc=$?
+    ((rc == 1)) && [[ $out == *"To stop this run by hand, stop its nvim and agent-tty processes, then remove its state dir: rm -rf $(printf %q "$dir")"* && -d $dir ]] ||
+      fail "$name" "cleanup with NODE_DIR='$val' exited $rc without the hand-cleanup hint for $dir, or removed it: $out"
     rm -rf -- "$dir"
   done
   mkdir "$TMP/no-node"
@@ -776,7 +783,7 @@ get_values_case() {
   [[ $got == "$weird_out" ]] || fail "$name" "get -z OUT printed '$got', not the whole OUT"
   got=$(env PATH="$good_path" VCN_STATE="$dir" "$V" get OUT)
   [[ $got == "${weird_out%$'\n'}" ]] || fail "$name" "get OUT in a command substitution printed '$got'"
-  for got in PATH SID "a b" "" "OUT; touch $TMP/marker-$name"; do
+  for got in PATH SID "a b" "" "O.T" "OUT; touch $TMP/marker-$name"; do
     rc=0
     out=$(env PATH="$good_path" VCN_STATE="$dir" "$V" get "$got" 2>&1) || rc=$?
     ((rc == 1)) && [[ $out == "vcn: get: "* ]] || fail "$name" "get '$got' exited $rc with '$out', wanted 1 and a get: refusal"
diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh
index 33a98eba6..e1809e56a 100755
--- a/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh
+++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-launch-refusals.sh
@@ -24,6 +24,7 @@
 #   tmp-load-refused  mktemp answers with a path that is not its own resolved path (a // in it): load refuses the new state dir,
 #                  and launch leaves no state dir and no evidence dir
 #   node-relative  node is found through a relative PATH entry (no mise): its dir would go on PATH in every agent-tty call
+#   att-root-nosticky  /tmp/agent-tty is this user's 0700 dir, and /tmp is world-writable without the sticky bit
 #   tmp-root       TMPDIR is /: launch gives mktemp /vcn.XXXXXX, not //vcn.XXXXXX (a mktemp shim stops launch and prints it)
 #   tmp-space      a dir above TMPDIR that others can write has a name that ends in a space
 #   out-space      the same above VERIFY_OUT
@@ -219,8 +220,10 @@ tmp_link_foreign_case
 # can rename entries in it, could swap the socket dir of a run and answer every command. Launch makes the dir 0700 when it is
 # missing and refuses one that is not this user's alone.
 # att_root_case     [bwrap args]: launch in a sandbox after the planting shell ran.  is
-# the text of a refusal, which must leave nothing behind, or empty when launch must get past the check (it stops later,
-# because no agent-tty passes doctor) and leave /tmp/agent-tty with  and this user as its owner.
+# the text of a refusal, which must leave nothing behind, or empty when launch must get past the check and leave
+# /tmp/agent-tty with  and this user as its owner. The agent-tty here is `false`, so a launch that got past the check stops
+# at the next step, `agent-tty doctor`, and says so: that text, not only the absence of one refusal, is what shows the launch went
+# on, so a guard that refuses a safe dir with any other message fails the case.
 att_root_case() {
   local name=$1 plant=$2 want=$3 mode=$4 out rc=0
   shift 4
@@ -228,16 +231,16 @@ att_root_case() {
   local args=("${sb[@]}" "$@" --setenv VCN_AGENT_TTY /usr/bin/false)
   out=$(bwrap "${args[@]}" /usr/bin/bash -c "$plant"'
     /w/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh launch; echo "rc=$?"
-    [[ ! -e /tmp/out && -z $(ls -d /tmp/vcn.* 2>/dev/null) ]] || echo LEFT-BEHIND
+    [[ ! -e /tmp/out && ! -e /run/o && -z $(ls -d /tmp/vcn.* /run/t/vcn.* 2>/dev/null) ]] || echo LEFT-BEHIND
     stat -c "ROOT %a %u" /tmp/agent-tty 2>&1' 2>&1) || rc=$?
   if [[ -n $want ]]; then
     [[ $out == *"refusing the agent-tty socket dir: $want"* && $out == *"rc=1"* && $out != *VCN_STATE=* && $out != *LEFT-BEHIND* ]] ||
       fail "$name: launch did not refuse /tmp/agent-tty with '$want', exit 1 and nothing left behind: $out"
     echo "PASS $name: $want, and launch refused it before it made anything"
   else
-    [[ $out != *"refusing the agent-tty socket dir"* && $out == *"rc=1"* && $out == *"ROOT $mode 0"* ]] ||
-      fail "$name: launch refused /tmp/agent-tty or did not leave it with mode $mode and this user as owner: $out"
-    echo "PASS $name: launch accepted /tmp/agent-tty and left it with mode $mode"
+    [[ $out != *"refusing the agent-tty socket dir"* && $out == *'no agent-tty passes `agent-tty doctor`'* && $out == *"rc=1"* && $out == *"ROOT $mode 0"* ]] ||
+      fail "$name: launch did not go on to agent-tty doctor after /tmp/agent-tty, or left it with a mode other than $mode or another owner: $out"
+    echo "PASS $name: launch accepted /tmp/agent-tty, went on to agent-tty doctor and left the dir with mode $mode"
   fi
 }
 host_root_dir=""
@@ -255,7 +258,12 @@ fi
 att_root_case att-root-loose 'mkdir -m 777 /tmp/agent-tty' "/tmp/agent-tty is group- or world-writable" ""
 att_root_case att-root-link 'ln -s /tmp /tmp/agent-tty' "/tmp/agent-tty is a symlink" ""
 att_root_case att-root-made : "" 700
+att_root_case att-root-own-700 'mkdir -m 700 /tmp/agent-tty' "" 700
 att_root_case att-root-own-755 'mkdir -m 755 /tmp/agent-tty' "" 755
+# The dir is safe, but /tmp is not sticky, so another user could rename it. TMPDIR and VERIFY_OUT sit in a dir of their own, so
+# only the check of the dirs above /tmp/agent-tty can refuse.
+att_root_case att-root-nosticky 'mkdir -m 700 /tmp/agent-tty' "/tmp, above the agent-tty socket dir, is writable by others and not sticky" "" \
+  --perms 0777 --tmpfs /tmp --dir /run/t --setenv TMPDIR /run/t --setenv VERIFY_OUT /run/o
 # A newline at the end of a name is cut by a command substitution. The resolved TMPDIR is a dir with a newline at the end of its
 # name and mode 777, and a twin symlink without the newline leads to a safe dir: a launch that cuts the newline would take the twin.
 mkdir -m 700 "$TMP/nl" "$TMP/nl/safe"
diff --git a/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh b/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh
index d2f04ff27..8695b56ba 100755
--- a/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh
+++ b/.agents/skills/verify-claudecode-nvim/scripts/proof-static.sh
@@ -3,23 +3,37 @@
 # so `mise run check` runs them in CI:
 #   no-bare-tools  vcn.sh has no jq or setsid command except through $JQ_BIN and $SETSID_BIN, not even as the default of a
 #                  parameter expansion (reads the source, so it reaches every call site, which a run of launch does not)
-#   doc-vars       a code block, or the inline code of a doc, that expands PORT, SID, NVIM_PID or NODE_DIR sets it in the same
-#                  block (or the same doc, for inline code), because a fresh shell has none of them. Prose that names an
-#                  assignment sets nothing, and neither does a comment
+#   doc-vars       a code block, or the inline code of a doc, that expands PORT, SID, NVIM_PID or NODE_DIR sets it with `VAR=$(` in
+#                  the same block (or the same doc, for inline code), because a fresh shell has none of them. Prose that names
+#                  an assignment sets nothing, and neither does a comment
 #   no-source-run-env  no script of the skill, and no recipe in its docs, sources a run.env, except `load` in vcn.sh, which checks the
 #                  state dir first (the callers read a value through `vcn.sh get`)
+#   doc-get-exact  no recipe reads a path of the run (OUT, WORK, ...) through `$(... get NAME)`, which cuts a newline at the end
+#   doc-recipe     the recipe that features/README.md and SKILL.md give for reading OUT and WORK returns both whole, for a
+#                  VERIFY_OUT that ends in a newline (the case runs the documented line on a hand-made run.env)
+# What the checks do not see: an indented code block (four spaces) and 
, a command that a variable or an eval of a built
+# string holds, a source in a file that is not a shell script (.lua, .py, .mjs), and a fence in a quote or a list that markdown
+# would not open. A source after `builtin`, `command` or `eval`, in backticks or quotes, and an inline span that a line break
+# splits are seen. The docs must exist: a missing SKILL.md or features/*.md fails every case that reads them.
 # Prints one `ok ` per case, or `FAIL : ` and exits 1, and ends with `CASES `.
 set -euo pipefail
 V="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)/vcn.sh"
 TMP=$(mktemp -d)
 trap 'rm -rf "$TMP"' EXIT
 cases=0
+skill=$(dirname "$V")/..
 
 fail() {
   echo "FAIL $1: $2" >&2
   exit 1
 }
 
+# need_docs : the docs that the cases read must exist, or a rename leaves them nothing to check and every one passes.
+need_docs() {
+  [[ -f $skill/SKILL.md ]] || fail "$1" "$skill/SKILL.md is missing"
+  compgen -G "$skill/features/*.md" >/dev/null || fail "$1" "$skill/features has no .md file"
+}
+
 # jq-resolved and setsid-resolved reach only the calls that a launch makes. This case reads the source: any word jq or setsid
 # in a code line, except the two resolutions (`=$(bin jq)`, `=$(bin setsid)`), is a bare call and fails it. A default in a
 # parameter expansion (`${JQ_BIN:-jq}`) names the tool as bare as a call does, and the word pattern skips it on purpose, because
@@ -69,7 +83,8 @@ bare_tools_case() {
 # code_units  [1]: prints each fenced block, then the inline code spans outside the blocks, each unit ended by a line that
 # holds only %%unit%%. A block or a span that sources a run.env sets every variable of the run by itself, so it is left out: it
 # needs no `VAR=$(`, and it gives none to the other recipes. With a 1, it prints only those units that source. A comment that
-# names such a source is no source.
+# names such a source is no source, but only a whole-line comment is dropped when the units that source are listed, so that
+# `echo "x #1"; source run.env` is found. A span that a line break splits is one span.
 code_units() {
   awk -v want="${2:-0}" 'function emit(text) { if ((sources(text) ? 1 : 0) == want) printf "%s", text }
     function run_len(t, ch,   n) { n = 0; while (substr(t, n + 1, 1) == ch) n++; return n }
@@ -78,11 +93,20 @@ code_units() {
       for (i = 1; i <= n; i++) {
         row = rows[i]
         sub(/^[ \t]*#.*/, "", row)
-        sub(/[ \t]#.*$/, "", row)
-        if (row ~ /(^|[^A-Za-z0-9_.-])(source|\.)[ \t]+[^;#]*run\.env/) return 1
+        if (!want) sub(/[ \t]#.*$/, "", row)
+        if (row ~ /(^|[^A-Za-z0-9_.-])(source|\.|eval)[ \t]+[^;#]*run\.env/) return 1
       }
       return 0
     }
+    function flush(   line, span) {
+      line = para
+      para = ""
+      while (match(line, /`[^`]+`/)) {
+        span = substr(line, RSTART + 1, RLENGTH - 2)
+        if ((sources(span) ? 1 : 0) == want) spans = spans span "\n"
+        line = substr(line, RSTART + RLENGTH)
+      }
+    }
     { t = $0; sub(/^[ \t]+/, "", t) }
     fenced {
       n = run_len(t, fch)
@@ -97,21 +121,21 @@ code_units() {
       next
     }
     { c = substr(t, 1, 1) }
-    (c == "`" || c == "~") && run_len(t, c) >= 3 { fenced = 1; fch = c; flen = run_len(t, c); next }
-    { line = $0
-      while (match(line, /`[^`]+`/)) {
-        span = substr(line, RSTART + 1, RLENGTH - 2)
-        if ((sources(span) ? 1 : 0) == want) spans = spans span "\n"
-        line = substr(line, RSTART + RLENGTH)
-      } }
-    END { if (fenced) { emit(block); print "%%unit%%" } printf "%s%%%%unit%%%%\n", spans }' "$1"
+    (c == "`" || c == "~") && run_len(t, c) >= 3 { flush(); fenced = 1; fch = c; flen = run_len(t, c); next }
+    t == "" { flush(); next }
+    t ~ /^(#|[-*+][ \t]|[0-9]+[.)][ \t])/ { flush() }
+    { para = (para == "" ? "" : para " ") $0 }
+    END { if (fenced) { emit(block); print "%%unit%%" } flush(); printf "%s%%%%unit%%%%\n", spans }' "$1"
 }
 
 # The two patterns that decide whether a unit expands a variable and whether it sets it. units_missing and the self-test below
 # both call these, so a change to one is a change to what the self-test checks.
-var_uses_re() { printf '%s' '\$\{?'"$1"'([^A-Za-z0-9_]|$)'; }
+var_uses_re() { printf '%s' '(\$\{?|\$\(\(([^)]*[^A-Za-z0-9_$])?)'"$1"'([^A-Za-z0-9_]|$)'; }
 var_sets_re() { printf '%s' '(^|[^A-Za-z0-9_$])'"$1"'=\$\('; }
 
+# strip_comments: drops a whole-line comment and a trailing comment. A comment is not run, so it neither uses nor sets a variable.
+strip_comments() { sed -E 's/^[[:space:]]*#.*//; s/[[:space:]]#.*$//'; }
+
 # units_missing  : succeeds when a unit of the file expands  and does not set it.
 units_missing() {
   local line unit="" uses_re sets_re
@@ -122,6 +146,7 @@ units_missing() {
       unit+=$line$'\n'
       continue
     fi
+    unit=$(strip_comments <<<"$unit")
     if grep -qE "$uses_re" <<<"$unit" && ! grep -qE "$sets_re" <<<"$unit"; then
       return 0
     fi
@@ -131,13 +156,16 @@ units_missing() {
 }
 
 doc_vars_case() {
-  local name=doc-vars skill file var uses_re sets_re sample missing="" fence
-  skill=$(dirname "$V")/..
+  local name=doc-vars file var uses_re sets_re sample missing="" fence
+  need_docs "$name"
   sample=$TMP/doc-vars-sample.md
   for var in PORT SID NVIM_PID NODE_DIR; do
     uses_re=$(var_uses_re "$var")
     sets_re=$(var_sets_re "$var")
     grep -qE "$uses_re" <<<"see \"\$$var.lock\" and \${$var}" || fail "$name" "the use pattern misses \$$var"
+    grep -qE "$uses_re" <<<"n=\$(($var + 1))" || fail "$name" "the use pattern misses $var in an arithmetic expansion"
+    grep -qE "$uses_re" <<<"n=\$(( x+$var ))" || fail "$name" "the use pattern misses $var after an operator in an arithmetic expansion"
+    ! grep -qE "$uses_re" <<<"n=\$((X_$var + 1))" || fail "$name" "the use pattern matches a longer name in an arithmetic expansion"
     ! grep -qE "$uses_re" <<<"echo $var=\$CLAUDE_CODE_SSE_$var" || fail "$name" "the use pattern matches a longer name"
     grep -qE "$sets_re" <<<"$var=\$(basename \"\$L\"/*.lock .lock)" || fail "$name" "the set pattern misses an assignment of $var"
     grep -qE "$sets_re" <<<"export $var=\$(x)" || fail "$name" "the set pattern misses an exported assignment of $var"
@@ -172,6 +200,20 @@ doc_vars_case() {
     units_missing "$sample" "$var" || fail "$name" "a trailing comment that names a source of run.env exempted a block that expands $var"
     printf 'Run `source "$VCN_STATE/run.env"` first, then `echo "$%s"`.\n' "$var" >"$sample"
     units_missing "$sample" "$var" || fail "$name" "a source in one inline recipe set $var for another recipe"
+    # A comment is not run: an assignment in one sets nothing, whole-line or trailing.
+    printf '```bash\n# %s=$(x)\necho "$%s"\n```\n' "$var" "$var" >"$sample"
+    units_missing "$sample" "$var" || fail "$name" "an assignment of $var in a whole-line comment set it"
+    printf '```bash\necho "$%s" # %s=$(x)\n```\n' "$var" "$var" >"$sample"
+    units_missing "$sample" "$var" || fail "$name" "an assignment of $var in a trailing comment set it"
+    printf '```bash\necho "$%s" # %s is set above\n%s=$(x)\n```\n' "$var" "$var" "$var" >"$sample"
+    ! units_missing "$sample" "$var" || fail "$name" "a comment on the line of a use hid a real assignment of $var"
+    # An expansion in arithmetic is a use, and a span that a line break splits is one span.
+    printf '```bash\necho $((%s + 1))\n```\n' "$var" >"$sample"
+    units_missing "$sample" "$var" || fail "$name" "a use of $var in \$(( )) passed without an assignment"
+    printf 'Run `echo\n"$%s"` and nothing else.\n' "$var" >"$sample"
+    units_missing "$sample" "$var" || fail "$name" "a span split over two lines that expands $var passed"
+    printf 'Set `%s=$(basename\n"$L")` first, then `echo "$%s"`.\n' "$var" "$var" >"$sample"
+    ! units_missing "$sample" "$var" || fail "$name" "an assignment in a span split over two lines was not seen"
     for file in "$skill"/SKILL.md "$skill"/features/*.md; do
       ! units_missing "$file" "$var" || missing+=" ${file#"$skill"/}:$var"
     done
@@ -188,23 +230,31 @@ sourcing_units() { code_units "$1" 1 | grep -v '^%%unit%%$' || true; }
 # The callers of a run moved to `vcn.sh get` and `vcn.sh dashboard`. A source of run.env in the skill's own scripts runs every
 # line of the file with no check of the state dir, and one in a doc teaches a caller to do it. Only `load` in vcn.sh sources it.
 no_source_case() {
-  local name=no-source-run-env skill file hits sample=$TMP/no-source.md n line
-  # A source is a command: at the start of a line or after ; & | ( { ! or a keyword. The words in an echo are not.
-  local src_re='(^|[;&|({!]|(^|[[:space:]])(if|then|do|else|elif|while|until)[[:space:]])[[:space:]]*(source|\.)[[:space:]]+[^;#`]*run\.env'
+  local name=no-source-run-env file hits sample=$TMP/no-source.md n line
+  need_docs "$name"
+  # A source is a command: at the start of a line, after ; & | ( { ! a quote or a backtick, or after a keyword, `builtin`,
+  # `command` or `eval`. The words in an echo are not.
+  local src_re='(^|[;&|({!`'"'"'"]|(^|[[:space:]])(if|then|do|else|elif|while|until|builtin|command|eval)[[:space:]])[[:space:]]*(source|\.)[[:space:]]+[^;#`]*run\.env|(^|[;&|({![:space:]])eval[[:space:]]+[^;#]*run\.env'
   for line in 'source "$VCN_STATE/run.env"' '  . "$OUT/run.env"' 'if source "$S/run.env"; then' 'x && source run.env' 'then source "$S/run.env"' \
-    '! source "$S/run.env"' 'while . ./run.env; do' 'f() { . "$S/run.env"; }'; do
+    '! source "$S/run.env"' 'while . ./run.env; do' 'f() { . "$S/run.env"; }' 'builtin source "$S/run.env"' 'command . "$S/run.env"' \
+    "eval 'source \"\$S/run.env\"'" 'x=`source "$S/run.env"`' 'echo "x #1"; source "$S/run.env"' 'eval "$(cat "$S/run.env")"'; do
     grep -qE "$src_re" <<<"$line" || fail "$name" "the script pattern misses: $line"
   done
   for line in 'echo "a state dir was refused and its run.env not sourced"' 'echo "named through a . or .. part, its run.env"' 'echo "did not source its run.env"'; do
     ! grep -qE "$src_re" <<<"$line" || fail "$name" "the script pattern takes words of an echo for a source: $line"
   done
-  skill=$(dirname "$V")/..
   printf 'Run:\n\n```bash\nsource "$VCN_STATE/run.env"\n```\n' >"$sample"
   [[ -n $(sourcing_units "$sample") ]] || fail "$name" "a fenced block that sources a run.env was not found"
   printf 'Run:\n\n   ~~~\n. "$OUT/run.env"\n   ~~~\n' >"$sample"
   [[ -n $(sourcing_units "$sample") ]] || fail "$name" "an indented ~~~ block that sources a run.env was not found"
   printf 'Run `source "$VCN_STATE/run.env"; echo`.\n' >"$sample"
   [[ -n $(sourcing_units "$sample") ]] || fail "$name" "an inline span that sources a run.env was not found"
+  printf 'Run `builtin source\n"$VCN_STATE/run.env"` first.\n' >"$sample"
+  [[ -n $(sourcing_units "$sample") ]] || fail "$name" "a span split over two lines that sources a run.env was not found"
+  printf '```bash\necho "x #1"; source "$VCN_STATE/run.env"\n```\n' >"$sample"
+  [[ -n $(sourcing_units "$sample") ]] || fail "$name" "a source after a # inside a string was not found"
+  printf '```bash\neval "$(cat "$VCN_STATE/run.env")"\n```\n' >"$sample"
+  [[ -n $(sourcing_units "$sample") ]] || fail "$name" "an eval of run.env was not found"
   printf 'Do not `source` `$VCN_STATE/run.env`.\n\n```bash\n# source run.env\necho x\n```\n' >"$sample"
   [[ -z $(sourcing_units "$sample") ]] || fail "$name" "prose or a comment that names a source was taken for one"
   rm -f -- "$sample"
@@ -224,7 +274,60 @@ no_source_case() {
   cases=$((cases + 1))
 }
 
+# `$(...)` cuts the newlines at the end of its output, and VERIFY_OUT can end in one. A recipe that reads a path of the run through
+# `$($V get OUT)` writes its next file to the twin of the evidence dir, which is a different path in the same checked parent. The
+# docs read a path with `get -z`. A value that is no path (PORT, SID) can use a substitution.
+doc_get_exact_case() {
+  local name=doc-get-exact file hits line
+  local sub_re='\$\([^)]*get[[:space:]]+(OUT|WORK|VCN_STATE|ATT_HOME|NVIM_SOCK|NVIM_BIN|NODE_DIR|ATT_BIN|ATT_SOCK|JQ_BIN)([^A-Za-z0-9_]|$)'
+  need_docs "$name"
+  for line in 'OUT=$($V get OUT)' 'x="$(vcn.sh get WORK)"' 'echo "$($V get VCN_STATE)"' 'WORK=$($V get WORK)'; do
+    grep -qE "$sub_re" <<<"$line" || fail "$name" "the pattern misses: $line"
+  done
+  for line in 'IFS= read -r -d "" OUT < <($V get -z OUT)' 'PORT=$($V get PORT)' 'SID=$($V get SID)' 'x=$($V get OUTPUT)'; do
+    ! grep -qE "$sub_re" <<<"$line" || fail "$name" "the pattern takes this line for a path read through a substitution: $line"
+  done
+  for file in "$skill"/SKILL.md "$skill"/features/*.md; do
+    hits=$(code_units "$file" | grep -nE "$sub_re" || true)
+    [[ -z $hits ]] || fail "$name" "${file#"$skill"/} reads a path through \$(... get ...), which cuts a newline at its end: $(tr '\n' ' ' <<<"$hits")"
+  done
+  echo "ok $name: no recipe reads OUT, WORK or another path of the run through a command substitution"
+  cases=$((cases + 1))
+}
+
+# The recipe of the docs, run as it is written. VERIFY_OUT can end in a newline (and WORK follows it), a command substitution would
+# cut it, and the next file that a caller writes would go to another path. The state dir and the run.env are hand-made, in the
+# resolved path of this proof's temp dir. `get` starts no run.
+doc_recipe_case() {
+  local name=doc-recipe file recipe dir out_want work_want rtmp repo got
+  need_docs "$name"
+  rtmp=$(realpath -- "$TMP")
+  repo=$(realpath -- "$skill/../../..")
+  dir=$(mktemp -d "$rtmp/vcn.XXXXXX")
+  out_want=$'/tmp/a b OUT=/x\t\'q"\nline2\n'
+  work_want=$dir/work$'\n'
+  printf 'VCN_STATE=%q\nOUT=%q\nWORK=%q\nNODE_DIR=/usr/bin\nJQ_BIN=/usr/bin/jq\n' "$dir" "$out_want" "$work_want" >"$dir/run.env"
+  printf '%s' "$out_want" >"$TMP/out.want"
+  printf '%s' "$work_want" >"$TMP/work.want"
+  got=$(cd "$repo" && env VCN_STATE="$dir" V="$V" bash -c 'OUT=$($V get OUT); printf %s "$OUT" >"$1"' _ "$TMP/out.got" 2>&1) ||
+    fail "$name" "the control, a command substitution, failed: $got"
+  ! cmp -s "$TMP/out.got" "$TMP/out.want" || fail "$name" "the control read OUT whole through a command substitution, so the case would not see a cut"
+  for file in "$skill"/SKILL.md "$skill"/features/README.md; do
+    recipe=$(code_units "$file" | grep -F 'getz()' || true)
+    [[ -n $recipe && $(grep -c '' <<<"$recipe") == 1 ]] || fail "$name" "${file#"$skill"/} must hold one inline recipe with getz(), found: ${recipe:-none}"
+    rm -f "$TMP/out.got" "$TMP/work.got"
+    got=$(cd "$repo" && env VCN_STATE="$dir" V="$V" bash -c "$recipe"$'\n''printf %s "$OUT" >"$1"; printf %s "$WORK" >"$2"' _ "$TMP/out.got" "$TMP/work.got" 2>&1) ||
+      fail "$name" "the recipe of ${file#"$skill"/} failed: $got"
+    cmp -s "$TMP/out.got" "$TMP/out.want" || fail "$name" "the recipe of ${file#"$skill"/} read OUT as '$(cat "$TMP/out.got")', not the whole value"
+    cmp -s "$TMP/work.got" "$TMP/work.want" || fail "$name" "the recipe of ${file#"$skill"/} read WORK as '$(cat "$TMP/work.got")', not the whole value"
+  done
+  echo "ok $name: the recipe of SKILL.md and of features/README.md read OUT and WORK whole, with a newline at their end"
+  cases=$((cases + 1))
+}
+
 bare_tools_case
 doc_vars_case
 no_source_case
+doc_get_exact_case
+doc_recipe_case
 echo "CASES $cases"
diff --git a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh
index 36f4a7959..a2f46056d 100755
--- a/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh
+++ b/.agents/skills/verify-claudecode-nvim/scripts/vcn.sh
@@ -103,7 +103,7 @@ load() {
   # A run.env that has no NODE_DIR yet (launch stopped while it wrote the file) is left to cleanup: nothing runs agent-tty for it.
   if [[ -n ${NODE_DIR+x} ]]; then
     why=$(bad_node_dir "$NODE_DIR")
-    [[ -z $why ]] || die "NODE_DIR=$NODE_DIR in $VCN_STATE/run.env is not usable: $why"
+    [[ -z $why ]] || die "NODE_DIR=$NODE_DIR in $VCN_STATE/run.env is not usable: $why. No command, cleanup included, runs agent-tty with it. To stop this run by hand, stop its nvim and agent-tty processes, then remove its state dir: rm -rf $(printf %q "$VCN_STATE")"
   fi
   # A run that an older vcn.sh started has no JQ_BIN.
   [[ -n ${JQ_BIN-} ]] || JQ_BIN=$(bin jq)

From 760887119126a36c26e5536f215fa3df1d732c60 Mon Sep 17 00:00:00 2001
From: Thomas Kosiewski 
Date: Thu, 12 Nov 2026 06:35:03 +0000
Subject: [PATCH 8/9] docs(skills): give the time range of the refusal proof
 that the last gate measured
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The gate of the previous commit ran proof-launch-refusals.sh (42 PASS lines) in 149 s on
a host at a load of about 20. Earlier runs took 163 s, 287 s and 338 s. SKILL.md now says
2 to 6 minutes (149 s to 338 s).

_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
---
 .agents/skills/verify-claudecode-nvim/SKILL.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md
index c3874a228..a995d40f7 100644
--- a/.agents/skills/verify-claudecode-nvim/SKILL.md
+++ b/.agents/skills/verify-claudecode-nvim/SKILL.md
@@ -131,7 +131,7 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul
 - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`.
 - `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused, `cleanup` included, which names the `rm -rf` of the state dir for stopping the run by hand (an absolute `NODE_DIR` that holds no node is not refused, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1.
 - `scripts/proof-static.sh` proves five things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` (also in `$(( ))`) sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them, no script and no recipe sources a `run.env` except `load` in `vcn.sh`, no recipe reads a path of the run (`OUT`, `WORK`) through `$(... get NAME)`, which cuts a newline at its end, and the recipe that `features/README.md` and this file give for reading `OUT` and `WORK` returns both whole for a `VERIFY_OUT` that ends in a newline (the case runs the documented line on a hand-made `run.env`). A code block is a fence of three or more backticks or tildes with any indent, and an inline span that a line break splits is one span. A comment sets and sources nothing, and an assignment or a source in one does not count. A source after `builtin`, `command` or `eval`, in backticks or in quotes, is found. The checks do not see an indented code block, `
`, a command that a variable holds, or a source in a `.lua`, `.py` or `.mjs` file. A missing `SKILL.md` or `features/*.md` fails them. A block or span that sources a `run.env` is left out of the first two checks. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `.
-- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0700` or `0755`: each such case requires the launch to go on to `agent-tty doctor`, so a guard that refuses a safe dir with any message fails it, and that launch refuses your `0700` dir when `/tmp` is world-writable without the sticky bit, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 3 to 6 minutes (163 s to 338 s measured, depending on the load of the host), because most cases start a launch.
+- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0700` or `0755`: each such case requires the launch to go on to `agent-tty doctor`, so a guard that refuses a safe dir with any message fails it, and that launch refuses your `0700` dir when `/tmp` is world-writable without the sticky bit, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 2 to 6 minutes (149 s to 338 s measured, depending on the load of the host), because most cases start a launch.
   - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`.
   - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`.
   - The `race` case puts a `mkdir` shim first on `PATH`. The shim plays another launch that makes the dir above `VERIFY_OUT` first, group-writable. Launch must refuse that dir in the check after `mkdir` and leave it in place.

From 98653693c26b52738918fa4bead496bf4da82b8d Mon Sep 17 00:00:00 2001
From: Thomas Kosiewski 
Date: Thu, 12 Nov 2026 08:41:08 +0000
Subject: [PATCH 9/9] docs(skills): give the refusal proof's slowest measured
 time
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The last gate ran proof-launch-refusals.sh in 626 s on a host at a load
of 50 to 90. SKILL.md said 149 s to 338 s. Name the range that the
gates measured: 149 s to 626 s.

_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking:
---
 .agents/skills/verify-claudecode-nvim/SKILL.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.agents/skills/verify-claudecode-nvim/SKILL.md b/.agents/skills/verify-claudecode-nvim/SKILL.md
index a995d40f7..b091ff9dc 100644
--- a/.agents/skills/verify-claudecode-nvim/SKILL.md
+++ b/.agents/skills/verify-claudecode-nvim/SKILL.md
@@ -131,7 +131,7 @@ To confirm, `grep -lzxF "VCN_RUN_TAG=$VCN_STATE" /proc/[0-9]*/environ 2>/dev/nul
 - `scripts/init.lua` is the nvim config. It puts this checkout first on `runtimepath`, appends each `VCN_RTP` dir, sets `terminal.provider = "none"` so no `claude` CLI starts, and merges `VCN_SETUP`.
 - `scripts/proof-agent-tty-resolution.sh` proves how launch picks an agent-tty and loads `VCN_RTP`, with stand-ins for a broken agent-tty and for mise: launch skips an agent-tty that fails `agent-tty doctor`, `VCN_AGENT_TTY` wins, launch exits 1 with the fix message when none passes, `require()` finds a module in each `VCN_RTP` dir, a `run.env` without `JQ_BIN` still runs `jq`, a `run.env` whose `NODE_DIR` is empty, relative or has a colon is refused, `cleanup` included, which names the `rm -rf` of the state dir for stopping the run by hand (an absolute `NODE_DIR` that holds no node is not refused, so `cleanup` can still run), a `VCN_STATE` that is not its own resolved path (a `.` or `..` part, a symlink, a trailing `/`, `/.` or `//`), is group-writable, sits under a dir that others can write (also when the dir's name ends in a space, a tab or a newline), belongs to another user, or sits under a dir that another user owns, is refused and its `run.env` is not sourced, and a `state_checked` in the environment does not skip that check (the two refusals for another user's dir run in a `bwrap` user namespace and print `SKIP` where `bwrap` is missing, cannot build the namespace, or no root-owned `0755` dir (`/srv`, `/opt`, `/usr` or `/etc`) exists for the top layer of its overlay), a state dir or a dir above it that only the group, or only others, can write is refused, a walk that gets one `stat` record too few refuses the state dir, a state dir whose name ends in a newline is accepted, a symlink in `TMPDIR` does not leave the socket dir, `record` writes none of another user's bytes after a second symlink of `TMPDIR` is repointed, `get` answers the values of a hand-made `run.env` exactly (a path with a space, an equals sign, quotes and a newline, at its end too with `-z`) and refuses a name that `run.env` does not hold, `get` and each of the five journeys refuse a state dir that others can write before they source its `run.env`, `journey-opendiff-accept.sh` writes all its files into the `OUT` of its run for a `VERIFY_OUT` with ` OUT=` in it, a newline in it or at its end, and for an `OUT` that the caller exported (`journey-out`), `$V dashboard` shows the running session in a terminal (`script(1)` stands in for one, and the case prints `SKIP` without it), a command run with a `TMPDIR` that does not exist still works, and `record` on a run without `$VCN_STATE/tmp` makes the dir (mode `0700`) and writes a WebM, SIGTERM to a running launch leaves no state dir or process, a second signal does not stop the teardown (a Node stand-in for `agent-tty home forget` finishes), a storm of signals leaves no run behind, the socket directory that agent-tty made is removed, a child killed from outside gets the full teardown, a signal during the failure screen of a launch that failed by itself leaves exit 1 and a screen with text, a signal before the teardown of such a failure has started gets the fast teardown, `cleanup` removes a run that has no agent-tty, the proof never reads or cleans a `/tmp/vcn.*` dir that it did not start, because it runs every launch with a private `TMPDIR`. It starts real runs, so it needs everything under Needs. It prints `ok ` per case and ends with `CASES `, or prints `FAIL : ` and exits 1.
 - `scripts/proof-static.sh` proves five things by reading the skill's own files, with no run and no `agent-tty`: `vcn.sh` has no `jq` or `setsid` command except through `$JQ_BIN` and `$SETSID_BIN` (not even as the default in `${JQ_BIN:-jq}`), every recipe in `SKILL.md` and `features/*.md` that expands `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` (also in `$(( ))`) sets it with `VAR=$(` in the same code block (for inline code, in the same doc), because a fresh shell has none of them, no script and no recipe sources a `run.env` except `load` in `vcn.sh`, no recipe reads a path of the run (`OUT`, `WORK`) through `$(... get NAME)`, which cuts a newline at its end, and the recipe that `features/README.md` and this file give for reading `OUT` and `WORK` returns both whole for a `VERIFY_OUT` that ends in a newline (the case runs the documented line on a hand-made `run.env`). A code block is a fence of three or more backticks or tildes with any indent, and an inline span that a line break splits is one span. A comment sets and sources nothing, and an assignment or a source in one does not count. A source after `builtin`, `command` or `eval`, in backticks or in quotes, is found. The checks do not see an indented code block, `
`, a command that a variable holds, or a source in a `.lua`, `.py` or `.mjs` file. A missing `SKILL.md` or `features/*.md` fails them. A block or span that sources a `run.env` is left out of the first two checks. `mise run check` runs it, so CI does. It prints `ok ` per case, then `CASES `.
-- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0700` or `0755`: each such case requires the launch to go on to `agent-tty doctor`, so a guard that refuses a safe dir with any message fails it, and that launch refuses your `0700` dir when `/tmp` is world-writable without the sticky bit, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 2 to 6 minutes (149 s to 338 s measured, depending on the load of the host), because most cases start a launch.
+- `scripts/proof-launch-refusals.sh` proves that launch exits 1 and leaves no run behind when `initialize` fails (it sends `jsonrpc` `1.0` and the plugin answers -32600), and when `VERIFY_OUT` or the default parent dir is unsafe or cannot be created, and when `TMPDIR` or a dir above it is world-writable and not sticky, or `TMPDIR` does not exist or has a `.` or `..` part (`G/L/../y`), or `TMPDIR` is a symlink in a dir that others can write, or a symlink that another user owns (a `bwrap` case that prints `SKIP` where `bwrap` or a root-owned `/var/run` symlink to `/run` is missing), or a symlink to a loose dir whose name ends in a newline, and when `mktemp` answers with a path that `load` refuses and launch leaves no state dir and no evidence dir behind, and when `node` is found through a relative `PATH` entry (no mise), because its dir would go on `PATH` in every `agent-tty` call, and when a dir that others can write sits above `VERIFY_OUT` as given or as resolved (a symlink in its path leads into one, or sits in one), and when `/tmp/agent-tty` is a symlink, is group- or world-writable or is owned by another user (`bwrap` cases with a `/tmp` of their own, which print `SKIP` where `bwrap`, a root-owned `0755` dir to bind, or a user namespace is missing). It also proves that launch makes `/tmp/agent-tty` with mode `0700` when it is missing and accepts one of yours with mode `0700` or `0755`: each such case requires the launch to go on to `agent-tty doctor`, so a guard that refuses a safe dir with any message fails it, and that launch refuses your `0700` dir when `/tmp` is world-writable without the sticky bit, that a sticky `TMPDIR` is accepted, that a `TMPDIR` symlink and a safe dir whose names end in a newline are read whole, and that a symlink to it gives a state dir with no symlink in its path, and that a symlink named `vcn` in a sticky `TMPDIR` does not change which dirs are checked, that `TMPDIR=/` gives `mktemp` the template `/vcn.XXXXXX` (not `//vcn.XXXXXX`), and that a `VERIFY_OUT` under a symlink works when `stat` prints translated file types. It also proves that a refused launch leaves the proof's temp dir as it found it, and that a relative `VERIFY_OUT` that starts with `-` works. It prints `PASS ` per case or `FAIL: `. It takes 2 to 11 minutes (149 s to 626 s measured, depending on the load of the host), because most cases start a launch.
   - The `out-dash`, `out-acl`, `out-made` and `init` cases start a real run, so they need everything under Needs, including Playwright Chromium for the user who runs the proof. Without it, `out-dash` fails at `agent-tty doctor`.
   - The `out-acl-unremovable`, `out-acl` and `out-made` cases need `setfacl` and a filesystem with default ACLs. Without them, the proof prints `SKIP` for all three. `out-acl` checks that every evidence file of a run in a `0500` dir with a default ACL is `0600`. `out-made` checks that launch creates a new `VERIFY_OUT` two levels below a dir with a default ACL, makes both new dirs `0700` with no ACL left on either, and that every evidence file is `0600`.
   - The `race` case puts a `mkdir` shim first on `PATH`. The shim plays another launch that makes the dir above `VERIFY_OUT` first, group-writable. Launch must refuse that dir in the check after `mkdir` and leave it in place.