[TS Calls] Add guarded semantic models with a simplified contract

[CaelmBleidd]

What this PR delivers

Capability work for #365

• add guarded semantic-model selection and execution to the existing unknown-call boundary
• preserve normal and exceptional completion, deferred state changes, aliases, residual fallback, and one observer decision per application
• add Array.shift as the intrinsic example backed by symbolic-memory memcpy
• require stable call-target evidence and a supported receiver representation; unknown and fake receivers use fallback

Contract simplification gate for #383

Starting from fad3d155 (the rebased last pre-simplification head after the original #365 registry and intrinsic packaging), this PR:

• collapses descriptor, registration, backend, and implementation wrappers into one TsUnknownCallModel object with an ID, declarative target, and guarded execution
• removes implementation-kind tags, supported-domain IDs, and stored precision values; residual presence expresses partial handling
• replaces the old profile and registry layers with one immutable enabled-model catalog and one residual fallback setting
• derives observable outcomes from model or residual decisions instead of storing a second outcome value
• removes automatic runtime contract-validation queries for trusted model guards; focused tests own disjointness and completeness obligations
• removes per-family fallback overrides
• keeps enabled-set identity based only on model IDs rather than implementation-specific version fields

No obsolete contract or configuration layer from that list remains in the #383 code path.

Unresolved Array.shift elements

• keep a definitely-array receiver applicable when its element sort is unresolved
• copy the Boolean, number, and address symbolic-memory regions that form the fake-value representation
• read unresolved elements from the current symbolic memory rather than allocation history, including aliased symbolic-index writes
• normalize conditional fake-wrapper/raw-reference values through the existing lazy fake-value machinery without nesting wrappers
• materialize the removed element through the live TsStepScope, preserving the exactly-one-type constraint and updated solver models in every successor
• shift already materialized fake wrappers for concrete unknown arrays and preserve reference aliases
• keep allocation history immutable during shift; current-state resolution observes the final symbolic memory
• cover mixed any[], empty arrays, all three symbolic regions, aliases, repeated shifts, and multi-element reference arrays

Scope boundary

This PR completes the common contract and intrinsic integration only. It does not claim source-model execution as delivered.

PR #380 / #366 is rebased on this branch and supplies the concrete downstream implementation: the same model object and catalog expose an EtsIR-backed successor completion, model EtsIR files become part of the analysis scene, and the normal interpreter executes the source body. Array.pop remains the source-model example. No second dispatcher, backend registry, or plugin framework is introduced.

Diff accounting

The complete PR includes the original #365 capability, the #383 simplification, the unresolved-element follow-up, and the review fix, so its aggregate size is not the size of the simplification alone.

Comparison	Production (src/main)	Tests (src/test)	Documentation	Total
Whole PR: origin/main...9251124f	+871 / -240	+926 / -173	+242 / -0	+2039 / -413
Contract simplification: fad3d155..bcc9d62b	+461 / -788	+387 / -776	+239 / -0	+1087 / -1564
Final #383 cleanup: 34597f57..bcc9d62b	+8 / -23	+14 / -23	+20 / -18	+42 / -64
Unresolved Array.shift: bcc9d62b..eba8e4e6	+268 / -42	+131 / -10	+9 / -6	+408 / -58
Review fix: eba8e4e6..9251124f	+39 / -70	+98 / -7	+0 / -0	+137 / -77

The contract-simplification production diff is net -327 lines. The final gate cleanup is net -15 production lines, and the review fix removes another net 31 production lines while adding focused regressions. These comparisons deliberately exclude earlier capability additions when describing deletion of complexity.

Verification

Local verification at 9251124f:

• ./gradlew :usvm-ts:test :usvm-ts:detektMain :usvm-ts:detektTest --offline --no-daemon --max-workers=2 --console=plain
• four focused external review probes for current-memory reads, shifted wrappers, resolver behavior, and bounded history
• git diff --check origin/main...9251124f
• linear history on ece06b3e with no PR-local merge commits

GitHub CI is green for ci-core, ci-jvm, ci-python, ci-ts, ci-ts-pbt, lint, and detekt at 9251124f.

This PR replaces #376 after its squash commit was removed from main.

Closes #365
Closes #383

Part of #360