• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
        • Alias-normalization
          • Alias-norm.lisp
            • Lhs-alias-canonicalize-replace-top
            • Aliases-bound-fix
            • Lhs-pairs-set-aliases
            • Setalias
            • Lhs-replace-range
            • Lhatom-bound-fix
            • Constraintlist-subst-from-svexarr
            • Aliases-add-pair
            • Lhs-alias-canonicalize-top
            • Lhs-varbound-fix
            • Aliases-bound-fix-aux
            • Canonicalize-alias-pairs
            • Aliases-finish-canonicalize
            • Assigns-subst
            • Aliases-put-pairs
            • Getalias
            • Lhs-alias-norm
            • Constraintlist-subst-from-svexarr-nrev
            • Assigns-subst-nrev
            • Svex-subst-from-svexarr-memo-ok
            • Collect-aliases
            • Aliases-fix
            • Aliases-empty
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
        • Compile.lisp
        • Assign->segment-drivers
        • Segment-driver-map-resolve
        • Assigns->segment-drivers
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Alias-norm.lisp

Lhatom-bound-fix

Signature

(lhatom-bound-fix bound offset x) → xx

Arguments

bound — Guard (integerp bound).

offset — Guard (natp offset).

x — Guard (lhatom-p x).

Returns

xx — Type (and (lhatom-p xx) (lhatom-normorderedp bound offset xx)).

Definitions and Theorems

Function: lhatom-bound-fix

(defun lhatom-bound-fix (bound offset x)
  (declare (xargs :guard (and (integerp bound)
                              (natp offset)
                              (lhatom-p x))))
  (declare (xargs :guard (lhatom-normorderedp bound offset x)))
  (let ((__function__ 'lhatom-bound-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (if (lhatom-normorderedp bound offset x)
             (lhatom-fix x)
           (lhatom-z))
         :exec x)))

Theorem: return-type-of-lhatom-bound-fix

(defthm return-type-of-lhatom-bound-fix
  (b* ((xx (lhatom-bound-fix bound offset x)))
    (and (lhatom-p xx)
         (lhatom-normorderedp bound offset xx)))
  :rule-classes :rewrite)

Theorem: lhatom-bound-fix-of-ifix-bound

(defthm lhatom-bound-fix-of-ifix-bound
  (equal (lhatom-bound-fix (ifix bound) offset x)
         (lhatom-bound-fix bound offset x)))

Theorem: lhatom-bound-fix-int-equiv-congruence-on-bound

(defthm lhatom-bound-fix-int-equiv-congruence-on-bound
  (implies (int-equiv bound bound-equiv)
           (equal (lhatom-bound-fix bound offset x)
                  (lhatom-bound-fix bound-equiv offset x)))
  :rule-classes :congruence)

Theorem: lhatom-bound-fix-of-nfix-offset

(defthm lhatom-bound-fix-of-nfix-offset
  (equal (lhatom-bound-fix bound (nfix offset) x)
         (lhatom-bound-fix bound offset x)))

Theorem: lhatom-bound-fix-nat-equiv-congruence-on-offset

(defthm lhatom-bound-fix-nat-equiv-congruence-on-offset
  (implies (nat-equiv offset offset-equiv)
           (equal (lhatom-bound-fix bound offset x)
                  (lhatom-bound-fix bound offset-equiv x)))
  :rule-classes :congruence)

Theorem: lhatom-bound-fix-of-lhatom-fix-x

(defthm lhatom-bound-fix-of-lhatom-fix-x
  (equal (lhatom-bound-fix bound offset (lhatom-fix x))
         (lhatom-bound-fix bound offset x)))

Theorem: lhatom-bound-fix-lhatom-equiv-congruence-on-x

(defthm lhatom-bound-fix-lhatom-equiv-congruence-on-x
  (implies (lhatom-equiv x x-equiv)
           (equal (lhatom-bound-fix bound offset x)
                  (lhatom-bound-fix bound offset x-equiv)))
  :rule-classes :congruence)

Theorem: lhatom-bound-fix-when-lhatom-normorderedp

(defthm lhatom-bound-fix-when-lhatom-normorderedp
  (implies (lhatom-normorderedp bound offset x)
           (equal (lhatom-bound-fix bound offset x)
                  (lhatom-fix x))))

Theorem: lhatom-bound-fix-forward-to-normorderedp

(defthm lhatom-bound-fix-forward-to-normorderedp
  (lhatom-normorderedp bound
                       idx (lhatom-bound-fix bound idx x))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((lhatom-bound-fix bound idx x)))))

Theorem: lhatom-vars-of-lhatom-bound-fix

(defthm lhatom-vars-of-lhatom-bound-fix
  (implies (not (member v (lhatom-vars x)))
           (not (member v
                        (lhatom-vars (lhatom-bound-fix b o x))))))