[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
• 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
• cover mixed any[], empty arrays, all three symbolic regions, aliases, 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, and the unresolved-element follow-up, 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...eba8e4e6	+899 / -237	+832 / -170	+242 / -0	+1973 / -407
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

The contract-simplification production diff is net -327 lines. The final gate cleanup is net -15 production lines. These comparisons deliberately exclude the earlier capability additions when describing deletion of complexity.

Verification

Local verification at eba8e4e6:

• ./gradlew :usvm-ts:test :usvm-ts:detektMain :usvm-ts:detektTest --console=plain
• git diff --check origin/main...eba8e4e6
• 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 eba8e4e6.

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

Closes #365
Closes #383

Part of #360