credential-profiles: read the credential-store URL rule from allod/secrets #86

Merged

vnprc merged 2 commits from agent/credential-url-predicate into master

2026-09-20 16:32:36 +01:00

allod-agent commented

2026-09-20 16:03:38 +01:00

Member

What changes

flake.nix, the credential-profiles check: the local isCredentialStoreUrlTemplate and isCredentialStoreUrlSource definitions and the comment claiming they match the other copies are deleted; the local_auth_refresh clause calls secrets.lib.isCredentialStoreUrlSource. The three hand-written accept templates and nineteen hand-written mutations are replaced by the table's vectors, each applied onto the registry's real credential (alias and targets kept, only value and format replaced) so a rejection can only come from the predicate; every reject vector must fail on the predicate's own message, and an empty accept or reject list fails the check rather than proving nothing.
credential-store-url-parity (new): cmp of cmd/allod/testdata/credential-store-url.json from the pinned allod-tools input against credential-store-url.json from the pinned secrets input, naming both paths on failure.
No lock change: master already pins secrets at 255af16 and allod-tools at 29c0875, which carry the exports and the copy.

One limit worth knowing: the reject pin reuses the same error string the clause emits, so it proves the predicate clause fired for each reject vector, not the wording of the message. Master's fixtures had the same shape.

Risk

R2. Check code only, no generated behaviour; the one integration edge is the two flake inputs the check reads, both already pinned past what it needs. Rollback is a revert.

Validation

Run by the integrator at fe87d7f:

nix build .#checks.x86_64-linux.credential-profiles .#checks.x86_64-linux.credential-store-url-parity --rebuild exits 0. The worker showed the parity check failing on a byte-altered copy of the tools file (differ: char 275, line 10, both paths named), then reverted.
nix flake check --no-build exits 0 (worker run, alone).
The pinned inputs' two copies of the table compare identical with cmp, and the secrets export exposes 26 vectors, all of which the check consumes.
No local definition or parity prose remains: grep -rn "character for character\|isCredentialStoreUrlTemplate = \|isCredentialStoreUrlSource = " flake.nix modules/ checks/ prints nothing.

Cold cross-family review: gpt-5.6-terra via codex exec, reasoning effort high, read the diff at bcafebd (a Claude-family worker authored it). Two findings, both confirmed and fixed in fe87d7f. Blocker: the vectors were applied onto the registry's own refresh entry, so a registry with no local_auth_refresh entry would run no vector and still pass; the validator reads generated machine state (the age secret, the netrc activation script, the machine set), so a registry-independent fixture would need a whole fixture machine in a check run already near the box's memory ceiling, and the fix is instead a loud assertion that the pinned registry carries at least one refresh entry, shown firing with the entry stripped. Should-fix: the anti-vacuity guard accepted one accept and one reject, so a table truncated identically in both repositories would pass here and pass parity; the current sizes are now pinned as minimums. The reviewer traced and cleared: vector application keeps the registry alias, targets, secret path and generated age inputs; each reject pin proves the source-predicate clause fired, since its condition calls the export directly; the format = "raw" reject vector exercises the source guard; parity reads the framework's pinned allod-tools input at the stated path, fails if either file is absent, and has a unique derivation name; no local predicate binding remains and the deployed-file parser stays only in modules/netrc.nix; the lock is unchanged. No second reading follows the fix round; the fixes are settled by the rebuilt checks and the sabotage runs the worker recorded.

Next steps after this lands

Public: bump the deploy lock as usual; the check runs on the framework's own inputs and needs nothing from a deployment. Private, for the deployment that carries its own fork of allod/secrets: the fork must export lib.credentialStoreUrl (the grammar and vectors as data), which the already-merged allod secret rotate reads and refuses an older checkout without, and lib.localAuthRefreshSources (the validated refresh projection), which the refresh script in allod/nexus#58 reads and refuses an older checkout without; and it retires its own copy of the predicate by composing its format policy on lib.isCredentialStoreUrlTemplate from the public flake and running the shared table against the result. Those exports are shaped by the public secrets flake; the fork mirrors them or re-exports the public lib. Verification on the deployment is a refresh that gets past preflight and a rotation that no longer refuses the checkout.

Closes allod/secrets#29

