Repository navigation
Conversation
A //@ comment that lsc didn't read was dropped without a word, so a false postcondition that was misspelled or misplaced passed with "0 verified, 0 errors" (midspiral#238). Extraction now records where each contract annotation's value is used and ends with one check over the file's comments: a malformed or unknown //@ comment, or a contract annotation that nothing used, is an error naming the file, line and text. Declarations left out on purpose (unselected, extern or skip) are exempt from the placement check, and TypeScript's //@ts- comments are left alone. Option lines are recognized by config's own grammar. Four example lines that were never read are removed; the generated Dafny and Lean files are unchanged.
|
CI as expected: the four
|
namin
left a comment
namin
left a comment
There was a problem hiding this comment.
This is great. Cool that it found some ignored annotations in the case studies too!
| 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}`); |
There was a problem hiding this comment.
I'd prefer the relative file path than just the base
| : 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")); |
There was a problem hiding this comment.
now that we've updated the case studies, should we make this a warning? or else there should be a flag to make it a warning. i am concerned that some code bases might have further conventions for //@
Problem
A
//@comment thatlscdoesn't read is dropped without a word (#238). When it states a postcondition, a false contract passes:lsc checkexits 0 with0 verified, 0 errors. It happens when the line is malformed (//@ensures, extra spaces, a tab, no expression, a misspelled keyword) and when a well-formed annotation sits where no reader looks (above an arrow with a block body, after an unrelated statement, arequiresinside a loop body).Fix
lscnow fails on a//@comment it ignores, as discussed in the issue, with the limits under "Not covered":requires,ensures,contract,invariant,decreases,done_with,type) are recorded where their value is used, not where they are parsed, so an annotation that is parsed and then dropped also counts as unread: a block-body arrow's parent annotations, a loop'srequires, a seconddecreases. Two helpers,annotExprsandfirstAnnotExpr, replace thefilter(...).map(a => a.expr)lines at those sites and record the read.//@comment in the file must be a contract annotation that was read, or one of the other directives in SPEC §2.1 followed by a space or the end of the line. Option lines are recognized byconfig.ts's own grammar through a newisOptionDirective, so//@ option …and//@<tab>safe-slicekeep working.lscleaves out on purpose (functions outside the//@ verifyselection,externfunctions,skipped statements, consts, classes and methods) are not checked for placement, so a contract in an unselected function stays fine; a typo there, like//@verify, is still caught. TypeScript's//@ts-…comments are not ours.The check runs at the end of
extractModuleand reusesfileCommentLinesfromconfig.ts, which now also yields each comment's text. All failures are collected into one error, so softening it to a warning is a change in one place. SPEC §2.1 gets one paragraph describing the rule.Not covered
Directives other than contract annotations are checked by keyword only. A correctly spelled bare directive in a place nothing reads (
//@ pureabove a statement), or one with extra text (//@ pure extra), still passes. Covering those would mean every reader recording what it matched, which could be a follow-up. The list of directive keywords next toKEYWORDShas to be kept in step with the readers.Reading annotations above an arrow with a block body, as for an expression body, would change behavior, so it isn't part of this PR. That case is now an error instead of a silent pass.
What breaks
The check found annotations that were already being ignored. In this repository, four example lines:
//@ type i natand//@ type j natinside loop bodies innullableArray.ts,//@ type qHead natintoposort.ts, and//@ type Twith no type inreadonlyArray.ts. They are removed; the generated.dfy.gen,.dfyand Lean files are byte-identical.I ran
lsc extracton the 82LemmaScript-files.txtentries of the 30case-studies-dafnymatrix entries, each cloned at the branchci.ymluses. Onf245e98none fails. With this change four files do, and in each the generated Dafny confirms the annotation is ignored today:xyflow-lemmascript(lemmascript)packages/system/src/utils/general.ts//@ ensures \result >= 0aboveexport const getOverlappingArea = (…) => { … }getOverlappingArea_ensureslemma is generated; the postcondition is never checkedgithub-star-checker-lemmascriptsrc/domain.ts//@ type idx natand//@ type i natin loop bodiesvar idx := 0;rallly-lemmascript(lemmascript)apps/web/src/features/poll/scoring.ts//@ type i natin a loop bodyvar i := 0;collab-todo-lemmascriptsrc/domain.ts//@ __mapFromArrayThe
case-studies-dafnyjobs for these four will fail on this PR until those lines are fixed. I can open the case-study changes with the staging branchesci.ymldescribes.//@ typeinside a loop body shows up in three examples and two case studies, so people seem to expect it to work there. Should loops read it? That would be a separate change.Regression
tools/tests/unread-annotations.test.ts: twelve unread forms and placements fail extraction with their line, including the brownfield//@verifytypo and two arrows sharing oneconststatement; seven controls still extract, two of them asserting the contract arrives. Onf245e98the twelve fail and the seven pass.Validation
On Ubuntu 24.04 (WSL), Node 24.15, Dafny 4.11.0, against
f245e98:npm run typecheck,(cd tools && npm run typecheck)andnpm run typecheck:examples: pass.tools/test-fixtures.sh: pass. The unit suite is 333 passed, 0 failed (314 onf245e98, plus the 19 new tests)../regen-dafny.sh --no-verifyand./regen-lean.sh: pass, no generated-file drift.lsc check --backend=dafnyon all 72examples/*.ts: 0 failures.lake build. The Lean inputs are byte-identical tof245e98, whose CI passed.Compatibility
No new option, syntax or dependency. A file whose
//@comments are all read extracts exactly as before. A file with an ignored one now fails instead of passing silently, which is the point of the change.Closes #238.