hl-addr-combine - ACL2 Book

Included Books

top

other

(in-package "ACL2")

local

(local (include-book "arithmetic-5/top" :dir :system))

local

(local (encapsulate nil
    (local (defthm logior-floor-expt-2-n-opposite
        (implies (and (integerp x) (integerp y) (integerp n) (<= 0 n))
          (equal (floor (logior x y) (expt 2 n))
            (logior (floor x (expt 2 n)) (floor y (expt 2 n)))))))
    (local (defthm mod-logior-expt-2-n-opposite
        (implies (and (integerp x) (integerp y) (integerp n))
          (equal (mod (logior x y) (expt 2 n))
            (logior (mod x (expt 2 n)) (mod y (expt 2 n)))))))
    (local (in-theory (disable logior-floor-expt-2-n mod-logior-expt-2-n)))
    (defthm |(logior a (* b (expt 2 n)))|
      (implies (and (natp a) (integerp b) (natp n) (< a (expt 2 n)))
        (equal (logior a (* b (expt 2 n))) (+ a (* b (expt 2 n)))))
      :hints (("Goal" :in-theory (disable floor-mod-elim)
         :use ((:instance floor-mod-elim
            (x (logior a (* b (expt 2 n))))
            (y (expt 2 n)))))))
    (defthm |(logior a (* (expt 2 n) b))|
      (implies (and (natp a) (integerp b) (natp n) (< a (expt 2 n)))
        (equal (logior a (* (expt 2 n) b)) (+ a (* (expt 2 n) b)))))))

local

(local (encapsulate nil
    (local (defthm lemma1
        (implies (and (< a (expt 2 n))
            (< b (expt 2 n))
            (natp a)
            (natp b)
            (natp n))
          (equal (mod (+ b (* (expt 2 n) a)) (expt 2 n))
            (mod b (expt 2 n))))))
    (local (defthm lemma2
        (implies (and (< a (expt 2 n))
            (< b (expt 2 n))
            (natp a)
            (natp b)
            (natp n))
          (equal (floor (+ b (* (expt 2 n) a)) (expt 2 n)) a))))
    (local (defthm equal-by-floor-and-mod
        (implies (and (natp a) (natp b) (natp n))
          (equal (equal a b)
            (and (equal (floor a n) (floor b n))
              (equal (mod a n) (mod b n)))))
        :rule-classes nil))
    (defthm |a*2^n + b == c*2^n + d when <= 2^n|
      (implies (and (< a (expt 2 n))
          (< b (expt 2 n))
          (< c (expt 2 n))
          (< d (expt 2 n))
          (natp a)
          (natp b)
          (natp c)
          (natp d)
          (natp n))
        (equal (equal (+ b (* (expt 2 n) a)) (+ d (* (expt 2 n) c)))
          (and (equal a c) (equal b d))))
      :hints (("Goal" :use ((:instance equal-by-floor-and-mod
            (a (+ b (* (expt 2 n) a)))
            (b (+ d (* (expt 2 n) c)))
            (n (expt 2 n)))))))))

hl-nat-combinefunction

(defund hl-nat-combine
  (a b)
  (declare (xargs :guard (and (natp a) (natp b))))
  (mbe :logic (+ (/ (* (+ a b 1) (+ a b)) 2) b)
    :exec (+ (let* ((a+b (+ a b)) (a+b+1 (+ 1 a+b)))
        (if (= (logand a+b 1) 0)
          (* (ash a+b -1) a+b+1)
          (* a+b (ash a+b+1 -1))))
      b)))

natp-of-hl-nat-combineencapsulate

(encapsulate nil
  (local (in-theory (enable hl-nat-combine)))
  (local (defun sum-up-to
      (n)
      (declare (xargs :guard (natp n)))
      (if (zp n)
        0
        (+ n (sum-up-to (1- n))))))
  (local (defthm sum-up-to-identity
      (implies (natp n) (equal (/ (* n (+ 1 n)) 2) (sum-up-to n)))))
  (local (defthm hl-nat-combine-redefinition
      (implies (and (natp a) (natp b))
        (equal (hl-nat-combine a b) (+ (sum-up-to (+ a b)) b)))
      :hints (("Goal" :use ((:instance sum-up-to-identity (n (+ a b))))))))
  (defthm natp-of-hl-nat-combine
    (implies (and (natp a) (natp b))
      (natp (hl-nat-combine a b))))
  (local (defun sum-interval
      (a b)
      (declare (xargs :guard (and (natp a) (natp b))
          :measure (nfix (- (nfix b) (nfix a)))))
      (let ((a (nfix a)) (b (nfix b)))
        (if (<= b a)
          0
          (+ b (sum-interval a (- b 1)))))))
  (local (defthmd decompose-sum-up-to
      (implies (and (natp a) (natp b) (< a b))
        (equal (sum-up-to b) (+ (sum-up-to a) (sum-interval a b))))))
  (local (defthm decompose-rhs
      (implies (and (natp a)
          (natp b)
          (natp c)
          (natp d)
          (< (+ a b) (+ c d)))
        (equal (hl-nat-combine c d)
          (+ (sum-up-to (+ a b)) (sum-interval (+ a b) (+ c d)) d)))
      :hints (("Goal" :use ((:instance decompose-sum-up-to (b (+ c d)) (a (+ a b))))))))
  (local (defthm sum-interval-lower-bound
      (implies (and (natp a) (natp b) (< a b))
        (< a (sum-interval a b)))
      :rule-classes :linear))
  (defthm hl-nat-combine-is-one-to-one
    (implies (and (natp a) (natp b) (natp c) (natp d))
      (equal (equal (hl-nat-combine a b) (hl-nat-combine c d))
        (and (equal a c) (equal b d))))
    :hints (("Goal" :cases ((equal (+ a b) (+ c d)) (< (+ a b) (+ c d))
         (< (+ c d) (+ a b))))))
  (defthm hl-nat-combine-monotonic-a
    (implies (and (natp a) (natp a2) (natp b) (< a a2))
      (< (hl-nat-combine a b) (hl-nat-combine a2 b)))
    :rule-classes :linear)
  (defthm hl-nat-combine-monotonic-b
    (implies (and (natp a) (natp b) (natp b2) (< b b2))
      (< (hl-nat-combine a b) (hl-nat-combine a b2)))
    :rule-classes :linear))

