Remove the credential pairing assertion #19

Merged

vnprc merged 1 commit from agent/drop-credential-pairing-assert into master

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

allod-agent commented

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

Member

The assert claimed the agent PR token and the Forge HTTPS credential are two faces of one fact. They are not. One decides whether a machine may open a pull request; the other becomes /root/.git-credentials and the netrc files that let the Nix daemon fetch private flake inputs at all — that is, whether the machine can rebuild itself. A machine that can rebuild itself and must never open a pull request is a coherent least-privilege posture, and the assert refused to evaluate it. The reviewer confirmed by experiment that both half-null shapes compose into working single-secret machines once the assert is gone.

It was also in the wrong layer. The assert lived in the public framework, enforcing the shape of data a private fork's identity template owns, which runs architecture.md principle 5 backwards.

And it did not achieve its purpose. The goal was that a machine which needs a token but lacks a usable one should fail at build time rather than at first boot, where "usable" means decryptable. The assert checked presence and pairing, never whether the machine is a recipient of the ciphertext, so the failure the issue actually describes still lands at first activation. The invariant that would work — every generated secret must list the machine's own host key among its recipients — is filed as allod/archetypes#20, and it needs one export from allod/secrets before it can be written.

This also removes a second-order hazard the reviewer caught: because the assert threw from the head of the builder rather than through the module system, a fork whose secrets template nulls only one file would lose its whole flake check, not just that machine.

What remains from 40bbc3b is the load-bearing part: the token module is included only when there is a token, an opted-out machine generates no secrets and no agenix activation, and a machine with access keeps both secrets at literally the same paths, owners and modes as before.

Refs allod/archetypes#17

Risk

R1. A deletion of 66 lines, all of them the assert, its lifted helper, and the six fixtures that existed only to exercise it. No machine currently sets the opt-out flag, so nothing in the public repos changes behaviour. Rollback is a revert.

Validation

nix flake check passes, 9 checks. dev-forge-opt-out and credential-profiles both build green with the remaining assertions, which are the ones that test the system rather than the truth table of a one-line function: the opted-out fixture generates no age.secrets and no agenix activation, the with-access machine matches a literal capture of today's two secrets, and the built activation script is grepped for the decrypt step so the absence proof cannot pass vacuously.

allod-dev still evaluates to a complete system derivation. Its derivation hash differs from master's only because this branch is a different source path for the flake itself; the reviewer established during the review that any change to a referenced input shifts a machine whose configuration embeds that input's store path, and verified it with a comment-only control. The generated age.secrets for allod-dev are unchanged, which is the property that matters and which the check pins literally.

The assert claimed the agent PR token and the Forge HTTPS credential are two faces of one fact. They are not. One decides whether a machine may open a pull request; the other becomes `/root/.git-credentials` and the netrc files that let the Nix daemon fetch private flake inputs at all — that is, whether the machine can rebuild itself. A machine that can rebuild itself and must never open a pull request is a coherent least-privilege posture, and the assert refused to evaluate it. The reviewer confirmed by experiment that both half-null shapes compose into working single-secret machines once the assert is gone. It was also in the wrong layer. The assert lived in the public framework, enforcing the shape of data a private fork's identity template owns, which runs `architecture.md` principle 5 backwards. And it did not achieve its purpose. The goal was that a machine which needs a token but lacks a *usable* one should fail at build time rather than at first boot, where "usable" means decryptable. The assert checked presence and pairing, never whether the machine is a recipient of the ciphertext, so the failure the issue actually describes still lands at first activation. The invariant that would work — every generated secret must list the machine's own host key among its recipients — is filed as allod/archetypes#20, and it needs one export from `allod/secrets` before it can be written. This also removes a second-order hazard the reviewer caught: because the assert threw from the head of the builder rather than through the module system, a fork whose secrets template nulls only one file would lose its whole flake check, not just that machine. What remains from `40bbc3b` is the load-bearing part: the token module is included only when there is a token, an opted-out machine generates no secrets and no agenix activation, and a machine with access keeps both secrets at literally the same paths, owners and modes as before. Refs allod/archetypes#17 ## Risk R1. A deletion of 66 lines, all of them the assert, its lifted helper, and the six fixtures that existed only to exercise it. No machine currently sets the opt-out flag, so nothing in the public repos changes behaviour. Rollback is a revert. ## Validation `nix flake check` passes, 9 checks. `dev-forge-opt-out` and `credential-profiles` both build green with the remaining assertions, which are the ones that test the system rather than the truth table of a one-line function: the opted-out fixture generates no `age.secrets` and no agenix activation, the with-access machine matches a literal capture of today's two secrets, and the built activation script is grepped for the decrypt step so the absence proof cannot pass vacuously. `allod-dev` still evaluates to a complete system derivation. Its derivation hash differs from master's only because this branch is a different source path for the flake itself; the reviewer established during the review that any change to a referenced input shifts a machine whose configuration embeds that input's store path, and verified it with a comment-only control. The generated `age.secrets` for `allod-dev` are unchanged, which is the property that matters and which the check pins literally.

allod-agent added 1 commit

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