[devin-ai-integration]

What and why

The gRPC service keeps the objects Instantiate creates alive across requests in a held runtime (heldObjects), and VerifySatisfaction sweeps that population. VerifyRequirement with no subject_symbol_id instead built a fresh worker runtime holding nothing: after Instantiate test::fleet, it answered a definition-owned verification case inconclusive: needs an object of test::Definition: none is instantiated while VerifySatisfaction on the same model reported the case pass on each held object. The REPL is the reference surface: %instantiate fleet then %requirement test::costReq prints one requirement verdict (undecided, its subject unbound) and one case verdict per held object (pass on IDs 2 and 3).

Root cause: Service.VerifyRequirement, VerifyConstraint and RunAnalysis went through newVerifyContext → s.newRuntime, a worker of the request's own, so caseCarriers(sym, nil) swept the empty worker. The fix is verifyContext.overHeld: with no subject named and a population held, the request's context is the held runtime under held.lock(ctx) (the same v.on(rt) pattern satisfyVerdicts uses), performOn keeps the analysis.Held(rt) contract, the explore path (exploreAnalysis, a background plan over fresh runtimes) is untouched, and RunAnalysis sets and restores the held runtime's schedule (verifyContext.scheduled). A named subject keeps today's worker. A sweep over the population that would make one more object than OPENSYSML_GRPC_MAX_HELD_OBJECTS allows is RESOURCE_EXHAUSTED, as Instantiate is: runtime.VerificationVerdict now carries the error an error verdict reports (Err), and EvalContext.thisValue wraps its cause with %w so errors.Is(err, ErrInstanceLimitExceeded) reaches it.

Wire shape: no proto change. The measured REPL output is one requirement verdict plus N case verdicts, which VerifyRequirementResponse (verdict + repeated verification_verdicts) already carries; instances now carries every object a case verdict is about (runRoots, as RunAnalysis does).

Second commit (%satisfy labels): a definition's satisfy r; decided over held objects labelled a nested object (on test::fleet.cheap ID: 2) while %validate fleet labelled the same object (on test::fleet.cheap[1] ID: 2). The runtime now spells a carrier's path once (heldSegments/indexedSegment, shared with the validation walk's heldChildren; carrierFeatures keeps carrierLabels' rule that a subsetting collection's object ends in its declaration), the REPL joins it in one place (objectPath, replacing featurePath and objectVerdict's own join), the CLI's -satisfy follows, and the gRPC satisfy verdict carries it as instance_path as ValidateInstance's verdicts do (instancePath).

Specification basis

SysML v2.1 Beta 2 §7.24 Verification Cases (§7.6.3: a usage nested in a definition is a feature of each object of it), §7.20.1 (the owner of a satisfy with no by is the satisfying feature). Moves the rows "A verification case a part definition owns is a feature of every object of that definition" and "A satisfy r; stating no by is about the objects of the type stating it" in docs/project/spec-compliance.md (status unchanged, ✅; implementation and test columns extended). Not stricter than the spec: no new diagnostic.

Behaviour changes

• gRPC VerifyRequirement with no subject_symbol_id, objects held: a definition-owned verification case runs once per held object of the definition and its verification_verdicts name each object (instance_id, instance_type_id); instances carries those objects. Before: one inconclusive … needs an object verdict. With nothing held: unchanged.
• gRPC VerifyConstraint/VerifyRequirement with no subject, objects held: a constraint or requirement a definition owns is checked on the held object carrying it; over several carriers the verdict is undecided with FAILURE_REASON_AMBIGUOUS_SUBJECT (REPL %constraint/%requirement parity). Before: declared defaults on a fresh exemplar.
• gRPC RunAnalysis with no subject, objects held: a case a definition owns runs as a feature of the one held object of that definition; over two it reports the runtime's error verdict naming both carriers (REPL %analysis parity). Before: inconclusive … needs an object.
• gRPC VerifyRequirement/VerifySatisfaction/ValidateInstance: a verification sweep over the held population that would pass OPENSYSML_GRPC_MAX_HELD_OBJECTS is RESOURCE_EXHAUSTED (as Instantiate), the population unchanged. Before: an error case verdict quoting this names no object here: object limit exceeded.
• gRPC RunAnalysis with no subject, objects held: a verification case whose run would pass the held-objects bound is RESOURCE_EXHAUSTED (the failure in the case's verdict as well as in the call's error). Before: an error verdict.
• gRPC RunAnalysis tool_dry_run over the held population: the preview's writes and objects are undone and the runtime's tool runner put back, as the REPL's %tool preview does. Before: the preview's performance stayed held and the dry runner stayed on the runtime.
• REPL %satisfy, CLI -satisfy, gRPC VerifySatisfaction over a definition's satisfy r;: the object is labelled fleet.cheap[1]/cheap[1] (indexed, as %validate), the gRPC verdict gaining instance_path. Before: fleet.cheap, no instance_path.

