Accept a token or credential string that stages exactly one file #112

Merged

vnprc merged 5 commits from agent/accept-single-file-token-strings into master

2026-09-23 16:49:53 +01:00

allod-agent commented

2026-09-23 05:26:27 +01:00

Member

Summary

A machine can now hand mkDevVm (and a hypervisor identity can hand modules/host-user-credentials.nix) a ciphertext built with builtins.path { path = ./secrets/x.age; name = "x.age"; }; that construction stages the one file and was refused with a message describing a leak it does not cause. Every running machine is identical: the four composed machines' toplevel derivations and all 18 check outputs match master hash for hash. The directory-interpolating form "${dir}/x.age", the one that pulls a whole source tree into the closure, is still refused, and two checks each carry a fixture that proves it is. Admitting builtins.path also admits "${./secrets/x.age}", the same string with the same context; that trade is the issue's stated decision and is recorded in nix/secret-file-form.nix. If this is wrong, revert the one commit: no machine changes either way.

What changed

New nix/secret-file-form.nix holds the predicate both call sites share: null, or a Nix path or a string whose only string-context element is a source path (path = true) equal to the string itself, and in either case a regular file. A context-free store-path string, a derivation output, a directory staged whole, and a symlink are refused.
nix/builders/dev.nix and modules/host-user-credentials.nix use it; the two assertion messages now share one explanation. modules/pi-provider-lifecycle.nix keeps its own builtins.isPath test on Pi token files; the issue does not name it and it is left for its own decision.
checks/dev-forge-opt-out.nix and checks/host-user-credentials.nix: the sabotage per argument is now the directory form ("${fixtureDir}/x.age"), since the single-file string is admitted by design; each check gains one builtins.path control (stagedTokens, stagedControl) that must evaluate. In host-user-credentials pathControl is now withAccess (same two path literals, already forced to toplevel) so the fixture count is unchanged.

Risk

R3: the assertion is a closure-leak guard. The residual worst case is a value that stages more than one file passing the new predicate. The predicate accepts only a string equal to its sole source-path context element; a directory interpolation is strictly longer than its context element, a literal has none, a derivation output's context is the .drv. Measured on Nix 2.34.8 for all five spellings before the change was written.

Validation

./check.sh on the branch: all 31 steps passed (18 checks built). Machine drvPaths and all check out paths identical to a master run of the same gate.
Negative controls, each reverted afterwards: stagesOneFile forced false made both checks fail on stagedTokens / stagedControl; isAcceptedForm forced true made both fail on directoryAgentToken / directoryUserForgejoToken.
Cross-family review (codex, gpt-5.6-sol, high effort) of the first commit returned two findings. Confirmed and fixed in the second commit: a directory staged whole, "${./secrets}" or the path literal ./secrets, passed the predicate (and had always passed the old one); isAcceptedForm now also requires builtins.readFileType not to be "directory", and bareDirectoryToken in dev-forge-opt-out sabotages that clause. Refuted with a measurement: the claim that builtins.path returns a path value and so the staged controls never reach the string clause; builtins.typeOf is "string", and forcing stagesOneFile false makes both staged controls fail. A second pass on the fixed code returned one finding: the file-type clause also admitted "symlink" and "unknown". Settled by measurement: builtins.path resolves a source symlink before copying (a symlink to a directory stages the directory and was already refused; a symlink to a file stages the regular file), and a path literal to a symlink stages only the dangling symlink, so no leak path existed. The clause is nonetheless tightened to == "regular", which refuses the dangling-symlink case a machine could never use.

Closes allod/archetypes#70

## Summary A machine can now hand `mkDevVm` (and a hypervisor identity can hand `modules/host-user-credentials.nix`) a ciphertext built with `builtins.path { path = ./secrets/x.age; name = "x.age"; }`; that construction stages the one file and was refused with a message describing a leak it does not cause. Every running machine is identical: the four composed machines' toplevel derivations and all 18 check outputs match master hash for hash. The directory-interpolating form `"${dir}/x.age"`, the one that pulls a whole source tree into the closure, is still refused, and two checks each carry a fixture that proves it is. Admitting `builtins.path` also admits `"${./secrets/x.age}"`, the same string with the same context; that trade is the issue's stated decision and is recorded in `nix/secret-file-form.nix`. If this is wrong, revert the one commit: no machine changes either way. ## What changed - New `nix/secret-file-form.nix` holds the predicate both call sites share: null, or a Nix path or a string whose only string-context element is a source path (`path = true`) equal to the string itself, and in either case a regular file. A context-free store-path string, a derivation output, a directory staged whole, and a symlink are refused. - `nix/builders/dev.nix` and `modules/host-user-credentials.nix` use it; the two assertion messages now share one explanation. `modules/pi-provider-lifecycle.nix` keeps its own `builtins.isPath` test on Pi token files; the issue does not name it and it is left for its own decision. - `checks/dev-forge-opt-out.nix` and `checks/host-user-credentials.nix`: the sabotage per argument is now the directory form (`"${fixtureDir}/x.age"`), since the single-file string is admitted by design; each check gains one `builtins.path` control (`stagedTokens`, `stagedControl`) that must evaluate. In host-user-credentials `pathControl` is now `withAccess` (same two path literals, already forced to toplevel) so the fixture count is unchanged. ## Risk R3: the assertion is a closure-leak guard. The residual worst case is a value that stages more than one file passing the new predicate. The predicate accepts only a string equal to its sole source-path context element; a directory interpolation is strictly longer than its context element, a literal has none, a derivation output's context is the `.drv`. Measured on Nix 2.34.8 for all five spellings before the change was written. ## Validation - `./check.sh` on the branch: all 31 steps passed (18 checks built). Machine drvPaths and all check out paths identical to a master run of the same gate. - Negative controls, each reverted afterwards: `stagesOneFile` forced false made both checks fail on `stagedTokens` / `stagedControl`; `isAcceptedForm` forced true made both fail on `directoryAgentToken` / `directoryUserForgejoToken`. - Cross-family review (codex, gpt-5.6-sol, high effort) of the first commit returned two findings. Confirmed and fixed in the second commit: a directory staged whole, `"${./secrets}"` or the path literal `./secrets`, passed the predicate (and had always passed the old one); `isAcceptedForm` now also requires `builtins.readFileType` not to be `"directory"`, and `bareDirectoryToken` in dev-forge-opt-out sabotages that clause. Refuted with a measurement: the claim that `builtins.path` returns a path value and so the staged controls never reach the string clause; `builtins.typeOf` is `"string"`, and forcing `stagesOneFile` false makes both staged controls fail. A second pass on the fixed code returned one finding: the file-type clause also admitted `"symlink"` and `"unknown"`. Settled by measurement: `builtins.path` resolves a source symlink before copying (a symlink to a directory stages the directory and was already refused; a symlink to a file stages the regular file), and a path literal to a symlink stages only the dangling symlink, so no leak path existed. The clause is nonetheless tightened to `== "regular"`, which refuses the dangling-symlink case a machine could never use. Closes allod/archetypes#70

