Issue 336: Underflow not detected for range length field

[senier]

This fixes cases where negative fields length were not detected. The reason was a misconception of what we (need to) proof here. The attempted proof we had in the code so far was something like (H1 and H2 being the constraints from the range type):

H1: Length >= 40
H2: Length <= 1500
GOAL: Length - 50 >= 0

We then checked whether a solution could be found:

if proof.result != ProofResult.sat:
   ... # Error

What this does is checking whether one solution exists for the goal, which is clearly the case for Length >= 50. What we actually want and what is implemented now is proving that Length - 50 < 0 is unsatisfiable.

Why wouldn't our tests detect this issue? The error message for a different check (that the start of the field is non-negative) was apparently copied from the length check, but not changed. In addition to the length issue, the test case also had a negative start which triggered that second erroneous error message. As it looked as expected, the ineffectiveness of the length check remained unnoticed. The non-negative test was apparently also copied and checked for the wrong message. Hence, the invalid message remained unnoticed.

Lessons learned:

1. Don't copy and paste tests (without careful review)
2. Don't copy and paste checks (without careful review)
3. Proofs show that "there exists one solution" for your formula - if you want to show that a formula never is true, show that its negation is unsatisfiable
4. We need to review the other checks we do regarding 3.

Other changes:

Since upgrading to isort 4.3.21 via pip3 on Debian, third-party packages are not detected anymore. As a result, isort erroneously removes a lot of whitespace. I added our third-party libs to the isort config, which solves the issue for now and also is more robust if a dependency is not installed.

Close #336

[codecov]

Codecov Report

Merging #337 into develop will not change coverage.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop     #337   +/-   ##
========================================
  Coverage    97.95%   97.95%           
========================================
  Files           25       25           
  Lines         4447     4447           
  Branches       746      745    -1     
========================================
  Hits          4356     4356           
  Misses          54       54           
  Partials        37       37           

Impacted Files	Coverage Δ
rflx/model.py	99.74% <100.00%> (ø)

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b5e031f...9fe9ffb. Read the comment docs.