Add transactional adoption materialization

docs/proofkit-contract-map.md

@@ -40,7 +40,7 @@ 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 |
-| Adoption and scaffolding | `adopt plan`, `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, 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, 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, final files, final requirements, rollout policy, text extraction, code observation extraction, and pilot truth | inventory, candidate-only plan, selected child output, report, seed packet, or agent envelope |
+| 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 |
 | Test inventory and coverage | `test-evidence-inventory`, `test-evidence-inventory --projection discovery-draft`, `test-evidence-inventory --normalized-inventory`, `requirement-coverage-input-compose`, `requirement-coverage-view`, `requirement-browser-server --view coverage` | caller-owned direct or source-set test inventory, caller-owned explicit test discovery facts, declared quality findings, requirement source, proof binding or compact proof contract, coverage universe, optional owner-invariant registry, aggregate coverage compose input | strict inventory/source-set admission, candidate-only discovery draft projection, fail-closed normalized inventory projection, deterministic coverage-view input composition from explicit facts, missing declared assertion-signal and declared-quality classification, bounded agent action guidance, requirement/test/command/owner-invariant joins, nonsemantic command-evidence classification, stable coverage failure/warning classifications, presentation-only coverage view | inventory completeness, oracle quality, test quality, test discovery extraction, native test execution, receipt freshness, producer trust, merge policy | candidate inventory guidance, inventory report, normalized inventory data product, coverage-view input, coverage view, or browser presentation |
@@ -132,6 +132,7 @@ Semantic context routes are `requirement-context-compose`,
 | 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. |
 | 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. |
 | Candidate boundary is uncertain. | `adoption-doctor` or `gradual-adoption-guidance --agent-envelope` | Escalate to owner review when the boundary is advisory, ambiguous, or missing native witnesses. |
 | Temporary external design, implementation-plan, PR, code, or test observations may contain durable requirements. | `requirement-authoring-plan` | Treat output as candidate-only; stop before writing `requirements.v1.json`, retaining temporary documents, or claiming requirement meaning. |
 | Requirement records exist. | `requirement-source-admission`; use `requirement-source-transition` for lifecycle changes. | Escalate when blocking requirements lack proof routes or lifecycle replacement ids are incomplete. |

docs/specs/proofkit-spec-proof-core/overview.md

@@ -190,6 +190,16 @@ execution receipts, and merge policy.
 - `REQ-PROOFKIT-SPEC-031`: the adoption version edge binds exact ABI, command,
   contract, generated-artifact, and release-change inventories while proving
   that the retired `init` route has no remaining public owner.
+- `REQ-PROOFKIT-SPEC-032`: adoption materialization admits candidate artifacts
+  through their existing owners, proves cross-record closure, and binds a
+  read-only plan plus apply and recovery receipts to complete state identities.
+- `REQ-PROOFKIT-SPEC-033`: repository transactions confine bounded immutable
+  plans, private journals, atomic target replacement, exact rollback, and
+  action-stable replay recovery without claiming repository-wide atomicity.
+- `REQ-PROOFKIT-SPEC-034`: the pre-materialization-to-transactional-
+  materialization public version edge binds all three transactional
+  materialization routes and their exact public contracts to a compatible
+  release record without reinterpreting the frozen prior edge.
 
 ## Non-Claims
 

docs/specs/proofkit-spec-proof-core/requirements.v1.json

@@ -650,7 +650,7 @@
     {
       "requirementId": "REQ-PROOFKIT-SPEC-031",
       "ownerId": "proofkit.spec-proof-core",
-      "invariant": "The adoption-front-door public version edge binds the exact previous and current public ABI digests, the exact removal of init, the exact addition of adopt plan and repository-inventory, one explicit selection policy covering every command whose declared input-contract identifier changed while leaving source-bound digest churn to the enclosing ABI digests, the live current input-contract identifier and wire schema of every selected command, every changed generated artifact identity, and the ordered breaking and additive change inventories to one digest-bound release change record; the superseded init route has no active descriptor, dispatcher, CLI contract, command family, or package owner.",
+      "invariant": "The frozen 0.6.0-to-0.7.0 adoption-front-door public version edge binds the exact previous and released public ABI digests, the exact removal of init, the exact addition of adopt plan and repository-inventory, one explicit selection policy covering every command whose declared input-contract identifier changed while leaving source-bound digest churn to the enclosing ABI digests, the released input-contract identifier and wire schema of every selected command, every changed generated artifact identity, and the ordered breaking and additive change inventories to one digest-bound frozen release change record; the superseded init route has no active descriptor, dispatcher, CLI contract, command family, or package owner, and later releases cannot reinterpret this historical edge through live contract metadata.",
       "claimLevel": "blocking",
       "riskClass": "high",
       "proofBindingRefs": ["proofkit/requirement-bindings.json"],
@@ -659,6 +659,45 @@
       "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
       "deferral": null,
       "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
+    },
+    {
+      "requirementId": "REQ-PROOFKIT-SPEC-032",
+      "ownerId": "proofkit.spec-proof-core",
+      "invariant": "Adoption materialization fully admits one candidate packet through the existing requirement-source, requirement-binding, test-inventory, repository-inventory, and adoption-plan owners; proves exact cross-record identity and reference closure; derives canonical child-owned bytes plus one routing-only manifest without mirroring child field semantics; and emits a deterministic read-only plan whose transaction and desired-state identities bind the complete admitted before and after states. Apply recomputes that complete plan and requires both expected identities before any mutation, recovery accepts only one observed transaction identity and one state-compatible action, every plan and receipt is closed under its own output admission, and caller review declarations remain declarations rather than requirement, proof, execution, or approval evidence.",
+      "claimLevel": "blocking",
+      "riskClass": "critical",
+      "proofBindingRefs": ["proofkit/requirement-bindings.json"],
+      "nonClaimRefs": ["NC-PROOFKIT-SPEC-032"],
+      "nonClaims": ["Materialization does not infer requirement meaning, authenticate witness truth or freshness, execute native witnesses, approve merge or release, establish rollout or production readiness, or make its routing manifest a second semantic owner."],
+      "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
+      "deferral": null,
+      "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
+    },
+    {
+      "requirementId": "REQ-PROOFKIT-SPEC-033",
+      "ownerId": "proofkit.spec-proof-core",
+      "invariant": "The repository-transaction owner confines every effect to one explicit repository root; freezes a bounded canonical execution plan before effects; rejects non-canonical, reserved, symlinked, case-folding, Unicode-folding, and prefix-alias target identities; keeps staged payloads, backups, ownership records, and publish temporaries in one private transaction namespace; records each created directory by exact filesystem identity; and performs each target replacement by same-filesystem atomic rename. A bounded durable journal identifies the exact before-state prefix, applied-target count, and terminal result; apply fails closed on stale state, unknown control records, and cooperative concurrency; rollback removes only transaction-owned artifacts and restores exact bytes and modes; resume and rollback are state-compatible, action-stable, cancellation-aware, and replay-idempotent; terminal receipts preserve the complete observable result until a later valid transaction replaces them. These guarantees cover process interruption at every injected mutation boundary but do not claim filesystem-wide atomic visibility, power-loss durability beyond successful synchronization, protection from arbitrary readers, or safety against a non-cooperative same-user process mutating the private namespace.",
+      "claimLevel": "blocking",
+      "riskClass": "critical",
+      "proofBindingRefs": ["proofkit/requirement-bindings.json"],
+      "nonClaimRefs": ["NC-PROOFKIT-SPEC-033"],
+      "nonClaims": ["Repository transactions do not provide multi-file atomic visibility to concurrent arbitrary readers, distributed transactions, protection from a hostile same-user process, or stronger power-loss durability than the admitted filesystem synchronization operations."],
+      "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
+      "deferral": null,
+      "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
+    },
+    {
+      "requirementId": "REQ-PROOFKIT-SPEC-034",
+      "ownerId": "proofkit.spec-proof-core",
+      "invariant": "The 0.7.0-to-0.8.0 public version edge binds the exact previous and current public ABI digests; the exact addition of adopt materialize plan, apply, and recover with their public routes and input/output contract identities and digests; an explicit added-command selection policy; and the complete ordered additive inventory to one digest-bound current release change record. The edge is compatible, contains no breaking changes or migration steps, and does not mutate or reinterpret the frozen 0.6.0-to-0.7.0 edge.",
+      "claimLevel": "blocking",
+      "riskClass": "high",
+      "proofBindingRefs": ["proofkit/requirement-bindings.json"],
+      "nonClaimRefs": ["NC-PROOFKIT-SPEC-034"],
+      "nonClaims": ["A source-bound version edge does not authenticate registry publication, provider ingestion, consumer adoption, native witness truth, rollout, or production readiness."],
+      "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
+      "deferral": null,
+      "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
     }
   ],
   "nonClaims": [

go.mod

@@ -14,6 +14,8 @@ require (
 	github.com/mattn/go-isatty v0.0.24
 	go.yaml.in/yaml/v3 v3.0.5
 	golang.org/x/mod v0.40.0
+	golang.org/x/sys v0.47.0
+	golang.org/x/text v0.41.0
 	golang.org/x/tools v0.49.0
 )
 
@@ -31,7 +33,6 @@ require (
 	go.yaml.in/yaml/v4 v4.0.0-rc.3 // indirect
 	golang.org/x/exp/typeparams v0.0.0-20260824195058-e88cd73687aa // indirect
 	golang.org/x/sync v0.22.0 // indirect
-	golang.org/x/sys v0.47.0 // indirect
 	golang.org/x/telemetry v0.0.0-20260902144106-3ef544be8421 // indirect
 	golang.org/x/vuln v1.7.0 // indirect
 	honnef.co/go/tools v0.8.1 // indirect

go.sum

@@ -38,6 +38,8 @@ golang.org/x/sys v0.47.0 h1:o7XGOvZQCADBQQ4Y7VNq2dRWQR7JmOUW8Kxx4ZsNgWs=
 golang.org/x/sys v0.47.0/go.mod h1:4GL1E5IUh+htKOUEOaiffhrAeqysfVGipDYzABqnCmw=
 golang.org/x/telemetry v0.0.0-20260902144106-3ef544be8421 h1:o5Q1WWgqIjOriF3xZyV3Y32kRr4lbgdHDbg2Wdw8/i0=
 golang.org/x/telemetry v0.0.0-20260902144106-3ef544be8421/go.mod h1:/KSYFnLndIrA1A+Rs5r6vSifQhuFz75BPNN3J/hvzN0=
+golang.org/x/text v0.41.0 h1:vz/seA0lnX87Othu2f/0L24RcgrXD9/YFTSuGjj3rH8=
+golang.org/x/text v0.41.0/go.mod h1:jvf1O8ajNzZqhSrQBPbutR/EB83Cc0CFrezNQIwbb5M=
 golang.org/x/tools v0.49.0 h1:3NI7VXzL9+1WZD52Dx2ttoPwD5DWrFGpl9mFZDlmisI=
 golang.org/x/tools v0.49.0/go.mod h1:SJNXV9DBKT0UbdttsQjbfJlAE/q+y36++zo3uL3N0Oo=
 golang.org/x/tools/go/expect v0.1.1-deprecated h1:jpBZDwmgPhXsKZC6WhL20P4b/wmnpsEAGHaNy0n/rJM=