diff --git a/AGENTS.md b/AGENTS.md index 6361705..8e92be1 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -127,7 +127,7 @@ Omit `simplifying_assumptions` when no hypothesis rewriting is needed; its list When verifying a small slice of a larger TS project: -- Add `//@ verify` to the function bodies you want verified. As soon as *any* function in the file has it, `lsc` switches to opt-in mode and silently skips the rest. Type and `const` declarations are always extracted. +- Add `//@ verify` to the function bodies you want verified. A marked function, method, or module-level `const` switches `lsc` to opt-in mode. Constants are lowered only when explicitly marked (before the declaration) or transitively referenced by selected code or proof annotations; unrelated initializers cannot block verification. Class methods retain referenced fields (the full shape if `this` is used as a whole), and needed types are retained. - For functions outside the LS fragment that you still want callers to reason about, use `//@ extern` (deterministic axiom) or `//@ havoc` (nondeterministic). - **In-place means in-place.** When the user asks for in-place verification of an existing function, add annotations only. Don't refactor the production code, don't restructure control flow, don't rename things. The point is that the verified function and the shipping function are byte-for-byte the same. diff --git a/SPEC.md b/SPEC.md index e800a8d..f296cb4 100644 --- a/SPEC.md +++ b/SPEC.md @@ -30,7 +30,7 @@ Annotations are TypeScript comments of the form `//@ `. | `backend` | Top of file | Restrict file to a specific backend (see §2.6) | | `option ` | Top of file | Override an eligible `lemmascript.json` option for this file (see §7.6) | | `safe-slice` | Top of file | Legacy alias for `option safe-slice true` (see §2.7) | -| `verify` | Before first statement of function/method body | Mark function for verification (see §2.5) | +| `verify` | Before first statement of function/method body, or before a module-level `const` | Select declaration for verification (see §2.6) | | `requires` | Before first statement of function body | Precondition | | `ensures` | Before first statement of function body | Postcondition (`\result` refers to return value) | | `contract` | Before first statement of function body | Natural-language description of intent — prover-ignored; surfaced by `lsc extract` for vetting against the formal `requires`/`ensures` (see §2.13) | @@ -199,9 +199,9 @@ function isEmptyResult(result: string): boolean { } ``` -**Behavior:** If any function in the file has `//@ verify`, `lsc` switches to selective mode and only extracts functions marked with `//@ verify`. Functions without it are silently skipped. Type declarations, interface declarations, and module-level `const` declarations are always extracted (they may be needed by verified functions). +**Behavior:** A marked function, method, or module-level `const` activates selective mode. Only marked function bodies are extracted. Constants are selected **before their initializers are lowered**: keep those explicitly marked with a leading `//@ verify`, plus transitive dependencies of selected bodies and proof annotations (including loop and ghost annotations). Locally shadowed names do not select module constants. Unrelated unsupported initializers are ignored; unsupported selected dependencies remain errors. Types needed by selected declarations are retained, as are explicit `declare-type` declarations. -If no function in the file has `//@ verify`, all functions are extracted as before. This keeps existing LemmaScript projects (where every function is in-fragment) working without changes. +If no declaration in the file has `//@ verify`, whole-file extraction behaves as before. This keeps existing LemmaScript projects (where every function is in-fragment) working without changes. ### 2.7 Backend Restriction: `//@ backend` @@ -217,7 +217,7 @@ The `safe-slice` option selects JS-clamping semantics for two-arg `arr.slice(lo, ### 2.8 Classes -Class methods can be verified with `//@ verify`. The class fields become Dafny class fields, and `this.field` references work directly. +Class methods can be verified with `//@ verify`. Fields referenced by selected methods or their proof annotations become Dafny class fields, and `this.field` references work directly. Using `this` as a whole (for example, assigning it to an alias) retains the full field shape; unselected methods are not lowered. ```typescript export class Counter { diff --git a/tools/fixtures/selective-class.ts b/tools/fixtures/selective-class.ts new file mode 100644 index 0000000..4f2b624 --- /dev/null +++ b/tools/fixtures/selective-class.ts @@ -0,0 +1,26 @@ +//@ backend dafny + +const UNUSED_PATTERN = /outside/; +const BASE = 1; +const STEP = BASE + 1; +const LIMIT = 100; + +export class Counter { + count = 0; + max = 10; + written = 0; + unused: (value: string) => RegExp = value => new RegExp(value); + + increment(): number { + //@ verify + //@ requires this.count + STEP <= this.max && this.max <= LIMIT + //@ ensures this.count <= this.max + this.written = 1; + this.count = this.count + STEP; + return this.count; + } + + unrelated(): RegExp { + return /unrelated/; + } +} diff --git a/tools/fixtures/selective-extraction.ts b/tools/fixtures/selective-extraction.ts new file mode 100644 index 0000000..fd472d2 --- /dev/null +++ b/tools/fixtures/selective-extraction.ts @@ -0,0 +1,18 @@ +const UNUSED_PATTERN = /outside/; +const BASE = 2; +const STEP = BASE + 1; +const MINIMUM = 0; + +//@ verify +const EXPLICIT = BASE + 2; + +export function advance(n: number): number { + //@ verify + //@ requires n >= MINIMUM + //@ ensures \result === n + STEP && \result >= MINIMUM + return n + STEP; +} + +function unrelated(): RegExp { + return /unrelated/; +} diff --git a/tools/fixtures/unsupported-extraction.ts b/tools/fixtures/unsupported-extraction.ts index 59a5efd..9971e4c 100644 --- a/tools/fixtures/unsupported-extraction.ts +++ b/tools/fixtures/unsupported-extraction.ts @@ -1,3 +1,4 @@ +//@ verify const UNSUPPORTED_PATTERN = /x/; export function fine(n: number): number { diff --git a/tools/src/extract.ts b/tools/src/extract.ts index 795cd28..a861e86 100644 --- a/tools/src/extract.ts +++ b/tools/src/extract.ts @@ -12,6 +12,7 @@ import type { RawExpr, RawStmt, RawFunction, RawModule, RawClass, RawConst, RawG import { normalizeBigIntLiteral } from "./rawir.js"; import { setUserNames, freshName } from "./names.js"; import { DEFAULT_OPTIONS, type LscOptions } from "./config.js"; +import { expressionValueReferences, functionValueReferences } from "./value-references.js"; // ── Expression extraction ──────────────────────────────────── @@ -49,11 +50,9 @@ const _externs = new Map(); * types would emit decls that no emitted declaration mentions. */ const _externSigTypes: { type: Type; node: Node }[] = []; let _currentSourceFile: SourceFile | null = null; -/** True only while extracting a function body. Module-level constants that - * reference cross-file callees (e.g., `BusEvent.define(...)` inside a - * module-level record) would otherwise pollute the output with externs - * that no verified function actually calls — and whose TS return types - * often don't translate to valid Dafny. */ +/** Register cross-file calls while extracting function bodies or constants + * selected by brownfield dependencies. Legacy whole-file constant extraction + * leaves this off to avoid registering unused namespace/initialization code. */ let _inFunctionExtraction = false; /** Effective options for the current extraction. Reset at extractModule entry. */ let _extractOptions: LscOptions = DEFAULT_OPTIONS; @@ -2200,39 +2199,18 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA } } - // Extract module-level const declarations - const constants: RawConst[] = []; + // Index constants without inspecting their types or lowering initializers. + // Selection must happen first: unused brownfield code may be out of model. + const constDecls = new Map(); + const verifiedConsts = new Set(); for (const stmt of sourceFile.getStatements()) { - if (Node.isVariableStatement(stmt)) { - if (hasLeadingDirective(stmt, "skip")) continue; - for (const decl of stmt.getDeclarationList().getDeclarations()) { - if (stmt.getDeclarationList().getFlags() & 2 /* const */) { - const init = decl.getInitializer(); - // Skip huge string constants — they crash the verifier and have no verification value - const initType = decl.getType(); - const isHugeString = (initType.isString() || initType.isStringLiteral()) && (init as Expression).getText().length > 200; - // Skip anonymous-object consts (e.g., `const Util = { dotMatch(s, p) { ... } }`). - // ts-morph names these `__type` / `__object`; Dafny has no model for - // object-namespace-with-methods. The methods themselves should be - // extracted via the function path if marked `//@ verify`. - const declTsType = typeToString(decl.getType()); - const isAnonObject = declTsType.startsWith("__"); - if (init && !isHugeString && !isAnonObject && !Node.isArrowFunction(init)) { - try { - constants.push({ - name: decl.getName(), - tsType: declTsType, - value: extractExpr(init as Expression), - }); - } catch (e) { - const reason = e instanceof Error ? e.message : String(e); - throw new Error( - `Failed to extract const '${decl.getName()}' at ${sourceFile.getBaseName()}:${decl.getStartLineNumber()}: ${reason}`, - ); - } - } - } - } + if (!Node.isVariableStatement(stmt) || stmt.getDeclarationKind() !== "const" + || hasLeadingDirective(stmt, "skip")) continue; + for (const decl of stmt.getDeclarations()) { + const init = decl.getInitializer(); + if (init && Node.isArrowFunction(init)) continue; + constDecls.set(decl.getName(), decl); + if (hasLeadingDirective(stmt, "verify")) verifiedConsts.add(decl.getName()); } } @@ -2359,7 +2337,7 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA !hasLeadingDirective(method, "skip") && hasLineDirective(method.getFullText(), "verify"), ), ); - const hasVerifyDirective = nonExternFns.some(hasVerify) || hasVerifiedClassMethod; + const hasVerifyDirective = nonExternFns.some(hasVerify) || hasVerifiedClassMethod || verifiedConsts.size > 0; const fnsToExtract = hasVerifyDirective ? nonExternFns.filter(hasVerify) : nonExternFns; // `//@ autohavoc` — enable the auto-havoc abstraction (see autohavoc.ts). @@ -2392,6 +2370,86 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA return raw; }); + // Extract selected methods before selecting constants and types, so their + // bodies and specs contribute dependencies just like top-level functions. + const classes: RawClass[] = []; + const classMethodNodes: { node: FunctionDeclaration }[] = []; + for (const cls of sourceFile.getClasses()) { + if (hasLeadingDirective(cls, "skip")) continue; + const methods: RawFunction[] = []; + for (const method of cls.getMethods()) { + if (hasLeadingDirective(method, "skip") || !hasLineDirective(method.getFullText(), "verify")) continue; + const node = method as unknown as FunctionDeclaration; + methods.push(extractFunction(node)); + classMethodNodes.push({ node }); + } + if (methods.length === 0) continue; + const refs = methods.map(functionValueReferences); + // Keep the full shape when `this` escapes (including an alias of `this`). + // Otherwise reads/writes and specs select fields; property names from + // other receivers are conservatively included too. + const fields = cls.getProperties() + .filter(prop => refs.some(r => r.wholeThis || r.fields.has(prop.getName())) + || hasLeadingDirective(prop, "verify")) + .map(prop => ({ name: prop.getName(), tsType: typeToString(prop.getType()) })); + classes.push({ name: cls.getName() ?? "Anonymous", fields, methods }); + } + const allFunctions = [...functions, ...classes.flatMap(cls => cls.methods)]; + const allFunctionNodes = [...fnsToExtract, ...classMethodNodes]; + + const neededConsts = new Set(verifiedConsts); + if (hasVerifyDirective) { + for (const fn of allFunctions) { + for (const name of functionValueReferences(fn).names) neededConsts.add(name); + } + // Same-file extern contracts are emitted too; their bodies stay opaque. + for (const f of allFns) { + if (hasSkip(f) || !hasExtern(f)) continue; + const ext = _externs.get(externName(f) ?? f.name); + if (!ext) continue; + const refs = functionValueReferences({ ...ext, decreases: null, body: [] }); + for (const name of refs.names) neededConsts.add(name); + } + } else { + for (const name of constDecls.keys()) neededConsts.add(name); + } + const extractedConsts = new Map(); + _typeParamMap = new Map(); + // Set iteration visits newly-added dependencies as well, terminating even + // for cycles. Emit in source order below, independent of discovery order. + for (const name of neededConsts) { + const decl = constDecls.get(name); + if (!decl) continue; + const init = decl.getInitializer(); + if (!init) continue; + const prevInFn = _inFunctionExtraction; + try { + const initType = decl.getType(); + const tsType = typeToString(initType); + // Preserve legacy whole-file exclusions. A selected constant must be + // modeled or fail explicitly, even if it is a large string/object. + if (!hasVerifyDirective && (tsType.startsWith("__") + || ((initType.isString() || initType.isStringLiteral()) && init.getText().length > 200))) continue; + _inFunctionExtraction = hasVerifyDirective; + const value = extractExpr(init); + extractedConsts.set(name, { name, tsType, value }); + if (hasVerifyDirective) { + for (const dependency of expressionValueReferences(value).names) neededConsts.add(dependency); + } + } catch (e) { + const reason = e instanceof Error ? e.message : String(e); + throw new Error( + `Failed to extract const '${name}' at ${sourceFile.getBaseName()}:${decl.getStartLineNumber()}: ${reason}`, + ); + } finally { + _inFunctionExtraction = prevInFn; + } + } + const constants = [...constDecls.keys()].flatMap(name => { + const constant = extractedConsts.get(name); + return constant ? [constant] : []; + }); + // Resolve type references in function signatures via ts-morph's type // checker — walk the TypeNode tree, resolve each TypeReferenceNode to its // declaration through symbol resolution, recurse. This is the principled @@ -2453,14 +2511,17 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA return; } } - for (const f of fnsToExtract) { + for (const f of allFunctionNodes) { for (const p of f.node.getParameters()) resolveTypeNodeRefs(p.getTypeNode()); resolveTypeNodeRefs(f.node.getReturnTypeNode()); } + if (hasVerifyDirective) { + for (const c of constants) resolveTypeNodeRefs(constDecls.get(c.name)!.getTypeNode()); + } // Resolve union param types: A | B → intersection of fields const typeDeclMap = new Map(typeDecls.map(d => [d.name, d])); - for (const fn of functions) { + for (const fn of allFunctions) { for (const p of fn.params) { if (!p.tsType.includes(" | ")) continue; const arms = p.tsType.split(" | ").map(a => a.trim()); @@ -2489,7 +2550,7 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA } } - // In brownfield mode, filter consts to only those referenced by verified functions. + // In brownfield mode, retain the types needed by selected declarations. if (hasVerifyDirective) { const referencedNames = new Set(); function collectNames(stmts: RawStmt[]) { @@ -2524,7 +2585,7 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA // spec references stay exact-match (so a body `let xs: Hunk[]` doesn't pull // `Hunk` into the filter early and reorder output that resolveType re-adds). const sigTypes = new Set(); - for (const fn of functions) { + for (const fn of allFunctions) { for (const p of fn.params) { referencedNames.add(p.tsType); sigTypes.add(p.tsType); } referencedNames.add(fn.returnType); sigTypes.add(fn.returnType); collectNames(fn.body); @@ -2535,27 +2596,11 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA } } } - // A constant's initializer can reference other constants - // (`const ZERO_NINE = ZERO + nthDigit(-1)`). Close over those initializers - // before filtering — mirroring the transitive type filter below — or a - // constant reachable only from another constant is dropped and the backend - // sees an undefined name. - // Snapshot first: what the closure adds are VALUE references, and a value - // and a type can share a name (`const Action = Schema.Literals(…)` next to - // `type Action = Schema.Schema.Type`). Keeping the constant - // alive must not also drag in the unrelated type alias, so the type filter - // below runs off the pre-closure set. - const typeReferencedNames = new Set(referencedNames); - for (let grew = true; grew; ) { - grew = false; - for (const c of constants) { - if (!referencedNames.has(c.name)) continue; - const before = referencedNames.size; - collectNamesExpr(c.value); - if (referencedNames.size !== before) grew = true; - } + // Value names from constant initializers must not select same-named types + // (e.g. a schema value and its inferred type alias). Their TYPES do matter. + for (const tsType of [...constants.map(c => c.tsType), ...classes.flatMap(c => c.fields.map(f => f.tsType))]) { + for (const m of tsType.matchAll(/\b([a-zA-Z_]\w*)\b/g)) referencedNames.add(m[1]); } - constants.splice(0, constants.length, ...constants.filter(c => referencedNames.has(c.name))); // Filter types to only those referenced by verified functions (transitive) const neededTypes = new Set(); function markType(name: string) { @@ -2563,13 +2608,15 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA const d = typeDecls.find(t => t.name === name); if (!d) return; neededTypes.add(name); + if (d.aliasOf) + for (const m of d.aliasOf.matchAll(/\b([a-zA-Z_]\w*)\b/g)) markType(m[1]); for (const f of d.fields ?? []) - for (const m of f.tsType.matchAll(/\b([A-Z]\w*)\b/g)) markType(m[1]); + for (const m of f.tsType.matchAll(/\b([a-zA-Z_]\w*)\b/g)) markType(m[1]); for (const v of d.variants ?? []) for (const f of v.fields) - for (const m of f.tsType.matchAll(/\b([A-Z]\w*)\b/g)) markType(m[1]); + for (const m of f.tsType.matchAll(/\b([a-zA-Z_]\w*)\b/g)) markType(m[1]); } - for (const name of typeReferencedNames) markType(name); + for (const name of referencedNames) markType(name); // Signature types also mark their base after stripping array/optional // WRAPPERS (`Out[]`/`Msg | undefined` → `Out`/`Msg`), so a function returning // a local `Out[]` keeps `Out`. Wrappers only — never dig into generic args @@ -2644,9 +2691,9 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA } } } - for (let i = 0; i < fnsToExtract.length; i++) { - const f = fnsToExtract[i]; - const fn = functions[i]; + for (let i = 0; i < allFunctionNodes.length; i++) { + const f = allFunctionNodes[i]; + const fn = allFunctions[i]; // Skip params whose TS type was overridden by `//@ type ` // — the verification works against the override, so cross-file resolving // the original type pulls in unused datatypes (often with unsupported @@ -2657,12 +2704,18 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA resolveType(p.getType(), p); } } + if (hasVerifyDirective) { + for (const c of constants) { + const decl = constDecls.get(c.name)!; + resolveType(decl.getType(), decl); + } + } // Extern signature types: see _externSigTypes. for (const r of _externSigTypes) resolveType(r.type, r.node); // Resolve anonymous object return types into synthetic named types - for (let i = 0; i < fnsToExtract.length; i++) { - const f = fnsToExtract[i]; - const fn = functions[i]; + for (let i = 0; i < allFunctionNodes.length; i++) { + const f = allFunctionNodes[i]; + const fn = allFunctions[i]; const retType = f.node.getReturnType(); // Prefer alias symbol (named type aliases) over underlying object symbol (__type) const aliasSym = retType.getAliasSymbol(); @@ -2736,24 +2789,6 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA } } - // Extract classes with //@ verify methods - const classes: RawClass[] = []; - for (const cls of sourceFile.getClasses()) { - if (hasLeadingDirective(cls, "skip")) continue; - const methods: RawFunction[] = []; - for (const method of cls.getMethods()) { - if (hasLeadingDirective(method, "skip")) continue; - if (!method.getFullText().includes('//@ verify')) continue; - methods.push(extractFunction(method as any)); - } - if (methods.length === 0) continue; - const fields: { name: string; tsType: string }[] = []; - for (const prop of cls.getProperties()) { - fields.push({ name: prop.getName(), tsType: typeToString(prop.getType()) }); - } - classes.push({ name: cls.getName() ?? "Anonymous", fields, methods }); - } - // Clear the synth-union accumulator so typeToString reverts to plain // union stringification outside of an extractModule call. _synthArrayUnions = null; diff --git a/tools/src/value-references.ts b/tools/src/value-references.ts new file mode 100644 index 0000000..3448f5e --- /dev/null +++ b/tools/src/value-references.ts @@ -0,0 +1,138 @@ +/** Value dependencies of extracted code, including its proof annotations. + * Walk the verification model so skipped/havoced code contributes no dependencies. + * Keep binders in scope: a local named like a module constant does not use it. */ +import type { RawExpr, RawFunction, RawStmt } from "./rawir.js"; +import { parseExpr } from "./specparser.js"; + +class ValueReferences { + readonly names = new Set(); + readonly fields = new Set(); + wholeThis = false; + + expr(e: RawExpr, bound: ReadonlySet = new Set()): void { + const visit = (expr: RawExpr) => this.expr(expr, bound); + switch (e.kind) { + case "var": + // Compound assignments/increments can encode a path as a var name. + if (e.name.includes(".") || e.name.includes("[")) { + this.spec(e.name, bound); + } else if (!bound.has(e.name)) { + this.names.add(e.name); + if (e.name === "this") this.wholeThis = true; + } + return; + case "binop": visit(e.left); visit(e.right); return; + case "unop": case "nonNull": visit(e.expr); return; + case "call": visit(e.fn); e.args.forEach(visit); return; + case "field": + this.fields.add(e.field); + // A direct field read does not require the whole receiver's shape. + if (e.obj.kind !== "var" || e.obj.name !== "this") visit(e.obj); + return; + case "index": + if (e.idx.kind === "str") this.fields.add(e.idx.value); + visit(e.obj); visit(e.idx); return; + case "record": + if (e.spread) visit(e.spread); + e.fields.forEach(f => visit(f.value)); + return; + case "recordMerge": visit(e.base); visit(e.override); return; + case "arrayLiteral": e.elems.forEach(visit); return; + case "emptyCollection": e.initElems?.forEach(visit); return; + case "conditional": visit(e.cond); visit(e.then); visit(e.else); return; + case "nullish": visit(e.left); visit(e.right); return; + case "optChain": + visit(e.obj); + for (const step of e.chain) { + if (step.kind === "field") this.fields.add(step.name); + if (step.kind === "call") step.args.forEach(visit); + if (step.kind === "index") visit(step.idx); + } + return; + case "lambda": { + const scope = new Set([...bound, ...e.params.map(p => p.name)]); + if (Array.isArray(e.body)) this.block(e.body, scope); + else this.expr(e.body, scope); + return; + } + case "forall": case "exists": + this.expr(e.body, new Set([...bound, e.var])); + return; + case "num": case "bigint": case "str": case "bool": case "result": case "havoc": + return; + } + } + + spec(text: string | null, bound: ReadonlySet): void { + if (text !== null) this.expr(parseExpr(text), bound); + } + + block(stmts: RawStmt[], outer: ReadonlySet): void { + const bound = new Set(outer); + for (const s of stmts) { + switch (s.kind) { + case "let": + this.expr(s.init, bound); + bound.add(s.name); + break; + case "ghostLet": + // These constructors have type arguments but no value arguments; + // resolve.ts handles them separately from the spec parser too. + if (!/^new\s+(Set|Map)<(.+)>\(\)$/.test(s.init)) this.spec(s.init, bound); + bound.add(s.name); + break; + case "assign": + this.expr({ kind: "var", name: s.target }, bound); + this.expr(s.value, bound); + break; + case "ghostAssign": + this.expr({ kind: "var", name: s.target }, bound); + this.spec(s.value, bound); + break; + case "return": this.expr(s.value, bound); break; + case "expr": this.expr(s.expr, bound); break; + case "assert": this.spec(s.expr, bound); break; + case "if": + this.expr(s.cond, bound); + this.block(s.then, bound); + this.block(s.else, bound); + break; + case "while": + this.expr(s.cond, bound); + s.invariants.forEach(spec => this.spec(spec, bound)); + this.spec(s.decreases, bound); + this.spec(s.doneWith, bound); + this.block(s.body, bound); + break; + case "forof": { + this.expr(s.iterable, bound); + const scope = new Set([...bound, ...s.names]); + s.invariants.forEach(spec => this.spec(spec, scope)); + this.spec(s.doneWith, scope); + this.block(s.body, scope); + break; + } + case "switch": + this.expr(s.expr, bound); + s.cases.forEach(c => this.block(c.body, bound)); + this.block(s.defaultBody, bound); + break; + case "break": case "continue": case "throw": break; + } + } + } +} + +export function functionValueReferences(fn: Pick) { + const refs = new ValueReferences(); + const bound = new Set(fn.params.map(p => p.name)); + for (const spec of [...fn.requires, ...fn.ensures, fn.decreases]) refs.spec(spec, bound); + refs.block(fn.body, bound); + return refs; +} + +export function expressionValueReferences(expr: RawExpr) { + const refs = new ValueReferences(); + refs.expr(expr); + return refs; +} diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh index 4e5e957..0c5d986 100755 --- a/tools/test-fixtures.sh +++ b/tools/test-fixtures.sh @@ -52,6 +52,22 @@ cp -R tools/fixtures/utf16-project "$fixture_dir/utf16-project" cp tools/fixtures/optional-binder-collisions.ts "$fixture_dir/optional-binder-collisions.ts" cp tools/fixtures/unpaired-surrogate.ts "$fixture_dir/unpaired.ts" cp tools/fixtures/optional-guard-order.ts "$fixture_dir/optional-guard-order.ts" +cp tools/fixtures/selective-extraction.ts "$fixture_dir/selective-extraction.ts" +cp tools/fixtures/selective-class.ts "$fixture_dir/selective-class.ts" + +# Selection precedes lowering: unused unsupported constants/class fields must +# not block generation, while every needed constant remains available to prove. +npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/selective-extraction.ts" +npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/selective-class.ts" +# Mutating class methods use the usual hand-written modifies proof addition. +node --input-type=module - "$fixture_dir/selective-class.dfy" <<'JS' +import { readFileSync, writeFileSync } from "node:fs"; +const file = process.argv[2]; +writeFileSync(file, readFileSync(file, "utf8").replace( + " method increment() returns (res: int)\n", "$& modifies this\n")); +JS +npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/selective-class.ts" +npx tsx tools/src/lsc.ts gen --backend=lean "$fixture_dir/selective-extraction.ts" npx tsx tools/src/lsc.ts gen --backend=dafny "$fixture_dir/impure.ts" if ! grep -Fq 'method {:axiom} rollDie' "$fixture_dir/impure.dfy.gen"; then diff --git a/tools/tests/selective-extraction.test.ts b/tools/tests/selective-extraction.test.ts new file mode 100644 index 0000000..3723af4 --- /dev/null +++ b/tools/tests/selective-extraction.test.ts @@ -0,0 +1,308 @@ +import { test } from "node:test"; +import assert from "node:assert/strict"; +import { Project, ScriptTarget } from "ts-morph"; +import { extractModule } from "../src/extract.ts"; +import { resolveModule } from "../src/resolve.ts"; +import { narrowModule } from "../src/narrow.ts"; +import { transformModuleDafny, transformModuleLean } from "../src/transform.ts"; +import { emitDafnyFile } from "../src/dafny-emit.ts"; +import { emitLeanFile, resetLeanModule } from "../src/lean-emit.ts"; +import type { RawModule } from "../src/rawir.ts"; + +function extract(text: string, checkTypes = true) { + const project = new Project({ compilerOptions: { + strict: true, target: ScriptTarget.ESNext, lib: ["lib.esnext.d.ts"], types: [], skipLibCheck: true, + } }); + const source = project.createSourceFile("selective.ts", text); + if (checkTypes) assert.deepEqual(project.getPreEmitDiagnostics().map(d => d.getMessageText()), []); + return extractModule(source); +} + +function dafny(raw: RawModule) { + const { typesFile, defFile } = transformModuleDafny(narrowModule(resolveModule(raw))); + return emitDafnyFile({ ...defFile, decls: [...(typesFile?.decls ?? []), ...defFile.decls] }); +} + +test("unused unsupported constants are excluded before extraction for both backends", () => { + const raw = extract(` + const UNUSED = /unused/; + const BASE = 3, OTHER_UNUSED = /other/; + const OFFSET = BASE + 4; + function selected(n: number): number { + //@ verify + //@ ensures \\result === n + OFFSET + return n + OFFSET; + } + function unrelated() { return /outside/; } + `); + assert.deepEqual(raw.constants.map(c => c.name), ["BASE", "OFFSET"]); + assert.deepEqual(raw.functions.map(f => f.name), ["selected"]); + const dafnyText = dafny(raw); + const lean = transformModuleLean(narrowModule(resolveModule(raw))); + resetLeanModule(); + const leanText = [lean.typesFile, lean.defFile].filter(f => f !== null).map(f => emitLeanFile(f!)).join("\n"); + for (const text of [dafnyText, leanText]) { + assert.match(text, /BASE/); + assert.match(text, /OFFSET/); + assert.doesNotMatch(text, /UNUSED|unrelated/); + } +}); + +test("a marked constant activates selective mode and retains its transitive dependencies", () => { + const raw = extract(` + const UNUSED = /unused/; + const BASE = 2; + //@ verify + const CHOSEN = BASE + 1; + function unrelated() { return /outside/; } + `); + assert.deepEqual(raw.constants.map(c => c.name), ["BASE", "CHOSEN"]); + assert.deepEqual(raw.functions, []); + assert.match(dafny(raw), /const CHOSEN: int := \(BASE \+ 1\)/); +}); + +for (const [name, text] of [ + ["direct dependency", ` + const BAD = /bad/; + function selected(s: string) { + //@ verify + return BAD.test(s); + }`], + ["transitive dependency", ` + const BAD = /bad/; + const ALIAS = BAD; + function selected(s: string) { + //@ verify + return ALIAS.test(s); + }`], + ["explicit selection", ` + //@ verify + const BAD = /bad/;`], + ["whole-file mode", ` + const BAD = /bad/; + function selected(n: number) { return n; }`], +] as const) { + test(`unsupported selected constants still fail: ${name}`, () => { + assert.throws(() => extract(text), /Failed to extract const 'BAD' at selective\.ts:\d+: Unsupported expression: \/bad\//); + }); +} + +test("dependencies include every statement/spec position and collection elements", () => { + const names = ["PRE", "POST", "DEC", "INV", "LOOP_DEC", "DONE", "ASSERTED", "ASSUMED", "GHOST", "UPDATE", "CASE", "DEFAULT", "ELEMENT"]; + const raw = extract(` + ${names.map(name => `const ${name} = 1;`).join("\n")} + const UNUSED = /unused/; + function selected(n: number, tag: string): number { + //@ verify + //@ requires n >= PRE + //@ ensures \\result >= POST + //@ decreases DEC + //@ ghost let g = GHOST + //@ ghost g = UPDATE + //@ ghost let seen = new Set() + //@ assert n >= ASSERTED + //@ assume n >= ASSUMED + let i = 0; + while (i < n) { + //@ invariant i <= n + INV + //@ decreases n + LOOP_DEC - i + //@ done_with i >= DONE + i++; + } + const values = new Set([ELEMENT]); + switch (tag) { + case "a": return CASE; + default: return DEFAULT; + } + } + `); + assert.deepEqual(raw.constants.map(c => c.name), names); +}); + +test("params, locals, loop/lambda/quantifier binders and property names do not select constants", () => { + const raw = extract(` + const param = /bad/, local = /bad/, item = /bad/, lambda = /bad/, q = /bad/; + const field = /bad/, ghost = /bad/, text = /bad/; + function selected(param: number, box: { field: number }, xs: number[]): number { + //@ verify + //@ requires forall(q, q === q) + //@ ensures \\result >= param + //@ contract mentions text without depending on it + //@ ghost let ghost = 0 + //@ assert ghost === 0 + let local = param + box.field; + for (const item of xs) { + //@ invariant item === item + local += item; + } + const mapped = xs.map(lambda => lambda + local); + const label = "text"; + return local; + } + `); + assert.deepEqual(raw.constants, []); +}); + +test("shadowing in one branch does not hide a dependency in another", () => { + const raw = extract(` + const LIMIT = 2; + function selected(flag: boolean): number { + //@ verify + if (flag) { + const LIMIT = 1; + return LIMIT; + } + return LIMIT; + } + `); + assert.deepEqual(raw.constants.map(c => c.name), ["LIMIT"]); +}); + +test("skipped and havoced statements do not retain their source dependencies", () => { + const raw = extract(` + const UNUSED = /unused/; + //@ skip + //@ verify + const SKIPPED = /skipped/; + function selected(s: string): boolean { + //@ verify + //@ skip + UNUSED.test(s); + //@ havoc + const answer = UNUSED.test(s); + return answer; + } + `); + assert.deepEqual(raw.constants, []); +}); + +test("expression arrows and inline verified callbacks retain constant dependencies", () => { + const raw = extract(` + const UNUSED = /unused/; + const ARROW = 1, CALLBACK = 2; + //@ verify + const selected = (n: number): number => n + ARROW; + function register(f: (n: number) => number) {} + register((n: number) => { + //@ verify + return n + CALLBACK; + }); + `); + assert.deepEqual(raw.constants.map(c => c.name), ["ARROW", "CALLBACK"]); + assert.equal(raw.functions.length, 2); +}); + +test("constant cycles terminate during dependency selection", () => { + const raw = extract(` + const FIRST: number = SECOND; + const SECOND: number = FIRST; + function selected(): number { + //@ verify + return FIRST; + } + `, false); // Deliberately invalid TS: selection must terminate; verification rejects the cycle. + assert.deepEqual(raw.constants.map(c => c.name), ["FIRST", "SECOND"]); +}); + +test("class methods select constants, written/read fields, and spec-only fields before lowering", () => { + const raw = extract(` + const UNUSED = /unused/; + const BASE = 1, STEP = BASE + 1, LIMIT = 100; + class Counter { + count = 0; + max = 10; + written = 0; + unused: (value: string) => RegExp = value => new RegExp(value); + increment(): number { + //@ verify + //@ requires this.count + STEP <= this.max && this.max <= LIMIT + //@ ensures this.count <= this.max + this.written = 1; + this.count = this.count + STEP; + return this.count; + } + unrelated() { return /outside/; } + } + `); + assert.deepEqual(raw.constants.map(c => c.name), ["BASE", "STEP", "LIMIT"]); + assert.deepEqual(raw.classes[0].fields.map(f => f.name), ["count", "max", "written"]); + assert.deepEqual(raw.classes[0].methods.map(f => f.name), ["increment"]); + assert.doesNotMatch(dafny(raw), /unused|UNUSED|unrelated/); +}); + +test("using this as a whole retains the class shape", () => { + const raw = extract(` + class Counter { + count = 0; + other = 1; + selected(): number { + //@ verify + const alias = this; + return alias.count; + } + } + `); + assert.deepEqual(raw.classes[0].fields.map(f => f.name), ["count", "other"]); +}); + +test("types used only by selected constants are retained", () => { + const raw = extract(` + type Box = { count: number }; + type Boxes = Box[]; + //@ verify + const BOXES: Boxes = [{ count: 1 }]; + `); + assert.deepEqual(raw.typeDecls.map(d => d.name), ["Box", "Boxes"]); + assert.match(dafny(raw), /datatype Box/); +}); + +test("a type reference does not select a same-named module constant", () => { + const raw = extract(` + const Box = /unused/; + type Box = { count: number }; + function selected(box: Box): number { + //@ verify + return box.count; + } + `); + assert.deepEqual(raw.constants, []); + assert.match(dafny(raw), /datatype Box/); +}); + +test("same-file extern contracts retain constants without inspecting the extern body", () => { + const raw = extract(` + const UNUSED = /outside/; + const LIMIT = 10; + //@ extern + function external(s: string): number { + //@ ensures \\result <= LIMIT + return UNUSED.test(s) ? 0 : 1; + } + function selected(s: string): number { + //@ verify + return external(s); + } + `); + assert.deepEqual(raw.constants.map(c => c.name), ["LIMIT"]); + assert.equal(raw.externs[0].qualified, "external"); +}); + +test("selected constants resolve imported types and calls", () => { + const project = new Project({ compilerOptions: { strict: true, target: ScriptTarget.ESNext, types: [] } }); + project.createSourceFile("dependency.ts", ` + export type Box = { count: number }; + export function size(n: number): number { return n; } + `); + const source = project.createSourceFile("selective.ts", ` + import { type Box, size } from "./dependency"; + const UNUSED = /unused/; + //@ verify + const BOX: Box = { count: size(1) }; + `); + assert.deepEqual(project.getPreEmitDiagnostics().map(d => d.getMessageText()), []); + const raw = extractModule(source); + assert.deepEqual(raw.constants.map(c => c.name), ["BOX"]); + assert.equal(raw.externs[0].qualified, "size"); + assert.deepEqual(raw.typeDecls.map(d => d.name), ["Box"]); + assert.match(dafny(raw), /datatype Box/); +});