Proof backend and concrete evaluation disagree about integer division

[brianhuffman]

Cryptol> let p x y = y != (0:Integer) ==> x / -y == -x / y
Cryptol> :check p
Using random testing.
Passed 100 tests.
Cryptol> :prove p
p 3 -2 = False
(Total Elapsed Time: 0.029s, using Z3)
Cryptol> p 3 (-2)
True

[LeventErkok]

Curious how you translate this. With SBV, I'm getting:

Prelude Data.SBV> prove $ \x y -> y ./= 0 .=> x `sDiv` (-y) .== (-x) `sDiv` (y::SInteger)
Unknown.
  Reason: smt tactic failed to show goal to be sat/unsat (incomplete (theory arithmetic))

[brianhuffman]

Here's the output using :set prover=offline:

; Automatically created by SBV on 2019-11-24 12:55:52.399205 PST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic ALL) ; has unbounded values, using catch-all.
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
(define-fun s2 () Int 0)
; --- skolem constants ---
(declare-fun s0 () Int)
(declare-fun s1 () Int)
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s3 () Bool (distinct s1 s2))
(define-fun s4 () Int (- s1))
(define-fun s5 () Int (div s0 s4))
(define-fun s6 () Int (- s0))
(define-fun s7 () Int (div s6 s1))
(define-fun s8 () Bool (= s5 s7))
(define-fun s9 () Bool (not s3))
(define-fun s10 () Bool (or s8 s9))
(assert (not s10))
(check-sat)

z3 version 4.8.6 returns "sat" on this input file.

[brianhuffman]

Perhaps the Data.SBV.Dynamic interface is giving us the raw SMTLib div operation, while Data.SBV.sDiv is a wrapper that simulates the behavior of Haskell's div or quot? (As I recall, the SMTLib div matches neither of Haskell's integer division operators.)

[LeventErkok]

@brianhuffman When I feed that script to z3, it tells me unknown. I'm using z3 compiled from github sources on Nov 16th.

You're correct, however, that the Data.SBV.Dynamic directly goes through SMTLib's version of division; which would be the wrong thing to do. We probably need to move that translation to the dynamic interface. At least let's register this as an issue in the tracker to avoid confusion.

[LeventErkok]

Captured here: https://github.com/LeventErkok/sbv/issues/495

[robdockins]

We still need to decide what the Cryptol semantics of (/) on integers should be to properly close this issue. The current help text indicates that this operation "rounds down". If we take that literally, it indicates we should take a "round toward negative infinity" definition, which is what the concrete interpreter is currently doing, I believe.

I'm inclined to take that approach, which represents the minimal change. However, it's worth asking if there are any good reasons to instead adopt the round-to-zero or SMTLib euclidean division operations instead?

[robdockins]

For discussion and potential test-case purposes, here is a Cryptol file that specifies some properties that "round to negative infinity" division enjoys; I believe these properties uniquely specify the exact operation.

In my what4 branch (where I've applied the translation discussed in #687) both :check and :prove (using CVC4) validate these properties.

// Invariant: denominator is strictly positive
type Q = (Integer, Integer)

toQ : Integer -> Integer -> Q
toQ n d =
  if d == 0 then error "zero denominator" else
  if d < 0 then (negate n, negate d) else (n, d)

eqQ : Q -> Q -> Bit
eqQ (a,b) (c,d) = a*d == b*c

// Note, relies on the fact that b > 0 and d > 0
ltQ : Q -> Q -> Bit
ltQ (a,b) (c,d) = a*d < b*c

// Note, relies on the fact that b > 0 and d > 0
leQ : Q -> Q -> Bit
leQ (a,b) (c,d) = a*d <= b*c

abs : Integer -> Integer
abs x = if x >= 0 then x else negate x

property divRoundsDown (x : Integer) (y : Integer) =
  y == 0 \/ leQ (toQ (x / y) 1) (toQ x y)

property modAbs (x : Integer) (y : Integer) =
  y == 0 \/ abs (x % y) < abs y

property modSign (x : Integer) (y : Integer) =
  y == 0 \/ ( (negate x % y) == negate (x % negate y) )

property divModEuclidean (x : Integer) (y : Integer) =
  y == 0 \/ (y * (x / y) + x % y == x)

[LeventErkok]

@robdockins Would be really cool to fix the corresponding SBV issue as well. (https://github.com/LeventErkok/sbv/issues/495). A pull request would be really nice. (Not sure if your Cryptol fix directly carries over there though, but shouldn't be too hard to handle I think.)

[robdockins]

@LeventErkok what's your preferred outcome for that bug?

[LeventErkok]

@robdockins Assuming Cryptol and Haskell's semantics of division is the same (and if not, why are they not?), then a good outcome would be you'd fix this directly in SBV and not change the existing Cryptol code at all (i.e., rollback your commit) and it'd just work. Hope that makes sense!

[robdockins]

To answer the direct question, I think we're agreed that Cryptol's division operation on Integers should be flooring division that matches Haskell's quotRem semantics.

As to SBV, I took a minute to look into it. The svQuot operation from Data.SBV.Dynamic is the overloaded operation on SVal that operates over all the numeric types. It directly exposes the operation available from the underlying solvers (properly, in my opinion). It's worth noting that the documentation on svQuot and svRem is quite explicit about which operations on bounded and unbounded integers you will get. I don't think we want to change the semantics of this operation.

So, we can rename svQuot and svRem as we pass them through the Dynamic interface (svQuotRaw or somesuch?), and provide svQuot, svRem, svDiv, svMod operations that are restricted to KUnbounded values and that match Haskell's integer operations... but I'm not really sure that's worth taking the trouble.

[robdockins]

Minor correction: the Haskell operation providing the flooring operation is actually divMod, sorry.

[LeventErkok]

Ah, good point. I've forgotten that this was "documented" behavior. Though rather surprising.

I guess the preferred solution would be to make svQuot and svRem in the dynamic interface match exactly what Haskell does. Bottom line, whether you're using the regular or dynamic interface, you should always get Haskell semantics with SBV. In other words, change the documented behavior from what it is currently.

Whether the current behavior should be preserved using some new names is an interesting question. I suppose it doesn't hurt, but really Cryptol is the only "customer" of the dynamic interface. If you guys don't need it, I suppose there's no point in providing them. But also would be nice to have them around just in case. So perhaps provide those versions with suffix _SMTLib?