P5: stabilize proof barriers and post-run hygiene

[YingzuoLiu]

Summary

Stabilize the required P5 multi-worker proof without changing production runtime or authority semantics.

Accepted base: bf15e7abf7f2abdab8ab52eab1344c17e96a200f
Final head: aa2887f1ab260115da2a619d9cb48226cc6edd66
Final tree: b61488d7249bb1192ce86adb4814e5c27c9977c5

The failures were in deterministic proof orchestration, not the lease/fencing implementation:

1. A reusable hook could be re-armed before its prior consumer acknowledged release.
2. A controller could arm a new claim.before / claim.result schedule while a worker was already inside claim_next_run, so the worker skipped the new before hook but consumed the new result hook.
3. A worker intentionally stopped by S5 could retain a synchronized multiprocessing.Array mutex, deadlocking controller diagnostics.
4. Final PostgreSQL hygiene sampling could race with workers that were still polling and observe a legitimate in-flight transaction.

Changes

• Drain and acknowledge the previous named hook generation before re-arming it.
• Serialize hook arming against the proof adapter's complete claim_next_run cycle with a shared claim-cycle lock.
• Track generations in a lock-free RawArray; each slot has exactly one writer.
• Stop workers before polling idle_in_transaction_count.
• Add bounded worker-stack diagnostics, a 300-second CI hard timeout, and bounded SIGCONT/terminate/SIGKILL cleanup.
• Add deterministic spawn/SIGSTOP/straddle regressions and document the scheduling contract.

Changed files remain limited to proof scaffolding, tests, documentation, and its CI wrapper:

• .github/workflows/ci.yml
• docs/p5-multi-worker-recovery-proof.md
• examples/p5_multi_worker_proof.py
• examples/p5_proof_worker.py
• tests/test_p5_multi_worker_proof.py

No runtime_service/ production code changed. No cloud SDK, AWS resource, AWS API, apply, or destroy is involved.

Red-before-green evidence

Each relevant fix was independently reverted and the corresponding regression went red:

• remove completion acknowledgement: stale-release regression fails;
• remove cross-hook drain: cross-hook spawn regression fails;
• remove claim-cycle serialization: exact in-flight straddle regression fails;
• restore synchronized generation storage: SIGSTOP regression detects the poisoned lock.

A separate cross-process generation stress probe completed 200 generations.

Local verification

• P5-focused tests: 21 passed
• Ruff: pass
• mypy: pass
• compileall: pass
• git diff --check: pass
• workflow YAML parse: pass

The final proof-only synchronization refinements were not followed by another local full-suite run. The final head's GitHub test (3.11) and test (3.12) jobs are both green.

Final-head CI evidence

Workflow run: 32965043620

The first final-head attempt was fully green across all eight jobs, including PostgreSQL conformance, PostgreSQL mutation proof, action recovery, P5 proof, and P5 mutation proof.

Because the defect was timing-sensitive, the P5 chain was then rerun twice without changing the head or tree. All three independent samples passed:

Sample	P5 proof	Evidence	Mutation proof	Evidence
1	success	job 98166081039	success, 9/9 killed	job 98166268713
2	success	job 98166991298	success, 9/9 killed	job 98167199145
3	success	job 98167976191	success, 9/9 killed	job 98168183893

Each P5 proof log records S1–S8 as passed and a summary of {"failed": 0, "passed": 8}. Each dependent mutation log records P5M01–P5M09 as killed.

Earlier commits/runs on this branch include genuine failed diagnostic attempts that exposed the races above. They are intentionally retained as history; the final-head claims use only the SHA/tree and job IDs listed here.

Scope

This PR remains separate from #38 so the portable-substrate contract stays independently reviewable. It repairs the repository-level P5 evidence gate that blocked later P6 work; it does not broaden P6 scope and does not authorize a merge or any real AWS action.