Repository navigation
fix(skills): say only what the static proof sees and make the getz recipe fail loudly - #566
Merged
Merged
Conversation
…cipe fail loudly Follow-up to #545 from its readiness advisor. - proof-static.sh: the header, the ok lines and the SKILL.md bullet name what each scanner sees and list the four shapes it does not (a source that a backslash splits, a quoted source, BASH_ENV, let and (( ))). - doc-get-exact also flags $(... get -z NAME) and a read without -d ''. - doc-recipe uses a value with a backslash, runs each documented line with no V of its own, and needs a refused get (a state dir that load refuses, no OUT, no WORK) to exit 1 with a message. - getz prints "vcn.sh get <NAME> failed" and returns 1, the line joins the two calls with &&, and the SKILL.md line sets V itself. - SKILL.md: the "Keep it short" sentence of TMPDIR is back after "the default passes.", and the refusal proof's time has no maximum. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
Codex Review Summary: ✅ CompletedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 44d57979c1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
… stop the call on a refused get Codex review of #566 and the readiness advisor found gaps in the new checks. - doc-get-exact: the -d '' test now looks at the read that takes the value, not at the whole line. A quoted name (get -z "OUT") counts. - doc-recipe: the refused-get runs keep a directory and a name in two arrays, so a state dir with a colon in its path works, and the state dirs now live in a dir with a colon in its name. The recipe must exit with status 1 and no later command of the call may run. - The getz line ends with || exit 1, so the call stops after a refused get. Before, the call went on with OUT empty. - The header, the ok lines and the SKILL.md bullet say what the scanner sees: the inline code of a doc counts as one unit, two shapes are new stated limits (a read -d '' with no IFS=, a backtick substitution of get), and the left-out checks are named. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
The usage comment of vcn.sh said that "read -r -d ''" keeps a newline at the end of a value. With the default IFS, read trims it. The docs and the doc-recipe case already use "IFS= read -r -d ''". Comment only: no line of code changes. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 858a482a1f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…tatic proof Codex found that doc-get-exact reads each line alone, so a command substitution whose get sits on the next line passes. No code block and no script has that shape (a search found none), and the stop rule for this scanner is a stated limit, not another rule. The header and the SKILL.md bullet now name it. _Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
Member
Author
|
@codex review |
Member
Author
|
@codex security review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ca9c9a320b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| # path with `read -r -d ''` on `get -z`. A value that is no path (PORT, SID) can use a substitution. | ||
| path_names='OUT|WORK|VCN_STATE|ATT_HOME|NVIM_SOCK|NVIM_BIN|NODE_DIR|ATT_BIN|ATT_SOCK|JQ_BIN' | ||
| get_name_re='get[[:space:]]+(-z[[:space:]]+)?["'\'']?('"$path_names"')["'\'']?([^A-Za-z0-9_]|$)' | ||
| sub_re='\$\([^)]*'"$get_name_re" |
There was a problem hiding this comment.
When a one-line recipe contains an earlier nested substitution, such as OUT=$(cd "$(dirname "$V")"; "$V" get -z OUT), [^)]* stops at the inner closing parenthesis, so path_reads misses the unsafe outer substitution. Bash still strips trailing newlines from OUT, but doc-get-exact remains green even though this shape is not among the documented scanner limitations; scan the complete substitution or explicitly list and reject this form.
Useful? React with 👍 / 👎.
🛡️ Codex Security ReviewSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
Member
Author
|
Merge record (correction).
Generated with |
This was referenced Nov 12, 2026
hareki
pushed a commit
to hareki/claudecode.nvim
that referenced
this pull request
Nov 14, 2026
coder#576) ## Why coder#566 made the `doc-get-exact` case of `proof-static.sh` flag a documented read of a run path that cuts the newline at the end of the path. That check parsed shell with regexes and then with an awk tokenizer. Each review round found one more shape that the parser missed: a nested substitution, a `<(` with two commands, a `read` in a group or a loop, and a quoted `'get'` word. No doc or script has any of those shapes. The parser did not converge, so this PR removes it. ## What changed All changes are in `.agents/skills/verify-claudecode-nvim/`: `scripts/proof-static.sh` and `SKILL.md`. `scripts/vcn.sh` and both launch proofs are unchanged. `doc-get-exact` now reads text and parses no shell. The one line that reads a path whole is the `getz()` recipe of `features/README.md`, which `doc-recipe` already runs. So in a code block or a single-backtick inline span that `code_units` reads, a plain shell `get` of a path word passes only as that line. The shapes that the check misses, read or not, are listed under Stated limits. For each line of a code block or an inline span (`code_units` output), the check does five steps. 1. It joins a line that ends in a backslash to the next line, as the shell does. 2. It deletes every single quote, double quote and backslash. The shell does the same to `g"et"`, `O'UT'` and `\get`. 3. It finds each word `get`, an optional `-z`, and the word after them. `-z` never counts as that word. A `get` of a name that holds no path does not end the search on its line. 4. That word passes when it is `PORT`, `SID`, `NVIM_PID`, `TUI_PID`, `NVIM_08` or a name that starts with `CLIENT_PID` (none holds a path), a lowercase word (for `claude mcp get nvim`), or the placeholder `NAME` or `<NAME>`. 5. For any other word, also one that starts with a `$`, the whole original line must equal the recipe line of `features/README.md`, byte for byte. So the copy in `SKILL.md` must equal the copy in the README. After the doc loop, the case checks that it read every `.md` file of the skill (13 today) and saw the recipe line at least twice across those docs. A loop that drops a doc before that count, or reads only the units that source a `run.env`, fails that check. A doc that the loop skips after the count is not caught. Any other `.md` file in the skill, a dot-named one included, also makes the check fail, and the message does not print the count that `find` got. The `proof-static.sh` header, the `ok doc-get-exact` line and the `SKILL.md` bullet say what the scan checks. None of them mentions the doc count yet, and the header and the bullet still use the wider wording that this body narrows. The bullet no longer holds a code span that would fail the check. ## What a doc author sees In the code blocks and spans that the check reads, a plain shell line can read `OUT` or `WORK` only with the one recipe line. The shapes under Stated limits pass. Any other line there with `get OUT`, `get -z OUT`, `get WORK` and so on fails, in a comment or in a string too. The failure names the doc and the line. The old allowed form `IFS= read -r -d '' OUT < <("$V" get -z OUT)` now fails in a doc. ## Stated limits These shapes pass although they hold a `get` of a path. Main's previous version missed them too. - A double-backtick inline span that holds a backtick substitution. `code_units` reads only single-backtick spans. - A name that `xargs` passes, as in `OUT=$(printf OUT | xargs "$V" get)`. - A redirection glued to `get`, as in `get</dev/null OUT`. Bash runs it as `get OUT`. - An inline `<code>` span. - An argument list in a Lua or Python block, such as `{ "get", "OUT" }`. - A recipe copy split by a backslash and a newline inside single quotes. These shapes make the check fail on a copy of the recipe that markdown renders the same way but that differs in bytes. The check fails closed. - A copy in a fenced block inside a list item, because the block keeps the list indent. - A copy in a span that wraps across lines inside a list item. - A copy in a double-backtick span that CommonMark pads with spaces. - A copy with CRLF line ends. - A copy with one trailing space. Other limits: - A `get` word that a shell expansion builds is not seen: brace expansion (`{get,}`), a variable or an alias that holds the word, or an eval. A name that a `$'..'` or `${..}` expansion builds is flagged, because the word then starts with a `$`. - The recipe line of `features/README.md` is the anchor and is trusted as written. `doc-recipe` runs it, but nothing flags an extra `get` that someone adds to it. - The case reads the docs (`SKILL.md` and `features/*.md`). It does not read the scripts. The five journeys define their own `get()` helper with the safe read, and `proof-agent-tty-resolution.sh` tests `get` itself. - The limits of the other cases are unchanged: an indented code block, `<pre>`, a fence that markdown would not open, and four shapes that no file of the skill has (a `source` whose `run.env` is on the next line after a backslash, a quoted command word, `BASH_ENV`, and a use of `PORT`, `SID`, `NVIM_PID` or `NODE_DIR` without a `$`). - These limits of the previous version are gone, because this check makes them wrong: a `get` in a pipe or a file that feeds `read`, a `get` whose name is a variable, a `get` on the next line of a substitution, and a backtick substitution of `get` in a code block. ## Evidence **Gate** on `1e2057d5`: `mise run clean && mise run all` exits 0 in 669 s on this host. luacheck: 200 files, 0 warnings, 0 errors. Busted: 1908 successes, 0 failures, 0 errors, 36 pending. `mise run format-check`: 458 files, 0 changed. `proof-static.sh` on the real files, run on its own: `CASES 5`, exit 0. **Self-tests** in `doc-get-exact`: 73 lines must fail and 17 lines must pass, plus the recipe line itself. The 73 are the 35 lines of the previous version, 9 for quoted `get` and `-z` words, 13 quote, backslash, `$'..'` and case-pattern shapes, 1 for a get of a name that holds no path before a get of a path on one line, 9 multi-line, tab and unit-marker samples, and 6 changed copies of the recipe (a comment added before or after it, a command added, `-d ''` removed, `IFS= ` removed, `-z` removed). All hold on the real files. **Scan.** The case reads 13 docs (`SKILL.md` and 12 `features/*.md`) and finds 0 hits. I also ran the rule on every line of the scripts. The hits are expected: the `get()` helper of each of the five journeys (3 lines each), 13 lines of `proof-agent-tty-resolution.sh` (tests of `get` itself), the self-test samples of `proof-static.sh`, and 3 usage lines of `vcn.sh`. **Mutants.** Each row changes one rule of the proof (b01 to b25) or one doc (d1 to d13) and runs `proof-static.sh`. All 38 runs fail at `doc-get-exact`. The three cases before it print `ok`. | Rule | Mutants | What fails | | --- | --- | --- | | Pass list | b01 adds `OUT`, b02 drops `PORT`, b03 drops the `CLIENT_PID` rule, b04 drops the lowercase rule, b05 drops the `<NAME>` brackets | b01 misses `OUT=$($V get OUT)`. b02 to b05 flag a line that reads no path | | Word handling | b06 takes the whole token, b07 does not skip `-z`, b08 counts an empty word as a miss, b09 has no word-start guard | false positives on `$($V get PORT)`, `get -z CLIENT_PID_a`, `get -z` and `forget OUT` | | Word loop | b21 returns and b22 breaks at a pass word | both miss the line with a get of `PORT` before a get of `OUT` | | Byte equality | b10 flags nothing, b11 accepts a line that contains `getz`, b12 accepts a prefix, b13 never accepts | b10 misses. b11 and b12 pass a changed recipe. b13 flags the recipe | | Quote stripping | b14 keeps single quotes, b15 keeps double quotes, b16 keeps backslashes | misses `'get' OUT`, `"get" OUT` and `ge\t OUT` | | Line join | b17 no join, b18 joins with a space, b19 no flush at the end, b20 drops a pending line at a unit end | misses the two-line, `g` plus `et` and trailing-backslash samples | | Doc scan | b23 drops `SKILL.md`, b24 drops `features/*.md`, b25 reads only the units that source a `run.env` | the count check: 12 docs, 1 doc and 0 recipe lines are not every doc with the recipe in two | | Docs | d1 and d13 change the recipe copy in `SKILL.md`, d2 adds a substitution, d3 the old allowed form, d4 a quoted `'get'`, d5 a nested substitution, d6 two joined lines, d7 a `get` on the next line of a substitution, d8 a group that feeds `read`, d9 `read -d ''` without `IFS=`, d10 `get $'OUT'`, d11 a backtick substitution in a code block, d12 a pipe | each fails with the doc and the line | Six doc breaks (quoted `'get'`, joined lines, `get` on the next line of a substitution, `$'OUT'`, backticks in a code block, a pipe) ran green on the previous head `55e68244`. The same breaks (d4, d6, d7, d10, d11, d12) fail on this head, so this check closes shapes that the previous version missed or listed as limits. ## Not changed Nothing outside the skill changes. --- _Generated with [`xum`](https://github.com/coder/xum) • Model: `anthropic:claude-sonnet-5-5` • Thinking: `xhigh`_
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
#545's readiness advisor left five small follow-ups in the
verify-claudecode-nvimskill. Four are claims that said more than the check behind them, and one is a recipe that failed without a word. Codex and a second independent review found more gaps in the new checks, and this PR closes all but the scanner gaps listed under "Not covered".What changed
All changes are in
.agents/skills/verify-claudecode-nvim/.scripts/vcn.shchanges one comment line (the usage header, see 7) and no code.bin()and theVCN_NVIMbranch are untouched, and so are both launch proofs.proof-static.shheader, its fiveoklines and theSKILL.mdbullet say only what the scanner sees, except thedoc-get-exactgaps under "Not covered". They list what it does not see: an indented code block,<pre>, a command that a variable holds, a source in a.lua,.pyor.mjsfile, areadthat takesgetthrough a pipe or a file, and seven shapes that no code block and no code line of a script has (a command substitution orread < <(...)whosegetis on the next line, aread -d ''with noIFS=, a backtick substitution ofget, asourcewhoserun.envis on the next line after a backslash, a quoted command word such as"source" run.env, arun.envnamed throughBASH_ENV, and a use ofPORT,SID,NVIM_PIDorNODE_DIRwithout a$, as inletor(( ))). I searched the skill for each of the seven and found none. The scanner has no new rule for them: a stated limit is the fix for a shape that no file has. Thedoc-varsline also says that the inline code of a doc counts as one unit, andSKILL.mdnames the checks that skip a block that sources arun.env.doc-get-exactalso flags$(... get -z NAME), and aread ... < <(... get NAME)that has no-d ''among its own words. Anotherreadon the same line does not hide it. A name in quotes (get -z "OUT") counts as the name. A new functionpath_readsholds both rules, and the case's samples call it too.doc-recipereads a value that holds a backslash (back\slash \\ end\n, besides the newline and quotes), and runs each documented line with noVin the environment, from the repo root. Before, it suppliedV, so a line that lost its ownV=still passed. It builds its state dirs inside a dir nameda:b, so a path with a colon works.getzfails loudly.getz() { IFS= read -r -d '' "$1" < <("$V" get -z "$1") || { echo "vcn.sh get $1 failed" >&2; return 1; }; }; getz OUT && getz WORK || exit 1. Whengetrefuses, the call printsvcn.sh get <NAME> failedand stops with status 1, so no later command runs with an emptyOUT. (The first head of this PR only returned 1 from the function, and the call went on.) TheSKILL.mdline setsV=itself, as the README line does.doc-recipehas three refused-get runs per doc: a group-writable state dir (loadrefuses it), arun.envwithoutOUT, and one withoutWORK. Each must exit with status 1 exactly, name the failedget, and run no later command.SKILL.mdline 55: the sentence "Keep it short: nvim's socket ..." is back after "the default passes.". fix(skills): read run values through vcn.sh get, check the agent-tty socket dir, run the static proofs in CI #545 had put theagent-ttysentences between them.SKILL.mdline 134: the refusal proof's time is "2 minutes or more, 149 s to 966 s measured, depending on the load of the host", with no maximum. My own runs measured 149 s to 626 s. The 966 s is the figure from the issue brief.vcn.shusage comment (line 19): it said thatread -r -d ""keeps a newline at the end of a value. With the defaultIFS,readtrims it (a probe:a\nreads asa, and asa\nwithIFS=). It now saysIFS= read -r -d "". No line of code changes: the non-comment lines of the file are identical.Evidence
Every row is a mutant of the proof or of a doc, run on a copy of the final skill dir. Each red row fails at the case that the row names. The last rows are the opposite: a break that the check cannot see stays green, which shows what the check is for.
CASES 5-zin the substitution rule-zgroupdoc-get-exact: the patterns miss: x=$($V get -z OUT)readrulepath_readswithout itdoc-get-exact: the patterns miss: IFS= read -r OUT < <($V get -z OUT)-d ''only-dflag counts... read -r -d x OUT ...-d ''bound to its own read... read -r -d "" scratch <<< x; IFS= read -r OUT < <($V get -z OUT)... OUT=$($V get -z "OUT")readof a path and no-ddoc-get-exact: features/README.md reads a path ...$($V get -z OUT)or a quoted namedoc-get-exact: SKILL.md reads a path ...getzwithout-rdoc-recipe: ... read OUT as '...'Vof its owngetzwithoutV=doc-recipe: ... failed: ... command not foundgetzwithout itdoc-recipe: ... did not say 'vcn.sh get OUT failed'&&between the twogetz;in README or SKILL.mddoc-recipe: ... exited 0, wanted 1, after a refused get (OUT ...)WORKfailure{ getz WORK || :; }in README or SKILL.mddoc-recipe: ... exited 0, wanted 1, after a refused get (WORK ...)doc-recipe: did not say 'vcn.sh get b/vcn.XXXXXX:OUT failed': vcn: no run at /tmp/.../a!= 0, READMEexit 2exit 2mutant is redWORKcaseWORKgetzwithout-r, or withoutV=,$($V get -z OUT)in SKILL.md,read -r OUTof a path in the READMEget -z "OUT"Codex's colon case, reproduced first: with a colon in
TMPDIR, the old proof failsdoc-recipewithdid not say 'vcn.sh get tmp/tmp.XXXXXXXXXX/vcn.XXXXXX:OUT failed'and a truncatedVCN_STATE. The final proof passes the same run (CASES 5).Gate
On
858a482a, the last head that changed code. The final headca9c9a32adds only comment lines andSKILL.mdtext; an independent rerun ofmise run allonca9c9a32gave exit 0, 1756 successes, 0 failures, 0 errors, 28 pending, andproof-static.shCASES 5.mise run clean && mise run allluacheck: 0 warnings, 0 errors in 185 files. Itschecktask runsproof-static.shcheck.shofverify-diff-lifecycle== RESULT: PASSproof-static.shCASES 5VCN_NVIM= Neovim v0.8.0 (the official release binary),vcn.sh launch,doctor,journey-opendiff-accept.sh,cleanupPASS opendiff-accept, the state dir and the saved PIDs are gone. This ran becausevcn.shchanges (one comment line)proof-launch-refusals.sh,proof-agent-tty-resolution.sh44d57979): refusals exit 0 with 42PASSin 360 s (3 ACLSKIP), resolution exit 0 withCASES 49and noSKIPin 1765 s (a restart of the host killed its first run, so this is its second). Both proofs runvcn.sh, which differs from that head by one comment line, and neither reads another file that this PR changed, so they did not run againNot covered
$(...)with a)before itsget(for exampleOUT=$(cd "$(dirname "$V")"; "$V" get -z OUT)), aread ... < <(...)with;,&or|before itsget, and{ IFS= read -r OUT; } < <(...)orwhile IFS= read -r OUT; do ...; done < <(...). No doc or script has these shapes today. A follow-up PR fixes the scanner for them.getz OUT && getz WORK || exit 1ends the shell of the call that runs it.SKILL.mdsays that every bash call is a fresh shell, and the README starts every bash call with this line, so no session is lost, but a reader who pastes the line into a long-lived shell closes it.Generated with
xum• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh