refactor: checks 改造为属性测试骨架

[luochen1990]

动机

把 checks 从"示例式测试"改造为"属性测试骨架", 为后续真正的属性测试 (生成器 / 笛卡尔积枚举) 铺路.

改动

三要素分离

• test-configs (退化生成器): 枚举 8 个具体 NixOS 配置, 后续可增强为真正的生成器
• properties (属性): 3 条 forall 遍历 software 的不变式, 从 config 自行提取前提条件 (P ⟹ Q)
• driver (package.nix): 笛卡尔积 — 每个 config × 每个 property

3 条属性

属性	不变式	forall
no-leak	P(sw 关闭) ⟹ Q(注入项 absent)	8 software × env/etc 键
entries-invariant	entries == resolveAll(...) 不受 enable 控制	8 software
inject-correctness	P(sw 启用) ⟹ Q(注入值 ∈ provider URLs)	8 software × env/etc/special 键

三态断言 (skip/check/pass)

区分"前提不满足"与"断言通过", 避免假绿. 断言数从 50 提升到 296 (208 passed + 88 skipped).

其他

• software-spec.nix: per-software 规格表 (SSOT: provider key / 注入键), properties forall 遍历的数据源
• 删除 7 个旧 scenarios 文件, 被 3 个 properties 替代
• statix W08 禁用 (字符串插值 ${} 被误判为括号)

验证

just check 全绿: 208 passed, 88 skipped, 0 failed (total 296).

后续 PR

• 生成器增强: test-configs 从枚举升级为排列组合 / 笛卡尔积
• injectKeys 映射提取到模块层 (让 config.cfg.nix 和 properties 共享 SSOT)