The framework's credential check stops carrying its own copy of the rule that decides what a valid credential-store URL template is, and reads the one definition allod/secrets now exports instead. On a running machine nothing changes: this touches only a `nix flake check` in this repository, and the activation-time parser in `modules/netrc.nix` that guards the file on disk stays independent on purpose. What changes for a maintainer is that the rule now lives in one place: the check's witnesses are the shared table of 4 accept and 22 reject vectors in allod/secrets, every vector runs through the real `local_auth_refresh` validator, and a new `credential-store-url-parity` check fails if allod/tools' copy of that table ever drifts a byte from the secrets one. If it is wrong, revert this PR; the local definitions come back and nothing downstream depends on the new check. This is stage 3 of allod/secrets#29 and the last public piece: stages 1, 2 and 5 are merged, and stage 4 (allod/nexus#58) is merge-ready with master merged in. Closing the issue leaves one private step, stated at the end. ## What changes - `flake.nix`, the `credential-profiles` check: the local `isCredentialStoreUrlTemplate` and `isCredentialStoreUrlSource` definitions and the comment claiming they match the other copies are deleted; the `local_auth_refresh` clause calls `secrets.lib.isCredentialStoreUrlSource`. The three hand-written accept templates and nineteen hand-written mutations are replaced by the table's vectors, each applied onto the registry's real credential (alias and targets kept, only `value` and `format` replaced) so a rejection can only come from the predicate; every reject vector must fail on the predicate's own message, and an empty accept or reject list fails the check rather than proving nothing. - `credential-store-url-parity` (new): `cmp` of `cmd/allod/testdata/credential-store-url.json` from the pinned `allod-tools` input against `credential-store-url.json` from the pinned `secrets` input, naming both paths on failure. - No lock change: master already pins secrets at 255af16 and allod-tools at 29c0875, which carry the exports and the copy. One limit worth knowing: the reject pin reuses the same error string the clause emits, so it proves the predicate clause fired for each reject vector, not the wording of the message. Master's fixtures had the same shape. ## Risk R2. Check code only, no generated behaviour; the one integration edge is the two flake inputs the check reads, both already pinned past what it needs. Rollback is a revert. ## Validation Run by the integrator at fe87d7f: - `nix build .#checks.x86_64-linux.credential-profiles .#checks.x86_64-linux.credential-store-url-parity --rebuild` exits 0. The worker showed the parity check failing on a byte-altered copy of the tools file (`differ: char 275, line 10`, both paths named), then reverted. - `nix flake check --no-build` exits 0 (worker run, alone). - The pinned inputs' two copies of the table compare identical with `cmp`, and the secrets export exposes 26 vectors, all of which the check consumes. - No local definition or parity prose remains: `grep -rn "character for character\|isCredentialStoreUrlTemplate = \|isCredentialStoreUrlSource = " flake.nix modules/ checks/` prints nothing. Cold cross-family review: `gpt-5.6-terra` via `codex exec`, reasoning effort `high`, read the diff at bcafebd (a Claude-family worker authored it). Two findings, both confirmed and fixed in fe87d7f. Blocker: the vectors were applied onto the registry's own refresh entry, so a registry with no `local_auth_refresh` entry would run no vector and still pass; the validator reads generated machine state (the age secret, the netrc activation script, the machine set), so a registry-independent fixture would need a whole fixture machine in a check run already near the box's memory ceiling, and the fix is instead a loud assertion that the pinned registry carries at least one refresh entry, shown firing with the entry stripped. Should-fix: the anti-vacuity guard accepted one accept and one reject, so a table truncated identically in both repositories would pass here and pass parity; the current sizes are now pinned as minimums. The reviewer traced and cleared: vector application keeps the registry alias, targets, secret path and generated age inputs; each reject pin proves the source-predicate clause fired, since its condition calls the export directly; the `format = "raw"` reject vector exercises the source guard; parity reads the framework's pinned `allod-tools` input at the stated path, fails if either file is absent, and has a unique derivation name; no local predicate binding remains and the deployed-file parser stays only in `modules/netrc.nix`; the lock is unchanged. No second reading follows the fix round; the fixes are settled by the rebuilt checks and the sabotage runs the worker recorded. ## Next steps after this lands Public: bump the deploy lock as usual; the check runs on the framework's own inputs and needs nothing from a deployment. Private, for the deployment that carries its own fork of allod/secrets: the fork must export `lib.credentialStoreUrl` (the grammar and vectors as data), which the already-merged `allod secret rotate` reads and refuses an older checkout without, and `lib.localAuthRefreshSources` (the validated refresh projection), which the refresh script in allod/nexus#58 reads and refuses an older checkout without; and it retires its own copy of the predicate by composing its `format` policy on `lib.isCredentialStoreUrlTemplate` from the public flake and running the shared table against the result. Those exports are shaped by the public secrets flake; the fork mirrors them or re-exports the public `lib`. Verification on the deployment is a refresh that gets past preflight and a rotation that no longer refuses the checkout. Closes allod/secrets#29

allod-agent added 2 commits

2026-09-20 16:03:38 +01:00

credential-profiles: read the credential-store URL rule from secrets bcafebdd2f

The check no longer spells out what a credential-store URL template
looks like. It calls the predicate allod/secrets exports, and it builds
both its accept witnesses and its reject fixtures from the vector table
in that repo, so the set of cases it covers is data rather than a copy
that review has to keep in step. The four fixtures that mutate
something other than the template - wrong local username, unknown
source credential, unknown contract, wrong generated age destination -
are unchanged.

A vector states only the two fields the predicate reads, value and
format, so it is applied onto the registry's own credential rather than
replacing it. Keeping the alias the refresh entry names is what lets a
rejected vector be pinned on the predicate's own message instead of on
the reference failing to resolve.

A new check, credential-store-url-parity, compares the copy of that
table checked in to allod/tools against the definition in allod/secrets
and fails naming both repositories when they differ. Nothing else
compares the two files, and allod/tools cannot evaluate Nix cheaply
enough to read the export instead of copying it.

Refs allod/secrets#29

credential-profiles: fail closed when the shared vector witnesses cannot run fe87d7f4f1

Two holes a cold review found in the cutover, both of which let the check
pass while proving nothing about the credential-store URL predicate.

The witnesses and mutations run through the first local_auth_refresh
reference the pinned registry declares. With no such entry the fixture is
null, every vector list is empty, and the assertions over them hold
vacuously. A synthetic reference cannot stand in: the validator reads the
generated age.secrets and activation text off the real machines, and an
invented credential has no ciphertext deployed to /root/.git-credentials,
so driving it would mean building a fixture machine inside a check that
already peaks near this box's memory. It now asserts the registry carries
at least one reference and says why the vectors need it.

The other guard required one accept vector and one reject vector, which a
table truncated the same way in both repositories still satisfies - and
that truncation passes credential-store-url-parity too, since parity only
compares the copies to each other. The guard now pins the sizes the check
was written against as floors, so the table can grow freely and a shrink
is a deliberate edit here as well.

Refs allod/secrets#29

allod-agent referenced this pull request from allod/secrets

2026-09-20 16:04:00 +01:00

One credential-store URL predicate: stop hand-synchronising five spellings of one grammar #29