Add bounded project status workflow

.github/workflows/ci.yml

@@ -151,6 +151,9 @@ jobs:
           go-version-file: go.mod
           cache: true
 
+      - name: Run Darwin filesystem invariants
+        run: go test ./internal/kernel/rootpath ./internal/kernel/repositorytransaction ./internal/command/projectstatus -count=1
+
       - name: Run platform smoke
         run: |
           set -euo pipefail

docs/proofkit-contract-map.md

@@ -10,6 +10,8 @@ This map helps consuming repositories choose the smallest Proofkit CLI command
 or JSON contract without loading the full README or source tree. It is not an
 exhaustive schema reference. The canonical command inventory is
 `proofkit/cli-contract.v2.json`.
+Its `commandRouteGrammar.omittedRoutePolicy` field owns how consumers expand a
+command record that omits an explicit `route`.
 
 Formal rule:
 
@@ -39,7 +41,8 @@ owner boundaries. It is not a second command-family inventory.
 
 | Family | Main commands | Caller provides | Proofkit owns | Consumer owns | Output authority |
 |---|---|---|---|---|---|
-| Agent workflow planning | `change-workflow-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 |
+| 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 |
 | Requirement source | `capability-map-admission`, `requirement-authoring-plan`, `requirement-source-admission`, `requirement-source-transition`, `spec-overview-claims`, `requirement-spec-tree`, `requirement-spec-tree-view`, `requirement-source-view`, `requirement-browser-server` | `requirements.v1.json`, caller-owned capability maps, caller-owned authoring facts, overview claim extraction, explicit spec hierarchy, view options | candidate seed admission, candidate-only authoring packets, source-shape admission, lifecycle checks, explicit tree topology/source-ref admission, shared safe renderer fragments, presentation-only views | requirement meaning, extraction completeness, Markdown extraction completeness, hierarchy ownership, proof adequacy, file materialization | capability map report, authoring packet, source report, spec-tree report, rendered view, or browser presentation |
 | Requirement proof binding | `requirement-bindings`, `binding-partition`, `proof-slice`, `evidence-graph`, `requirement-proof-resolver`, `requirement-proof-source-set`, `requirement-proof-view`, `spec-proof-bundle-admission` | requirement records, bindings, witness commands, source-set facts, receipt reports, partition policy | graph validation, binding partition projection, compact slices, declaration-only compact route projection with full binding identity and role-qualified witness routes, resolver projection, bundle linkage checks | selector resolution, oracle quality, witness execution, mutation adequacy, finding completeness, proof freshness, trust, assurance, merge policy | proof report, partition report, slice, declaration lookup graph, or view |
@@ -128,8 +131,9 @@ Semantic context routes are `requirement-context-compose`,
 
 | State or goal | Next Proofkit route | Stop or escalation condition |
 |---|---|---|
+| 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-workflow-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. |
+| 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. |
 | No admitted spec/profile exists and the caller has explicit capability observations. | `capability-map-admission`; use `trustMode: "code_baseline"` only when maintainers intentionally freeze current code, otherwise use `trustMode: "audit_from_code"`. | Stop before treating seeds as stable requirements. The consumer owns observation extraction, materialization, requirement meaning, and proof adequacy. |
 | No admitted spec/profile exists and no capability observations exist. | Start with `adopt plan --mode fresh --repo-root <caller-selected-root>`; use `scaffold-project-structure`, `adoption-workflow-plan`, or `stack-preset` only as later specialist routes when an owner has selected them. | Treat front-door tasks as candidate-only. Stop before writing files; the consumer owns materialization, overwrite policy, and final requirement text. |
 | Owner-reviewed candidate requirement sources, proof bindings, and test inventory are ready for repository materialization. | Use command ID `adopt-materialize-plan` through route `adopt materialize plan --input <candidate-packet> --repo-root <caller-selected-root>`, review the exact transaction and desired-state identities, then use command ID `adopt-materialize-apply` through route `adopt materialize apply` with both expected identities. Use `adopt materialize recover` only for the exact observed transaction and state-compatible `resume` or `rollback` action. | Stop on stale state, unknown ownership, path-role collision, pending transaction, identity mismatch, or recovery-required output. A plan or receipt does not prove requirement meaning, witness truth, proof adequacy, merge approval, rollout, or production readiness. |

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

@@ -7,7 +7,7 @@ witnesses, merge, release, rollout, or production-readiness decisions.
 
 The public capability is deliberately small:
 
-1. `change-workflow-plan` admits explicit JSON and projects one next action for
+1. `change plan` admits explicit JSON and projects one next action for
    the optional built-in profile `proofkit.reviewed-change.v1`, whose ordered
    stages are `architecture`, `design`, `implementation_plan`,
    `implementation`, `verification`, `pull_request`, and `closeout`.
@@ -19,12 +19,19 @@ The public capability is deliberately small:
    the consuming witness declares the named mechanism.
 3. Existing descriptors, dispatch, command families, root-shape CLI contracts,
    agent envelopes, and package gates provide public-surface closure.
+4. `status --repo-root` classifies only a bounded normalized
+   materialized-project observation, and `next --repo-root` projects one
+   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.
 
-Neither workflow command scans a repository. Both command cores are stateless
-pure projections with no filesystem, Git, process, environment, clock, random,
-network, container, or provider dependency. Neither workflow command adds a
-setup facade, hidden route policy, external prompt resource, persisted
-experiment state, or second source codec. Agent-route brief and full
+The change planner and evidence-guidance cores are stateless pure projections.
+Project status reads only an explicit repository root, the conventional routing
+manifest, its declared children, and transaction control state through bounded
+owner-admitted transport. No workflow command executes Git, native witnesses,
+network, containers, or providers. No workflow command adds a setup facade,
+hidden route policy, external prompt resource, persisted experiment state,
+generic report interpreter, or second source codec. Agent-route brief and full
 projections remain independently owned by the spec-proof-core package.
 
 ## Requirements
@@ -69,6 +76,22 @@ projections remain independently owned by the spec-proof-core package.
   descriptor/dispatcher/family/help/root-contract/witness/generated/package
   surfaces, with npm-only non-runtime specification docs and cross-channel
   runtime behavior proof.
+- `REQ-PROOFKIT-WORKFLOW-012`: one truthful project-state owner, exhaustive
+  precedence, existing child and cross-record closure owners, and no promotion
+  of source declarations or caller status into execution evidence.
+- `REQ-PROOFKIT-WORKFLOW-013`: one application-write-free root-bound inspection
+  lease, cooperative writer exclusion, descriptor-relative exact-path
+  traversal, bounded content-cohort validation, fail-closed partial control
+  observations, one bounded retry, and a portable non-disclosing
+  normalized-observation identity.
+  Filesystem-owned read metadata such as access time is outside that guarantee.
+- `REQ-PROOFKIT-WORKFLOW-014`: one total state-to-action table, one bounded
+  next action, explicit owner decisions, and no embedded route universe.
+- `REQ-PROOFKIT-WORKFLOW-015`: status/next CLI channel and exit semantics,
+  checkpointed pre-emission failure discipline, one bounded stdout write
+  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.
 
 Shared stable-JSON/diagnostic hardening is owned by the supply-chain-quality
 spec. Typed local-reference closure is owned by the existing agent-envelope