other
(in-package "AIGNET")
other
(include-book "litp")
other
(include-book "std/util/defmvtypes" :dir :system)
other
(include-book "std/basic/arith-equivs" :dir :system)
other
(include-book "misc/definline" :dir :system)
other
(local (include-book "arithmetic/top-with-meta" :dir :system))
other
(local (include-book "centaur/bitops/ihsext-basics" :dir :system))
other
(defsection snode-accessors
(definlined snode->type
(slot0)
(declare (type (integer 0 *) slot0))
(mbe :logic (logand 3 (lnfix slot0))
:exec (if (<= slot0 4294967295)
(logand 3 (the (unsigned-byte 32) slot0))
(logand 3 slot0))))
(defthm snode->type-natp
(natp (snode->type slot0))
:rule-classes :type-prescription)
(defcong nat-equiv
equal
(snode->type slot)
1
:hints (("Goal" :in-theory (enable snode->type))))
(define snode->type^
((slot0 :type (unsigned-byte 32)))
:inline t
:enabled t
:guard-hints (("goal" :in-theory (enable snode->type)))
(mbe :logic (snode->type slot0)
:exec (logand 3 (the (unsigned-byte 32) slot0))))
(defthm snode->type-bound
(< (snode->type slot0) 4)
:hints (("Goal" :in-theory (enable snode->type)
:expand ((:free (m) (loghead 2 m)) (:free (m) (loghead 1 m))
(:free (m) (loghead 0 m)))))
:rule-classes :linear)
(definlined snode->phase
(slot1)
(declare (type (integer 0 *) slot1))
(mbe :logic (logand 1 (ash (lnfix slot1) -1))
:exec (if (<= slot1 4294967295)
(logand 1
(the (unsigned-byte 32)
(ash (the (unsigned-byte 32) slot1) -1)))
(logand 1 (ash (lnfix slot1) -1)))))
(define snode->phase^
((slot1 :type (unsigned-byte 32)))
:inline t
:enabled t
:guard-hints (("goal" :in-theory (enable snode->phase)))
(mbe :logic (snode->phase slot1)
:exec (logand 1
(the (unsigned-byte 32)
(ash (the (unsigned-byte 32) slot1) -1)))))
(defcong nat-equiv
equal
(snode->phase slot)
1
:hints (("Goal" :in-theory (enable snode->phase))))
(defthm bitp-snode->phase
(bitp (snode->phase slot1))
:hints (("Goal" :in-theory (enable snode->phase))))
(definlined snode->regp
(slot1)
(declare (type (integer 0 *) slot1))
(mbe :logic (logand 1 (lnfix slot1))
:exec (if (<= slot1 4294967295)
(logand 1 (the (unsigned-byte 32) slot1))
(logand 1 (lnfix slot1)))))
(define snode->regp^
((slot1 :type (unsigned-byte 32)))
:inline t
:enabled t
:guard-hints (("goal" :in-theory (enable snode->regp)))
(mbe :logic (snode->regp slot1)
:exec (logand 1 (the (unsigned-byte 32) slot1))))
(defcong nat-equiv
equal
(snode->regp slot)
1
:hints (("Goal" :in-theory (enable snode->regp))))
(defthm bitp-snode->regp
(bitp (snode->regp slot1))
:hints (("Goal" :in-theory (enable snode->regp))))
(definlined snode->fanin
(slot)
(declare (type (integer 0 *) slot))
(mbe :logic (ash (lnfix slot) -2)
:exec (if (<= slot 4294967295)
(ash (the (unsigned-byte 32) slot) -2)
(ash (lnfix slot) -2))))
(define snode->fanin^
((slot :type (unsigned-byte 32)))
:inline t
:enabled t
:guard-hints (("goal" :in-theory (enable snode->fanin)))
(mbe :logic (snode->fanin slot)
:exec (the (unsigned-byte 30)
(ash (the (unsigned-byte 32) slot) -2))))
(defcong nat-equiv
equal
(snode->fanin slot)
1
:hints (("Goal" :in-theory (enable snode->fanin))))
(definlined snode->ionum
(slot1)
(declare (type (integer 0 *) slot1))
(mbe :logic (ash (lnfix slot1) -2)
:exec (if (<= slot1 4294967295)
(ash (the (unsigned-byte 32) slot1) -2)
(ash (lnfix slot1) -2))))
(define snode->ionum^
((slot1 :type (unsigned-byte 32)))
:inline t
:enabled t
:guard-hints (("goal" :in-theory (enable snode->ionum)))
(mbe :logic (snode->ionum slot1)
:exec (the (unsigned-byte 30)
(ash (the (unsigned-byte 32) slot1) -2))))
(defcong nat-equiv
equal
(snode->ionum slot)
1
:hints (("Goal" :in-theory (enable snode->ionum)))))
other
(defsection mk-snode
(definlined mk-snode
(type regp phase fanin0 fanin1)
(declare (type (integer 0 *) fanin0)
(type (integer 0 *) fanin1)
(type (integer 0 3) type)
(type bit regp)
(type bit phase))
(mbe :logic (mv (logior (ash (lnfix fanin0) 2)
(logand 3 type))
(logior (lbfix regp)
(ash (lbfix phase) 1)
(ash (lnfix fanin1) 2)))
:exec (if (and (<= fanin0 1073741823)
(<= fanin1 1073741823))
(mv (logior (the (unsigned-byte 32)
(ash (the (unsigned-byte 30) fanin0) 2))
(the (unsigned-byte 2) type))
(logior (the bit regp)
(the (unsigned-byte 2) (ash (the bit phase) 1))
(the (unsigned-byte 32)
(ash (the (unsigned-byte 30) fanin1) 2))))
(mv (logior (ash (lnfix fanin0) 2) type)
(logior (the bit regp)
(the (unsigned-byte 2) (ash (the bit phase) 1))
(ash (lnfix fanin1) 2))))))
(define mk-snode^
((type (unsigned-byte-p 2 type)
:type (unsigned-byte 2)) (regp bitp :type bit)
(phase bitp :type bit)
(fanin0 (unsigned-byte-p 30 fanin0)
:type (unsigned-byte 30))
(fanin1 (unsigned-byte-p 30 fanin1)
:type (unsigned-byte 30)))
:inline t
:enabled t
:split-types t
:guard-hints (("goal" :in-theory (enable mk-snode)))
(mbe :logic (mk-snode type
regp
phase
fanin0
fanin1)
:exec (mv (the (unsigned-byte 32)
(logior (the (unsigned-byte 32)
(ash (the (unsigned-byte 30) fanin0) 2))
(the (unsigned-byte 2) type)))
(the (unsigned-byte 32)
(logior (the bit regp)
(the (unsigned-byte 2) (ash (the bit phase) 1))
(the (unsigned-byte 32)
(ash (the (unsigned-byte 30) fanin1) 2)))))))
(defmvtypes mk-snode$inline
(natp natp))
(local (in-theory (enable mk-snode)))
(defthm snode->type-of-mk-snode
(equal (snode->type (mv-nth 0
(mk-snode type
regp
phase
fanin0
fanin1)))
(logand 3 type))
:hints (("Goal" :in-theory (enable snode->type))))
(defthm snode->regp-of-mk-snode
(equal (snode->regp (mv-nth 1
(mk-snode type
regp
phase
fanin0
fanin1)))
(bfix regp))
:hints (("Goal" :in-theory (e/d (snode->regp loghead-of-ash)))))
(defthm snode->phase-of-mk-snode
(equal (snode->phase (mv-nth 1
(mk-snode type
regp
phase
fanin0
fanin1)))
(bfix phase))
:hints (("Goal" :in-theory (e/d (snode->phase loghead-of-ash)))))
(defthm snode->fanin-of-mk-snode
(and (equal (snode->fanin (mv-nth 0
(mk-snode type
regp
phase
fanin0
fanin1)))
(nfix fanin0))
(equal (snode->fanin (mv-nth 1
(mk-snode type
regp
phase
fanin0
fanin1)))
(nfix fanin1)))
:hints (("Goal" :in-theory (enable snode->fanin))))
(defthm snode->ionum-of-mk-snode
(equal (snode->ionum (mv-nth 1
(mk-snode type
regp
phase
fanin0
fanin1)))
(nfix fanin1))
:hints (("Goal" :in-theory (enable snode->ionum))))
(defthm normalize-mk-snode-0
(implies (syntaxp (not (and (equal regp ''0)
(equal phase ''0)
(equal fanin1 ''0))))
(equal (mv-nth 0
(mk-snode type
regp
phase
fanin0
fanin1))
(mv-nth 0
(mk-snode type 0 0 fanin0 0)))))
(defthm normalize-mk-snode-1
(implies (syntaxp (not (and (equal fanin0 ''0) (equal type ''0))))
(equal (mv-nth 1
(mk-snode type
regp
phase
fanin0
fanin1))
(mv-nth 1
(mk-snode 0 regp phase 0 fanin1)))))
(defthm unsigned-byte-p-of-mk-snode-0
(and (implies (unsigned-byte-p 30 fanin0)
(unsigned-byte-p 32
(mv-nth 0
(mk-snode type
regp
phase
fanin0
fanin1))))
(implies (unsigned-byte-p 30 fanin1)
(unsigned-byte-p 32
(mv-nth 1
(mk-snode type
regp
phase
fanin0
fanin1)))))))