Add portable agent bootstrap sources and freshness checks

ADOPTION.md

@@ -196,6 +196,67 @@ the proof binding already contains safe witness command facts and the caller
 provides witness command vocabulary. The projection avoids duplicated command
 identity; native execution and command freshness remain caller-owned.
 
+## Portable Agent Bootstrap
+
+`REQ-PROOFKIT-WORKFLOW-016` through `REQ-PROOFKIT-WORKFLOW-018` own the bounded
+Phase5A generation/check contract. Use `integration source --tool codex` or
+`integration source --tool claude` through a repository-approved, already
+installed launcher. JSON is the default and includes the exact generated
+content, descriptor-owned target path, materialization identity, content and
+consumed-capability digests, and separate metadata/body byte counts. Text is
+the exact file content. The limits are 512 metadata bytes and 4096 body bytes,
+not tokenizer-specific token counts.
+
+The fixed repository paths are `.agents/skills/agentic-proofkit/SKILL.md` for
+`codex` and `.claude/skills/agentic-proofkit/SKILL.md` for `claude`. Neither tool
+is selected implicitly; selecting one does not inspect the other location.
+The generator reads no repository files, writes nothing, and has no `--output`
+or install option. Generated instructions contain no hooks or permission grants
+and delegate policy, planning, and evidence semantics to current owners.
+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.
+
+```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 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.
+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
+`missing`, `stale`, or `invalid`; exit 1 reports an invocation or operational
+error, including denied reads, ambiguous paths, observed changes, cancellation,
+or cleanup failure. It never prints observed bytes, their digest, or caller
+root paths. Source exits 0 on successful generation and 1 on error.
+
+Generated identity binds the shared template, selected descriptor, and exact
+consumed registered public invocation contracts. Package version is absent
+from the generated bytes; version-only or unrelated-command changes preserve
+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
+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
+controls; a prompt directly requesting CLI execution is not skill-use evidence.
+Removing a file does not revoke instructions already loaded into host context.
+
 ## Requirement, Contract, And Test Order
 
 The durable semantic source is the repository-owned requirement package:

BACKLOG.md

@@ -48,6 +48,7 @@ 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. |

NON_CLAIMS.md

@@ -36,6 +36,24 @@ This repository state does not claim:
 Consuming repositories must keep their own specifications, proof bindings,
 native witnesses, CI gates, rollback policy, and rollout decisions.
 
+Phase5A integration source/check implements only bounded portable generation
+and read-only generated-byte freshness. It does not install, update, remove,
+repair, activate host instructions, grant tool permissions, or authorize native
+execution. Phase5B managed lifecycle remains open; manual shell export does not
+close it. `current` neither proves semantic full proof nor guarantees stability
+after return. Consumed registered-contract identity is not complete transitive
+native-semantic identity, and byte budgets are not token counts.
+
+Declared witness routes do not prove execution. Installed npm/Python integration
+smokes and final frozen-tree closure require actual execution against the named
+source and artifacts. Native-host discovery, body loading, and approved-launcher
+invocation require separate isolated evidence; direct CLI calls cannot prove
+skill use. Removing an on-disk file does not revoke already-loaded instructions.
+Read-only checks do not suppress filesystem-owned access metadata updates or
+exclude uncooperative writers. Cancellation after the final pre-emission check
+cannot retract bytes accepted by an external stdout writer, and prefix-accepting
+transport failure does not imply an atomic sink.
+
 Reference infrastructure boundary:
 
 ```text

docs/proofkit-contract-map.md

@@ -41,6 +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 |
 | 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 |
@@ -131,6 +132,7 @@ 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. |
 | 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

@@ -24,6 +24,11 @@ The public capability is deliberately small:
    bounded action. Admitted in-bound records bind exact content digests;
    unread out-of-bound records bind only their invalid class. Neither command
    claims native execution or proof completion.
+5. `integration source --tool <claude|codex>` emits one portable static
+   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.
 
 The change planner and evidence-guidance cores are stateless pure projections.
 Project status reads only an explicit repository root, the conventional routing
@@ -92,11 +97,47 @@ projections remain independently owned by the spec-proof-core package.
   without claiming cancellation rollback or atomicity from an external sink,
   and a versioned breaking replacement
   of the flat change route by `change plan` across source and installed carriers.
+- `REQ-PROOFKIT-WORKFLOW-016`: one private descriptor/template owner, portable
+  approved-launcher guidance, 512-byte metadata and 4096-byte body limits, and
+  identity over exactly consumed registered invocation contracts rather than
+  package version or the entire command universe.
+- `REQ-PROOFKIT-WORKFLOW-017`: pre-I/O invocation admission, a confined
+  application-write-free two-observation check with an 8192-byte read bound per
+  observation, distinct missing/current/stale/invalid states, non-disclosing
+  operational failures, and independent cancellation/cleanup outcomes.
+- `REQ-PROOFKIT-WORKFLOW-018`: exact source/check CLI flags, JSON root shapes,
+  exit semantics, one source/check-only command family, and source, generated,
+  and installed-carrier closure obligations. A binding is not an execution
+  receipt; final frozen-tree and installed-carrier integration proof requires
+  actual execution against the named source and artifacts.
 
 Shared stable-JSON/diagnostic hardening is owned by the supply-chain-quality
 spec. Typed local-reference closure is owned by the existing agent-envelope
 requirement. This workflow spec consumes those owners without duplicating them.
 
+## Thin Integration Boundary
+
+The production owner is `internal/command/agentintegration`. The descriptor
+alone selects `.agents/skills/agentic-proofkit/SKILL.md` for `codex` or
+`.claude/skills/agentic-proofkit/SKILL.md` for `claude`. Source and check share
+the same renderer. Common name/description frontmatter and static Markdown
+delegate to the current CLI instead of embedding schemas or workflow policy.
+The bootstrap persists logical routes, not machine-local executable paths;
+an absent or ambiguous repository-approved installed launcher needs an owner
+decision, never an implicit package manager, install, or network fallback.
+
+The source contract's default JSON includes exact content and its digest;
+`--format text` emits those file bytes. Check returns only expected generated
+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`.
+
+Phase5B managed installation, update, and safe removal remains explicitly open.
+Host discovery, body loading, and approved-launcher invocation require separate
+isolated native-host observations; direct CLI execution cannot prove skill use.
+
 ## Non-Claims
 
 - Generated prompts are not authenticated and need not be obeyed or adequate.
@@ -106,5 +147,9 @@ requirement. This workflow spec consumes those owners without duplicating them.
 - Least dependency closure does not prove context truth, freshness, semantic
   sufficiency, or global minimality.
 - A finite pilot does not prove universal repository fit.
+- Bootstrap byte bounds are not token counts, and consumed registered-contract
+  identity is not complete transitive semantic proof.
+- Generated-byte freshness does not install, activate, authorize, or grant
+  permissions. File removal does not revoke instructions already in host context.
 - This spec does not select a persisted requirement-source codec.
 - This spec does not approve merge, release, rollout, or production readiness.