[devin-ai-integration]

What and why

A composite requirement usage nested in a requirement definition or usage is a subrequirement: automatically one of the container's required constraints, and when it declares no subject of its own, bound to the container's subject. Before this change the runtime collected only require/assume members of a requirement body, so a nested requirement light { require constraint { v.mass < 10.0 } } contributed nothing to its container: r.result stayed true, sysml -requirement P::r reported the requirement as holding vacuously, and the gRPC/MCP verdicts said the same — a silent false pass for every grouped requirement.

requirement def R {
  subject v : Veh;
  requirement light { require constraint { v.mass < 10.0 } }
}
part veh : Veh { attribute :>> mass = 20.0; }
requirement r : R { subject v = veh; }

	before	after
sysml -requirement P::r	✓ Requirement P::r satisfied (vacuous)	✗ Requirement P::r failed — Required condition evaluated to false: v.mass < 10.0, exit 1
-e P::r.result (and box.rr.result on a part-held usage)	true	false
gRPC VerifyRequirement / MCP verify_requirement	holds	does not hold, naming the condition
container whose own subject nothing binds (requirement descent { requirement thrust : ThrustMargin; } checked directly)	holds vacuously	could not be evaluated: no value for feature engine (not covered)
container whose own require fails beside a subrequirement assuming false	result = true	result = false — the assumption guards the subrequirement alone
subrequirement owning subject s : Veh; that nothing binds	judged on the container's subject	no value for feature s

The fix sits where membership and subject binding are derived, not in a special case at evaluation time:

• internal/semantic/semantics/nested.go: the implicit-subsetting rule that already names Requirements::RequirementCheck::subrequirements for a composite requirement usage in the requirement family is split into nestedSubsettingFQN and exposed as Model.IsSubrequirement, answered from the declarations alone (so it holds whether or not the library is loaded).
• internal/exec/runtime/condition.go: condition collection treats a subrequirement as one required constraint of its container (appendSubrequirementConditions): a Condition group marked Subrequirement whose value is the subrequirement's own check over its whole chain — allTrue(assumptions()) implies allTrue(constraints()) (subrequirementHoldsAt), so its assumptions guard it alone and never the container's other constraints, and one stating no required condition, or one brought in by assume r;, leaves the container as vacuous as it is (requiresAny) — with the same cycle guard and parameter masking a named require/assume constraint gets; constraintScope binds the subrequirement's inherited subject names to the container's subject value only when the usage owns no subject declaration (subrequirementSubject, SubjectsOf), leaving one it owns alone whether bound (subject e = v.eng;) or not (subject s : Veh; is reported unbound). conditionOwnerOf lets a usage body supply its conditions through a subrequirement the way it does through a named constraint.
• internal/exec/solve/translate.go: the SMT translation reads a subrequirement group the same way, as the implication its own check is (assertedCondition), so the solver and the evaluator keep agreeing on the differential conformance corpus.

