From 43c48473d43ccb5b0b0797d08f52bce32066b155 Mon Sep 17 00:00:00 2001 From: Jason Bowman Date: Fri, 31 Jul 2026 23:15:16 -0700 Subject: [PATCH] den: declare value-conditional policy codomains (binds, suppresses) Both records emit their codomain from a value-conditional body, so a body fired at a value-less sentinel takes the false branch and the codomain cannot be observed by firing. env-to-hosts declares the accessGroups member binding it carries into host scope; drop-user-to-host-on-droid declares the policy its exclusion suppresses. Stratification is decided from the declared graph, so an edge known only at runtime is one the check never sees. Both are authored as policy records rather than bare functions because a bare closure has no field to declare a codomain on. The extra fields are inert under the current den pin: the fleet surfaces are byte-identical across the change. --- modules/den/batteries/nix-on-droid.nix | 17 +++++- modules/den/policies/fleet.nix | 82 +++++++++++++++----------- 2 files changed, 61 insertions(+), 38 deletions(-) diff --git a/modules/den/batteries/nix-on-droid.nix b/modules/den/batteries/nix-on-droid.nix index abbf7980..0d5ee9cc 100644 --- a/modules/den/batteries/nix-on-droid.nix +++ b/modules/den/batteries/nix-on-droid.nix @@ -94,9 +94,20 @@ in # modules below, and an mkForce on home.username/homeDirectory in # core.nix-on-droid-base. All three keep the stock den batteries untouched, so # nixos/darwin hosts stay byte-identical.) - den.policies.drop-user-to-host-on-droid = - { host, ... }: - lib.optional (host.class == "droid") (den.lib.policy.exclude den.policies.user-to-host); + # Written as a policy record rather than a bare function so it can carry + # `suppresses`. The exclusion is value-conditional — it fires only where the host + # is droid — so a body fired at a sentinel context takes the false branch and + # produces no suppression at all. The suppression codomain therefore cannot be + # observed by firing the body and has to be stated here; the stratification reads + # suppression edges from the declared graph, and an empty recovery would let the + # first real exclusion be refused. + den.policies.drop-user-to-host-on-droid = { + __isPolicy = true; + suppresses = [ "user-to-host" ]; + fn = + { host, ... }: + lib.optional (host.class == "droid") (den.lib.policy.exclude den.policies.user-to-host); + }; # Registered at default scope (not host scope) to mirror den's os-class.nix: # user content is emitted at host AND user scope, so the exclude must fire in diff --git a/modules/den/policies/fleet.nix b/modules/den/policies/fleet.nix index c58d0751..cd5de5a2 100644 --- a/modules/den/policies/fleet.nix +++ b/modules/den/policies/fleet.nix @@ -39,42 +39,54 @@ in ) environments; # environment -> hosts: walk den.hosts whose environment matches. - den.policies.env-to-hosts = - { environment, ... }: - let - inherit (config) fleet; - envGrant = (fleet.user-access.by-environment.${environment.name} or { groups = [ ]; }).groups; - envGate = environment.system-access-groups or [ ]; - in - lib.concatMap ( - system: + # + # Written as a policy record rather than a bare function so it can carry `binds`. + # The `accessGroups` member binding below is emitted from a value-conditional body, + # and a body fired at a sentinel context takes the false branch and carries no + # binding — so this codomain cannot be observed by firing and has to be declared. + # A containment binding is a positive dependency edge of every policy that + # destructures it (env-users), and the stratification is decided from the declared + # graph, so an edge known only at runtime is one the check never sees. + den.policies.env-to-hosts = { + __isPolicy = true; + binds = [ "accessGroups" ]; + fn = + { environment, ... }: + let + inherit (config) fleet; + envGrant = (fleet.user-access.by-environment.${environment.name} or { groups = [ ]; }).groups; + envGate = environment.system-access-groups or [ ]; + in lib.concatMap ( - hostName: - let - hostCfg = den.hosts.${system}.${hostName}; - hostGrant = (fleet.user-access.by-host.${hostName} or { groups = [ ]; }).groups; - hostGate = hostCfg.system-access-groups; - # Effective gate: union of env + host gates (matching main's mergedAccessGroups) - effectiveGate = lib.unique (envGate ++ hostGate); - # Effective grant: union of env + host grants + host gates - # (host system-access-groups is both a gate and an implicit grant) - allGrants = lib.unique (envGrant ++ hostGrant ++ hostGate); - # Users must match both a grant AND a gate group - accessGroups = - if effectiveGate == [ ] then - allGrants - else - builtins.filter (g: builtins.elem g effectiveGate) allGrants; - in - lib.optionals ((hostCfg.environment or "prod") == environment.name && hostCfg.intoAttr != [ ]) [ - (resolve.to "host" { - host = hostCfg; - inherit accessGroups; - }) - (den.lib.policy.instantiate hostCfg) - ] - ) (builtins.attrNames (den.hosts.${system} or { })) - ) (builtins.attrNames (den.hosts or { })); + system: + lib.concatMap ( + hostName: + let + hostCfg = den.hosts.${system}.${hostName}; + hostGrant = (fleet.user-access.by-host.${hostName} or { groups = [ ]; }).groups; + hostGate = hostCfg.system-access-groups; + # Effective gate: union of env + host gates (matching main's mergedAccessGroups) + effectiveGate = lib.unique (envGate ++ hostGate); + # Effective grant: union of env + host grants + host gates + # (host system-access-groups is both a gate and an implicit grant) + allGrants = lib.unique (envGrant ++ hostGrant ++ hostGate); + # Users must match both a grant AND a gate group + accessGroups = + if effectiveGate == [ ] then + allGrants + else + builtins.filter (g: builtins.elem g effectiveGate) allGrants; + in + lib.optionals ((hostCfg.environment or "prod") == environment.name && hostCfg.intoAttr != [ ]) [ + (resolve.to "host" { + host = hostCfg; + inherit accessGroups; + }) + (den.lib.policy.instantiate hostCfg) + ] + ) (builtins.attrNames (den.hosts.${system} or { })) + ) (builtins.attrNames (den.hosts or { })); + }; # Schema wiring. den.schema.flake.includes = [ den.policies.to-fleet ];