feat: add managed agent integration lifecycle

.github/workflows/ci.yml

@@ -90,6 +90,15 @@ jobs:
       - name: Run all Go tests
         run: npm run go:test
 
+      - name: Verify deletion across filesystem boundaries
+        run: |
+          set -euo pipefail
+          root="$(mktemp -d "${RUNNER_TEMP}/proofkit-cross-filesystem.XXXXXX")"
+          mkdir "${root}/other"
+          sudo mount -t tmpfs -o "size=16m,mode=0700,uid=$(id -u),gid=$(id -g)" tmpfs "${root}/other"
+          trap 'sudo umount "${root}/other" && rmdir "${root}/other" "${root}"' EXIT
+          PROOFKIT_CROSS_FILESYSTEM_ROOT="${root}" go test ./internal/kernel/repositorytransaction -run '^TestDeletionRejectsDifferentFilesystemBeforeControlMutation$' -count=1 -v
+
       - name: Run Go vet
         run: npm run go:vet
 

ADOPTION.md

@@ -217,23 +217,46 @@ Resolve the approved installed launcher for each session. An absent or
 ambiguous binding needs an owner decision, not an install, network fallback,
 package-manager default, or persisted machine-local executable path.
 
-For one manual export, first inspect the explicit repository root and every
-component of the selected path. Stop on symlinks, aliases, unknown ownership,
-local edits, or an existing target; do not overwrite it. The example below
-assumes the owner has approved the npm launcher, inspected and prepared the
-ordinary parent directories, and ensured no concurrent writer can replace
-them. Replace the example absolute root with that inspected root. The shell,
-not Proofkit, creates the file; noclobber protects an existing final file but
-does not establish race-free parent traversal or transactional installation.
+For managed installation, select the tool and root explicitly, inspect the
+plan, then apply its exact transaction and desired-state identities. The
+following example assumes a repository-approved, already installed npm
+launcher; other approved carriers expose the same logical routes. Replace the
+root and identity placeholders with the reviewed plan's values.
 
 ```bash
-(set -o noclobber; npm exec --offline -- agentic-proofkit integration source --tool codex --format text > /absolute/inspected/repository/.agents/skills/agentic-proofkit/SKILL.md)
+npm exec --offline -- agentic-proofkit integration plan --tool codex --operation install --repo-root /absolute/inspected/repository --format text
+npm exec --offline -- agentic-proofkit integration apply --tool codex --operation install --repo-root /absolute/inspected/repository --expect-transaction <reviewed-transaction-sha256-ref> --expect-desired-state <reviewed-desired-state-sha256-ref>
 npm exec --offline -- agentic-proofkit integration check --tool codex --repo-root /absolute/inspected/repository
 ```
 
-Check a failed export before treating its output as usable: shell redirection
-may leave an empty or partial new file if generation or transport fails.
-Resolve such a file manually under repository ownership; check never repairs it.
+`REQ-PROOFKIT-WORKFLOW-019` owns managed file lifecycle. Use `--operation
+update` or `--operation remove` with a fresh reviewed plan for those operations.
+The fixed bootstrap and `proofkit/integrations/<tool>.v1.json` baseline share
+one native transaction. Local byte or mode edits are conflicts, not overwrite
+permission. An exact current manually exported bootstrap can be enrolled by
+install; an unknown or stale unbaselined file requires an owner decision.
+The baseline records exact cooperative before-state, not authenticated origin.
+Removal deletes selected managed files only, leaving their directories and
+adjacent instructions. It does not archive or replace instructions with an
+empty file. Baseline-only removal can clean a valid orphan baseline.
+
+After interruption, use `integration recover --repo-root <root> --transaction
+<pending-sha256-ref> --action <resume|rollback>`. It uses the existing native
+journal, not the current bootstrap source. A completed recovery is historical
+evidence; inspect current files separately. Desired-absence journals and new
+identity-bound terminal receipts use schema v2 and require this or a later
+supporting binary. Finishing recovery alone does not establish downgrade
+compatibility; no automatic downgrade or control-state deletion is supported.
+Present-only v1 journals and historical v1 receipts remain readable. A legacy
+receipt does not bind its missing desired identity: replan before applying.
+Repeated apply checks that the retained applied transaction binds the exact
+current desired state under one native lock; pending work blocks replay.
+
+Plan and apply default to JSON. Ready plans and passed receipts exit 0;
+classified conflicts, recovery, cleanup or durability outcomes exit 1 with a
+report and empty stderr. Invocation and operational failures use stderr.
+`--format text --color auto` colors labels only on a capable TTY without
+`NO_COLOR`; the default is uncolored. Check never repairs files.
 The checker admits flags before I/O and reads only the selected fixed path
 through an application-write-free confined lease with bounded reobservation.
 Exit 0 and `current` mean exact generated-byte equality; exit 2 reports
