Cryptol+z3 takes way too long to prove a simple property about bit rotations

[brianhuffman]

Rotating right by r is the inverse of rotating left by r:

Loading module Cryptol
Cryptol> :prove \(r:[5]) (x:[32]) -> (x <<< r) >>> r == x
Q.E.D.
(Total Elapsed Time: 36.137s, using Z3)

It takes a really long time for z3 to figure this out! (Yices and CVC4 are pretty fast, admittedly.)

However, z3 could be fast on this problem! The issue is that the rotations are encoded in smtlib using tables:

; Automatically created by SBV on 2019-02-14 14:12:06.697067 PST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_UFBV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- literal constants ---
(define-fun s33 () (_ BitVec 32) #x00000000)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 5))
(declare-fun s1 () (_ BitVec 32))
; --- constant tables ---
; --- skolemized tables ---
(declare-fun table0 ((_ BitVec 5)) (_ BitVec 32))
(declare-fun table1 ((_ BitVec 5)) (_ BitVec 32))
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s2 () (_ BitVec 32) ((_ rotate_left 1) s1))
(define-fun s3 () (_ BitVec 32) ((_ rotate_left 2) s1))
(define-fun s4 () (_ BitVec 32) ((_ rotate_left 3) s1))
(define-fun s5 () (_ BitVec 32) ((_ rotate_left 4) s1))
(define-fun s6 () (_ BitVec 32) ((_ rotate_left 5) s1))
(define-fun s7 () (_ BitVec 32) ((_ rotate_left 6) s1))
(define-fun s8 () (_ BitVec 32) ((_ rotate_left 7) s1))
(define-fun s9 () (_ BitVec 32) ((_ rotate_left 8) s1))
(define-fun s10 () (_ BitVec 32) ((_ rotate_left 9) s1))
(define-fun s11 () (_ BitVec 32) ((_ rotate_left 10) s1))
(define-fun s12 () (_ BitVec 32) ((_ rotate_left 11) s1))
(define-fun s13 () (_ BitVec 32) ((_ rotate_left 12) s1))
(define-fun s14 () (_ BitVec 32) ((_ rotate_left 13) s1))
(define-fun s15 () (_ BitVec 32) ((_ rotate_left 14) s1))
(define-fun s16 () (_ BitVec 32) ((_ rotate_left 15) s1))
(define-fun s17 () (_ BitVec 32) ((_ rotate_left 16) s1))
(define-fun s18 () (_ BitVec 32) ((_ rotate_left 17) s1))
(define-fun s19 () (_ BitVec 32) ((_ rotate_left 18) s1))
(define-fun s20 () (_ BitVec 32) ((_ rotate_left 19) s1))
(define-fun s21 () (_ BitVec 32) ((_ rotate_left 20) s1))
(define-fun s22 () (_ BitVec 32) ((_ rotate_left 21) s1))
(define-fun s23 () (_ BitVec 32) ((_ rotate_left 22) s1))
(define-fun s24 () (_ BitVec 32) ((_ rotate_left 23) s1))
(define-fun s25 () (_ BitVec 32) ((_ rotate_left 24) s1))
(define-fun s26 () (_ BitVec 32) ((_ rotate_left 25) s1))
(define-fun s27 () (_ BitVec 32) ((_ rotate_left 26) s1))
(define-fun s28 () (_ BitVec 32) ((_ rotate_left 27) s1))
(define-fun s29 () (_ BitVec 32) ((_ rotate_left 28) s1))
(define-fun s30 () (_ BitVec 32) ((_ rotate_left 29) s1))
(define-fun s31 () (_ BitVec 32) ((_ rotate_left 30) s1))
(define-fun s32 () (_ BitVec 32) ((_ rotate_left 31) s1))
(define-fun s34 () (_ BitVec 32) (table0 s0))
(define-fun s35 () (_ BitVec 32) ((_ rotate_right 1) s34))
(define-fun s36 () (_ BitVec 32) ((_ rotate_right 2) s34))
(define-fun s37 () (_ BitVec 32) ((_ rotate_right 3) s34))
(define-fun s38 () (_ BitVec 32) ((_ rotate_right 4) s34))
(define-fun s39 () (_ BitVec 32) ((_ rotate_right 5) s34))
(define-fun s40 () (_ BitVec 32) ((_ rotate_right 6) s34))
(define-fun s41 () (_ BitVec 32) ((_ rotate_right 7) s34))
(define-fun s42 () (_ BitVec 32) ((_ rotate_right 8) s34))
(define-fun s43 () (_ BitVec 32) ((_ rotate_right 9) s34))
(define-fun s44 () (_ BitVec 32) ((_ rotate_right 10) s34))
(define-fun s45 () (_ BitVec 32) ((_ rotate_right 11) s34))
(define-fun s46 () (_ BitVec 32) ((_ rotate_right 12) s34))
(define-fun s47 () (_ BitVec 32) ((_ rotate_right 13) s34))
(define-fun s48 () (_ BitVec 32) ((_ rotate_right 14) s34))
(define-fun s49 () (_ BitVec 32) ((_ rotate_right 15) s34))
(define-fun s50 () (_ BitVec 32) ((_ rotate_right 16) s34))
(define-fun s51 () (_ BitVec 32) ((_ rotate_right 17) s34))
(define-fun s52 () (_ BitVec 32) ((_ rotate_right 18) s34))
(define-fun s53 () (_ BitVec 32) ((_ rotate_right 19) s34))
(define-fun s54 () (_ BitVec 32) ((_ rotate_right 20) s34))
(define-fun s55 () (_ BitVec 32) ((_ rotate_right 21) s34))
(define-fun s56 () (_ BitVec 32) ((_ rotate_right 22) s34))
(define-fun s57 () (_ BitVec 32) ((_ rotate_right 23) s34))
(define-fun s58 () (_ BitVec 32) ((_ rotate_right 24) s34))
(define-fun s59 () (_ BitVec 32) ((_ rotate_right 25) s34))
(define-fun s60 () (_ BitVec 32) ((_ rotate_right 26) s34))
(define-fun s61 () (_ BitVec 32) ((_ rotate_right 27) s34))
(define-fun s62 () (_ BitVec 32) ((_ rotate_right 28) s34))
(define-fun s63 () (_ BitVec 32) ((_ rotate_right 29) s34))
(define-fun s64 () (_ BitVec 32) ((_ rotate_right 30) s34))
(define-fun s65 () (_ BitVec 32) ((_ rotate_right 31) s34))
(define-fun s66 () (_ BitVec 32) (table1 s0))
(define-fun s67 () Bool (= s1 s66))
(assert (= (table0 #b00000) s1))
(assert (= (table0 #b00001) s2))
(assert (= (table0 #b00010) s3))
(assert (= (table0 #b00011) s4))
(assert (= (table0 #b00100) s5))
(assert (= (table0 #b00101) s6))
(assert (= (table0 #b00110) s7))
(assert (= (table0 #b00111) s8))
(assert (= (table0 #b01000) s9))
(assert (= (table0 #b01001) s10))
(assert (= (table0 #b01010) s11))
(assert (= (table0 #b01011) s12))
(assert (= (table0 #b01100) s13))
(assert (= (table0 #b01101) s14))
(assert (= (table0 #b01110) s15))
(assert (= (table0 #b01111) s16))
(assert (= (table0 #b10000) s17))
(assert (= (table0 #b10001) s18))
(assert (= (table0 #b10010) s19))
(assert (= (table0 #b10011) s20))
(assert (= (table0 #b10100) s21))
(assert (= (table0 #b10101) s22))
(assert (= (table0 #b10110) s23))
(assert (= (table0 #b10111) s24))
(assert (= (table0 #b11000) s25))
(assert (= (table0 #b11001) s26))
(assert (= (table0 #b11010) s27))
(assert (= (table0 #b11011) s28))
(assert (= (table0 #b11100) s29))
(assert (= (table0 #b11101) s30))
(assert (= (table0 #b11110) s31))
(assert (= (table0 #b11111) s32))
(assert (= (table1 #b00000) s34))
(assert (= (table1 #b00001) s35))
(assert (= (table1 #b00010) s36))
(assert (= (table1 #b00011) s37))
(assert (= (table1 #b00100) s38))
(assert (= (table1 #b00101) s39))
(assert (= (table1 #b00110) s40))
(assert (= (table1 #b00111) s41))
(assert (= (table1 #b01000) s42))
(assert (= (table1 #b01001) s43))
(assert (= (table1 #b01010) s44))
(assert (= (table1 #b01011) s45))
(assert (= (table1 #b01100) s46))
(assert (= (table1 #b01101) s47))
(assert (= (table1 #b01110) s48))
(assert (= (table1 #b01111) s49))
(assert (= (table1 #b10000) s50))
(assert (= (table1 #b10001) s51))
(assert (= (table1 #b10010) s52))
(assert (= (table1 #b10011) s53))
(assert (= (table1 #b10100) s54))
(assert (= (table1 #b10101) s55))
(assert (= (table1 #b10110) s56))
(assert (= (table1 #b10111) s57))
(assert (= (table1 #b11000) s58))
(assert (= (table1 #b11001) s59))
(assert (= (table1 #b11010) s60))
(assert (= (table1 #b11011) s61))
(assert (= (table1 #b11100) s62))
(assert (= (table1 #b11101) s63))
(assert (= (table1 #b11110) s64))
(assert (= (table1 #b11111) s65))
(assert (not s67))
(check-sat)

Checking this with z3 takes more than 30 seconds. But checking this equivalent variant takes only a few milliseconds:

(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_UFBV)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 5))
(declare-fun s1 () (_ BitVec 32))
; --- formula ---
(define-fun s2 () (_ BitVec 32) ((_ rotate_left s0) s1))
(define-fun s3 () (_ BitVec 32) ((_ rotate_right s0) s2))
(define-fun s4 () Bool (= s1 s3))
(assert (not s4))
(check-sat)

We should be using the rotate_left and rotate_right functions with symbolic rotation amounts instead of generating lookup tables for rotations.

[brianhuffman]

Ok, it looks like rotate_left and rotate_right with an argument that's not a numeric literal is not part of the smtlib standard. (The smtlib standard does include left- and right-shift operators with symbolic shift amounts, however, but we're not using them either.)

Another encoding of symbolic rotates that z3 handles much better than lookup tables is to use a barrel-shifter-style construction, where we branch on the bits of the rotation amount:

(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_UFBV)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 5))
(declare-fun s1 () (_ BitVec 32))
; --- formula ---
(define-fun x0 () Bool (distinct #b0 ((_ extract 0 0) s0)))
(define-fun x1 () Bool (distinct #b0 ((_ extract 1 1) s0)))
(define-fun x2 () Bool (distinct #b0 ((_ extract 2 2) s0)))
(define-fun x3 () Bool (distinct #b0 ((_ extract 3 3) s0)))
(define-fun x4 () Bool (distinct #b0 ((_ extract 4 4) s0)))

(define-fun s2 () (_ BitVec 32) (ite x0 ((_ rotate_left 1) s1) s1))
(define-fun s3 () (_ BitVec 32) (ite x1 ((_ rotate_left 2) s2) s2))
(define-fun s4 () (_ BitVec 32) (ite x2 ((_ rotate_left 4) s3) s3))
(define-fun s5 () (_ BitVec 32) (ite x3 ((_ rotate_left 8) s4) s4))
(define-fun s6 () (_ BitVec 32) (ite x4 ((_ rotate_left 16) s5) s5))

(define-fun s7 () (_ BitVec 32) (ite x0 ((_ rotate_right 1) s6) s6))
(define-fun s8 () (_ BitVec 32) (ite x1 ((_ rotate_right 2) s7) s7))
(define-fun s9 () (_ BitVec 32) (ite x2 ((_ rotate_right 4) s8) s8))
(define-fun s10 () (_ BitVec 32) (ite x3 ((_ rotate_right 8) s9) s9))
(define-fun s11 () (_ BitVec 32) (ite x4 ((_ rotate_right 16) s10) s10))

(define-fun s12 () Bool (= s11 s1))
(assert (not s12))
(check-sat)

z3 can handle this in just a few hundredths of a second.

[LeventErkok]

@brianhuffman

I'm not sure why you say: _The smtlib standard does include left- and right-shift operators with symbolic shift amounts, however, but we're not using them either._:

Prelude Data.SBV> proveWith z3{verbose=True} $ \x -> (x::SWord8) `sShiftLeft` (2::SWord8) .== x*4
...
[GOOD] (set-logic QF_BV)
...
[GOOD] (define-fun s1 () (_ BitVec 8) #x02)
[GOOD] (define-fun s3 () (_ BitVec 8) #x04)
[GOOD] (declare-fun s0 () (_ BitVec 8))
...
[GOOD] (define-fun s2 () (_ BitVec 8) (bvshl s0 s1))
[GOOD] (define-fun s4 () (_ BitVec 8) (bvmul s0 s3))
[GOOD] (define-fun s5 () Bool (= s2 s4))
[GOOD] (assert (not s5))
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess
Q.E.D.

So, SBV does call the variable versions for sShiftLeft and sShiftRight; is that not what Cryptol is using? If not, we should fix that!

Regarding the rotate: That is a shame indeed; I wish SMTLib allowed for variable rotations. But looks like z3 supports them, so we can:

• Add a SolverCapability to indicate variable rotates are supported, and have SBV spit these out without creating the tables. We already do this for a number of things, so it would be quite within the SBV philosophy. See here: https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Core/Symbolic.hs#L1586-L1601

• Implement the barrel-shifter-style construction as you mentioned; and have all solvers take advantage of this.

  • Do both!

I'd go for option 1, since it is probably simpler to do and honestly z3 is used almost always as the backend; though I do know you also care about ABC.

Pull requests most welcome!

[brianhuffman]

Oh, my mistake about cryptol/sbv not using the symbolic shift amounts; at some point in the past this was true but I guess not anymore.

[LeventErkok]

Yes, it used to be that way back in the day when they didn't have symbolic shift amounts. I wonder why they didn't add it to the rotates.

I'm working on a patch to implement the first idea above, i.e., do it via SolverCapability. If you want to also have the barrel-shifter, I'll leave that to you: You can add that orthogonally later on. (Or, I suppose you can also do that directly inside Cryptol, no SBV support should be necessary for that.)

[LeventErkok]

@brianhuffman

I've played around with this a bit, but ran into z3 issues; filed here: https://github.com/Z3Prover/z3/issues/2142

Depending on their response, my inclination is to support such symbolic rotate cases only if z3 ends up properly supporting them. I've a feeling they don't really support it, but some variants seem to go through the parser.

[LeventErkok]

Ah, as I suspected; z3 doesn't really support symbolic rotates. The fact that what you tried passed was a fluke apparently. They just put in a patch to reject it at parse-time now.

I'll see if I can get your barrel-shift based idea working. I like it better this way as all solvers (potentially) can benefit from it.

[LeventErkok]

@brianhuffman

I've checked in an implementation of "barrel" rotates: https://github.com/LeventErkok/sbv/commit/10e58be41e11a13500838137d07b52f654617edd

Instead of modifying the existing rotate code, I opted to add these as separate functions. The semantics of rotates is already rather complicated, and I think it's worth having the regular version in there in case there's something wrong with the barrel versions. They require bit-vector arguments and also insist that the rotate amount is unsigned. I think that should take care of the Cryptol use case, by generating simpler code.

I tried with z3, and it does seem to be performing well with them. Give it a shot and let me know what you find out. (There'll be an SBV release soon, and then I expect a rather lengthy period of inactivity, so it's best to flesh out any issues quickly.)

[robdockins]

I tested this just now... it seems like we are still using SBV in a way that generates tables for the rotates... but Z3 now seems to solve this problem quickly (0.05s with Z3 4.8.7)? I'm not sure what changed.

Do we still want to swap over to the barrel-shifter?

[robdockins]

This proof is now done essentially instantly by all the solvers I have access to (except ABC, which crashes shrug), I think we can close this. For posterity, my Z3 at the moment is 4.8.7