§28. Changes from v4.5

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

Incorporates the Phase A close-out review of Oct 30 against commit 805cd1c: four read-only code audits of Oct 29 (ids C/P/D/K/H in the review document), the third-party handoff of Oct 30 (R01–R16, S01–S07), and the owner decisions of Oct 30. Ids in brackets name the finding each change closes; the review document in the project carries the file:line evidence for each.

New invariants and schema

• I24: agent authority bound per instance; AgentStarted { name, instance, by }; agent run refuses a name in use; B-20 (High) registered and closed by this [new finding; R05 context].
• I25: post-commit bookkeeping on every commit path; a commit whose floor record cannot be written does not commit [R02, C8].
• I6 and §12 Concurrency carry the same exclusive-state list, now including Checking and Publishing; TxnState::exclusive is that list and the ledger reads it [S07, D11, C20].
• I7: probe evidence per probe and the approver’s identity in the record [C1, C17]. I8: re-validation also when leaving Built [C2, P1]. I12: parked states bounded or reported [S03]. I20: launched agents inside the rule [R05]. I23: the override CAS is under the daemon’s lock; X-12 for writers outside it [R11].
• TxnState::Publishing for the boot-only path [R01]. RejectReason::{Precondition, ActivationUnknown} [C3, R10].

§9 and §10

• verify_candidate checks the recorded NAR hash of the store path, not existence; the dry activation must succeed, in time, untruncated [C6/P2, R10].
• Promote/restore under flock; txn/<id>/ by exclusive mkdir and deleted after terminal + checkpoint; the content-addressed override store pruned [C5, R11].
• Orphan build roots aged out at startup and before every GC, including crashed builds [C4/P5].
• Stale check, re-derive and re-decide on every path into Activating, including from Built [C2].
• Executor-owned post-check per probe against the pre-change set, and over every observed unit [R07, C22].
• Probe timeout is a whole-probe deadline; the batch never waits past it; typed probes’ sandboxing deferred to C with bytes_max enforced for every reading kind [R06, P10]. Slow ticks warned [P9].
• Graphical expectation for seated sessions only; SessionEstablished unchanged [S05].
• External dependencies need a traversable edge (Requires or Diagnostic ≥ 0.7); the module rejects weaker ones [S06, P12].
• Boot confirmation as two milestones, admission and confirmation [S02].

§11

• Equivalent effects, equivalent facts: SetOverride{Stopped|Absent|Detected} carries the effects it causes; existing-generation operations derive from a dry activation of the target and its recorded override content [R03/C11, R04/C7].
• Preconditions checked by the executor for every proposal [C3].
• Agent identity per instance; Actor::Model authorized as an agent, never as the daemon [new finding, C14].

§12, §12a–§12h

• Admission before work: authorization, catalog membership and the interlock checked before stage/evaluate/build; prebuild work bounded and charged [R09].
• Tokens die with the daemon; consumed nonces in the checkpoint; approvals recorded with approver and bound_to; the approved execution logged [S07, C1].
• Boot-only path: Publishing journaled before publish_boot_once; the publishing generation is the fallback, never known_good automatically; crash-table row for Publishing; AwaitingBoot never re-prepared [R01, S01].
• Re-prepared transactions keep their original caller and source [C21].
• Post-commit bookkeeping in the kernel’s commit on every path [R02, C8]. Floor derived relative to every earlier generation, so a Revert sets no floor [C9/H17].
• Worker subprocess wording replaced: a worker thread in A; Lease.worker_pid/jobs reserved for D (deviations row) [C13/P3].
• §12a write-backs queue behind an active generation transaction [P7]. §12f: parking in Built bounded at 24 h; AwaitingBoot reported as waiting; deferred repairs are deferred in fact [S03, P8]. §12c: a damaged checkpoint or record is Integrity, never Absent [C16].
• §12d: launched agents in planarian-agents.slice, ordered and conditioned on readiness, stopped wholesale by the posture, with per-launch and per-uid limits [R05]; greetd ordered when it is the display manager [P13]; “administrators” means Planarian’s, not wheel [P14]; planarian-recovery has a start limit and raises Crashed [P15]; weakening posture/timeout takes effect at the next boot because the posture units read the booted generation [P16].

§13–§16

• Incident control state changes only on an authorized, successful human action [R08].
• The repair:reapply catalog entry ships [P22].
• Residue notice teaches the attributed form [P23] (unchanged text in §14; the requirement is restated as a §15 case).
• §15: the v4.6 acceptance cases; the harness contract (runners exit nonzero on ERROR/FAIL/PARTIAL and on unwaived UNSUPPORTED; CI strict) [R12, R15]; invisibility measured over service cgroups with a real p99 [R13].
• §16: report boot, posture exist; ack <unit>; mark-good’s TTY from the daemon; agent run refuses names in use [P17, P18, K10].

§17a, §17b, §18, §19, §6

• §17a: the accounting is checked (no duplicate ids, baseline invariants required, obligations tied to verifier output) [R14, D1]; the Phase A proof status stated, with the residue Kani harnesses and the I17 proof named as still required [D4].
• §17b: three tables, Closed rows kept; B-20 and X-12 [D13].
• §17c (new, Oct 31): the guarantees site; bypass rows name the invariants they limit; rule 22.
• I6, §10, §12 Concurrency (owner decision, Oct 31): unit and device repairs run during a boot-only Promoted, and a canonical unit that needed a repair since admission means the change is not confirmed.
• §12f Rollbacks (owner decision, Oct 31): a user- or intent-requested rollback runs at once; a diagnoser rollback after failed in-place repair is a repair, exempt from activation windows but not from the disruption floors, and deferred with its incident under quiet mode unless its target is a foreground dependency; the revert of a failing candidate is never deferred. Three §15 cases.
• §18: rules 19–21 (the handoff order; equivalent effects; nothing from a failed tool); rule 4’s preserve list to I25 [D5].
• §19: the Oct 30 decisions recorded; two owner items added [Q7, Q8].
• §6: the layout describes the repository as it is [D14, H14].

Documentation, to be corrected in the sweep (not spec changes): ga-status.md describes the pre-805cd1c agent model and two of three verification numbers; guarantees.md carries the v4.4 trust count and P9; AGENTS.md lacks rules 12–21 and says the console is unbuilt; catalog-review.md counts a 71-entry catalog; phase-a.toml says v4.4; vm.yml and AGENTS.md count 7/62 jobs and 70 runner minutes; assumptions.md P5 names txn::journal::chain; verification.md cites §8 for §7 [D6–D10, D12, H2–H4, R16]. docs/why.md is still to be written; the review’s §5 has notes on the draft.