• 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

Aliases-bound-fix

Signature

(aliases-bound-fix aliases) → aliases-fix

Arguments

aliases — Guard (aliases-normorderedp aliases).

Returns

aliases-fix — Type (aliases-normorderedp aliases-fix).

Definitions and Theorems

Function: aliases-bound-fix$inline

(defun aliases-bound-fix$inline (aliases)
  (declare (xargs :stobjs (aliases)))
  (declare (xargs :guard (aliases-normorderedp aliases)))
  (let ((__function__ 'aliases-bound-fix))
    (declare (ignorable __function__))
    (mbe :logic (aliases-bound-fix-aux (aliass-length aliases)
                                       aliases)
         :exec (aliases-fix aliases))))

Theorem: aliases-normorderedp-of-aliases-bound-fix

(defthm aliases-normorderedp-of-aliases-bound-fix
  (b* ((aliases-fix (aliases-bound-fix$inline aliases)))
    (aliases-normorderedp aliases-fix))
  :rule-classes :rewrite)

Theorem: nth-of-aliases-bound-fix

(defthm nth-of-aliases-bound-fix
  (equal (nth n (aliases-bound-fix aliases))
         (lhs-varbound-fix (nfix n)
                           0 (nth n aliases))))

Theorem: aliases-bound-fix-when-aliases-normorderedp

(defthm aliases-bound-fix-when-aliases-normorderedp
  (implies (aliases-normorderedp aliases)
           (equal (aliases-bound-fix aliases)
                  aliases)))

Theorem: aliases-bound-fix$inline-of-lhslist-fix-aliases

(defthm aliases-bound-fix$inline-of-lhslist-fix-aliases
  (equal (aliases-bound-fix$inline (lhslist-fix aliases))
         (aliases-bound-fix$inline aliases)))

Theorem: aliases-bound-fix$inline-lhslist-equiv-congruence-on-aliases

(defthm aliases-bound-fix$inline-lhslist-equiv-congruence-on-aliases
  (implies (lhslist-equiv aliases aliases-equiv)
           (equal (aliases-bound-fix$inline aliases)
                  (aliases-bound-fix$inline aliases-equiv)))
  :rule-classes :congruence)

Theorem: len-of-aliases-bound-fix

(defthm len-of-aliases-bound-fix
  (equal (len (aliases-bound-fix aliases))
         (len aliases)))

Function: aliases-equiv

(defun aliases-equiv (x y)
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'aliases-equiv
                                     (list x y))
          (equal (aliases-bound-fix x)
                 (aliases-bound-fix y))))

Theorem: aliases-equiv-is-an-equivalence

(defthm aliases-equiv-is-an-equivalence
  (and (booleanp (aliases-equiv x y))
       (aliases-equiv x x)
       (implies (aliases-equiv x y)
                (aliases-equiv y x))
       (implies (and (aliases-equiv x y)
                     (aliases-equiv y z))
                (aliases-equiv x z)))
  :rule-classes (:equivalence))

Theorem: aliases-equiv-implies-equal-aliases-bound-fix-1

(defthm aliases-equiv-implies-equal-aliases-bound-fix-1
  (implies (aliases-equiv x x-equiv)
           (equal (aliases-bound-fix x)
                  (aliases-bound-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: aliases-bound-fix-under-aliases-equiv

(defthm aliases-bound-fix-under-aliases-equiv
  (aliases-equiv (aliases-bound-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-aliases-bound-fix-1-forward-to-aliases-equiv

(defthm equal-of-aliases-bound-fix-1-forward-to-aliases-equiv
  (implies (equal (aliases-bound-fix x) y)
           (aliases-equiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-aliases-bound-fix-2-forward-to-aliases-equiv

(defthm equal-of-aliases-bound-fix-2-forward-to-aliases-equiv
  (implies (equal x (aliases-bound-fix y))
           (aliases-equiv x y))
  :rule-classes :forward-chaining)

Theorem: aliases-equiv-of-aliases-bound-fix-1-forward

(defthm aliases-equiv-of-aliases-bound-fix-1-forward
  (implies (aliases-equiv (aliases-bound-fix x) y)
           (aliases-equiv x y))
  :rule-classes :forward-chaining)

Theorem: aliases-equiv-of-aliases-bound-fix-2-forward

(defthm aliases-equiv-of-aliases-bound-fix-2-forward
  (implies (aliases-equiv x (aliases-bound-fix y))
           (aliases-equiv x y))
  :rule-classes :forward-chaining)

Theorem: lhslist-equiv-refines-aliases-equiv

(defthm lhslist-equiv-refines-aliases-equiv
  (implies (lhslist-equiv x y)
           (aliases-equiv x y))
  :rule-classes (:refinement))