fix: fail on //@ annotations that lsc does not read

SPEC.md

@@ -51,6 +51,8 @@ Annotations are TypeScript comments of the form `//@ <keyword> <expression>`.
 | `autohavoc` | File-level, or before a `//@ verify` function | Abstract every unmodellable expression to a nondeterministic value, so verification rests only on declared contracts (see §2.12). Dafny only. |
 | `skip` | Before a statement or top-level value declaration | Omit it from the verification model (for side-effect-only code or an intentionally unsupported declaration). |
 
+`lsc` rejects a `//@` comment it does not read: a malformed one, an unknown keyword, or a `requires`, `ensures`, `contract`, `invariant`, `decreases`, `done_with` or `type` placed where nothing takes it. Placement is not checked inside declarations left out on purpose (unselected, `extern` or `skip`), and TypeScript's own `//@ts-…` comments are left alone.
+
 ### 2.2 Spec Expression Grammar
 
 At top level, `//@ skip` may precede a function, class, or `const` declaration;

examples/nullableArray.ts

@@ -67,7 +67,6 @@ export function dropOrphans(messages: Message[]): Message[] {
 
   let i = 0;
   while (i < messages.length) {
-    //@ type i nat
     //@ invariant i <= messages.length
     //@ invariant filteredContents.length === messages.length
     const cur = filteredContents[i];
@@ -80,7 +79,6 @@ export function dropOrphans(messages: Message[]): Message[] {
   const result: Message[] = [];
   let j = 0;
   while (j < messages.length) {
-    //@ type j nat
     //@ invariant j <= messages.length
     //@ invariant result.length <= j
     const f = filteredContents[j];

examples/readonlyArray.ts

@@ -14,6 +14,5 @@ export function firstOrZero(xs: readonly number[]): number {
 
 export function lengthOf<T>(xs: ReadonlyArray<T>): number {
   //@ ensures \result === xs.length
-  //@ type T
   return xs.length;
 }

examples/toposort.ts

@@ -72,7 +72,6 @@ export function topologicalSort(
   let sorted: string[] = [];
   let qHead = 0;
   while (qHead < queue.length) {
-    //@ type qHead nat
     //@ invariant qHead <= queue.length
     //@ invariant sorted.length === qHead
     //@ invariant sorted.length <= nodeIds.length

tools/src/config.ts

@@ -130,13 +130,14 @@ function parseDirectiveValue(key: keyof OptionSpecs, text: string, source: strin
 }
 
 /**
- * Find comment lines, marking those that occur before any code.
+ * Find comment lines and the comment on each, marking those that occur before
+ * any code.
  *
  * Use the parsed syntax tree to skip strings, regexes, and template text.
  * Without those boundaries, the scanner can read /[/*]/ as a block comment
  * or treat a template's closing backtick as the start of another template.
  */
-function* fileCommentLines(sourceText: string): Generator<{ text: string; index: number; inLeadingRegion: boolean }> {
+export function* fileCommentLines(sourceText: string): Generator<{ text: string; comment: string; index: number; inLeadingRegion: boolean }> {
   // Normalize once so a leading BOM also works before a shebang.
   sourceText = sourceText.replace(/^\uFEFF/, "");
   const lines = sourceText.split(/\r\n|[\n\r\u2028\u2029]/);
@@ -163,8 +164,9 @@ function* fileCommentLines(sourceText: string): Generator<{ text: string; index:
     if (token === ts.SyntaxKind.SingleLineCommentTrivia || token === ts.SyntaxKind.MultiLineCommentTrivia) {
       const firstLine = sourceFile.getLineAndCharacterOfPosition(scanner.getTokenStart()).line;
       const lastLine = sourceFile.getLineAndCharacterOfPosition(scanner.getTokenEnd() - 1).line;
+      const comment = scanner.getTokenText();
       for (let index = firstLine; index <= lastLine; index++) {
-        yield { text: lines[index], index, inLeadingRegion };
+        yield { text: lines[index], comment, index, inLeadingRegion };
       }
     } else if (token !== ts.SyntaxKind.WhitespaceTrivia && token !== ts.SyntaxKind.NewLineTrivia &&
                token !== ts.SyntaxKind.ShebangTrivia) {
@@ -175,6 +177,22 @@ function* fileCommentLines(sourceText: string): Generator<{ text: string; index:
   }
 }
 
+const OPTION_DIRECTIVE = /^[ \t]*\/\/@[ \t]+option(?:[ \t]+(.*?))?[ \t]*$/;
+const ALIAS_DIRECTIVE = /^[ \t]*\/\/@[ \t]+([A-Za-z][A-Za-z0-9-]*)[ \t]*$/;
+
+/** The option a legacy alias such as `//@ safe-slice` sets, if `line` is one. */
+function aliasedOption(line: string): keyof OptionSpecs | undefined {
+  const alias = line.match(ALIAS_DIRECTIVE)?.[1];
+  if (alias === undefined) return undefined;
+  return KNOWN_KEYS.find(key => "directiveAliases" in OPTION_SPECS[key] &&
+    (OPTION_SPECS[key].directiveAliases as readonly string[]).includes(alias));
+}
+
+/** Whether `parseFileOptions` reads `line` as an option directive or a legacy alias. */
+export function isOptionDirective(line: string): boolean {
+  return OPTION_DIRECTIVE.test(line) || aliasedOption(line) !== undefined;
+}
+
 /** Parse top-of-file `//@ option key value` directives and legacy aliases. */
 export function parseFileOptions(sourceText: string, source: string): ExplicitOptions {
   const seen = new Map<keyof OptionSpecs, number>();
@@ -191,7 +209,7 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp
 
   const parseLine = (lineText: string, index: number, inLeadingRegion: boolean): void => {
     const line = index + 1;
-    const optionMatch = lineText.match(/^[ \t]*\/\/@[ \t]+option(?:[ \t]+(.*?))?[ \t]*$/);
+    const optionMatch = lineText.match(OPTION_DIRECTIVE);
     if (optionMatch) {
       if (!inLeadingRegion) fail(`${source}:${line}`, "//@ option directives must appear before the first source statement");
       const parts = (optionMatch[1] ?? "").trim().split(/\s+/).filter(Boolean);
@@ -206,19 +224,10 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp
       return;
     }
 
-    const aliasMatch = lineText.match(/^[ \t]*\/\/@[ \t]+([A-Za-z][A-Za-z0-9-]*)[ \t]*$/);
-    if (!aliasMatch) return;
-    const alias = aliasMatch[1];
-    for (const key of KNOWN_KEYS) {
-      const aliases = "directiveAliases" in OPTION_SPECS[key]
-        ? OPTION_SPECS[key].directiveAliases as readonly string[]
-        : [];
-      if (!aliases.includes(alias)) continue;
-      // Legacy aliases retain their pre-config placement behavior. New generic
-      // option directives are deliberately restricted to the file preamble.
-      setOption(key, true as LscOptions[typeof key], line);
-      return;
-    }
+    // Legacy aliases retain their pre-config placement behavior. New generic
+    // option directives are deliberately restricted to the file preamble.
+    const key = aliasedOption(lineText);
+    if (key) setOption(key, true as LscOptions[typeof key], line);
   };
 
   for (const { text, index, inLeadingRegion } of fileCommentLines(sourceText)) {

tools/src/extract.ts

@@ -11,7 +11,7 @@ import { initTypeParser } from "./types.js";
 import type { RawExpr, RawStmt, RawFunction, RawModule, RawClass, RawConst, RawGhostLet, RawGhostAssign } from "./rawir.js";
 import { normalizeBigIntLiteral } from "./rawir.js";
 import { setUserNames, freshName } from "./names.js";
-import { DEFAULT_OPTIONS, type LscOptions } from "./config.js";
+import { DEFAULT_OPTIONS, fileCommentLines, isOptionDirective, type LscOptions } from "./config.js";
 
 // ── Expression extraction ────────────────────────────────────
 
@@ -737,24 +737,82 @@ function extractExpr(node: Expression): RawExpr {
 
 const PREFIX = "//@ ";
 const KEYWORDS = ["requires", "ensures", "contract", "invariant", "decreases", "done_with", "type"] as const;
+/** The other directives (SPEC §2.1) besides options, read by keyword elsewhere. */
+const DIRECTIVES = ["verify", "pure", "impure", "skip", "extern", "havoc", "autohavoc", "assert", "assume",
+  "ghost", "declare-type", "backend", "lean-module"];
 export type AnnotKind = (typeof KEYWORDS)[number];
-interface Annotation { kind: AnnotKind; expr: string }
+/** `line` is set only for annotations in the file being extracted. */
+interface Annotation { kind: AnnotKind; expr: string; line?: number }
+
+function parseAnnotation(text: string): Annotation | null {
+  if (!text.startsWith(PREFIX)) return null;
+  const content = text.slice(PREFIX.length);
+  const sp = content.indexOf(" ");
+  if (sp === -1) return null;
+  const kw = content.slice(0, sp);
+  if (!(KEYWORDS as readonly string[]).includes(kw)) return null;
+  return { kind: kw as AnnotKind, expr: content.slice(sp + 1).trim() };
+}
 
 function parseAnnotations(node: Node): Annotation[] {
   const result: Annotation[] = [];
   for (const range of node.getLeadingCommentRanges()) {
-    const text = range.getText().trim();
-    if (!text.startsWith(PREFIX)) continue;
-    const content = text.slice(PREFIX.length);
-    const sp = content.indexOf(" ");
-    if (sp === -1) continue;
-    const kw = content.slice(0, sp);
-    if (!(KEYWORDS as readonly string[]).includes(kw)) continue;
-    result.push({ kind: kw as AnnotKind, expr: content.slice(sp + 1).trim() });
+    const a = parseAnnotation(range.getText().trim());
+    if (!a) continue;
+    a.line = currentFileLine(node, range.getPos());
+    result.push(a);
   }
   return result;
 }
 
+/** The line of `pos` in `node`'s file, when that is the file being extracted. */
+function currentFileLine(node: Node, pos: number): number | undefined {
+  const sourceFile = node.getSourceFile();
+  return sourceFile === _currentSourceFile ? sourceFile.getLineAndColumnAtPos(pos).line : undefined;
+}
+
+/** Lines of the annotations whose value reached the Raw IR. */
+const _readLines = new Set<number>();
+/** Line spans the extractor leaves out on purpose: `//@ skip`, unselected and extern functions. */
+const _skippedSpans: [number, number][] = [];
+
+/** The annotation's expression, recording that it was read. */
+function readExpr(a: Annotation): string {
+  if (a.line !== undefined) _readLines.add(a.line);
+  return a.expr;
+}
+function annotExprs(annots: Annotation[], kind: AnnotKind): string[] {
+  return annots.filter(a => a.kind === kind).map(readExpr);
+}
+/** Only the first is read; a repeated one is reported as unread. */
+function firstAnnotExpr(annots: Annotation[], kind: AnnotKind): string | null {
+  const a = annots.find(a => a.kind === kind);
+  return a ? readExpr(a) : null;
+}
+function skipSpan(node: Node): void {
+  const first = node.getLeadingCommentRanges()[0];
+  const from = first ? node.getSourceFile().getLineAndColumnAtPos(first.getPos()).line : node.getStartLineNumber();
+  _skippedSpans.push([from, node.getEndLineNumber()]);
+}
+
+/** Fail on `//@` comments lsc ignores: a malformed or unknown one, or a
+ *  contract annotation where no reader looks. Other directives are checked
+ *  by keyword only. TypeScript's `//@ts-…` comments are not ours. */
+function checkAnnotationsRead(sourceFile: SourceFile): void {
+  const errors: string[] = [];
+  for (const { comment, index } of fileCommentLines(sourceFile.getFullText())) {
+    const text = comment.trim();
+    if (!text.startsWith("//@") || text.startsWith("//@ts-")) continue;
+    const line = index + 1;
+    const keyword = text.match(/^\/\/@ (\S+)(?: |$)/)?.[1];
+    const read = parseAnnotation(text)
+      ? _readLines.has(line) || _skippedSpans.some(([from, to]) => from <= line && line <= to)
+      : DIRECTIVES.includes(keyword ?? "") || isOptionDirective(text);
+    if (!read) errors.push(`${sourceFile.getBaseName()}:${line}: lsc does not read this annotation: ${text}`);
+  }
+  if (errors.length > 0) throw new Error(errors.join("\n"));
+}
+
 function collectAnnotations(node: Node, body?: Node[]): Annotation[] {
   const own = parseAnnotations(node);
   if (body && body.length > 0) return [...own, ...parseAnnotations(body[0])];
@@ -881,8 +939,8 @@ function extractTypeDecl(decl: TypeAliasDeclaration, extraDecls?: TypeDeclInfo[]
   // Leading `//@ type <ty>` overrides extraction — the declared TS type is
   // replaced by the annotated backend type. Used to coerce literal unions
   // (`5 | 15 | 30` → `nat`) and other types LS can't model precisely.
-  const override = parseAnnotations(decl).find(a => a.kind === "type");
-  if (override) return { name, typeParams: tpField, kind: "alias", aliasOf: override.expr };
+  const override = firstAnnotExpr(parseAnnotations(decl), "type");
+  if (override) return { name, typeParams: tpField, kind: "alias", aliasOf: override };
 
   if (type.isUnion()) {
     const members = type.getUnionTypes();
@@ -979,7 +1037,9 @@ function extractInterface(decl: InterfaceDeclaration, extraDecls?: TypeDeclInfo[
     if (Node.isPropertySignature(member)) {
       const text = member.getTrailingCommentRanges().map(r => r.getText()).join(" ");
       const match = text.match(/\/\/@ type (\w+)/);
-      if (match) overrides.set(member.getName(), match[1]);
+      if (match) {
+        overrides.set(member.getName(), readExpr({ kind: "type", expr: match[1], line: currentFileLine(member, member.getEnd()) }));
+      }
     }
   }
   return extractRecord(decl.getName(), decl.getType(), decl, overrides, extraDecls);
@@ -1400,6 +1460,7 @@ function extractStmts(stmts: Node[]): RawStmt[] {
 
     // //@ skip — omit this statement from the verification model
     if (leadingComments.some(r => r.getText().trim() === "//@ skip")) {
+      skipSpan(s);
       continue;
     }
 
@@ -1606,9 +1667,9 @@ function extractStmts(stmts: Node[]): RawStmt[] {
       result.push({
         kind: "while",
         cond: extractExpr(s.getExpression()),
-        invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr),
-        decreases: annots.find(a => a.kind === "decreases")?.expr ?? null,
-        doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null,
+        invariants: annotExprs(annots, "invariant"),
+        decreases: firstAnnotExpr(annots, "decreases"),
+        doneWith: firstAnnotExpr(annots, "done_with"),
         body: extractStmts(bodyStmts),
         line,
       });
@@ -1656,8 +1717,8 @@ function extractStmts(stmts: Node[]): RawStmt[] {
         kind: "forof",
         names,
         iterable: extractExpr(iterableExpr),
-        invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr),
-        doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null,
+        invariants: annotExprs(annots, "invariant"),
+        doneWith: firstAnnotExpr(annots, "done_with"),
         body: extractStmts(bodyStmts),
         line,
       });
@@ -1717,9 +1778,9 @@ function extractStmts(stmts: Node[]): RawStmt[] {
       }
 
       let condExpr: RawExpr = cond ? extractExpr(cond) : { kind: "bool", value: true };
-      let invariants = annots.filter(a => a.kind === "invariant").map(a => a.expr);
-      let decreases = annots.find(a => a.kind === "decreases")?.expr ?? null;
-      let doneWith = annots.find(a => a.kind === "done_with")?.expr ?? null;
+      let invariants = annotExprs(annots, "invariant");
+      let decreases = firstAnnotExpr(annots, "decreases");
+      let doneWith = firstAnnotExpr(annots, "done_with");
       for (const [from, to] of renames) {
         for (let k = 0; k < hoisted.length; k++) hoisted[k] = renameRawStmt(hoisted[k], from, to);
         condExpr = renameRawExpr(condExpr, from, to);
@@ -1756,8 +1817,8 @@ function extractStmts(stmts: Node[]): RawStmt[] {
         kind: "forof",
         names: [name],
         iterable: extractExpr(s.getExpression()),
-        invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr),
-        doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null,
+        invariants: annotExprs(annots, "invariant"),
+        doneWith: firstAnnotExpr(annots, "done_with"),
         body: extractStmts(bodyStmts),
         line,
       });
@@ -1976,7 +2037,9 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot
   for (const a of annots) {
     if (a.kind === "type") {
       const parts = a.expr.split(/\s+/);
-      if (parts.length === 2) typeAnnotations.push({ name: parts[0], type: parts[1] });
+      if (parts.length !== 2) continue;
+      readExpr(a);
+      typeAnnotations.push({ name: parts[0], type: parts[1] });
     }
   }
 
@@ -2065,10 +2128,10 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot
       if (inferred.isAny()) return "unknown";
       return _eraseGenerics(typeToString(inferred));
     })(),
-    requires: annots.filter(a => a.kind === "requires").map(a => a.expr),
-    ensures: annots.filter(a => a.kind === "ensures").map(a => a.expr),
-    contract: annots.filter(a => a.kind === "contract").map(a => a.expr),
-    decreases: annots.find(a => a.kind === "decreases")?.expr ?? null,
+    requires: annotExprs(annots, "requires"),
+    ensures: annotExprs(annots, "ensures"),
+    contract: annotExprs(annots, "contract"),
+    decreases: firstAnnotExpr(annots, "decreases"),
     pure: hasPureAnnotation(fn, body && Node.isBlock(body) ? body.getStatements() as Node[] : undefined),
     autohavoc: false,  // set in extractModule (file-level directive or per-function)
     typeAnnotations,
@@ -2094,6 +2157,8 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA
   // here), deduped by qualified name.
   _externs.clear();
   _externSigTypes.length = 0;
+  _readLines.clear();
+  _skippedSpans.length = 0;
 
   // Match a `//@ <kw>` directive only as the first non-whitespace on a line,
   // so prose mentioning an annotation does not activate it.
@@ -2204,7 +2269,7 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA
   const constants: RawConst[] = [];
   for (const stmt of sourceFile.getStatements()) {
     if (Node.isVariableStatement(stmt)) {
-      if (hasLeadingDirective(stmt, "skip")) continue;
+      if (hasLeadingDirective(stmt, "skip")) { skipSpan(stmt); continue; }
       for (const decl of stmt.getDeclarationList().getDeclarations()) {
         if (stmt.getDeclarationList().getFlags() & 2 /* const */) {
           const init = decl.getInitializer();
@@ -2361,6 +2426,12 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA
   );
   const hasVerifyDirective = nonExternFns.some(hasVerify) || hasVerifiedClassMethod;
   const fnsToExtract = hasVerifyDirective ? nonExternFns.filter(hasVerify) : nonExternFns;
+  // A statement holding a selected function keeps its comments checked.
+  for (const f of allFns) {
+    if (fnsToExtract.includes(f)) continue;
+    const wholeStmt = f.parentStmt && !fnsToExtract.some(s => s.parentStmt === f.parentStmt);
+    skipSpan(wholeStmt ? f.parentStmt! : f.node);
+  }
 
   // `//@ autohavoc` — enable the auto-havoc abstraction (see autohavoc.ts).
   // File-level: a directive at column 0 (top of file) enables it for every
@@ -2739,11 +2810,11 @@ 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;
+    if (hasLeadingDirective(cls, "skip")) { skipSpan(cls); continue; }
     const methods: RawFunction[] = [];
     for (const method of cls.getMethods()) {
-      if (hasLeadingDirective(method, "skip")) continue;
-      if (!method.getFullText().includes('//@ verify')) continue;
+      if (hasLeadingDirective(method, "skip")) { skipSpan(method); continue; }
+      if (!method.getFullText().includes('//@ verify')) { skipSpan(method); continue; }
       methods.push(extractFunction(method as any));
     }
     if (methods.length === 0) continue;
@@ -2758,6 +2829,8 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA
   // union stringification outside of an extractModule call.
   _synthArrayUnions = null;
 
+  checkAnnotationsRead(sourceFile);
+
   return {
     file: sourceFile.getFilePath(),
     typeDecls,