Add the typed requirement source model

BACKLOG.md

@@ -48,8 +48,7 @@ records, generated release manifests, or the owning docs named above.
 
 | Status | ID | Scope | Completion condition |
 |---|---|---|---|
-| NEXT | SOURCE-MODEL-01 | Define one representation-neutral typed requirement-source v2 model before selecting a source syntax. | A private bounded model admits atomic requirement identities, grouped authoring, premises, scenarios, definitions, vocabulary, lifecycle, references, and deterministic normalization; an independently authored field/variant completeness manifest plus mutant corpus proves every normative field reaches each required downstream owner, with no production parser or persisted normalized mirror. |
-| BLOCKED | SOURCE-CODEC-01 | Select at most one compact source codec without creating dual authority. | After `SOURCE-MODEL-01`, one versioned experiment manifest freezes disjoint role sets: the flat-v1 baseline control, grouped-model ablations, and exactly complete grouped-JSON plus at most one complete restricted-DSL codec candidate over the same model. Only codec candidates can win the predeclared replacement relation; controls and ablations measure causality and cannot become production grammars. A newly discovered candidate requires a new manifest version and complete experiment. A frozen corpus and strict `Replace(candidate, grouped-json)` predicate cover grammar completeness, safety, semantic parity, diagnostics, canonical bytes, review accuracy, token cost, diff amplification, parse/format cost, and unknowns. Every metric is classified exactly once by a versioned registry with role, direction, baseline pair, aggregation, material threshold, primary decision requirement, and missing-observation semantics; duplicate or unclassified metrics fail admission, hard constraints cannot trade off, report-only metrics cannot decide replacement, promised byte/token reductions must be materially better, and bounded diff/parse costs must be noninferior. If grouped JSON fails its hard gate, retain the current flat v1 source and perform no v2 cutover; otherwise select the restricted text candidate only when it is the unique strict replacement, while a tie, unknown, incomparability, or non-material improvement selects grouped JSON. The losing parser and formatter are deleted before experiment closeout, and production admits exactly one grammar. |
+| NEXT | SOURCE-CODEC-01 | Select at most one compact source codec without creating dual authority. | After `SOURCE-MODEL-01`, one versioned experiment manifest freezes disjoint role sets: the flat-v1 baseline control, grouped-model ablations, and exactly complete grouped-JSON plus at most one complete restricted-DSL codec candidate over the same model. Only codec candidates can win the predeclared replacement relation; controls and ablations measure causality and cannot become production grammars. A newly discovered candidate requires a new manifest version and complete experiment. A frozen corpus and strict `Replace(candidate, grouped-json)` predicate cover grammar completeness, safety, semantic parity, diagnostics, canonical bytes, review accuracy, token cost, diff amplification, parse/format cost, and unknowns. Every metric is classified exactly once by a versioned registry with role, direction, baseline pair, aggregation, material threshold, primary decision requirement, and missing-observation semantics; duplicate or unclassified metrics fail admission, hard constraints cannot trade off, report-only metrics cannot decide replacement, promised byte/token reductions must be materially better, and bounded diff/parse costs must be noninferior. If grouped JSON fails its hard gate, retain the current flat v1 source and perform no v2 cutover; otherwise select the restricted text candidate only when it is the unique strict replacement, while a tie, unknown, incomparability, or non-material improvement selects grouped JSON. The losing parser and formatter are deleted before experiment closeout, and production admits exactly one grammar. |
 | 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/specs/proofkit-spec-proof-core/overview.md

@@ -142,6 +142,14 @@ execution receipts, and merge policy.
   evidence planes, consumes the normalized v1/v2 context boundary, and accepts
   code topology only as explicit caller-owned input with source-digest,
   parent-edge, abstraction-order, and pre-materialization budget closure.
