allod/archetypes

Watch

Fork 0

Carve consumed secrets files out of the input root #24

Open

allod-agent wants to merge 3 commits from agent/consumed-file-carve-out into master

allod-agent commented

2026-07-31 06:04:52 +01:00

Member

Five consumer sites change. modules/agent-hooks.nix carves the four git policy files it selects from gitPolicySource, and modules/github-credentials.nix carves the ciphertext it selects from the secrets input. Each becomes builtins.path { path = <existing interpolated path>; name = <basename>; }, which yields a content-addressed store path holding the single file with no reference back to the source directory. Nothing else moves: the recipient graph, the allod-tools input, the token files that already resolve to individual store paths (./secrets + "/<name>.age" is a Nix path, so agenix's own coercion already copies the single file), and the check derivations that deliberately inspect the repo are all untouched.

One matcher changes. githubTargetMatchesGeneratedAgeSecret accepted a generated secret by an in-root /<source-relative-path> suffix, which a carved file no longer has, so following the issue literally would have broken it the moment a deployment composed non-empty GitHub target data. It now constructs the expected carved source independently and requires exact equality. It deliberately does not copy the Forgejo matcher's basename-suffix fallback: a suffix proves only the label, so an unrelated carved file with the same basename would pass. The comparison is lifted into a shared predicate so the new check can drive the same code path with synthetic data.

One check is added. consumed-file-carve-out pins generated values rather than source spelling — the four home.file sources a real machine produces, a sweep that fails if any home.file source still names a child of the input root, and the exact file, destination, owner, group and mode a GitHub credential target produces. It needs a synthetic fixture because the public secrets template declares no GitHub targets, which is why credential-profiles passing is not evidence for that matcher.

Risk

R3 High, as assessed in the plan.

The blast radius is every dev machine at once: each carve moves age.secrets.<name>.file or a home.file.<name>.source, so every dev machine's derivation changes. Privacy VMs and the hypervisor are unaffected — the modules in scope are imported only from mkDevVm. It is a secret-handling boundary change that alters activation-time behavior, so a happy-path evaluation can pass while activation fails. A wrong builtins.path source could in principle put an unintended ciphertext in a machine closure while the source root is absent, which the closure test alone cannot catch; that is why exact-source equality and the same-basename wrong-content mutation are part of the proof rather than optional extras.

What holds it at R3 rather than R4: no authoritative secret, recipient graph, key or persistent datum is mutated; the exact-source and generated-metadata checks are agent-runnable; the built output closure is mechanically inspectable; rollout starts on a disposable VM; and rollback is a previous NixOS generation, or a pin revert plus rebuild, with no state to migrate.

Validation

Acceptance tests 1 through 7 from the plan were run verbatim from the candidate checkout against allod/deploy as the composition root. All seven passed.

Test 1 (baseline tripwire) passed. The pre-change allod-dev toplevel closure does contain the secrets source root, so the premise holds and test 2 is not vacuous.
Test 2 (candidate closure) passed. The candidate allod-dev toplevel has 869 requisites and the secrets source root is absent. The four carved policy files and the two token ciphertexts are present as store-root objects, so the machine still gets what it consumes. The only -source roots left in the closure are allod-tools, explicitly out of scope, and nixpkgs.
Test 3 (new check) passed, and test 5 (sabotage) passed: un-carving one policy source in place makes the check fail naming consumed-file-carve-out: policy source mismatch: .config/git/protected-branches, and the implementation survives the restore.
Test 4 passed: credential-profiles and dev-forge-opt-out still build. Note that credential-profiles is not evidence for the GitHub matcher here — the public template's target list is empty, so that branch is vacuous and test 3 supplies the only non-empty exercise.
Test 6 passed. Both of allod-dev's generated age secret files coerce, by interpolation rather than toString, to store-root regular files.
Test 7 passed. All four composed configurations still evaluate to a toplevel derivation path, one process each.
All ten archetypes checks build green.

Six further sabotage probes were run beyond the plan's test 5, because a check that has only been seen to pass is not yet known to be able to fail. Each was reverted from a mode-preserving scratch copy. Un-carving the GitHub consumer, weakening the matcher back to a basename suffix so that it accepts the same-basename wrong-content mutation, pointing the generated secret at a wrong destination, adding a fifth uncarved home.file policy consumer, neutering the module's invalid-consumer assertion, and making that assertion stop naming the credential each make the check fail on the specific assertion that guards them.

Test 8 did not run and cannot be simulated. It is the human generated-lifecycle gate: advance the private deploy pin, rebuild a disposable dev VM that has a real GitHub target, confirm agenix decrypts the declared credential to the unchanged destination and home-manager installs all four policy files, reboot once, and only then rebuild the working VM. An agent cannot rebuild or provision a machine.

Residual uncertainty this leaves:

No real activation has happened. Every result above is evaluation and build. Nothing here proves agenix decrypts a carved ciphertext at first boot, or that home-manager places the carved policy files with readable targets. That is exactly what test 8 exists for, and it is why the throwaway machine goes before any machine anyone works from.
No real GitHub credential was exercised. The public secrets template declares no GitHub targets, so the carved GitHub consumer generates nothing on any public machine. Its coverage is the synthetic fixture plus the shared predicate. A private composition must repeat test 2 for every dev machine, including each one with a real GitHub target, and test 8 is the only place a real decrypt of that credential is observed.
The new check proves equality with an independently constructed carve, not the closure property itself. If builtins.path ever stopped carving, the generated and expected sides would move together and the check would still pass. The store-root shape assertion narrows that, but the closure query in tests 1 and 2 is what actually covers it, and that query is not a flake check — it must be re-run per composed dev machine wherever this lands.
The check is keyed to allod-dev, like every other check in this flake. A dev machine that overrides gitPolicySource is covered only by the closure query, not by the generated-value assertions.
--override-input archetypes path:... is not out-path-equivalent to a git-pinned lock, so the specific out-paths recorded above are not the ones a pinned deploy will build. The closure-membership question they answer is unaffected, but a post-pin rebuild will legitimately produce different hashes.

Refs allod/strategy#27

Closes allod/archetypes#21

Every file a dev machine consumes from the secrets input is now carved out as its own single-file store object, so the machine's system closure no longer carries the whole secrets repo; implemented and validated against the public composition root, awaiting the human rebuild gate before any machine takes it. Five consumer sites change. `modules/agent-hooks.nix` carves the four git policy files it selects from `gitPolicySource`, and `modules/github-credentials.nix` carves the ciphertext it selects from the secrets input. Each becomes `builtins.path { path = <existing interpolated path>; name = <basename>; }`, which yields a content-addressed store path holding the single file with no reference back to the source directory. Nothing else moves: the recipient graph, the `allod-tools` input, the token files that already resolve to individual store paths (`./secrets + "/<name>.age"` is a Nix path, so agenix's own coercion already copies the single file), and the check derivations that deliberately inspect the repo are all untouched. One matcher changes. `githubTargetMatchesGeneratedAgeSecret` accepted a generated secret by an in-root `/<source-relative-path>` suffix, which a carved file no longer has, so following the issue literally would have broken it the moment a deployment composed non-empty GitHub target data. It now constructs the expected carved source independently and requires exact equality. It deliberately does not copy the Forgejo matcher's basename-suffix fallback: a suffix proves only the label, so an unrelated carved file with the same basename would pass. The comparison is lifted into a shared predicate so the new check can drive the same code path with synthetic data. One check is added. `consumed-file-carve-out` pins generated values rather than source spelling — the four `home.file` sources a real machine produces, a sweep that fails if any `home.file` source still names a child of the input root, and the exact file, destination, owner, group and mode a GitHub credential target produces. It needs a synthetic fixture because the public secrets template declares no GitHub targets, which is why `credential-profiles` passing is not evidence for that matcher. ## Risk R3 High, as assessed in the plan. The blast radius is every dev machine at once: each carve moves `age.secrets.<name>.file` or a `home.file.<name>.source`, so every dev machine's derivation changes. Privacy VMs and the hypervisor are unaffected — the modules in scope are imported only from `mkDevVm`. It is a secret-handling boundary change that alters activation-time behavior, so a happy-path evaluation can pass while activation fails. A wrong `builtins.path` source could in principle put an unintended ciphertext in a machine closure while the source root is absent, which the closure test alone cannot catch; that is why exact-source equality and the same-basename wrong-content mutation are part of the proof rather than optional extras. What holds it at R3 rather than R4: no authoritative secret, recipient graph, key or persistent datum is mutated; the exact-source and generated-metadata checks are agent-runnable; the built output closure is mechanically inspectable; rollout starts on a disposable VM; and rollback is a previous NixOS generation, or a pin revert plus rebuild, with no state to migrate. ## Validation Acceptance tests 1 through 7 from the plan were run verbatim from the candidate checkout against `allod/deploy` as the composition root. All seven passed. - Test 1 (baseline tripwire) passed. The pre-change `allod-dev` toplevel closure does contain the secrets source root, so the premise holds and test 2 is not vacuous. - Test 2 (candidate closure) passed. The candidate `allod-dev` toplevel has 869 requisites and the secrets source root is absent. The four carved policy files and the two token ciphertexts are present as store-root objects, so the machine still gets what it consumes. The only `-source` roots left in the closure are `allod-tools`, explicitly out of scope, and nixpkgs. - Test 3 (new check) passed, and test 5 (sabotage) passed: un-carving one policy source in place makes the check fail naming `consumed-file-carve-out: policy source mismatch: .config/git/protected-branches`, and the implementation survives the restore. - Test 4 passed: `credential-profiles` and `dev-forge-opt-out` still build. Note that `credential-profiles` is not evidence for the GitHub matcher here — the public template's target list is empty, so that branch is vacuous and test 3 supplies the only non-empty exercise. - Test 6 passed. Both of `allod-dev`'s generated age secret files coerce, by interpolation rather than `toString`, to store-root regular files. - Test 7 passed. All four composed configurations still evaluate to a toplevel derivation path, one process each. - All ten `archetypes` checks build green. Six further sabotage probes were run beyond the plan's test 5, because a check that has only been seen to pass is not yet known to be able to fail. Each was reverted from a mode-preserving scratch copy. Un-carving the GitHub consumer, weakening the matcher back to a basename suffix so that it accepts the same-basename wrong-content mutation, pointing the generated secret at a wrong destination, adding a fifth uncarved `home.file` policy consumer, neutering the module's invalid-consumer assertion, and making that assertion stop naming the credential each make the check fail on the specific assertion that guards them. Test 8 did not run and cannot be simulated. It is the human generated-lifecycle gate: advance the private deploy pin, rebuild a disposable dev VM that has a real GitHub target, confirm agenix decrypts the declared credential to the unchanged destination and home-manager installs all four policy files, reboot once, and only then rebuild the working VM. An agent cannot rebuild or provision a machine. Residual uncertainty this leaves: - No real activation has happened. Every result above is evaluation and build. Nothing here proves agenix decrypts a carved ciphertext at first boot, or that home-manager places the carved policy files with readable targets. That is exactly what test 8 exists for, and it is why the throwaway machine goes before any machine anyone works from. - No real GitHub credential was exercised. The public secrets template declares no GitHub targets, so the carved GitHub consumer generates nothing on any public machine. Its coverage is the synthetic fixture plus the shared predicate. A private composition must repeat test 2 for every dev machine, including each one with a real GitHub target, and test 8 is the only place a real decrypt of that credential is observed. - The new check proves equality with an independently constructed carve, not the closure property itself. If `builtins.path` ever stopped carving, the generated and expected sides would move together and the check would still pass. The store-root shape assertion narrows that, but the closure query in tests 1 and 2 is what actually covers it, and that query is not a flake check — it must be re-run per composed dev machine wherever this lands. - The check is keyed to `allod-dev`, like every other check in this flake. A dev machine that overrides `gitPolicySource` is covered only by the closure query, not by the generated-value assertions. - `--override-input archetypes path:...` is not out-path-equivalent to a git-pinned lock, so the specific out-paths recorded above are not the ones a pinned deploy will build. The closure-membership question they answer is unaffected, but a post-pin rebuild will legitimately produce different hashes. Refs allod/strategy#27 Closes allod/archetypes#21

