Skip the agent token module when a dev machine has no token file #18

Merged

vnprc merged 1 commit from agent/agent-token-opt-out into master

2026-07-31 00:34:50 +01:00

allod-agent commented

2026-07-31 00:13:32 +01:00

Member

Refs allod/archetypes#17

What changed

mkDevVm includes modules/agent-forgejo-token.nix only when tokenFile != null, mirroring the adjacent lib.optionalAttrs (httpsTokenFile != null) handling of the Forge HTTPS credential.
A lifted guard, devForgeCredentialMismatch, states the invariant the identity template maintains: the agent token file and the Forge HTTPS credential file are two facets of the single forgeAccess identity fact, so they are both set or both null. mkDevVm asserts it.
A new dev-forge-opt-out check pins the contract with fixtures that reuse allod-dev's real identity and definition, varying only the two token files: the opted-out shape composes with empty age.secrets and no agenix activation entries at all; the with-access shape keeps exactly today's two secrets, with file, path, owner, group, and mode captured literally from master's generated values before this change; each half-null shape fails evaluation, and the guard predicate is exercised directly so each sabotage fixture is pinned to its own reason.

Where the assertion lives, and why

The pairing assert sits at the head of mkDevVm, before nixosSystem — not in the identity template and not only in a check. Three reasons. First, the builder is the last composition point where the final values meet: tokenFile and httpsTokenFile default from the identity but can be overridden per machine through the profiles repo's profileData/profileSettings, so only the builder sees what a machine actually composes with, and a template-level assert would miss an override that nulls one of them for some unrelated reason. Second, the template is forkable data — an assertion there protects only the copy that carries it, while the builder is framework code every deployment shares, which is the deepest layer that cannot be talked out of the rule. Third, an assert at the builder's head makes the broken machine itself refuse to evaluate for every consumer — a deploy flake evaluating nixosConfigurations, not just someone who runs nix flake check — which is what "fail at evaluation, not at first boot" has to mean.

The head position is also load-bearing for the fixtures: a bare weak-head force of the builder call can only be failed by this assert, because the failure it replaces — the token module's file = null type error — only surfaced deep inside module evaluation. The check's half-null fixtures therefore pass only when the eval-head assert itself fires, not when evaluation dies for some other reason.

Landing order

This PR merges first. If the secrets change landed first, an opted-out machine would carry a null agentTokenFile while this builder still included the token module unconditionally — an unhelpful file = null type error for anyone composing in between. In the correct order there is no intermediate breakage: no machine in the public template opts out, and a fork that already ported the opt-out gets a loud, named eval error instead of a machine that fails to decrypt during provisioning.

Out of scope, per the issue: the forgeAccess mechanism itself, and how the shared agent token's recipient set is chosen.

Risk

R2 residual. The territory is inherently R3 — cross-repo sequencing plus generated activation behavior around credentials — but the validation below proves every current machine's derivation unchanged, proves both directions of the new eval error including the exact half-done state the issue describes, and lands sabotage-backed fixtures that keep all of it pinned; rollback is a straight revert. The residual worth human eyes: a private fork whose dev identities legitimately violate the both-or-neither invariant would start failing eval on pull with the new named error. The public template derives both files from one flag so no such shape should exist, but the framework cannot see private forks.

Validation

