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

Merged

vnprc merged 3 commits from agent/pi-token-form-shared-predicate into master

2026-09-23 17:27:46 +01:00

allod-agent commented

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

Member

Summary

No running machine changes: all four toplevel derivations and all 18 check outputs are identical to master. The Pi provider module now judges a token ciphertext file by the same rule mkDevVm and the hypervisor credential module already share, so all three seams accept the same spellings and refuse the same leak; before, it accepted only a path literal. That case is unreachable from a deployment today (the secrets library always builds a path), so the visible change is in what the check proves: the module's three assertions were never evaluated by any check, and now the fixture is forced to toplevel and a sabotage with a directory-interpolated token file is shown to trip exactly the form assertion. If the wording or the stricter rule is unwanted, revert the one commit.

What changed

nix/secret-file-form.nix exposes the null-free half of the rule as isRegularSingleFile and its explanation as formExplanation; isAcceptedForm and explanation are defined in terms of them and are unchanged in meaning, so mkDevVm and host-user-credentials accept exactly what they did.
modules/pi-provider-lifecycle.nix uses isRegularSingleFile in badTokenFiles (a missing or null file stays rejected) and its message borrows the shared explanation.
checks/pi-provider-lifecycle.nix forces the fixture's system.build.toplevel (the only way NixOS assertions run, nix.md) and asserts none fail; a second fixture spells one token file as "${fixtureDir}/default-token.age", is read through config.assertions rather than a tryEval so the failing assertion is named, and must yield exactly one failure containing "unacceptable token ciphertext file". The sabotaged machine is consumed in that one assertion.

Risk

R2: a localized change to a guard whose reachable inputs are unchanged, with the new coverage as the main effect. Worst credible failure after the checks pass: the sabotage passing for an unrelated reason; the assertion requires exactly one failing NixOS assertion with the form message, so a broken sabotage machine (zero or several failures) is reported, not accepted.

Validation

./check.sh on the branch: all 31 steps passed (18 checks built). Machine drvPaths and all 18 check outputs identical to a master run, pi-provider-lifecycle included: the new assertions run at evaluation time and its runCommand inputs are unchanged, so the derivation-unchanged witness holds for every check.
Peak memory of the pi-provider-lifecycle step: 1182 MiB (master: 1012 to 1016 MiB), from forcing the fixture toplevel and evaluating the sabotaged machine's assertions.
Negative control: isRegularSingleFile forced to true makes the check fail with "directoryTokenRefusals is not exactly the token-ciphertext form assertion:" and an empty list; restored before commit.
Cross-family review (codex, gpt-5.6-terra, high effort): two findings, both wording, both applied in the second commit. (1) The sabotage comment claimed the sabotaged machine never lives beside the positive fixture; the positive fixture stays live for later reads, so the two overlap during the one assertion that reads the sabotage. The comment now says so and quotes the measured cost (about 170 MiB). (2) The assertion message said "missing", which read as a nonexistent file; a nonexistent path throws in readFileType before the assertion, so the message now says "lacks a token ciphertext file". No finding in the vacuity or acceptance-change categories.

Closes allod/archetypes#114

## Summary No running machine changes: all four toplevel derivations and all 18 check outputs are identical to master. The Pi provider module now judges a token ciphertext file by the same rule mkDevVm and the hypervisor credential module already share, so all three seams accept the same spellings and refuse the same leak; before, it accepted only a path literal. That case is unreachable from a deployment today (the secrets library always builds a path), so the visible change is in what the check proves: the module's three assertions were never evaluated by any check, and now the fixture is forced to toplevel and a sabotage with a directory-interpolated token file is shown to trip exactly the form assertion. If the wording or the stricter rule is unwanted, revert the one commit. ## What changed - `nix/secret-file-form.nix` exposes the null-free half of the rule as `isRegularSingleFile` and its explanation as `formExplanation`; `isAcceptedForm` and `explanation` are defined in terms of them and are unchanged in meaning, so mkDevVm and host-user-credentials accept exactly what they did. - `modules/pi-provider-lifecycle.nix` uses `isRegularSingleFile` in `badTokenFiles` (a missing or null file stays rejected) and its message borrows the shared explanation. - `checks/pi-provider-lifecycle.nix` forces the fixture's `system.build.toplevel` (the only way NixOS assertions run, nix.md) and asserts none fail; a second fixture spells one token file as `"${fixtureDir}/default-token.age"`, is read through `config.assertions` rather than a `tryEval` so the failing assertion is named, and must yield exactly one failure containing "unacceptable token ciphertext file". The sabotaged machine is consumed in that one assertion. ## Risk R2: a localized change to a guard whose reachable inputs are unchanged, with the new coverage as the main effect. Worst credible failure after the checks pass: the sabotage passing for an unrelated reason; the assertion requires exactly one failing NixOS assertion with the form message, so a broken sabotage machine (zero or several failures) is reported, not accepted. ## Validation - `./check.sh` on the branch: all 31 steps passed (18 checks built). Machine drvPaths and all 18 check outputs identical to a master run, `pi-provider-lifecycle` included: the new assertions run at evaluation time and its `runCommand` inputs are unchanged, so the derivation-unchanged witness holds for every check. - Peak memory of the `pi-provider-lifecycle` step: 1182 MiB (master: 1012 to 1016 MiB), from forcing the fixture toplevel and evaluating the sabotaged machine's assertions. - Negative control: `isRegularSingleFile` forced to `true` makes the check fail with "directoryTokenRefusals is not exactly the token-ciphertext form assertion:" and an empty list; restored before commit. - Cross-family review (codex, gpt-5.6-terra, high effort): two findings, both wording, both applied in the second commit. (1) The sabotage comment claimed the sabotaged machine never lives beside the positive fixture; the positive fixture stays live for later reads, so the two overlap during the one assertion that reads the sabotage. The comment now says so and quotes the measured cost (about 170 MiB). (2) The assertion message said "missing", which read as a nonexistent file; a nonexistent path throws in `readFileType` before the assertion, so the message now says "lacks a token ciphertext file". No finding in the vacuity or acceptance-change categories. Closes allod/archetypes#114

allod-agent added 2 commits

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

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

modules/pi-provider-lifecycle.nix decides a token ciphertext's form with
nix/secret-file-form.nix's isRegularSingleFile, the null-free half of the
rule mkDevVm and host-user-credentials use, and borrows its explanation.
checks/pi-provider-lifecycle.nix forces the fixture's toplevel so the
module's assertions are evaluated at all, and sabotages one token file
with the directory interpolation, asserting exactly the form assertion
fires. Refs allod/archetypes#114

Say what the sabotage costs and what the message means by missing 96e55189e5

allod-agent commented

2026-09-23 17:26:07 +01:00

Author

Member

Owner request: the two comment blocks added to checks/pi-provider-lifecycle.nix (over fixtureToplevel/failingAssertions and over the sabotage fixture) are reasoning essays, not the contract, trap or pointer writing.md allows. Trimming them; the memory-cost and tryEval reasoning stays in this PR body.

Owner request: the two comment blocks added to `checks/pi-provider-lifecycle.nix` (over `fixtureToplevel`/`failingAssertions` and over the sabotage fixture) are reasoning essays, not the contract, trap or pointer writing.md allows. Trimming them; the memory-cost and tryEval reasoning stays in this PR body.

allod-agent added 1 commit

2026-09-23 17:26:50 +01:00

Cut the new comments to the trap and the pointer d8751c8a7b