Chop a value down to the given size.
;; Chop X down to its least significant SIZE bits. (defund bvchop (size x) (declare (xargs :guard (and (natp size) (integerp x)))) (mbe :logic (mod (ifix x) (expt 2 (nfix size))) :exec (mod x (expt 2 size))))
