		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Bitnot-integer-value

Apply ~ to an integer value [C:6.5.3.3/4].

Signature
(bitnot-integer-value val) → resval
Arguments: val — Guard (valuep val).
Returns: resval — Type (value-resultp resval).

By the time we reach this ACL2 function, the value has been already promoted, so we put that restriction in the guard.

The result is obtained by complementing each bit of the operand [C:6.5.3.3/4]. Thus, the result must have the same type as the operand.

We calculate the result via lognot followed by result-integer-value, which works for both signed and unsigned operands, as explained below.

For a signed integer of n bits, the result of lognot is a signed integer of n bits: i.e. the following is a theorem

(implies (signed-byte-p n x)
         (signed-byte-p n (lognot x)))

which can be proved, for example, by including community book kestrel/arithmetic-light/expt.lisp.

Thus, applying result-integer-value never yields an error when applied to the result lognot, and just wraps the ACL2 integer into a C integer of the appropriate type.

For an unsigned integer of n bits, lognot returns a negative result (of n bits) if the high (i.e. sign) bit of the operand is set. In this case, to fit into the range of an unsigned C integer, we need to turn the negative integer into the non-negative one that has the same low n bits, and result-integer-value does that; note that mod is equivalent to ACL2::loghead, as can be seen in the definition of the latter.

Because the result of the signed operation is always in range, and the unsigned operation never causes errors in general, this operation never causes errors. So we prove an additional theorem saying that this operation always returns a value. But we need a hypothesis implied by the guard for this to hold. We keep the :returns type broader (i.e. value-resultp) but unconditional, for consistency with other operations.

Definitions and Theorems

Function: bitnot-integer-value

(defun bitnot-integer-value (val)
  (declare (xargs :guard (valuep val)))
  (declare (xargs :guard (and (value-integerp val)
                              (value-promoted-arithmeticp val))))
  (let ((__function__ 'bitnot-integer-value))
    (declare (ignorable __function__))
    (b* ((mathint (value-integer->get val))
         (result (lognot mathint))
         (resval (result-integer-value result (type-of-value val))))
      resval)))

Theorem: value-resultp-of-bitnot-integer-value

(defthm value-resultp-of-bitnot-integer-value
  (b* ((resval (bitnot-integer-value val)))
    (value-resultp resval))
  :rule-classes :rewrite)

Theorem: valuep-of-bitnot-integer-value

(defthm valuep-of-bitnot-integer-value
  (implies (value-integerp val)
           (b* ((?resval (bitnot-integer-value val)))
             (valuep resval))))

Theorem: bitnot-integer-value-of-value-fix-val

(defthm bitnot-integer-value-of-value-fix-val
  (equal (bitnot-integer-value (value-fix val))
         (bitnot-integer-value val)))

Theorem: bitnot-integer-value-value-equiv-congruence-on-val

(defthm bitnot-integer-value-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (bitnot-integer-value val)
                  (bitnot-integer-value val-equiv)))
  :rule-classes :congruence)