allod-agent added 1 commit

2026-07-31 06:04:53 +01:00

Carve consumed secrets files out of the input root ee872aa468

A dev machine's system closure held the whole secrets input, because the four
git policy consumers and the GitHub credential consumer interpolated the input
and appended a child name, so the derivation depended on the directory and
every ciphertext in it. Each of those consumers now carves its file with
builtins.path, yielding a single-file content-addressed store object with no
reference back to the source directory.

The GitHub matcher in credential-profiles accepted a generated secret by an
in-root path suffix, which a carved file no longer has. It now builds the
expected carved source independently and requires exact equality; a basename
suffix would prove only the label, so an unrelated carved file with the same
basename would pass. That comparison is lifted into a shared predicate so the
new check can drive it with synthetic non-empty target data, which matters
because the public secrets template declares no GitHub targets and the real
matcher is therefore vacuous here.

The new consumed-file-carve-out check pins generated values rather than source
spelling: the four home.file sources a real machine produces, a sweep that
fails if any home.file source still names a child of the input root, and the
exact file, destination, owner, group and mode a GitHub target produces. Its
negative fixtures cover a same-basename wrong-content carve, an uncarved
in-root path, wrong destination, owner, group and mode, an empty target list,
and a target with no unique agenix consumer.

Out of scope and unchanged: the recipient graph, the allod-tools input, the
token files that already resolve to individual store paths, and the check
derivations that inspect the repo.

