[TS] Model property presence and mutations on symbolic objects (#425)

[CaelmBleidd]

Closes #425.

Object literals and symbolic input objects now track property presence separately from the stored value. After obj.fresh = undefined, "fresh" in obj is true; after delete obj.fresh, it is false and reads return undefined. Writes can add undeclared fields and change their runtime kind without requiring the receiver's nominal type to declare that field.

TsOptions.inputPropertyPresence controls initial own-property assumptions for symbolic inputs:

Policy	Initial presence
DECLARED_FIELDS (default)	Required declared fields exist; optional and undeclared fields have symbolic presence. Inherited declarations and field redeclarations are respected.
SYMBOLIC	Every queried field may be present or absent.
ASSUME_PRESENT	Every queried field initially exists.
ASSUME_ABSENT	Every queried field is initially absent.

Writes and deletions override every policy. A present optional property may still contain undefined.

Supported behavior:

• Concrete dot, bracket, and in keys, including numeric, empty, and Unicode names.
• Boolean, number, string, null, undefined, object, and array payloads; literal and symbolic writes; copying unresolved values and changing runtime kinds.
• Deletion/restoration, conditional mutations, aliases, nested objects and arrays, consistent reads, typeof, strict equality, string length/concatenation, and before/after snapshots for the covered scenarios.

Conditional heap references use StepScope.fork: the cached model orders the branches, and every other feasible receiver is scheduled at the same statement. Array storage lookup consumes the resulting leaf reference. Shared helpers resolve an object literal's own declaration, check unsupported prototype behavior, and join unresolved payloads with their kind selectors. Field reads separate presence, storage selection, initial annotation constraints, and value materialization; initial string constraints apply only while the initial value is active. An explicit internal runtime-object type replaces the empty structural-type filter. Mutation regions are named for both writes and deletions.

The one-line core fix forwards ignoreNullRefs when splitting conditional references. Without it, copying an absent field loses its undefined branch; both the core round-trip regression and a Node-replayed unknown-value copy reproduce the defect.

Symbolic keys, prototype lookup/mutation (including class prototype methods), named input-array properties, and in on arrays remain explicit unsupported outcomes. Arrays stored in object properties support element reads and writes.

Validation on ff1890aa4:

• Full usvm-ts: 1035 passed, 142 skipped, 0 failures.
• Full usvm-ts-calls: 13 passed, 0 failures.
• All 18 affected property tests passed, including Node.js replay. Supported scenarios share one exhaustive analysis between discoverProperties and replay; unsupported outcomes retain separate checks.
• Both dynamic-field/nominal-receiver regressions passed all ten repetitions; the runtime-object constraint has a dedicated primitive/reference contract test.
• TypeScript Detekt main/test: 0 findings. git diff --check passed.
• Unchanged core fix was separately verified on JDK 11: 221 passed, 1 skipped, 0 failures.

Remote CI is reported separately on the PR.