diff options
Diffstat (limited to 'books/workshops/1999/pipeline/b-ops-aux.lisp')
| -rw-r--r-- | books/workshops/1999/pipeline/b-ops-aux.lisp | 738 |
1 files changed, 738 insertions, 0 deletions
diff --git a/books/workshops/1999/pipeline/b-ops-aux.lisp b/books/workshops/1999/pipeline/b-ops-aux.lisp new file mode 100644 index 0000000..434d07c --- /dev/null +++ b/books/workshops/1999/pipeline/b-ops-aux.lisp @@ -0,0 +1,738 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; b-ops-aux.lisp: +;; This file contains auxiliary lemmas to assist the IHS library +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(in-package "ACL2") + +(include-book "b-ops-aux-def") + +(deflabel begin-b-ops-aux) + +;; Type of b-if +(defthm bitp-b-if + (implies (and (bitp y) (bitp z)) + (bitp (b-if x y z))) + :hints (("goal" :in-theory (enable bitp)))) + +(defthm integerp-b-if + (implies (and (integerp y) (integerp z)) + (integerp (b-if x y z))) + :hints (("goal" :in-theory (enable bitp)))) + +(defthm b-not-b-not + (equal (b-not (b-not i)) (bfix i)) + :hints (("goal" :in-theory (enable b-not bfix zbp)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Here are several basic lemmas about bit operations. + +;; If bit vector X is longer than (p+s), bits between the p'th and (p+s)'th +;; bits of the concatenation of x and y is equal to that of x. +(defthm rdb-logapp-1 + (implies (and (integerp x) (integerp y) (integerp i) (<= 0 i) + (integerp s) (<= 0 s) (integerp p) (<= 0 p) + (<= (+ s p) i)) + (equal (rdb (cons s p) (logapp i x y)) + (rdb (cons s p) x))) + :hints (("Goal" :in-theory (enable logapp* rdb bsp-size bsp-position)))) + +;; If bit vector X is shorter than p, bits from the p'th LSB to (p+s)'th +;; LSB of the concatenation of x and y is equal to that of y. +(defthm rdb-logapp-2 + (implies (and (integerp x) (integerp y) + (integerp s) (<= 0 s) (integerp p) (<= 0 p) + (integerp i) (<= 0 i) + (<= i p)) + (equal (rdb (cons s p) (logapp i x y)) + (rdb (cons s (- p i)) y))) + :hints (("Goal" :in-theory (enable logapp* rdb bsp-size bsp-position)))) + + +(defthm loghead-0 + (equal (loghead x 0) 0) + :hints (("Goal" :in-theory (enable loghead)))) + +(defthm loghead-1 + (equal (loghead 1 vector) (logcar vector)) + :hints (("Goal" :in-theory (enable logcar loghead)))) + +(defthm logcar-bitp + (implies (bitp x) + (equal (logcar x) x)) + :hints (("Goal" :in-theory (enable bitp logcar)))) + +(defthm logbit-0-bitp + (implies (bitp x) + (equal (logbit 0 x) x)) + :hints (("Goal" :in-theory (enable bitp logbit)))) + +(defthm loghead-bitp + (implies (bitp x) + (equal (loghead 1 x) x)) + :hints (("Goal" :in-theory (enable rdb)))) + + +(defthm logcons-0 + (implies (bitp x) + (equal (logcons x 0) x)) + :hints (("Goal" :in-theory (enable logcons)))) + +(defthm rdb-bitp + (implies (bitp x) + (equal (rdb (cons 1 0) x) x)) + :hints (("Goal" :in-theory (enable rdb)))) + +(defthm rdb-0 + (equal (rdb (cons 0 n) x) 0) + :hints (("Goal" :in-theory (enable rdb bsp-size)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Here begins a basic theory about lobops +; Recursive definition of Logbit*. +(defthm logbit* + (implies (and (integerp pos) + (>= pos 0) + (integerp i)) + (equal (logbit pos i) + (if (equal pos 0) + (logcar i) + (logbit (1- pos) (logcdr i))))) + :rule-classes :definition + :hints (("Goal" :in-theory (e/d (logbit logbitp*) (logbitp))))) + +(in-theory (disable logbit*)) + +(local +(defun logtail-induct (pos i) + (if (zp pos) + i + (logtail-induct (1- pos) (logcdr i))))) + + +(defthm logcar-logtail + (implies (and (integerp n) (<= 0 n) + (integerp x)) + (equal (logcar (logtail n x)) + (logbit n x))) + :hints (("Goal" :in-theory (e/d (logtail* logbit logbitp*) + (logbitp)) + :induct (logtail-induct n x)))) + +(defthm logcdr-logtail + (implies (and (integerp n) (<= 0 n) + (integerp x)) + (equal (logcdr (logtail n x)) + (logtail (1+ n) x))) + :hints (("Goal" :in-theory (enable logtail*) + :induct (logtail-induct n x)))) + +;; The following two lemmas are for expansion before BDD +(deflabel begin-bv-expand) +(defthm rdb-expand + (implies (and (syntaxp (and (quoted-constant-p s) (quoted-constant-p n))) + (integerp s) (< 0 s) + (integerp n) (<= 0 n) + (integerp x)) + (equal (rdb (cons s n) x) + (logcons (logbit n x) (rdb (cons (1- s) (1+ n)) x)))) + :hints (("Goal" :in-theory (enable rdb bsp-position bsp-size loghead* + logtail*)))) + + +;; logops supplement for logxxx operations. There are bunch of +;; definition rules logior* and so on, but they are definition rules. +;; We rewrite rules to forcibly open up the expressions before applying +;; BDD techniques. We redefine the same lemma as a rewrite rule. +(defthm open-logior-right-const + (implies (and (bitp i1) + (integerp i2) + (integerp j)) + (equal (logior (logcons i1 i2) j) + (logcons (b-ior i1 (logcar j)) (logior i2 (logcdr j))))) + :hints (("Goal" :in-theory (enable logior*)))) + + +(defthm open-logior-left-const + (implies (and (bitp j1) + (integerp j2) + (integerp i)) + (equal (logior i (logcons j1 j2)) + (logcons (b-ior (logcar i) j1) (logior (logcdr i) j2)))) + :hints (("Goal" :in-theory (enable logior*)))) + +(defthm open-logior + (implies (and (bitp i1) + (bitp j1) + (integerp i2) + (integerp j2)) + (equal (logior (logcons i1 i2) (logcons j1 j2)) + (logcons (b-ior i1 j1) (logior i2 j2)))) + :hints (("Goal" :in-theory (enable logior*)))) + +(defthm open-logxor-right-const + (implies (and (bitp i1) + (integerp i2) + (integerp j)) + (equal (logxor (logcons i1 i2) j) + (logcons (b-xor i1 (logcar j)) (logxor i2 (logcdr j))))) + :hints (("Goal" :in-theory (enable logxor*)))) + + +(defthm open-logxor-left-const + (implies (and (bitp j1) + (integerp j2) + (integerp i)) + (equal (logxor i (logcons j1 j2)) + (logcons (b-xor (logcar i) j1) (logxor (logcdr i) j2)))) + :hints (("Goal" :in-theory (enable logxor*)))) + +(defthm open-logxor + (implies (and (bitp i1) + (bitp j1) + (integerp i2) + (integerp j2)) + (equal (logxor (logcons i1 i2) (logcons j1 j2)) + (logcons (b-xor i1 j1) (logxor i2 j2)))) + :hints (("Goal" :in-theory (enable logxor*)))) + + + + +(defthm open-logand-right-const + (implies (and (bitp i1) + (integerp i2) + (integerp j)) + (equal (logand (logcons i1 i2) j) + (logcons (b-and i1 (logcar j)) (logand i2 (logcdr j))))) + :hints (("Goal" :in-theory (enable logand*)))) + + +(defthm open-logand-left-const + (implies (and (bitp j1) + (integerp j2) + (integerp i)) + (equal (logand i (logcons j1 j2)) + (logcons (b-and (logcar i) j1) (logand (logcdr i) j2)))) + :hints (("Goal" :in-theory (enable logand*)))) + +(defthm open-logand + (implies (and (bitp i1) + (bitp j1) + (integerp i2) + (integerp j2)) + (equal (logand (logcons i1 i2) (logcons j1 j2)) + (logcons (b-and i1 j1) (logand i2 j2)))) + :hints (("Goal" :in-theory (enable logand*)))) + +(defthm open-lognot + (implies (and (bitp i1) + (integerp i2)) + (equal (lognot (logcons i1 i2)) + (logcons (b-not i1) (lognot i2)))) + :hints (("Goal" :in-theory (enable lognot*)))) + +(defthm fold-logcdr-vector + (implies (and (integerp x) + (syntaxp (or (not (consp x)) + (not (equal (car x) 'logcons$inline))))) + (equal (logcdr x) (logtail 1 x))) + :hints (("goal" :in-theory (enable logtail*)))) +(in-theory (disable fold-logcdr-vector)) + +(defthm fold-logcar-vector + (implies (and (integerp x) + (syntaxp (or (not (consp x)) + (not (equal (car x) 'logcons$inline))))) + (equal (logcar x) (logbit 0 x))) + :hints (("goal" :in-theory (e/d (logbit logbitp*) + (logbitp))))) + +(in-theory (disable fold-logcar-vector)) +(deflabel end-bv-expand) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bv-eqv rules +(defthm bv-eqv* + (implies (and (integerp x) + (integerp y) + (integerp n) + (>= n 0)) + (equal (bv-eqv n x y) + (if (zp n) + 1 + (b-and (b-eqv (logcar x) (logcar y)) + (bv-eqv (1- n) (logcdr x) (logcdr y)))))) + :hints (("goal" :in-theory (enable bv-eqv loghead*))) + :rule-classes :definition) + +(in-theory (disable bv-eqv*)) + +;; Following lemma is useful in converting a formula with 'bv-eqv' to one +;; with 'equal'. +;; This can cause BDD simplification to fail, especially if when the words +;; need to be open up. +(defthm bv-eqv-iff-equal + (implies (and (unsigned-byte-p n x) (unsigned-byte-p n y)) + (equal (b1p (bv-eqv n x y)) + (equal x y))) + :hints (("Goal" :in-theory (enable bv-eqv b1p)))) + +(defthm bv-eqv-0 + (equal (bv-eqv 0 x y) 1) + :Hints (("Goal" :in-theory (enable bv-eqv)))) + +(defthm bv-x-x + (equal (bv-eqv n x x) 1) + :hints (("goal" :in-theory (enable bv-eqv)))) + +(defthm bv-eqv-assoc + (equal (bv-eqv n x y) (bv-eqv n y x)) + :hints (("Goal" :in-theory (enable bv-eqv)))) + +(defthm bv-eqv-bits + (implies (and (bitp x) (bitp y) (integerp n) (> n 0)) + (equal (bv-eqv n x y) (b-eqv x y))) + :hints (("Goal" :in-theory (enable bv-eqv* bitp bv-eqv-iff-equal)))) + +(defthm bv-eqv-expand + (implies (and (integerp x) (integerp y) + (integerp n) (> n 0) + (syntaxp (quoted-constant-p n))) + (equal (bv-eqv n x y) + (b-and (b-eqv (logcar x) (logcar y)) + (bv-eqv (1- n) (logcdr x) (logcdr y))))) + :hints (("Goal" :in-theory (enable bv-eqv*)))) + +;; Following lemma is a schematic lemma which will be used in BDD proof. +;; We noticed that several lemmas is a tautology under the property that +;; (bv-eqv x y) and (bv-eqv x z) are not simultaneously asserted, if y and +;; z are not equal. We instantiate the following lemma and add it to BDD +;; proof as a hint. +(defthm bv-eqv-transitivity + (implies (and (unsigned-byte-p n x) + (unsigned-byte-p n y) + (unsigned-byte-p n z) + (b1p (b-and (bv-eqv n x z) (bv-eqv n y z)))) + (equal x y)) + :hints (("Goal" :in-theory (enable bv-eqv ))) + :rule-classes nil) + +;; Bv-expander is the theory to be enabled to expand bit vectors before +;; applying bdd's. +(deftheory bv-expander + '(rdb-expand + open-lognot + open-logand open-logand-right-const open-logand-left-const + open-logior open-logior-right-const open-logior-left-const + open-logxor open-logxor-right-const open-logxor-left-const + fold-logcar-vector fold-logcdr-vector + bv-eqv-bits + bv-eqv-0 + bv-eqv-expand)) + +(in-theory (disable bv-expander)) + +(local (in-theory (enable b1p))) + +;; Bit-boolean-converter converting expressions of form (equal x 1) to +;; expressions using bitp, lest BDD package assigns different boolean values +;; to (b1p x) and (equal x 1). It also converts (equal x 0) to (not (b1p x)). +(defthm equal-to-1-to-b1p + (implies (bitp x) + (equal (equal x 1) + (b1p x))) + :Hints (("Goal" :In-theory (enable bitp)))) + +(defthm equal-to-0-to-not-b1p + (implies (bitp x) + (equal (equal x 0) + (not (b1p x)))) + :Hints (("Goal" :In-theory (enable bitp)))) + +(defthm equal-to-b1p-b-eqv + (implies (and (bitp x) (bitp y)) + (equal (equal x y) (b1p (b-eqv x y)))) + :hints (("Goal" :in-theory (enable b-eqv b1p zbp bitp)))) + +(deftheory equal-b1p-converter + '(equal-to-1-to-b1p equal-to-0-to-not-b1p)) + +(in-theory (disable equal-b1p-converter)) +(in-theory (disable equal-to-b1p-b-eqv)) + +;; From here, we define bit-to-boolean converter, especially for BDD +;; operation. +(deflabel begin-lift-b-ops) + +(defthm zbp-b-and + (equal (zbp (b-and x y)) + (or (zbp x) (zbp y))) + :Hints (("Goal" :in-theory (enable b-and)))) + +(defthm zbp-b-ior + (equal (zbp (b-ior x y)) + (and (zbp x) (zbp y))) + :Hints (("Goal" :in-theory (enable b-ior)))) + +(defthm zbp-b-xor + (equal (zbp (b-xor x y)) + (or (and (zbp x) (zbp y)) + (and (not (zbp x)) (not (zbp y))))) + :Hints (("Goal" :in-theory (enable b-xor)))) + +(defthm zbp-b-not + (equal (zbp (b-not x)) + (not (zbp x))) + :Hints (("Goal" :in-theory (enable b-not)))) + +(defthm zbp-b-eqv + (equal (zbp (b-eqv x y)) + (not (iff (zbp x) (zbp y)))) + :Hints (("Goal" :in-theory (enable b-eqv)))) + + + +(defthm b1p-b-and + (equal (b1p (b-and x y)) + (and (b1p x) (b1p y))) + :Hints (("Goal" :in-theory (enable b-and)))) + +(defthm b1p-b-ior + (equal (b1p (b-ior x y)) + (or (b1p x) (b1p y))) + :Hints (("Goal" :in-theory (enable b-ior)))) + +(defthm b1p-b-xor + (equal (b1p (b-xor x y)) + (or (and (b1p x) (not (b1p y))) + (and (not (b1p x)) (b1p y)))) + :Hints (("Goal" :in-theory (enable b-xor)))) + +(defthm b1p-b-not + (equal (b1p (b-not x)) + (not (b1p x))) + :Hints (("Goal" :in-theory (enable b-not)))) + +(defthm b1p-b-eqv + (equal (b1p (b-eqv x y)) + (iff (b1p x) (b1p y))) + :Hints (("Goal" :in-theory (enable b-eqv)))) + +(defthm b1p-nand (equal (b1p (b-nand x y)) (not (and (b1p x) (b1p y)))) + :hints (("Goal" :in-theory (enable b-nand)))) + +(defthm b1p-nor (equal (b1p (b-nor x y)) (not (or (b1p x) (b1p y)))) + :hints (("Goal" :in-theory (enable b-nor)))) + +(defthm b1p-andc1 (equal (b1p (b-andc1 x y)) (and (not (b1p x)) (b1p y))) + :hints (("Goal" :in-theory (enable b-andc1)))) + +(defthm b1p-andc2 (equal (b1p (b-andc2 x y)) (and (b1p x) (not (b1p y)))) + :hints (("Goal" :in-theory (enable b-andc2)))) + +(defthm b1p-orc1 (equal (b1p (b-orc1 x y)) (or (not (b1p x)) (b1p y))) + :hints (("Goal" :in-theory (enable b-orc1)))) + +(defthm b1p-orc2 (equal (b1p (b-orc2 x y)) (or (b1p x) (not (b1p y)))) + :hints (("Goal" :in-theory (enable b-orc2)))) + +(defthm zbp-to-b1p + (equal (zbp x) (not (b1p x))) + :hints (("Goal" :in-theory (enable b1p)))) + +(deflabel end-lift-b-ops) + +(deftheory lift-b-ops + (set-difference-theories (universal-theory 'end-lift-b-ops) + (universal-theory 'begin-lift-b-ops))) + +(in-theory (disable lift-b-ops)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; New Simplifier +; This simplifier simplifies bit terms into 1 and 0's using information +; represented by b1p. +; Origianl Simplify-Bit-Functions can simplify expressions with bit-functions +; if its arguments are 0 or 1's. For instance, it can reduce expressions +; with a rule like: +; (EQUAL (B-AND 1 X) (BFIX X)) +; In the new simplifier reduces the expressions if hypothesis satisfies +; certain conditions, like +; (implies (and (bitp x) (bitp y) (not (b1p y))) +; (equal (b-and x y) 0)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(deflabel begin-b1p-bit-rewriter) + +(defthm b1p-bit-forward + (implies (and (b1p b) (force (bitp b))) (equal b 1)) + :hints (("goal" :in-theory (enable b1p bitp zbp))) + :rule-classes :forward-chaining) + +(defthm not-b1p-bit-forward + (implies (and (not (b1p b)) (force (bitp b))) (equal b 0)) + :hints (("goal" :in-theory (enable b1p bitp zbp))) + :rule-classes :forward-chaining) + +(defthm simplify-bit-functions-2 + (and (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-and x y) 0)) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-and x y) 0)) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-and x y) y)) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-and x y) x)) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-ior x y) y)) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-ior x y) x)) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-ior x y) 1)) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-ior x y) 1)) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-xor x y) y)) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-xor x y) x)) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-xor x y) (b-not y))) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-xor x y) (b-not x))) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-eqv x y) (b-not y))) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-eqv x y) (b-not x))) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-eqv x y) y)) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-eqv x y) x)) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-nand x y) 1)) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-nand x y) 1)) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-nand x y) (b-not y))) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-nand x y) (b-not x))) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-nor x y) (b-not y))) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-nor x y) (b-not x))) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-nor x y) 0)) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-nor x y) 0)) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-andc1 x y) y)) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-andc1 x y) 0)) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-andc1 x y) 0)) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-andc1 x y) (b-not x))) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-andc2 x y) 0)) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-andc2 x y) x)) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-andc2 x y) (b-not y))) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-andc2 x y) 0)) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-orc1 x y) 1)) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-orc1 x y) (b-not x))) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-orc1 x y) y)) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-orc1 x y) 1)) + + (implies (and (bitp x) (bitp y) (not (b1p x))) + (equal (b-orc2 x y) (b-not y))) + (implies (and (bitp x) (bitp y) (not (b1p y))) + (equal (b-orc2 x y) 1)) + (implies (and (bitp x) (bitp y) (b1p x)) + (equal (b-orc2 x y) 1)) + (implies (and (bitp x) (bitp y) (b1p y)) + (equal (b-orc2 x y) x))) + :hints (("Goal" :in-theory (enable b1p zbp b-and bitp)))) + +(deflabel end-b1p-bit-rewriter) + +(deftheory b1p-bit-rewriter + (set-difference-theories (universal-theory 'end-b1p-bit-rewriter) + (universal-theory 'begin-b1p-bit-rewriter))) + +(in-theory (disable b1p-bit-rewriter)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; BDD helps +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(deftheory pre-bdd-disables + '(bv-eqv-iff-equal simplify-bit-functions)) + +(deftheory bdd-disables + '(bv-eqv-iff-equal simplify-bit-functions)) + +(theory-invariant (incompatible (:rewrite bv-eqv-iff-equal) + (:rewrite rdb-expand))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; range of unsigned-byte-p +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; theories about the range of unsigned-byte-p +(defthm plus-unsigned-byte-p-lt-2-*-expt-2-width + (implies (and (unsigned-byte-p width val1) + (unsigned-byte-p width val2)) + (< (+ val1 val2) (* 2 (expt 2 width)))) + :hints (("goal" :in-theory (enable unsigned-byte-p)))) + +(defun logbit-induction (pos val) + (if (zp pos) + val + (logbit-induction (1- pos) (logcdr val)))) + +; If a value are in the range 0 <= val < 2^width +; then the width'th bit of val is not set. +(defthm logbit-0-if-val-lt-expt-2-width + (implies (and (integerp width) (<= 0 width) + (integerp val) + (<= 0 val) (< val (expt 2 width))) + (equal (logbit width val) 0)) + :hints (("goal" :in-theory (e/d (logbit* expt logcar logcdr) + (exponents-add)) + :induct (logbit-induction width val))) + :rule-classes nil) + + +(encapsulate nil +(local + (defthm logbit-1-if-val-gt-expt-2-width-help1 + (IMPLIES (AND (INTEGERP WIDTH) + (< 0 WIDTH) + (INTEGERP VAL) + (<= (* 2 (EXPT 2 (+ -1 WIDTH))) VAL) + (< (/ VAL 2) (* 2 (EXPT 2 (+ -1 WIDTH))))) + (> (* 2 (EXPT 2 (+ -1 WIDTH))) + (FLOOR VAL 2))) + :rule-classes nil)) + +(local + (defthm logbit-1-if-val-gt-expt-2-width-help2 + (implies (and (integerp val) + (integerp width) (< 0 width) + (< VAL (* 2 2 (EXPT 2 (+ -1 WIDTH))))) + (< (/ VAL 2) (* 2 (EXPT 2 (+ -1 WIDTH))))) + :hints (("goal" :in-theory (e/d (expt) (exponents-add)))) + :rule-classes nil)) + +(local +(defthm logbit-1-if-val-gt-expt-2-width-help + (IMPLIES (AND (INTEGERP WIDTH) + (INTEGERP VAL) + (< 0 WIDTH) + (<= (* 2 (EXPT 2 (+ -1 WIDTH))) (FLOOR VAL 2))) + (<= (* 2 2 (EXPT 2 (+ -1 WIDTH))) VAL)) + :hints (("goal" :in-theory (e/d (exponents-add) (expt)) + :use ((:instance logbit-1-if-val-gt-expt-2-width-help1) + (:instance logbit-1-if-val-gt-expt-2-width-help2)))))) + + +; If a value are in the range 2^width <= val < 2^width * 2, +; then the width'th bit of val is set. +(defthm logbit-1-if-val-gt-expt-2-width + (implies (and (integerp width) (<= 0 width) + (integerp val) + (<= (expt 2 width) val) + (< val (* 2 (expt 2 width)))) + (equal (logbit width val) 1)) + :hints (("goal" :in-theory (e/d (logbit* expt logcar logcdr) + (exponents-add)) + :induct (logbit-induction width val))) + :rule-classes nil) +) + +; Suppose val1 and val2 are unsigned-byte-p whose width is w. +; If w'th bit of the sum (+ val1 val2) is not set, +; (+ val1 val2) < 2^w. +(defthm plus-unsigned-byte-lt-expt-2-width-if-logbit + (implies (and (unsigned-byte-p width val1) + (unsigned-byte-p width val2) + (not (b1p (logbit width (+ val1 val2))))) + (< (+ val1 val2) (expt 2 width))) + :hints (("goal" :in-theory (enable unsigned-byte-p) + :use (:instance logbit-1-if-val-gt-expt-2-width + (val (+ val1 val2)))))) + + + +; Suppose val1 and val2 are unsigned-byte-p whose width is w. +; If w'th bit of the sum (+ val1 val2) is set, then +; 2^w < (+ val1 val2). +(defthm plus-unsigned-byte-gt-expt-2-width-if-logbit + (implies (and (unsigned-byte-p width val1) + (unsigned-byte-p width val2) + (b1p (logbit width (+ val1 val2)))) + (<= (expt 2 width) (+ val1 val2))) + :hints (("goal" :in-theory (enable unsigned-byte-p) + :use (:instance logbit-0-if-val-lt-expt-2-width + (val (+ val1 val2)))))) + +; Suppose val1 and val2 are unsigned-byte-p whose width is w. +; If the sum of val1 and val2 does not carry out to w'th bit, +; (loghead w (+ val1 val2)) = (+ val1 val2) +(defthm loghead-unsigned-byte-+-if-not-carry + (implies (and (integerp width) + (<= 0 width) + (unsigned-byte-p width val1) + (unsigned-byte-p width val2) + (not (b1p (logbit width (+ val1 val2))))) + (equal (loghead width (+ val1 val2)) (+ val1 val2))) + :hints (("goal" :in-theory (e/d (loghead) + (bfix)) + :do-not-induct t))) + +(encapsulate nil +(local +(defthm j*k-ge-2*k-if-j-gt-1 + (implies (and (integerp j) + (< 1 j) + (integerp k) + (< 0 k)) + (<= (* 2 k) (* j k))) + :hints (("Goal" :in-theory (enable <-*-right-cancel))) + :rule-classes :linear)) + +; A trivia theorem. +; If y < x < 2*y, then (x mod y) = x - y +(defthm mod-x-y-=-minux-x-y + (implies (and (integerp x) (integerp y) (< 0 y) + (<= y x) (< x (* 2 y))) + (equal (mod x y) (- x y))) + :Hints (("goal" :in-theory (disable (:generalize floor-bounded-by-/))) + ("subgoal 1" :cases ((<= j 1))))) +) + +(in-theory (disable mod-x-y-=-minux-x-y)) + +; Suppose val1 and val2 are unsigned-byte-p whose width is w. +; If the sum of val1 and val2 does not carry out to w'th bit, +; (loghead w (+ val1 val2)) = (+ val1 val2) +(defthm loghead-unsigned-byte-+-if-carry + (implies (and (integerp width) + (<= 0 width) + (unsigned-byte-p width val1) + (unsigned-byte-p width val2) + (b1p (logbit width (+ val1 val2)))) + (equal (loghead width (+ val1 val2)) + (- (+ val1 val2) (expt 2 width)))) + :hints (("goal" :in-theory (enable loghead mod-x-y-=-minux-x-y) + :do-not-induct t))) |