[TS] Execute bigint values and arithmetic in usvm-ts #420

Problem

USVM's TypeScript symbolic machine cannot represent or execute BigInt values. TsContext.typeToSort has no BigInt sort, and BigInt cases in binary operators are TODOs. TsBigInt in the test-value API does not provide execution support.

Minimal example

export function isTwoAfterIncrement(x: bigint): boolean {
  return x + 1n === 2n;
}

Expected results: isTwoAfterIncrement(1n) === true and isTwoAfterIncrement(0n) === false. Add a case beyond Number.MAX_SAFE_INTEGER to prevent accidental conversion through IEEE-754 Number.

Acceptance criteria

• Use the distinct BigInt EtsIR type and literal from [TS] Preserve bigint types and literals in native EtsIR jacodb#368; never reinterpret BigInt as Number.
• Represent symbolic BigInt inputs, arithmetic and equality with exact integer semantics for the supported operations.
• Handle BigInt truthiness (0n is false; nonzero BigInt is true) and explicitly reject unsupported mixed BigInt/Number operations according to JavaScript semantics rather than silently coercing them.
• Extract BigInt witnesses as BigInt values and confirm the reached result with concrete TypeScript/Node.js replay.
• Keep unsupported BigInt operations explicit until modeled; they must not be reported as successful exact execution.

Source evidence and verification boundary

• Sort mapping.
• BigInt operator TODOs.
• Disabled BigInt equality test.

This is a source-backed gap. The example has not yet been run as a new end-to-end regression.