allod/archetypes

Watch

Fork 0

Carve the consumed secrets files so a dev machine stops carrying the whole repo #87

Merged

vnprc merged 6 commits from agent/carve-consumed-files into master

2026-09-21 16:43:24 +01:00

allod-agent commented

2026-09-20 21:57:13 +01:00

Member

Nothing changes about who can decrypt what: the recipient graph is untouched. The four policy files land at the same paths with the same bytes and the same mode, and exactly one machine's derivation moves — privacy-1, nexus and the installer build to byte-identical derivations. On the public template the measured closure drops the source root and shrinks by 174 KiB.

What proves it: the built allod-dev system closure contained /nix/store/irdys9…-source before and does not after, and a new consumed-file-carve-out check pins the property, with fourteen sabotage and control runs showing it actually fails when the carve regresses.

If it is wrong, boot the previous NixOS generation or revert this PR and rebuild. No state migrates and no secret is rewritten.

Closes allod/archetypes#21

Supersedes allod/archetypes#24, which implemented the same issue in July from a base 86 commits behind current master. This carries its carves and its retention sweep, and closes the two findings its own review pass left open: the check now iterates every composed dev machine against that machine's effective gitPolicySource rather than assuming allod-dev and the default source, and it drives a composed machine through the real consumer resolution instead of only a hand-passed fixture consumer.

What changed

modules/agent-hooks.nix — the four home.file policy sources go through a local policyFile helper that carves with builtins.path. Line 11's allod-tools source is deliberately untouched; it carries no ciphertext and is separate work.
modules/github-credentials.nix — age.secrets.<name>.file is carved the same way instead of "${secrets}/${consumer.secret}".
flake.nix — githubTargetMatchesAgeSecret in the outer let is the one place that decides whether a registered GitHub target is bound to the ciphertext a machine actually deploys. A carved file has no source-relative suffix left to match on, so the binding is exact equality against an independently carved path rather than the old /${consumer.secret} suffix test. It deliberately does not adopt the Forgejo matcher's basename fallback, which a same-named unrelated file would satisfy. credential-profiles now calls it.
flake.nix — the comment on mkDevVm's token-argument assertion described both of these sites as open leaks. It now records what that assertion still cannot see, and that the new check is what holds these two sites instead.
flake.nix — new check consumed-file-carve-out.

What the check witnesses

Generated values, never source spelling — a grep for "${secrets}/" would miss a renamed variable.

Every dev machine's four policy sources are carved, tested two ways: the source-agnostic property (a carved value's string context is exactly one entry, itself) and exact equality against a carve built from that machine's effective gitPolicySource, reconstructed with the same precedence machineConfigurations uses. A fork that legitimately points one machine at its own policy root is checked against its own source rather than failing.
Comparisons are on text and string context. Nix's == compares text only, and context is what the closure follows, so text alone would accept a context-stripped value that retains nothing — a dangling symlink and an agenix failure at activation after a GC.
The GitHub path, which the public template cannot exercise because it declares no targets: the module applied directly to a synthetic target with explicit non-default group and mode, a second target that omits both to witness the module's own defaults, an empty target list, and a target whose credential has no unique agenix consumer.
A composed dev machine carrying a non-empty GitHub target, built through mkDevVm against the real registry credential allod-dev-host, plus a grep of that fixture's agenix activation script for the carved store path. An evaluation passing proves nothing about activation.
A sweep over every home.file source of every home-manager user, and every age.secrets file, that each dev machine generates — failing if any still retains a source root. The four named assertions say nothing about a fifth consumer added uncarved later, which is how this leak would come back. It mirrors home-manager's own sourceStorePath rather than approximating it: a bare-root source is a leak whether or not it carries context, while a strict descendant is a leak only when context-bearing, because a context-free path is one home-manager narrows to the single file itself. Disabled entries are skipped, as home-manager skips them, since source has no default and forcing it would throw on a config home-manager accepts. Each root is compared in both of its spellings — toString names where a path was fetched, interpolation copies it to a fresh object — because a leaking consumer's text can be built on either.
Unit assertions on the check's own logic, because the fork branch no in-tree machine reaches is exactly the branch forks depend on: the source-resolution precedence (profile over profileData over the default, and a profile carrying only definition is not a source) and the retention rule against a synthetic path-valued root. Each was broken in turn and named itself.
Its own context comparison, asserted to reject a context-stripped value, so the check cannot pass because its comparison stopped being able to fail.

