Calls: freeze per-class startup runtime graphs

usvm-ts-calls/STARTUP_GRAPH_FREEZING.md

@@ -0,0 +1,76 @@
+# Freeze original class startup graphs
+
+`freeze-class-startup-inputs.py` consumes the unchanged selection ledger and original
+project acquisition receipts. It uses the existing `inspect-startup-closure` traversal,
+then writes a machine startup manifest with every original class, per-class graph
+receipts and shared thin source roots. It does not install dependencies or execute
+project code. Build the adapter before invoking the CLI.
+
+```sh
+python3 usvm-ts-calls/scripts/freeze-class-startup-inputs.py \
+  --ledger /absolute/path/selection-ledger.json \
+  --acquisition /absolute/path/manager-retry-attempt \
+  --acquisition /absolute/path/priority-attempt \
+  --acquisition /absolute/path/secondary-attempt \
+  --inspector /absolute/path/fast-check-adapter/dist/src/source-inspector-cli.js \
+  --frontend-typescript /absolute/path/pinned-frontend/node_modules/typescript \
+  --tool-revision EXACT_40_HEX_BUILD_REVISION \
+  --native-frontend-revision bundled:EXACT_FRONTEND_REVISION \
+  --output /absolute/path/new-startup-graph-attempt
+```
+
+Acquisition arguments are ordered preferences: the first successful frozen receipt
+wins; if none succeeded, the first failure remains explicit provenance. A failed
+whole devDependency installation does not automatically reject a class. Its graph
+can still qualify when every consumed runtime/config/lock input is proven by the
+exact original Git revision and all runtime edges are resolved or explicitly recorded
+as boundaries. Generated or installed inputs require their immutable acquisition
+snapshot. Changed inputs and unresolved static modules retain incomplete rows.
+
+Startup traversal follows actual TS/JS runtime code and literal CommonJS requests.
+JSON, native builtins and unresolved dynamic module requests remain explicit boundaries,
+including source offsets/expressions where the target cannot be statically resolved.
+The graph receipt never claims those boundaries have symbolic models or native replay
+support. Checked/native admission remains strict and separate. Initialization and
+binding limitations remain diagnostics rather than disappearing from the report.
+
+Original target/import bytes are copied verbatim. Physical installed runtime sources
+receive an explicit content-preserving `.usvm-installed` namespace mapping, while
+frontend roots contain only the acquired runtime source graph. Project copies are
+shared across classes; dependency snapshots are not copied wholesale. Each machine
+manifest row freezes its exact frontend config, selected source bytes and a graph
+receipt relative to the manifest root. Original installation receipts remain unchanged.
+
+The CLI reads the pinned frontend TypeScript option/lib inventory and compiler SHA.
+Startup-only compatibility projects unsupported type-check-only options and newer
+library declarations into that frontend environment. Original resolved options,
+each before/after boundary and unprojected unknown semantic options are retained.
+For example, `lib: ["es2024"]` can use the frontend's `esnext` declarations; this does
+not emulate ES2024 runtime operations. Unknown semantic/emission options are preserved
+for explicit frontend diagnostics. Checked and native replay configs are unchanged.
+
+Frontend compatibility also checks option names and enum values against that exact
+compiler's inventory. The receipt records `frontendCompilerProjection.status` and
+`unsupportedCompatibilityBoundaries` with typed
+`FRONTEND_COMPILER_OPTION_UNSUPPORTED` reasons. This is detection only: unsupported
+semantic/emission options and enum values remain unchanged. In particular, TypeScript
+5.4.5 cannot accept Utilityjs's `module: "node20"` or
+`rewriteRelativeImportExtensions`; `noEmit` does not prove those settings harmless.
+The former controls Node module/interoperability semantics, while the latter also
+affects semantic diagnostics and derived import-extension options. This change does
+not make `DisjointSet` start: it requires genuine frontend support for those options
+or a compatible compiler upgrade. An acquired graph can still have unsupported
+frontend compatibility, and `COMPATIBLE` is only an inventory check, not proof of
+successful IR generation or symbolic support.
+
+`acquisitionComplete` proves the frozen per-class graph, including explicit opaque
+boundaries. Genuine machine class entry, useful candidate values and class-only
+replay-checked coverage are later, distinct checks. Keep all original rows in those
+reports; do not select a new cohort from successful startups.
+
+Focused checks require a built adapter:
+
+```sh
+python3 -m unittest discover -s usvm-ts-calls/scripts \
+  -p test_freeze_class_startup_inputs.py -v
+```

usvm-ts-calls/STARTUP_RUNTIME_RESOLUTION.md

@@ -0,0 +1,29 @@
+# Resolve acquired startup runtime bytes
+
+`FrozenModuleResolver.resolveStartup(specifier, from, importKind)` is an additive
+acquisition API. The existing checked/native-replay `resolve` contract is unchanged.
+It selects actual in-root TypeScript or JavaScript runtime source, including installed
+packages, original generated JavaScript and package export patterns. Import and
+require conditions are selected separately; declaration entries never replace runtime.
+An explicit package export must exist exactly: missing `.js` exports are not guessed
+as `.ts` sources. Relative source imports retain the existing absent-JS/source-TS
+mapping, while present JavaScript always wins.
+
+The result is either a source edge or an explicit runtime boundary. Node builtins
+are recorded by name, containing source and import kind; JSON boundaries also verify
+JSON syntax and freeze the actual JSON bytes. Boundary acquisition does not implement
+JSON evaluation, native builtins or their symbolic models. Missing packages, unsupported
+formats, declaration-only entries, escaping paths and incompatible context-dependent
+aliases still fail explicitly.
+
+`freeze` adds `runtimeBoundaries` only when present, keeps consumed runtime/package/
+config/lock hashes, and enables JavaScript in the derived startup frontend configuration.
+The config is derived from explicit original compiler settings, rather than defaults
+computed by a newer TypeScript version. No imports or original source bytes are edited.
+
+Graph consumers must follow each source edge and retain every boundary diagnostic.
+Installed source paths are acquisition identities: they need a content-preserving,
+explicit original-to-materialized namespace mapping before frontend lowering, because
+physical `node_modules` paths have unstable frontend identities. Do not turn the full
+installation snapshot into frontend roots. A complete acquired graph is separate from
+engine support, successful class entry and replay-checked coverage.