allod-agent added 4 commits

2026-09-23 05:26:27 +01:00

Accept a token/credential string that stages exactly one file 93387eb6d8

mkDevVm's tokenFile/httpsTokenFile and host-user-credentials.nix's
userForgejoTokenFile/siteHostingConfigFile now accept null, a Nix path,
or a string whose only string-context element equals the string itself
- the shape builtins.path { path = ./secrets/x.age; name = "x.age"; }
produces, and the identical string "${./secrets/x.age}". The shared
predicate lives in the new nix/secret-file-form.nix, imported by both
call sites, so the two assertions stay in step.

The directory form "${dir}/x.age" still refuses: its context key names
the directory, not the file, so it fails the equality test and still
carries the whole source repository into the closure. A context-free
store-path string and a derivation output still refuse too, for the
same reason - neither's context names the one file it stages.

checks/dev-forge-opt-out.nix and checks/host-user-credentials.nix each
gain a stagedTokens/stagedControl fixture proving the builtins.path
form is admitted, and their sabotage fixtures move from the
single-file string spelling (now accepted by design) to the directory
spelling, which stays refused.

Refuse a directory staged whole through the same-string context test 3e12c4f2d7

isAcceptedForm's context test alone accepts a bare directory
interpolation, "${dir}", and the path literal dir itself: both have
one context element equal to the string, the same shape a single
staged file has. Add builtins.readFileType file != "directory" after
the form test, so a path or a same-string context that names a
directory is refused; a missing file now fails here with Nix's own
"No such file" error instead of surfacing later out of agenix's copy.

checks/dev-forge-opt-out.nix gains bareDirectoryToken, sabotaging the
file-type clause on one argument - the clause is shared code, so one
argument suffices; host-user-credentials.nix is not touched, since
it would force a module evaluation per fixture for the same shared
clause.

Name the thing, not its position, in the two new sabotage comments 0448ac04e8

Follows ab75b54: "the context clause above" and "sabotage per argument
above" go false the moment code moves. Name stagesOneFile and
directoryAgentToken/directoryForgeToken instead.

Require a regular file, not merely a non-directory df1e2b1a09

readFileType != "directory" also passed "symlink" and "unknown". A
symlink path literal stages the dangling symlink itself rather than
one file, so tighten to == "regular"; builtins.path already resolves
a source symlink before copying, so this changes no accepted
construction, only what the predicate demands of the file itself.

allod-agent referenced this pull request

2026-09-23 05:37:59 +01:00

Name the thing, not its position, in the checks' messages #113

allod-agent referenced this pull request

2026-09-23 05:43:05 +01:00

Bring the flake check's memory peak back under the dev VM's headroom #31

allod-agent commented

2026-09-23 16:00:21 +01:00

Author

Member

Merged origin/master (with allod/archetypes#113 and the allod-tools lock bump) into this branch as 9aad6ad, a plain merge with no conflicts; the adjacent-hunk collision the body warned about did not materialise. git diff origin/master on the branch is exactly this PR's five files. ./check.sh on the merged branch: all 31 steps passed, 18 checks built, every machine drvPath and check out path identical to a run on the new master.

Merged `origin/master` (with allod/archetypes#113 and the allod-tools lock bump) into this branch as `9aad6ad`, a plain merge with no conflicts; the adjacent-hunk collision the body warned about did not materialise. `git diff origin/master` on the branch is exactly this PR's five files. `./check.sh` on the merged branch: all 31 steps passed, 18 checks built, every machine drvPath and check out path identical to a run on the new master.

allod-agent added 1 commit

2026-09-23 16:00:21 +01:00

Merge remote-tracking branch 'origin/master' into agent/accept-single-file-token-strings 9aad6adf25