• 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
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Alias-norm.lisp

Lhs-alias-canonicalize-replace-top

Signature

(lhs-alias-canonicalize-replace-top x aliases) 
  → 
(mv xx aliases1)

Arguments

x — Guard (lhs-p x).

aliases — Guard (aliases-normorderedp aliases).

Returns

xx — Type (and (lhs-p xx) (implies (svarlist-boundedp (lhs-vars x) (len aliases)) (svarlist-boundedp (lhs-vars xx) (len aliases)))) .

aliases1 — Type (and (aliases-normorderedp aliases1) (implies (svarlist-boundedp (lhs-vars x) (len aliases)) (equal (len aliases1) (len aliases)))) .

Definitions and Theorems

Function: lhs-alias-canonicalize-replace-top

(defun lhs-alias-canonicalize-replace-top (x aliases)
  (declare (xargs :stobjs (aliases)))
  (declare (xargs :guard (and (lhs-p x)
                              (aliases-normorderedp aliases))))
  (declare
       (xargs :guard (svarlist-boundedp (lhs-vars x)
                                        (aliass-length aliases))))
  (let ((__function__ 'lhs-alias-canonicalize-replace-top))
    (declare (ignorable __function__))
    (b* (((mv first rest) (lhs-decomp x))
         ((unless first)
          (let ((aliases (aliases-bound-fix aliases)))
            (mv nil aliases)))
         ((lhrange first) first))
      (lhatom-case
           first.atom :z
           (b* (((mv restx aliases)
                 (lhs-alias-canonicalize-replace-top rest aliases)))
             (mv (lhs-cons first restx) aliases))
           :var
           (b* ((idx (svar-index first.atom.name))
                (alias (getalias idx aliases))
                ((mv firstx aliases)
                 (lhs-alias-canonicalize-replace
                      (lhs-rsh first.atom.rsh alias)
                      idx first.w first.atom.rsh aliases))
                ((mv restx aliases)
                 (lhs-alias-canonicalize-replace-top rest aliases)))
             (mv (lhs-concat first.w firstx restx)
                 aliases))))))

Theorem: return-type-of-lhs-alias-canonicalize-replace-top.xx

(defthm return-type-of-lhs-alias-canonicalize-replace-top.xx
  (b* (((mv ?xx ?aliases1)
        (lhs-alias-canonicalize-replace-top x aliases)))
    (and (lhs-p xx)
         (implies (svarlist-boundedp (lhs-vars x)
                                     (len aliases))
                  (svarlist-boundedp (lhs-vars xx)
                                     (len aliases)))))
  :rule-classes :rewrite)

Theorem: return-type-of-lhs-alias-canonicalize-replace-top.aliases1

(defthm return-type-of-lhs-alias-canonicalize-replace-top.aliases1
  (b* (((mv ?xx ?aliases1)
        (lhs-alias-canonicalize-replace-top x aliases)))
    (and (aliases-normorderedp aliases1)
         (implies (svarlist-boundedp (lhs-vars x)
                                     (len aliases))
                  (equal (len aliases1) (len aliases)))))
  :rule-classes :rewrite)

Theorem: len-aliases-of-lhs-alias-canonicalize-replace-top

(defthm len-aliases-of-lhs-alias-canonicalize-replace-top
 (implies
  (svarlist-boundedp (lhs-vars x)
                     (len aliases))
  (equal
       (len (mv-nth 1
                    (lhs-alias-canonicalize-replace-top x aliases)))
       (len aliases))))

Theorem: lhs-alias-canonicalize-replace-top-of-lhs-fix-x

(defthm lhs-alias-canonicalize-replace-top-of-lhs-fix-x
  (equal (lhs-alias-canonicalize-replace-top (lhs-fix x)
                                             aliases)
         (lhs-alias-canonicalize-replace-top x aliases)))

Theorem: lhs-alias-canonicalize-replace-top-lhs-equiv-congruence-on-x

(defthm lhs-alias-canonicalize-replace-top-lhs-equiv-congruence-on-x
  (implies
       (lhs-equiv x x-equiv)
       (equal (lhs-alias-canonicalize-replace-top x aliases)
              (lhs-alias-canonicalize-replace-top x-equiv aliases)))
  :rule-classes :congruence)

Theorem: lhs-alias-canonicalize-replace-top-of-aliases-bound-fix-aliases

(defthm
    lhs-alias-canonicalize-replace-top-of-aliases-bound-fix-aliases
 (equal
  (lhs-alias-canonicalize-replace-top x (aliases-bound-fix aliases))
  (lhs-alias-canonicalize-replace-top x aliases)))

Theorem: lhs-alias-canonicalize-replace-top-aliases-equiv-congruence-on-aliases

(defthm
 lhs-alias-canonicalize-replace-top-aliases-equiv-congruence-on-aliases
 (implies
      (aliases-equiv aliases aliases-equiv)
      (equal (lhs-alias-canonicalize-replace-top x aliases)
             (lhs-alias-canonicalize-replace-top x aliases-equiv)))
 :rule-classes :congruence)