		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Svex-varmasks->a4env

Signature
(svex-varmasks->a4env vars masks boolmasks) → (mv err a4env)
Arguments: vars — Guard (svarlist-p vars).; masks — Guard (svex-mask-alist-p masks).; boolmasks — Guard (svar-boolmasks-p boolmasks).
Returns: err — some mask was negative.
Type (iff err (not (svex-maskbits-ok vars masks))).; a4env — Type (nat-bool-a4env-p! a4env).

Definitions and Theorems

Function: svex-varmasks->a4env

(defun svex-varmasks->a4env (vars masks boolmasks)
  (declare (xargs :guard (and (svarlist-p vars)
                              (svex-mask-alist-p masks)
                              (svar-boolmasks-p boolmasks))))
  (let ((__function__ 'svex-varmasks->a4env))
    (declare (ignorable __function__))
    (b* (((mv err res &)
          (svex-varmasks->a4env-rec vars masks boolmasks 0 nil)))
      (mv err res))))

Theorem: return-type-of-svex-varmasks->a4env.err

(defthm return-type-of-svex-varmasks->a4env.err
  (b* (((mv ?err ?a4env)
        (svex-varmasks->a4env vars masks boolmasks)))
    (iff err
         (not (svex-maskbits-ok vars masks))))
  :rule-classes :rewrite)

Theorem: nat-bool-a4env-p!-of-svex-varmasks->a4env.a4env

(defthm nat-bool-a4env-p!-of-svex-varmasks->a4env.a4env
  (b* (((mv ?err ?a4env)
        (svex-varmasks->a4env vars masks boolmasks)))
    (nat-bool-a4env-p! a4env))
  :rule-classes :rewrite)

Theorem: alist-keys-of-svex-varmasks->a4env

(defthm alist-keys-of-svex-varmasks->a4env
  (b* (((mv ?err ?a4env)
        (svex-varmasks->a4env vars masks boolmasks)))
    (implies (not err)
             (equal (alist-keys a4env)
                    (rev (svarlist-fix vars))))))

Theorem: svex-varmasks->a4env-of-svarlist-fix-vars

(defthm svex-varmasks->a4env-of-svarlist-fix-vars
  (equal (svex-varmasks->a4env (svarlist-fix vars)
                               masks boolmasks)
         (svex-varmasks->a4env vars masks boolmasks)))

Theorem: svex-varmasks->a4env-svarlist-equiv-congruence-on-vars

(defthm svex-varmasks->a4env-svarlist-equiv-congruence-on-vars
 (implies (svarlist-equiv vars vars-equiv)
          (equal (svex-varmasks->a4env vars masks boolmasks)
                 (svex-varmasks->a4env vars-equiv masks boolmasks)))
 :rule-classes :congruence)

Theorem: svex-varmasks->a4env-of-svex-mask-alist-fix-masks

(defthm svex-varmasks->a4env-of-svex-mask-alist-fix-masks
  (equal (svex-varmasks->a4env vars (svex-mask-alist-fix masks)
                               boolmasks)
         (svex-varmasks->a4env vars masks boolmasks)))

Theorem: svex-varmasks->a4env-svex-mask-alist-equiv-congruence-on-masks

(defthm
     svex-varmasks->a4env-svex-mask-alist-equiv-congruence-on-masks
 (implies (svex-mask-alist-equiv masks masks-equiv)
          (equal (svex-varmasks->a4env vars masks boolmasks)
                 (svex-varmasks->a4env vars masks-equiv boolmasks)))
 :rule-classes :congruence)

Theorem: svex-varmasks->a4env-of-svar-boolmasks-fix-boolmasks

(defthm svex-varmasks->a4env-of-svar-boolmasks-fix-boolmasks
  (equal (svex-varmasks->a4env vars
                               masks (svar-boolmasks-fix boolmasks))
         (svex-varmasks->a4env vars masks boolmasks)))

Theorem: svex-varmasks->a4env-svar-boolmasks-equiv-congruence-on-boolmasks

(defthm
  svex-varmasks->a4env-svar-boolmasks-equiv-congruence-on-boolmasks
 (implies (svar-boolmasks-equiv boolmasks boolmasks-equiv)
          (equal (svex-varmasks->a4env vars masks boolmasks)
                 (svex-varmasks->a4env vars masks boolmasks-equiv)))
 :rule-classes :congruence)