feat(runtime): apply nested redefinition chains below composite features

.github/workflows/pr.yml

@@ -212,8 +212,8 @@ jobs:
       - name: Download the pilot library XMI
         run: ./scripts/download-pilot-library-xmi.sh
 
-      # Per-package timeout: under -race, passes and model run within 1% of go's 10m
-      # default. Matches `make test`.
+      # Per-package timeout: under -race the runtime package runs 22-29 minutes on
+      # these runners. Matches `make test`.
       - name: Run Go race tests
         run: make test
 

Makefile

@@ -208,10 +208,10 @@ conformance-pkg: ## Run the conformance suite through the public Go API (client/
 
 test: ## Run Go tests with race detection and coverage
 	@echo "Running Go race tests..."
-	@# Per-package timeout: under -race, passes and model run within 1% of go's 10m default.
+	@# Per-package timeout: under -race the runtime package runs 22-29 minutes on CI runners.
 	@# -pgo=off: coverage plus cmd/*/default.pgo trips golang/go#80891 (link: fingerprint mismatch).
-	go test -v -race -pgo=off -timeout 30m -coverprofile=coverage.txt -covermode=atomic ./...
-	go test -C $(TOOLS_DIR) -v -race -pgo=off -timeout 30m ./...
+	go test -v -race -pgo=off -timeout 45m -coverprofile=coverage.txt -covermode=atomic ./...
+	go test -C $(TOOLS_DIR) -v -race -pgo=off -timeout 45m ./...
 
 coverage: ## Write the coverage profile the SonarCloud scan reads
 	@echo "Writing coverage.txt..."

changes/unreleased/nested-redefinition.added.md