+- `REQ-PROOFKIT-SPEC-024`: a private representation-neutral requirement-source
+  v2 model separates immutable atomic, authoring-layout, and typed-reference
+  projections, closes every metadata owner, group-member relation, and typed
+  reference under independently observed input, instantiated-scenario, and
+  expanded-output bounds with fixed budget-error precedence, and proves exact
+  package, field, representation, variant, and positive/negative relation
+  coverage without attributing correlated edits to independent field
+  causality, selecting a codec, or changing a public source boundary.
 
 ## Non-Claims
 

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

@@ -555,6 +555,19 @@
       "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
       "deferral": null,
       "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
+    },
+    {
+      "requirementId": "REQ-PROOFKIT-SPEC-024",
+      "ownerId": "proofkit.spec-proof-core",
+      "invariant": "A private representation-neutral requirement-source v2 model admits one bounded source into immutable atomic, authoring-layout, and typed-reference projections; it preserves atomic requirement identity while expanding grouped statement stems and premises, preserves group-to-member relations under composite identity, assigns every effective metadata field to exactly one resolving profile or member owner, admits lifecycle, deferral, update-policy, scenario, vocabulary, non-claim, and derivation semantics through closed variants and references, applies architecture-independent input, instantiated-scenario, and expanded-materialization cardinality and text budgets in a fixed precedence before per-item semantic work, rejects both lexical and single-pass parameter-instantiated observation contradictions, normalizes admitted set-like values deterministically, emits nondisclosing diagnostics deterministically for each exact input, and preserves ordered action sequences. An independently authored exact typed-field and closed-variant manifest plus an identity-aware admitted semantic mutant corpus proves individual field projection, both metadata-owner branches, or an explicitly named referential relation with negative near-miss controls and without attributing correlated edits to independent field causality; independent structural observers prove exact package exports and direct imports, representation neutrality, exact input, instantiated-scenario, and expanded-output costs, and exact versus limit-minus-one budget behavior.",
+      "claimLevel": "blocking",
+      "riskClass": "high",
+      "proofBindingRefs": ["proofkit/requirement-bindings.json"],
+      "nonClaimRefs": ["NC-PROOFKIT-SPEC-024"],
+      "nonClaims": ["This private single-source model does not select or expose a source codec, parse or serialize a persisted source, retain a normalized mirror, establish cross-source requirement identity, authenticate derivation objects, digests, selectors, or freshness, authenticate a caller-declared sourceKind or prove its author's authority or trust class, cut over any current requirement consumer, prove requirement meaning or implementation correctness, execute native witnesses, approve merge or release, or establish rollout or production readiness."],
+      "lifecycle": {"state": "active", "replacementRequirementIds": [], "evidenceRefs": []},
+      "deferral": null,
+      "updatePolicy": {"reviewOwnerId": "proofkit.spec-proof-core", "requiresImpactDeclaration": true, "requiresProofBindingReview": true}
     }
   ],
   "nonClaims": [

internal/kernel/requirementsourcemodel/accessor_immutability_test.go

@@ -0,0 +1,155 @@
+package requirementsourcemodel
+
+import (
+	"reflect"
+	"testing"
+)
+
+func assertAccessorReturnsDetachedState[T any](t *testing.T, name string, accessor func() T) {
+	t.Helper()
+	baseline := detachedTestCopy(accessor())
+	mutated := accessor()
+	mutationCount := mutateReferencedState(reflect.ValueOf(&mutated).Elem(), false)
+	if mutationCount == 0 || reflect.DeepEqual(mutated, baseline) {
+		t.Fatalf("%s fixture exposes no mutable reference state", name)
+	}
+	if fresh := accessor(); !reflect.DeepEqual(fresh, baseline) {
+		t.Fatalf("%s accessor exposed mutable owner state after %d independent mutations", name, mutationCount)
+	}
+}
+
+func detachedTestCopy[T any](value T) T {
+	copy := deepCopyTestValue(reflect.ValueOf(value))
+	return copy.Interface().(T)
+}
+
+func deepCopyTestValue(value reflect.Value) reflect.Value {
+	if !value.IsValid() {
+		return value
+	}
+	switch value.Kind() {
+	case reflect.Interface:
+		if value.IsNil() {
+			return reflect.Zero(value.Type())
+		}
+		result := reflect.New(value.Type()).Elem()
+		result.Set(deepCopyTestValue(value.Elem()))
+		return result
+	case reflect.Pointer:
+		if value.IsNil() {
+			return reflect.Zero(value.Type())
+		}
+		result := reflect.New(value.Type().Elem())
+		result.Elem().Set(deepCopyTestValue(value.Elem()))
+		return result
+	case reflect.Slice:
+		if value.IsNil() {
+			return reflect.Zero(value.Type())
+		}
+		result := reflect.MakeSlice(value.Type(), value.Len(), value.Len())
+		for index := 0; index < value.Len(); index++ {
+			result.Index(index).Set(deepCopyTestValue(value.Index(index)))
+		}
+		return result
+	case reflect.Map:
+		if value.IsNil() {
+			return reflect.Zero(value.Type())
+		}
+		result := reflect.MakeMapWithSize(value.Type(), value.Len())
+		iterator := value.MapRange()
+		for iterator.Next() {
+			result.SetMapIndex(deepCopyTestValue(iterator.Key()), deepCopyTestValue(iterator.Value()))
+		}
+		return result
+	case reflect.Struct:
+		result := reflect.New(value.Type()).Elem()
+		for index := 0; index < value.NumField(); index++ {
+			result.Field(index).Set(deepCopyTestValue(value.Field(index)))
+		}
+		return result
+	case reflect.Array:
+		result := reflect.New(value.Type()).Elem()
+		for index := 0; index < value.Len(); index++ {
+			result.Index(index).Set(deepCopyTestValue(value.Index(index)))
+		}
+		return result
+	default:
+		return value
+	}
+}
+
+func mutateReferencedState(value reflect.Value, behindReference bool) int {
+	if !value.IsValid() {
+		return 0
+	}
+	switch value.Kind() {
+	case reflect.Interface:
+		if value.IsNil() {
+			return 0
+		}
+		copy := reflect.New(value.Elem().Type()).Elem()
+		copy.Set(value.Elem())
+		count := mutateReferencedState(copy, behindReference)
+		if count != 0 && value.CanSet() {
+			value.Set(copy)
+		}
+		return count
+	case reflect.Pointer:
+		if value.IsNil() {
+			return 0
+		}
+		return mutateReferencedState(value.Elem(), true)
+	case reflect.Slice:
+		count := 0
+		for index := 0; index < value.Len(); index++ {
+			count += mutateReferencedState(value.Index(index), true)
+		}
+		return count
+	case reflect.Map:
+		count := 0
+		iterator := value.MapRange()
+		for iterator.Next() {
+			entry := reflect.New(value.Type().Elem()).Elem()
+			entry.Set(iterator.Value())
+			entryCount := mutateReferencedState(entry, true)
+			if entryCount != 0 {
+				value.SetMapIndex(iterator.Key(), entry)
+				count += entryCount
+			}
+		}
+		return count
+	case reflect.Struct:
+		count := 0
+		for index := 0; index < value.NumField(); index++ {
+			count += mutateReferencedState(value.Field(index), behindReference)
+		}
+		return count
+	case reflect.Array:
+		count := 0
+		for index := 0; index < value.Len(); index++ {
+			count += mutateReferencedState(value.Index(index), behindReference)
+		}
+		return count
+	case reflect.String:
+		if behindReference && value.CanSet() {
+			value.SetString(value.String() + ".mutated")
+			return 1
+		}
+	case reflect.Bool:
+		if behindReference && value.CanSet() {
+			value.SetBool(!value.Bool())
+			return 1
+		}
+	case reflect.Int, reflect.Int8, reflect.Int16, reflect.Int32, reflect.Int64:
+		if behindReference && value.CanSet() {
+			value.SetInt(value.Int() + 1)
+			return 1
+		}
+	case reflect.Uint, reflect.Uint8, reflect.Uint16, reflect.Uint32, reflect.Uint64:
+		if behindReference && value.CanSet() {
+			value.SetUint(value.Uint() + 1)
+			return 1
+		}
+	}
+	return 0
+}

internal/kernel/requirementsourcemodel/clone.go

@@ -0,0 +1,182 @@
+package requirementsourcemodel
+
+func cloneDraft(value Draft) Draft {
+	profiles := make([]Profile, len(value.Profiles))
+	for index, profile := range value.Profiles {
+		profiles[index] = Profile{ProfileID: profile.ProfileID, Fields: cloneMetadataFields(profile.Fields)}
+	}
+	groups := make([]Group, len(value.Groups))
+	for index, group := range value.Groups {
+		groups[index] = cloneGroup(group)
+	}
+	derivations := make([]Derivation, len(value.Derivations))
+	for index, derivation := range value.Derivations {
+		derivations[index] = cloneDerivation(derivation)
+	}
+	return Draft{
+		SourceID:            value.SourceID,
+		SpecPackagePath:     value.SpecPackagePath,
+		SourceNonClaimRefs:  cloneStrings(value.SourceNonClaimRefs),
+		NonClaimDefinitions: append([]NonClaimDefinition(nil), value.NonClaimDefinitions...),
+		Vocabulary:          append([]VocabularyTerm(nil), value.Vocabulary...),
+		Derivations:         derivations,
+		Profiles:            profiles,
+		Groups:              groups,
+		Scenarios:           cloneScenarios(value.Scenarios),
+	}
+}
+
+func cloneAtomicProjection(value AtomicProjection) AtomicProjection {
+	return AtomicProjection{
+		SourceID:            value.SourceID,
+		SpecPackagePath:     value.SpecPackagePath,
+		SourceNonClaimRefs:  cloneStrings(value.SourceNonClaimRefs),
+		NonClaimDefinitions: append([]NonClaimDefinition(nil), value.NonClaimDefinitions...),
+		Vocabulary:          append([]VocabularyTerm(nil), value.Vocabulary...),
+		Requirements:        cloneAtomicRequirements(value.Requirements),
+		Scenarios:           cloneScenarios(value.Scenarios),
+	}
+}
+
+func cloneAtomicRequirements(values []AtomicRequirement) []AtomicRequirement {
+	result := make([]AtomicRequirement, len(values))
+	for index, value := range values {
+		result[index] = AtomicRequirement{
+			RequirementID:  value.RequirementID,
+			Invariant:      value.Invariant,
+			SharedPremises: cloneStrings(value.SharedPremises),
+			OwnerID:        value.OwnerID,
+			ClaimLevel:     value.ClaimLevel,
+			RiskClass:      value.RiskClass,
+			NonClaimRefs:   cloneStrings(value.NonClaimRefs),
+			Lifecycle:      cloneLifecycle(value.Lifecycle),
+			Deferral:       cloneDeferral(value.Deferral),
+			UpdatePolicy:   value.UpdatePolicy,
+		}
+	}
+	return result
+}
+
+func cloneLayoutProjection(value LayoutProjection) LayoutProjection {
+	profiles := make([]Profile, len(value.Profiles))
+	for index, profile := range value.Profiles {
+		profiles[index] = Profile{ProfileID: profile.ProfileID, Fields: cloneMetadataFields(profile.Fields)}
+	}
+	groups := make([]Group, len(value.Groups))
+	for index, group := range value.Groups {
+		groups[index] = cloneGroup(group)
+	}
+	origins := make([]Origin, len(value.Origins))
+	for index, origin := range value.Origins {
+		origins[index] = Origin{
+			RequirementID: origin.RequirementID,
+			GroupID:       origin.GroupID,
+			ProfileID:     origin.ProfileID,
+			FieldOwners:   append([]FieldOwner(nil), origin.FieldOwners...),
+		}
+	}
+	return LayoutProjection{SourceID: value.SourceID, Profiles: profiles, Groups: groups, Origins: origins}
+}
+
+func cloneReferenceProjection(value ReferenceProjection) ReferenceProjection {
+	derivations := make([]Derivation, len(value.Derivations))
+	for index, derivation := range value.Derivations {
+		derivations[index] = cloneDerivation(derivation)
+	}
+	return ReferenceProjection{
+		SourceID:    value.SourceID,
+		Derivations: derivations,
+		Edges:       append([]ReferenceEdge(nil), value.Edges...),
+	}
+}
+
+func cloneGroup(value Group) Group {
+	members := make([]Member, len(value.Members))
+	for index, member := range value.Members {
+		members[index] = Member{
+			RequirementID:       member.RequirementID,
+			StatementCompletion: member.StatementCompletion,
+			Fields:              cloneMetadataFields(member.Fields),
+		}
+	}
+	return Group{
+		GroupID:        value.GroupID,
+		ProfileID:      value.ProfileID,
+		StatementStem:  value.StatementStem,
+		SharedPremises: cloneStrings(value.SharedPremises),
+		Members:        members,
+	}
+}
+
+func cloneMetadataFields(value MetadataFields) MetadataFields {
+	result := value
+	if value.NonClaimRefs.Present {
+		result.NonClaimRefs.Value = cloneStrings(value.NonClaimRefs.Value)
+	}
+	if value.Lifecycle.Present {
+		result.Lifecycle.Value = cloneLifecycle(value.Lifecycle.Value)
+	}
+	if value.Deferral.Present {
+		result.Deferral.Value = cloneDeferral(value.Deferral.Value)
+	}
+	return result
+}
+
+func cloneLifecycle(value Lifecycle) Lifecycle {
+	return Lifecycle{
+		State:                     value.State,
+		ReplacementRequirementIDs: cloneStrings(value.ReplacementRequirementIDs),
+		EvidenceRefs:              cloneStrings(value.EvidenceRefs),
+	}
+}
+
+func cloneDeferral(value *Deferral) *Deferral {
+	if value == nil {
+		return nil
+	}
+	result := *value
+	result.EvidenceRefs = cloneStrings(value.EvidenceRefs)
+	return &result
+}
+
+func cloneScenarios(values []Scenario) []Scenario {
+	result := make([]Scenario, len(values))
+	for index, value := range values {
+		examples := make([]Example, len(value.Examples))
+		for exampleIndex, example := range value.Examples {
+			items := make(map[string]ScenarioValue, len(example.Values))
+			for key, item := range example.Values {
+				items[key] = item
+			}
+			examples[exampleIndex] = Example{ExampleID: example.ExampleID, Values: items}
+		}
+		result[index] = Scenario{
+			ScenarioID:            value.ScenarioID,
+			RequirementIDs:        cloneStrings(value.RequirementIDs),
+			Parameters:            cloneStrings(value.Parameters),
+			Preconditions:         cloneStrings(value.Preconditions),
+			ActionSequence:        cloneStrings(value.ActionSequence),
+			ExpectedObservations:  cloneStrings(value.ExpectedObservations),
+			ForbiddenObservations: cloneStrings(value.ForbiddenObservations),
+			Examples:              examples,
+			VocabularyRefs:        cloneStrings(value.VocabularyRefs),
+			NonClaimRefs:          cloneStrings(value.NonClaimRefs),
+		}
+	}
+	return result
+}
+
+func cloneDerivation(value Derivation) Derivation {
+	return Derivation{
+		DerivationID:   value.DerivationID,
+		SourceKind:     value.SourceKind,
+		SourceRef:      value.SourceRef,
+		Selector:       value.Selector,
+		RequirementIDs: cloneStrings(value.RequirementIDs),
+		NonClaimRefs:   cloneStrings(value.NonClaimRefs),
+	}
+}
+
+func cloneStrings(values []string) []string {
+	return append([]string(nil), values...)
+}