@@ -249,8 +272,7 @@ identity when consumed projections remain unchanged. Shared native source
 digests may conservatively invalidate freshness. This is materialization
 freshness, not proof of every transitive runtime behavior.
 
-Phase5B managed install/update/remove remains open. Manual export is not an
-installer, rollback protocol, or proof of host activation. Installed npm/Python
+Managed file lifecycle is not proof of host activation. Installed npm/Python
 integration proof requires actual carrier execution; source-only tests do not
 discharge it. Native-host file discovery, body loading, and approved-launcher calls
 are separate observations requiring isolated sessions and absent/altered-file

BACKLOG.md

@@ -48,7 +48,6 @@ records, generated release manifests, or the owning docs named above.
 
 | Status | ID | Scope | Completion condition |
 |---|---|---|---|
-| NEXT | INTEGRATION-01 | Complete the explicitly selected tool's managed bootstrap lifecycle without treating generation/check as installation or host activation. | One existing repository transaction owner performs reviewed install/update/remove with exact prior-byte and desired-state preconditions, conflict preservation for local edits, real final absence on removal, and rollback/recovery/cancellation/cleanup witnesses; adjacent and global instructions remain unchanged. Isolated native-host tests separately establish file discovery, body loading, and approved-launcher invocation, or retain those precise non-claims. |
 | BLOCKED | SOURCE-CUTOVER-01 | Migrate self-hosted requirement sources only after one codec, the typed v2 model, nested structural contracts, and the complete evidence counterfeit corpus pass their gates. | The `REQ-PROOFKIT-QUALITY-010` execution-backed command-oracle closure and `SCHEMA-01` are complete; a digest-bound clause ledger proves representation-only equality or owner-reviewed semantic decomposition for every legacy requirement; all bindings/scenarios/contracts/context/diff/graph/browser owners cut over atomically; v1 admission and the losing codec are removed; and active-v1 inventory is zero. |
 | BLOCKED | SCHEMA-01 | Replace root-shape-only public contracts with one independent complete nested structural-contract owner. | A versioned schema owner covers nested fields, variants, cardinalities, bounds, enums, defaults, duplicate and unknown-field policy, and cross-field constraints; generated artifacts pass parity against an independently authored completeness manifest and mutant corpus without becoming semantic or policy authority. |
 | BLOCKED | SOURCE-PILOT-01 | Validate the selected source-v2 model and agent routing against heterogeneous external repositories without mutating them. | At least two independent repository classes complete no-push dual runs whose frozen inputs compare incumbent and candidate mapping, diagnostics, token cost, authoring accuracy, proof-route gaps, and rollback; unresolved parity or authority gaps keep incumbent owners active. |

docs/proofkit-contract-map.md

@@ -41,7 +41,7 @@ owner boundaries. It is not a second command-family inventory.
 
 | Family | Main commands | Caller provides | Proofkit owns | Consumer owns | Output authority |
 |---|---|---|---|---|---|
