mkDevVm's token-path assertion refuses builtins.path, which already stages one file #70

New issue

Open

opened 2026-09-04 01:43:24 +01:00 by vnprc-agent · 0 comments

vnprc-agent commented

2026-09-04 01:43:24 +01:00

Let a deployment hand mkDevVm a token file built with builtins.path without being refused, because that construction already produces exactly the outcome the assertion protects: one .age file in the machine's closure and nothing else. Nothing is blocked by this — the workaround is a one-line switch to the path form and it costs nothing — but a correct construction is currently rejected with a message that reads as if it were the leak.

Primary goals:

Stop refusing a safe construction — builtins.path { path = ./secrets/x.age; name = "x.age"; } stages exactly that file and interpolates to the same store path as ./secrets + "/x.age", yet builtins.isPath is false on it, so the assertion rejects it.
Keep refusing the leak — the directory form "${dir}/x.age" must still fail, and its sabotage witness must still fail with it.
Decide the collateral question, not just the predicate — the only value-level test that admits builtins.path also admits "${./dir/x.age}", which the current comment refuses on purpose. That trade is the real decision here, and it may be resolved by changing nothing but the message.

Current state

flake.nix:798-801 filters tokenFile and httpsTokenFile with !(file == null || builtins.isPath file), and the message at :803-808 explains the ban as covering every string "whatever it interpolates". builtins.path returns a string: builtins.typeOf is "string" and builtins.isPath is false, even though the entire point of the call is that it copies the one named file and nothing more.

Measured on a single file, the three spellings a deployment can reach for:

spelling	value	string context	what lands in the store
`builtins.path { path = ./m/f.nix; name = "f.nix"; }`	`/nix/store/2ihkflrk…-f.nix`	`[ "/nix/store/2ihkflrk…-f.nix" ]`	the one file
`"${./m/f.nix}"`	`/nix/store/2ihkflrk…-f.nix`	`[ "/nix/store/2ihkflrk…-f.nix" ]`	the one file
`"${./m}/f.nix"`	`/nix/store/imwcmwsb…-m/f.nix`	`[ "/nix/store/imwcmwsb…-m" ]`	the whole directory

A deployment that reached for row one precisely to keep a whole repository out of a machine's closure — the outcome allod/archetypes#21 is about — is therefore refused by the assertion written to encourage that outcome.

The predicate that would work, and what it costs

The leak is distinguishable by string context rather than by type. A safe value equals its sole context element; "${dir}/x.age" is strictly longer than its context element, because the context names the directory, not the file. So builtins.isPath file || <file equals its single context path> accepts rows one and two and still refuses row three, and the existing sabotage witness keeps failing.

The cost is row two, which the current comment refuses deliberately on the ground that it is one keystroke from the leaking spelling. Any value-level predicate that admits row one admits row two as well: they are the same string with the same context, and Nix keeps no record of which expression produced it. This is not a matter of finding a sharper test — it is a choice between refusing a safe third construction and admitting a safe second one.

If the refusal of row two is worth keeping, the alternative resolution is to leave the predicate alone and fix the message, which today says to "write ./secrets + "/agent-pr-token.age", not a string" without telling a reader why a store-path string that stages one file is refused anyway. Either way closes this. The part that costs a reader time is being rejected for something that is not the mistake described.

Scope

In: the predicate behind nonPathTokenArguments at flake.nix:798-801, or the message at :803-808, whichever way the trade is decided. Whatever lands, the directory-interpolating form stays refused and provably so.

Out: allod/archetypes#21's two measured leaks — modules/agent-hooks.nix interpolating the policy source per file, and modules/github-credentials.nix writing a string into age.secrets.<name>.file. This assertion sees neither, as its own comment records, and nothing proposed here changes that.

Let a deployment hand `mkDevVm` a token file built with `builtins.path` without being refused, because that construction already produces exactly the outcome the assertion protects: one `.age` file in the machine's closure and nothing else. Nothing is blocked by this — the workaround is a one-line switch to the path form and it costs nothing — but a correct construction is currently rejected with a message that reads as if it were the leak. Primary goals: - **Stop refusing a safe construction** — `builtins.path { path = ./secrets/x.age; name = "x.age"; }` stages exactly that file and interpolates to the same store path as `./secrets + "/x.age"`, yet `builtins.isPath` is `false` on it, so the assertion rejects it. - **Keep refusing the leak** — the directory form `"${dir}/x.age"` must still fail, and its sabotage witness must still fail with it. - **Decide the collateral question, not just the predicate** — the only value-level test that admits `builtins.path` also admits `"${./dir/x.age}"`, which the current comment refuses on purpose. That trade is the real decision here, and it may be resolved by changing nothing but the message. ### Current state `flake.nix:798-801` filters `tokenFile` and `httpsTokenFile` with `!(file == null || builtins.isPath file)`, and the message at `:803-808` explains the ban as covering every string "whatever it interpolates". `builtins.path` returns a **string**: `builtins.typeOf` is `"string"` and `builtins.isPath` is `false`, even though the entire point of the call is that it copies the one named file and nothing more. Measured on a single file, the three spellings a deployment can reach for: | spelling | value | string context | what lands in the store | | --- | --- | --- | --- | | `builtins.path { path = ./m/f.nix; name = "f.nix"; }` | `/nix/store/2ihkflrk…-f.nix` | `[ "/nix/store/2ihkflrk…-f.nix" ]` | the one file | | `"${./m/f.nix}"` | `/nix/store/2ihkflrk…-f.nix` | `[ "/nix/store/2ihkflrk…-f.nix" ]` | the one file | | `"${./m}/f.nix"` | `/nix/store/imwcmwsb…-m/f.nix` | `[ "/nix/store/imwcmwsb…-m" ]` | the whole directory | A deployment that reached for row one precisely to keep a whole repository out of a machine's closure — the outcome allod/archetypes#21 is about — is therefore refused by the assertion written to encourage that outcome. ### The predicate that would work, and what it costs The leak is distinguishable by string context rather than by type. A safe value **equals** its sole context element; `"${dir}/x.age"` is strictly longer than its context element, because the context names the directory, not the file. So `builtins.isPath file || <file equals its single context path>` accepts rows one and two and still refuses row three, and the existing sabotage witness keeps failing. The cost is row two, which the current comment refuses deliberately on the ground that it is one keystroke from the leaking spelling. Any value-level predicate that admits row one admits row two as well: they are the same string with the same context, and Nix keeps no record of which expression produced it. This is not a matter of finding a sharper test — it is a choice between refusing a safe third construction and admitting a safe second one. If the refusal of row two is worth keeping, the alternative resolution is to leave the predicate alone and fix the message, which today says to "write `./secrets + "/agent-pr-token.age"`, not a string" without telling a reader why a store-path string that stages one file is refused anyway. Either way closes this. The part that costs a reader time is being rejected for something that is not the mistake described. ### Scope In: the predicate behind `nonPathTokenArguments` at `flake.nix:798-801`, or the message at `:803-808`, whichever way the trade is decided. Whatever lands, the directory-interpolating form stays refused and provably so. Out: allod/archetypes#21's two measured leaks — `modules/agent-hooks.nix` interpolating the policy source per file, and `modules/github-credentials.nix` writing a string into `age.secrets.<name>.file`. This assertion sees neither, as its own comment records, and nothing proposed here changes that.