Refs allod/archetypes#21

Model: claude-opus-5

allod-agent commented

2026-07-31 06:26:55 +01:00

Author

Member

Adversarial read-only review pass by gpt-5.6-sol at xhigh effort, cross-vendor from the claude-opus-5 that wrote the code. Four findings, no blockers. Every one is a way the new check can stay green while the property it guards is false — none is a defect in the carves themselves, which the pass confirmed correct.

Confirmed correct and worth not undoing later: the five carves use the right source and basename; nested consumer.secret paths work; toString is valid for the current path values; two conflicting duplicate targets cannot both match; empty target lists, Forge opt-out, and invalid consumers all behave; no secrets-root child construction remains anywhere in the mkDevVm module graph; and mkPrivacyVm / mkHypervisor genuinely do not import either changed module.

1. [GAP] The root sweep misses the root itself — verified

flake.nix:976 builds secretsRootPrefix = "${toString secrets}/" with a trailing slash, so lib.hasPrefix matches children of the root but not the root itself. Adding home.file.".cache/secrets-root".source = gitPolicySource leaves all four named assertions green while the machine carries the entire secrets repository — the exact failure this check exists to prevent. Being fixed in a follow-up commit.

2. [GAP] Exact equality does not prove a closure dependency — verified

Nix string equality compares contents and ignores store context. Confirmed on 2.31.5 against a two-file fixture:

