[TS] Execute modeled Number exponentiation (#428)

[CaelmBleidd]

Scope

Implements the modeled part of #428 for JavaScript Number exponentiation.

Stacked on #455 (caelmbleidd/ts-422-string-value-equality) at 127ecb5df35366c550a32725cf4e6af25208f673. This PR has five linear #428 implementation commits through de035f9f113b1289db9532706da200c5caf57974, followed by the Node replay test cleanup at 377f02d85acf07961ec3e99dc845ed8fedd48170. The five-commit implementation aggregate through de035f9f has the same patch-id as the old #428 range above the previous #455 base 7527353569ca3235f939e8c0305535d02e419ed4. #455 supplies the reusable unsupported-path outcome contract and is stacked on #453.

• Number bases support fixed exponents 0, 1, 2, and 0.5. The square-root case maps both signed zeros to +0 and -Infinity to +Infinity as JavaScript requires.
• Concrete special cases ±0 ** -1 and -1 ** ±Infinity keep their exact discrete results.
• Other concrete powers, symbolic exponents, other powers of symbolic bases, and operand conversions outside the existing Number/Boolean/null/undefined model raise UnsupportedOperationException instead of inventing a result. In particular, 0.1 ** 0.7 is reported as unsupported.

The floating-point SMT model has no general power operation, and JVM Math.pow can differ from Node.js by one ULP. This PR deliberately limits support to the cases above. A pinned review of the rebased head de035f9f found duplicate Node process handling in its regression test; 377f02d8 replaces it with the shared replay utility. Pinned core correctness and AI code hygiene my-review passes of the current head found no actionable defects. This PR remains draft because #428 covers general exponentiation beyond these modeled cases.

What remains for #428

• Model powers of a symbolic base for exponents beyond 0, 1, 2, and 0.5, and symbolic exponents.
• Handle other concrete powers with JavaScript-compatible IEEE-754 results, including cases where JVM Math.pow differs by one ULP.
• Handle operand conversions beyond the existing Number/Boolean/null/undefined model. Until then, these paths must stay explicit unsupported outcomes.

Verification

• On current head 377f02d8, with local JacoDB [TS PBT] Schedule assertion, coverage and hypothesis targets under one budget #399 (b5e10a1a) substituted, the focused Exponentiation suite passed 8/8 tests, including Node replay; :usvm-ts:detektTest and git diff --check passed. The scenario assertions and 10-second timeout are preserved through the shared assertNodeReplay helper.
• On preceding head de035f9f, Division, Remainder, and Neg passed 10 tests with 3 existing skips, and :usvm-ts:detektMain passed.
• The full :usvm-ts:test run on preceding head de035f9f and the same JacoDB revision ran 1,110 tests: 967 passed, 143 skipped, no failures or errors.
• Ordinary analyzeWithOutcome reports unmodeled powers in unsupportedPaths, with no completed state, while supported powers have no unsupported paths. Generated square(3), signed-zero, and negative-infinity witnesses replay in Node.js with Object.is.
• The source-level 0.1 ** 0.7 regression verifies an unsupported analysis outcome and executes the same TypeScript function in Node.js without relying on a version-specific expected bit pattern.
• The symbolic reciprocal path is explicitly unsupported because replacing x ** -1 with FP division is not guaranteed to preserve JavaScript rounding. Tests also replay concrete NaN, infinity, signed-zero, and fractional-power cases in Node.js.
• The earlier manually dispatched CI run 37075099806 belongs to the previous stacked head. Local checks above do not establish CI or general JavaScript exponentiation correctness for the current head.