Repository navigation
fix(skills): make doc-get-exact an exact allow-list of the getz recipe - #576
Conversation
…et-exact
The doc-get-exact case of proof-static.sh stopped a command substitution at its first ")" and read a "<(" only when one simple
pattern matched. A get of OUT or WORK that cut the newline at the end of the path passed in these shapes: a nested
substitution before the get, a "<(" with a cd or a second command, a read that a group or a loop wraps, and a read with no IFS=.
path_reads is now a small awk scanner that tracks quotes and a stack of open "$(", "<(" and "(" groups. It flags a get of a path
name in any open "$(" and in every "<(" except IFS= read -r -d '' NAME < <(COMMAND get -z NAME). The header, the ok line and the
SKILL.md bullet say what is checked and what is not.
_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
|
@codex review |
|
@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: 55e6824434
ℹ️ 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".
The awk scanner of doc-get-exact parsed quotes and parentheses, and each review round found one more shape it missed
(a nested substitution, a "<(" with two commands, a read in a group, a quoted 'get' word). No doc or script has any of them.
The check now reads text and parses no shell. It joins a line that ends in a backslash to the next one, deletes every quote mark
and backslash, and finds each "get [-z] WORD". WORD passes when it is PORT, SID, NVIM_PID, TUI_PID, NVIM_08, CLIENT_PID*, a
lowercase word or the placeholder NAME or <NAME>. For any other WORD the whole line must equal the getz() line of
features/README.md byte for byte, so the copy in SKILL.md must equal it too. The header, the ok line and the SKILL.md bullet say
what is checked. They drop the limits that this check makes wrong and keep one: a get or a name that a shell expansion builds.
_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
ThomasK33
changed the title
|
@codex review |
|
@codex security review |
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
🛡️ 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. |
…get-exact
A mutant of the word loop that stops at a pass word survived every self-test, because no sample had a get of a name that holds no
path before a get of a path on one line. The sample PORT=$("$V" get PORT); OUT=$("$V" get OUT) must be flagged now.
The scan of the real docs also stayed green when the loop dropped SKILL.md, dropped features/*.md or read only the units that
source a run.env. The case now counts the docs it reads against every .md file of the skill and counts the recipe lines it sees,
which must be at least two (SKILL.md and features/README.md).
_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
_Generated with xum • Model: anthropic:claude-sonnet-5-5 • Thinking: xhigh_
|
@codex review |
|
@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: 1e2057d548
ℹ️ 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".
|
Maintainer decision (ThomasK33, 2026-11-13, in the agent chat): option B for this PR. Waiver recorded before the merge: merge Generated with |
Why
#566 made the
doc-get-exactcase ofproof-static.shflag 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, areadin 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.shandSKILL.md.scripts/vcn.shand both launch proofs are unchanged.doc-get-exactnow reads text and parses no shell. The one line that reads a path whole is thegetz()recipe offeatures/README.md, whichdoc-recipealready runs. So in a code block or a single-backtick inline span thatcode_unitsreads, a plain shellgetof 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_unitsoutput), the check does five steps.g"et",O'UT'and\get.get, an optional-z, and the word after them.-znever counts as that word. Agetof a name that holds no path does not end the search on its line.PORT,SID,NVIM_PID,TUI_PID,NVIM_08or a name that starts withCLIENT_PID(none holds a path), a lowercase word (forclaude mcp get nvim), or the placeholderNAMEor<NAME>.$, the whole original line must equal the recipe line offeatures/README.md, byte for byte. So the copy inSKILL.mdmust equal the copy in the README.After the doc loop, the case checks that it read every
.mdfile 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 arun.env, fails that check. A doc that the loop skips after the count is not caught. Any other.mdfile in the skill, a dot-named one included, also makes the check fail, and the message does not print the count thatfindgot.The
proof-static.shheader, theok doc-get-exactline and theSKILL.mdbullet 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
OUTorWORKonly with the one recipe line. The shapes under Stated limits pass. Any other line there withget OUT,get -z OUT,get WORKand so on fails, in a comment or in a string too. The failure names the doc and the line. The old allowed formIFS= read -r -d '' OUT < <("$V" get -z OUT)now fails in a doc.Stated limits
These shapes pass although they hold a
getof a path. Main's previous version missed them too.code_unitsreads only single-backtick spans.xargspasses, as inOUT=$(printf OUT | xargs "$V" get).get, as inget</dev/null OUT. Bash runs it asget OUT.<code>span.{ "get", "OUT" }.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.
Other limits:
getword 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$.features/README.mdis the anchor and is trusted as written.doc-reciperuns it, but nothing flags an extragetthat someone adds to it.SKILL.mdandfeatures/*.md). It does not read the scripts. The five journeys define their ownget()helper with the safe read, andproof-agent-tty-resolution.shtestsgetitself.<pre>, a fence that markdown would not open, and four shapes that no file of the skill has (asourcewhoserun.envis on the next line after a backslash, a quoted command word,BASH_ENV, and a use ofPORT,SID,NVIM_PIDorNODE_DIRwithout a$).getin a pipe or a file that feedsread, agetwhose name is a variable, ageton the next line of a substitution, and a backtick substitution ofgetin a code block.Evidence
Gate on
1e2057d5:mise run clean && mise run allexits 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.shon 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 quotedgetand-zwords, 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,-zremoved). All hold on the real files.Scan. The case reads 13 docs (
SKILL.mdand 12features/*.md) and finds 0 hits. I also ran the rule on every line of the scripts. The hits are expected: theget()helper of each of the five journeys (3 lines each), 13 lines ofproof-agent-tty-resolution.sh(tests ofgetitself), the self-test samples ofproof-static.sh, and 3 usage lines ofvcn.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 atdoc-get-exact. The three cases before it printok.OUT, b02 dropsPORT, b03 drops theCLIENT_PIDrule, b04 drops the lowercase rule, b05 drops the<NAME>bracketsOUT=$($V get OUT). b02 to b05 flag a line that reads no path-z, b08 counts an empty word as a miss, b09 has no word-start guard$($V get PORT),get -z CLIENT_PID_a,get -zandforget OUTPORTbefore a get ofOUTgetz, b12 accepts a prefix, b13 never accepts'get' OUT,"get" OUTandge\t OUTgplusetand trailing-backslash samplesSKILL.md, b24 dropsfeatures/*.md, b25 reads only the units that source arun.envSKILL.md, d2 adds a substitution, d3 the old allowed form, d4 a quoted'get', d5 a nested substitution, d6 two joined lines, d7 ageton the next line of a substitution, d8 a group that feedsread, d9read -d ''withoutIFS=, d10get $'OUT', d11 a backtick substitution in a code block, d12 a pipeSix doc breaks (quoted
'get', joined lines,geton the next line of a substitution,$'OUT', backticks in a code block, a pipe) ran green on the previous head55e68244. 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• Model:anthropic:claude-sonnet-5-5• Thinking:xhigh