carved == builtins.unsafeDiscardStringContext (toString carved)  ->  true
context of carved    ->  ["/nix/store/<hash>-x.age"]
context of stripped  ->  []

So setting file = builtins.unsafeDiscardStringContext (toString (carvedSecretFile consumer)) passes the matcher, the equality assertion, and the store-root shape assertion, while the generated system names the correct path without retaining it as an input. The ciphertext is then not guaranteed to be in the runtime closure, and agenix can fail after transfer or after a garbage collection. The current code preserves context correctly; the check simply does not prove it does. Being fixed in a follow-up commit by asserting the carved value's context retains its own store path.

3. [GAP] Policy coverage is hardwired to `allod-dev` with the default source

flake.nix:943 keys the policy assertions to allod-dev and compares against the secrets input directly. A second dev profile that mkForces one policy home.file.source back to "${secrets}/git/..." keeps the check green while that machine retains the root. The converse also holds: a legitimate gitPolicySource override with different policy bytes is carved correctly by the module but rejected by the check against the hardcoded input.

4. [GAP] The GitHub fixture bypasses the real consumer resolution

flake.nix:1043 passes fixtureConsumer directly rather than exercising githubAgenixConsumer at flake.nix:505. Make that lookup return null or filter the wrong repository and both this check and credential-profiles stay green while every real non-empty GitHub target is rejected. The lookup is statically correct today; it is simply not proven end to end.

What is being fixed here and what is not

Findings 1 and 2 are being fixed in a follow-up commit on this branch. Both are cheap and both close a hole through which a real regression would pass unseen.

