[TS] Compare string values in equality operators

[CaelmBleidd]

Closes #422.

TypeScript string equality previously compared heap references, so two distinct references with the same contents could compare unequal. Compare modeled strings by UTF-16 length and code units for ===, !==, ==, and !=, while preserving object identity and strict/loose nullish equality.

This branch is rebased on main at 7b9a88b52851b54ba6f379c2c4a81a2a4449d068, after #453 and #459. It retains the current test organization introduced by #453.

Change

• Typed string inputs have bounded backing arrays, and literals have initialized contents.
• An any or unknown reference acquires backing only after the execution path proves it is a non-nullish string. The backing belongs to the original reference, so aliases, .length, equality, and witness extraction use the same contents. Unrefined and nullish alternatives retain their existing constraints.
• Internal string backing uses a private field identity. It cannot collide with user properties such as box.value, which previously caused a feasible string branch to disappear.
• analyzeWithOutcome exposes explicit unsupported paths separately from supported states. Unsupported terminal states do not contribute to coverage or the default COVERED_NEW collector. Calls reports UNSUPPORTED when an exhausted analysis reaches no target and contains an explicitly unsupported path.

Support boundary

String contents are bounded by the configured maxArraySize / maxStringLength. References whose string type has not been established and whose backing is absent can still produce explicit unsupported outcomes. A future symbolic string producer must create bounded backing and register its reference. Witness extraction can still reject an input that remains unrefined on an early-return path; successful refined-string witnesses are checked and replayed.

Strict comparison of two fake any wrappers still has the preexisting nested-fake-object limitation. With throwExceptionOnStepFailure=false, unsupported operation exceptions become explicit unsupported terminal paths; with that option true, they propagate. Calls uses the latter setting.

Verification

• On head 7217c2a1094af74217dc0d2ba03e0c058d0fd4e1, :usvm-ts:test: 1,117 tests, 975 passed, 142 skipped, zero failures or errors. :usvm-ts-calls:test: all 13 passed.
• All 19 focused string equality, symbolic input, witness-bound, witness-resolution, and array-isolation tests passed. Source behavior is checked through discoverProperties, with direct machine assertions for completion and unsupported outcomes and Node.js replay for concrete witnesses.
• :usvm-ts:detektMain, :usvm-ts:detektTest, :usvm-ts-calls:detektMain, :usvm-ts-calls:detektTest, and git diff --check passed.
• The permanent box.value guard regression failed on the previous late-backing implementation because result 1 disappeared, and passed with the pinned base production code and the private-field fix.

The local checks above use the repository's pinned JacoDB dependency. CI run 37229853473 also passed all six jobs on published head 7217c2a1094af74217dc0d2ba03e0c058d0fd4e1: core, JVM, Python, TypeScript, TypeScript PBT, and lint.