@@ -0,0 +1 @@
+- A chain redefinition written as a member of a type or usage, `attribute :>> mid.leaf.value = 99.0;`, now applies below every composite feature the chain walks — the chain-expression is a feature hosting the chain and the host is redefinable (KerML 1.0 §7.3.4, §8.3.3.3) — exactly as the nested-body form `part :>> mid { part :>> leaf { attribute :>> value = 99.0; } }` does, for declared values (`=` and `default =`), declared types, multiplicities and redefining bodies, on scalar and multi-valued intermediates alike, ranked exactly as the nested-body form written in the same body (a redefinition declared by the chain's owner or something specializing it wins; the child's type's own loses). A valued chain below a feature bound to an existing object governs the binding when it is declared in a more specific body and is rejected as a restating body when written in the same one (`feature both valued and restated in a body`); a chain declaring only a type or multiplicity conflicts with nothing. A chain crossing a `ref`, port or subject owns no object below it, so it is reported as a `redefinition-through-reference` error and never applied. (The pinned pilot evaluator accepts the notation but reads the original value — a pilot-evaluator gap.)

docs/project/pilot-differential-baseline.json

@@ -61,7 +61,7 @@
         "dir": "examples",
         "origin": "ours",
         "files": 45,
-        "digest": "sha256:9c6076ce0461ef1da3f78ae43148589e97d620bf933d7234642a84852f43b563"
+        "digest": "sha256:d4572d53fabf769532e416d0f82f0ae615fdc7fe48b86c17f976338a1e759696"
       },
       {
         "name": "probes",

docs/project/pilot-differential.md

@@ -2923,6 +2923,18 @@ the Xpect baseline is left alone; a sweep of `examples/`, `testdata/` and the bu
 with both binaries produces identical diagnostics. The 8 only-ours rejection cases are the
 control-node successions the pilot leaves as `TODO`s; the three new cases are both-reject.
 
+### Nested-redefinition chain evaluation
+
+A chain redefinition written as a member of a type or usage — `attribute :>> mid.leaf.value = 99.0;`
+— is spec semantics, not an extension: the chain parses to a feature hosting the chain
+(`semantics/nested_redefinition.go` `NestedRedefinitionsOf`,
+`runtime/nested_redefinition.go`), and the host is redefinable, so the redefinition applies
+below every composite feature the chain walks, exactly as the nested-body form does. The pinned
+pilot accepts the notation but reads the original value — a pilot-evaluator gap, not a
+divergence to report — so the pass reports nothing for a plain chain, and only a chain crossing
+a `ref`, port or subject is an error (`redefinition-through-reference`). The differential
+baseline did not move.
+
 ## Current branch movement and adjudications
 
 The settled control is a clean run of `466de743cbd46eaa6983fd8cf0cffc4097a2137f`,

docs/project/spec-compliance.md

@@ -589,6 +589,7 @@ checked after the result is bound is not a form the runtime offers, and none is
 | Semantic Rule | Implementation | Test Case | Status |
 |--------------|----------------|-----------|--------|
 | A redefining feature's declared type need not conform to the redefined feature's type: a redefinition is a subsetting (KerML 1.0, formal/2026-03-01, §8.3.3.3.6), so the redefining feature is typed by its own typings *and* the redefined feature's types (§8.3.3.3.4), and neither §8.3.3.3.6 nor SysML v2 §8.3.x declares a type-conformance constraint (the normative redefinition constraints are `validateRedefinitionDirectionConformance`, `validateRedefinitionEndConformance`, `validateRedefinitionFeaturingTypes` and `validateRedefinitionMultiplicityConformance`). The pinned pilot validator is silent on `part :>> p : B` under `part p : A` with `A`, `B` unrelated, and on `attribute :>> q : String` under `q : Integer`, and `ShapeItems.sysml` relies on it (`item :>> faces : Polygon` and `item :>> faces : PlanarSurface` under `faces : StructuredSurface`). OpenSysML still reports the unrelated-type case as `redefinition-type-mismatch`, an extension, because a redefinition typed by two unrelated types is almost always a slip — but as a **warning**, so no conforming model is rejected | `passes/constraint.go` `checkRedefinition` | `passes/constraint_test.go:TestConstraint_RedefinitionTypeMismatch`, `:TestConstraint_RedefinitionConformingTypeStaysSilent`, `:TestConstraint_ShapeItemsRedefinitionsAreNotErrors`; `passes/constraint_unions_test.go` | ⚠️ approximate (advisory warning where the specification and the reference have no rule) |
+| A chain redefinition written as a member of a type or usage (`attribute :>> mid.leaf.value = 99.0;`) applies below every composite feature the chain walks: the chain parses to a feature hosting it — the chain determines the host feature's featuring type and featured type (KerML 1.0, formal/2025-12-01, §7.3.4) — and the host is redefinable (§8.3.3.3), so the object of an affected member behaves as if the chain had been written as nested redefining usages, carrying the member's declared value (`=` or `default =`), type, multiplicity and body, evaluated in the declaring body's scope, inherited through the type's generals and applied per element of a multi-valued intermediate. A nested-body redefinition declared by the chain's owner or something specializing it wins; the child's type's own redefinition and bodies in types the owner specializes lose, as with the nested-body form — and a chain crossing a `ref`/port/subject owns nothing below it and is never applied (an error, `redefinition-through-reference`). The pinned pilot evaluator (0.62.0) accepts the notation but reads the original value; recorded as a pilot-evaluator gap | `semantics/nested_redefinition.go` `NestedRedefinitionsOf` (own members, chain targets resolved), `IsReferenceUsage`/`IsSubjectUsage`; `runtime/nested_redefinition.go` `pendingNestedRedefinitions`, `applyNestedRedefinitions`, `redefinitionContext`/`blocksChain`; `passes/nested_redefinition.go` `NestedRedefinitionPass` | `semantics/nested_redefinition_test.go`, `passes/nested_redefinition_test.go`, `runtime/robustness_nested_redefinition_test.go:TestRuntimeRobustnessNestedRedefinition`, `runtime/nested_redefinition_test.go`, conformance `nested_redefinition_chain`, `nested_redefinition_chain_equiv`, `nested_redefinition_precedence` | ✅ Faithful |
 | A usage that redefines an inherited usage (`part derived :> base { part :>> inner { … } }`) specializes what it redefines, so it keeps every nested member the redefined usage declared and overrides only what it restates | `semantics/model.go` `NewModel` (attaches the model to `resolve.Resolver`, so a redefinition target reachable only through inheritance resolves and the redefining usage gains it as a supertype), consumed by `runtime/shape.go` `FeaturesOf` over `Model.MembersOf` | `redefinition_inherited_nested_values.sysml`, `ballandchain_variant_configuration.sysml`, `robustness_test.go:deep_specialization_chain_of_redefinitions`, `conflicting_redefinitions_at_several_levels` | ✅ Faithful (multi-level chains, a redefinition of a redefinition, and conflicting restatements where the innermost wins; the merge is the inherited-member view, not a feature value-level merge in the instantiator) |
 | A union's instances are exactly those of its unioning types (KerML §8.3.3), so a type declared `classifier MyWheel unions MyWheel1, MyWheel2` conforms to every type all of its unioning types conform to, and `feature redefines rollsOn : MyWheel` redefining `rollsOn : Wheel` is well-formed. Unioning is not a generalization edge — a union inherits nothing from its members — so it is resolved separately from `DirectSupertypes` | `semantics/model.go` `Model.Conforms` → `unionConforms`, `UnioningTypes` | `passes/constraint_unions_test.go:TestConstraintRedefinitionConformsThroughUnion`, `:TestConstraintRedefinitionUnionMemberDoesNotConform`, `:TestConstraintRedefinitionUnionCycleTerminates` | ✅ Faithful (conformance only: a union's *members* are not computed. `intersects` and `differences` are read for classification rather than conformance — see the cast row — so a type is not made to conform through them) |
 | The type a redefinition must inherit the redefined feature from is the feature's *featuring* type where it declares one (`member feature CC1_snapshots :>> Occurrences::Occurrence::snapshots featured by CC1;` is featured by `CC1`, not by the feature it is written inside — KerML §7.4.5, §8.3.4.3), and a bare `feature` owned by a package has no featuring type, so nothing can inherit it and the rule does not apply; a target that is not an inherited member may still be *accessible* through the featuring context — a context conforming to the target's own featuring context, or one that redefines a common feature whose own contexts conform (the variable-feature snapshot encoding; the pilot checks accessibility, `FeatureUtil.canAccess`, not inherited membership) | `passes/constraint.go` `checkRedefinition` over `featuringOwners` (the declared `featured by` targets, else the lexical owner), `isInheritedMember`, `isPackageLevelFeature`, and the accessibility fallback `redefinedAccessible`/`featuringContexts`/`featuredWithin`/`featuringContextConforms` | `passes/constraint_test.go:TestConstraint_RedefinitionUsesFeaturingType`, `:TestConstraint_PackageLevelRedefinitionHasNoInheritedOwner`, `:TestConstraint_PackageLevelUnfeaturedRedefinitionExemptsNoInheritedRule`, `passes/f100_redefinition_featuring_test.go` (a `featured by` context inheriting the target, the snapshot-style pair, and the unrelated-context/no-common-target/unrelated-typing negatives) | ⚠️ Approximate (`TimeVaryingCarDriver.kerml:93` is accepted, an unrelated `featured by` context still rejected; the accessibility walk approximates the pilot's `canAccess` — only a *declared* `featured by` is read, the featuring a nested feature implies is not computed. The package-level exemption is decided by the absence of a `featured by` relationship, so a package-level feature that declares one is still checked) |

docs/reference/grammar/conformance-audit.md

@@ -120,6 +120,48 @@ the warning names the position, not the keyword.
 | `assume <constraint>;`, `require <constraint>;` | a requirement, concern, viewpoint or objective body | `RequirementConstraintMember` (`SysML.xtext:2039`) is the only production that admits it |
 | a one-ended `first <node>;` | an action body | `InitialNodeMember` is reachable from `ActionBodyItem` alone (`:1376`), never from `DefinitionBodyItem` (`:516`); elsewhere a succession names both ends, `first <source> then <target>` |
 
+### Chain redefinitions — `redefinition-through-reference`
+
+A redefinition target written as a feature chain of two or more segments,
+`:>> mid.leaf.value = 99.0;`, is standard KerML semantics: the chain-expression
+is itself a feature hosting the chain — its featuring type from the first
+segment and its featured type from the last (KerML 1.0 §7.3.4) — and the host
+feature is redefinable (§8.3.3.3). OpenSysML applies the redefining member
+below every composite feature the chain walks: every object of the type behaves
+as if the chain had been written as nested redefining usages
+(`part :>> mid { part :>> leaf { attribute :>> value = 99.0; } }`), carrying a
+declared value (`=` or `default =`), a declared type, a multiplicity and a body
+of its own. The pinned pilot evaluator accepts the notation but reads the
+original value — a pilot-evaluator gap, not a divergence the model is warned
+about (see the [pilot differential](../../project/pilot-differential.md)).
+
+Rules of the reading, in detail:
+
+- The shorthand ranks exactly as the nested-body form written in the same
+  body does: a nested-body redefinition declared by the chain's owner or
+  something specializing it wins; the child's type's own redefinition and
+  bodies in types the owner specializes lose.
+- Each chain applies below every object of the declaring type, including every
+  element of a multi-valued intermediate (`part wheels : Wheel[2];` then
+  `attribute :>> wheels.radius = 0.4;` redefines `radius` on each wheel).
+- A value the redefining member declares is evaluated in the declaring body's
+  scope, so `= factor * 2.0` reads the outer feature exactly as the nested-body
+  form does.
+- A valued chain below a feature bound to an existing object follows the
+  body's rule for an inherited value: one declared in a more specific body
+  governs the binding (a fresh object materializes below it and the bound one
+  keeps its own value), while one written in the same body as the binding is
+  rejected as a restating body is (`feature both valued and restated in a
+  body`). A chain declaring only a type or multiplicity conflicts with
+  nothing.
+- A chain walking through a reference — a `ref` usage, a port or a `subject` —
+  owns no object below the reference for the redefinition to land on. OpenSysML
+  reports `nested redefinition through reference <segment> has no owned object
+  to redefine on` as an error in every mode, and the redefinition is never
+  applied at runtime.
+- A chain whose target does not resolve declares no nested redefinition and is
+  reported by name resolution instead.
+
 ### Removed extension notation — no longer accepted
 
 An inline condition introduced by a keyword (`assert <expression>;` or

examples/self-model/execution.sysml

@@ -13,9 +13,10 @@ package OpenSysMLExecution {
     item def TypeShape :> SideTable;
 
     // One entry of a type's flattened schema (runtime.EffectiveFeature): name, symbol, owner,
-    // type, multiplicity, the stated value and its declaration, and whether it is a set, unique.
+    // type, multiplicity, the stated value and its declaration, whether it is a set, unique,
+    // and whether a more specific nested chain governs its bound value.
     item def EffectiveFeature {
-        attribute fieldCount : Integer = 9;
+        attribute fieldCount : Integer = 10;
         attribute inheritsDefault : Boolean = true;
         attribute inheritsMultiplicity : Boolean = true;
     }

examples/self-model/pipeline.sysml

@@ -182,7 +182,7 @@ package OpenSysMLPipeline {
     #SemanticEngine part def PassRegistry :> Stage {
         attribute :>> goPackage = "internal/check/passes";
         attribute tierCount : Integer = 4;
-        attribute passCount : Integer = 59;
+        attribute passCount : Integer = 60;
         attribute sortsByLevel : Boolean = true;
         attribute skipsDocumentScopedAboveFailure : Boolean = true;
 
@@ -297,6 +297,7 @@ package OpenSysMLPipeline {
         }
         part oosemMethod : ConstraintCheck { attribute :>> goType = "OOSEMMethodPass"; }
         part mosa : ConstraintCheck { attribute :>> goType = "MOSAPass"; }
+        part nestedRedefinitions : ConstraintCheck { attribute :>> goType = "NestedRedefinitionPass"; }
 
         in item typed : TypeTable;
         out item findings : Diagnostic;

internal/check/passes/analyze.go

@@ -77,6 +77,7 @@ func DefaultRegistry() *Registry {
 	reg.Register(behavior.ControlNodeSuccessionPass{})
 	reg.Register(OOSEMMethodPass{})
 	reg.Register(MOSAPass{})
+	reg.Register(NestedRedefinitionPass{})
 	return reg
 }