Repository navigation
Conversation
The TypeScript adapter that json-report-cli-adapter-source generates ran
the CLI with spawnSync(binaryPath, args, {cwd, env, input, maxBuffer}) and
no timeout. On Unix-like systems, Node gives the child one end of a
Unix-domain socket pair for the input option, writes the input, shuts down
writing and keeps its end open until the child exits. On macOS, a child
blocked in read(2) on that socket is sometimes not woken by the shutdown,
so an adapter call that passed input could block forever. With the adapter
generated by the parent commit, Node 26.11.1 and the CLI on 59 captured
spec-proof-bundle-admission inputs (58 of them 514 to 585 KB as stable
JSON), 9 of 3540 calls on darwin/arm64 did not return within 5 seconds.
The one held for 60 seconds stayed blocked, with a Unix socket as its
standard input. The adapter generated by this commit returned in all of
2950 such calls.
- The generated runProofkitCommand writes the stable JSON input to a file
created with O_EXCL and mode 0600 in a fresh mkdtemp directory under
os.tmpdir() of the calling process, opens it read-only and gives that
descriptor to spawnSync as stdio[0]. Except on Windows, it then removes
the file and the directory by path (rmSync of the file, rmdirSync of
the directory) before the CLI starts, so the CLI reads a file that no
longer has a name, and a signal that ends the calling process during
the call leaves no input on disk. When the call returns or throws, the
descriptor is closed and whatever is not yet removed is removed: on
Windows, where an open file can keep its name until it is closed, after
a throw before the early removal, and after a failed early removal. The
removal needs no descriptor of its own, and a failed removal fails the
call. Errors of this transport are thrown through
formatProofkitCliError, as the errors that spawnSync returns already
were.
- A call without input (inputMode "none") gives the child the null device
instead of a shut-down socket. The adapter passes no --input flag for
such a call, so the CLI does not read its standard input.
- cwd, env and maxBuffer are passed as before, and stdout, stderr, status
and the errors that spawnSync returns are handled as before. Argument
errors that spawnSync throws itself, such as a negative maxBuffer or a
NUL byte in binaryPath, cwd or an env value, are now thrown as plain
Errors carrying formatProofkitCliError's redacted, bounded message,
without Node's error class or code. A secret-shaped env value that
Node's message quotes is therefore redacted, where it was shown before.
A child that exits without reading a large input no longer makes the
call throw EPIPE; the call reports the child's status and diagnostic
instead.
- The generated source is 1189 lines with digest
sha256:e782b2cb6e17f1671a43418cf224a566365a4ebe90730a40699adbffbd1b0ac4.
The bundle keeps its record shape, generatorId
proofkit.json-report-cli-adapter-source.typescript.v2 and contractId
proofkit.json-report-cli-adapter-source.output.v1. Neither the CLI
contract nor a bound requirement statement specifies how the adapter
feeds the CLI's standard input, so under the contract-identity rule of
docs/proofkit-contract-map.md this is a defect correction.
- proofkit/cli-contract.v2.json re-pins the native-source digest of the
command's output contract. The generated contract projections and the
public CLI ABI hash follow from that digest.
- scripts/generated-starter-structure.test.mjs declares the byte deltas of
the three adapter bundle rows from the frozen predecessor streams: the
imports, the transport, the source digest and the pretty and compact
line count. The corpus is unchanged.
- A source check requires that the single spawnSync call passes exactly
cwd, env, maxBuffer and a stdin descriptor, with no input member, and
that the input file is removed by path right after it is opened, except
on Windows. The generated-adapter semantics test probes the child's
standard input: a regular file of mode 0600 with no remaining link that
holds exactly the stable JSON, alone in a mode 0700 directory when it is
opened and gone before the child runs, or the null device for a call
without input, although the harness's own standard input is a pipe.
The Windows branch, run by reporting win32 as the platform, keeps the
file under its name until the call returns. Simulated failures of the
read-only open, of either removal call and of the end-of-call removal
make the call throw and leave no descriptor open; only the failed
end-of-call removal leaves the directory. The test also covers an early
refusal, maxBuffer, a negative maxBuffer, a secret-shaped env value, a
missing binary and a missing temporary directory.
- README.md states where a call with input writes it, that the caller
needs a writable temporary directory, when the input is removed on
Windows and elsewhere, and when it can remain on disk.
No timeout is added.
Proof on this tree:
A local npm run check sequence on darwin/arm64 passed (exit 0) on tree
a17845a with Node 26.11.1, npm 12.2.0, CPython 3.15.0 and Go 1.27.3,
with no Go test verdict replayed from the test cache: 561/561 runtime
browser cases in Chromium, Firefox and WebKit with zero retries. One
recorded deviation: the host firewall blocks Go-built binaries from the
network, so go:vulncheck ran against a vulnerability-database snapshot
fetched with curl (modified 2026-10-21T00:27:29Z): no vulnerabilities.
This was referenced Oct 24, 2026
This branch has not been deployed
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.
fix(adapter): give the generated adapter's CLI child its input as a file
Part of the UI-DESIGN-01 chain, stacked on it. The change itself is a consumer-facing defect fix, not UI work.
chain/tx-cli-stdin(fix(test): give spawned CLI children their input as a file, not a socket #232, the test-transport fix), which sits on test(browser): assert media emulation in the document under test #231. This PR is one commit on that branch's head. Merge after fix(test): give spawned CLI children their input as a file, not a socket #232.The fix ships in the release after 0.17.0. The 0.17.0 change record is closed and is not edited here.
Why
The TypeScript adapter that
json-report-cli-adapter-sourcegenerates runs the Proofkit CLI withspawnSync(binaryPath, args, {cwd, env, input, maxBuffer})and no timeout. The previous PR in this chain showed the mechanism, with C and Go reproducers:inputoption. It writes the input, callsshutdown(SHUT_WR)and keeps its end open until the child exits.read(2)on that socket is sometimes not woken by the shutdown.So in the adapter, a call with input can block forever. The defect predates 0.16.0, which ships the same adapter source bytes.
Reproduction on darwin/arm64 with Node 26.11.1:
spec-proof-bundle-admissioninputs; 58 of them are 514 to 585 KB.sha256:e9089d40…, as in 0.16.0)sha256:e782b2cb…)sha256:b93c6917…)What changes
The generated adapter (
internal/command/jsonreportcliadaptersource):O_EXCLand mode 0600, in a freshmkdtempdirectory (mode 0700) underos.tmpdir()of the calling process. It opens the file read-only and passes that descriptor as the child'sstdio[0].rmSyncof the file, thenrmdirSyncof the directory) before the CLI starts. The CLI reads a file that no longer has a name. A signal that ends the calling process during the call leaves no input on disk.formatProofkitCliError.inputMode: "none") give the child the null device instead of a shut-down socket. The adapter passes no--inputflag for these calls, so the CLI never reads stdin there; the change removes the same mechanism from this path too.cwd,envandmaxBufferare passed as before.spawnSyncreturns are handled as before.spawnSyncthrows itself, for example a negativemaxBufferor a NUL byte inbinaryPath,cwdor anenvvalue, now go throughformatProofkitCliErrorlike the adapter's other errors.Errors with its redacted, bounded message, without Node's error class or code.envvalue is now redacted instead of shown.TMPDIR, notoptions.env, because the parent writes and removes the file and the child gets only a descriptor./tmpis safe: the directory name is unpredictable, its mode is 0700, andO_EXCLrefuses a pre-existing file or symbolic link.Tests:
spawnSynccall passes exactlycwd,env,maxBufferand a stdin descriptor, with noinputmember. The input file is removed by path right after it is opened, except on Windows.win32as the platform; Windows itself is not tested. The file keeps its name until the call returns, and is then removed.--inputflag and no directory.maxBuffer;maxBuffer(a plainError, no code);envvalue (redacted);Records, each re-pinned from tool or test output:
proofkit/cli-contract.v2.json, the generated contract projections that follow from it, and the public CLI ABI hash.scripts/generated-starter-structure.test.mjsdeclares five exact byte deltas for the three adapter bundle rows against the frozen predecessor streams: the imports, the transport, the source digest, and the pretty and compact line count. Each delta has refusal checks. The frozen corpus is unchanged.README.md states:
Other sites checked; none uses the mechanism:
os.execveon POSIX, andsubprocess.runwithout input otherwise;shlauncher, whichexecs the binary;Contract identity and compatibility
Contract identity. Under the rule in
docs/proofkit-contract-map.md,contractIdstaysproofkit.json-report-cli-adapter-source.output.v1andgeneratorIdstays…typescript.v2:source,sourceSha256andlineCounttake new values of unchanged types.Compatibility against 0.16.0: not breaking.
--outputcalls.spawnSync … EPIPE.spawnSyncthrows itself are now plainErrors. Examples are a negative or non-numericmaxBuffer, or a NUL byte inbinaryPath,cwdor anenvvalue.formatProofkitCliError.RangeError,TypeError) and code (ERR_OUT_OF_RANGE,ERR_INVALID_ARG_TYPE,ERR_INVALID_ARG_VALUE).envvalue, 0.16.0 threw Node's message with the value in it, secret-shaped or not.Suggested entry for the change record of the release after 0.17.0:
changeId:proofkit.json-report-cli-adapter-source.stdin-filesummary: "The TypeScript adapter that json-report-cli-adapter-source generates no longer gives the CLI its JSON input through spawnSync's input socket, on which a macOS child could stay blocked forever. A call with input writes the input to a file created with mode 0600 in a fresh mode 0700 directory under the calling process's temporary directory and gives the CLI that file, opened read-only, as its standard input; the caller therefore needs a writable temporary directory. Except on Windows, the file and directory are removed before the CLI starts; on Windows, which is not a supported platform and does not apply these modes, they are removed when the call returns or throws. The input can remain on disk only if the calling process ends before that removal or the removal fails, and a failed removal fails the call. A call without input gives the child the null device. A CLI that refuses before reading a large input now reports its own diagnostic instead of an EPIPE error. Argument errors that spawnSync throws itself are now plain Error objects with the adapter's redacted, bounded diagnostic, without Node's error class or code, so a secret-shaped env value in such a message is redacted. The generated source bytes, sourceSha256 and lineCount change; the record shape, generatorId and contractId are unchanged."Proof
Proof: A local
npm run checksequence on darwin/arm64 passed (exit 0) on treea17845a6e8e2with Node 26.11.1, npm 12.2.0, CPython 3.15.0 and Go 1.27.3, with no Go test verdict replayed from the test cache: 561/561 runtime browser cases in Chromium, Firefox and WebKit with zero retries. One recorded deviation: the host firewall blocks Go-built binaries from the network, sogo:vulncheckran against a vulnerability-database snapshot fetched with curl (modified 2026-10-21T00:27:29Z): no vulnerabilities.Narrow evidence on darwin/arm64 with Node 26.11.1 (CI's version; the host default is 26.12.0):
ulimit -n 64, a call leaves no descriptor open and no input file.input, directly or through an alias;input:key;rmSync;O_EXCL;maxBufferorenvdropped;go test -p 2 -count=1 ./...passes (148 packages).npm run command-contract:check,source-hygiene,text-policyandmermaid:checkpass.node --test scripts/generated-starter-structure.test.mjspasses 6/6.tsc --strict, and with--exactOptionalPropertyTypes, as before.git diff --checkover the range is clean.Non-claims
win32as the platform, not on Windows.