Findings 3 and 4 are recorded rather than fixed, because both are coverage limits rather than defects, and both need something this repository does not have: 3 wants the check to iterate composed dev machines instead of assuming one machine and the default source, and 4 wants a synthetic registry faithful enough to drive the real resolver. They also sit on top of a larger gap already known — the public secrets template declares no GitHub targets at all, so the entire GitHub path has no real-machine coverage anywhere public. Confirmed arithmetically: the candidate closure gained four files, not five, because only the policy files are carved for allod-dev. Closing 3 and 4 properly is the same work as giving that path real coverage, and it wants a decision about whether it belongs here or against the private fleet.

Verdict from the pass: safe to merge with these gaps recorded, and not safe to deploy until the human rebuild and reboot gate has run. That gate now carries more weight than the plan assumed, since it is the first time the GitHub credential path is exercised against real data.

Adversarial read-only review pass by `gpt-5.6-sol` at `xhigh` effort, cross-vendor from the `claude-opus-5` that wrote the code. Four findings, no blockers. Every one is a way the new check can stay green while the property it guards is false — none is a defect in the carves themselves, which the pass confirmed correct. **Confirmed correct and worth not undoing later:** the five carves use the right source and basename; nested `consumer.secret` paths work; `toString` is valid for the current path values; two conflicting duplicate targets cannot both match; empty target lists, Forge opt-out, and invalid consumers all behave; no secrets-root child construction remains anywhere in the `mkDevVm` module graph; and `mkPrivacyVm` / `mkHypervisor` genuinely do not import either changed module. ## 1. [GAP] The root sweep misses the root itself — verified `flake.nix:976` builds `secretsRootPrefix = "${toString secrets}/"` with a trailing slash, so `lib.hasPrefix` matches children of the root but not the root itself. Adding `home.file.".cache/secrets-root".source = gitPolicySource` leaves all four named assertions green while the machine carries the entire secrets repository — the exact failure this check exists to prevent. Being fixed in a follow-up commit. ## 2. [GAP] Exact equality does not prove a closure dependency — verified Nix string equality compares contents and ignores store context. Confirmed on 2.31.5 against a two-file fixture: ``` carved == builtins.unsafeDiscardStringContext (toString carved) -> true context of carved -> ["/nix/store/<hash>-x.age"] context of stripped -> [] ``` So setting `file = builtins.unsafeDiscardStringContext (toString (carvedSecretFile consumer))` passes the matcher, the equality assertion, and the store-root shape assertion, while the generated system names the correct path without retaining it as an input. The ciphertext is then not guaranteed to be in the runtime closure, and agenix can fail after transfer or after a garbage collection. The current code preserves context correctly; the check simply does not prove it does. Being fixed in a follow-up commit by asserting the carved value's context retains its own store path. ## 3. [GAP] Policy coverage is hardwired to `allod-dev` with the default source `flake.nix:943` keys the policy assertions to `allod-dev` and compares against the secrets input directly. A second dev profile that `mkForce`s one policy `home.file.source` back to `"${secrets}/git/..."` keeps the check green while that machine retains the root. The converse also holds: a legitimate `gitPolicySource` override with different policy bytes is carved correctly by the module but rejected by the check against the hardcoded input. ## 4. [GAP] The GitHub fixture bypasses the real consumer resolution `flake.nix:1043` passes `fixtureConsumer` directly rather than exercising `githubAgenixConsumer` at `flake.nix:505`. Make that lookup return `null` or filter the wrong repository and both this check and `credential-profiles` stay green while every real non-empty GitHub target is rejected. The lookup is statically correct today; it is simply not proven end to end. ## What is being fixed here and what is not Findings 1 and 2 are being fixed in a follow-up commit on this branch. Both are cheap and both close a hole through which a real regression would pass unseen. Findings 3 and 4 are recorded rather than fixed, because both are coverage limits rather than defects, and both need something this repository does not have: 3 wants the check to iterate composed dev machines instead of assuming one machine and the default source, and 4 wants a synthetic registry faithful enough to drive the real resolver. They also sit on top of a larger gap already known — the public secrets template declares no GitHub targets at all, so the entire GitHub path has no real-machine coverage anywhere public. Confirmed arithmetically: the candidate closure gained four files, not five, because only the policy files are carved for `allod-dev`. Closing 3 and 4 properly is the same work as giving that path real coverage, and it wants a decision about whether it belongs here or against the private fleet. Verdict from the pass: safe to merge with these gaps recorded, and not safe to deploy until the human rebuild and reboot gate has run. That gate now carries more weight than the plan assumed, since it is the first time the GitHub credential path is exercised against real data.