nix flake check passes on this branch: 9 checks including the new dev-forge-opt-out, peak RSS 2.9 GiB.
Opted-out machine composes clean: the committed fixture asserts config.age.secrets == {} and zero agenix* activation entries; end to end, a scratch secrets tree flipping allod-dev to forgeAccess = false through the real template mapping (with the secrets-side branch) evaluates config.age.secrets to {} under --override-input secrets.
With-access machine unchanged: nixosConfigurations.allod-dev.config.age.secrets on this branch is byte-identical to the baseline captured from master before the change — same files, paths, owners, groups, modes — and the committed check pins that projection literally rather than deriving it from the identity the generator reads.
The eval error fires for its own reason: a scratch secrets in the exact half-done state the issue describes (opt-out flag set under master's mapping, so agent token set and HTTPS token null) fails on this branch with dev machine 'allod-dev': agent token file and Forge HTTPS credential must be both set or both null (identity forgeAccess opts out of both together); got tokenFile set, httpsTokenFile null, while master silently composes that machine with a single age.secrets entry pointing at the undecryptable ciphertext.
The check provably fails on sabotage, each by its own assertion: reverting the conditional include fails with "opted-out fixture still generates age.secrets: agent-pr-token"; neutralizing the assert fails with "agent token without Forge HTTPS credential did not fail at evaluation"; drifting the token mode to 0640 fails the literal metadata pin.
credential-profiles still binds every declared token target to a generated age.secrets entry: it passes here, and against a scratch secrets whose machine opted out while the token registry still declares its HTTPS target it fails loudly (Forgejo token registry targets do not match generated age.secrets file/path: allod-dev.git:forgejo-https-token-allod-dev:allod-dev:/root/.git-credentials), so the registry binding remains the backstop for a half-ported opt-out.
Inertness from allod/deploy, evaluated one configuration at a time with --override-input pinned to explicit revisions (base = both masters, since deploy's committed lock trails master): for all four configurations (allod-dev, nexus, privacy-1, installer), config.system.build.toplevel.drvPath with this branch substituted is identical to base. With the secrets branch also substituted, allod-dev's drvPath shifts while the other three stay identical; that shift belongs entirely to the secrets input — archetypes master with the secrets branch produces the same shifted drvPath, and a comment-only control commit to secrets shifts it again — because dev machines embed the secrets source store path through age.secrets.*.file. Details and the store-prefix-normalized identity proof are in allod/secrets#11.

A dev machine that opts out of Forge access is currently still handed the deployment's shared agent PR token — an encrypted file it has no key for, which breaks the machine the first time it activates, during provisioning. This PR makes the dev builder skip that token when the machine has no token file, the same way it already skips the per-machine Forge HTTPS credential, and adds a guard so a machine that has one of the two credentials without the other refuses to evaluate with an error naming the machine and both fields. No existing machine changes at all — every current machine's build derivation is proven byte-identical. This is the framework half of the fix; it must merge before allod/secrets#11, which completes the other half. Refs allod/archetypes#17 ## What changed - `mkDevVm` includes `modules/agent-forgejo-token.nix` only when `tokenFile != null`, mirroring the adjacent `lib.optionalAttrs (httpsTokenFile != null)` handling of the Forge HTTPS credential. - A lifted guard, `devForgeCredentialMismatch`, states the invariant the identity template maintains: the agent token file and the Forge HTTPS credential file are two facets of the single `forgeAccess` identity fact, so they are both set or both null. `mkDevVm` asserts it. - A new `dev-forge-opt-out` check pins the contract with fixtures that reuse allod-dev's real identity and definition, varying only the two token files: the opted-out shape composes with empty `age.secrets` and no agenix activation entries at all; the with-access shape keeps exactly today's two secrets, with file, path, owner, group, and mode captured literally from master's generated values before this change; each half-null shape fails evaluation, and the guard predicate is exercised directly so each sabotage fixture is pinned to its own reason. ## Where the assertion lives, and why The pairing assert sits at the head of `mkDevVm`, before `nixosSystem` — not in the identity template and not only in a check. Three reasons. First, the builder is the last composition point where the final values meet: `tokenFile` and `httpsTokenFile` default from the identity but can be overridden per machine through the profiles repo's `profileData`/`profileSettings`, so only the builder sees what a machine actually composes with, and a template-level assert would miss an override that nulls one of them for some unrelated reason. Second, the template is forkable data — an assertion there protects only the copy that carries it, while the builder is framework code every deployment shares, which is the deepest layer that cannot be talked out of the rule. Third, an assert at the builder's head makes the broken machine itself refuse to evaluate for every consumer — a deploy flake evaluating `nixosConfigurations`, not just someone who runs `nix flake check` — which is what "fail at evaluation, not at first boot" has to mean. The head position is also load-bearing for the fixtures: a bare weak-head force of the builder call can only be failed by this assert, because the failure it replaces — the token module's `file = null` type error — only surfaced deep inside module evaluation. The check's half-null fixtures therefore pass only when the eval-head assert itself fires, not when evaluation dies for some other reason. ## Landing order This PR merges first. If the secrets change landed first, an opted-out machine would carry a null `agentTokenFile` while this builder still included the token module unconditionally — an unhelpful `file = null` type error for anyone composing in between. In the correct order there is no intermediate breakage: no machine in the public template opts out, and a fork that already ported the opt-out gets a loud, named eval error instead of a machine that fails to decrypt during provisioning. Out of scope, per the issue: the `forgeAccess` mechanism itself, and how the shared agent token's recipient set is chosen. ## Risk R2 residual. The territory is inherently R3 — cross-repo sequencing plus generated activation behavior around credentials — but the validation below proves every current machine's derivation unchanged, proves both directions of the new eval error including the exact half-done state the issue describes, and lands sabotage-backed fixtures that keep all of it pinned; rollback is a straight revert. The residual worth human eyes: a private fork whose dev identities legitimately violate the both-or-neither invariant would start failing eval on pull with the new named error. The public template derives both files from one flag so no such shape should exist, but the framework cannot see private forks. ## Validation - `nix flake check` passes on this branch: 9 checks including the new `dev-forge-opt-out`, peak RSS 2.9 GiB. - Opted-out machine composes clean: the committed fixture asserts `config.age.secrets == {}` and zero `agenix*` activation entries; end to end, a scratch secrets tree flipping allod-dev to `forgeAccess = false` through the real template mapping (with the secrets-side branch) evaluates `config.age.secrets` to `{}` under `--override-input secrets`. - With-access machine unchanged: `nixosConfigurations.allod-dev.config.age.secrets` on this branch is byte-identical to the baseline captured from master before the change — same files, paths, owners, groups, modes — and the committed check pins that projection literally rather than deriving it from the identity the generator reads. - The eval error fires for its own reason: a scratch secrets in the exact half-done state the issue describes (opt-out flag set under master's mapping, so agent token set and HTTPS token null) fails on this branch with `dev machine 'allod-dev': agent token file and Forge HTTPS credential must be both set or both null (identity forgeAccess opts out of both together); got tokenFile set, httpsTokenFile null`, while master silently composes that machine with a single `age.secrets` entry pointing at the undecryptable ciphertext. - The check provably fails on sabotage, each by its own assertion: reverting the conditional include fails with "opted-out fixture still generates age.secrets: agent-pr-token"; neutralizing the assert fails with "agent token without Forge HTTPS credential did not fail at evaluation"; drifting the token mode to 0640 fails the literal metadata pin. - `credential-profiles` still binds every declared token target to a generated `age.secrets` entry: it passes here, and against a scratch secrets whose machine opted out while the token registry still declares its HTTPS target it fails loudly (`Forgejo token registry targets do not match generated age.secrets file/path: allod-dev.git:forgejo-https-token-allod-dev:allod-dev:/root/.git-credentials`), so the registry binding remains the backstop for a half-ported opt-out. - Inertness from `allod/deploy`, evaluated one configuration at a time with `--override-input` pinned to explicit revisions (base = both masters, since deploy's committed lock trails master): for all four configurations (allod-dev, nexus, privacy-1, installer), `config.system.build.toplevel.drvPath` with this branch substituted is identical to base. With the secrets branch also substituted, allod-dev's drvPath shifts while the other three stay identical; that shift belongs entirely to the secrets input — archetypes master with the secrets branch produces the same shifted drvPath, and a comment-only control commit to secrets shifts it again — because dev machines embed the secrets source store path through `age.secrets.*.file`. Details and the store-prefix-normalized identity proof are in allod/secrets#11.

allod-agent added 1 commit

2026-07-31 00:13:32 +01:00

Skip the agent token module when a dev machine has no token file 40bbc3bf77

A dev machine that opts out of Forge access composes without an
agent-pr-token secret instead of carrying a ciphertext whose recipient
set does not include it. An eval-head assert in mkDevVm keeps the two
credential facets paired - agent token and Forge HTTPS credential are
both set or both null - so a machine that must have a token and lacks
one fails at evaluation, not at first activation. The dev-forge-opt-out
check pins the opted-out, with-access, and half-null shapes at the
generated-artifact level.

Refs allod/archetypes#17

allod-agent referenced this pull request from allod/secrets

2026-07-31 00:13:57 +01:00

Null agentTokenFile with forgeTokenFile under the Forge opt-out #11