How it was verified

• Failing-first: grpc/held_population_verify_test.go TestVerifyRequirementWithoutASubjectSweepsTheHeldPopulation (fails on develop: costTest=inconclusive, 1 verdict), plus TestVerifyConstraintWithoutASubjectIsAboutTheHeldCarrier, TestRunAnalysisWithoutASubjectRunsOnTheHeldObject; grpc/robustness_held_population_test.go TestGRPCRobustnessHeldPopulation (bound → RESOURCE_EXHAUSTED, population unchanged, named subject unaffected); gRPC conformance verify_requirement_held_population and verify_requirement_no_object (new VerifyRequirement runner with instantiate, expected_status, expected_verification_verdicts). TestDefinitionOwnedCaseWithNoObjectNeedsOne (nothing held) unchanged and green.
• Labels: cmd/sysml/satisfy_label_test.go and repl TestSatisfyLabelsObjectsAsValidateDoes (same (on test::fleet.cheap[1] ID: 2) line from -satisfy/%satisfy and -validate/%validate); the existing runtime TestReportedFeaturesEndInTheDeclaration keeps the subsetting-collection declaration rule.
• Review round 1: grpc/held_population_preview_test.go TestToolPreviewLeavesTheHeldPopulationAsItWas (fails without the fix: held after the preview = 4 objects, want 3, dry runner left on); TestGRPCRobustnessHeldPopulation gains case run at the bound.
• Fallout: 0 fixtures, goldens or expectations re-recorded; 0 existing tests changed. The only movement during development was TestReportedFeaturesEndInTheDeclaration, fixed by keeping the declaration rule rather than editing the test.
• Gate (re-run on the tree merged with develop e19d9beb3; the spec-compliance.md conflict took develop's citation column and kept the rows here):
• go build ./..., go vet ./..., gofmt -l . (empty): clean.
• go test -timeout 60m ./...: 123 packages ok, 0 failures (the default 10-minute package timeout is too short for cmd/sysml and tests/codegen under a parallel run on this machine, hence the flag).
• make test-shard SHARD=runtime (race, allocation bound): ok in 1638 s, 88.0 % coverage; no bound raised.
• make docs-check, python3 scripts/check-doc-ids.py, python3 scripts/changelog.py check: pass.
• PSSM referee (pssm-referee -check): reproduces the committed counts — pass 56, fail 6, not-expressible 34, differs-by-design 7 (103 tests). No movement.
• Pilot execution referee (pilot-exec-diff, 514 cases): agree 229, kind-only 1, order-only 0, disagree 38, differs-by-design 5, pilot-unevaluated 167, pilot-silent 24, pilot-error 7, ours-error 10, ours-undetermined 17, both-error 16, nondeterministic 0 — identical to the committed baseline.
• WebAssembly module (GOOS=js GOARCH=wasm -tags sysml_prod -ldflags "-s -w", Go gzip.BestCompression): develop e19d9beb3 22,455,061 B gz → head 22,457,220 B gz (+2,159 B, +0.01 %). Budget untouched.
• Docs: make docs-check (venv python) and scripts/check-doc-ids.py pass; python3 scripts/changelog.py check passes.

Open decisions (found, left alone)

• Displaced objects in sweeps: after instantiating one declaration twice, satisfy sweeps (SatisfactionSubjects over the surface's held roots) visit both objects while definition-owned case runs and checks (caseCarriers, conditionSubject over rootInstances) take the newest only — REPL and gRPC alike, and runtime verification_runs_once_per_repeated_object pins the newest-only rule. Which rule a sweep should follow is yours.
• Subsetting-collection labels: %validate names an element reached through part small : Component :> subsystem as subsystem[1], verdicts name it small (TestReportedFeaturesEndInTheDeclaration). Same on develop; aligning them moves either validation goldens or that rule.
• RunAnalysis/%analysis of a definition-owned case over two carriers nested under one held root (fleet.cheap[2]) runs once, on the first (cheap[1]), while two held roots are an ambiguity and VerifyRequirement sweeps both. REPL and gRPC agree; left as is.
• A run of a verification case over the held population keeps the performance it materialized in the population (as the REPL's session runtime does); only a tool dry run is undone.
• An explore schedule runs on runtimes of its own, one per linearization, holding nothing: the held population does not reach explored runs. Unchanged, documented in the wire contract.

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

[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