allod-agent added 1 commit

2026-07-31 06:31:31 +01:00

Close two ways the carve-out check could stay green while wrong bc438c4fa1

The home.file sweep matched only children of the secrets root, so a
consumer set to the root itself with no appended path slipped past while
the machine carried the whole repository. Match the root as well as its
children, and say retain rather than name a child in the diagnostic.

String equality ignores store context, so naming the carved file is not
the same as depending on it: a context-stripped copy compares equal while
retaining nothing, leaving the ciphertext outside the runtime closure and
agenix able to fail after transfer or a collection. Require both the
policy sources and the GitHub predicate to carry their own store path, and
add the context-stripped mutation that only that guard rejects.

Both guards were shown to fail on sabotage. All ten checks pass and the
toplevel is byte-identical, so this is check-only and moves no machine.

Refs allod/archetypes#21

Model: claude-opus-5

allod-agent commented

2026-07-31 06:31:46 +01:00

Author

Member

Findings 1 and 2 are fixed in bc438c4. Both guards were shown to fail on sabotage rather than assumed to work.

Finding 1: adding home.file.".cache/secrets-root".source = gitPolicySource — a consumer equal to the root with no appended path — now fails with home.file source(s) still retain the secrets input root: .cache/secrets-root. Before the fix it passed silently.

Finding 2: deleting the context guard from githubSecretMatchesTarget makes the check fail on the newly added context-stripped carved path mutation. That mutation compares equal to the real carved value, so nothing else in the check rejects it. The guard is builtins.hasAttr (unsafeDiscardStringContext p) (builtins.getContext p), applied to both the four policy sources and the GitHub predicate, so it covers every machine credential-profiles sees rather than only the fixture.

Verified after the change: all ten archetypes checks pass; allod-dev's toplevel is byte-identical to the pre-fix candidate (99frlacp…), so this is check-only and moves no machine; and the secrets root is still absent from the runtime closure.

Findings 3 and 4 remain open as recorded above — both need coverage this repository cannot supply on its own, and both fold into the larger question of giving the GitHub path any real-machine coverage at all.

Findings 1 and 2 are fixed in `bc438c4`. Both guards were shown to fail on sabotage rather than assumed to work. Finding 1: adding `home.file.".cache/secrets-root".source = gitPolicySource` — a consumer equal to the root with no appended path — now fails with `home.file source(s) still retain the secrets input root: .cache/secrets-root`. Before the fix it passed silently. Finding 2: deleting the context guard from `githubSecretMatchesTarget` makes the check fail on the newly added `context-stripped carved path` mutation. That mutation compares equal to the real carved value, so nothing else in the check rejects it. The guard is `builtins.hasAttr (unsafeDiscardStringContext p) (builtins.getContext p)`, applied to both the four policy sources and the GitHub predicate, so it covers every machine `credential-profiles` sees rather than only the fixture. Verified after the change: all ten archetypes checks pass; `allod-dev`'s toplevel is byte-identical to the pre-fix candidate (`99frlacp…`), so this is check-only and moves no machine; and the secrets root is still absent from the runtime closure. Findings 3 and 4 remain open as recorded above — both need coverage this repository cannot supply on its own, and both fold into the larger question of giving the GitHub path any real-machine coverage at all.

vnprc force-pushed agent/consumed-file-carve-out from bc438c4fa1 to 38711aa943

2026-09-02 07:12:18 +01:00

Compare

allod-agent added 1 commit

2026-09-03 01:56:27 +01:00

Pass targets to the GitHub credential module in the carve-out fixture 74565b21de

allod-agent commented

2026-09-03 01:56:45 +01:00

Author

Member

Rebase check: one stale call site, now fixed; the carve-out itself is sound

74565b2 repairs a test call site the rebase exposed. ./check.sh passes: all 32 steps.

What broke. modules/github-credentials.nix gained an explicit targets argument on master after this PR was written — part of the microvm-refusal work in allod/archetypes#29. Production moved with it (mkGithubCredentialModule passes targets in), but this PR's consumed-file-carve-out check still called the module the old way, reading targets off secrets.lib. After the rebase the check failed with function 'anonymous lambda' called without required argument 'targets'.

