Leo logical or bitwise negation operation.
(op-not arg) → result
Function:
(defun op-not (arg) (declare (xargs :guard (valuep arg))) (let ((__function__ 'op-not)) (declare (ignorable __function__)) (b* ((err (list :op-not (value-fix arg)))) (cond ((value-case arg :bool) (value-bool (not (value-bool->get arg)))) ((value-case arg :u8) (value-u8 (loghead 8 (lognot (value-u8->get arg))))) ((value-case arg :u16) (value-u16 (loghead 16 (lognot (value-u16->get arg))))) ((value-case arg :u32) (value-u32 (loghead 32 (lognot (value-u32->get arg))))) ((value-case arg :u64) (value-u64 (loghead 64 (lognot (value-u64->get arg))))) ((value-case arg :u128) (value-u128 (loghead 128 (lognot (value-u128->get arg))))) ((value-case arg :i8) (value-i8 (lognot (value-i8->get arg)))) ((value-case arg :i16) (value-i16 (lognot (value-i16->get arg)))) ((value-case arg :i32) (value-i32 (lognot (value-i32->get arg)))) ((value-case arg :i64) (value-i64 (lognot (value-i64->get arg)))) ((value-case arg :i128) (value-i128 (lognot (value-i128->get arg)))) (t (reserrf err))))))
Theorem:
(defthm value-resultp-of-op-not (b* ((result (op-not arg))) (value-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm op-not-of-value-fix-arg (equal (op-not (value-fix arg)) (op-not arg)))
Theorem:
(defthm op-not-value-equiv-congruence-on-arg (implies (value-equiv arg arg-equiv) (equal (op-not arg) (op-not arg-equiv))) :rule-classes :congruence)