Formal verification for lower bound of bit masked AND

bit-masked-and-lower-bound.z3

; https://github.com/llvm/llvm-project/pull/120352/
(define-sort I8 () (_ BitVec 8))

(define-fun extract-msb ((x I8)) Int ((_ bv2int 1) ((_ extract 7 7) x)))
(define-fun-rec cl1 ((x I8)) Int (ite (= #x00 x) 0 (ite (= 0 (extract-msb x)) 0 (+ 1 (cl1 (bvshl x #x01))))))
; (assert (= (cl1 #x00) 0))
; (assert (= (cl1 #x01) 0))
; (assert (= (cl1 #x82) 1))
; (assert (= (cl1 #xc1) 2))
; (assert (= (cl1 #xf7) 4))
; (assert (= (cl1 #xf9) 5))
; (check-sat)

(define-fun set-bit ((x I8) (pos Int)) I8 (bvor x (bvshl #x01 ((_ int2bv 8) pos))))
; (assert (= (set-bit #x01 2) #x05))
; (assert (= (set-bit #x80 0) #x81))
; (assert (= (set-bit #x03 7) #x83))
; (check-sat)

(define-fun clear-bit ((x I8) (pos Int)) I8 (bvand x (bvnot (bvshl #x01 ((_ int2bv 8) pos)))))
; (assert (= (clear-bit #x01 2) #x01))
; (assert (= (clear-bit #x83 7) #x03))
; (assert (= (clear-bit #xf3 1) #xf1))
; (check-sat)

(define-fun-rec set-bits ((x I8) (lo Int) (hi Int)) I8 (ite (>= lo hi) x (bvor (set-bit x lo) (set-bits #x00 (+ 1 lo) hi))))
; (assert (= (set-bits #b10001001 2 5) #b10011101))
; (assert (= (set-bits #b10000001 3 4) #b10001001))
; (assert (= (set-bits #b10100000 0 0) #b10100000))
; (check-sat)

(define-fun-rec clear-bits ((x I8) (lo Int) (hi Int)) I8 (ite (>= lo hi) x (bvand (clear-bit x lo) (clear-bits #xff (+ 1 lo) hi))))
; (assert (= (clear-bits #b01110110 2 5) #b01100010))
; (assert (= (clear-bits #b01111110 3 4) #b01110110))
; (assert (= (clear-bits #b01011111 0 0) #b01011111))
; (check-sat)

(define-fun bvmax ((x I8) (y I8)) I8 (ite (bvult x y) y x))
; (assert (= (bvmax #x01 #x03) #x03))
; (assert (= (bvmax #x71 #x70) #x71))
; (check-sat)

; auto estimateBound = [BitWidth, &Mask](APInt ALo, const APInt &BLo,
;                                        const APInt &BHi) {
;   unsigned LeadingOnes = ((BLo & BHi) | Mask).countLeadingOnes();
;   unsigned StartBit = BitWidth - LeadingOnes;
;   ALo.clearLowBits(StartBit);
;   return ALo;
; };
(define-fun estimateBound ((Mask I8) (ALo I8) (BLo I8) (BHi I8)) I8
    (let ((LeadingOnes (cl1 (bvor Mask (bvand BLo BHi)))))
         (clear-bits ALo 0 (- 8 LeadingOnes))))
; (assert (= #b10010000 (estimateBound #b11000000 #b10010110 #b10111000 #b10111101)))
; (check-sat)


; // Calculate the mask for the higher common bits.
; auto Mask = ~((LLo ^ LHi) | (RLo ^ RHi) | (LLo ^ RLo));
; unsigned LeadingOnes = Mask.countLeadingOnes();
; Mask.clearLowBits(BitWidth - LeadingOnes);
; auto LowerBoundByLHS = estimateBound(LLo, RLo, RHi);
; auto LowerBoundByRHS = estimateBound(RLo, LLo, LHi);
; return APIntOps::umax(LowerBoundByLHS, LowerBoundByRHS);
(define-fun lowerBound ((LLo I8) (LHi I8) (RLo I8) (RHi I8)) I8
    (let ((TmpMask (bvnot (bvor (bvxor LLo LHi) (bvxor RLo RHi) (bvxor LLo RLo)))))
        (let ((LeadingOnes (cl1 TmpMask)))
            (let ((Mask (clear-bits TmpMask 0 (- 8 LeadingOnes))))
                (bvmax (estimateBound Mask LLo RLo RHi) (estimateBound Mask RLo LLo LHi))))))
; (assert (= #b10010000 (lowerBound #b10010001 #b10010110 #b10111000 #b10111101)))
; (check-sat)


(declare-const LLo I8)
(declare-const LHi I8)
(declare-const RLo I8)
(declare-const RHi I8)

(declare-const L I8)
(declare-const R I8)

(assert (bvule L LHi))
(assert (bvuge L LLo))
(assert (bvule R RHi))
(assert (bvuge R RLo))

(declare-const Res I8)
(assert (= Res (bvand L R)))

(declare-const LowerBound I8)
(assert (= LowerBound (lowerBound LLo LHi RLo RHi)))

(push)
(assert (not (bvuge Res LowerBound)))
(check-sat) ; unsat
(pop)