perf(runtime): attribute and fix the 0.9.1 satisfaction, gRPC, migration and lint regressions

[devin-ai-integration]

What and why

Closes out the "priced, not fixed" and "unattributed" findings of docs/project/performance-release-0.9.1-vs-0.9.0.md (#728): Satisfy +46–56% / +64% allocs, GRPCVerifyConstraint +29%, migrate WriterSiblingBlocks +21%, and the single-threaded analysis cost. Each was profiled (-cpuprofile/-memprofile, pprof -top -cum) or bisected, the recomputation removed, and what remains attributed to the commit and rule that needs it. No semantics change: every fix is a memo, a fast path or an allocation removed, and no test, golden or corpus expectation was changed.

Satisfaction tracing (internal/exec/runtime) — the shared-default/shared-verdict trace of 758c9c260/afbdb615d was mostly recomputation around the record, not the record:

• observeRead copied every path of a nested shared record into the trace per read → records the record pointer once (sharedRead.shared), expanded in sharedPaths only when a verdict is shared.
• sharedPaths deduplicated through a pathKey string built per read and assembled each root-relative path twice → hasPath compares slices; each path assembled once (sharedPath).
• bindingDeclaredFor spelled a dotted path at every ancestor and looked each up in bindingsForFeature → Model.bindingRoots memoizes per type the first segment of every binding end path; the path is spelled/looked up only where a binding starts at that feature (a binding matches only on end.Path == path, so the prefilter is exact).
• Every journal mark and rollback cloned clock.waiters (slices.Clone[clockWaiter] was 289 MB of the run's heap — also in 0.9.0) → Clock.attach/detach/forgetFinished replace the slice instead of editing it in place, so a mark keeps the slice it saw.

gRPC VerifyConstraint — bisected to 7bd51ece6 (implicit nested-usage subsetting): +20% time / +17% bytes against its parent. The instance graph the response serializes now carries every nested usage's subsetted collection; the graphs before/after this PR are byte-identical and differ from 0.9.0 only in those collections, so the growth is the rule's output. Around it: declaredSubsettedNames memoized on Model.declaredSubsetted; appendUniqueInstances and reachesNames make their sets on first use; reachesSubsetted looks up the owner's values instead of building a by-name map.

Migration writer — 101f3b7cd grew the per-block buffer; the cost was a fresh buffer per block and strings.Repeat per line. The writer now reuses closed buffers (open/close with a free list), indents from a table, and grows a line's builder once.

Single-threaded analysis — UndeclaredSignalPass.Run was 19.8% of AnalyseResolved, all in kit.WalkScoped → ast.Inspect, walked twice (gather sent signals, check triggers). kit.ScopedNodes keeps the walk's result on the pass context for the document it analyzes (root looked up under Resolver().Untracked so no gather comes to depend on it); both passes iterate it. The lint's semantic queries were already journaled memos on semantics.Model; no new cache there is warranted.

Six-run interleaved benchstat, v0.9.0 / before (17f8a80b5) / after:

benchmark	v0.9.0	before	after
Satisfy/satellites=32	3.20 ms / 1.74 MiB / 25.9k	4.82 ms (+51%) / 3.12 MiB (+80%) / 42.4k (+64%)	4.20 ms (+31%) / 1.66 MiB (−4%) / 28.9k (+12%)
Satisfy/satellites=128	15.3 ms / 10.7 MiB / 103k	22.2 ms (+45%) / 16.2 MiB (+52%) / 169k (+64%)	17.8 ms (~, p=0.065) / 6.65 MiB (−38%) / 115k (+12%)
Satisfy/satellites=512	102 ms / 102 MiB / 411k	147 ms (+43%) / 125 MiB (+22%) / 675k (+64%)	92 ms (~) / 26.6 MiB (−74%) / 459k (+12%)
Satisfy geomean		+46% / +50% / +64%	+11% / −46% / +12%
GRPCVerifyConstraint	668 µs (±67%) / 456 KiB / 8.53k	869 µs / 542 KiB (+19%) / 9.49k (+11%)	807 µs / 511 KiB (+12%) / 9.19k (+8%)
WriterSiblingBlocks	3.65 ms / 5.38 MiB / 80.0k	4.19 ms (+15%) / 5.69 MiB (+6%) / 80.0k	1.77 ms (−51%) / 1.91 MiB (−65%) / 20.0k (−75%)
AnalyseResolved	1.04 ms / 486 KiB	1.36 ms (+31%) / 534 KiB (+10%)	1.18 ms (+14%) / 538 KiB (+11%)

Priced, with commit and profile frames in findings 5–8 of the record: the per-read recording and per-ancestor bindingRootedAt lookups of the tracing (+31% on the 32-satellite row, within noise at 128/512; 758c9c260/afbdb615d); the subsetted collections the gRPC response now carries (+12% bytes; 7bd51ece6); the lints and interface records on a resolved document (+14%).

How it was verified

• benchstat over six interleaved rounds of the four benchmark sets on v0.9.0, 17f8a80b5 and this tree; four-run pairs of 7bd51ece6/101f3b7cd against their parents; CPU and heap profiles behind each finding (tables and commands in the record).
• gofmt -l . empty, go vet ./..., make lint, make build, go test -race ./... pass.
• Corpus gates with OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 (100/100 training clean; pilot ratchets unchanged at 56/58, 92/99, 56/56) and the SMT tests with OPENSYSML_REQUIRE_SMT=1 OPENSYSML_SMT=/usr/bin/z3 pass.
• The only test edit is TestPathKeyDistinguishesDottedNames → TestHasPathDistinguishesDottedNames: pathKey no longer exists, and the test asserts the same dotted-name property of its replacement.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change — the pathKey unit test retargeted to hasPath; otherwise performance-only, covered by the existing suites and benchmarks
• 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 — no gate count moved
• 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/ef1f41df283a48fe8f40e04cfdcabd8d
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/ef1f41df283a48fe8f40e04cfdcabd8d?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

[devin-ai-integration]

Runtime differential completed against base 17f8a80b5 and candidate e48a6938a. No semantic output differences found in the exercised cases.

Shared-clock exploration: visual before/after evidence

Both binaries completed two runs with identical ordering, probabilities, and witnesses: armed=true in both, and sawLit=false/true depending on which waiter runs first. Version lines intentionally identify different builds.

Base	Candidate

Additional runtime comparisons and caveats

• Both trees built with make build.
• CLI/REPL: stress satisfaction (96/384 holding checks at 32/128 satellites), repeated satisfaction, pass/fail/inconclusive verification, mixed shared defaults, nested clocks, and mission completion matched (stdout, stderr, exit status) over 29 command pairs.
• gRPC: ten complete response pairs matched structurally, including nested/subset feature values, repeated requests, negative verdicts, and a 230-instance graph.
• Migration: six XMI/PSSM outputs matched byte-for-byte (including a 5.4 MB PSSM output).
• Lint: missing-signal, valid, cross-document, and disabled-warning controls matched.
• Five initial invalid invocations were rejected identically, then corrected and rerun; matching rejections were not treated as runtime coverage.

These are representative runtime checks, not exhaustive semantic or performance certification.

Devin testing session

[devin-ai-integration]

✅ Devin Review: No Issues Found

Devin Review analyzed this PR and found no bugs or issues to report.