feat(model): persistent semantic model per workspace, invalidated per document

[devin-ai-integration]

What and why

Implements "Approach 1 — a persistent semantic model, invalidated per document" (§3, 3.1–3.4) of docs/project/large-model-scaling-design.md. Every edit used to clear the whole workspace — diagCache, the reverse-reference index — and the next request started from a fresh resolve.Resolver and semantics.Model, so a keystroke in a two-line file beside a large model cost a re-analysis of the model.

• One resolver and one model per model.Workspace (workspace.go: semanticsLocked, made on first use, handed to every passes.Context the workspace builds through passes.AnalyzeShared / Context.Share). A context built outside a workspace still constructs its own; CLI paths and tests are unchanged.
• Document-granular dependency relation, recorded rather than computed: symbols.Index reports every read to a ReadRecorder (a name looked up, a namespace enumerated or its children read, a document's root or kind, the whole table) and every write to a Changes set (symbols/changes.go, index.go, layer.go). The resolver (resolve/frames.go) keeps a frame per document — what was memoized while that document was analyzed, and what it read — and records a dependency on another document when a resolution returned that document's symbol (Resolver.found → Depend(sym.DocName)), when it imports a namespace the other contributes to, or when both contribute to one namespace. Index.TakeChanges + Resolver.Invalidate compute the transitive closure of the frames a change reaches.
• Invalidation by owning document (workspace.go: invalidateLocked → Resolver.Invalidate): drops the changed document's frame and its dependents', their memo entries (resolver, semantic model and argument typer all journal through the resolver's existing JournalNew, now a per-table ledger), their diagnostics and their reverse references. SetConformanceMode still invalidates everything. The semantic model's memoizing methods own their entries with defer m.own(sym).LeaveDoc() before the cache lookup, so a hit also records that the reader depends on the entry's owner — needed for compound-keyed memos such as composed[(S, T)].
• Cached gather + per-request judge for the workspace-wide passes (passes/gathers.go, oosem_gather.go, mosa_gather.go, identity_gather.go, and semantics/coherent_quantity.go via Model.shared): each document's OOSEM/MOSA/identity facts are gathered once into passes.Gathers, owned by the workspace, regathered for the changed documents only (Gathers.Regather), and each analysis judges over the union. Unions live in named resolver frames so that a regather that moves a shared judgment's input drops its readers. Populated gathers serve concurrent readers under a mutex.
• LSP refresh sweep (internal/lsp/files.go): refreshOpenDiagnostics republishes from the cache for open documents outside the changed one's dependent set.
• REPL: acceptFrom/dropStaleDebugSessions/keepIdentitiesOf needed no change; the transcript is one document and a submission that only adds an unrelated member still leaves the debugger running (internal/repl tests unchanged). The file-load path (%load, sysml -validate a b) is being changed separately to one document per file and is not touched here.

Where the implementation differs from the design: §3.2 suggests the REPL treating each top-level submission as its own document. That was not needed for the contract stated (the debugger's supersession is declaration-granular and already independent of the workspace's caching), so it is not done here.

Which path pays the bookkeeping, and which does not

Tracking is always on for a workspace, as the design states. Every memoized read records "the current document depends on this entry's owner" — about 25 M reads × ~8 ns on the 200-satellite constellation — so a one-shot sysml -validate, which analyzes through a REPL session's workspace, pays it with nothing to invalidate:

sysml -validate -memstats, 200 satellites, one file, 3 runs	develop	this branch
wall	1.85–1.96 s	2.19–2.25 s
allocated	738 MiB / 10.97 M allocations	767 MiB / 10.98 M allocations
peak RSS (/usr/bin/time)	421 MiB	428 MiB

At 1 600 satellites: 17.7 s / 5.5 GiB → 20.5 s / 5.8 GiB. This is a measured regression of the batch path, reported rather than hidden. What removes it: #312 (perf/parallel-batch-validation, stacked on #309) — its Workspace.DiagnosticsAll runs each uncached document through analyze(name, doc, batch) → passes.AnalyzeInBatch, which builds a private passes.Context per document (NewContextWithOptions: its own resolver and model over the read-only index) and never touches the workspace's persistent resolver, so the batch path there records nothing and pays none of this. Verified against #312's internal/core/model/batch.go and passes.Context.Batch.

Follow-up, not done here: Context.Batch is where #312's workers should receive this branch's passes.Gathers, so that the audits gather each document once for the whole batch rather than once per worker. It is described in docs/internals/performance.md and the stress-test record's further work.

Overlap to reconcile on whichever lands second: #309/#312 also edit workspace.go (Open/Update/SetOnDisk reindex via AddBuiltDocument; diagnosticsLocked delegating to analyze). This branch is based on develop, not on either.

How it was verified

Incremental equals fresh. TestIncrementalEqualsFresh (internal/core/model/incremental_test.go) replays a scripted sequence and a seeded random one — edit a document to a mutation or back to an earlier version, close, open — over the fixture sets, and TestIncrementalEqualsFreshCorpora over the four OMG corpora; after every step it compares diagnostics, the resolution of every written reference and the reverse references with a workspace built fresh from the same documents. Both run in go test ./... (the corpus variant skips without the corpora, fails with the require variables set).

Focused tests added: resolver frames, ledgers and transitive invalidation (resolve/frames_test.go); index read recording and change sets (symbols/changes_test.go); gathers gather each document once, regather only the changed one, propagate a union change to its readers, serve concurrent analyses (passes/gathers_test.go); workspace edits across documents, union-dependent diagnostics, retained state (model/workspace_test.go, stressmodel/satnet_test.go).

Measurements (Intel Xeon Platinum 8559C, 8 CPUs, 31 GiB RAM, Go 1.25.0, Linux; go test -run '^$' -bench ... -benchmem -benchtime=5x -count=3 ./internal/stressmodel, medians; "develop" is bcc6b13e0 built on the same machine):

	develop	this branch
BenchmarkEditBeside/32	48 ms, 22 MiB/op	0.82 ms, 0.31 MiB/op
BenchmarkEditBeside/128	189 ms, 83 MiB/op	2.5 ms, 0.64 MiB/op
BenchmarkEditBeside/512	861 ms, 327 MiB/op	8.7 ms, 2.0 MiB/op
BenchmarkEditImported/512 (6 files; edit the library, then every file's diagnostics)	8.78 s, 2.77 GiB	5.26 s, 1.17 GiB
BenchmarkLoadFiles/512 (6 files through one workspace)	9.20 s, 3.05 GiB	5.26 s, 1.56 GiB
1 600 satellites in 34 files through one workspace, open + analyze all	126.5 s	18.3 s
BenchmarkLoad/512, one file	5.13 s, 254 MiB held	5.99 s, 478 MiB held
live heap, 1 000 edits beside 32 satellites (TestEditsHoldNoStaleState)	—	67.2 MB after the 1st edit → 70.2 MB after the 1 000th

The design's target (512 satellites: ~1.53 s → < 50 ms) is met; develop on this machine measures 861 ms rather than the 1.53 s in the record, so both columns above were taken here. Editing the imported library costs one analysis of the model (the same 5.26 s as loading the six files). The 34-file figure is the §5 workload: the three audits gathered every document once per document analyzed; now once. A loaded workspace holds about twice the heap it did (the memo tables that used to be discarded after each analysis).

Gates:

$ gofmt -l .
$ go build ./... && go vet ./...
$ go test -count=1 ./...            # all ok
$ go test -race -count=1 ./...      # all ok
$ make lint                         # ✓ Lint passed
$ make docs-check                   # OK
$ make docs-counts                  # ✓ Documentation counts and refereed figures are current (8,369 → 8,391 tests)
$ ./scripts/download-training-examples.sh && ./scripts/download-pilot-corpora.sh
$ OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 \
    go test -count=1 -v ./internal/core/model -run 'TestTrainingExamples|TestPilotCorpora'
    training_examples_test.go:60: 100/100 training files clean
    pilot_corpora_test.go:78: kerml-examples: 55/58 pilot corpus files clean
    pilot_corpora_test.go:78: sysml-examples: 95/99 pilot corpus files clean
    pilot_corpora_test.go:78: sysml-validation: 56/56 pilot corpus files clean

training_examples_expected.txt and the pilot expectations are untouched.

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (docs/internals/performance.md, docs/project/satellite-network-stress-test.md)
• Changelog entry added as changes/unreleased/persistent-semantic-model.performance.md
• baselines regenerated and make docs-counts run (test count moved)
• No internal work-item labels in the body, docs, or changelog

[devin-ai-integration]

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

• Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
• Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

Merging with perf/parallel-batch-validation (#312)

A trial merge of origin/perf/parallel-batch-validation into this branch conflicts in nine files. Whichever lands second can resolve it as follows; on the resolved tree go build ./... && go test ./internal/core/model/... ./internal/repl/... pass (also -race for the batch and incremental tests), with the editor path on the persistent model and DiagnosticsAll on private per-worker contexts.

• internal/core/model/workspace.go
  • reindexLocked: keep perf(model): parse, index and validate a load's files on a pool of workers #312's w.index.AddBuiltDocument(name, doc.AST, doc.Scope) + ExpandWildcardImports(), followed by this branch's w.invalidateLocked() (no argument — the changed document comes from Index.TakeChanges).
  • analyze(name, doc, batch): batch != nil → passes.AnalyzeInBatch(...) (private resolver/model per worker, as in perf(model): parse, index and validate a load's files on a pool of workers #312); otherwise resolver, sem := w.semanticsLocked() → passes.AnalyzeShared(..., resolver, sem, w.gathers).
  • Add batched map[string]bool to Workspace. DiagnosticsAll marks every name it computed; invalidateLocked deletes those diagCache entries on any change (a batch analysis records no dependencies, so it cannot be kept selectively) and invalidateAllLocked clears the set. This is what perf(model): parse, index and validate a load's files on a pool of workers #312 alone does today, where every edit clears the whole cache.
• internal/core/passes/analyze.go: keep both PrepareBatch / AnalyzeInBatch (perf(model): parse, index and validate a load's files on a pool of workers #312) and AnalyzeShared (this branch); all of them funnel into analyze(ctx, root). pass.go merges cleanly (Context.Batch and Context.Share coexist).
• internal/core/symbols/index.go: in perf(model): parse, index and validate a load's files on a pool of workers #312's addDocument(name, root, rs, kind, explicitKind), call idx.changedDoc(name) right after idx.RemoveDocument(name), as AddDocument does on this branch.
• internal/stressmodel: take satnet.go from perf(model): parse, index and validate a load's files on a pool of workers #312 whole (its SatelliteNetwork.Split supersedes this branch's split.go, which is deleted); keep both sides of bench_test.go (BenchmarkValidateSplit and BenchmarkAnalyzeSplitPerDocument/openFiles) and of satnet_test.go.
• README.md, docs/project/spec-compliance.md: keep both count changes, then make docs-counts. docs/project/satellite-network-stress-test.md: keep perf(model): parse, index and validate a load's files on a pool of workers #312's batch-pool section and this branch's editor / split-plane sections side by side.

With #312's sysml -validate going through DiagnosticsAll, the batch path no longer touches the persistent model, so the tracking overhead reported in the description applies to the editor path only.

[devin-ai-integration]

Devin Review found 1 new potential issue.