-| Agent integration generation/check | `integration source`, `integration check` | explicit `claude` or `codex` tool; explicit repository root for check only | one portable bounded bootstrap, exact consumed registered-contract identity, descriptor-owned path, and confined read-only generated-byte freshness | launcher admission, manual materialization, instruction ownership, host discovery/activation, permissions, native verification, and any future managed lifecycle | generated source or missing/current/stale/invalid freshness report; neither is installation or execution authority |
+| Agent integrations | `integration source`, `integration check`, `integration plan`, `integration apply`, `integration recover` | explicit tool for source/check/plan/apply; root for filesystem operations; operation and both reviewed identities for apply; transaction/action for recovery | one bounded renderer, read-only freshness, canonical cooperative baseline, and managed file lifecycle through the native transaction owner | launcher admission, instruction ownership, host discovery/activation, permissions and native verification | generated source, freshness classification, reviewed transaction plan or historical transaction receipt; none proves host activation |
 | Project state navigation | `status`, `next` | explicit repository root | bounded transaction-first materialized-project inspection, normalized observation identity, deterministic project-state classification, and one non-executable next action; admitted in-bound records bind exact content digests, while unread out-of-bound records intentionally identify only their invalid class | repository policy, byte identity for unread out-of-bound records, witness execution, receipt trust/currentness/scope, merge, release, deployment, rollout, and production readiness | project-status report, next-action packet, or bounded text projection |
 | Agent workflow planning | `change plan`, `native-evidence-guidance` | explicit checkpoint, completed stage ids, bounded context refs, governing authority ref, and required context ref ids | optional built-in `proofkit.reviewed-change.v1` checkpoint relation, reference-closed next-stage context, deterministic agent prompts, bounded text/JSON/envelope projections, and repository-neutral native-evidence guidance with closed applicability classes | custom workflow topology, repository state discovery, stage execution, native witness semantics, evidence collection, review conclusions, merge, release, deployment, and rollout authority | next-action plan, terminal workflow report, bounded agent envelope, or guidance catalog |
 | Adoption and scaffolding | `adopt plan`, `adopt materialize plan`, `adopt materialize apply`, `adopt materialize recover`, `repository-inventory`, `adoption-contract-envelope`, `adoption-workflow-plan`, `adoption-checklist`, `adoption-doctor`, `gradual-adoption`, `gradual-adoption-bootstrap`, `gradual-adoption-guidance`, `capability-map-admission`, `pilot-admission`, `scaffold-profile-plan`, `scaffold-project-structure`, `stack-preset` | explicit repository root, explicit fresh/code-baseline/audit-from-code intent, optional stack hint, owner-reviewed candidate packet, expected transaction and desired-state identities, recovery action, aggregate adoption contract envelope, checklist facts, target paths, owner routes, caller-extracted stale authority vocabulary facts, explicit pre-spec capability observations, and pilot records | bounded fixed-catalog root inventory, candidate-only front-door tasks, owner-closed read-only materialization plans, confined transactional apply and recovery receipts, aggregate contract-envelope admission, deterministic starter plans, checklist/report admission, bounded guidance envelopes, dry-run manifests, pre-spec trust-mode admission, adoption gap and stale-authority classification, and pilot shape admission | stack selection, arbitrary source inspection, candidate review, final requirement meaning, proof adequacy, rollout policy, text extraction, code observation extraction, and pilot truth | inventory, candidate-only plan, transaction-bound materialization plan or receipt, selected child output, report, seed packet, or agent envelope |
@@ -132,7 +132,9 @@ Semantic context routes are `requirement-context-compose`,
 
 | State or goal | Next Proofkit route | Stop or escalation condition |
 |---|---|---|
