Share the token-ciphertext form test with the Pi provider module and give its assertions a witness #114

New issue

Closed

opened 2026-09-23 16:59:07 +01:00 by allod-agent · 0 comments

allod-agent commented

2026-09-23 16:59:07 +01:00

Member

Bring the Pi provider module's token-ciphertext form test up to the same standard as mkDevVm's and host-user-credentials': one shared predicate (nix/secret-file-form.nix, allod/archetypes#112) at all three seams, and a check that can show the Pi seam refusing a leaking value.

Primary goals:

One rule at three doors — modules/pi-provider-lifecycle.nix decides whether a token ciphertext is one regular file with the predicate mkDevVm and host-user-credentials already share, and its message borrows the shared explanation, so the three seams accept the same spellings and refuse the same leak.
The Pi assertions get a witness — today no check evaluates them: checks/pi-provider-lifecycle.nix reads the fixture's activation scripts and never forces system.build.toplevel or reads config.assertions, so all three assertions entries in the module could be deleted with every check green. A positive fixture must be shown to reach them, and a sabotage must make the form assertion fire.
No reachable behaviour changes — a deployment cannot hand this module a hand-spelled value today (allod/secrets derives every token file from ./secrets and mkDevVm pins the projection to the joined contract), so the change is consistency and coverage, not a fix a user can observe.

Current state and specifics

modules/pi-provider-lifecycle.nix:149-155 computes badTokenFiles with !(builtins.isPath ….file), the pre-#112 rule; :197-201 is the assertion, message "contains a missing or non-path token ciphertext file". nix/secret-file-form.nix holds the rule the other two seams use: null, or a path or a string whose only string-context element is a source path equal to itself, and a regular file. Null is not valid for a Pi token, so the Pi seam wants the "regular single file" half of that rule without the null clause; the shared file should expose that half by name rather than have the module re-derive it.

checks/pi-provider-lifecycle.nix:47-48 supplies the two token files as path literals; :109-113 are the only reads of the fixture machine and they are activation-script texts. NixOS assertions are reached only through system.build.toplevel (nix.md), so the fixture's assertions are unevaluated, and there is no negative fixture at all.

allod/secrets lib/pi-credential-contract.nix:50 builds every token file as ciphertextRoot + "/pi-credentials/<id>/<token>.age" with ciphertextRoot = ./secrets, and mkDevVm asserts the machine's Pi projection equals the joined contract, which is why the case is unreachable from a deployment today.

Scope

In: the predicate swap and message in modules/pi-provider-lifecycle.nix; exposing the null-free half of the rule in nix/secret-file-form.nix without changing what the other two seams accept; in checks/pi-provider-lifecycle.nix, a positive proof that the fixture's assertions are evaluated and hold, and one sabotage fixture with a directory-interpolated token file that the form assertion refuses, held as a thunk so the check's peak stays bounded (nix.md). The gate's derivation-unchanged witness applies to every machine and every check but this one; the PR names it.

Out: the two leaks recorded in allod/archetypes#21 (modules/agent-hooks.nix, modules/github-credentials.nix), which no argument-level assertion sees; changing how allod/secrets spells token files.

Bring the Pi provider module's token-ciphertext form test up to the same standard as mkDevVm's and host-user-credentials': one shared predicate (`nix/secret-file-form.nix`, allod/archetypes#112) at all three seams, and a check that can show the Pi seam refusing a leaking value. Primary goals: - **One rule at three doors** — `modules/pi-provider-lifecycle.nix` decides whether a token ciphertext is one regular file with the predicate mkDevVm and host-user-credentials already share, and its message borrows the shared explanation, so the three seams accept the same spellings and refuse the same leak. - **The Pi assertions get a witness** — today no check evaluates them: `checks/pi-provider-lifecycle.nix` reads the fixture's activation scripts and never forces `system.build.toplevel` or reads `config.assertions`, so all three `assertions` entries in the module could be deleted with every check green. A positive fixture must be shown to reach them, and a sabotage must make the form assertion fire. - **No reachable behaviour changes** — a deployment cannot hand this module a hand-spelled value today (`allod/secrets` derives every token file from `./secrets` and mkDevVm pins the projection to the joined contract), so the change is consistency and coverage, not a fix a user can observe. ### Current state and specifics `modules/pi-provider-lifecycle.nix:149-155` computes `badTokenFiles` with `!(builtins.isPath ….file)`, the pre-#112 rule; `:197-201` is the assertion, message "contains a missing or non-path token ciphertext file". `nix/secret-file-form.nix` holds the rule the other two seams use: null, or a path or a string whose only string-context element is a source path equal to itself, and a regular file. Null is not valid for a Pi token, so the Pi seam wants the "regular single file" half of that rule without the null clause; the shared file should expose that half by name rather than have the module re-derive it. `checks/pi-provider-lifecycle.nix:47-48` supplies the two token files as path literals; `:109-113` are the only reads of the fixture machine and they are activation-script texts. NixOS assertions are reached only through `system.build.toplevel` (`nix.md`), so the fixture's assertions are unevaluated, and there is no negative fixture at all. `allod/secrets` `lib/pi-credential-contract.nix:50` builds every token file as `ciphertextRoot + "/pi-credentials/<id>/<token>.age"` with `ciphertextRoot = ./secrets`, and mkDevVm asserts the machine's Pi projection equals the joined contract, which is why the case is unreachable from a deployment today. ### Scope In: the predicate swap and message in `modules/pi-provider-lifecycle.nix`; exposing the null-free half of the rule in `nix/secret-file-form.nix` without changing what the other two seams accept; in `checks/pi-provider-lifecycle.nix`, a positive proof that the fixture's assertions are evaluated and hold, and one sabotage fixture with a directory-interpolated token file that the form assertion refuses, held as a thunk so the check's peak stays bounded (`nix.md`). The gate's derivation-unchanged witness applies to every machine and every check but this one; the PR names it. Out: the two leaks recorded in allod/archetypes#21 (`modules/agent-hooks.nix`, `modules/github-credentials.nix`), which no argument-level assertion sees; changing how `allod/secrets` spells token files.

allod-agent referenced this issue from a commit

2026-09-23 17:06:45 +01:00

Share the token-ciphertext form test with the Pi provider module

allod-agent referenced this issue from a pull request that will close it,

2026-09-23 17:06:45 +01:00

Share the token-ciphertext form test with the Pi provider module #115