Risk

R3. It is a secret-handling boundary change on generated lifecycle behavior, and it moves every dev machine at once: agenix decrypts age.secrets.<name>.file during activation and home-manager places four files. A happy-path evaluation can pass while activation fails.

It is not R4: no authoritative secret, recipient graph, key or persistent state is mutated; the exposure change is mechanically inspectable in a built closure rather than a judgement about the diff; rollback is a previous generation or a revert plus rebuild; and a wrong source would have to survive exact-equality-plus-context comparison against an independently constructed expectation.

The residual risk this leaves for a human is activation on a real machine, which no check here reaches. Rebuild a disposable dev VM first, not the machine you work from — this runs at activation on every dev VM including that one.

Validation

Run one check at a time; nix flake check on this flake peaks near 7 GiB on an 8 GiB VM (allod/archetypes#31).

All 19 checks build green, individually, on the final commit.
Closure, the central witness: before, allod-dev's realised toplevel had 867 requisites including /nix/store/irdys9zflw7f86pmhbwy281m8q8rkmsk-source; after, 870 requisites with the root absent and the four carved files present. Exactly one closure path had referenced the root — home-manager-files.
The four carved files are byte-identical to their sources, mode 444 on both sides, and the generated home-manager tree is identical in structure with only the four link targets moved.
Derivation identity: privacy-1, nexus and installer evaluate to the same .drv as master; only allod-dev moves. Closure size 2678.79 → 2678.62 MiB. The third commit, the sweep, is check-only: allod-dev's derivation is unchanged across it.
Evaluation cost of the new check: 3.9s wall, 713 MiB peak. It is the second most expensive check in the flake, next to ssh-settings at 4.6s and 710 MiB; dev-forge-opt-out is 1.5s and 390 MiB. The sweep is what costs it — it forces every home.file and age.secrets entry of every dev machine. Well clear of the 7 GiB ceiling that makes nix flake check unusable here.
Sabotage runs, all executed, each failing and each cleanly restored:

sabotage	result
un-carve one policy source	fails: `policy source mismatch: .config/git/protected-branches on allod-dev`
un-carve the GitHub ciphertext	fails on the synthetic target's file/path/owner/group/mode
delete the module's `group` default	fails (`attribute 'group' missing`) where it previously passed
delete the module's `mode` default	fails (`attribute 'mode' missing`)
strip string context from the carve	fails on all four policy files, text-identical but retaining nothing
add a fifth `home.file` consumer naming the bare root	fails: `home.file source retains a source root: .cache/secrets-root on allod-dev`
add an `age.secrets` entry with the uncarved string spelling	fails: `age.secrets file retains a source root`
a second home-manager user with `home.file."secrets-root".source = "${secrets}"`	fails, naming the user as well as the target
a consumer spelled the original way, `"${gitPolicySource}/git/protected-branches"`	fails under both the default input and a fork override
control: `home.file."ciphertext-copy".source = identity.agentTokenFile`	passes under both inputs — home-manager narrows that path to `/nix/store/s6q5hi8s…-agent-pr-token.age`, so it is not a leak
control: `home.file."unused".enable = false` with no source	passes rather than throwing, as home-manager itself accepts it
a context-free path naming a directory in the root — reachable only under a fork, where `gitPolicySource` is a path	fails with the directory gate, passes without it
invert `gitPolicySourceFrom`'s precedence	fails: `unit assertion failed: profile wins over profileData`
drop the interpolated spelling from `rootTexts`	fails: `unit assertion failed: a child spelled "${root}/x" matches`

The fork-safety fix is the one property a sabotage run cannot reach, so it was witnessed with a substituted input instead: a profiles input carrying profileData.allod-dev.gitPolicySource = ./fork-policy, a policy root with different bytes, run as nix build --override-input profiles path:<fork> .#checks.x86_64-linux.consumed-file-carve-out.

run	result
fork override, final tree	passes; the machine's policy file resolves to `/nix/store/3vfd7pcd…-protected-branches`, carved from the fork's own root, contents `fork-only-protected-branches`
fork override, one policy source un-carved	fails: `policy source mismatch: .config/git/protected-branches on allod-dev`
fork override, on `beec6d5` before the fork-safety fix	fails on all four files — the spurious failure the review predicted

The third row is what keeps the first from being vacuous: the same input fails before the fix and passes after.

Known rough edge: the two default-deletion sabotages fail with a bare missing-attribute error rather than the check's own message. They fail closed and loudly, which is the property that matters; the message is worth sharpening if anyone trips it.

Not run: activation on a real machine, which is the human gate above.

Review

Two cold cross-family passes, on code neither reviewer wrote, plus a fix round after each.

Pass one (gpt-5.6-sol, on the first commit) found three defects, all verified against the source before being acted on: text equality ignoring string context; the synthetic metadata assertion passing vacuously through or defaults on group and mode; and the policy assertion rejecting a fork that legitimately overrides gitPolicySource. Two more were added in the same round — the mismatch message did not name the machine, and nothing witnessed a composed machine or its activation script.

Pass two (gpt-6-astra at ultra effort, on the final tree, which pass one never saw) found five more, all verified, four of them in the retention sweep — the newest code and the part no cold reader had read:

the sweep read only the dev identity's home-manager user, so a second user's files were invisible;
source == root is permanently false when the root is a path or attrset rather than a string, which killed the bare-root half of the retention test (measured: "${./modules}" == ./modules is false);
toString was the wrong coercion for home.file sources, so a context-free Nix path that home-manager narrows correctly was reported as a leak — a config home-manager accepts, failing the check;
home.file."x".enable = false with no source is valid, and home-manager filters on enable before touching source, but the sweep forced every entry's and threw;
the context self-test read a file from the secrets input that a fork may not have.

Pass three (deepseek-v4, on the final tree) confirmed pass two's five fixes independently, and walked the source-resolution duplication against the real merge at flake.nix:612-661 line by line without finding a shape where the two disagree. It left two residuals. The first is that the fork-shaped logic was witnessed only outside the tree, by a substituted profiles input that is not in the repository — so a future change drifting the duplication would go green here and fail only on a fork. That is what the unit assertions above now cover. The second it reported as age.secrets.x.file = secrets slipping through, which measurement contradicts — "${secrets}" equals secretsSource exactly, so equality already caught it — but one step over there was a real hole in both sweeps: a context-free path naming a directory, which home-manager and agenix carve wholesale. builtins.readFileType now gates it, and applying that rule to both sweeps removed the last reason they used different coercions, so they are one helper.

One finding arrived between rounds and was settled by running it rather than by another reading, as risk.md prescribes: normalising the root with toString alone catches a bare-root consumer but misses a child spelled the original uncarved way, because that child's text is built on the interpolated copy of the root rather than on its fetch location. It reproduces only under a fork, since the two spellings coincide by default. Both spellings are now checked, and the table above carries the run.

A fourth reader (kimi-k3) produced no review at all: the provider refused the request with insufficient_balance, a billing refusal rather than a verdict, so it is not counted as a pass.
Worth stating plainly: every defect found in this change has been in the check, not in the carve. The two module edits have gone unchallenged since the first commit. What kept being wrong was the thing meant to prove them — which is why the sabotage and control table above is the deliverable rather than a formality.

One witness in this arc was invalid and is worth recording, because it is the failure mode the table exists to prevent. The directory gate was first witnessed with home.file."x".source = gitPolicySource + "/git" under the default input — but gitPolicySource defaults to the secrets flake input, an attrset, and attrset-plus-string coerces to a string with context, so that run only re-proved the context-bearing case the sweep already caught. It fails identically with and without the gate. The isolating witness needs gitPolicySource to be a path, which happens only under a fork: path-plus-string yields a path, context-free, naming a directory. Under the fork override that shape passes on 19d6266 and fails on 81ca50b, which is the gate doing the work.

A dev VM no longer carries a copy of the deployment's whole secrets repository. Until now every dev machine's system closure contained the secrets flake's source directory — every other machine's encrypted SSH host keys and Forge keys included — because four git-policy files and the GitHub credential were named by interpolating the input root. Each is now carved out as its own single-file store path, so a machine holds the files it uses and nothing else. Nothing changes about who can decrypt what: the recipient graph is untouched. The four policy files land at the same paths with the same bytes and the same mode, and exactly one machine's derivation moves — privacy-1, nexus and the installer build to byte-identical derivations. On the public template the measured closure drops the source root and shrinks by 174 KiB. What proves it: the built `allod-dev` system closure contained `/nix/store/irdys9…-source` before and does not after, and a new `consumed-file-carve-out` check pins the property, with fourteen sabotage and control runs showing it actually fails when the carve regresses. If it is wrong, boot the previous NixOS generation or revert this PR and rebuild. No state migrates and no secret is rewritten. Closes allod/archetypes#21 Supersedes allod/archetypes#24, which implemented the same issue in July from a base 86 commits behind current master. This carries its carves and its retention sweep, and closes the two findings its own review pass left open: the check now iterates every composed dev machine against that machine's effective `gitPolicySource` rather than assuming `allod-dev` and the default source, and it drives a composed machine through the real consumer resolution instead of only a hand-passed fixture consumer. ## What changed - `modules/agent-hooks.nix` — the four `home.file` policy sources go through a local `policyFile` helper that carves with `builtins.path`. Line 11's `allod-tools` source is deliberately untouched; it carries no ciphertext and is separate work. - `modules/github-credentials.nix` — `age.secrets.<name>.file` is carved the same way instead of `"${secrets}/${consumer.secret}"`. - `flake.nix` — `githubTargetMatchesAgeSecret` in the outer `let` is the one place that decides whether a registered GitHub target is bound to the ciphertext a machine actually deploys. A carved file has no source-relative suffix left to match on, so the binding is exact equality against an independently carved path rather than the old `/${consumer.secret}` suffix test. It deliberately does not adopt the Forgejo matcher's basename fallback, which a same-named unrelated file would satisfy. `credential-profiles` now calls it. - `flake.nix` — the comment on `mkDevVm`'s token-argument assertion described both of these sites as open leaks. It now records what that assertion still cannot see, and that the new check is what holds these two sites instead. - `flake.nix` — new check `consumed-file-carve-out`. ### What the check witnesses Generated values, never source spelling — a grep for `"${secrets}/"` would miss a renamed variable. - Every dev machine's four policy sources are carved, tested two ways: the source-agnostic property (a carved value's string context is exactly one entry, itself) and exact equality against a carve built from that machine's **effective** `gitPolicySource`, reconstructed with the same precedence `machineConfigurations` uses. A fork that legitimately points one machine at its own policy root is checked against its own source rather than failing. - Comparisons are on text **and** string context. Nix's `==` compares text only, and context is what the closure follows, so text alone would accept a context-stripped value that retains nothing — a dangling symlink and an agenix failure at activation after a GC. - The GitHub path, which the public template cannot exercise because it declares no targets: the module applied directly to a synthetic target with explicit non-default `group` and `mode`, a second target that omits both to witness the module's own defaults, an empty target list, and a target whose credential has no unique agenix consumer. - A **composed** dev machine carrying a non-empty GitHub target, built through `mkDevVm` against the real registry credential `allod-dev-host`, plus a grep of that fixture's agenix activation script for the carved store path. An evaluation passing proves nothing about activation. - A sweep over **every** `home.file` source of **every** home-manager user, and every `age.secrets` file, that each dev machine generates — failing if any still retains a source root. The four named assertions say nothing about a fifth consumer added uncarved later, which is how this leak would come back. It mirrors home-manager's own `sourceStorePath` rather than approximating it: a bare-root source is a leak whether or not it carries context, while a strict descendant is a leak only when context-bearing, because a context-free path is one home-manager narrows to the single file itself. Disabled entries are skipped, as home-manager skips them, since `source` has no default and forcing it would throw on a config home-manager accepts. Each root is compared in both of its spellings — `toString` names where a path was fetched, interpolation copies it to a fresh object — because a leaking consumer's text can be built on either. - Unit assertions on the check's own logic, because the fork branch no in-tree machine reaches is exactly the branch forks depend on: the source-resolution precedence (`profile` over `profileData` over the default, and a `profile` carrying only `definition` is not a source) and the retention rule against a synthetic path-valued root. Each was broken in turn and named itself. - Its own context comparison, asserted to reject a context-stripped value, so the check cannot pass because its comparison stopped being able to fail. ## Risk **R3.** It is a secret-handling boundary change on generated lifecycle behavior, and it moves every dev machine at once: agenix decrypts `age.secrets.<name>.file` during activation and home-manager places four files. A happy-path evaluation can pass while activation fails. It is not R4: no authoritative secret, recipient graph, key or persistent state is mutated; the exposure change is mechanically inspectable in a built closure rather than a judgement about the diff; rollback is a previous generation or a revert plus rebuild; and a wrong source would have to survive exact-equality-plus-context comparison against an independently constructed expectation. The residual risk this leaves for a human is activation on a real machine, which no check here reaches. Rebuild a disposable dev VM first, not the machine you work from — this runs at activation on every dev VM including that one. ## Validation Run one check at a time; `nix flake check` on this flake peaks near 7 GiB on an 8 GiB VM (allod/archetypes#31). - All 19 checks build green, individually, on the final commit. - Closure, the central witness: before, `allod-dev`'s realised toplevel had 867 requisites including `/nix/store/irdys9zflw7f86pmhbwy281m8q8rkmsk-source`; after, 870 requisites with the root absent and the four carved files present. Exactly one closure path had referenced the root — `home-manager-files`. - The four carved files are byte-identical to their sources, mode 444 on both sides, and the generated home-manager tree is identical in structure with only the four link targets moved. - Derivation identity: `privacy-1`, `nexus` and `installer` evaluate to the same `.drv` as master; only `allod-dev` moves. Closure size 2678.79 → 2678.62 MiB. The third commit, the sweep, is check-only: `allod-dev`'s derivation is unchanged across it. - Evaluation cost of the new check: 3.9s wall, 713 MiB peak. It is the second most expensive check in the flake, next to `ssh-settings` at 4.6s and 710 MiB; `dev-forge-opt-out` is 1.5s and 390 MiB. The sweep is what costs it — it forces every `home.file` and `age.secrets` entry of every dev machine. Well clear of the 7 GiB ceiling that makes `nix flake check` unusable here. - Sabotage runs, all executed, each failing and each cleanly restored: | sabotage | result | | --- | --- | | un-carve one policy source | fails: `policy source mismatch: .config/git/protected-branches on allod-dev` | | un-carve the GitHub ciphertext | fails on the synthetic target's file/path/owner/group/mode | | delete the module's `group` default | fails (`attribute 'group' missing`) where it previously passed | | delete the module's `mode` default | fails (`attribute 'mode' missing`) | | strip string context from the carve | fails on all four policy files, text-identical but retaining nothing | | add a fifth `home.file` consumer naming the bare root | fails: `home.file source retains a source root: .cache/secrets-root on allod-dev` | | add an `age.secrets` entry with the uncarved string spelling | fails: `age.secrets file retains a source root` | | a second home-manager user with `home.file."secrets-root".source = "${secrets}"` | fails, naming the user as well as the target | | a consumer spelled the original way, `"${gitPolicySource}/git/protected-branches"` | fails under both the default input and a fork override | | control: `home.file."ciphertext-copy".source = identity.agentTokenFile` | passes under both inputs — home-manager narrows that path to `/nix/store/s6q5hi8s…-agent-pr-token.age`, so it is not a leak | | control: `home.file."unused".enable = false` with no source | passes rather than throwing, as home-manager itself accepts it | | a context-free path naming a directory in the root — reachable only under a fork, where `gitPolicySource` is a path | fails with the directory gate, passes without it | | invert `gitPolicySourceFrom`'s precedence | fails: `unit assertion failed: profile wins over profileData` | | drop the interpolated spelling from `rootTexts` | fails: `unit assertion failed: a child spelled "${root}/x" matches` | The fork-safety fix is the one property a sabotage run cannot reach, so it was witnessed with a substituted input instead: a `profiles` input carrying `profileData.allod-dev.gitPolicySource = ./fork-policy`, a policy root with different bytes, run as `nix build --override-input profiles path:<fork> .#checks.x86_64-linux.consumed-file-carve-out`. | run | result | | --- | --- | | fork override, final tree | passes; the machine's policy file resolves to `/nix/store/3vfd7pcd…-protected-branches`, carved from the fork's own root, contents `fork-only-protected-branches` | | fork override, one policy source un-carved | fails: `policy source mismatch: .config/git/protected-branches on allod-dev` | | fork override, on `beec6d5` before the fork-safety fix | fails on all four files — the spurious failure the review predicted | The third row is what keeps the first from being vacuous: the same input fails before the fix and passes after. Known rough edge: the two default-deletion sabotages fail with a bare missing-attribute error rather than the check's own message. They fail closed and loudly, which is the property that matters; the message is worth sharpening if anyone trips it. Not run: activation on a real machine, which is the human gate above. ## Review Two cold cross-family passes, on code neither reviewer wrote, plus a fix round after each. **Pass one** (`gpt-5.6-sol`, on the first commit) found three defects, all verified against the source before being acted on: text equality ignoring string context; the synthetic metadata assertion passing vacuously through `or` defaults on `group` and `mode`; and the policy assertion rejecting a fork that legitimately overrides `gitPolicySource`. Two more were added in the same round — the mismatch message did not name the machine, and nothing witnessed a composed machine or its activation script. **Pass two** (`gpt-6-astra` at ultra effort, on the final tree, which pass one never saw) found five more, all verified, four of them in the retention sweep — the newest code and the part no cold reader had read: - the sweep read only the dev identity's home-manager user, so a second user's files were invisible; - `source == root` is permanently false when the root is a path or attrset rather than a string, which killed the bare-root half of the retention test (measured: `"${./modules}" == ./modules` is `false`); - `toString` was the wrong coercion for `home.file` sources, so a context-free Nix path that home-manager narrows correctly was reported as a leak — a config home-manager accepts, failing the check; - `home.file."x".enable = false` with no source is valid, and home-manager filters on `enable` before touching `source`, but the sweep forced every entry's and threw; - the context self-test read a file from the secrets input that a fork may not have. **Pass three** (`deepseek-v4`, on the final tree) confirmed pass two's five fixes independently, and walked the source-resolution duplication against the real merge at `flake.nix:612-661` line by line without finding a shape where the two disagree. It left two residuals. The first is that the fork-shaped logic was witnessed only outside the tree, by a substituted `profiles` input that is not in the repository — so a future change drifting the duplication would go green here and fail only on a fork. That is what the unit assertions above now cover. The second it reported as `age.secrets.x.file = secrets` slipping through, which measurement contradicts — `"${secrets}"` equals `secretsSource` exactly, so equality already caught it — but one step over there was a real hole in both sweeps: a context-free path naming a *directory*, which home-manager and agenix carve wholesale. `builtins.readFileType` now gates it, and applying that rule to both sweeps removed the last reason they used different coercions, so they are one helper. One finding arrived between rounds and was settled by running it rather than by another reading, as `risk.md` prescribes: normalising the root with `toString` alone catches a bare-root consumer but misses a child spelled the original uncarved way, because that child's text is built on the interpolated copy of the root rather than on its fetch location. It reproduces only under a fork, since the two spellings coincide by default. Both spellings are now checked, and the table above carries the run. A fourth reader (`kimi-k3`) produced no review at all: the provider refused the request with `insufficient_balance`, a billing refusal rather than a verdict, so it is not counted as a pass. Worth stating plainly: every defect found in this change has been in the check, not in the carve. The two module edits have gone unchallenged since the first commit. What kept being wrong was the thing meant to prove them — which is why the sabotage and control table above is the deliverable rather than a formality. One witness in this arc was invalid and is worth recording, because it is the failure mode the table exists to prevent. The directory gate was first witnessed with `home.file."x".source = gitPolicySource + "/git"` under the default input — but `gitPolicySource` defaults to the `secrets` flake input, an attrset, and attrset-plus-string coerces to a **string with context**, so that run only re-proved the context-bearing case the sweep already caught. It fails identically with and without the gate. The isolating witness needs `gitPolicySource` to be a *path*, which happens only under a fork: path-plus-string yields a path, context-free, naming a directory. Under the fork override that shape passes on `19d6266` and fails on `81ca50b`, which is the gate doing the work.

allod-agent added 3 commits

2026-09-20 21:57:13 +01:00

Carve the four git-policy files and the GitHub credential ciphertext beec6d5d2a

modules/agent-hooks.nix and modules/github-credentials.nix each put a
whole secrets flake input into a dev VM's closure: the former by
interpolating gitPolicySource and appending /git/<name> per policy
file, the latter by writing "${secrets}/${consumer.secret}" straight
into age.secrets.<name>.file. Because a flake input resolves to a
directory, both leak every ciphertext the secrets repo holds into
every dev VM, not just the one file each site actually uses.

Both now carve a single-file store path with builtins.path, so the
generated value names only the file consumed. The GitHub target
matcher in credential-profiles matched on a path suffix, which a
carved path (/nix/store/<hash>-<basename>.age) does not have; it is
replaced with exact equality against an independently constructed
carved path, lifted into a shared predicate,
githubTargetMatchesAgeSecret, in the flake's outer let so both the
real check and a synthetic fixture can call it. The mkDevVm comment
that recorded both leaks as measured and open is updated to say what
still holds them: a new check, not that assertion.

checks.<system>.consumed-file-carve-out pins the property: every dev
machine's four policy sources equal their carved expectation, and,
since the public template declares no GitHub targets, a synthetic
non-empty target proves the GitHub path with sabotage witnesses for a
same-basename different-content file, an empty target list, and a
credential with no unique agenix consumer.

Refs allod/archetypes#21

Fix round: pin string context, real defaults, and a fork's own source ae13624e90

Fixes five defects found reading the carve-out change cold.

Text equality alone does not pin what lands in the closure: Nix string
equality ignores context, so a context-stripped value (nothing left to
decrypt) or a context-inflated one (the right pathname plus the whole
secrets root riding along) can both match on text. sameCarvedValue, in
the flake's outer let, compares text and builtins.getContext together,
and githubTargetMatchesAgeSecret and the new check's comparisons now
go through it. A cheap witness proves the helper can actually fail on
context alone.

The synthetic GitHub target omitted group and mode, and the
assertions read them back through `or "users"` / `or "0600"`, so
deleting those two defaults from the module left the check green. The
synthetic and composed targets now carry explicit, non-default
group/mode and are asserted with plain equality; a second synthetic
target that omits both still witnesses the module's own defaults.

The policy assertion compared every dev machine against this repo's
own secretsSource, which fails a fork whose profile or profileData
legitimately overrides gitPolicySource (the fork-safety class of
allod/archetypes#36). It now asserts the source-agnostic property
directly — a carved value's context is exactly one entry, itself —
and, for the exact comparison, reconstructs the effective source with
the same profileSettings-over-profileData-over-default merge order
machineConfigurations uses.

The policy mismatch message now names the machine after the target,
keeping the grep prefix an external sabotage test depends on
byte-identical.

A new fixture calls mkDevVm directly with a non-empty GitHub target
(allod-dev-host, a template credential with one agenix consumer) to
witness a composed machine and its own agenix activation script
installing the carved path, not only the module applied in isolation.

Refs allod/archetypes#21

Add a retention sweep to the carve-out check b91c31bad7

Ported from an older open PR for the same issue (allod/archetypes#24,
agent/consumed-file-carve-out), whose own review found the hole: the
four named policy-file assertions say nothing about a fifth home.file
consumer added uncarved later. That PR's reviewer demonstrated it with
home.file.".cache/secrets-root".source = gitPolicySource, which left
every named assertion green while the machine carried the whole
secrets repository.

homeFileRetentionErrors sweeps every home.file entry a dev machine
actually generates, for every dev machine rather than only allod-dev,
against both roots a consumer could retain: the machine's own
effective policy source and the secrets input root. Retention is
equality with the root or a path inside it, so a consumer set to the
bare root with no appended child is caught too, not only its
children. toString is right here, per the ported comment: a home.file
source is always a store path already or a literal path inside this
flake, never the pre-coercion child-of-source-root spelling an
age.secrets token path has.

ageSecretRetentionErrors extends the sweep to config.age.secrets,
which the older PR did not cover. toString would be wrong there: a
token file such as identity.agentTokenFile is a genuine Nix path, and
toString on it legitimately renders the pre-coercion in-source-root
text without copying it — indistinguishable by text from a real leak.
Interpolating instead ("${secret.file}"), the way agenix itself
consumes a path argument, copies the single file to its own store
object first, so the result is correct for both the real token
secrets and a regression in the second module.

Refs allod/archetypes#21

allod-agent referenced this pull request

2026-09-20 21:57:28 +01:00

Carve consumed secrets files out of the input root #24

allod-agent referenced this pull request

2026-09-20 21:58:06 +01:00

Carve out consumed files so a dev machine stops carrying the whole secrets repo #21

allod-agent added 2 commits

2026-09-20 22:48:23 +01:00

Second fix round: every user, a real string root, home-manager's own rule 49aba73f46

Fixes five defects a second review pass found in the retention sweep.

The sweep read only the dev identity's home-manager user
(config.home-manager.users.${username}), so a second user added by any
module in a machine's list — home-manager.users.root, say — was
invisible to it. It now sweeps every user in config.home-manager.users
and names the user in the message alongside the target and machine.
The four named policy assertions stay keyed to the dev identity's
username, since those are about specific files that specific user
gets.

retainsRoot compared a `source` string against `root` with a bare `==`,
but effectiveGitPolicySource can be a fork's own path- or
attrset-valued override, and `==` between a string and a path is false
regardless of text. Normalising with `toString`, not interpolation,
makes the comparison work for both: interpolating a raw path copies it
to a fresh, differently-hashed store object, so comparing that against
a `source` that was only `toString`'d would never match even the exact
bare-root case being guarded, while `toString` on the same path twice
yields identical text.

toString-ing a home.file source and calling any retention a leak
disagreed with what home-manager itself does (modules/files.nix's
sourceStorePath): a context-free source is one home-manager carves
fresh via builtins.path, discarding the pre-coercion text, so a Nix
path such as identity.agentTokenFile is safe despite its in-root
toString. Retention now has two rules: equality with the bare root is
flagged unconditionally (a directory-level carve of the whole root is
still the whole root's contents, not a narrowed leaf), while a strict
descendant is flagged only when context-bearing, matching home-manager's
own verbatim-vs-carve distinction.

`home.file."x".enable = false;` with no source or text is a valid
declaration — source has no default, and home-manager's own module
filters on enable before ever touching source. The sweep now does the
same, filtering disabled entries out before forcing .source.

The context self-test read a file from the secrets input's git/
directory; a fork whose machines all override gitPolicySource may have
no such directory. It now builds its sample from this repository's own
tracked flake.nix, which every fork has.

Refs allod/archetypes#21

Third fix round: check a root's two spellings, not one 19d6266db2

Fixes a residual hole in retainsRoot measured against the fork fixture:
a root has two spellings, and a leaking consumer's text can be built on
either, but the sweep only ever compared against one.

toString root names the path where it was fetched and copies nothing;
"${root}" copies it to a fresh content-addressed object. Both are real
store objects a consumer's source text can be built on: the bare-root
case (last round's fix) needs toString, because a source that was
itself only toString'd can never match an interpolated root. But a
context-bearing *child* built the original uncarved way --
"${gitPolicySource}/git/protected-branches" -- is built on the
interpolated copy, not on where gitPolicySource was fetched from, so
it needs the interpolated spelling instead. For an attrset root
(secretsSource, the default) the two spellings coincide, which is why
no witness so far caught this: it only shows up for a path-valued
root, i.e. a fork that overrides gitPolicySource.

rootTexts tries both spellings, lib.unique collapsing them back to one
for every machine that does not override the source, so nothing extra
is copied or compared there. The two retention rules and the
hasContext gate on the descendant case are unchanged.

Refs allod/archetypes#21

allod-agent added 1 commit

2026-09-20 23:19:43 +01:00

Fourth fix round: witness the fork logic in-tree, close the directory case 81ca50ba13

Fixes two residuals a third review pass found.

Every dev machine in this repository takes effectiveGitPolicySource's
default branch and retainsRoot's own root is always an attrset
(secretsSource), so neither the profile/profileData override layers
nor rootTexts' path-valued-root branch was reachable from anything in
the tree — both were witnessed only through a substituted profiles
input that lives outside the repository. A future change that drifts
the merge duplication or breaks rootTexts would go green here and fail
only on a fork, silently.

effectiveGitPolicySource is now a thin wrapper around
gitPolicySourceFrom, a pure function over { profile; profileData;
default }, with unit assertions pinning its precedence contract
against synthetic data: profile wins over profileData, profileData
wins over the default, the default applies when neither sets it, and
a profile carrying only "definition" does not count as a source.
retainsRoot gets the same treatment with a synthetic path-valued root
(a path in this repository), pinning that a bare-root source matches,
a child spelled "${root}/x" matches, and a context-free regular file
inside the root does not. Both assertion sets carry their own message
prefix, distinct from the sweep's.

The second: a context-free path is not automatically safe just because
home-manager/agenix will carve it — carving a directory copies
everything under it, the exact leak this change removes, one level
down. `readFileType` (guarded by `pathExists`, so a descendant that
does not exist is ignored rather than throwing) now gates the
context-free case on regular-file-vs-directory rather than treating
every context-free descendant as safe. Applying the same rule to
age.secrets as home.file removed the only reason those two sweeps used
different coercions, so the shared step — toString, then check every
root — is now one helper, sourceRetainsAnyRoot, instead of two copies
that had to be kept in step.

Refs allod/archetypes#21