Covered: a subrequirement without its own subject (bound to the container's), a typed one inheriting its definition's subject (the clause's requirement driving : DrivingRequirement; form), one with its own subject (kept), nesting two levels deep, a subrequirement under a requirement usage, assume constraint vs require constraint inside the subrequirement, the result read, and the CLI, gRPC and MCP verdict surfaces.

Not changed here (stated as still open in the compliance row): a requirement usage is not materialized as an object of its own, so the reflective reads r.subrequirements / r.constraints still answer [] and r.light.result stays <undetermined>, although the container's result now counts it.

Specification basis

SysML v2.1 Beta 2 §7.21.2 Requirements ("A composite requirement usage nested in a requirement definition or usage is a subrequirement … Subrequirements are considered to automatically be required constraints of the containing requirement definition or usage … if a subject parameter is not explicitly declared for a subrequirement, it is assumed to have the same subject as its containing requirement definition or usage, with its subject bound to that of the container", with the VehicleRequirementsGroup example); §8.3.21.9 checkRequirementUsageSubrequirementSpecialization; Requirements.sysml abstract requirement subrequirements[0..*] :> requirementChecks, constraints and RequirementCheck::result = allTrue(assumptions()) implies allTrue(constraints()).

An assume constraint inside a subrequirement belongs to the subrequirement's own check: its value within the container is allTrue(assumptions()) implies allTrue(constraints()) over what it states, in the check verdict and the result read alike — a false assumption makes the subrequirement hold vacuously and nothing else (subrequirement_assumption_scoped, subrequirement_assumption_result), a true one leaves its required conditions to decide (subrequirement_assume_require). The container's own assumptions keep the check path's existing trusted-precondition reading; only what the subrequirement states is scoped by this change.

Moves docs/project/spec-compliance.md: the nested-usage subject-binding row (⚠️, "Open: … not yet materialized as a member of its container's subrequirements and constraints …") now states the fixed behaviour and the remaining reflective-read gap; the "Nested requirements" runtime row cites the subrequirement fixtures.

How it was verified

Four layers:

• golden AST tests/parser/testdata/parse/subrequirement_container_subject.{sysml,golden}
• execution conformance subrequirement_container_subject, subrequirement_typed_inherits_subject, subrequirement_explicit_subject, subrequirement_two_levels, subrequirement_under_usage, subrequirement_assume_require, subrequirement_assumption_scoped, subrequirement_assumption_result, subrequirement_assumed_reference, subrequirement_owned_subject, subrequirement_result_read (no trace: no ordering is involved)
• internal/exec/runtime/robustness_subrequirement_test.go: container_subject_unbound (typed unbound-subject error, no vacuous pass), naming_its_container (require r; inside r's subrequirement is ErrNoConditions, returns, no hang) and owned_subject_unbound (an owned subject s : Veh; nothing binds is ErrNoValue naming s, not judged on the container's subject)
• surfaces: cmd/sysml/subrequirement_test.go (-requirement exit 1 naming v.mass < 10.0, exit 0 when every subrequirement holds), internal/frontend/grpc/subrequirement_test.go (VerifyRequirement by two subjects), runtimetools_test.go (verify_requirement on Demo::massGroup)

Models whose verdicts could move: examples/ holds no requirement usage nested in a requirement (scanned every .sysml). docs/manual/examples/: cookbook.sysml Cookbook::pointingRequirement and requirements.sysml Requirements::spec::r2 nest doc-only subrequirements, so -requirement on them is byte-identical to develop's (they still hold vacuously, the vacuity note included); trace-2-hierarchy.sysml descent/touchdown are satisfied through their subrequirements (satisfy specification.descent.thrust by engine …) — -requirement=LanderHierarchy::specification::mass, every -satisfy verdict and the rendered HierarchyReport are byte-identical to develop's, while checking descent or touchdown itself directly now reports no value for feature engine (the group's own subject is unbound; its subrequirements read it) instead of a vacuous pass.

Dry-merge of the head against origin/develop (c1cad1303) and against PR #1529's head (8a100b317), each in a detached worktree: both merge clean, the only file either side and this branch both touch is docs/project/spec-compliance.md (different rows, auto-merged); on each merged tree TestExecutionConformance, TestRuntimeRobustnessSubrequirement, TestReturnParameter*, internal/exec/solve, cmd/sysml -run TestRequirement and the training-corpus gate (TestTrainingExamples*, TestRequirementDefinitionsFile) all pass.

Gates, run serially with the training/pilot/spec-example/library-XMI/PSSM corpora required (OPENSYSML_REQUIRE_*=1): go build ./... ✅, go vet ./... ✅, gofmt -l . empty ✅, go test -count=1 -timeout 30m ./... ✅ on the final tree, every package ok (an earlier run had caught internal/exec/solve TestDifferentialConformanceCorpus disagreeing with the evaluator on subrequirement_assumption_result, which is what the translate.go change fixes), python3 scripts/changelog.py check ✅, mkdocs build --strict ✅, make lint ✅.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/ff3b5848a88b4fdf8f4331d3dbeae409
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/ff3b5848a88b4fdf8f4331d3dbeae409?variant=devin
Requested by: @HuiJun

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring