• 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
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
          • Rewriting
          • Svex
          • Bit-blasting
            • Svex-focused-equivalence-checking
            • A4vec-operations
            • Svexlist-eval-gl
            • Aig-symbolic-arithmetic
            • Svex-varmasks/env->aig-env-rec
            • Svex-varmasks->a4env-rec
            • Svexlist/env-list-eval-gl
            • 4vmask-to-a4vec-rec-env
            • 4vmask-to-a4vec-rec
            • Svexlist->a4vecs-for-varlist
            • Svex-varmasks/env->aig-env-stats-rec
            • Svexlist->a4vec-nrev
            • A4veclist/svex-env-list-eval
            • A4vec
            • Svexlist-x-out-unused-vars
            • Svex->a4vec-memotable-correctp
            • A4vec/svex-env-eval
            • Svex-varmasks->a4env
            • Svex-varmasks/env->aig-env-rec-log
            • 4vmask-to-a4vec-env
            • 4veclist-from-bitlist-log-rec
            • Svex-apply-aig
            • Svexlist-vars-for-symbolic-eval
            • Nat-bool-a4env-upper-boundp
            • 4vmask-to-a4vec
            • Svexlist/env-list-vars-for-symbolic-eval
            • Svex-maskbits-for-vars
            • Svexlist->a4vec-aig-env-for-varlist
            • 4vec-from-bitlist
            • Svexlist-full-masks-p
            • Svex-varmasks/env->aig-env-stats
            • Svex-varmasks/env->aig-env
            • Svexlistlist->a4vec
            • Svex-const-concat-args
            • Svex-mask-alist-extract-vars
            • Svexlist->a4vec-top
            • Nat-bool-a4vec-upper-boundp
            • Nat-bool-a4env-lower-boundp
            • Maybe-a3vec-fix
            • Svex-maskbits-ok
              • Svex-envlist-check-boolmasks
              • Svex-env-check-boolmasks
              • Nat-bool-list-upper-boundp
              • Nat-bool-a4vec-lower-boundp
              • Maybe-svexlist-rewrite-fixpoint
              • 4vmask-to-a4vec-varcount
              • A4vec-eval
              • Svexlist-nth
              • A4veclist-nth
              • Nat-bool-list-lower-boundp
              • 4veclist-from-bitlist
              • V2i-first-n
              • A4veclist-eval-gl
              • Svex-envlist-keyset
              • Svex-a4vec-env-eval
              • A4veclist/env-list-eval
              • Svexlist-variable-mask-alist
              • Sparseint-nfix
              • A4veclist-length
              • A4veclist-eval
              • 4vec-boolmaskp
              • Nat-bool-list-nats
              • Nat-bool-a4env-p
              • Nat-bool-listp
              • A4veclist->aiglist
              • Svexlist-rewrite-fixpoint-memo
              • Nat-bool-a4vec-p
              • A4vec->aiglist
              • Svex-is-const-concat
              • Nat-bool-a4env-vars
              • Svexlist-mask-alist-memo
              • Nat-bool-a4vec-vars
              • Svexlist-vars-memo
              • A4vec-constantp
              • Svex-aig-memotable
              • Svex-a4vec-env
              • A4veclistlist
              • A4veclist
              • Symbolic-params-x-out-cond
            • Functions
            • 4vmask
            • Why-infinite-width
            • Svex-vars
            • Evaluation
            • Values
          • Symbolic-test-vector
          • Vl-to-svex
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Bit-blasting

    Svex-maskbits-ok

    Signature
    (svex-maskbits-ok vars masks) → *
    Arguments
    vars — Guard (svarlist-p vars).
    masks — Guard (svex-mask-alist-p masks).

    Definitions and Theorems

    Function: svex-maskbits-ok

    (defun svex-maskbits-ok (vars masks)
      (declare (xargs :guard (and (svarlist-p vars)
                                  (svex-mask-alist-p masks))))
      (let ((__function__ 'svex-maskbits-ok))
        (declare (ignorable __function__))
        (b* (((when (atom vars)) t)
             (mask (svex-mask-lookup (svex-var (car vars))
                                     masks))
             ((when (sparseint-< mask 0)) nil))
          (svex-maskbits-ok (cdr vars) masks))))

    Theorem: svex-maskbits-ok-of-svarlist-fix-vars

    (defthm svex-maskbits-ok-of-svarlist-fix-vars
      (equal (svex-maskbits-ok (svarlist-fix vars)
                               masks)
             (svex-maskbits-ok vars masks)))

    Theorem: svex-maskbits-ok-svarlist-equiv-congruence-on-vars

    (defthm svex-maskbits-ok-svarlist-equiv-congruence-on-vars
      (implies (svarlist-equiv vars vars-equiv)
               (equal (svex-maskbits-ok vars masks)
                      (svex-maskbits-ok vars-equiv masks)))
      :rule-classes :congruence)

    Theorem: svex-maskbits-ok-of-svex-mask-alist-fix-masks

    (defthm svex-maskbits-ok-of-svex-mask-alist-fix-masks
      (equal (svex-maskbits-ok vars (svex-mask-alist-fix masks))
             (svex-maskbits-ok vars masks)))

    Theorem: svex-maskbits-ok-svex-mask-alist-equiv-congruence-on-masks

    (defthm svex-maskbits-ok-svex-mask-alist-equiv-congruence-on-masks
      (implies (svex-mask-alist-equiv masks masks-equiv)
               (equal (svex-maskbits-ok vars masks)
                      (svex-maskbits-ok vars masks-equiv)))
      :rule-classes :congruence)