Lit marker blocks computation on bitvectors

[cpitclaudel]

The following code times out:

const SIXTYFOUR_128: bv128 := 64 // as bv128

lemma Timeout(left: bv64, right: bv64)
{
  var e0 := (((left as bv128 << (64 as bv128)) | right as bv128) >> SIXTYFOUR_128) as bv64;
  var e1 := ((left as bv128 << (64 as bv128)) >> SIXTYFOUR_128) as bv64;
  assert e0 == e1;
}

Uncommenting // as bv128 fixes the proof. This is due to #2587 : adding as bv128 removes the Lit marker.

The example is surprisingly unstable and sensitive to small changes. At the Boogie level, it looks like this:

type Box;

function {:identity} Lit<T>(x: T) : T;
axiom (forall<T> x: T :: {:identity} { Lit(x): T } Lit(x): T == x);

function {:bvbuiltin "bvor"} or_bv128(bv128, bv128) : bv128;
function {:bvbuiltin "bvshl"} LeftShift_bv128(bv128, bv128) : bv128;
function {:bvbuiltin "bvlshr"} RightShift_bv128(bv128, bv128) : bv128;

procedure Timeout(left: bv64, right: bv64);
implementation Timeout(left: bv64, right: bv64) {
  var e0: bv64;
  var e1: bv64;
  var tmp: bv128;

  e0 := RightShift_bv128(or_bv128(LeftShift_bv128((0bv64 ++ left): bv128, 64bv128), (0bv64 ++ right): bv128), Lit(64bv128))[64:0];
  e1 := RightShift_bv128(LeftShift_bv128((0bv64 ++ left): bv128, 64bv128), Lit(64bv128))[64:0];
  tmp := RightShift_bv128(LeftShift_bv128((0bv64 ++ left): bv128, 64bv128), Lit(64bv128));

  assert e0 == e1;
}

This example on its own is not enough: one also needs to pass both of the following options to Boogie, or else it finishes instantly:

• -proverOpt:O:auto_config=false and
• -proverOpt:O:smt.case_split=3

Additionally, removing any one of the three Lit marker fixes the issue. So does removing the unused variable tmp.

Here's a minimized version of the SMT2 file (I was surprised to see that it only times out if I add the push/pop pair; not otherwise).

(set-option :print-success false)
(set-info :smt-lib-version 2.6)
(set-option :auto_config false)
(set-option :smt.case_split 3)
(set-option :smt.mbqi false)
(set-option :model.compact false)
(set-option :model.v2 true)
(set-option :pp.bv_literals false)

(set-info :category "industrial")

(declare-sort |T@U| 0)
(declare-sort |T@T| 0)

(declare-fun type (T@U) T@T)

(declare-fun Lit (T@U) T@U)
(assert (forall ((x@@8 T@U))
                (! (= (Lit x@@8) x@@8)
                   :qid |bv8timeoutbpl.4:18|
                   :skolemid |0|
                   :pattern ((Lit x@@8)))))

(declare-fun U_2_bv128 (T@U) (_ BitVec 128))
(declare-fun bv128_2_U ((_ BitVec 128)) T@U)
(declare-fun bv128Type () T@T)
(assert
 (and
  (forall ((arg0@@12 (_ BitVec 128)))
          (! (= (U_2_bv128 (bv128_2_U arg0@@12)) arg0@@12)
             :qid |typeInv:U_2_bv128|
             :pattern ( (bv128_2_U arg0@@12))))
  (forall ((x@@9 T@U))
          (! (=> (= (type x@@9) bv128Type) (= (bv128_2_U (U_2_bv128 x@@9)) x@@9))
             :qid |cast:U_2_bv128|
             :pattern ( (U_2_bv128 x@@9))))
  (forall ((arg0@@13 (_ BitVec 128)))
          (! (= (type (bv128_2_U arg0@@13)) bv128Type)
             :qid |funType:bv128_2_U|
             :pattern ( (bv128_2_U arg0@@13))))))

(declare-fun e0@0 () (_ BitVec 64))
(declare-fun left () (_ BitVec 64))
(declare-fun right () (_ BitVec 64))
(declare-fun e1@0 () (_ BitVec 64))
(declare-fun tmp@0 () (_ BitVec 128))

(push 1)
(set-info :boogie-vc-id Timeout)
(set-option :timeout 5000)
(set-option :rlimit 0)
(assert (= e0@0 ((_ extract 63 0)
                 (bvlshr
                  (bvor (bvshl (concat #x0000000000000000 left) #x00000000000000000000000000000040)
                        (concat #x0000000000000000 right))
                  (U_2_bv128 (Lit (bv128_2_U #x00000000000000000000000000000040)))))))
(assert (= e1@0 ((_ extract 63 0)
                 (bvlshr
                  (bvshl (concat #x0000000000000000 left) #x00000000000000000000000000000040)
                  (U_2_bv128 (Lit (bv128_2_U #x00000000000000000000000000000040)))))))
(assert (= tmp@0 (bvlshr
                  (bvshl (concat #x0000000000000000 left) #x00000000000000000000000000000040)
                  (U_2_bv128 (Lit (bv128_2_U #x00000000000000000000000000000040))))))
(assert (not (= e0@0 e1@0)))
(check-sat)
(pop 1)

Here too we can fix the timeout by either:

• Removing the (U_2_bv128 (Lit (bv128_2_U in any one of the three places that it appears in
• Removing the third assert, which pertains to the unused variable tmp@0.

The first one is readily explained: without these, Z3's internal rewriter kicks in and rewrites the last assert to false:

-------- [rewriter] main_loop ../src/ast/rewriter/rewriter_def.h:746 ---------
(let ((a!1 (bvlshr (bvor (bvshl (concat (_ bv0 64) left) (_ bv64 128))
                         (concat (_ bv0 64) right))
                   (_ bv64 128))))
  (= e0@0 ((_ extract 63 0) a!1)))
=>
(= e0@0 left)
------------------------------------------------
-------- [rewriter] main_loop ../src/ast/rewriter/rewriter_def.h:746 ---------
(let ((a!1 ((_ extract 63 0)
             (bvlshr (bvshl (concat (_ bv0 64) left) (_ bv64 128)) (_ bv64 128)))))
  (= e1@0 a!1))
=>
(= e1@0 left)
------------------------------------------------
-------- [rewriter] main_loop ../src/ast/rewriter/rewriter_def.h:746 ---------
(not (= e0@0 e1@0))
=>
false
------------------------------------------------

I haven't investigated why the removing tmp@0 solves the issue.