local

(local (defthm guard-lemma
    (implies (and (< b 1073741824) (natp b) (integerp a))
      (equal (logior b (* 1073741824 a)) (+ b (* 1073741824 a))))
    :hints (("Goal" :in-theory (disable |(logior a (* (expt 2 n) b))|)
       :use ((:instance |(logior a (* (expt 2 n) b))| (n 30) (a b) (b a)))))))

hl-addr-combinefunction

(defund hl-addr-combine
  (a b)
  (declare (xargs :guard (and (natp a) (natp b))))
  (mbe :logic (if (and (< a (expt 2 30)) (< b (expt 2 30)))
      (- (+ (* a (expt 2 30)) b))
      (- (hl-nat-combine a b) (+ (expt 2 59) (expt 2 29) -1)))
    :exec (if (and (< a 1073741824) (< b 1073741824))
      (the (signed-byte 61)
        (- (the (signed-byte 61)
            (logior (the (signed-byte 61) (ash (the (signed-byte 31) a) 30))
              (the (signed-byte 31) b)))))
      (- (hl-nat-combine a b) 576460752840294399))))

hl-addr-combine-is-one-to-oneencapsulate

(encapsulate nil
  (local (in-theory (enable hl-addr-combine)))
  (local (defthm small-case-non-positive
      (implies (and (< a (expt 2 30)) (< b (expt 2 30)) (natp a) (natp b))
        (<= (hl-addr-combine a b) 0))))
  (local (encapsulate nil
      (local (defthmd monotonicity-corollary-1
          (implies (and (natp a) (natp b) (<= (expt 2 30) a))
            (<= 576460752840294400 (hl-nat-combine a b)))
          :hints (("Goal" :in-theory (disable hl-nat-combine-monotonic-a
               hl-nat-combine-monotonic-b)
             :use ((:instance hl-nat-combine-monotonic-b (a a) (b 0) (b2 b)) (:instance hl-nat-combine-monotonic-a
                 (a (expt 2 30))
                 (a2 a)
                 (b 0)))))))
      (local (defthmd monotonicity-corollary-2
          (implies (and (natp a) (natp b) (<= (expt 2 30) b))
            (<= 576460753914036224 (hl-nat-combine a b)))
          :hints (("Goal" :in-theory (disable hl-nat-combine-monotonic-a
               hl-nat-combine-monotonic-b)
             :use ((:instance hl-nat-combine-monotonic-b
                (a 0)
                (b (expt 2 30))
                (b2 b)) (:instance hl-nat-combine-monotonic-a (a 0) (a2 a) (b b)))))))
      (defthm large-case-positive
        (implies (and (or (not (< a (expt 2 30))) (not (< b (expt 2 30))))
            (natp a)
            (natp b))
          (< 0 (hl-addr-combine a b)))
        :hints (("Goal" :use ((:instance monotonicity-corollary-1) (:instance monotonicity-corollary-2)))))))
  (local (defthm small-case-one-to-one
      (implies (and (< a (expt 2 30))
          (< b (expt 2 30))
          (< c (expt 2 30))
          (< d (expt 2 30))
          (natp a)
          (natp b)
          (natp c)
          (natp d))
        (equal (equal (hl-addr-combine a b) (hl-addr-combine c d))
          (and (equal a c) (equal b d))))
      :hints (("Goal" :in-theory (disable (expt))))))
  (local (defthm large-case-one-to-one
      (implies (and (or (<= (expt 2 30) a) (<= (expt 2 30) b))
          (or (<= (expt 2 30) c) (<= (expt 2 30) d))
          (natp a)
          (natp b)
          (natp c)
          (natp d))
        (equal (equal (hl-addr-combine a b) (hl-addr-combine c d))
          (and (equal a c) (equal b d))))))
  (local (in-theory (disable hl-addr-combine)))
  (defthm hl-addr-combine-is-one-to-one
    (implies (and (natp a) (natp b) (natp c) (natp d))
      (equal (equal (hl-addr-combine a b) (hl-addr-combine c d))
        (and (equal a c) (equal b d))))
    :hints (("Goal" :cases ((and (< a (expt 2 30))
          (< b (expt 2 30))
          (< c (expt 2 30))
          (< d (expt 2 30))) (and (or (<= (expt 2 30) a) (<= (expt 2 30) b))
           (or (<= (expt 2 30) c) (<= (expt 2 30) d))))) ("Subgoal 3" :in-theory (disable small-case-non-positive large-case-positive)
        :use ((:instance small-case-non-positive (a a) (b b)) (:instance small-case-non-positive (a c) (b d))
          (:instance large-case-positive (a a) (b b))
          (:instance large-case-positive (a c) (b d)))))))