:prove command generating wrong smtlib output for right-shift operators

[brianhuffman]

Cryptol has both unsigned (>>) and signed (>>$) right-shift operators. They are different, and we can prove that:

Cryptol> :prove \(x:[8]) -> (x >>$ 0x4) == (x >> 0x4)
(\(x : [8]) -> (x >>$ 0x4) == (x >> 0x4)) 0x80 = False
(Total Elapsed Time: 0.008s, using Z3)

Now, if we tweak this predicate slightly by adding a drop`{0} (which is an identity function), then :exhaust can still find a counterexample, but :prove now says QED!

Cryptol> :exhaust \(x:[8]) -> (x >>$ 0x4) == (drop`{0} x >> 0x4)
Using exhaustive testing.
(\(x : [8]) -> (x >>$ 0x4) == (drop`{0} x >> 0x4)) 0x80 = False
Cryptol> :prove \(x:[8]) -> (x >>$ 0x4) == (drop`{0} x >> 0x4)
Q.E.D.
(Total Elapsed Time: 0.006s, using Z3)

Setting the :prover to offline sheds some light on the situation. With the original predicate, the smtlib output mentions both bvashr (arithmetic, i.e. signed shift right) and bvlshr (logical, i.e. unsigned shift right).

Cryptol> :set prover=offline
Cryptol> :prove \(x:[8]) -> (x >>$ 0x4) == (x >> 0x4)
Writing to SMT-Lib file standard output...
To determine the validity of the expression, use an external SMT solver.
; Automatically created by SBV on 2019-01-31 14:26:56.589387 PST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- literal constants ---
(define-fun s5 () (_ BitVec 4) #x4)
(define-fun s2 () (_ BitVec 8) #x04)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 8))
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s1 () (_ BitVec 8) ((_ extract 7 0) s0))
(define-fun s3 () (_ BitVec 8) (bvashr s1 s2))
(define-fun s4 () (_ BitVec 8) ((_ extract 7 0) s3))
(define-fun s6 () (_ BitVec 8) ((_ zero_extend 4) s5))
(define-fun s7 () (_ BitVec 8) (bvlshr s0 s6))
(define-fun s8 () Bool (= s4 s7))
(assert (not s8))
(check-sat)

But when we add the drop back in, now both shift operators are the signed bvashr version!

Cryptol> :prove \(x:[8]) -> (x >>$ 0x4) == (drop`{0} x >> 0x4)
Writing to SMT-Lib file standard output...
To determine the validity of the expression, use an external SMT solver.
; Automatically created by SBV on 2019-01-31 14:27:00.012554 PST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- literal constants ---
(define-fun s5 () (_ BitVec 4) #x4)
(define-fun s2 () (_ BitVec 8) #x04)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 8))
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s1 () (_ BitVec 8) ((_ extract 7 0) s0))
(define-fun s3 () (_ BitVec 8) (bvashr s1 s2))
(define-fun s4 () (_ BitVec 8) ((_ extract 7 0) s3))
(define-fun s6 () (_ BitVec 8) ((_ zero_extend 4) s5))
(define-fun s7 () (_ BitVec 8) (bvashr s1 s6))
(define-fun s8 () Bool (= s4 s7))
(assert (not s8))
(check-sat)

Putting a drop in a different place causes the smtlib output to have bvlshr in both places:

Cryptol> :prove \(x:[8]) -> (x == drop`{0} x) ==> (x >>$ 0x4) == (x >> 0x4)
Writing to SMT-Lib file standard output...
To determine the validity of the expression, use an external SMT solver.
; Automatically created by SBV on 2019-01-31 14:27:52.14699 PST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- literal constants ---
(define-fun s6 () (_ BitVec 4) #x4)
(define-fun s3 () (_ BitVec 8) #x04)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 8))
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s1 () (_ BitVec 8) ((_ extract 7 0) s0))
(define-fun s2 () Bool (= s0 s1))
(define-fun s4 () (_ BitVec 8) (bvlshr s1 s3))
(define-fun s5 () (_ BitVec 8) ((_ extract 7 0) s4))
(define-fun s7 () (_ BitVec 8) ((_ zero_extend 4) s6))
(define-fun s8 () (_ BitVec 8) (bvlshr s0 s7))
(define-fun s9 () Bool (= s5 s8))
(define-fun s10 () Bool (not s2))
(define-fun s11 () Bool (or s9 s10))
(assert (not s11))
(check-sat)

I'm not sure whether this is a bug in SBV, or whether Cryptol is using SBV improperly. By the way, the same buggy behavior is also present in saw-script.

[atomb]

We're wondering whether this is a bug in SBV, since both Cryptol and SAW can trigger it, and they call SBV through different code paths. Do you have any thoughts, @LeventErkok?

[LeventErkok]

The relevant SBV code is here:

https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Core/Operations.hs#L383-L398

My guess would be the signedness of the SVal is changing after the drop. Maybe it has an implicit assumption that the result is always unsigned? That would explain it. Perhaps print the annotated IR to see what type comes out of the call to drop?

[brianhuffman]

I noticed that other pairs of signed/unsigned operators show the same problem. All of these work with :prove, while :exhaust finds a counterexample for each.

Cryptol> :prove \(x:[8]) -> (x <$ 4) == (drop`{0} x < 4)
Q.E.D.
(Total Elapsed Time: 0.007s, using Z3)
Cryptol> :prove \(x:[8]) -> (x <=$ 4) == (drop`{0} x <= 4)
Q.E.D.
(Total Elapsed Time: 0.006s, using Z3)
Cryptol> :prove \(x:[8]) -> (x >$ 4) == (drop`{0} x > 4)
Q.E.D.
(Total Elapsed Time: 0.005s, using Z3)
Cryptol> :prove \(x:[8]) -> (x >=$ 4) == (drop`{0} x >= 4)
Q.E.D.
(Total Elapsed Time: 0.007s, using Z3)
Cryptol> :prove \(x:[8]) -> (x /$ 4) == (drop`{0} x / 4)
Q.E.D.
(Total Elapsed Time: 0.006s, using Z3)
Cryptol> :prove \(x:[8]) -> (x %$ 4) == (drop`{0} x % 4)
Q.E.D.
(Total Elapsed Time: 0.006s, using Z3)

[brianhuffman]

The Cryptol code for doing symbolic signed shift right is here:
https://github.com/GaloisInc/cryptol/blob/master/src/Cryptol/Symbolic/Prims.hs#L570-L582

The important bit is the pattern of using svSign and svUnsign to get the signed version of a SBV operator, like SBV.svUnsign (SBV.svShiftRight (SBV.svSign x) y). All of Cryptol's signed operators use a similar pattern.

In SBV, svSign and svUnsign are implemented in terms of svChangeSign:
https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Core/Operations.hs#L597-L612

svChangeSign :: Bool -> SVal -> SVal
svChangeSign s x
  | Just n <- svAsInteger x = svInteger k n
  | True                    = SVal k (Right (cache y))
  where
    k = KBounded s (intSizeOf x)
    y st = do xsw <- svToSV st x
              newExpr st k (SBVApp (Extract (intSizeOf x - 1) 0) [xsw])

Apparently svChangeSign works by creating a new Extract node that is essentially a no-op (because it extracts all the bits) that is tagged with the desired signedness. However, drop`{0} also produces the same extract-all-bits operation in SBV. Perhaps hash-consing is interfering with the sign-change operation somehow?

[LeventErkok]

I bet that’s it. Can you put this in a SBV ticket on github? I’ll fix it over the weekend.

Good catch!

[LeventErkok]

@brianhuffman @atomb

Just pushed a fix. Give it a shot! I trust it should solve the problem: LeventErkok/sbv@d4a05c8

[brianhuffman]

I tested your patch with Cryptol, and it fixes all of the problematic :prove commands that I mentioned above. Thanks, @LeventErkok!

[LeventErkok]

Great! There'll be an 8.1 release sometime this month. Let me know if you need it earlier.

[brianhuffman]

No need to rush. We'll switch cryptol to sbv-8.1 when it's ready. I'll close this ticket once that happens.

[brianhuffman]

Cryptol is using SBV version 8.1 since revision 361e052.