Iron: The Not implication rule encodes the inverse, so refined Int values can break bounds
Fixed · high · Soundness bug
The Not[C1] implies Not[C2] rule encodes the inverse instead of the contrapositive, so a value that is at most 5 passes as at most 3. The compiler accepts an invalid refinement, and the value breaks the bound at runtime.
Found: ; reported: ; status since: . Reporter: Mike Murunov
Page for this report · Public report · Fix or proposed fix (see status)
Of course I'm accepting PRs 👍