The fixture now threads one target list to both the module argument and the synthetic secrets input, which is the seam production uses. Passing them separately would let the two halves of a fixture disagree about which targets are declared.

Worth stating plainly: the rebase is what caught this. A stale PR that still evaluates is more dangerous than one that fails to.

The sabotage still bites. Un-carving one policy source in place fails with consumed-file-carve-out: policy source mismatch: .config/git/protected-branches (expected /nix/store/…-protected-branches, got /nix/store/…-source/git/protected-branches). The check is not passing for a new and wrong reason.

Closure re-measured against current master

Built allod-dev and inspected the realised closure rather than re-reading the earlier test log:

875 requisites, and the secrets source root is absent.
All six consumed files are present as individual store objects: the four git policy files, agent-pr-token.age, and forgejo-https-token-allod-dev.age.
The only -source roots remaining are nixpkgs and allod-tools, matching what this PR claimed and both out of scope.

No consumer was missed. That is structural rather than lucky: the carve changes how a file enters the closure, not which files are consumed, so an uncarved consumer would still drag in the whole root — and the root is gone. A grep for interpolations of the secrets root also finds no consumer added since this PR was written; the remaining hits are checks that deliberately read the repo.

A trap for the next reader

toString on either age secret shows a path inside the secrets source root, which reads exactly like the carve failed for those two files. It did not. builtins.getContext "${secret.file}" shows the closure depending on individual store objects (…-agent-pr-token.age), because Nix path coercion copies the single file on its own — which is what this PR's body says and what its test 6 asserts by interpolation rather than toString.

Recording it here because the obvious check gives the wrong answer, and the next person to audit this will reach for toString first.

## Rebase check: one stale call site, now fixed; the carve-out itself is sound `74565b2` repairs a test call site the rebase exposed. `./check.sh` passes: all 32 steps. **What broke.** `modules/github-credentials.nix` gained an explicit `targets` argument on master after this PR was written — part of the microvm-refusal work in `allod/archetypes#29`. Production moved with it (`mkGithubCredentialModule` passes `targets` in), but this PR's `consumed-file-carve-out` check still called the module the old way, reading targets off `secrets.lib`. After the rebase the check failed with `function 'anonymous lambda' called without required argument 'targets'`. The fixture now threads one target list to both the module argument and the synthetic secrets input, which is the seam production uses. Passing them separately would let the two halves of a fixture disagree about which targets are declared. Worth stating plainly: the rebase is what caught this. A stale PR that still evaluates is more dangerous than one that fails to. **The sabotage still bites.** Un-carving one policy source in place fails with `consumed-file-carve-out: policy source mismatch: .config/git/protected-branches (expected /nix/store/…-protected-branches, got /nix/store/…-source/git/protected-branches)`. The check is not passing for a new and wrong reason. ## Closure re-measured against current master Built `allod-dev` and inspected the realised closure rather than re-reading the earlier test log: - 875 requisites, and the secrets source root is **absent**. - All six consumed files are present as individual store objects: the four git policy files, `agent-pr-token.age`, and `forgejo-https-token-allod-dev.age`. - The only `-source` roots remaining are nixpkgs and `allod-tools`, matching what this PR claimed and both out of scope. No consumer was missed. That is structural rather than lucky: the carve changes how a file enters the closure, not which files are consumed, so an uncarved consumer would still drag in the whole root — and the root is gone. A grep for interpolations of the secrets root also finds no consumer added since this PR was written; the remaining hits are checks that deliberately read the repo. ## A trap for the next reader `toString` on either age secret shows a path *inside* the secrets source root, which reads exactly like the carve failed for those two files. It did not. `builtins.getContext "${secret.file}"` shows the closure depending on individual store objects (`…-agent-pr-token.age`), because Nix path coercion copies the single file on its own — which is what this PR's body says and what its test 6 asserts by interpolation rather than `toString`. Recording it here because the obvious check gives the wrong answer, and the next person to audit this will reach for `toString` first.

This pull request doesn't have enough approvals yet. 0 of 1 approvals granted.

This branch is out-of-date with the base branch

You are not authorized to merge this pull request.

View command line instructions