From dc40fe6242ee5cd5c16e10e23e11d26cf25506ef Mon Sep 17 00:00:00 2001 From: JamesLinYJ <110664404+JamesLinYJ@users.noreply.github.com> Date: Mon, 9 Nov 2026 15:06:04 +0800 Subject: [PATCH] release: prepare v0.2.8 with Rust 1.99.1 --- .../Processes-broken.cfg | 4 + .../taskmgr-verify-processes/Processes.cfg | 4 + .../taskmgr-verify-processes/Processes.tla | 57 +++ .../skills/taskmgr-verify-processes/SKILL.md | 46 +++ .../skills/taskmgr-verify-processes/view.mjs | 7 + .../skills/taskmgr-verify-sampling/SKILL.md | 47 +++ .../Sampling-broken.cfg | 4 + .../taskmgr-verify-sampling/Sampling.cfg | 4 + .../taskmgr-verify-sampling/Sampling.tla | 72 ++++ .../skills/taskmgr-verify-sampling/view.mjs | 7 + .../skills/taskmgr-verify-services/SKILL.md | 46 +++ .../Services-broken.cfg | 4 + .../taskmgr-verify-services/Services.cfg | 4 + .../taskmgr-verify-services/Services.tla | 83 +++++ .../skills/taskmgr-verify-services/view.mjs | 7 + .../skills/taskmgr-verify-sessions/SKILL.md | 44 +++ .../Sessions-broken.cfg | 4 + .../taskmgr-verify-sessions/Sessions.cfg | 4 + .../taskmgr-verify-sessions/Sessions.tla | 44 +++ .../skills/taskmgr-verify-sessions/view.mjs | 7 + .../skills/taskmgr-verify-startup/SKILL.md | 48 +++ .../taskmgr-verify-startup/Startup-broken.cfg | 4 + .../skills/taskmgr-verify-startup/Startup.cfg | 4 + .../skills/taskmgr-verify-startup/Startup.tla | 58 +++ .../skills/taskmgr-verify-startup/view.mjs | 7 + .agents/skills/taskmgr-verify-worker/SKILL.md | 45 +++ .../taskmgr-verify-worker/Worker-broken.cfg | 4 + .../skills/taskmgr-verify-worker/Worker.cfg | 4 + .../skills/taskmgr-verify-worker/Worker.tla | 47 +++ .agents/skills/taskmgr-verify-worker/view.mjs | 7 + .github/workflows/ci.yml | 10 +- .github/workflows/release.yml | 15 +- Cargo.lock | 2 +- Cargo.toml | 2 +- README.md | 6 + README.zh-CN.md | 4 + docs/compatibility-matrix.md | 31 ++ localization/de.toml | 1 + localization/en_us.toml | 1 + localization/es.toml | 1 + localization/fr.toml | 1 + localization/pt.toml | 1 + localization/ru.toml | 1 + localization/zh_cn.toml | 1 + localization/zh_tw.toml | 1 + rust-toolchain.toml | 2 +- src/{app/mod.rs => app.rs} | 2 +- src/{config/mod.rs => config.rs} | 2 +- .../mod.rs => infrastructure.rs} | 2 +- .../{diagnostics/mod.rs => diagnostics.rs} | 8 +- .../{native/mod.rs => native.rs} | 2 +- src/{pages/mod.rs => pages.rs} | 2 +- .../{applications/mod.rs => applications.rs} | 333 +++++++++++------- src/pages/{cpu/mod.rs => cpu.rs} | 2 +- src/pages/{gpu/mod.rs => gpu.rs} | 2 +- .../{performance/mod.rs => performance.rs} | 2 +- src/pages/{processes/mod.rs => processes.rs} | 2 +- src/pages/{services/mod.rs => services.rs} | 2 +- src/pages/{startup/mod.rs => startup.rs} | 2 +- src/{system/mod.rs => system.rs} | 2 +- src/{ui/mod.rs => ui.rs} | 2 +- .../{localization/mod.rs => localization.rs} | 13 +- src/ui/localization/text_key.rs | 1 + verification/.gitignore | 3 + verification/README.md | 27 ++ verification/formal/TOOLCHAIN.md | 15 + .../applications/Applications-broken.cfg | 4 + .../formal/applications/Applications.cfg | 4 + .../formal/applications/Applications.tla | 81 +++++ verification/formal/applications/README.md | 20 ++ .../history/ApplicationsLegacy-broken.cfg | 4 + .../history/ApplicationsLegacy.cfg | 4 + .../history/ApplicationsLegacy.tla | 50 +++ .../formal/applications/history/README.md | 1 + .../applications/history/legacy-view.mjs | 7 + verification/formal/applications/view.mjs | 7 + verification/formal/models.json | 186 ++++++++++ verification/formal/source_probe.py | 286 +++++++++++++++ verification/formal/verify.py | 130 +++++++ 79 files changed, 1865 insertions(+), 152 deletions(-) create mode 100644 .agents/skills/taskmgr-verify-processes/Processes-broken.cfg create mode 100644 .agents/skills/taskmgr-verify-processes/Processes.cfg create mode 100644 .agents/skills/taskmgr-verify-processes/Processes.tla create mode 100644 .agents/skills/taskmgr-verify-processes/SKILL.md create mode 100644 .agents/skills/taskmgr-verify-processes/view.mjs create mode 100644 .agents/skills/taskmgr-verify-sampling/SKILL.md create mode 100644 .agents/skills/taskmgr-verify-sampling/Sampling-broken.cfg create mode 100644 .agents/skills/taskmgr-verify-sampling/Sampling.cfg create mode 100644 .agents/skills/taskmgr-verify-sampling/Sampling.tla create mode 100644 .agents/skills/taskmgr-verify-sampling/view.mjs create mode 100644 .agents/skills/taskmgr-verify-services/SKILL.md create mode 100644 .agents/skills/taskmgr-verify-services/Services-broken.cfg create mode 100644 .agents/skills/taskmgr-verify-services/Services.cfg create mode 100644 .agents/skills/taskmgr-verify-services/Services.tla create mode 100644 .agents/skills/taskmgr-verify-services/view.mjs create mode 100644 .agents/skills/taskmgr-verify-sessions/SKILL.md create mode 100644 .agents/skills/taskmgr-verify-sessions/Sessions-broken.cfg create mode 100644 .agents/skills/taskmgr-verify-sessions/Sessions.cfg create mode 100644 .agents/skills/taskmgr-verify-sessions/Sessions.tla create mode 100644 .agents/skills/taskmgr-verify-sessions/view.mjs create mode 100644 .agents/skills/taskmgr-verify-startup/SKILL.md create mode 100644 .agents/skills/taskmgr-verify-startup/Startup-broken.cfg create mode 100644 .agents/skills/taskmgr-verify-startup/Startup.cfg create mode 100644 .agents/skills/taskmgr-verify-startup/Startup.tla create mode 100644 .agents/skills/taskmgr-verify-startup/view.mjs create mode 100644 .agents/skills/taskmgr-verify-worker/SKILL.md create mode 100644 .agents/skills/taskmgr-verify-worker/Worker-broken.cfg create mode 100644 .agents/skills/taskmgr-verify-worker/Worker.cfg create mode 100644 .agents/skills/taskmgr-verify-worker/Worker.tla create mode 100644 .agents/skills/taskmgr-verify-worker/view.mjs rename src/{app/mod.rs => app.rs} (99%) rename src/{config/mod.rs => config.rs} (90%) rename src/{infrastructure/mod.rs => infrastructure.rs} (90%) rename src/infrastructure/{diagnostics/mod.rs => diagnostics.rs} (99%) rename src/infrastructure/{native/mod.rs => native.rs} (96%) rename src/{pages/mod.rs => pages.rs} (93%) rename src/pages/{applications/mod.rs => applications.rs} (87%) rename src/pages/{cpu/mod.rs => cpu.rs} (99%) rename src/pages/{gpu/mod.rs => gpu.rs} (99%) rename src/pages/{performance/mod.rs => performance.rs} (99%) rename src/pages/{processes/mod.rs => processes.rs} (99%) rename src/pages/{services/mod.rs => services.rs} (99%) rename src/pages/{startup/mod.rs => startup.rs} (99%) rename src/{system/mod.rs => system.rs} (93%) rename src/{ui/mod.rs => ui.rs} (94%) rename src/ui/{localization/mod.rs => localization.rs} (93%) create mode 100644 verification/.gitignore create mode 100644 verification/README.md create mode 100644 verification/formal/TOOLCHAIN.md create mode 100644 verification/formal/applications/Applications-broken.cfg create mode 100644 verification/formal/applications/Applications.cfg create mode 100644 verification/formal/applications/Applications.tla create mode 100644 verification/formal/applications/README.md create mode 100644 verification/formal/applications/history/ApplicationsLegacy-broken.cfg create mode 100644 verification/formal/applications/history/ApplicationsLegacy.cfg create mode 100644 verification/formal/applications/history/ApplicationsLegacy.tla create mode 100644 verification/formal/applications/history/README.md create mode 100644 verification/formal/applications/history/legacy-view.mjs create mode 100644 verification/formal/applications/view.mjs create mode 100644 verification/formal/models.json create mode 100644 verification/formal/source_probe.py create mode 100644 verification/formal/verify.py diff --git a/.agents/skills/taskmgr-verify-processes/Processes-broken.cfg b/.agents/skills/taskmgr-verify-processes/Processes-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/.agents/skills/taskmgr-verify-processes/Processes-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-processes/Processes.cfg b/.agents/skills/taskmgr-verify-processes/Processes.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/.agents/skills/taskmgr-verify-processes/Processes.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-processes/Processes.tla b/.agents/skills/taskmgr-verify-processes/Processes.tla new file mode 100644 index 0000000..0ae4f7e --- /dev/null +++ b/.agents/skills/taskmgr-verify-processes/Processes.tla @@ -0,0 +1,57 @@ +---- MODULE Processes ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, generation, handle, applied +vars == <> + +Init == + /\ phase = "Selected" + /\ generation = 1 + /\ handle = 0 + /\ applied = 0 + +Confirm == + /\ phase = "Selected" + /\ phase' = ("Queued") + /\ UNCHANGED <> + +ReusePid == + /\ handle = 0 /\ generation = 1 /\ phase \in {"Selected", "Queued"} + /\ generation' = (2) + /\ UNCHANGED <> + +OpenProcess == + /\ phase = "Queued" + /\ handle' = (generation) + /\ phase' = ("Opened") + /\ UNCHANGED <> + +CheckCreationTime == + /\ phase = "Opened" + /\ phase' = (IF Broken \/ handle = 1 THEN "Verified" ELSE "Failed") + /\ UNCHANGED <> + +Apply == + /\ phase = "Verified" + /\ phase' = ("Applied") + /\ applied' = (handle) + /\ UNCHANGED <> + +ApiFailure == + /\ phase = "Verified" + /\ phase' = ("Failed") + /\ UNCHANGED <> + +Close == + /\ phase \in {"Selected", "Queued"} + /\ phase' = ("Cancelled") + /\ UNCHANGED <> + +Done == + /\ phase \in {"Applied", "Failed", "Cancelled"} + /\ UNCHANGED <> + +Next == Confirm \/ ReusePid \/ OpenProcess \/ CheckCreationTime \/ Apply \/ ApiFailure \/ Close \/ Done + +Safety == applied # 2 +==== diff --git a/.agents/skills/taskmgr-verify-processes/SKILL.md b/.agents/skills/taskmgr-verify-processes/SKILL.md new file mode 100644 index 0000000..0569b2f --- /dev/null +++ b/.agents/skills/taskmgr-verify-processes/SKILL.md @@ -0,0 +1,46 @@ +--- +name: taskmgr-verify-processes +description: "检查 TaskManagerRust 结束进程：按创建时间核对，再使用同一已打开句柄的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。" +--- + +# 结束进程：按创建时间核对，再使用同一已打开句柄 + +保证：只有创建时间与保存身份匹配的进程句柄才会交给操作。 + +破坏后的用户影响：否则 PID 复用可能导致结束或修改另一个进程。 + +## 源码与模型对应 + +同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。 + +| 源码 | 模型边界 | +| --- | --- | +| `src/system/process_identity.rs` | open_process_for_identity | +| `src/pages/processes/action_worker.rs` | open_action_process / execute_end / execute_set_priority | +| `src/pages/processes/actions.rs` | apply_confirmed_affinity 的已验证句柄边界 | + +模型：`Processes.tla`；正常配置：`Processes.cfg`；负例配置：`Processes-broken.cfg`；中文视图：`view.mjs`。 + +## 运行 + +先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录： + +```sh +python3 verification/formal/verify.py processes --self-test +``` + +需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。 + +当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。 + +自检会在临时源码副本里跳过 open_process_for_identity 的创建时间比较。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。 + +对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。 + +## 范围与维护 + +一个 PID、两个创建时间、一个进程句柄、一次操作；依赖 Windows 句柄固定进程对象的语义。适用于 handle-based 操作，不证明进程树全体原子性、亲和性位宽运算或线程快照完整性。 + +TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。 + +遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。 diff --git a/.agents/skills/taskmgr-verify-processes/view.mjs b/.agents/skills/taskmgr-verify-processes/view.mjs new file mode 100644 index 0000000..ce2f185 --- /dev/null +++ b/.agents/skills/taskmgr-verify-processes/view.mjs @@ -0,0 +1,7 @@ +export const title = "结束进程 - 按创建时间核对, 再使用同一已打开句柄"; +const names = {"Selected": "选中进程并保存身份", "Queued": "确认操作，后台排队", "Opened": "打开目标的进程句柄", "Verified": "创建时间匹配，持有该句柄", "Applied": "操作已执行", "Failed": "目标变化或操作失败", "Cancelled": "操作未开始时关闭程序"}; +export const state = v => v.applied === 2 ? "误操作了复用后的进程" : v.phase === "Verified" && v.handle === 2 ? "身份检查被绕过，错误句柄被放行" : names[v.phase]; +const steps = {"Confirm": "确认结束进程", "ReusePid": "原进程退出，PID 被复用", "OpenProcess": "后台按 PID 打开进程", "CheckCreationTime": "比较保存与实际创建时间", "Apply": "使用核对后的同一进程句柄", "ApiFailure": "进程退出或系统调用失败", "Close": "关闭程序，取消尚未开始的请求", "Done": "保留执行结果"}; +export const step = a => steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/.agents/skills/taskmgr-verify-sampling/SKILL.md b/.agents/skills/taskmgr-verify-sampling/SKILL.md new file mode 100644 index 0000000..a123249 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sampling/SKILL.md @@ -0,0 +1,47 @@ +--- +name: taskmgr-verify-sampling +description: "检查 TaskManagerRust 性能采样：缺失或无效数据不得画成真实零值的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。" +--- + +# 性能采样：缺失或无效数据不得画成真实零值 + +保证：缺失容量、无效间隔或失败读数不能成为新增的真实零值历史点。 + +破坏后的用户影响：否则图表会把未知或失败伪装成资源空闲。 + +## 源码与模型对应 + +同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。 + +| 源码 | 模型边界 | +| --- | --- | +| `src/pages/gpu.rs` | record_memory_history / memory_percentage | +| `src/pages/performance.rs` | apply_system_sample 的内存容量与历史门控 | +| `src/pages/cpu.rs` | apply_system_sample 对 invalid delta 的历史与 stale 决策 | +| `src/system/disk.rs` | 零间隔成功读取仅推进基线，不发布速率 | + +模型：`Sampling.tla`；正常配置：`Sampling.cfg`；负例配置：`Sampling-broken.cfg`；中文视图：`view.mjs`。 + +## 运行 + +先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录： + +```sh +python3 verification/formal/verify.py sampling --self-test +``` + +需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。 + +当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。 + +自检会在临时源码副本里删除 record_memory_history 的缺失或零容量门控。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。 + +对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。 + +## 范围与维护 + +一次发布决策、四种来源、一个既有历史点。CPU valid 标志与原生计数器计算视为输入；磁盘仅抽象零间隔分支；不证明 Win32 采样数值准确或所有溢出算术。 + +TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。 + +遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。 diff --git a/.agents/skills/taskmgr-verify-sampling/Sampling-broken.cfg b/.agents/skills/taskmgr-verify-sampling/Sampling-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sampling/Sampling-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-sampling/Sampling.cfg b/.agents/skills/taskmgr-verify-sampling/Sampling.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sampling/Sampling.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-sampling/Sampling.tla b/.agents/skills/taskmgr-verify-sampling/Sampling.tla new file mode 100644 index 0000000..3506402 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sampling/Sampling.tla @@ -0,0 +1,72 @@ +---- MODULE Sampling ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, kind, eligible, history +vars == <> + +Init == + /\ phase = "Ready" + /\ kind = "none" + /\ eligible = FALSE + /\ history = 1 + +ChooseCpu == + /\ phase = "Ready" + /\ phase' = ("Sampling") + /\ kind' = ("cpu") + /\ UNCHANGED <> + +ChooseMemory == + /\ phase = "Ready" + /\ phase' = ("Sampling") + /\ kind' = ("memory") + /\ UNCHANGED <> + +ChooseGpu == + /\ phase = "Ready" + /\ phase' = ("Sampling") + /\ kind' = ("gpu") + /\ UNCHANGED <> + +ChooseDisk == + /\ phase = "Ready" + /\ phase' = ("Sampling") + /\ kind' = ("disk") + /\ UNCHANGED <> + +ValidSample == + /\ phase = "Sampling" + /\ phase' = ("Candidate") + /\ eligible' = (TRUE) + /\ UNCHANGED <> + +MissingOrInvalid == + /\ phase = "Sampling" + /\ phase' = ("Candidate") + /\ eligible' = (FALSE) + /\ UNCHANGED <> + +Publish == + /\ phase = "Candidate" /\ (eligible \/ (Broken /\ kind = "gpu")) + /\ phase' = ("Fresh") + /\ history' = (history + 1) + /\ UNCHANGED <> + +ZeroDiskInterval == + /\ phase = "Sampling" /\ kind = "disk" + /\ phase' = ("BaselineOnly") + /\ UNCHANGED <> + +RetainHistory == + /\ phase = "Candidate" /\ ~eligible /\ ~(Broken /\ kind = "gpu") + /\ phase' = ("Stale") + /\ UNCHANGED <> + +Done == + /\ phase \in {"Fresh", "Stale", "BaselineOnly"} + /\ UNCHANGED <> + +Next == ChooseCpu \/ ChooseMemory \/ ChooseGpu \/ ChooseDisk \/ ValidSample \/ MissingOrInvalid \/ Publish \/ ZeroDiskInterval \/ RetainHistory \/ Done + +Safety == history > 1 => eligible +==== diff --git a/.agents/skills/taskmgr-verify-sampling/view.mjs b/.agents/skills/taskmgr-verify-sampling/view.mjs new file mode 100644 index 0000000..5caa463 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sampling/view.mjs @@ -0,0 +1,7 @@ +export const title = "性能采样 - 缺失或无效数据不得画成真实零值"; +const names = {"Ready": "保留上一轮可信曲线", "Sampling": "后台读取性能数据", "Candidate": "检查数据有效性", "Fresh": "追加真实采样点，包括真实零值", "Stale": "保持旧曲线，显示未知或未刷新", "BaselineOnly": "零间隔磁盘采样仅推进基线"}; +export const state = v => v.history > 1 && !v.eligible ? "未知容量被画成真实零值" : names[v.phase]; +const steps = {"ChooseCpu": "采样 CPU", "ChooseMemory": "采样物理内存", "ChooseGpu": "采样 GPU 显存", "ChooseDisk": "采样磁盘", "ValidSample": "读数及计算前提有效", "MissingOrInvalid": "数据缺失、容量未知或间隔无效", "Publish": "追加本次历史点", "ZeroDiskInterval": "磁盘读取成功但间隔为零，仅推进基线", "RetainHistory": "不追加伪造的零值", "Done": "等待下一次采样"}; +export const step = a => steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/.agents/skills/taskmgr-verify-services/SKILL.md b/.agents/skills/taskmgr-verify-services/SKILL.md new file mode 100644 index 0000000..dde7db5 --- /dev/null +++ b/.agents/skills/taskmgr-verify-services/SKILL.md @@ -0,0 +1,46 @@ +--- +name: taskmgr-verify-services +description: "检查 TaskManagerRust 服务重启：只有完成停止后才允许启动的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。" +--- + +# 服务重启：只有完成停止后才允许启动 + +保证：重启成功必须经过确认停止和发起启动两个阶段。 + +破坏后的用户影响：否则旧的 Running 状态会掩盖没有完成的重启。 + +## 源码与模型对应 + +同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。 + +| 源码 | 模型边界 | +| --- | --- | +| `src/pages/services/model.rs` | restart_after_stop / stop_has_completed / classify_control_result | +| `src/pages/services/sampler.rs` | restart_open_service / poll_service_stop | +| `src/pages/services.rs` | start_worker | + +模型：`Services.tla`；正常配置：`Services.cfg`；负例配置：`Services-broken.cfg`；中文视图：`view.mjs`。 + +## 运行 + +先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录： + +```sh +python3 verification/formal/verify.py services --self-test +``` + +需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。 + +当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。 + +自检会在临时源码副本里把 restart_after_stop 的非停止分支改成 Ok(state)。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。 + +对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。 + +## 范围与维护 + +一个服务、一次重启、最多两个未停止观察。ticks 是有限观察预算，不是 30 秒时钟证明；SCM 调用可能阻塞、开始/关闭的跨线程竞争不在成功判定性质内。 + +TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。 + +遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。 diff --git a/.agents/skills/taskmgr-verify-services/Services-broken.cfg b/.agents/skills/taskmgr-verify-services/Services-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/.agents/skills/taskmgr-verify-services/Services-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-services/Services.cfg b/.agents/skills/taskmgr-verify-services/Services.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/.agents/skills/taskmgr-verify-services/Services.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-services/Services.tla b/.agents/skills/taskmgr-verify-services/Services.tla new file mode 100644 index 0000000..8b3043f --- /dev/null +++ b/.agents/skills/taskmgr-verify-services/Services.tla @@ -0,0 +1,83 @@ +---- MODULE Services ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, stopped, started, ticks +vars == <> + +Init == + /\ phase = "Selected" + /\ stopped = FALSE + /\ started = FALSE + /\ ticks = 0 + +Confirm == + /\ phase = "Selected" + /\ phase' = ("Stopping") + /\ UNCHANGED <> + +RejectControl == + /\ phase = "Stopping" + /\ phase' = ("Failed") + /\ UNCHANGED <> + +AcceptStop == + /\ phase = "Stopping" + /\ phase' = ("Waiting") + /\ UNCHANGED <> + +ObserveOldRunning == + /\ phase = "Waiting" /\ ticks < 2 + /\ ticks' = (ticks + 1) + /\ phase' = (IF Broken THEN "Success" ELSE "Waiting") + /\ UNCHANGED <> + +Progress == + /\ phase = "Waiting" /\ ticks < 2 + /\ ticks' = (ticks + 1) + /\ UNCHANGED <> + +ObserveStopped == + /\ phase = "Waiting" + /\ phase' = ("Stopped") + /\ stopped' = (TRUE) + /\ UNCHANGED <> + +Timeout == + /\ phase = "Waiting" /\ ticks = 2 + /\ phase' = ("Failed") + /\ UNCHANGED <> + +QueryFailure == + /\ phase = "Waiting" + /\ phase' = ("Failed") + /\ UNCHANGED <> + +Cancel == + /\ phase \in {"Stopping", "Waiting", "Stopped"} + /\ phase' = ("Cancelled") + /\ UNCHANGED <> + +Start == + /\ phase = "Stopped" + /\ phase' = ("Starting") + /\ started' = (TRUE) + /\ UNCHANGED <> + +StartAccepted == + /\ phase = "Starting" + /\ phase' = ("Success") + /\ UNCHANGED <> + +StartFailed == + /\ phase = "Starting" + /\ phase' = ("Failed") + /\ UNCHANGED <> + +Done == + /\ phase \in {"Success", "Failed", "Cancelled"} + /\ UNCHANGED <> + +Next == Confirm \/ RejectControl \/ AcceptStop \/ ObserveOldRunning \/ Progress \/ ObserveStopped \/ Timeout \/ QueryFailure \/ Cancel \/ Start \/ StartAccepted \/ StartFailed \/ Done + +Safety == (started => stopped) /\ (phase = "Success" => (stopped /\ started)) +==== diff --git a/.agents/skills/taskmgr-verify-services/view.mjs b/.agents/skills/taskmgr-verify-services/view.mjs new file mode 100644 index 0000000..08799ac --- /dev/null +++ b/.agents/skills/taskmgr-verify-services/view.mjs @@ -0,0 +1,7 @@ +export const title = "服务重启 - 只有完成停止后才允许启动"; +const names = {"Selected": "选中可重启的服务", "Stopping": "提交停止命令", "Waiting": "等待停止，跟踪进度", "Stopped": "已确认服务停止", "Starting": "提交启动命令", "Success": "启动已接受，等待刷新", "Failed": "操作失败或等待超时", "Cancelled": "关闭程序，中止后续启动"}; +export const state = v => v.phase === "Success" && (!v.stopped || !v.started) ? "未启动却报告重启成功" : names[v.phase]; +const steps = {"Confirm": "点击重启", "RejectControl": "停止命令失败", "AcceptStop": "停止命令已接受", "ObserveOldRunning": "查询仍返回旧的运行状态", "Progress": "服务报告停止进度", "ObserveStopped": "查询确认已停止", "Timeout": "停止等待达到上限", "QueryFailure": "状态查询失败", "Cancel": "关闭程序，取消等待", "Start": "发送启动命令", "StartAccepted": "查询为运行中或启动中", "StartFailed": "启动失败或状态不符", "Done": "保留操作结果"}; +export const step = a => steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/.agents/skills/taskmgr-verify-sessions/SKILL.md b/.agents/skills/taskmgr-verify-sessions/SKILL.md new file mode 100644 index 0000000..4e34b37 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sessions/SKILL.md @@ -0,0 +1,44 @@ +--- +name: taskmgr-verify-sessions +description: "检查 TaskManagerRust 用户会话：消息逐次保留，注销和断开去重的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。" +--- + +# 用户会话：消息逐次保留，注销和断开去重 + +保证：每次确认发送的消息都保留，只有重复注销或断开可以合并。 + +破坏后的用户影响：否则发往同一会话的第二条消息可能无提示地丢失。 + +## 源码与模型对应 + +同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。 + +| 源码 | 模型边界 | +| --- | --- | +| `src/pages/users.rs` | merge_user_requests / session_action_already_queued / queue_session_action；execute_session_command 的终结边界 | + +模型：`Sessions.tla`；正常配置：`Sessions.cfg`；负例配置：`Sessions-broken.cfg`；中文视图：`view.mjs`。 + +## 运行 + +先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录： + +```sh +python3 verification/formal/verify.py sessions --self-test +``` + +需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。 + +当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。 + +自检会在临时源码副本里删除 SendMessage 不参与去重的条件。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。 + +对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。 + +## 范围与维护 + +同一会话两条独立确认的消息及一次重复破坏性命令；核对身份/执行/报告被抽象为命令终结，性质只验证消息保留，不证明 WTS 身份核对与调用之间的原子性。 + +TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。 + +遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。 diff --git a/.agents/skills/taskmgr-verify-sessions/Sessions-broken.cfg b/.agents/skills/taskmgr-verify-sessions/Sessions-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sessions/Sessions-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-sessions/Sessions.cfg b/.agents/skills/taskmgr-verify-sessions/Sessions.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/.agents/skills/taskmgr-verify-sessions/Sessions.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-sessions/Sessions.tla b/.agents/skills/taskmgr-verify-sessions/Sessions.tla new file mode 100644 index 0000000..62486af --- /dev/null +++ b/.agents/skills/taskmgr-verify-sessions/Sessions.tla @@ -0,0 +1,44 @@ +---- MODULE Sessions ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, submitted, queue, reported, disconnect +vars == <> + +Init == + /\ phase = "Ready" + /\ submitted = 0 + /\ queue = <<>> + /\ reported = <<>> + /\ disconnect = FALSE + +SendMessage == + /\ submitted < 2 + /\ submitted' = (submitted + 1) + /\ queue' = (IF Broken /\ Len(queue) > 0 THEN queue ELSE Append(queue, submitted + 1)) + /\ phase' = ("Queued") + /\ UNCHANGED <> + +QueueDisconnect == + /\ ~disconnect + /\ disconnect' = (TRUE) + /\ UNCHANGED <> + +RepeatDisconnect == + /\ disconnect + /\ UNCHANGED <> + +ReportMessage == + /\ Len(queue) > 0 + /\ reported' = (Append(reported, Head(queue))) + /\ queue' = (Tail(queue)) + /\ phase' = (IF Len(queue) = 1 THEN "Done" ELSE "Queued") + /\ UNCHANGED <> + +Done == + /\ submitted = 2 /\ Len(queue) = 0 + /\ UNCHANGED <> + +Next == SendMessage \/ QueueDisconnect \/ RepeatDisconnect \/ ReportMessage \/ Done + +Safety == reported \o queue = SubSeq(<<1, 2>>, 1, submitted) +==== diff --git a/.agents/skills/taskmgr-verify-sessions/view.mjs b/.agents/skills/taskmgr-verify-sessions/view.mjs new file mode 100644 index 0000000..bf3377c --- /dev/null +++ b/.agents/skills/taskmgr-verify-sessions/view.mjs @@ -0,0 +1,7 @@ +export const title = "用户会话 - 消息逐次保留, 注销和断开去重"; +const names = {"Ready": "选择用户会话", "Queued": "消息已接受，等待逐次处理", "Done": "已逐条完成或报告失败"}; +export const state = v => Object.keys(v.queue).length + Object.keys(v.reported).length < v.submitted ? "已确认消息被静默丢弃" : names[v.phase]; +const steps = {"SendMessage": "确认发送一条消息", "QueueDisconnect": "接受注销或断开命令", "RepeatDisconnect": "重复注销或断开被合并", "ReportMessage": "核对会话并执行，或报告失败", "Done": "等待后续用户操作"}; +export const step = a => steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/.agents/skills/taskmgr-verify-startup/SKILL.md b/.agents/skills/taskmgr-verify-startup/SKILL.md new file mode 100644 index 0000000..f43aeba --- /dev/null +++ b/.agents/skills/taskmgr-verify-startup/SKILL.md @@ -0,0 +1,48 @@ +--- +name: taskmgr-verify-startup +description: "检查 TaskManagerRust 启动项修改后退出：处理已接受的修改再结束进程的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。" +--- + +# 启动项修改后退出：处理已接受的修改再结束进程 + +保证：正常退出前，按顺序处理每一个已经接受的启动项修改。 + +破坏后的用户影响：否则窗口关闭会静默丢失用户已经提交的设置。 + +## 源码与模型对应 + +同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。 + +| 源码 | 模型边界 | +| --- | --- | +| `src/infrastructure/worker.rs` | defer_drain_until_exit / into_exit_drain / drain_before_process_exit | +| `src/main.rs` | main 中 UI 返回到进程退出的顺序 | +| `src/pages/startup.rs` | destroy / submit | +| `src/pages/startup/model.rs` | merge_startup_requests | +| `src/pages/startup/sampler.rs` | perform 的顺序处理 | + +模型：`Startup.tla`；正常配置：`Startup.cfg`；负例配置：`Startup-broken.cfg`；中文视图：`view.mjs`。 + +## 运行 + +先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录： + +```sh +python3 verification/formal/verify.py startup --self-test +``` + +需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。 + +当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。 + +自检会在临时源码副本里从 main 删除 drain_before_process_exit 调用。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。 + +对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。 + +## 范围与维护 + +最多两次已接受修改，FIFO；修改失败也算已处理并留下失败结果。假设 collector 不 panic、线程可启动、系统 API 最终返回；不承诺每个写入成功或强制关机时持久化。 + +TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。 + +遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。 diff --git a/.agents/skills/taskmgr-verify-startup/Startup-broken.cfg b/.agents/skills/taskmgr-verify-startup/Startup-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/.agents/skills/taskmgr-verify-startup/Startup-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-startup/Startup.cfg b/.agents/skills/taskmgr-verify-startup/Startup.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/.agents/skills/taskmgr-verify-startup/Startup.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-startup/Startup.tla b/.agents/skills/taskmgr-verify-startup/Startup.tla new file mode 100644 index 0000000..22cace9 --- /dev/null +++ b/.agents/skills/taskmgr-verify-startup/Startup.tla @@ -0,0 +1,58 @@ +---- MODULE Startup ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, accepted, queue, current, finished +vars == <> + +Init == + /\ phase = "Open" + /\ accepted = 0 + /\ queue = <<>> + /\ current = 0 + /\ finished = <<>> + +AcceptToggle == + /\ phase = "Open" /\ accepted < 2 + /\ accepted' = (accepted + 1) + /\ queue' = (Append(queue, accepted + 1)) + /\ UNCHANGED <> + +Refresh == + /\ phase = "Open" + /\ UNCHANGED <> + +BeginWrite == + /\ phase # "Exited" /\ current = 0 /\ Len(queue) > 0 + /\ current' = (Head(queue)) + /\ queue' = (Tail(queue)) + /\ UNCHANGED <> + +FinishWrite == + /\ current # 0 /\ phase # "Exited" + /\ current' = (0) + /\ finished' = (Append(finished, current)) + /\ UNCHANGED <> + +CloseWindow == + /\ phase = "Open" + /\ phase' = ("Closed") + /\ UNCHANGED <> + +DrainOnExit == + /\ phase = "Closed" + /\ phase' = ("Draining") + /\ UNCHANGED <> + +Exit == + /\ phase \in {"Closed", "Draining"} /\ (Broken \/ (phase = "Draining" /\ current = 0 /\ Len(queue) = 0)) + /\ phase' = ("Exited") + /\ UNCHANGED <> + +Done == + /\ phase = "Exited" + /\ UNCHANGED <> + +Next == AcceptToggle \/ Refresh \/ BeginWrite \/ FinishWrite \/ CloseWindow \/ DrainOnExit \/ Exit \/ Done + +Safety == (finished = SubSeq(<<1, 2>>, 1, Len(finished))) /\ (phase = "Exited" => finished = SubSeq(<<1, 2>>, 1, accepted)) +==== diff --git a/.agents/skills/taskmgr-verify-startup/view.mjs b/.agents/skills/taskmgr-verify-startup/view.mjs new file mode 100644 index 0000000..a74854e --- /dev/null +++ b/.agents/skills/taskmgr-verify-startup/view.mjs @@ -0,0 +1,7 @@ +export const title = "启动项修改后退出 - 处理已接受的修改再结束进程"; +const names = {"Open": "窗口可用，修改可排队", "Closed": "窗口关闭，已接受的修改仍保留", "Draining": "退出前处理剩余修改", "Exited": "修改处理完毕，进程退出"}; +export const state = v => v.phase === "Exited" && Object.keys(v.finished).length < v.accepted ? "进程提前退出，修改丢失" : v.phase === "Open" ? (v.accepted === 0 ? "启动项列表" : v.current !== 0 ? "后台正在修改启动项" : Object.keys(v.queue).length ? "修改已接受，等待执行" : "本轮修改已处理") : names[v.phase]; +const steps = {"AcceptToggle": "接受一次启用或禁用", "Refresh": "请求刷新，保留修改队列", "BeginWrite": "后台开始下一次修改", "FinishWrite": "完成修改或记录该次失败", "CloseWindow": "关闭窗口，停止向界面通知", "DrainOnExit": "开始退出前排空队列", "Exit": "全部已接受修改处理完才退出", "Done": "已退出"}; +export const step = (a, from, to) => a === "Exit" && Object.keys(to.finished).length < to.accepted ? "未处理完修改就直接退出" : steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/.agents/skills/taskmgr-verify-worker/SKILL.md b/.agents/skills/taskmgr-verify-worker/SKILL.md new file mode 100644 index 0000000..3c80c8b --- /dev/null +++ b/.agents/skills/taskmgr-verify-worker/SKILL.md @@ -0,0 +1,45 @@ +--- +name: taskmgr-verify-worker +description: "检查 TaskManagerRust 后台任务：关闭通知，再销毁窗口的有限状态性质；修改所列状态转换、队列或生命周期代码时使用。" +--- + +# 后台任务：关闭通知，再销毁窗口 + +保证：关闭通知入口后，不再向已销毁窗口发送新的完成通知。 + +破坏后的用户影响：否则 UI 消息可能到达过期或复用的 HWND。 + +## 源码与模型对应 + +同步提交：`7003888753316de6662996112f8e3100ee470208`（2026-11-09）。逐文件 SHA-256 记录在 `verification/formal/models.json`。 + +| 源码 | 模型边界 | +| --- | --- | +| `src/infrastructure/worker.rs` | WorkerStopSignal::close_notifications / notify；BackgroundWorker::drop | +| `src/app/page_host.rs` | DialogPage::destroy 显式销毁路径 | + +模型：`Worker.tla`；正常配置：`Worker.cfg`；负例配置：`Worker-broken.cfg`；中文视图：`view.mjs`。 + +## 运行 + +先跟随本技能目录的符号链接定位实际检出目录（同时含 `Cargo.toml` 和 `verification/formal/verify.py`），再从该仓库根目录执行。不要误用外层工作区或其他旧检出目录： + +```sh +python3 verification/formal/verify.py worker --self-test +``` + +需要 Python 3.9+、Rust 1.99+、Java 11+ 和校验过 SHA-256 的 `tla2tools` 1.7.4。工具查找顺序为 `--jar`、`TLA2TOOLS`、`verification/.tools/tla2tools-1.7.4.jar`。工具哈希、来源和首次准备方法见 `verification/formal/TOOLCHAIN.md`。输出自动放到新的系统临时目录，也可以用 `--out` 指定仓库外的新目录。 + +当前模型和真实源码重放应通过。自检中的 TLA+ 与 Rust 负例必须失败；这两种预期失败不是当前代码失败。 + +自检会在临时源码副本里把 close_notifications 的 closed 赋值改为 false。它编译实际 Rust 函数体，验证断言确实失败，然后用未改动源码重新运行。它不修改产品代码。Win32 边界是受控替身；worker 重放用标准库单消费者有界通道替代 crossbeam，保留实际 worker 算法，不能外推为两种通道完全等价的证明。 + +对每次 TLA+ 结果使用 `/statechart`：通过时展示状态转换，失败时解释最短反例。读取当前安装的 `/statechart` 技能，不在这里固定其命令或安装路径；在仓库外复制模型、配置和 `view.mjs` 后运行它。 + +## 范围与维护 + +一个页面、一个后台任务、一次关闭；通知检查与 PostMessage 同处互斥锁。只验证已封闭通知之后不会调用 PostMessage，不验证已排队消息的 HWND 复用。 + +TLC 穷尽的是这个有限模型，不是整个 Rust 程序。API 原子性、调度公平性和环境动作只能按源码中实际边界建模；不要把“检查后再调用”合并成一步。未检查无界活性或真实设备行为。 + +遇到 `SOURCE DRIFT` 先比对本表函数与模型，判断是预期设计改变还是回归；不要仅刷新哈希让检查变绿。预期改变时同步状态、动作、性质和真实源码重放，保留负例敏感性，再更新同步提交和哈希。非预期失败保留反例，报告源码中的事件顺序，不弱化性质。产品修复需按当前用户任务授权处理。后续维护可使用 `/maintain-formal-verification-skill`。 diff --git a/.agents/skills/taskmgr-verify-worker/Worker-broken.cfg b/.agents/skills/taskmgr-verify-worker/Worker-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/.agents/skills/taskmgr-verify-worker/Worker-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-worker/Worker.cfg b/.agents/skills/taskmgr-verify-worker/Worker.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/.agents/skills/taskmgr-verify-worker/Worker.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/.agents/skills/taskmgr-verify-worker/Worker.tla b/.agents/skills/taskmgr-verify-worker/Worker.tla new file mode 100644 index 0000000..9081864 --- /dev/null +++ b/.agents/skills/taskmgr-verify-worker/Worker.tla @@ -0,0 +1,47 @@ +---- MODULE Worker ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, gate, work, late +vars == <> + +Init == + /\ phase = "Open" + /\ gate = TRUE + /\ work = "idle" + /\ late = FALSE + +Submit == + /\ phase = "Open" /\ work = "idle" + /\ work' = ("running") + /\ UNCHANGED <> + +Complete == + /\ work = "running" + /\ work' = ("ready") + /\ UNCHANGED <> + +Notify == + /\ work = "ready" + /\ work' = ("notified") + /\ late' = (late \/ (gate /\ phase = "Gone")) + /\ UNCHANGED <> + +Retire == + /\ phase = "Open" + /\ phase' = ("Retired") + /\ gate' = (IF Broken THEN gate ELSE FALSE) + /\ UNCHANGED <> + +DestroyWindow == + /\ phase = "Retired" + /\ phase' = ("Gone") + /\ UNCHANGED <> + +Done == + /\ phase = "Gone" /\ work \in {"idle", "notified"} + /\ UNCHANGED <> + +Next == Submit \/ Complete \/ Notify \/ Retire \/ DestroyWindow \/ Done + +Safety == ~late +==== diff --git a/.agents/skills/taskmgr-verify-worker/view.mjs b/.agents/skills/taskmgr-verify-worker/view.mjs new file mode 100644 index 0000000..b5e3b24 --- /dev/null +++ b/.agents/skills/taskmgr-verify-worker/view.mjs @@ -0,0 +1,7 @@ +export const title = "后台任务 - 关闭通知, 再销毁窗口"; +const names = {"Open": "页面可用", "Retired": "通知已关闭", "Gone": "页面已销毁"}; +export const state = v => v.late ? "窗口销毁后仍收到通知" : ((v.phase !== "Open" && v.gate ? (v.phase === "Gone" ? "页面已销毁但通知入口仍开放" : "页面已退休但通知入口未关闭") : names[v.phase]) + " - " + ({idle:"无任务", running:"任务执行中", ready:"结果待通知", notified:"通知已处理"}[v.work])); +const steps = {"Submit": "提交后台任务", "Complete": "任务完成", "Notify": "尝试发送完成通知", "Retire": "关闭页面，封闭通知入口", "DestroyWindow": "销毁窗口", "Done": "退出完成"}; +export const step = a => steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 591e3d1..2e8283f 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -53,7 +53,10 @@ jobs: id: toolchain run: | rustup set profile minimal - rustup toolchain install stable ` + $channel = Select-String -Path rust-toolchain.toml -Pattern '^\s*channel\s*=\s*"([^"]+)"' + if ($null -eq $channel) { throw 'rust-toolchain.toml has no channel' } + $toolchain = $channel.Matches[0].Groups[1].Value + rustup toolchain install $toolchain ` --component rustfmt ` --component clippy ` --target x86_64-pc-windows-msvc @@ -138,7 +141,10 @@ jobs: id: toolchain run: | rustup set profile minimal - rustup toolchain install stable ` + $channel = Select-String -Path rust-toolchain.toml -Pattern '^\s*channel\s*=\s*"([^"]+)"' + if ($null -eq $channel) { throw 'rust-toolchain.toml has no channel' } + $toolchain = $channel.Matches[0].Groups[1].Value + rustup toolchain install $toolchain ` --component clippy ` --target '${{ matrix.target }}' rustup show active-toolchain diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 42621d3..08c51eb 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -64,7 +64,10 @@ jobs: - name: Install Rust toolchain run: | rustup set profile minimal - rustup toolchain install stable --profile minimal + $channel = Select-String -Path rust-toolchain.toml -Pattern '^\s*channel\s*=\s*"([^"]+)"' + if ($null -eq $channel) { throw 'rust-toolchain.toml has no channel' } + $toolchain = $channel.Matches[0].Groups[1].Value + rustup toolchain install $toolchain --profile minimal rustup show active-toolchain - name: Resolve or create release tag @@ -188,7 +191,10 @@ jobs: - name: Install Rust toolchain run: | rustup set profile minimal - rustup toolchain install stable --profile minimal + $channel = Select-String -Path rust-toolchain.toml -Pattern '^\s*channel\s*=\s*"([^"]+)"' + if ($null -eq $channel) { throw 'rust-toolchain.toml has no channel' } + $toolchain = $channel.Matches[0].Groups[1].Value + rustup toolchain install $toolchain --profile minimal rustup show active-toolchain - name: Validate tag and package version @@ -254,7 +260,10 @@ jobs: id: toolchain run: | rustup set profile minimal - rustup toolchain install stable ` + $channel = Select-String -Path rust-toolchain.toml -Pattern '^\s*channel\s*=\s*"([^"]+)"' + if ($null -eq $channel) { throw 'rust-toolchain.toml has no channel' } + $toolchain = $channel.Matches[0].Groups[1].Value + rustup toolchain install $toolchain ` --target '${{ matrix.target }}' rustup show active-toolchain $commit = @( diff --git a/Cargo.lock b/Cargo.lock index 8e3ad27..22ae7e9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -295,7 +295,7 @@ dependencies = [ [[package]] name = "taskmgr-rs" -version = "0.2.7" +version = "0.2.8" dependencies = [ "crc32fast", "crossbeam-channel", diff --git a/Cargo.toml b/Cargo.toml index c729865..bf12aab 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,7 +2,7 @@ # 这里定义包名、版本、发布构建策略，以及 Win32 API 绑定所需的功能开关。 [package] name = "taskmgr-rs" -version = "0.2.7" +version = "0.2.8" authors = ["taskmgr-rs contributors"] description = "A classic Windows Task Manager built in Rust with native Win32 APIs." license = "MIT" diff --git a/README.md b/README.md index a4145bb..428053d 100644 --- a/README.md +++ b/README.md @@ -19,6 +19,12 @@ This is not a copy of the modern Task Manager. CPU and GPU details come from sys - **Services** lists Win32 services with description, status, startup type, and the owning process. Start, stop, pause, continue, and Go to Process run only when the current row allows them. Go to Process requires a process id plus creation time. - **Startup** lists Run-key and Startup-folder apps with name, publisher or command, location, and enabled state. Enable and disable write the StartupApproved value and report a failure immediately when the entry is missing or the new state cannot be read back. Entries are not deleted. +On the Applications page, every **End Task** action asks for confirmation, then terminates +all selected applications' processes, including their other windows. Unsaved data will be lost; +the applications are not asked to save first. The button, context menu and Delete shortcut use +the same behavior. Holding Ctrl does not bypass confirmation. Cancelling leaves the processes +running. Targets are captured before the confirmation dialog and checked again before termination. + ## Download The current build is on the [Releases page](https://github.com/JamesLinYJ/taskmgr-rs/releases/latest): diff --git a/README.zh-CN.md b/README.zh-CN.md index 34bd1d1..e430c30 100644 --- a/README.zh-CN.md +++ b/README.zh-CN.md @@ -19,6 +19,10 @@ - **服务**：列出 Win32 服务的名称、描述、状态、启动类型和所属进程。启动、停止、暂停、继续和转到进程只在当前行允许时可用。转到进程同时要求进程 ID 和创建时间。 - **启动**：列出 Run 键和“启动”文件夹中的项目，显示名称、发布者或命令、位置和启用状态。启用和禁用只写入 StartupApproved；项目缺失或读回的状态与请求不一致时会立刻报错，不会删除原项。 +应用程序页每次“结束任务”都会先确认，确认后终止选中应用所属的整个进程，包括该进程的其他窗口。 +应用不会再弹出保存提示，未保存的数据会丢失。按钮、右键菜单和 Delete 快捷键行为一致，按住 Ctrl 也不会跳过确认；取消确认不会结束进程。 +操作目标在确认框出现前保存，执行时重新核对身份，确认期间选择变化不会换成另一个目标。 + ## 下载 最新版本在 [Releases](https://github.com/JamesLinYJ/taskmgr-rs/releases/latest)： diff --git a/docs/compatibility-matrix.md b/docs/compatibility-matrix.md index 0ca6958..6861818 100644 --- a/docs/compatibility-matrix.md +++ b/docs/compatibility-matrix.md @@ -53,6 +53,37 @@ Toolchain: Rust 1.98.1 stable; MSVC 14.51.36231; Windows SDK 10.0.26100.0. Exist slice loops were changed to `as_chunks` to satisfy the repository's current stable Clippy gate; no dependencies or registry configuration schema were changed. +## Targeted module-layout and application-action validation — 2026-11-09 + +Windows 11 Insider **29698.1000** in the Parallels ARM64 VM; Rust 1.99.0. +Source: `7003888753316de6662996112f8e3100ee470208` plus the working-tree module migration +and application-action changes. All 16 `mod.rs` files were moved to same-named `.rs` files. +The VM source copy was checked against the host Rust source files with SHA-256 before testing. + +| Target | Automated checks | Tests | +| --- | --- | --- | +| ARM64 | fmt, all-target check, strict Clippy, all-target tests, release build passed | 442 passed, 5 ignored | +| x86-64 under emulation | Same checks passed | 442 passed, 5 ignored | +| x86 under emulation | Same checks passed | 441 passed, 5 ignored | + +The final implementation unifies every Applications End Task entry point behind explicit +confirmation and termination through a retained process handle verified by creation time. +There is no normal-close or Ctrl-only variant, and no SC_CLOSE sink in this action path. +Cancelling submits nothing; targets are captured before the dialog; same-process windows are +deduplicated by complete identity within each request; failures preserve later requests. + +Controlled native tests reject unknown/mismatched process identities and terminate only an +owned test child through the shared default action, even without a usable HWND. Confirmation, +selection changes, queue order, deduplication and partial failures have regression coverage. +The ignored count includes the child fixture launched explicitly by its parent regression test. + +The previous HWND-close counterexample is retained as historical evidence. The current model +still permits window reuse, but termination uses only the saved process identity and the same +verified handle. Model and actual-function replay now pass; removing the creation-time guard +makes both fail. These are automated VM results, not a complete manual UI checklist, +stable-Windows coverage or physical-device acceptance. See +[formal verification](../verification/README.md) for bounds and reproduction commands. + ## GPU and driver coverage | Date | Windows build / arch | Vendor and adapter | Driver | GPU Engine | Dedicated usage | Shared usage | Metadata / temperature | UI | Status | diff --git a/localization/de.toml b/localization/de.toml index c2fe8cc..5766596 100644 --- a/localization/de.toml +++ b/localization/de.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "Das Beenden der Aufgaben beendet die Prozesse aller ausgewählten Anwendungen einschließlich ihrer anderen Fenster. Nicht gespeicherte Daten gehen verloren. Fortfahren?" AppTitle = "Windows NT Task-Manager" RunTitle = "Ausführen" RunPrompt = "Geben Sie den Namen eines Programms, Ordners, Dokuments oder einer Internetressource ein, und Windows wird es für Sie öffnen." diff --git a/localization/en_us.toml b/localization/en_us.toml index 69d8f59..9435430 100644 --- a/localization/en_us.toml +++ b/localization/en_us.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "Ending tasks will terminate the processes of all selected applications, including their other windows. Unsaved data will be lost. Continue?" AppTitle = "Windows NT Task Manager" RunTitle = "Run" RunPrompt = "Type the name of a program, folder, document, or Internet resource, and Windows will open it for you." diff --git a/localization/es.toml b/localization/es.toml index e0fe1f5..54a4d59 100644 --- a/localization/es.toml +++ b/localization/es.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "Finalizar las tareas terminará los procesos de todas las aplicaciones seleccionadas, incluidas sus otras ventanas. Se perderán los datos sin guardar. ¿Continuar?" AppTitle = "Administrador de tareas de Windows NT" RunTitle = "Ejecutar" RunPrompt = "Escriba el nombre de un programa, carpeta, documento o recurso de Internet, y Windows lo abrirá por usted." diff --git a/localization/fr.toml b/localization/fr.toml index b646759..67f2c3e 100644 --- a/localization/fr.toml +++ b/localization/fr.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "La fin des tâches terminera les processus de toutes les applications sélectionnées, y compris leurs autres fenêtres. Les données non enregistrées seront perdues. Continuer ?" AppTitle = "Gestionnaire des tâches Windows NT" RunTitle = "Exécuter" RunPrompt = "Tapez le nom d’un programme, dossier, document ou d’une ressource Internet, et Windows l’ouvrira pour vous." diff --git a/localization/pt.toml b/localization/pt.toml index 79d9e47..4ab3958 100644 --- a/localization/pt.toml +++ b/localization/pt.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "Terminar as tarefas encerrará os processos de todas as aplicações selecionadas, incluindo as outras janelas desses processos. Os dados não guardados serão perdidos. Continuar?" AppTitle = "Gerenciador de Tarefas do Windows NT" RunTitle = "Executar" RunPrompt = "Digite o nome de um programa, pasta, documento ou recurso da Internet, e o Windows o abrirá para você." diff --git a/localization/ru.toml b/localization/ru.toml index 52f9a57..8751f2e 100644 --- a/localization/ru.toml +++ b/localization/ru.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "Завершение задач остановит процессы всех выбранных приложений, включая другие окна этих процессов. Несохранённые данные будут потеряны. Продолжить?" AppTitle = "Диспетчер задач Windows NT" RunTitle = "Выполнить" RunPrompt = "Введите имя программы, папки, документа или интернет-ресурса, и Windows откроет его." diff --git a/localization/zh_cn.toml b/localization/zh_cn.toml index 18492a7..ad67eba 100644 --- a/localization/zh_cn.toml +++ b/localization/zh_cn.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "结束任务将终止所有选中应用所属的进程，包括这些进程的其他窗口。未保存的数据将丢失。是否继续？" AppTitle = "Windows NT 任务管理器" RunTitle = "运行" RunPrompt = "Windows 将根据你所输入的名称，为你打开相应的程序、文件夹、文档或 Internet 资源。" diff --git a/localization/zh_tw.toml b/localization/zh_tw.toml index 1dbb14c..cf22c9d 100644 --- a/localization/zh_tw.toml +++ b/localization/zh_tw.toml @@ -1,4 +1,5 @@ [text] +EndApplicationsWarning = "結束工作將終止所有選取應用程式所屬的處理程序，包括這些處理程序的其他視窗。未儲存的資料將遺失。是否繼續？" AppTitle = "Windows NT 工作管理員" RunTitle = "執行" RunPrompt = "Windows 將根據你所輸入的名稱，為你開啟相應的程式、資料夾、文件或 Internet 資源。" diff --git a/rust-toolchain.toml b/rust-toolchain.toml index ea1c18c..3f65b19 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,4 +1,4 @@ [toolchain] -channel = "stable" +channel = "1.99.1" components = ["rustfmt", "clippy"] targets = ["i686-pc-windows-msvc", "x86_64-pc-windows-msvc", "aarch64-pc-windows-msvc"] diff --git a/src/app/mod.rs b/src/app.rs similarity index 99% rename from src/app/mod.rs rename to src/app.rs index d23243b..0d8f134 100644 --- a/src/app/mod.rs +++ b/src/app.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 应用组合根 // -// 文件: src/app/mod.rs +// 文件: src/app.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/config/mod.rs b/src/config.rs similarity index 90% rename from src/config/mod.rs rename to src/config.rs index 4b62090..95bfdec 100644 --- a/src/config/mod.rs +++ b/src/config.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 配置模块入口 // -// 文件: src/config/mod.rs +// 文件: src/config.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/infrastructure/mod.rs b/src/infrastructure.rs similarity index 90% rename from src/infrastructure/mod.rs rename to src/infrastructure.rs index 4ff1d53..17d673a 100644 --- a/src/infrastructure/mod.rs +++ b/src/infrastructure.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 基础设施模块入口 // -// 文件: src/infrastructure/mod.rs +// 文件: src/infrastructure.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/infrastructure/diagnostics/mod.rs b/src/infrastructure/diagnostics.rs similarity index 99% rename from src/infrastructure/diagnostics/mod.rs rename to src/infrastructure/diagnostics.rs index b8575b3..5bf38fb 100644 --- a/src/infrastructure/diagnostics/mod.rs +++ b/src/infrastructure/diagnostics.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 结构化诊断日志 // -// 文件: src/infrastructure/diagnostics/mod.rs +// 文件: src/infrastructure/diagnostics.rs // // 日期: 2026年07月27日 // 环境: Fedora Linux 45 x86_64；Linux 内核 7.2.0-0.rc4.260725g0ce37745d4bf.39.fc45.x86_64；Rust 1.97.1；MinGW GCC 16.1.1；Wine 11.14 (Staging) @@ -866,7 +866,7 @@ fn report_dropped_events(shared: &SharedState, sink: &mut Option) { Field::unsigned("regular", regular), Field::unsigned("priority", priority), ], - "src/infrastructure/diagnostics/mod.rs", + "src/infrastructure/diagnostics.rs", line!(), ); write_record(shared, sink, record); @@ -3195,8 +3195,8 @@ mod tests { #[test] fn source_paths_do_not_expose_build_machine_prefixes() { assert_eq!( - normalized_source_path(r"C:\build\taskmgr-rs\src\app\mod.rs"), - "src/app/mod.rs" + normalized_source_path(r"C:\build\taskmgr-rs\src\app.rs"), + "src/app.rs" ); } diff --git a/src/infrastructure/native/mod.rs b/src/infrastructure/native.rs similarity index 96% rename from src/infrastructure/native/mod.rs rename to src/infrastructure/native.rs index b0eacae..dbf5489 100644 --- a/src/infrastructure/native/mod.rs +++ b/src/infrastructure/native.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 原生基础设施入口 // -// 文件: src/infrastructure/native/mod.rs +// 文件: src/infrastructure/native.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/pages/mod.rs b/src/pages.rs similarity index 93% rename from src/pages/mod.rs rename to src/pages.rs index 81079d0..02e3be4 100644 --- a/src/pages/mod.rs +++ b/src/pages.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 功能页面模块入口 // -// 文件: src/pages/mod.rs +// 文件: src/pages.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/pages/applications/mod.rs b/src/pages/applications.rs similarity index 87% rename from src/pages/applications/mod.rs rename to src/pages/applications.rs index f2a62e5..787ac6b 100644 --- a/src/pages/applications/mod.rs +++ b/src/pages/applications.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 应用程序页面 // -// 文件: src/pages/applications/mod.rs +// 文件: src/pages/applications.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex @@ -27,7 +27,7 @@ use std::collections::{HashMap, HashSet}; // // 线程模型： // 一个单飞 worker 枚举窗口，另一个单飞协调器驱动固定数量的长期图标线程。 -// 结束任务使用第三条长期单飞 worker：UI 线程只提交窗口身份，EndTask 在后台执行。 +// 结束任务使用第三条长期单飞 worker：统一确认后，使用已验证的进程句柄结束目标。 // UI 线程只提交请求和应用完整结果，采集失败不会覆盖上一轮可信列表。 // // 缓存失效策略： @@ -39,6 +39,9 @@ use std::ptr::{null, null_mut}; use windows_sys::Win32::Foundation::{ ERROR_INVALID_DATA, ERROR_RESOURCE_DATA_NOT_FOUND, HINSTANCE, HWND, LPARAM, RECT, }; +use windows_sys::Win32::System::Threading::{ + PROCESS_QUERY_LIMITED_INFORMATION, PROCESS_TERMINATE, TerminateProcess, +}; use windows_sys::Win32::UI::Controls::{ ImageList_GetImageCount, LVCF_FMT, LVCF_SUBITEM, LVCF_TEXT, LVCF_WIDTH, LVCFMT_LEFT, LVCOLUMNW, LVIF_IMAGE, LVIF_PARAM, LVIF_STATE, LVIF_TEXT, LVIS_FOCUSED, LVIS_SELECTED, LVITEMW, @@ -48,20 +51,17 @@ use windows_sys::Win32::UI::Controls::{ LVS_AUTOARRANGE, LVS_ICON, LVS_REPORT, LVS_SHOWSELALWAYS, LVS_SMALLICON, LVS_TYPEMASK, LVSIL_NORMAL, LVSIL_SMALL, NM_DBLCLK, NMHDR, NMLISTVIEW, NMLVDISPINFOW, }; -use windows_sys::Win32::UI::Input::KeyboardAndMouse::{ - EnableWindow, GetKeyState, SetFocus, VK_CONTROL, -}; +use windows_sys::Win32::UI::Input::KeyboardAndMouse::{EnableWindow, SetFocus}; use windows_sys::Win32::UI::WindowsAndMessaging::{ BeginDeferWindowPos, CascadeWindows, CheckMenuRadioItem, DeferWindowPos, DeleteMenu, DrawMenuBar, EnableMenuItem, EndDeferWindowPos, GetClientRect, GetDesktopWindow, GetDlgItem, - GetWindowLongW, GetWindowThreadProcessId, IsIconic, IsWindow, MB_ICONERROR, MB_OK, - MDITILE_HORIZONTAL, MDITILE_VERTICAL, MF_BYCOMMAND, MF_DISABLED, MF_GRAYED, MessageBoxW, - SW_MAXIMIZE, SW_MINIMIZE, SW_RESTORE, SWP_NOACTIVATE, SWP_NOMOVE, SWP_NOSIZE, SWP_NOZORDER, - SendMessageW, SetForegroundWindow, SetMenuDefaultItem, SetWindowLongW, SetWindowPos, - ShowWindow, ShowWindowAsync, TPM_RETURNCMD, TileWindows, TrackPopupMenuEx, WM_COMMAND, - WM_SETREDRAW, + GetWindowLongW, GetWindowThreadProcessId, IDYES, IsIconic, IsWindow, MB_DEFBUTTON2, + MB_ICONERROR, MB_ICONWARNING, MB_OK, MB_YESNO, MDITILE_HORIZONTAL, MDITILE_VERTICAL, + MF_BYCOMMAND, MF_DISABLED, MF_GRAYED, MessageBoxW, SW_MAXIMIZE, SW_MINIMIZE, SW_RESTORE, + SWP_NOACTIVATE, SWP_NOMOVE, SWP_NOSIZE, SWP_NOZORDER, SendMessageW, SetForegroundWindow, + SetMenuDefaultItem, SetWindowLongW, SetWindowPos, ShowWindow, ShowWindowAsync, TPM_RETURNCMD, + TileWindows, TrackPopupMenuEx, WM_COMMAND, WM_SETREDRAW, }; -use windows_sys::core::BOOL; use self::icons::{ TaskIconBatchRequest, TaskIconCompletion, TaskIconExecutor, TaskIconRequest, TaskIconResult, @@ -76,7 +76,8 @@ use crate::infrastructure::native::{ }; use crate::infrastructure::worker::{SingleFlightWorker, keep_pending}; use crate::system::process_identity::{ - FindProcPayload, ProcIdentity, find_proc_lparam, query_process_identity_for_pid, + FindProcPayload, ProcIdentity, find_proc_lparam, open_process_for_identity, + query_process_identity_for_pid, }; use crate::ui::localization::{TextKey, text}; use crate::ui::menus::build_popup_menu; @@ -98,12 +99,6 @@ const ACTIVE_COLUMNS: [TaskColumnId; 2] = [TaskColumnId::Name, TaskColumnId::Sta const DEFAULT_MARGIN: i32 = 8; const TEXT_CALLBACK_WIDE: *mut u16 = -1isize as *mut u16; -// 外部函数 EndTask（user32），用于强制结束指定窗口的任务。 -#[link(name = "user32")] -unsafe extern "system" { - fn EndTask(hwnd: HWND, shutdown: BOOL, force: BOOL) -> BOOL; -} - #[derive(Clone, Copy, PartialEq, Eq)] pub enum TaskColumnId { Name = 0, @@ -991,23 +986,34 @@ impl TaskPageState { } fn request_end_task(&mut self) { - // Ctrl is part of the click. GetKeyState reports this UI thread's message state, so the - // worker receives the flag instead of sampling the keyboard itself. - let force = unsafe { (GetKeyState(i32::from(VK_CONTROL)) & (1 << 15)) != 0 }; - let targets = self.selected_task_identities(true); - if targets.is_empty() { + let Some(request) = confirmed_end_task_request(self.selected_task_identities(true), || { + self.confirm_end_tasks() + }) else { return; - } - let request = vec![EndTaskRequest { targets, force }]; + }; let Some(worker) = self.end_task_worker.as_mut() else { self.report_end_task_failure(windows_sys::Win32::Foundation::ERROR_BROKEN_PIPE); return; }; - if let Err(error) = worker.request(request, self.hwnd_page) { + if let Err(error) = worker.request(vec![request], self.hwnd_page) { self.report_end_task_failure(error); } } + fn confirm_end_tasks(&self) -> bool { + let title = to_wide_null(text(TextKey::WarningTitle)); + let body = to_wide_null(text(TextKey::EndApplicationsWarning)); + // SAFETY: both strings outlive this synchronous call; the page HWND is borrowed. + unsafe { + MessageBoxW( + self.hwnd_page, + body.as_ptr(), + title.as_ptr(), + MB_YESNO | MB_ICONWARNING | MB_DEFBUTTON2, + ) == IDYES + } + } + fn drain_end_task_results(&mut self) { let drained = match self.end_task_worker.as_mut() { Some(worker) => worker.drain(self.hwnd_page), @@ -1090,8 +1096,8 @@ impl TaskPageState { )?); } if self.end_task_worker.is_none() { - // EndTask can block inside the target window's queue. Retire this worker without - // joining it on the UI thread; a destroyed page drops the completion instead. + // Retire without joining on the UI thread. Requests not yet started are + // cancelled; an in-flight operation finishes without notifying a destroyed page. self.end_task_worker = Some(SingleFlightWorker::spawn_cancellable_initialized( "taskmgr-rs-task-end", PWM_TASK_WORKER_COMPLETE, @@ -1539,41 +1545,55 @@ fn last_error_or_gen_failure() -> u32 { } struct EndTaskRequest { + // Never retain a window handle for termination: only a saved process incarnation. + targets: Vec, +} + +fn confirmed_end_task_request( targets: Vec, - force: bool, + confirm: impl FnOnce() -> bool, +) -> Option { + // Snapshot before the modal dialog; selection/refresh changes cannot retarget consent. + let targets: Vec<_> = targets.into_iter().map(|target| target.process).collect(); + if targets.is_empty() || !confirm() { + return None; + } + Some(EndTaskRequest { targets }) } fn queue_end_tasks(pending: &mut Vec, incoming: Vec) { - // An accepted End Task is not a refresh sample. Append it; do not replace an earlier command. + // Each accepted command is retained, including repeated confirmations for one process. pending.extend(incoming); } fn run_end_tasks(requests: Vec) -> Option { - run_end_task_queue(&requests, window_matches_identity, |hwnd, force| { - // SAFETY: `window_matches_identity` just accepted this HWND on this thread. EndTask - // does not retain the handle after it returns. - let ended = unsafe { EndTask(hwnd, 0, if force { 1 } else { 0 }) } != 0; - if ended { - Ok(()) - } else { - Err(last_error_or_gen_failure()) - } - }) + run_end_task_queue(&requests, terminate_task_process) } -fn run_end_task_queue( +fn terminate_task_process(identity: ProcIdentity) -> Result<(), u32> { + let handle = open_process_for_identity( + identity, + PROCESS_TERMINATE | PROCESS_QUERY_LIMITED_INFORMATION, + )?; + // SAFETY: this is the same owned process object whose creation time was checked. + // A closed/reused HWND cannot change the target, and there is no PID re-open here. + if unsafe { TerminateProcess(handle.as_raw(), 1) } == 0 { + Err(last_error_or_gen_failure()) + } else { + Ok(()) + } +} + +fn run_end_task_queue( requests: &[EndTaskRequest], - mut matches: Match, - mut end_task: End, + mut terminate_process: Terminate, ) -> Option where - Match: FnMut(TaskIdentity) -> bool, - End: FnMut(HWND, bool) -> Result<(), u32>, + Terminate: FnMut(ProcIdentity) -> Result<(), u32>, { let mut first_error = None; for request in requests { - let error = - end_matching_tasks(&request.targets, request.force, &mut matches, &mut end_task); + let error = end_task_processes(&request.targets, &mut terminate_process); if first_error.is_none() { first_error = error; } @@ -1581,24 +1601,21 @@ where first_error } -fn end_matching_tasks( - targets: &[TaskIdentity], - force: bool, - matches: &mut Match, - end_task: &mut End, +fn end_task_processes( + targets: &[ProcIdentity], + terminate_process: &mut Terminate, ) -> Option where - Match: FnMut(TaskIdentity) -> bool, - End: FnMut(HWND, bool) -> Result<(), u32>, + Terminate: FnMut(ProcIdentity) -> Result<(), u32>, { let mut first_error = None; + let mut processes = HashSet::new(); for identity in targets.iter().copied() { - // Re-check HWND, thread id, and ProcIdentity (pid + creation time) immediately before - // EndTask. An unknown or reused window is skipped and is not reported as success. - if !matches(identity) { + // Deduplicate only this request, by full identity rather than a recycled PID. + if !processes.insert(identity) { continue; } - if let Err(error) = end_task(identity.hwnd(), force) { + if let Err(error) = terminate_process(identity) { record_win32_error("ending task", error); first_error.get_or_insert(error); } @@ -1723,84 +1740,162 @@ mod tests { } #[test] - fn end_task_skips_a_mismatched_window_and_reports_only_the_first_failure() { - let skipped = TaskIdentity { + fn end_task_requires_confirmation_and_empty_selection_does_not_prompt() { + let identity = TaskIdentity { hwnd: 1, - process: ProcIdentity::pid_only(10), + process: ProcIdentity::new(10, 100), thread_id: 2, }; - let failed = TaskIdentity { - hwnd: 3, - process: ProcIdentity::new(11, 100), - thread_id: 4, - }; - let succeeded = TaskIdentity { - hwnd: 5, - process: ProcIdentity::new(12, 200), - thread_id: 6, - }; - let failed_again = TaskIdentity { - hwnd: 7, - process: ProcIdentity::new(13, 300), - thread_id: 8, - }; - let mut calls = Vec::new(); - let error = end_matching_tasks( - &[skipped, failed, succeeded, failed_again], - true, - &mut |identity: TaskIdentity| identity.process.is_verified(), - &mut |hwnd, force| { - calls.push((hwnd as isize, force)); - if hwnd as isize == failed.hwnd { - Err(5) - } else if hwnd as isize == failed_again.hwnd { - Err(9) - } else { - Ok(()) - } - }, + let mut prompts = 0; + assert!( + confirmed_end_task_request(vec![identity], || { + prompts += 1; + false + }) + .is_none() ); + assert_eq!(prompts, 1); + assert!( + confirmed_end_task_request(vec![], || panic!("empty selection prompted")).is_none() + ); + } + + #[test] + fn end_task_confirmation_keeps_original_process_when_window_or_selection_changes() { + let identity = TaskIdentity { + hwnd: 1, + process: ProcIdentity::new(10, 100), + thread_id: 2, + }; + let mut selection = vec![identity]; + let request = confirmed_end_task_request(selection.clone(), || { + selection = vec![TaskIdentity { + process: ProcIdentity::new(20, 200), + ..identity + }]; + true + }) + .unwrap(); + assert_eq!(request.targets, vec![identity.process]); + let mut terminated = Vec::new(); assert_eq!( - calls, - vec![ - (failed.hwnd, true), - (succeeded.hwnd, true), - (failed_again.hwnd, true) - ] + run_end_task_queue(&[request], |process| { + terminated.push(process); + Ok(()) + }), + None ); + assert_eq!(terminated, vec![identity.process]); + assert_ne!(terminated[0], selection[0].process); + } + + #[test] + fn end_task_deduplicates_only_exact_process_matches_and_continues_after_failure() { + let identity = ProcIdentity::new(10, 100); + let later = ProcIdentity::new(10, 200); + let mut calls = Vec::new(); + let error = end_task_processes(&[identity, identity, later], &mut |process| { + calls.push(process); + Err(if process == identity { 5 } else { 87 }) + }); + assert_eq!(calls, vec![identity, later]); assert_eq!(error, Some(5)); } #[test] fn pending_end_task_commands_run_in_submission_order() { - let command = |hwnd: isize, force: bool| EndTaskRequest { - targets: vec![TaskIdentity { - hwnd, - process: ProcIdentity::new(10, 100), - thread_id: 2, - }], - force, + let command = |pid| EndTaskRequest { + targets: vec![ProcIdentity::new(pid, 100)], }; - let mut pending = vec![command(1, false)]; - queue_end_tasks(&mut pending, vec![command(2, true)]); - queue_end_tasks(&mut pending, vec![command(3, false)]); - + let mut pending = vec![command(1)]; + queue_end_tasks(&mut pending, vec![command(2)]); + queue_end_tasks(&mut pending, vec![command(3), command(2)]); let mut calls = Vec::new(); - let error = run_end_task_queue(&pending, |_| true, &mut |hwnd, force| { - calls.push((hwnd as isize, force)); - if hwnd as isize == 2 { - Err(5) - } else if hwnd as isize == 3 { - Err(9) - } else { - Ok(()) + let error = run_end_task_queue(&pending, |process| { + calls.push(process.pid); + match process.pid { + 2 => Err(5), + 3 => Err(9), + _ => Ok(()), } }); - - assert_eq!(calls, vec![(1, false), (2, true), (3, false)]); + assert_eq!(calls, vec![1, 2, 3, 2]); assert_eq!(error, Some(5)); } + #[test] + #[ignore = "controlled child process, launched by the termination regression test"] + fn application_termination_fixture() { + if std::env::var_os("TASKMGR_TERMINATION_FIXTURE").is_none() { + return; + } + use std::io::Write; + println!("TASKMGR_TERMINATION_FIXTURE_READY"); + std::io::stdout().flush().unwrap(); + std::thread::sleep(std::time::Duration::from_secs(30)); + } + + #[test] + fn native_end_task_rejects_wrong_identity_and_terminates_only_owned_fixture() { + use std::io::{BufRead, BufReader}; + use std::process::{Child, Command, Stdio}; + struct OwnedChild(Child); + impl Drop for OwnedChild { + fn drop(&mut self) { + let _ = self.0.kill(); + let _ = self.0.wait(); + } + } + let mut child = OwnedChild( + Command::new(std::env::current_exe().unwrap()) + .args([ + "--ignored", + "--exact", + "pages::applications::tests::application_termination_fixture", + "--nocapture", + ]) + .env("TASKMGR_TERMINATION_FIXTURE", "1") + .stdout(Stdio::piped()) + .spawn() + .unwrap(), + ); + let mut output = BufReader::new(child.0.stdout.take().unwrap()); + loop { + let mut line = String::new(); + assert_ne!( + output.read_line(&mut line).unwrap(), + 0, + "fixture exited before readiness" + ); + if line.contains("TASKMGR_TERMINATION_FIXTURE_READY") { + break; + } + } + let identity = query_process_identity_for_pid(child.0.id()).unwrap(); + let task = |process| TaskIdentity { + hwnd: -1, + thread_id: 0, + process, + }; + let command = |process| confirmed_end_task_request(vec![task(process)], || true).unwrap(); + assert!(confirmed_end_task_request(vec![task(identity)], || false).is_none()); + assert!(child.0.try_wait().unwrap().is_none()); + assert!(run_end_tasks(vec![command(ProcIdentity::pid_only(identity.pid))]).is_some()); + assert!( + run_end_tasks(vec![command(ProcIdentity::new( + identity.pid, + identity.creation_time_100ns + 1 + ))]) + .is_some() + ); + assert!(child.0.try_wait().unwrap().is_none()); + // No usable HWND is available. The shared default action must still target only + // the originally selected process, using the verified process-handle boundary. + assert_eq!(run_end_tasks(vec![command(identity)]), None); + let status = child.0.wait().unwrap(); + assert_eq!(status.code(), Some(1)); + } + #[test] fn unverified_process_identity_is_never_actionable() { let identity = TaskIdentity { diff --git a/src/pages/cpu/mod.rs b/src/pages/cpu.rs similarity index 99% rename from src/pages/cpu/mod.rs rename to src/pages/cpu.rs index a8b395d..758a48a 100644 --- a/src/pages/cpu/mod.rs +++ b/src/pages/cpu.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - CPU 诊断页面 // -// 文件: src/pages/cpu/mod.rs +// 文件: src/pages/cpu.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/pages/gpu/mod.rs b/src/pages/gpu.rs similarity index 99% rename from src/pages/gpu/mod.rs rename to src/pages/gpu.rs index 26557ea..b29cfa7 100644 --- a/src/pages/gpu/mod.rs +++ b/src/pages/gpu.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - GPU 性能页面 // -// 文件: src/pages/gpu/mod.rs +// 文件: src/pages/gpu.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/pages/performance/mod.rs b/src/pages/performance.rs similarity index 99% rename from src/pages/performance/mod.rs rename to src/pages/performance.rs index 0cde4ff..ff6b09d 100644 --- a/src/pages/performance/mod.rs +++ b/src/pages/performance.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 性能页面 // -// 文件: src/pages/performance/mod.rs +// 文件: src/pages/performance.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/pages/processes/mod.rs b/src/pages/processes.rs similarity index 99% rename from src/pages/processes/mod.rs rename to src/pages/processes.rs index 9d27136..ff09ff5 100644 --- a/src/pages/processes/mod.rs +++ b/src/pages/processes.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 进程页面 // -// 文件: src/pages/processes/mod.rs +// 文件: src/pages/processes.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/pages/services/mod.rs b/src/pages/services.rs similarity index 99% rename from src/pages/services/mod.rs rename to src/pages/services.rs index 6707c09..ff0a755 100644 --- a/src/pages/services/mod.rs +++ b/src/pages/services.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 服务页面 // -// 文件: src/pages/services/mod.rs +// 文件: src/pages/services.rs // // 日期: 2026年10月19日 // 环境: Linux 6.12.94+ x86_64；Rust 1.99.1 diff --git a/src/pages/startup/mod.rs b/src/pages/startup.rs similarity index 99% rename from src/pages/startup/mod.rs rename to src/pages/startup.rs index 3b8368a..07b899e 100644 --- a/src/pages/startup/mod.rs +++ b/src/pages/startup.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 启动项页面 // -// 文件: src/pages/startup/mod.rs +// 文件: src/pages/startup.rs // // 日期: 2026年10月20日 // 环境: Linux 6.12.94+ x86_64；Rust 1.99.1 diff --git a/src/system/mod.rs b/src/system.rs similarity index 93% rename from src/system/mod.rs rename to src/system.rs index e28e9f3..5451373 100644 --- a/src/system/mod.rs +++ b/src/system.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 系统采样模块入口 // -// 文件: src/system/mod.rs +// 文件: src/system.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/ui/mod.rs b/src/ui.rs similarity index 94% rename from src/ui/mod.rs rename to src/ui.rs index 4aede86..9d11d5a 100644 --- a/src/ui/mod.rs +++ b/src/ui.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 共享 UI 基础模块入口 // -// 文件: src/ui/mod.rs +// 文件: src/ui.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex diff --git a/src/ui/localization/mod.rs b/src/ui/localization.rs similarity index 93% rename from src/ui/localization/mod.rs rename to src/ui/localization.rs index d64a8a0..8ae0b2b 100644 --- a/src/ui/localization/mod.rs +++ b/src/ui/localization.rs @@ -2,7 +2,7 @@ // // taskmgr-rs - 本地化入口 // -// 文件: src/ui/localization/mod.rs +// 文件: src/ui/localization.rs // // 日期: 2026年07月19日 // 作者: OpenAI Codex @@ -16,19 +16,16 @@ use std::sync::OnceLock; use windows_sys::Win32::Globalization::GetUserDefaultUILanguage; -#[path = "terms.rs"] -mod language_terms; -#[path = "ui.rs"] -mod language_ui; -#[path = "text_key.rs"] +mod terms; mod text_key; +mod ui; -pub use language_terms::{ +pub use terms::{ adapter_state, network_column_titles, service_column_titles, session_state, startup_column_titles, user_column_titles, user_session_column_title, }; -pub use language_ui::localize_dialog; pub use text_key::TextKey; +pub use ui::localize_dialog; const LANG_CHINESE: u16 = 0x04; const LANG_GERMAN: u16 = 0x07; diff --git a/src/ui/localization/text_key.rs b/src/ui/localization/text_key.rs index 8fa7147..ba0eeca 100644 --- a/src/ui/localization/text_key.rs +++ b/src/ui/localization/text_key.rs @@ -30,6 +30,7 @@ pub enum TextKey { WarningTitle, PriorityChangeWarning, KillProcessWarning, + EndApplicationsWarning, DebugProcessWarning, InvalidOptionTitle, NoAffinityMaskMessage, diff --git a/verification/.gitignore b/verification/.gitignore new file mode 100644 index 0000000..81d26da --- /dev/null +++ b/verification/.gitignore @@ -0,0 +1,3 @@ +.tools/ +__pycache__/ +formal/__pycache__/ diff --git a/verification/README.md b/verification/README.md new file mode 100644 index 0000000..745eaab --- /dev/null +++ b/verification/README.md @@ -0,0 +1,27 @@ +# 有限状态验证 + +六个项目技能位于 `.agents/skills/taskmgr-verify-*`。应用程序检查是普通仓库验证文件，位于 `verification/formal/applications/`，不注册为技能。各项包含 TLA+ 模型、当前与负例配置、中文视图及源码对应说明。 + +| 检查名称 | 检查性质 | 当前结果 | +| --- | --- | --- | +| `worker` | 关闭通知入口后不再发送新的窗口通知 | 通过 | +| `services` | 重启成功之前已经确认停止并发起启动 | 通过 | +| `startup` | 正常退出前按顺序处理已经接受的修改 | 通过 | +| `sessions` | 独立消息逐次保留，重复注销和断开可合并 | 通过 | +| `processes` | 创建时间匹配的进程句柄才交给操作 | 通过 | +| `applications` | 确认后只终止保存身份对应的同一已验证进程对象 | 通过 | +| `sampling` | 缺失或无效读数不成为新的真实零值历史点 | 通过 | + +基线为 `7003888753316de6662996112f8e3100ee470208` 加 2026-11-09 工作区修改。16 个 mod.rs 已迁移到同名 .rs；五个覆盖模块仅头部路径变化。Applications 已统一为确认后通过已验证进程句柄终止，共六个技能和一项独立验证、七项当前检查。这是有限模型检查和真实 Rust 函数的受控重放，不是完整 Windows 程序证明。逐项边界见对应验证说明；工具版本与来源见 [工具链说明](formal/TOOLCHAIN.md)。 + +从包含 `Cargo.toml` 的仓库根目录运行： + +```sh +python3 verification/formal/verify.py all --self-test +``` + +可把 `all` 换成表中的检查名称。结果写入新的临时目录，或通过 `--out` 指定仓库外的新目录。当前完整检查退出码为 **0**。原普通窗口关闭路径已删除；旧 HWND 反例模型保留在 `formal/applications/history/` 中，仅作为历史证据，不计为当前通过性质。旧目标“安全发送窗口关闭消息”因用户要求彻底修复竞态，改为“确认后仅终止保存身份对应的进程”；新模型继续允许窗口复用，执行路径不再读取窗口身份。产品语义变更见 README 和 `confirmed_end_task_request` 的测试。 + +`--self-test` 编译实际 Rust 函数，以受控 Win32 边界重放关键路径；随后在临时源码副本和模型中引入负例，确认失败，再重跑原始版本。它不会修改产品源码。worker 重放使用标准库单消费者有界通道替身，不证明其与 crossbeam 的所有行为等价。 + +运行器首先检查覆盖源码的 SHA-256。出现 `SOURCE DRIFT` 时先核对实现和模型，不能只刷新哈希。每次结果按对应验证说明使用 `/statechart` 绘图；覆盖源码变化后可用 `/maintain-formal-verification-skill` 同步验证。 diff --git a/verification/formal/TOOLCHAIN.md b/verification/formal/TOOLCHAIN.md new file mode 100644 index 0000000..4eb0b73 --- /dev/null +++ b/verification/formal/TOOLCHAIN.md @@ -0,0 +1,15 @@ +# Formal verification toolchain + +- TLC: `tla2tools` release **1.7.4** (TLC reports **2.19**, revision `5a47802`). +- Download: https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar +- SHA-256: `936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88`. +- Put the downloaded file at `verification/.tools/tla2tools-1.7.4.jar` (ignored by Git), or pass `--jar`, or set `TLA2TOOLS`. +- Java 11+; this run uses OpenJDK **25.0.4.1**. `JAVA` or `--java` selects the executable. +- Python 3.9+; this run uses **3.9.6**. Rust **1.99.0** compiles the actual-source replays without Cargo or network dependencies. +- `/statechart` produces the Mermaid statecharts. Read that installed skill to rerun; its invocation is deliberately not embedded in the project. +- Rendered SVGs use **Pele 1.9.0**, installed outside the repository. No product dependency changed. + +Run every subsystem with `python3 verification/formal/verify.py all --self-test`. +Exit **0** means all selected current properties hold; **1** means a current invariant violation was found; **2** means source drift, a broken harness, missing tools, or an incomplete check. In the recorded baseline, Applications is a current finding, so the full suite exits 1. It is never relabeled as a passing result. + +TLC may need permission to open a temporary local Java RMI socket even with one worker. A sandbox permission error is a tooling failure, not an invariant violation. Each run uses its own temporary directory to avoid shared Java module extraction races. diff --git a/verification/formal/applications/Applications-broken.cfg b/verification/formal/applications/Applications-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/verification/formal/applications/Applications-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/verification/formal/applications/Applications.cfg b/verification/formal/applications/Applications.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/verification/formal/applications/Applications.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/verification/formal/applications/Applications.tla b/verification/formal/applications/Applications.tla new file mode 100644 index 0000000..651e138 --- /dev/null +++ b/verification/formal/applications/Applications.tla @@ -0,0 +1,81 @@ +---- MODULE Applications ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, generation, handle, applied, confirmed, windowGeneration +vars == <> + +Init == + /\ phase = "Selected" + /\ generation = 1 + /\ handle = 0 + /\ applied = 0 + /\ confirmed = FALSE + /\ windowGeneration = 1 + +ShowWarning == + /\ phase = "Selected" + /\ phase' = "Confirming" + /\ UNCHANGED <> + +Confirm == + /\ phase = "Confirming" + /\ confirmed' = TRUE + /\ phase' = ("Queued") + /\ UNCHANGED <> + +ReusePid == + /\ handle = 0 /\ generation = 1 /\ phase \in {"Selected", "Confirming", "Queued"} + /\ generation' = (2) + /\ UNCHANGED <> + +OpenProcess == + /\ phase = "Queued" + /\ handle' = (generation) + /\ phase' = ("Opened") + /\ UNCHANGED <> + +CheckCreationTime == + /\ phase = "Opened" + /\ phase' = (IF Broken \/ handle = 1 THEN "Verified" ELSE "Failed") + /\ UNCHANGED <> + +Apply == + /\ phase = "Verified" + /\ phase' = ("Applied") + /\ applied' = (handle) + /\ UNCHANGED <> + +ApiFailure == + /\ phase = "Verified" + /\ phase' = ("Failed") + /\ UNCHANGED <> + +Close == + /\ phase \in {"Selected", "Confirming", "Queued"} + /\ phase' = ("Cancelled") + /\ UNCHANGED <> + +Done == + /\ phase \in {"Applied", "Failed", "Cancelled"} + /\ UNCHANGED <> + +RecycleWindow == + /\ windowGeneration = 1 + /\ phase \in {"Confirming", "Queued", "Opened", "Verified"} + /\ windowGeneration' = 2 + /\ UNCHANGED <> + +CancelConfirmation == + /\ phase = "Confirming" + /\ phase' = "Cancelled" + /\ UNCHANGED <> + +OpenFailure == + /\ phase = "Queued" + /\ phase' = "Failed" + /\ UNCHANGED <> + +Next == ShowWarning \/ RecycleWindow \/ CancelConfirmation \/ OpenFailure \/ Confirm \/ ReusePid \/ OpenProcess \/ CheckCreationTime \/ Apply \/ ApiFailure \/ Close \/ Done + +Safety == applied = 0 \/ (confirmed /\ applied = 1) +==== diff --git a/verification/formal/applications/README.md b/verification/formal/applications/README.md new file mode 100644 index 0000000..fc0d156 --- /dev/null +++ b/verification/formal/applications/README.md @@ -0,0 +1,20 @@ +# 应用程序结束任务验证 + +这是普通仓库验证资料，不是 agent 技能。 + +执行 `python3 verification/formal/verify.py applications --self-test`，预期退出 0。 +源码范围与逐文件 SHA-256 见上层 models.json；基线 7003888753316de6662996112f8e3100ee470208 加当前工作区修改。 + +## 性质与映射 + +用户确认后，仅终止选择时保存身份对应的进程对象。applications.rs 中 request_end_task 统一按钮、Delete 和上下文菜单；confirmed_end_task_request 先复制 ProcIdentity 再确认，取消不提交。EndTaskRequest 只保留进程身份；run_end_tasks、run_end_task_queue 和 end_task_processes 顺序执行并按每次请求完整身份去重。terminate_task_process 经 process_identity.rs 的 open_process_for_identity 核对创建时间后，使用同一 owned handle 终止。没有窗口关闭消息或 Ctrl 特殊分支。 + +模型 Applications.tla 描述一个保存身份、一个 PID 的两个创建时间、一个窗口的两个代际、一次确认和一个拥有句柄。窗口复用动作保留，但不参与终止目标选择。Windows 句柄固定进程对象是平台前提。队列多目标、具体 API 错误码和确认框视觉交互不由单目标模型全部证明。 + +实际源码重放包含确认、排队和终止函数；Win32 替身模拟未知身份、PID 复用、窗口更换目标、API 失败和验证后外部查找变化。自检在临时副本移除创建时间守卫，必须检测到断言失败，再恢复重跑。Windows 原生测试只终止自建测试子进程。程序退出可取消未开始请求，进行中操作完成后的通知由 worker gate 封闭。 + +## 变更与历史 + +旧承诺是“发送普通关闭消息时仍是原窗口”，确有检查与使用间隙。用户要求彻底修复后，产品改为每次确认后结束整个进程，允许失去应用保存提示。新承诺是“确认后只终止保存身份对应的进程”。旧路径已删除，旧模型位于 history/，不能计为当前代码结果。当前状态图输入为 Applications.tla、Applications.cfg、view.mjs；负例使用 Applications-broken.cfg。 + +源码变化后先核对模型和重放，再更新哈希；不能通过删除环境动作或仅刷新哈希制造通过。输出放到仓库外；工具版本见 ../TOOLCHAIN.md。这是有限模型及受控重放，不是整个程序或所有 Windows 版本的证明。 diff --git a/verification/formal/applications/history/ApplicationsLegacy-broken.cfg b/verification/formal/applications/history/ApplicationsLegacy-broken.cfg new file mode 100644 index 0000000..ad24ec8 --- /dev/null +++ b/verification/formal/applications/history/ApplicationsLegacy-broken.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = TRUE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/verification/formal/applications/history/ApplicationsLegacy.cfg b/verification/formal/applications/history/ApplicationsLegacy.cfg new file mode 100644 index 0000000..dfa34f7 --- /dev/null +++ b/verification/formal/applications/history/ApplicationsLegacy.cfg @@ -0,0 +1,4 @@ +CONSTANT Broken = FALSE +INIT Init +NEXT Next +INVARIANT Safety diff --git a/verification/formal/applications/history/ApplicationsLegacy.tla b/verification/formal/applications/history/ApplicationsLegacy.tla new file mode 100644 index 0000000..02d46d0 --- /dev/null +++ b/verification/formal/applications/history/ApplicationsLegacy.tla @@ -0,0 +1,50 @@ +---- MODULE ApplicationsLegacy ---- +EXTENDS Naturals, Sequences, FiniteSets +CONSTANT Broken +VARIABLES phase, generation, applied +vars == <> + +Init == + /\ phase = "Selected" + /\ generation = 1 + /\ applied = 0 + +Confirm == + /\ phase = "Selected" + /\ phase' = ("Queued") + /\ UNCHANGED <> + +RecycleBeforeCheck == + /\ phase = "Queued" /\ generation = 1 + /\ generation' = (2) + /\ UNCHANGED <> + +CheckIdentity == + /\ phase = "Queued" + /\ phase' = (IF Broken \/ generation = 1 THEN "Checked" ELSE "Skipped") + /\ UNCHANGED <> + +RecycleAfterCheck == + /\ phase = "Checked" /\ generation = 1 + /\ generation' = (2) + /\ UNCHANGED <> + +CloseWindow == + /\ phase = "Checked" + /\ phase' = ("Applied") + /\ applied' = (generation) + /\ UNCHANGED <> + +Close == + /\ phase = "Queued" + /\ phase' = ("Cancelled") + /\ UNCHANGED <> + +Done == + /\ phase \in {"Applied", "Skipped", "Cancelled"} + /\ UNCHANGED <> + +Next == Confirm \/ RecycleBeforeCheck \/ CheckIdentity \/ RecycleAfterCheck \/ CloseWindow \/ Close \/ Done + +Safety == applied # 2 +==== diff --git a/verification/formal/applications/history/README.md b/verification/formal/applications/history/README.md new file mode 100644 index 0000000..5032c1c --- /dev/null +++ b/verification/formal/applications/history/README.md @@ -0,0 +1 @@ +这是统一进程句柄结束任务之前的历史窗口关闭模型，当前代码不再执行此路径。保留用于解释已移除的检查到发送竞态，不能计入当前模型通过数。修复前真实函数反例已保留在验证交付包中。 diff --git a/verification/formal/applications/history/legacy-view.mjs b/verification/formal/applications/history/legacy-view.mjs new file mode 100644 index 0000000..a9db675 --- /dev/null +++ b/verification/formal/applications/history/legacy-view.mjs @@ -0,0 +1,7 @@ +export const title = "结束应用 - 检查窗口之后的复用间隙"; +const names = {"Selected": "选中应用窗口", "Queued": "确认结束任务，后台排队", "Checked": "窗口身份检查通过", "Skipped": "目标身份已变化，跳过", "Applied": "已发送关闭请求", "Cancelled": "操作尚未开始时关闭程序"}; +export const state = v => v.phase === "Applied" && v.applied === 2 ? "误操作了复用后的窗口" : (v.phase === "Checked" && v.generation === 2 ? "已进入调用阶段，窗口身份已变化" : names[v.phase]); +const steps = {"Confirm": "点击结束任务", "RecycleBeforeCheck": "窗口在检查前被复用", "CheckIdentity": "核对窗口、线程与进程身份", "RecycleAfterCheck": "检查返回后，窗口销毁并被复用", "CloseWindow": "按原 HWND 发送关闭消息", "Close": "关闭程序，取消尚未开始的请求", "Done": "处理结束"}; +export const step = (a, from, to) => a === "CheckIdentity" && from.generation === 2 && to.phase === "Checked" ? "身份不匹配仍放行" : steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/verification/formal/applications/view.mjs b/verification/formal/applications/view.mjs new file mode 100644 index 0000000..2fbcc79 --- /dev/null +++ b/verification/formal/applications/view.mjs @@ -0,0 +1,7 @@ +export const title = "结束应用进程 - 按创建时间核对, 再使用同一已打开句柄"; +const names = {"Selected": "选中应用并保存进程身份", "Confirming": "等待确认结束整个进程", "Queued": "确认操作，后台排队", "Opened": "打开目标的进程句柄", "Verified": "创建时间匹配，持有该句柄", "Applied": "操作已执行", "Failed": "目标变化或操作失败", "Cancelled": "操作已取消，目标未结束"}; +export const state = v => v.applied === 2 ? "误操作了复用后的进程" : v.phase === "Verified" && v.handle === 2 ? "身份检查被绕过，错误句柄被放行" : names[v.phase]; +const steps = {"ShowWarning": "提示整个进程结束及数据丢失", "CancelConfirmation": "取消确认", "OpenFailure": "打开进程失败", "RecycleWindow": "窗口已变化，保存的进程身份不变", "Confirm": "确认结束应用进程", "ReusePid": "原进程退出，PID 被复用", "OpenProcess": "后台按 PID 打开进程", "CheckCreationTime": "比较保存与实际创建时间", "Apply": "使用核对后的同一进程句柄", "ApiFailure": "进程退出或系统调用失败", "Close": "关闭程序，取消尚未开始的请求", "Done": "保留执行结果"}; +export const step = a => steps[a] ?? a; +export const group = v => ["Failed", "Cancelled", "Skipped", "Stale"].includes(v.phase) ? "失败或取消" : ["Success", "Exited", "Done", "Applied", "Fresh"].includes(v.phase) ? "处理完成" : "处理过程"; +export const colors = {"处理过程":"blue", "处理完成":"teal", "失败或取消":"orange"}; diff --git a/verification/formal/models.json b/verification/formal/models.json new file mode 100644 index 0000000..d2f5c1a --- /dev/null +++ b/verification/formal/models.json @@ -0,0 +1,186 @@ +{ + "worker": { + "module": "Worker", + "title": "后台任务：关闭通知，再销毁窗口", + "bounds": "一个页面、一个后台任务、一次关闭；通知检查与 PostMessage 同处互斥锁。只验证已封闭通知之后不会调用 PostMessage，不验证已排队消息的 HWND 复用。", + "expected_tlc_exit": 0, + "skill": ".agents/skills/taskmgr-verify-worker", + "sync_commit": "7003888753316de6662996112f8e3100ee470208", + "coverage": [ + { + "path": "src/infrastructure/worker.rs", + "symbols": "WorkerStopSignal::close_notifications / notify；BackgroundWorker::drop", + "sha256": "8a4b46553585b0207d079577940874d760e7a40fb25473969eef74c9cc30da85" + }, + { + "path": "src/app/page_host.rs", + "symbols": "DialogPage::destroy 显式销毁路径", + "sha256": "a518134e5c8fb5a031b98e7be3c8e248022ce63e966a8d6e5109c07d3263faf4" + } + ], + "property": "关闭通知入口后，不再向已销毁窗口发送新的完成通知。", + "sync_state": "7003888 + working-tree module migration and application fix (2026-11-09)" + }, + "services": { + "module": "Services", + "title": "服务重启：只有完成停止后才允许启动", + "bounds": "一个服务、一次重启、最多两个未停止观察。ticks 是有限观察预算，不是 30 秒时钟证明；SCM 调用可能阻塞、开始/关闭的跨线程竞争不在成功判定性质内。", + "expected_tlc_exit": 0, + "skill": ".agents/skills/taskmgr-verify-services", + "sync_commit": "7003888753316de6662996112f8e3100ee470208", + "coverage": [ + { + "path": "src/pages/services/model.rs", + "symbols": "restart_after_stop / stop_has_completed / classify_control_result", + "sha256": "eb87388571264d869c2eecf78b0c7ebdc30f72bce04c9dd52b80c41363322eea" + }, + { + "path": "src/pages/services/sampler.rs", + "symbols": "restart_open_service / poll_service_stop", + "sha256": "ac7b45431a0d84ec0a9c977b8da64b3375e082a3fc13bd482462447078d55a2c" + }, + { + "path": "src/pages/services.rs", + "symbols": "start_worker", + "sha256": "425232397e5cddb40f675ee1e628c732de8ea37239574af675162cc2fc1b0c5a" + } + ], + "property": "重启成功必须经过确认停止和发起启动两个阶段。", + "sync_state": "7003888 + working-tree module migration and application fix (2026-11-09)" + }, + "startup": { + "module": "Startup", + "title": "启动项修改后退出：处理已接受的修改再结束进程", + "bounds": "最多两次已接受修改，FIFO；修改失败也算已处理并留下失败结果。假设 collector 不 panic、线程可启动、系统 API 最终返回；不承诺每个写入成功或强制关机时持久化。", + "expected_tlc_exit": 0, + "skill": ".agents/skills/taskmgr-verify-startup", + "sync_commit": "7003888753316de6662996112f8e3100ee470208", + "coverage": [ + { + "path": "src/infrastructure/worker.rs", + "symbols": "defer_drain_until_exit / into_exit_drain / drain_before_process_exit", + "sha256": "8a4b46553585b0207d079577940874d760e7a40fb25473969eef74c9cc30da85" + }, + { + "path": "src/main.rs", + "symbols": "main 中 UI 返回到进程退出的顺序", + "sha256": "edf4e251f3592768b781f9d39d56480cf3c64efdeb232832e91831e31648adf4" + }, + { + "path": "src/pages/startup.rs", + "symbols": "destroy / submit", + "sha256": "75a4a855cec6eedd194b08419807eb196ef8919494c1c7dd41843499f6a69114" + }, + { + "path": "src/pages/startup/model.rs", + "symbols": "merge_startup_requests", + "sha256": "2351cf0110082405e63f0c413f9bc4415d21ade0c5454b34556f2bc6d974dfbe" + }, + { + "path": "src/pages/startup/sampler.rs", + "symbols": "perform 的顺序处理", + "sha256": "5a4d42c9c0849fb7043f167514a198f932820aab9b6aa66b7f9d4923a9c8ccba" + } + ], + "property": "正常退出前，按顺序处理每一个已经接受的启动项修改。", + "sync_state": "7003888 + working-tree module migration and application fix (2026-11-09)" + }, + "sessions": { + "module": "Sessions", + "title": "用户会话：消息逐次保留，注销和断开去重", + "bounds": "同一会话两条独立确认的消息及一次重复破坏性命令；核对身份/执行/报告被抽象为命令终结，性质只验证消息保留，不证明 WTS 身份核对与调用之间的原子性。", + "expected_tlc_exit": 0, + "skill": ".agents/skills/taskmgr-verify-sessions", + "sync_commit": "7003888753316de6662996112f8e3100ee470208", + "coverage": [ + { + "path": "src/pages/users.rs", + "symbols": "merge_user_requests / session_action_already_queued / queue_session_action；execute_session_command 的终结边界", + "sha256": "9a8676fa26e8e8ff5ca7d56854c7962b6512ddaf2a0dabf976176eb4e148e0ed" + } + ], + "property": "每次确认发送的消息都保留，只有重复注销或断开可以合并。", + "sync_state": "7003888 + working-tree module migration and application fix (2026-11-09)" + }, + "processes": { + "module": "Processes", + "title": "结束进程：按创建时间核对，再使用同一已打开句柄", + "bounds": "一个 PID、两个创建时间、一个进程句柄、一次操作；依赖 Windows 句柄固定进程对象的语义。适用于 handle-based 操作，不证明进程树全体原子性、亲和性位宽运算或线程快照完整性。", + "expected_tlc_exit": 0, + "skill": ".agents/skills/taskmgr-verify-processes", + "sync_commit": "7003888753316de6662996112f8e3100ee470208", + "coverage": [ + { + "path": "src/system/process_identity.rs", + "symbols": "open_process_for_identity", + "sha256": "bc9ada6295a9f44bd0ec3b41caa2e6968823acf69d8e77aeedfe9f0c61519bba" + }, + { + "path": "src/pages/processes/action_worker.rs", + "symbols": "open_action_process / execute_end / execute_set_priority", + "sha256": "62b8e4ef94352d7da69774c847f251f9cbe81ebe7e8cfd8c5aafebb9c984235d" + }, + { + "path": "src/pages/processes/actions.rs", + "symbols": "apply_confirmed_affinity 的已验证句柄边界", + "sha256": "079527e7e1e51c06e202b77f9817b09a4a5cad2239f9c679a4a0c9a0ebdfc985" + } + ], + "property": "只有创建时间与保存身份匹配的进程句柄才会交给操作。", + "sync_state": "7003888 + working-tree module migration and application fix (2026-11-09)" + }, + "applications": { + "module": "Applications", + "title": "结束应用：确认后用同一已验证进程句柄", + "bounds": "一个保存进程身份、一个 PID 的两个创建时间、一个窗口的两个代际、一次确认与一个持有句柄。窗口复用动作保留，但不参与选取终止目标。依赖 Windows 进程句柄固定对象；多目标聚合和具体错误码由源码重放与测试补充。", + "expected_tlc_exit": 0, + "sync_commit": "7003888753316de6662996112f8e3100ee470208", + "coverage": [ + { + "path": "src/pages/applications.rs", + "symbols": "confirmed_end_task_request / request_end_task / run_end_tasks / run_end_task_queue / end_task_processes / terminate_task_process", + "sha256": "6be73007933a934a99936ff494962aef85f340457b54652a6f1c227bc6894f06" + }, + { + "path": "src/system/process_identity.rs", + "symbols": "open_process_for_identity", + "sha256": "bc9ada6295a9f44bd0ec3b41caa2e6968823acf69d8e77aeedfe9f0c61519bba" + } + ], + "property": "只有明确确认后，才能终止与保存身份匹配的进程对象；窗口变化不得改变目标。", + "sync_state": "7003888 + working-tree module migration and unified confirmed process termination (2026-11-09)", + "model_dir": "verification/formal/applications" + }, + "sampling": { + "module": "Sampling", + "title": "性能采样：缺失或无效数据不得画成真实零值", + "bounds": "一次发布决策、四种来源、一个既有历史点。CPU valid 标志与原生计数器计算视为输入；磁盘仅抽象零间隔分支；不证明 Win32 采样数值准确或所有溢出算术。", + "expected_tlc_exit": 0, + "skill": ".agents/skills/taskmgr-verify-sampling", + "sync_commit": "7003888753316de6662996112f8e3100ee470208", + "coverage": [ + { + "path": "src/pages/gpu.rs", + "symbols": "record_memory_history / memory_percentage", + "sha256": "a0230f76729be09bae65518670aca31752814843253fbfa00de9315dad68c11c" + }, + { + "path": "src/pages/performance.rs", + "symbols": "apply_system_sample 的内存容量与历史门控", + "sha256": "832c915d6c6e01a87b31ee08414634971fcddeeca8fa20e3c8e1ee13b09657c9" + }, + { + "path": "src/pages/cpu.rs", + "symbols": "apply_system_sample 对 invalid delta 的历史与 stale 决策", + "sha256": "a361dce6334acf5f123575ac7bebf2d3c20c03aeca21d44511b64211dc5544d3" + }, + { + "path": "src/system/disk.rs", + "symbols": "零间隔成功读取仅推进基线，不发布速率", + "sha256": "0f1fe204a30b8496cad8ce0518c0e9474f1fccb9e2c46779f38f17a98f340f53" + } + ], + "property": "缺失容量、无效间隔或失败读数不能成为新增的真实零值历史点。", + "sync_state": "7003888 + working-tree module migration and application fix (2026-11-09)" + } +} diff --git a/verification/formal/source_probe.py b/verification/formal/source_probe.py new file mode 100644 index 0000000..0d6c6b3 --- /dev/null +++ b/verification/formal/source_probe.py @@ -0,0 +1,286 @@ +# +------------------------------------------------------------------------- +# Taskmgr Rust state-machine counterexample probes +# File: verification/formal/source_probe.py +# Date: 2026-11-09; environment: Darwin arm64, Python 3.9.6, Rust 1.99.0 +# Author: OpenAI Codex +# -------------------------------------------------------------------------- +"""Compile current Rust function bodies with explicit OS/channel boundary doubles. + +These are controlled replays, not a proof of Rust/Win32 refinement. Product sources +are read only; mutations are written into a separate source tree by verify.py. +""" +import re +from pathlib import Path + + +def item(source, marker): + match = re.search(marker, source) + if not match: + raise ValueError('Source anchor missing: '+marker) + start = source.index('{', match.start()) + depth = 1 + i = start + 1 + while depth: + if source.startswith('//', i): + i = source.find('\n', i) + if i < 0: raise ValueError('Unclosed item') + elif source.startswith('/*', i): + level=1; i+=2 + while level: + if source.startswith('/*',i): level+=1; i+=2 + elif source.startswith('*/',i): level-=1; i+=2 + else: i+=1 + elif source[i] == '"': + i+=1 + while source[i] != '"': + i += 2 if source[i] == '\\' else 1 + i+=1 + else: + if source[i]=='{': depth+=1 + if source[i]=='}': depth-=1 + i+=1 + return source[match.start():i].replace('pub(super)', 'pub(crate)') + + +def function(root, path, name): + return item((root/path).read_text(), r'(?:pub(?:\([^)]*\))?\s+)?(?:const\s+)?fn\s+'+name+r'\b') + + +def functions(root, path, names): + return '\n\n'.join(function(root,path,n) for n in names) + + +HEADER='#![allow(dead_code, non_snake_case, unused_imports, unused_variables)]\n' +WORKER_STUBS=r''' +extern crate self as windows_sys; +extern crate self as crossbeam_channel; +pub use std::sync::mpsc::{Receiver, SyncSender as Sender, TryRecvError}; +pub fn bounded(size: usize) -> (Sender, Receiver) { std::sync::mpsc::sync_channel(size) } +static WRITTEN: std::sync::Mutex> = std::sync::Mutex::new(Vec::new()); +static NOTIFIED: std::sync::atomic::AtomicUsize = std::sync::atomic::AtomicUsize::new(0); +pub mod Win32 { + pub mod Foundation { + pub type HWND = *mut std::ffi::c_void; + pub const ERROR_BROKEN_PIPE:u32=109; + pub const ERROR_GEN_FAILURE:u32=31; + pub const ERROR_NOT_ENOUGH_MEMORY:u32=8; + pub unsafe fn GetLastError()->u32 {31} + } + pub mod UI { pub mod WindowsAndMessaging { + pub unsafe fn PostMessageW(_: crate::Win32::Foundation::HWND, _:u32, _:usize, _:isize)->i32 { + crate::NOTIFIED.fetch_add(1,std::sync::atomic::Ordering::SeqCst); 1 + } + }} +} +pub mod infrastructure { + pub mod native { pub fn record_win32_error(_: &str, _:u32) {} } + pub mod diagnostics { + pub struct Field; + impl Field { + pub fn text(_: &str, _: impl AsRef)->Self { Self } + pub fn unsigned(_: &str, _:u64)->Self { Self } + pub fn boolean(_: &str, _:bool)->Self { Self } + } + pub enum Level { Debug, Error, Info, Trace, Warn } + pub fn event(_:Level,_:&str,_:&str,_:&str,_:&[Field]) {} + pub fn event_with(_:Level,_:&str,_:&str,_:&str,_:Option,_:Option,_:&[Field]) {} + pub fn next_operation_id()->u64 { 1 } + pub fn current_operation_id()->Option { None } + pub fn with_operation_id(_:u64,f:impl FnOnce()->R)->R { f() } + pub fn initialize_from_env() {} + pub fn shutdown() { assert_eq!(*crate::WRITTEN.lock().unwrap(),vec![1,2],"process exit lost accepted startup writes"); } + } + #[path="WORKER_SOURCE"] pub mod worker; +} +''' + + +def worker_source(root): + return WORKER_STUBS.replace('WORKER_SOURCE',str((root/'src/infrastructure/worker.rs').resolve())) + + +def generate(root, area): + root=Path(root) + if area=='worker': + code=worker_source(root)+r''' +fn main() { + let stop=infrastructure::worker::WorkerStopSignal::default(); + stop.cancel(); + stop.notify(std::ptr::dangling_mut(),42); + assert_eq!(NOTIFIED.load(std::sync::atomic::Ordering::SeqCst),0,"notification escaped the retired gate"); +} +''' + elif area=='startup': + code=worker_source(root)+r''' +struct StartupRequest { toggles:Vec, refresh:bool } +struct StartupPageState { + worker:Option>, + rows:Vec<()>, +} +'''+functions(root,'src/pages/startup/model.rs',['merge_startup_requests']) + code+='\nimpl StartupPageState {\n'+function(root,'src/pages/startup.rs','destroy')+'\n}\n' + code+=r''' +mod capabilities { pub fn run_from_environment()->Option {None} } +mod app { + use super::*; + pub fn run()->i32 { + let mut worker=infrastructure::worker::SingleFlightWorker::spawn( + "formal-startup-probe",0,merge_startup_requests, + |request:StartupRequest| WRITTEN.lock().unwrap().extend(request.toggles) + ).unwrap(); + worker.request(StartupRequest{toggles:vec![1],refresh:false},std::ptr::null_mut()).unwrap(); + worker.request(StartupRequest{toggles:vec![2],refresh:false},std::ptr::null_mut()).unwrap(); + worker.request(StartupRequest{toggles:vec![],refresh:true},std::ptr::null_mut()).unwrap(); + let mut page=StartupPageState{worker:Some(worker),rows:vec![]}; + page.destroy(); + 0 + } +} +'''+function(root,'src/main.rs','main') + elif area=='services': + code=r''' +#[derive(Clone,Copy,Debug,PartialEq,Eq)] +enum ServiceRunState {Stopped, StopPending, Running, Paused, Unknown(u32)} +const ERROR_SERVICE_REQUEST_TIMEOUT:u32=1053; +'''+functions(root,'src/pages/services/model.rs',['stop_has_completed','restart_after_stop'])+r''' +fn main() { + for state in [ServiceRunState::Running,ServiceRunState::StopPending,ServiceRunState::Paused,ServiceRunState::Unknown(99)] { + let mut starts=0; + let outcome=restart_after_stop(Ok(state),|| {starts+=1;Ok(ServiceRunState::Running)}); + assert!(outcome.is_err(),"restart reported success without a completed stop and start"); + assert_eq!(starts,0); + } + let mut starts=0; + assert_eq!(restart_after_stop(Ok(ServiceRunState::Stopped),|| {starts+=1;Ok(ServiceRunState::Running)}),Ok(ServiceRunState::Running)); + assert_eq!(starts,1); + assert_eq!(restart_after_stop(Err(5),|| panic!("must not start after error")),Err(5)); +} +''' + elif area=='sessions': + code=r''' +#[derive(Clone,Debug,PartialEq,Eq)] enum UserSessionKind { Disconnect, Logoff, SendMessage } +#[derive(Clone,Debug,PartialEq,Eq)] struct UserSessionCommand {kind:UserSessionKind,sessions:Vec,title:String,body:String} +#[derive(Clone,Debug,PartialEq,Eq)] enum UserWorkerRequest {Refresh,Actions(Vec)} +'''+functions(root,'src/pages/users.rs',['merge_user_requests','session_action_already_queued','queue_session_action'])+r''' +fn main() { + let first=UserSessionCommand{kind:UserSessionKind::SendMessage,sessions:vec![1],title:"first".into(),body:"one".into()}; + let mut second=first.clone(); second.body="two".into(); + let mut pending=UserWorkerRequest::Actions(vec![first.clone()]); + merge_user_requests(&mut pending,UserWorkerRequest::Actions(vec![second.clone(),first.clone()])); + assert_eq!(pending,UserWorkerRequest::Actions(vec![first.clone(),second.clone(),first.clone()]),"a confirmed message was discarded"); + let mut outstanding=vec![first.clone()]; + assert!(queue_session_action(&mut outstanding,second,true)); + let disconnect=UserSessionCommand{kind:UserSessionKind::Disconnect,..first}; + let mut pending=UserWorkerRequest::Actions(vec![disconnect.clone()]); + merge_user_requests(&mut pending,UserWorkerRequest::Actions(vec![disconnect.clone()])); + assert_eq!(pending,UserWorkerRequest::Actions(vec![disconnect])); +} +''' + elif area=='processes': + code=r''' +const ERROR_INVALID_PARAMETER:u32=87; +#[derive(Clone,Copy)] struct ProcIdentity {pid:u32,creation_time_100ns:u64} +impl ProcIdentity { fn is_verified(&self)->bool {self.creation_time_100ns!=0} } +#[derive(Debug)] struct OwnedHandle(u64); +impl OwnedHandle { fn as_raw(&self)->u64 {self.0} } +fn open_process(_:u32,_:u32)->Result {Ok(OwnedHandle(200))} +fn query_process_creation_time(handle:u64)->Result {Ok(handle)} +'''+functions(root,'src/system/process_identity.rs',['open_process_for_identity'])+r''' +fn main() { + assert!(open_process_for_identity(ProcIdentity{pid:42,creation_time_100ns:100},1).is_err(),"reused PID yielded a handle to the wrong process"); + assert!(open_process_for_identity(ProcIdentity{pid:42,creation_time_100ns:0},1).is_err()); + assert_eq!(open_process_for_identity(ProcIdentity{pid:42,creation_time_100ns:200},1).unwrap().as_raw(),200); +} +''' + elif area=='applications': + code=r''' +use std::cell::Cell; +use std::collections::HashSet; +const ERROR_INVALID_PARAMETER:u32=87; +const PROCESS_TERMINATE:u32=1; +const PROCESS_QUERY_LIMITED_INFORMATION:u32=4096; +#[derive(Clone,Copy,Debug,PartialEq,Eq,Hash)] struct ProcIdentity {pid:u32,creation_time_100ns:u64} +impl ProcIdentity { fn is_verified(&self)->bool {self.creation_time_100ns!=0} } +#[derive(Debug)] struct OwnedHandle(u64); +#[derive(Clone,Copy)] struct TaskIdentity { hwnd:usize, process:ProcIdentity } +impl OwnedHandle { fn as_raw(&self)->u64 {self.0} } +thread_local! { + static GENERATION: Cell = const {Cell::new(200)}; + static FAILURE: Cell = const {Cell::new(0)}; + static APPLIED: Cell = const {Cell::new(0)}; +} +fn open_process(_:u32,access:u32)->Result { + assert_eq!(access,PROCESS_TERMINATE|PROCESS_QUERY_LIMITED_INFORMATION); + if FAILURE.get()==1 {return Err(5);} + Ok(OwnedHandle(GENERATION.get())) +} +fn query_process_creation_time(handle:u64)->Result { + if FAILURE.get()==2 {return Err(6);} + GENERATION.set(300); // Even if an environment lookup changes, the handle stays fixed. + Ok(handle) +} +unsafe fn TerminateProcess(handle:u64,_:u32)->i32 { + if FAILURE.get()==3 { return 0; } + APPLIED.set(handle); 1 +} +fn record_win32_error(_: &str,_:u32) {} +fn last_error_or_gen_failure()->u32 {31} +'''+functions(root,'src/system/process_identity.rs',['open_process_for_identity'])+'\n'+item((root/'src/pages/applications.rs').read_text(),r'struct EndTaskRequest\b')+'\n'+functions(root,'src/pages/applications.rs',['confirmed_end_task_request','run_end_tasks','run_end_task_queue','end_task_processes','terminate_task_process'])+r''' +fn main() { + let selected = TaskIdentity {hwnd:123,process:ProcIdentity{pid:42,creation_time_100ns:200}}; + assert!(confirmed_end_task_request(vec![selected],||false).is_none(),"cancelled action was accepted"); + assert!(confirmed_end_task_request(vec![],||panic!("empty selection prompted")).is_none()); + let command = |time| confirmed_end_task_request(vec![TaskIdentity {process:ProcIdentity{pid:42,creation_time_100ns:time},..selected}],||true).unwrap(); + assert!(run_end_tasks(vec![command(0)]).is_some()); + assert!(run_end_tasks(vec![command(100)]).is_some(),"reused PID was terminated"); + assert_eq!(APPLIED.get(),0); + for failure in 1..=3 { + GENERATION.set(200); FAILURE.set(failure); + assert!(run_end_tasks(vec![command(200)]).is_some()); + assert_eq!(APPLIED.get(),0,"API failure reached termination"); + } + FAILURE.set(0); GENERATION.set(200); + // Replay the old counterexample: HWND 123 now belongs to another selected process. + let mut current_window = selected; + let request = confirmed_end_task_request(vec![current_window],|| { + current_window.process=ProcIdentity{pid:99,creation_time_100ns:300}; + true + }).unwrap(); + assert_ne!(request.targets[0],current_window.process,"confirmation retargeted to recycled window"); + assert_eq!(run_end_tasks(vec![request]),None); + assert_eq!(APPLIED.get(),200,"operation did not use the saved identity and same verified handle"); +} + +''' + elif area=='sampling': + code=r''' +#[derive(Default)] struct HistoryBuffer {values:Vec} +impl HistoryBuffer {fn push(&mut self,v:u8) {self.values.push(v);}} +'''+functions(root,'src/pages/gpu.rs',['memory_percentage','record_memory_history'])+r''' +fn main() { + for usage in [None,Some(0),Some(5),Some(u64::MAX)] { + for limit in [None,Some(0),Some(10),Some(u64::MAX)] { + let mut history=HistoryBuffer::default(); + record_memory_history(&mut history,usage,limit); + let valid=usage.is_some() && limit.is_some_and(|v|v>0); + assert_eq!(history.values.len(),usize::from(valid),"unknown capacity became a measured history point"); + } + } + let mut history=HistoryBuffer::default(); + record_memory_history(&mut history,Some(0),Some(10)); + assert_eq!(history.values,vec![0]); +} +''' + else: raise ValueError(area) + return HEADER+code + + +MUTATIONS={ + 'worker': [('src/infrastructure/worker.rs','*closed = true;','*closed = false;')], + 'services': [('src/pages/services/model.rs','Ok(_) => Err(ERROR_SERVICE_REQUEST_TIMEOUT),','Ok(state) => Ok(state),')], + 'startup': [('src/main.rs',' infrastructure::worker::drain_before_process_exit();\n','')], + 'sessions': [('src/pages/users.rs','command.kind != UserSessionKind::SendMessage\n && queued','queued')], + 'processes': [('src/system/process_identity.rs','if creation_time_100ns != identity.creation_time_100ns {','if false {')], + 'applications': [('src/system/process_identity.rs','if creation_time_100ns != identity.creation_time_100ns {','if false {')], + 'sampling': [('src/pages/gpu.rs',' if limit.filter(|limit| *limit != 0).is_none() {\n return;\n }','')], +} diff --git a/verification/formal/verify.py b/verification/formal/verify.py new file mode 100644 index 0000000..5355344 --- /dev/null +++ b/verification/formal/verify.py @@ -0,0 +1,130 @@ +#!/usr/bin/env python3 +# +------------------------------------------------------------------------- +# Taskmgr bounded state-machine verification and real-source mutation checks +# File: verification/formal/verify.py +# Date: 2026-11-09; environment: Darwin arm64, Python 3.9.6, Java 25.0.4.1 +# Author: OpenAI Codex +# -------------------------------------------------------------------------- +"""Run TLC on finite models and replay their critical paths in extracted Rust. + +A model pass does not prove the full Win32 program. A drift error is not a bug +verdict. All generated Rust, mutations, Java temp files and logs stay in --out. +""" +import argparse +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +from source_probe import MUTATIONS, generate + +ROOT=Path(__file__).resolve().parents[2] +MODEL_FILE=Path(__file__).with_name('models.json') +JAR_SHA256='936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88' + +def sha(path): return hashlib.sha256(path.read_bytes()).hexdigest() + +def invoke(args,cwd,timeout,log): + result=subprocess.run([str(a) for a in args],cwd=cwd,text=True,capture_output=True,timeout=timeout) + log.write_text(result.stdout+result.stderr) + return result + +def check_model(area,m,out,jar,java,broken=False): + dest=out/area/('mutant-model' if broken else 'model') + dest.mkdir(parents=True) + folder=ROOT/(m.get('model_dir') or m['skill']) + module=m['module'] + for suffix in ['.tla','.cfg','-broken.cfg']: + shutil.copy2(folder/(module+suffix),dest/(module+suffix)) + (dest/'java-tmp').mkdir() + config=module+('-broken.cfg' if broken else '.cfg') + result=invoke([java,'-Xmx256m','-XX:+UseParallelGC','-Djava.io.tmpdir='+str(dest/'java-tmp'), + '-cp',jar,'tlc2.TLC','-workers','1','-seed','1','-fp','0','-config',config,module+'.tla'],dest,60,dest/'tlc.out') + text=result.stdout+result.stderr + if result.returncode==0 and 'Model checking completed. No error has been found.' in text: + verdict='pass' + elif 'Invariant Safety is violated.' in text: + verdict='violation' + else: raise RuntimeError('TLC did not finish checking '+area+': '+str(dest/'tlc.out')) + return {'verdict':verdict,'exit_code':result.returncode,'log':str(dest/'tlc.out')} + +def source_probe(area,m,out,source_root,mutant=False): + dest=out/area/('mutant-source' if mutant else 'source') + dest.mkdir(parents=True,exist_ok=True) + if mutant: + shadow=dest/'tree' + for record in m['coverage']: + path=record['path']; target=shadow/path + target.parent.mkdir(parents=True,exist_ok=True) + shutil.copy2(ROOT/path,target) + for path,old,new in MUTATIONS[area]: + file=shadow/path + text=file.read_text() + if text.count(old)!=1: raise RuntimeError('Mutation anchor drift: '+path) + file.write_text(text.replace(old,new,1)) + source_root=shadow + rust=dest/'probe.rs'; rust.write_text(generate(source_root,area)) + binary=dest/('probe.exe' if os.name=='nt' else 'probe') + build=invoke(['rustc','--edition=2024',rust,'-o',binary],dest,60,dest/'compile.log') + if build.returncode: raise RuntimeError('Probe did not compile: '+str(dest/'compile.log')) + result=invoke([binary],dest,10,dest/'replay.log') + if mutant and result.returncode==0: raise RuntimeError('Source mutation was not detected: '+area) + expected=1 if mutant else 0 + if bool(result.returncode)!=bool(expected): + raise RuntimeError('Unexpected source replay outcome: '+str(dest/'replay.log')) + return {'verdict':'assertion_failed' if result.returncode else 'pass','exit_code':result.returncode,'log':str(dest/'replay.log')} + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('area',nargs='?',default='all') + parser.add_argument('--self-test',action='store_true',help='also break each property in scratch copies of real Rust and TLA+') + parser.add_argument('--out',type=Path,help='new or empty folder outside the repository') + parser.add_argument('--jar',type=Path,default=Path(os.getenv('TLA2TOOLS',str(ROOT/'verification/.tools/tla2tools-1.7.4.jar')))) + parser.add_argument('--java',default=os.getenv('JAVA','java')) + args=parser.parse_args() + if args.area=='applications_force': args.area='applications' # prior CLI alias + models=json.loads(MODEL_FILE.read_text()) + if args.area!='all': models={args.area:models[args.area]} + for area,m in models.items(): + for record in m['coverage']: + file=ROOT/record['path'] + if not file.exists() or sha(file)!=record['sha256']: + raise RuntimeError('SOURCE DRIFT, not an invariant verdict: '+record['path']+'. Read the subsystem verification notes, compare code to model, then update the sync record only after review.') + if not args.jar.exists() or sha(args.jar)!=JAR_SHA256: + raise RuntimeError('Need verified TLA+ tools 1.7.4. Set TLA2TOOLS or --jar. Expected SHA-256 '+JAR_SHA256) + out=(args.out or Path(tempfile.mkdtemp(prefix='taskmgr-formal-'))).resolve() + if ROOT==out or ROOT in out.parents: raise RuntimeError('--out must be outside the repository') + if out.exists() and any(out.iterdir()): raise RuntimeError('--out must be new or empty') + out.mkdir(parents=True,exist_ok=True) + results={} + for area,m in models.items(): + record={'model':check_model(area,m,out,args.jar.resolve(),args.java), + 'source':source_probe(area,m,out,ROOT)} + expected='violation' if m['expected_tlc_exit'] else 'pass' + if record['model']['verdict']!=expected: + raise RuntimeError('Changed model verdict for '+area+'; inspect '+str(out/area)) + if args.self_test: + record['mutation_model']=check_model(area,m,out,args.jar.resolve(),args.java,True) + if record['mutation_model']['verdict']!='violation': raise RuntimeError('TLA mutation was not detected: '+area) + record['mutation_source']=source_probe(area,m,out,ROOT,True) + record['restored_model']=check_model(area,m,out/'restored',args.jar.resolve(),args.java) + record['restored_source']=source_probe(area,m,out/'restored',ROOT) + if record['restored_model']['verdict']!=expected: + raise RuntimeError('Original model did not return to its baseline: '+area) + results[area]=record + print(area+': '+record['model']['verdict']+'; real-source replay '+record['source']['verdict']+ + ('; both negative controls detected' if args.self_test else ''),flush=True) + report={'sync_commit':next(iter(models.values()))['sync_commit'],'tool':'tla2tools 1.7.4 / TLC 2.19', + 'scope':'finite models plus controlled Rust replays; not whole-program verification','results':results} + (out/'summary.json').write_text(json.dumps(report,ensure_ascii=False,indent=2)+'\n') + print('Report: '+str(out/'summary.json')) + return 1 if any(r['model']['verdict']=='violation' for r in results.values()) else 0 + +if __name__=='__main__': + try: sys.exit(main()) + except (OSError,RuntimeError,ValueError,KeyError,subprocess.TimeoutExpired) as exc: + print(str(exc),file=sys.stderr); sys.exit(2)