Description
In ProbeLean/Verify.lean, the sorryInDeclaration function returns false when an atom has codeText = none (no line range information):
match atom.codeText with
| none => false
| some range => warning.line >= range.linesStart && warning.line <= range.linesEnd
This means any declaration where the analysis couldn't extract line numbers will never have sorries attributed to it, and will always appear as "verified" -- even if it actually contains sorry.
Impact
False "verified" verdicts for atoms without line-range information. This is a soundness issue.
Suggested Fix
When codeText is none and the file path matches, consider returning true (conservatively assume the sorry belongs to this atom), or at minimum flag the atom as "unknown" verification status rather than "verified".
Description
In
ProbeLean/Verify.lean, thesorryInDeclarationfunction returnsfalsewhen an atom hascodeText = none(no line range information):This means any declaration where the analysis couldn't extract line numbers will never have sorries attributed to it, and will always appear as "verified" -- even if it actually contains
sorry.Impact
False "verified" verdicts for atoms without line-range information. This is a soundness issue.
Suggested Fix
When
codeTextisnoneand the file path matches, consider returningtrue(conservatively assume the sorry belongs to this atom), or at minimum flag the atom as "unknown" verification status rather than "verified".