Parallel extraction: Given a source value and a mask, extract the bits in the source that are pointed to by the mask, and put it in the destination starting from the bottom.

>>> satWith z3{printBase = 16} $ \r -> r .== pext (0xAA :: SWord 8) 0xAA
Satisfiable. Model:
  s0 = 0x0f :: Word8
>>> prove $ \x -> pext @8 x 0 .== 0
Q.E.D.
>>> prove $ \x -> pext @8 x (complement 0) .== x
Q.E.D.

Parallel deposit: Given a source value and a mask, write into the destination that are allowed by the mask, grabbing the bits from the source starting from the bottom.

>>> satWith z3{printBase = 16} $ \r -> r .== pdep (0xFF :: SWord 8) 0xAA
Satisfiable. Model:
  s0 = 0xaa :: Word8
>>> prove $ \x -> pdep @8 x 0 .== 0
Q.E.D.
>>> prove $ \x -> pdep @8 x (complement 0) .== x
Q.E.D.

Prove that extraction and depositing with the same mask restore the source in all masked positions:

>>> extractThenDeposit
Q.E.D.

Prove that depositing and extracting with the same mask will push preserve the bottom n-bits of the source, where n is the number of bits set in the mask.

>>> depositThenExtract
Q.E.D.

We can generate the code for these functions if they need to be used in SMTLib. Below is an example at 2-bits, which can be adjusted to produce any bit-size.

>>> putStrLn =<< sbv2smt pext_2
; Automatically generated by SBV. Do not modify!
; pext_2 :: SWord 2 -> SWord 2 -> SWord 2
(define-fun pext_2 ((l1_s0 (_ BitVec 2)) (l1_s1 (_ BitVec 2))) (_ BitVec 2)
                          (let ((l1_s3 #b0))
                          (let ((l1_s7 #b01))
                          (let ((l1_s8 #b00))
                          (let ((l1_s20 #b10))
                          (let ((l1_s2 ((_ extract 1 1) l1_s1)))
                          (let ((l1_s4 (distinct l1_s2 l1_s3)))
                          (let ((l1_s5 ((_ extract 0 0) l1_s1)))
                          (let ((l1_s6 (distinct l1_s3 l1_s5)))
                          (let ((l1_s9 (ite l1_s6 l1_s7 l1_s8)))
                          (let ((l1_s10 (= l1_s7 l1_s9)))
                          (let ((l1_s11 (bvlshr l1_s0 l1_s7)))
                          (let ((l1_s12 ((_ extract 0 0) l1_s11)))
                          (let ((l1_s13 (distinct l1_s3 l1_s12)))
                          (let ((l1_s14 (= l1_s8 l1_s9)))
                          (let ((l1_s15 ((_ extract 0 0) l1_s0)))
                          (let ((l1_s16 (distinct l1_s3 l1_s15)))
                          (let ((l1_s17 (ite l1_s16 l1_s7 l1_s8)))
                          (let ((l1_s18 (ite l1_s6 l1_s17 l1_s8)))
                          (let ((l1_s19 (bvor l1_s7 l1_s18)))
                          (let ((l1_s21 (bvand l1_s18 l1_s20)))
                          (let ((l1_s22 (ite l1_s13 l1_s19 l1_s21)))
                          (let ((l1_s23 (ite l1_s14 l1_s22 l1_s18)))
                          (let ((l1_s24 (bvor l1_s20 l1_s23)))
                          (let ((l1_s25 (bvand l1_s7 l1_s23)))
                          (let ((l1_s26 (ite l1_s13 l1_s24 l1_s25)))
                          (let ((l1_s27 (ite l1_s10 l1_s26 l1_s23)))
                          (let ((l1_s28 (ite l1_s4 l1_s27 l1_s18)))
                          l1_s28))))))))))))))))))))))))))))