in verify mode, const are now opt-in, only if used by verify functions

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.
 

SPEC.md

@@ -30,7 +30,7 @@ Annotations are TypeScript comments of the form `//@ <keyword> <expression>`.
 | `backend` | Top of file | Restrict file to a specific backend (see §2.6) |
 | `option <key> <value>` | 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 {

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/;
+  }
+}

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/;
+}

tools/fixtures/unsupported-extraction.ts

@@ -1,3 +1,4 @@
+//@ verify
 const UNSUPPORTED_PATTERN = /x/;
 
 export function fine(n: number): number {