		Search-engine friendly clone of the ACL2 documentation.

Instruction-semantic-functions

Simd-sub-spec

Specification for the SIMD subtraction instructions.

Signature
(simd-sub-spec total-size chunk-size x y) → result
Arguments: total-size — Guard (natp total-size).; chunk-size — Guard (posp chunk-size).; x — Guard (unsigned-byte-p total-size x).; y — Guard (unsigned-byte-p total-size y).
Returns: result — Type (unsigned-byte-p total-size result), given the guard.

This is for the (V)PSUBB/(V)PSUBW/(V)PSUBD/(V)PSUBQ instructions.

Given x and y of size total-size in bits, we perform a subtraction on each chunk of size chunk-size in bits, independently from the other chunks, keeping the low chunk-size bits of each result, and putting the resulting chunks together, in the same order, to obtain the final result of size total-size. This kind of operation is illustrated in Intel Manual Volume 1 Figure 9-4 (Dec 2023).

The total-size must be a multiple of chunk-size. For instance, for the VEX form of VPSUBW, total-size is 128 and chunk-size is 16.

Definitions and Theorems

Function: simd-sub-spec

(defun simd-sub-spec (total-size chunk-size x y)
  (declare (xargs :guard (and (natp total-size)
                              (posp chunk-size)
                              (unsigned-byte-p total-size x)
                              (unsigned-byte-p total-size y))))
  (declare (xargs :guard (integerp (/ total-size chunk-size))))
  (let ((__function__ 'simd-sub-spec))
    (declare (ignorable __function__))
    (b* (((when (zp total-size)) 0)
         ((unless (mbt (posp chunk-size))) 0)
         (x-lo (loghead chunk-size x))
         (y-lo (loghead chunk-size y))
         (result-lo (loghead chunk-size (- x-lo y-lo)))
         (x-hi (logtail chunk-size x))
         (y-hi (logtail chunk-size y))
         (result-hi (simd-sub-spec (- total-size chunk-size)
                                   chunk-size x-hi y-hi)))
      (logapp chunk-size result-lo result-hi))))

Theorem: return-type-of-simd-sub-spec

(defthm return-type-of-simd-sub-spec
  (implies
       (and (natp total-size)
            (posp chunk-size)
            (unsigned-byte-p total-size x)
            (unsigned-byte-p total-size y)
            (integerp (binary-* total-size (unary-/ chunk-size))))
       (b* ((result (simd-sub-spec total-size chunk-size x y)))
         (unsigned-byte-p total-size result)))
  :rule-classes :rewrite)