• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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-aux

Signature

(aliases-bound-fix-aux n aliases) → aliases1

Arguments

n — Guard (natp n).

Returns

aliases1 — Type (lhslist-p aliases1).

Definitions and Theorems

Function: aliases-bound-fix-aux

(defun aliases-bound-fix-aux (n aliases)
 (declare (xargs :stobjs (aliases)))
 (declare (xargs :guard (natp n)))
 (declare (xargs :guard (and (<= n (aliass-length aliases))
                             (aliases-normorderedp-aux n aliases))))
 (let ((__function__ 'aliases-bound-fix-aux))
   (declare (ignorable __function__))
   (if (zp n)
       (aliases-fix aliases)
     (let ((aliases (aliases-bound-fix-aux (1- n) aliases)))
       (set-alias (1- n)
                  (lhs-varbound-fix (1- n)
                                    0 (get-alias (1- n) aliases))
                  aliases)))))

Theorem: lhslist-p-of-aliases-bound-fix-aux

(defthm lhslist-p-of-aliases-bound-fix-aux
  (b* ((aliases1 (aliases-bound-fix-aux n aliases)))
    (lhslist-p aliases1))
  :rule-classes :rewrite)

Theorem: len-of-aliases-bound-fix-aux

(defthm len-of-aliases-bound-fix-aux
  (implies (<= n (len aliases))
           (equal (len (aliases-bound-fix-aux n aliases))
                  (len aliases))))

Theorem: nth-of-aliases-bound-fix-aux

(defthm nth-of-aliases-bound-fix-aux
  (equal (nth m (aliases-bound-fix-aux n aliases))
         (if (< (nfix m) (nfix n))
             (lhs-varbound-fix (nfix m)
                               0 (nth m aliases))
           (lhs-fix (nth m aliases)))))

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

(defthm aliases-normorderedp-aux-of-aliases-bound-fix-aux
  (aliases-normorderedp-aux n (aliases-bound-fix-aux n aliases)))

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

(defthm aliases-bound-fix-aux-when-aliases-normorderedp-aux
  (implies (and (aliases-normorderedp-aux n aliases)
                (<= (nfix n) (len aliases)))
           (equal (aliases-bound-fix-aux n aliases)
                  (lhslist-fix aliases))))

Theorem: aliases-bound-fix-aux-of-nfix-n

(defthm aliases-bound-fix-aux-of-nfix-n
  (equal (aliases-bound-fix-aux (nfix n) aliases)
         (aliases-bound-fix-aux n aliases)))

Theorem: aliases-bound-fix-aux-nat-equiv-congruence-on-n

(defthm aliases-bound-fix-aux-nat-equiv-congruence-on-n
  (implies (nat-equiv n n-equiv)
           (equal (aliases-bound-fix-aux n aliases)
                  (aliases-bound-fix-aux n-equiv aliases)))
  :rule-classes :congruence)

Theorem: aliases-bound-fix-aux-of-lhslist-fix-aliases

(defthm aliases-bound-fix-aux-of-lhslist-fix-aliases
  (equal (aliases-bound-fix-aux n (lhslist-fix aliases))
         (aliases-bound-fix-aux n aliases)))

Theorem: aliases-bound-fix-aux-lhslist-equiv-congruence-on-aliases

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