[PBT] Admit pure computed class keys and static cache initialization

usvm-ts-fast-check/fast-check-adapter/src/module-initialization.ts

@@ -73,6 +73,34 @@ export function unsupportedModuleInitialization(
     return declaredBeforeUse ? initializer(declaration.initializer, seen) : undefined
   }
 
+  const pureComputedName = (name: ts.ComputedPropertyName): boolean => {
+    if (initializer(name.expression) === 'primitive') return true
+
+    const expression = name.expression
+    if (!ts.isPropertyAccessExpression(expression) || expression.name.text !== 'iterator'
+      || !ts.isIdentifier(expression.expression) || expression.expression.text !== 'Symbol') return false
+    // The checked source program has no default library. No source binding means the standard runtime global.
+    return checker.getSymbolAtLocation(expression.expression) === undefined
+  }
+
+  const isStatic = (member: ts.ClassElement): boolean => ts.canHaveModifiers(member)
+    && !!ts.getModifiers(member)?.some(modifier => modifier.kind === ts.SyntaxKind.StaticKeyword)
+
+  const pureStaticField = (member: ts.ClassElement, members: ts.NodeArray<ts.ClassElement>): boolean => {
+    if (!ts.isPropertyDeclaration(member) || !member.initializer || !isStatic(member)) return true
+    if (!ts.isIdentifier(member.name)) return false
+    // Also safe when a TypeScript target emits a strict assignment rather than DefineField.
+    const constructorProperties = ['prototype', '__proto__', 'name', 'length', 'caller', 'arguments']
+    if (constructorProperties.includes(member.name.text)) return false
+    const name = member.name.text
+    const collidesWithStaticMember = members.some(other => {
+      if (other === member || !isStatic(other) || !other.name) return false
+      if (ts.isComputedPropertyName(other.name)) return true
+      return (ts.isIdentifier(other.name) || ts.isStringLiteralLike(other.name)) && other.name.text === name
+    })
+    return !collidesWithStaticMember && initializer(member.initializer) !== undefined
+  }
+
   const supported = (statement: ts.Statement): boolean => {
     if (ts.isImportDeclaration(statement) || ts.isExportDeclaration(statement)
       || ts.isFunctionDeclaration(statement) || ts.isInterfaceDeclaration(statement)
@@ -89,10 +117,9 @@ export function unsupportedModuleInitialization(
       const decorated = (ts.getDecorators(statement)?.length ?? 0) > 0
       if (extendsRuntimeBase || decorated) return false
       return statement.members.every(member => !ts.isClassStaticBlockDeclaration(member)
-        && !(member.name && ts.isComputedPropertyName(member.name))
+        && !(member.name && ts.isComputedPropertyName(member.name) && !pureComputedName(member.name))
         && !(ts.canHaveDecorators(member) && ts.getDecorators(member)?.length)
-        && !(ts.isPropertyDeclaration(member) && member.initializer
-          && member.modifiers?.some(modifier => modifier.kind === ts.SyntaxKind.StaticKeyword)))
+        && pureStaticField(member, statement.members))
     }
     if (ts.isEnumDeclaration(statement)) {
       return statement.members.every(member => !member.initializer || ts.isLiteralExpression(member.initializer))

usvm-ts-fast-check/fast-check-adapter/test/local-source-closure.test.ts

@@ -180,6 +180,49 @@ test('imported class implements an erased interface without a runtime initializa
   })
 })
 
+for (const [name, declaration] of [
+  ['literal string', "export class Subject { ['value'] = 1; ['read']() { return this.value; } }"],
+  ['signed number', 'export class Subject { [-2] = 1; [3]() { return 7; } }'],
+  ['primitive constant', "const KEY = 'read'; export class Subject { [KEY]() { return 7; } }"],
+  ['intrinsic iterator', 'export class Subject { [Symbol.iterator]() { return { next() { return { done: true }; } }; } }'],
+  ['static empty cache', 'export class Subject { private static cache: number[] = []; }'],
+  ['static constant alias', 'const CACHE = [1, 2]; export class Subject { private static cache = CACHE; }'],
+] as const) {
+  test(`imported class accepts pure ${name} without evaluating its body`, () => {
+    workspace({
+      'wrapper.ts': "import { Subject } from './subject'; export function scenario() { return new Subject(); }",
+      'subject.ts': declaration,
+    }, root => {
+      const result = inspectLocalSourceClosure(root, path.join(root, 'wrapper.ts'))
+
+      assert.deepEqual(result, { files: ['subject.ts', 'wrapper.ts'] })
+    })
+  })
+}
+
+for (const [name, declaration] of [
+  ['effectful call', "function key() { throw Error('must not execute'); } export class Subject { [key()]() {} }"],
+  ['mutable binding', "let KEY = 'read'; export class Subject { [KEY]() {} }"],
+  ['object coercion', "const KEY = { toString() { throw Error('must not execute'); } }; export class Subject { [KEY]() {} }"],
+  ['shadowed Symbol', "const Symbol = { iterator: 'read' }; export class Subject { [Symbol.iterator]() {} }"],
+  ['getter on shadowed Symbol', "const Symbol = { get iterator() { throw Error('must not execute'); } }; export class Subject { [Symbol.iterator]() {} }"],
+  ['other Symbol property', 'export class Subject { [Symbol.toStringTag]() {} }'],
+  ['static accessor collision', "export class Subject { static set cache(value: unknown) { throw Error('must not execute'); } static cache = []; }"],
+  ['constructor property assignment', "export class Subject { static name = 'renamed'; }"],
+] as const) {
+  test(`imported class keeps ${name} outside the initialization contract`, () => {
+    workspace({
+      'wrapper.ts': "import { Subject } from './subject'; export function scenario() { return new Subject(); }",
+      'subject.ts': declaration,
+    }, root => {
+      const result = inspectLocalSourceClosure(root, path.join(root, 'wrapper.ts'))
+
+      assert.equal(result.reasonCode, 'TOP_LEVEL_INITIALIZATION_UNSUPPORTED')
+      assert.match(result.diagnostic!, /subject\.ts/)
+    })
+  })
+}
+
 for (const [name, declaration] of [
   ['effectful extends expression', 'function base() { throw new Error("must not execute"); } export class Subject extends base() {}'],
   ['plain runtime extends', 'class Base {} export class Subject extends Base {}'],