-| A repository owner requests a portable Proofkit bootstrap or its exact-byte freshness. | `integration source --tool <tool>` generates JSON or exact file bytes with `--format text`; `integration check --tool <tool> --repo-root <caller-selected-root>` checks only the selected fixed path. Select `claude` or `codex` explicitly. | Source writes nothing; neither route accepts `--output` or install. Source exits 0/1 for success/error; check exits 0 for current, 2 for missing/stale/invalid, and 1 for invocation or operation error. Current proves only generated-byte equality. Use `ADOPTION.md` for inspected manual export; Phase5B installation/update/removal and host activation remain open. |
+| A repository owner requests a portable Proofkit bootstrap or its exact-byte freshness. | `integration source --tool <tool>` generates JSON or exact file bytes with `--format text`; `integration check --tool <tool> --repo-root <caller-selected-root>` checks only the selected fixed path. Select `claude` or `codex` explicitly. | Source writes nothing; neither route accepts `--output` or install. Source exits 0/1 for success/error; check exits 0 for current, 2 for missing/stale/invalid, and 1 for invocation or operation error. Current proves only generated-byte equality. Managed lifecycle is a separate explicit route; host activation remains an independent observation. |
+| A repository owner approves managed bootstrap installation, update or removal. | `integration plan --tool <tool> --operation <operation> --repo-root <root>`; inspect both identities, then `integration apply` with the same tool/operation/root and `--expect-transaction` plus `--expect-desired-state`. | The native transaction changes only the selected bootstrap and cooperative baseline; unknown content, local edits, stale identities and invalid baselines block mutation. Ready/passed exits 0; classified conflicts or recovery states exit 1 with a report. Text/color are opt-in. |
+| A managed file transaction was interrupted. | `integration recover --repo-root <root> --transaction <pending-id> --action <action>`; select resume or rollback explicitly. | Recovery does not generate the current source or infer a tool. Its result is historical; inspect current files separately. Finish v2 desired-absence recovery before downgrading. |
 | The repository may already contain a materialized Proofkit project. | `status --repo-root <caller-selected-root>` for the full bounded classification or `next --repo-root <caller-selected-root>` for its single action projection. | Treat `verification_required` as a request to run repository-owned verification, never as completion or approval. Stop on blocked or recovery-required states; the packet does not execute its route or own policy. |
 | The agent does not know where to start. | `adopt plan --mode <mode> --repo-root <caller-selected-root>`, where mode is `fresh`, `code-baseline`, or `audit-from-code` | Choose the trust intent explicitly. Treat the fixed-catalog inventory and tasks as a read-only candidate plan; stop before arbitrary source inspection, writing files, or making requirements authoritative. |
 | An agent needs a bounded, deterministic stage transition for an engineering change. | `change plan` selects the optional built-in `proofkit.reviewed-change.v1` profile; use `--agent-envelope` for the compact work packet and `native-evidence-guidance` when the consuming repository has not yet materialized repository-specific evidence instructions. | Supply only explicit current checkpoint, completed stages, and admitted context references. Apply conditional guidance slots only when their applicability class matches a declared consumer mechanism. Stop before treating the profile, plan, or guidance as repository policy or as proof that a stage ran, evidence exists, review passed, or merge/release is authorized. |

docs/specs/proofkit-agent-workflow/overview.md

@@ -28,7 +28,7 @@ The public capability is deliberately small:
    bootstrap without reading repositories or writing files;
    `integration check --tool <claude|codex> --repo-root <path>` compares only
    the selected descriptor-owned file through confined read-only inspection.
-   These are generation/check targets, not managed integration support.
+   Generation/check remain read-only; separate lifecycle routes manage files.
 
 The change planner and evidence-guidance cores are stateless pure projections.
 Project status reads only an explicit repository root, the conventional routing
@@ -132,9 +132,15 @@ identity and a bounded freshness classification, never observed content, its
 digest, or caller root paths. Exit 0 means current, exit 2 means a classified
 missing/stale/invalid file, and exit 1 means an invocation or operation error.
 Source returns 0 on success and 1 on error. Neither accepts `--output` or an
-install option. Manual export guidance is owned by `ADOPTION.md`.
+install option. Managed lifecycle guidance is owned by `ADOPTION.md`.
 
-Phase5B managed installation, update, and safe removal remains explicitly open.
+`REQ-PROOFKIT-WORKFLOW-019` owns `integration plan`, `integration apply`, and
+`integration recover`. A reviewed install/update/remove changes only the
+selected bootstrap and its canonical cooperative baseline through the existing
+repository transaction owner. Both expected identities are required for apply;
+local edits or malformed baselines block mutation. Recovery uses historical
+journal state without assuming the current tool renderer. Desired absence
+selects journal v2, while present-only v1 identities and recovery remain stable.
 Host discovery, body loading, and approved-launcher invocation require separate
 isolated native-host observations; direct CLI execution cannot prove skill use.