docs: record failure-safe PI proof

This commit is contained in:
2026-08-24 18:15:47 +08:00
parent 09841c8dbd
commit 6d2232c32f

View File

@@ -66,9 +66,10 @@
## Outcome
- Final code candidate `0d26d17cfc5d32c91d6e25d919be1fabd94a605b`
closes all three P1 implementation/proof defects from the planner's second
review. Final-product proof now runs Main from packaged `app.asar`, starts the
- Final code candidate `09841c8dbd7c58ce9ecda9dc49ea1c1b57759b67`
closes the three P1 implementation/proof defects from the planner's second
review and the two P1 defects from its third review. Final-product proof now
runs Main from packaged `app.asar`, starts the
packaged `resources/pi-runtime/dist/cli.js`, receives a real `subagent` tool
call from a controlled loopback provider, dispatches through the real
`PiSubagentScheduler`, and starts a real ephemeral Pi child with exactly the
@@ -79,11 +80,22 @@
`agent.settled`. Direct admission emits an explicit zero-duration queue wait;
reopening the same session after a resource rebuild is correctly classified
as warm.
- `provider.first_event` now accepts only Pi's Provider-backed assistant
`message_start`, never `turn_start` or the local user-message lifecycle. The
controlled Provider delays its first response by 75 ms; the packaged smoke
asserts the source marker, strict timestamp ordering, and a measured delay of
at least 75% of that value, so the old zero-millisecond false milestone fails.
- The 4+4 pressure proof now holds four real persistent Pi parents and four
real ephemeral Pi children as eight distinct live OS processes while four
write leases are active, proves the product UI remains interactive, and then
proves all processes, provider requests, process-budget entries, child
permits, dispatches, parents, and write leases return to zero.
- Pressure cleanup now attempts every bounded cleanup step even when an earlier
step fails, keeps the global run handle until cleanup succeeds, and supports
idempotent retry. Unit tests cover one-shot failure and a hanging step; final
Windows and Linux products also inject a `parents.settle` failure into a real
4+4 run, observe the expected first failure, retry, and prove every counter
and PID returns to zero.
- Real concurrent parent startup exposed a supported Windows failure in the
shared managed provider catalog: simultaneous temporary-file renames could
fail with `EPERM`. Same-path catalog writes are now serialized, with focused
@@ -109,50 +121,50 @@
## Verification
- Exact pnpm `10.33.4` frozen install passed on Windows and WSL2 Ubuntu 24.04
x64; both final-product runs were bound to clean commit `0d26d17`. The
x64; both final-product runs were bound to clean commit `09841c8`. The
lockfile change remains limited to the direct `@electron/asar@3.4.1`
verifier dependency.
- Candidate-final Windows checks passed: `pnpm run typecheck`; `pnpm run
lint:check` with 0 errors and five pre-existing warnings; focused proof tests
with 6 files/25 passed/2 skipped; focused concurrency tests with 4 files/26
passed; `pnpm test` with 178 files/1506 passed/2 skipped; `pnpm run test:e2e`
with 24/24; and repeated `pnpm run build:vite` production builds.
- Final Windows NSIS `release/Makelore-2.0.0-win-x64.exe` is 208,369,701 bytes
and cleanup tests passed; focused concurrency tests passed; `pnpm test` with
179 files/1508 passed/2 skipped; `pnpm run test:e2e` with 24/24; and repeated
`pnpm run build:vite` production builds.
- Final Windows NSIS `release/Makelore-2.0.0-win-x64.exe` is 208,525,071 bytes
with SHA-256
`C68DF05932055CF950A3491CB34CACB8A2D39F8F3D987B32FE4950621D1CC9B6`.
`396D6E8EC2BED60498DBC36CDA714176B629574914B85A5651C73DF8A63CECAA`.
Its unpacked `app.asar` SHA-256 is
`F03278F6CF08B2D72F1518EFAA8338A92A8DDA0261AEEFCE82D93ACB9333F4D8`.
`872E8D1E7F22994EFF10353DF380016A198C59C145EBF63491E13DA1B1071B7F`.
The post-installer-build final product proof passed from that ASAR with real
Pi parent/child PIDs and complete cleanup. Windows structured reports are
`release/evidence/pi-smoke-win-real-workers.json`,
`release/evidence/pi-performance-win-real-workers.json`, and
`release/evidence/pi-product-proof-win-final-installer-build.json`.
`release/evidence/pi-smoke-win-final.json` and
`release/evidence/pi-performance-win-final.json`.
- Windows formal five-sample performance passed every budget and recorded all
nine cold/warm milestones with five samples each. Cold p95 was queue `0 ms`,
resources `32 ms`, spawn `14 ms`, RPC `718 ms`, session `4 ms`, accepted `1
ms`, agent start `1 ms`, first event `0 ms`, and settled `869 ms`; warm p95
was `0/11/8/624/1/1/0/0/64 ms`. Five 4+4 pressure samples had UI p95 `188
ms`; Renderer first-commit p95 was `33.466 ms`; exit p95 was `19 ms`.
- WSL2 Linux x64 final product was rebuilt at exact clean commit `0d26d17`.
resources `30 ms`, spawn `18 ms`, RPC `750 ms`, session `4 ms`, accepted `2
ms`, agent start `1 ms`, Provider first event `151 ms`, and settled `1034
ms`; warm p95 was `0/10/9/660/1/2/0/144/146 ms`. Five 4+4 pressure samples
had UI p95 `140 ms`; Renderer first-commit p95 was `33.6862 ms`; exit p95 was
`16 ms`.
- WSL2 Linux x64 final product was rebuilt at exact clean commit `09841c8`.
AppImage/DEB/RPM SHA-256 values are respectively
`38c71302e26a0f7946ffcf72e23edd176b0abc1630da62ef25a808fddb6fdd5c`,
`7c4b29d819aba21c66abb1f41d62cd5b8aed24e44823e9eb875981133672f22b`,
and `cf6983f64a9d2c1f1080fabd9e1724914662e559843b9ceb4f11198a7312b917`.
`d0923c3d80c046c3e98750f7d55696e2753b710f9441d043a94768e0395a69c5`,
`930cc826993506f56544adc3c29fcddd993117c04e87332c81d031fd9d1ce070`,
and `81c1ceefbbe6314dec9c98b1441507458f23eea52c9acbf1360be0db20a88986`.
Final ASAR SHA-256 is
`300dfeb32ded8c6fa764c6604f7d10c175dcbdc28e219169402f65a0dd50d7f7`.
- Linux formal smoke passed Pi `0.84.2` production closure, 10,282-entry ASAR
`9ce9bce7a36e9d93a866b6982fb53c9e98f410d2dd92003fee2d3370deff7b15`.
- Linux formal smoke passed Pi `0.84.2` production closure, 10,284-entry ASAR
enumeration, zero product-owned OpenCode paths, actual final Pi processes,
real packaged extension/subagent dispatch, 4+4 pressure, and zero cleanup.
Reports copied beside the Windows evidence are
`release/evidence/pi-smoke-linux-wsl2-real-workers.json`,
`release/evidence/pi-performance-linux-wsl2-real-workers.json`, and
`release/evidence/pi-product-proof-linux-wsl2-real-workers.json`.
`release/evidence/pi-smoke-linux-wsl2-final.json` and
`release/evidence/pi-performance-linux-wsl2-final.json`.
- Linux formal five-sample performance passed every budget and recorded all
nine cold/warm milestones with five samples each. Cold p95 was queue `0 ms`,
resources `18 ms`, spawn `5 ms`, RPC `498 ms`, session `3 ms`, accepted `1
ms`, agent start `1 ms`, first event `0 ms`, and settled `602 ms`; warm p95
was `0/5/4/492/1/1/0/1/45 ms`. Five 4+4 pressure samples had UI p95 `142
ms`; Renderer first-commit p95 was `28.217 ms`; exit p95 was `9 ms`.
resources `14 ms`, spawn `6 ms`, RPC `480 ms`, session `2 ms`, accepted `2
ms`, agent start `0 ms`, Provider first event `114 ms`, and settled `740 ms`;
warm p95 was `0/6/5/467/1/1/0/111/112 ms`. Five 4+4 pressure samples had UI
p95 `115 ms`; Renderer first-commit p95 was `28.3212 ms`; exit p95 was `9
ms`.
- Linux results are WSL2/WSLg final-product evidence, not an independent native
non-WSL Linux desktop/compositor/distribution acceptance run. Controlled
provider-shaped smoke issued six requests per protocol (distinct cold, warm,
@@ -161,11 +173,11 @@
## Follow-ups
- Request planner re-review of `dc166a1..0d26d17`. The implementation evidence
now directly closes final packaged subagent dispatch, the single Main-owned
cold/warm timeline including zero-valued queue wait, and real
persistent-parent/ephemeral-child 4+4 pressure. The concurrent catalog-write
fix and its regression test are also included.
- Request planner re-review of `ead9d1d..09841c8`. In addition to the earlier
packaged subagent, correlated timeline, and real 4+4 fixes, this range makes
Provider first-event timing response-backed with delayed-response assertions
and makes pressure cleanup bounded, failure-safe, and retryable with both
unit and final-product fault-injection evidence.
- Do not start PI-160 or integrate the candidate while PI-150 remains blocked
by the native non-WSL Linux platform evidence boundary. If the planner finds
no new implementation defect, keep PI-150 as the active frontier until that