Function:
(defun svtv-1wire->lhs (x modidx moddb aliases) (declare (xargs :stobjs (moddb aliases))) (declare (xargs :guard (and (stringp x) (natp modidx) (moddb-ok moddb)))) (declare (xargs :guard (svtv-mod-alias-guard modidx moddb aliases))) (let ((__function__ 'svtv-1wire->lhs)) (declare (ignorable __function__)) (b* ((x (mbe :logic (str-fix x) :exec x)) ((mv err path range-msb range-lsb) (svtv-parse-path/select x)) ((when err) (mv err nil)) ((mv err wire wireidx bitsel) (moddb-path->wireidx/decl path modidx moddb)) ((when err) (mv (msg "Wire not found: ~s0 -- ~@1" x err) nil)) ((when (and bitsel range-msb)) (mv (msg "Shouldn't have a part-select of a bit-select: ~s0" x) nil)) ((wire wire) wire) (wire-lsb (if wire.revp (+ -1 wire.width wire.low-idx) wire.low-idx)) (wire-msb (if wire.revp wire.low-idx (+ -1 wire.width wire.low-idx))) (range-lsb (if range-msb range-lsb (or bitsel wire-lsb))) (range-msb (or range-msb bitsel wire-msb)) (range-ok (cond (range-msb (if wire.revp (and (<= wire.low-idx range-msb) (<= range-msb range-lsb) (< range-lsb (+ wire.low-idx wire.width))) (and (<= wire.low-idx range-lsb) (<= range-lsb range-msb) (< range-msb (+ wire.low-idx wire.width))))) (bitsel (and (<= wire.low-idx bitsel) (< bitsel (+ wire.low-idx wire.width)))))) ((unless range-ok) (mv (msg "~s0: bit/partselect out of bounds or reversed" x) nil)) (shift (if wire.revp (- wire-lsb range-lsb) (- range-lsb wire-lsb))) (range-width (+ 1 (abs (- range-msb range-lsb)))) (alias (get-alias wireidx aliases))) (mv nil (lhs-concat range-width (lhs-rsh shift alias) nil)))))
Theorem:
(defthm lhs-p-of-svtv-1wire->lhs.lhs (b* (((mv ?err ?lhs) (svtv-1wire->lhs x modidx moddb aliases))) (lhs-p lhs)) :rule-classes :rewrite)
Theorem:
(defthm svtv-1wire->lhs-of-str-fix-x (equal (svtv-1wire->lhs (str-fix x) modidx moddb aliases) (svtv-1wire->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-1wire->lhs-streqv-congruence-on-x (implies (acl2::streqv x x-equiv) (equal (svtv-1wire->lhs x modidx moddb aliases) (svtv-1wire->lhs x-equiv modidx moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-1wire->lhs-of-nfix-modidx (equal (svtv-1wire->lhs x (nfix modidx) moddb aliases) (svtv-1wire->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-1wire->lhs-nat-equiv-congruence-on-modidx (implies (nat-equiv modidx modidx-equiv) (equal (svtv-1wire->lhs x modidx moddb aliases) (svtv-1wire->lhs x modidx-equiv moddb aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-1wire->lhs-of-moddb-fix-moddb (equal (svtv-1wire->lhs x modidx (moddb-fix moddb) aliases) (svtv-1wire->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-1wire->lhs-moddb-equiv-congruence-on-moddb (implies (moddb-equiv moddb moddb-equiv) (equal (svtv-1wire->lhs x modidx moddb aliases) (svtv-1wire->lhs x modidx moddb-equiv aliases))) :rule-classes :congruence)
Theorem:
(defthm svtv-1wire->lhs-of-lhslist-fix-aliases (equal (svtv-1wire->lhs x modidx moddb (lhslist-fix aliases)) (svtv-1wire->lhs x modidx moddb aliases)))
Theorem:
(defthm svtv-1wire->lhs-lhslist-equiv-congruence-on-aliases (implies (lhslist-equiv aliases aliases-equiv) (equal (svtv-1wire->lhs x modidx moddb aliases) (svtv-1wire->lhs x modidx moddb aliases-equiv))) :rule-classes :congruence)