pyspec: add --reject-approximations CLI flag#1208
Conversation
Strict mode for the Python frontend. Sites that silently lower unsupported constructs to a Hole or drop a statement now raise `unsupportedConstruct` (exit 4). Off by default. Test: RejectApproximationsTest.lean.
julesmt
force-pushed
the
julesmt/features/reject-approximations
branch
from
a852801 to
e998c9d
Compare
|
@keyboardDrummer-bot Please resolve git conflicts. |
…ect-approximations # Conflicts: # Strata/Languages/Python/PySpecPipeline.lean # Strata/Languages/Python/Specs.lean # Strata/Languages/Python/Specs/ToLaurel.lean # Strata/SimpleAPI.lean # StrataMain.lean
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
Proof / #guard opportunities (none currently exist):
theorem rejectableHole_strict (c r) : (rejectableHole true c r).isOk = falseand the dual…false…isOk = true— trivialdecide-able lemmas (or#guards) that lock in the boolean dispatch.theorem rejectableHole_strict_message (c r) : ∃ msg ast, rejectableHole true c r = .error (.unsupportedConstruct msg ast) ∧ msg.startsWith "[approximation] "— pins the message prefix so downstream tooling that filters by[approximation]can rely on it.
Minor stylistic nits:
"silently dropped today"— the today inrejectableDrop's message is informal and dates the wording. Either drop it or replace with"by current translation".- The two helper messages and
Specs.lean'sspecWarningrewrite each have slightly different shapes (is approximated as Hole,is silently dropped today,[approximation] {message}). Once you have an end-to-end test from point 1, please consider unifying via a smallapproximationError : (kind : ApproxKind) → (construct : String) → Stringhelper.
| def mkInstanceMethodCall (className : String) (methodName : String) | ||
| For Any-typed receivers (no model available), returns a Hole under lax | ||
| mode, or raises `unsupportedConstruct` under `--reject-approximations`. -/ | ||
| def mkInstanceMethodCall (rejectApproximations : Bool) (className : String) (methodName : String) |
There was a problem hiding this comment.
After this PR, mkInstanceMethodCall is called from exactly two sites (the with-statement __enter__/__exit__ pair at lines 2059–2060), both of which pass ctx.rejectApproximations. Threading the bool explicitly is noise — please take the whole ctx : TranslationContext so the signature shrinks and future additions can read other fields too.
Also: the inline |>.map (fun h => { h with source := source }) in the Any branch is a workaround because rejectableHole ignores source. Cleaner to add a source : Option FileRange := none argument to rejectableHole itself and let it stamp the location in one place — the rejection error then carries the same source you already have, which makes the diagnostic much more useful under --reject-approximations.
| otherwise approximate an unsupported Python construct as a havoc'd | ||
| Hole. The `construct` argument names the surface form (e.g., | ||
| `"BinOp Div"`) for the error message. -/ | ||
| def rejectableHole (rejectApproximations : Bool) (construct astRepr : String) | ||
| : Except TranslationError StmtExprMd := | ||
| if rejectApproximations then | ||
| throw (.unsupportedConstruct | ||
| s!"[approximation] {construct} is approximated as Hole; not in the sound subset" | ||
| astRepr) | ||
| else | ||
| pure (mkStmtExprMd .Hole) | ||
|
|
||
| /-- Same as `rejectableHole` but for sites that silently drop a Python | ||
| statement (e.g., `raise`, `try…else`, `for…else`) under lax mode. | ||
| The error message names the dropped construct. -/ | ||
| def rejectableDrop (rejectApproximations : Bool) (construct astRepr : String) | ||
| : Except TranslationError Unit := | ||
| if rejectApproximations then | ||
| throw (.unsupportedConstruct | ||
| s!"[approximation] {construct} is silently dropped today; not in the sound subset" | ||
| astRepr) | ||
| else |
There was a problem hiding this comment.
Two callers pass (toString (repr e)) for astRepr. For deeply nested expressions this produces multi-kilobyte error strings — fine for unit tests, painful for users running on real specs. Consider taking (source : Option FileRange) instead and letting the diagnostic infrastructure render file:line:col plus a short construct name; the surface form is rarely useful when the location is known.
If you want to keep the AST repr as a fallback, capping it (astRepr.take 200 ++ "…") would prevent the worst cases without losing the unit-test guarantees.
| specError loc message := do | ||
| specErrorAt (←read).pythonFile loc message | ||
| specWarning loc message := do | ||
| let file := (←read).pythonFile | ||
| let w : PipelineMessage := { file, loc, phase := pySpecParsingPhase, kind := .pySpecParsingWarning, message } | ||
| modify fun s => { s with warnings := s.warnings.push w } | ||
| let ctx ← read | ||
| -- Under strict mode (`--reject-approximations`), every warning is an | ||
| -- error: the parser only emits warnings on patterns it falls back to | ||
| -- `.placeholder` for, which silently drops the user's spec. | ||
| if ctx.rejectApproximations then | ||
| specErrorAt ctx.pythonFile loc s!"[approximation] {message}" | ||
| else | ||
| let w : PipelineMessage := { file := ctx.pythonFile, loc, phase := pySpecParsingPhase, kind := .pySpecParsingWarning, message } |
There was a problem hiding this comment.
Same logical change as rejectableHole/rejectableDrop in PythonToLaurel.lean, but expressed differently (warning→error rewrite vs. helper-with-throw). With rejectApproximations now in both TranslationContext and PySpecContext, please factor the message format into a single helper module (e.g. Strata/Languages/Python/Approximation.lean) so the prefix [approximation] is only typed once and the three current call shapes can't drift.
No regression test currently fires this specError arm — please add one alongside the existing Specs/... tests so the warning-to-error promotion is exercised.
The strict-mode error helpers used to dump the full Python AST `repr` into every diagnostic, producing multi-kilobyte messages on real specs. Take an `Option FileRange` instead and render `file:offset` when one is available; cap the AST string fallback at 200 chars. Also stamp the returned `Hole` with the source so callers don't have to. Reword `"silently dropped today"` → `"silently dropped by current translation"` so the message doesn't read as date-dependent.
`mkInstanceMethodCall` took a single `rejectApproximations : Bool` parameter; both call sites just forwarded `ctx.rejectApproximations`. Take the whole context so future fields don't each grow a new bool parameter.
Three places currently spell out the `[approximation] ` prefix and the strict-mode wording inline: `rejectableHole`, `rejectableDrop`, and the `specWarning` warning→error promotion in `Specs.lean`. They were already drifting. Add a small `Strata.Languages.Python.Approximation` module with a `Kind` (`hole | drop | warningPromotion`), a single `prefixTag`, and a `render` function. All three sites now route through it. New sites won't need to retype the prefix.
Add four `rfl`-provable lemmas that pin the strict/lax branch of `rejectableHole` and `rejectableDrop`, plus existence lemmas pinning the strict-mode message to `Approximation.render`. A future refactor that flips a branch or drifts the prefix won't compile.
|
@tautschnig All of the items you've listed appear to already be addressed in the current state of the PR:
Is there anything else you'd like changed here, or can these review threads be resolved? |
3 participants
Adds
--reject-approximations. Today some constructs silently lower to aHoleor.placeholder, so the verifier can reportAnalysis successon code whose contract was dropped. The flag turns those sites into hard errors. Off by default.