sizes

(in-package "TRUTH")

(include-book "truth")

(include-book "centaur/fty/bitstruct" :dir :system)

(local (include-book "centaur/bitops/ihsext-basics" :dir :system))

(local (include-book "centaur/bitops/signed-byte-p" :dir :system))

(local (include-book "centaur/bitops/ash-bounds" :dir :system))

(local (include-book "arithmetic/top-with-meta" :dir :system))

(local (include-book "std/basic/arith-equivs" :dir :system))

(local (include-book "centaur/bitops/equal-by-logbitp" :dir :system))

(local (in-theory (disable unsigned-byte-p signed-byte-p)))

(local (add-default-post-define-hook :fix))

(define var-alist
  ((n natp) (numvars natp))
  :guard (<= n numvars)
  (if (zp n)
    nil
    (let ((n (1- n)))
      (cons (cons n (var n numvars))
        (var-alist n numvars)))))

(defun var-cases-fn
  (n numvars)
  (if (zp n)
    nil
    (if (eql n 1)
      `((otherwise ,(TRUTH::VAR 0 TRUTH::NUMVARS)))
      (cons `(,(1- TRUTH::N) ,(TRUTH::VAR (1- TRUTH::N) TRUTH::NUMVARS))
        (var-cases-fn (1- n) numvars)))))

(defmacro var-cases
  (n numvars)
  `(case ,TRUTH::N . ,(TRUTH::VAR-CASES-FN TRUTH::NUMVARS TRUTH::NUMVARS)))

(defun swap-adjacent-case
  (m numvars)
  `(logior (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (logand ,(TRUTH::LOGHEAD (ASH 1 TRUTH::NUMVARS)
  (LOGEQV (TRUTH::VAR TRUTH::M TRUTH::NUMVARS)
          (TRUTH::VAR (+ 1 TRUTH::M) TRUTH::NUMVARS)))
        (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
    (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (ash (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
          (logand ,(LOGAND (TRUTH::VAR (+ 1 TRUTH::M) TRUTH::NUMVARS)
         (LOGNOT (TRUTH::VAR TRUTH::M TRUTH::NUMVARS)))
            (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
        ,(- (ASH 1 TRUTH::M))))
    (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (ash (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
          (logand ,(LOGAND (TRUTH::VAR TRUTH::M TRUTH::NUMVARS)
         (LOGNOT (TRUTH::VAR (+ 1 TRUTH::M) TRUTH::NUMVARS)))
            (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
        ,(ASH 1 TRUTH::M)))))

(defun swap-adjacent-cases-fn
  (m numvars)
  (if (zp m)
    nil
    (cons (list (if (eql m 1)
          'otherwise
          (1- m))
        (swap-adjacent-case (1- m) numvars))
      (swap-adjacent-cases-fn (1- m) numvars))))

(defmacro swap-adjacent-cases
  (numvars)
  `(case m . ,(TRUTH::SWAP-ADJACENT-CASES-FN (1- TRUTH::NUMVARS) TRUTH::NUMVARS)))

(defun swap-vars-case
  (n m numvars)
  `(logior (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (logand ,(TRUTH::LOGHEAD (ASH 1 TRUTH::NUMVARS)
  (LOGEQV (TRUTH::VAR TRUTH::M TRUTH::NUMVARS)
          (TRUTH::VAR TRUTH::N TRUTH::NUMVARS)))
        (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
    (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (ash (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
          (logand ,(LOGAND (TRUTH::VAR TRUTH::N TRUTH::NUMVARS)
         (LOGNOT (TRUTH::VAR TRUTH::M TRUTH::NUMVARS)))
            (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
        ,(- (ASH 1 TRUTH::M) (ASH 1 TRUTH::N))))
    (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (ash (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
          (logand ,(LOGAND (TRUTH::VAR TRUTH::M TRUTH::NUMVARS)
         (LOGNOT (TRUTH::VAR TRUTH::N TRUTH::NUMVARS)))
            (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
        ,(- (ASH 1 TRUTH::N) (ASH 1 TRUTH::M))))))

(defun swap-vars-inner-loop
  (n m numvars)
  (if (zp m)
    nil
    (cons (list (if (eql m 1)
          'otherwise
          (1- m))
        (swap-vars-case n
          (1- m)
          numvars))
      (swap-vars-inner-loop n
        (1- m)
        numvars))))

(defun swap-vars-outer-case
  (n numvars)
  `(case m . ,(TRUTH::SWAP-VARS-INNER-LOOP TRUTH::N TRUTH::N TRUTH::NUMVARS)))

(defun swap-vars-outer-loop
  (n numvars)
  (if (or (zp n) (<= n 2))
    `((otherwise ,(TRUTH::SWAP-VARS-CASE 1 0 TRUTH::NUMVARS)))
    (cons (list (1- n)
        (swap-vars-outer-case (1- n) numvars))
      (swap-vars-outer-loop (1- n) numvars))))

(defmacro swap-vars-cases
  (numvars)
  (if (eql numvars 2)
    (swap-vars-case 1 0 numvars)
    `(case n . ,(TRUTH::SWAP-VARS-OUTER-LOOP TRUTH::NUMVARS TRUTH::NUMVARS))))

(defun swap-polarity-case
  (m numvars)
  `(logior (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (ash (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
          (logand ,(TRUTH::VAR TRUTH::M TRUTH::NUMVARS)
            (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
        ,(- (ASH 1 TRUTH::M))))
    (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS))
      (ash (the (unsigned-byte ,(- (ASH 1 TRUTH::NUMVARS) (ASH 1 TRUTH::M)))
          (logand ,(LOGNOT (TRUTH::VAR TRUTH::M TRUTH::NUMVARS))
            (the (unsigned-byte ,(ASH 1 TRUTH::NUMVARS)) truth)))
        ,(ASH 1 TRUTH::M)))))

(defun swap-polarity-cases-fn
  (m numvars)
  (if (zp m)
    nil
    (cons (list (if (eql m 1)
          'otherwise
          (1- m))
        (swap-polarity-case (1- m) numvars))
      (swap-polarity-cases-fn (1- m) numvars))))

(defmacro swap-polarity-cases
  (numvars)
  `(case m . ,(TRUTH::SWAP-POLARITY-CASES-FN TRUTH::NUMVARS TRUTH::NUMVARS)))

(defun permute-polarity-bindings-fn
  (m numvars)
  (declare (xargs :measure (nfix (- (nfix numvars) (nfix m)))
      :mode :program))
  (if (zp (- (nfix numvars) (nfix m)))
    nil
    (cons `(truth (if (logbitp ,TRUTH::M mask)
          (mbe :logic (swap-polarity ,TRUTH::M
              truth
              ,TRUTH::NUMVARS)
            :exec ,(TRUTH::SWAP-POLARITY-CASE TRUTH::M TRUTH::NUMVARS))
          truth))
      (permute-polarity-bindings-fn (1+ (nfix m))
        numvars))))

(defmacro permute-polarity-bindings
  (numvars)
  `(b* ,(TRUTH::PERMUTE-POLARITY-BINDINGS-FN 0 TRUTH::NUMVARS)
    truth))

(local (defthmd logcdr-when-not-integerp
    (implies (not (integerp x))
      (equal (logcdr x) 0))
    :hints (("Goal" :in-theory (enable logcdr)))))

(local (defthmd logcar-when-not-integerp
    (implies (not (integerp x))
      (equal (logcar x) 0))
    :hints (("Goal" :in-theory (enable logcar)))))

(local (encapsulate nil
    (local (defun ind
        (width a b)
        (if (zp width)
          (list a b)
          (ind (1- width)
            (logcdr a)
            (logcdr b)))))
    (defthm logand-with-unsigned-byte
      (implies (and (unsigned-byte-p width b)
          (syntaxp (and (quotep a) (quotep width)))
          (not (unsigned-byte-p width a)))
        (equal (logand a b)
          (logand (loghead width a) b)))
      :hints (("goal" :induct (ind width a b)
         :in-theory (enable* ihsext-recursive-redefs
           logcar-when-not-integerp
           logcdr-when-not-integerp))))))

(local (defthm unsigned-byte-p-of-1
    (implies (posp m)
      (unsigned-byte-p m 1))
    :hints (("Goal" :in-theory (enable unsigned-byte-p)))))

(local (defthm ash-of-minus-1
    (implies (natp n)
      (equal (ash -1 n) (- (ash 1 n))))
    :hints (("Goal" :in-theory (enable* ihsext-inductions
         ihsext-recursive-redefs
         logcons)))))

(local (defthm ash-by-bound
    (implies (and (< n bound)
        (syntaxp (quotep bound))
        (natp bound)
        (integerp n)
        (<= (ash 1 (- bound 1)) m))
      (<= (ash 1 n) m))
    :hints (("goal" :use ((:instance |(< (ash a b) (ash a c))|
          (a 1)
          (b (- bound 1))
          (c n)))
       :in-theory (disable |(< (ash a b) (ash a c))|)))))

(local (defthm ash-by-bound-neg
    (implies (and (< n bound)
        (syntaxp (quotep bound))
        (natp bound)
        (integerp n)
        (<= m (- (ash 1 (- bound 1)))))
      (<= m (- (ash 1 n))))
    :hints (("goal" :use ((:instance ash-by-bound (m (- m))))
       :in-theory (disable ash-by-bound)))))

(local (defthm ash-1-n-positive
    (implies (natp n)
      (posp (ash 1 n)))
    :rule-classes :type-prescription))

(local (defthm ash-of-logand
    (equal (ash (logand a b) sh)
      (logand (ash a sh) (ash b sh)))
    :hints (("Goal" :in-theory (enable* ihsext-inductions
         ihsext-recursive-redefs)))))

(local (defthm ash-1-monotonic
    (implies (and (< a b)
        (natp a)
        (integerp b))
      (< (ash 1 a) (ash 1 b)))
    :hints (("Goal" :in-theory (enable ash-is-expt-*-x)))
    :rule-classes ((:rewrite) (:linear))))

(local (defthm signed-byte-p-by-unsigned-byte-p
    (implies (unsigned-byte-p (1- w) x)
      (signed-byte-p w x))
    :hints (("Goal" :in-theory (enable unsigned-byte-p signed-byte-p)))))

(local (defthm logcount-of-loghead-+-1
    (implies (natp n)
      (equal (logcount (loghead (+ 1 n) mask))
        (+ (logbit n mask)
          (logcount (loghead n mask)))))
    :hints (("Goal" :in-theory (enable* ihsext-inductions
         ihsext-recursive-redefs)))))

(local (defthm logcount-of-loghead-bound
    (<= (logcount (loghead n x))
      (nfix n))
    :hints (("Goal" :in-theory (enable* ihsext-inductions
         ihsext-recursive-redefs)))
    :rule-classes :linear))

(local (in-theory (disable logior-<-0-linear-2
      logior-<-0-linear-1
      logand->=-0-linear-1
      upper-bound-of-logand
      |(< a (logtail n a))|
      natp-posp
      lognot-<-const
      posp-rw
      posp-redefinition
      ifix-when-not-integerp)))

(local (defthm truth-norm-when-unsigned-byte-p
    (implies (unsigned-byte-p (ash 1 (nfix numvars))
        truth)
      (equal (truth-norm truth numvars)
        truth))
    :hints (("Goal" :in-theory (enable truth-norm)))))

(local (defthmd normalize-logand-neg-with-ash-of-unsigned-byte-lemma
    (implies (and (natp k))
      (equal (logand n
          (ash (loghead m x) k))
        (logand (loghead (+ (nfix m) k)
            n)
          (ash (loghead m x) k))))
    :hints ((logbitp-reasoning))))

(local (defthm normalize-logand-neg-with-ash-of-unsigned-byte
    (implies (and (syntaxp (and (quotep n)
            (quotep k)
            (negp (unquote n))))
        (unsigned-byte-p m x)
        (syntaxp (quotep m))
        (natp k))
      (equal (logand n (ash x k))
        (logand (loghead (+ m k) n)
          (ash x k))))
    :hints (("goal" :use ((:instance normalize-logand-neg-with-ash-of-unsigned-byte-lemma))) (and stable-under-simplificationp
        '(:in-theory (enable unsigned-byte-p))))))

(local (defthmd ash-of-logtail-when-loghead-0
    (implies (and (equal (loghead m n) 0)
        (natp m))
      (equal (ash (logtail m n) m)
        (ifix n)))
    :hints ((logbitp-reasoning))))

(local (defthm normalize-logand-of-ash-to-ash-of-loghead
    (implies (and (syntaxp (and (quotep n) (quotep m)))
        (natp m)
        (equal (loghead m n) 0)
        (logmaskp (ash n (- m))))
      (equal (logand n (ash x m))
        (ash (logand (ash n (- m)) x) m)))
    :hints (("Goal" :in-theory (enable ash-of-logtail-when-loghead-0)))))

(local (defthmd normalize-logand-const-with-loghead-lemma
    (equal (logand (loghead m n)
        (loghead m x))
      (logand (loghead m n) x))
    :hints ((logbitp-reasoning))))

(local (defthm normalize-logand-const-with-loghead
    (implies (and (syntaxp (and (quotep n) (quotep m)))
        (unsigned-byte-p m n))
      (equal (logand n (loghead m x))
        (logand n x)))
    :hints (("goal" :use normalize-logand-const-with-loghead-lemma))))

(local (defun normalize-unsigned-byte-p-neg-const-ind
    (n m x)
    (if (zp n)
      (list m x)
      (normalize-unsigned-byte-p-neg-const-ind (1- n)
        (logcdr m)
        (logcdr x)))))

(local (defthmd normalize-unsigned-byte-p-neg-const-lemma
    (implies (and (unsigned-byte-p (integer-length m) x)
        (equal 0
          (loghead (integer-length m) m)))
      (equal (logand m x) 0))
    :hints (("goal" :induct (logand m x)
       :in-theory (enable* ihsext-recursive-redefs
         ihsext-inductions)
       :expand ((integer-length m))))))

(local (defthm normalize-unsigned-byte-p-neg-const
    (implies (and (syntaxp (and (quotep n) (quotep m)))
        (negp m)
        (unsigned-byte-p (integer-length m) x)
        (unsigned-byte-p n
          (loghead (integer-length m) m)))
      (unsigned-byte-p n (logand m x)))
    :hints (("goal" :induct (normalize-unsigned-byte-p-neg-const-ind n
         m
         x)
       :in-theory (enable* ihsext-recursive-redefs
         normalize-unsigned-byte-p-neg-const-lemma)
       :expand ((integer-length m) (:free (n)
           (unsigned-byte-p (+ 1 n) x)))))))

(local (in-theory (disable (tau-system))))

(progn (defconst *truth-defs*
    '(defsection truth<numvars>
      (defbitstruct truth<numvars> <width>)
      (defthm truth<numvars>-fix-is-truth-norm
        (equal (truth<numvars>-fix x)
          (truth-norm x <numvars>))
        :hints (("Goal" :in-theory (enable truth<numvars>-fix truth-norm))))
      (defthm truth-norm-when-truth<numvars>-p
        (implies (truth<numvars>-p x)
          (equal (truth-norm x <numvars>)
            x))
        :hints (("Goal" :in-theory (enable truth<numvars>-p truth-norm))))
      (defthm truth-norm-under-when-truth<numvars>-equiv
        (truth<numvars>-equiv (truth-norm x <numvars>)
          x)
        :hints (("Goal" :in-theory (enable truth<numvars>-equiv))))
      (defmacro truth<numvars>-fix$
        (x)
        `(mbe :logic (truth-norm ,TRUTH::X <numvars>)
          :exec (truth<numvars>-fix ,TRUTH::X)))
      (deffixtype truth<numvars>
        :pred truth<numvars>-p
        :fix truth<numvars>-fix$
        :equiv truth<numvars>-equiv)
      (deffixcong truth<numvars>-equiv
        equal
        (truth-norm x <numvars>)
        x)
      (local (defthm unsigned-byte-p-when-truth<numvars>-p-forward
          (implies (truth<numvars>-p x)
            (unsigned-byte-p <width> x))
          :rule-classes :forward-chaining))
      (define true<numvars>
        nil
        :inline t
        :enabled t
        (mbe :logic (truth-norm (true) <numvars>)
          :exec <mask>))
      (define truth-eval<numvars>
        ((truth truth<numvars>-p
           :type (unsigned-byte <width>)) (env :type (unsigned-byte <numvars>)))
        :guard (and (unsigned-byte-p <numvars> env))
        :split-types t
        :guard-hints (("goal" :in-theory (enable truth-eval)))
        :enabled t
        :inline t
        (mbe :logic (truth-eval truth env <numvars>)
          :exec (logbitp (the (unsigned-byte <numvars>) env)
            (the (unsigned-byte <width>) truth))))
      (defconst *vars<numvars>*
        (compress1 'vars<numvars>
          (cons '(:header :dimensions (<numvars>)
              :maximum-length <numvars+1>
              :name 'vars<numvars>)
            (var-alist <numvars> <numvars>))))
      (defmacro vars<numvars>
        nil
        (list 'quote *vars<numvars>*))
      (define var<numvars>
        ((n :type (integer 0 <numvars-1>)))
        :guard (and (natp n) (< n <numvars>))
        :split-types t
        :enabled t
        :inline t
        (mbe :logic (var n <numvars>)
          :exec (var-cases n <numvars>)))
      (define truth-norm<numvars>
        ((truth integerp))
        :guard-hints (("goal" :in-theory (enable truth-norm)))
        :enabled t
        :inline t
        (mbe :logic (truth-norm truth <numvars>)
          :exec (logand <mask> truth)))
      (define swap-polarity<numvars>
        ((m :type (integer 0 <numvars-1>)) (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp m) (< m <numvars>))
        :guard-hints (("Goal" :in-theory (enable swap-polarity)))
        :split-types t
        :enabled t
        (:@ :fixnum :inline t)
        (mbe :logic (swap-polarity m
            truth
            <numvars>)
          :exec (swap-polarity-cases <numvars>)))
      (define permute-polarity<numvars>
        ((mask :type (unsigned-byte <numvars>)) (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (unsigned-byte-p <numvars> mask))
        :guard-hints (("Goal" :expand ((:free (a b c)
              (permute-polarity a
                b
                c
                <numvars>)))) (and stable-under-simplificationp
            (let ((lit (car (last clause))))
              (case-match lit
                (('equal ('swap-polarity n truth numvars)
                   &) `(:expand ((swap-polarity ,TRUTH::N
                       ,TRUTH::TRUTH
                       ,TRUTH::NUMVARS))))))))
        :enabled t
        (mbe :logic (permute-polarity 0
            mask
            truth
            <numvars>)
          :exec (permute-polarity-bindings <numvars>)))
      (define positive-cofactor<numvars>
        ((n :type (integer 0 <numvars-1>)) (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n) (< n <numvars>))
        :guard-hints (("Goal" :in-theory (enable positive-cofactor)))
        :split-types t
        :enabled t
        :inline t
        (mbe :logic (positive-cofactor n
            truth
            <numvars>)
          :exec (b* (((the (unsigned-byte <width>) mask) (logand (the (unsigned-byte <width>)
                   (var<numvars> n))
                 (the (unsigned-byte <width>) truth))))
            (logior (the (unsigned-byte <width>) mask)
              (the (unsigned-byte <width>)
                (ash (the (unsigned-byte <width>) mask)
                  (the (integer <-width/2> 0)
                    (ash -1
                      (the (integer 0 <numvars-1>) (lnfix n))))))))))
      (define negative-cofactor<numvars>
        ((n :type (integer 0 <numvars-1>)) (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n) (< n <numvars>))
        :guard-hints (("goal" :in-theory (e/d (negative-cofactor)
             (var-negated-masked-size ash-of-logand))
           :use ((:instance size-of-logand-by-size-of-loghead
              (a truth)
              (b (lognot (var n <numvars>)))
              (m <width>)
              (n (- <width> (ash 1 (nfix n))))) (:instance var-negated-masked-size
               (numvars <numvars>)))))
        :guard-debug t
        :split-types t
        :enabled t
        :inline t
        (mbe :logic (negative-cofactor n
            truth
            <numvars>)
          :exec (b* (((the (unsigned-byte <width>) mask) (logand (the (signed-byte <width+1>)
                   (lognot (the (unsigned-byte <width>)
                       (var<numvars> n))))
                 (the (unsigned-byte <width>) truth))))
            (logior (the (unsigned-byte <width>) mask)
              (the (unsigned-byte <width>)
                (ash (the (unsigned-byte <width-1>) mask)
                  (the (integer 0 <width/2>)
                    (ash (the (unsigned-byte 1) 1)
                      (the (integer 0 <numvars-1>) (lnfix n))))))))))
      (define depends-on<numvars>
        ((n :type (integer 0 <numvars-1>)) (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n) (< n <numvars>))
        :split-types t
        :guard-hints (("goal" :in-theory (enable depends-on truth-norm)))
        :enabled t
        :inline t
        (mbe :logic (depends-on n truth <numvars>)
          :exec (b* ((var (var<numvars> n)))
            (not (eql (the (unsigned-byte <width>)
                  (logand (the (signed-byte <width+1>)
                      (lognot (the (unsigned-byte <width>) var)))
                    (the (unsigned-byte <width>) truth)))
                (the (unsigned-byte <width>)
                  (ash (the (unsigned-byte <width>)
                      (logand (the (unsigned-byte <width>) var)
                        (the (unsigned-byte <width>) truth)))
                    (the (integer <-width/2> 0)
                      (ash -1
                        (the (integer 0 <numvars-1>) (lnfix n)))))))))))
      (define is-xor-with-var<numvars>
        ((n :type (integer 0 <numvars-1>)) (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n) (< n <numvars>))
        :split-types t
        :guard-hints (("goal" :in-theory (enable is-xor-with-var truth-norm)))
        :enabled t
        (mbe :logic (is-xor-with-var n
            truth
            <numvars>)
          :exec (eql (the (unsigned-byte <width>)
              (positive-cofactor<numvars> n truth))
            (truth-norm<numvars> (the (signed-byte <width+1>)
                (lognot (the (unsigned-byte <width>)
                    (negative-cofactor<numvars> n truth))))))))
      (define swap-vars<numvars>
        ((n :type (integer 0 <numvars-1>)) (m :type (integer 0 <numvars-1>))
          (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n)
          (< n <numvars>)
          (natp m)
          (< m <numvars>))
        :guard-hints (("Goal" :in-theory (enable swap-vars swap-vars-aux)))
        :split-types t
        :enabled t
        (mbe :logic (swap-vars n
            m
            truth
            <numvars>)
          :exec (if (eql n m)
            truth
            (mv-let (n m)
              (if (< m n)
                (mv n m)
                (mv m n))
              (swap-vars-cases <numvars>)))))
      (define swap-vars-ordered<numvars>
        ((n :type (integer 0 <numvars-1>)) (m :type (integer 0 <numvars-1>))
          (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n)
          (< n <numvars>)
          (natp m)
          (<= m n))
        :guard-hints (("Goal" :in-theory (enable swap-vars swap-vars-aux)))
        :split-types t
        :enabled t
        (mbe :logic (swap-vars n
            m
            truth
            <numvars>)
          :exec (if (eql n m)
            truth
            (swap-vars-cases <numvars>))))
      (define swap-adjacent-vars<numvars>
        ((m :type (integer 0 <numvars-1>)) (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp m) (< m <numvars-1>))
        :guard-hints (("Goal" :in-theory (enable swap-vars swap-vars-aux)))
        :split-types t
        :enabled t
        (:@ :fixnum :inline t)
        (mbe :logic (swap-vars (+ 1 (nfix m))
            m
            truth
            <numvars>)
          :exec (swap-adjacent-cases <numvars>)))
      (define permute-var-up<numvars>
        ((m :type (integer 0 <numvars-1>)) (n :type (integer 0 <numvars-1>))
          (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp m)
          (natp n)
          (<= m n)
          (< n <numvars>))
        :split-types t
        :enabled t
        :guard-hints (("goal" :expand ((:free (n numvars)
              (permute-var-up m
                n
                truth
                numvars)))
           :in-theory (enable truth-norm
             permute-var-up<numvars>)))
        (mbe :logic (permute-var-up m
            n
            truth
            <numvars>)
          :exec (b* (((when (eql n m)) truth) (next (1+ m))
              (truth (swap-adjacent-vars<numvars> m truth)))
            (permute-var-up<numvars> next
              n
              truth))))
      (define permute-var-down<numvars>
        ((m :type (integer 0 <numvars-1>)) (n :type (integer 0 <numvars-1>))
          (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp m)
          (natp n)
          (<= m n)
          (< n <numvars>))
        :split-types t
        :enabled t
        :guard-hints (("goal" :expand ((:free (n numvars)
              (permute-var-down m
                n
                truth
                numvars)))
           :in-theory (enable truth-norm
             permute-var-down<numvars>)))
        (mbe :logic (permute-var-down m
            n
            truth
            <numvars>)
          :exec (b* (((when (eql n m)) truth) (next (1+ m))
              (truth (permute-var-down<numvars> next
                  n
                  truth)))
            (swap-adjacent-vars<numvars> m truth))))
      (define permute-stretch<numvars>
        ((n :type (integer 0 <numvars>)) (count :type (integer 0 <numvars>))
          (mask :type (unsigned-byte <numvars>))
          (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n)
          (<= n <numvars>)
          (unsigned-byte-p <numvars> mask)
          (equal count
            (logcount (loghead n mask))))
        :guard-hints (("goal" :expand ((:free (count numvars)
              (permute-stretch n
                count
                mask
                truth
                numvars)))
           :in-theory (enable truth-norm
             permute-stretch<numvars>)))
        :split-types t
        :enabled t
        (mbe :logic (permute-stretch n
            count
            mask
            truth
            <numvars>)
          :exec (b* (((when (eql n <numvars>)) truth) (bit (logbit (the (integer 0 <numvars-1>) n)
                  (the (unsigned-byte <numvars>) mask)))
              (truth (permute-stretch<numvars> (1+ n)
                  (+ bit count)
                  mask
                  truth)))
            (if (eql (the bit bit) 1)
              (permute-var-up<numvars> count n truth)
              truth))))
      (define permute-shrink<numvars>
        ((n :type (integer 0 <numvars>)) (count :type (integer 0 <numvars>))
          (mask :type (unsigned-byte <numvars>))
          (truth truth<numvars>-p
            :type (unsigned-byte <width>)))
        :guard (and (natp n)
          (<= n <numvars>)
          (unsigned-byte-p <numvars> mask)
          (equal count
            (logcount (loghead n mask))))
        :guard-hints (("goal" :expand ((:free (count numvars)
              (permute-shrink n
                count
                mask
                truth
                numvars)))
           :in-theory (enable truth-norm
             permute-shrink<numvars>)))
        :split-types t
        :enabled t
        (mbe :logic (permute-shrink n
            count
            mask
            truth
            <numvars>)
          :exec (b* (((when (eql n <numvars>)) truth) (bit (logbit (the (integer 0 <numvars-1>) n)
                  (the (unsigned-byte <numvars>) mask)))
              (truth (if (eql (the bit bit) 1)
                  (permute-var-down<numvars> count
                    n
                    truth)
                  truth)))
            (permute-shrink<numvars> (1+ n)
              (+ bit count)
              mask
              truth))))))
  (defmacro deftruthsize
    (n)
    `(make-event (template-subst *truth-defs*
        :str-alist '(("<NUMVARS>" ,(COERCE (TRUTH::EXPLODE-ATOM TRUTH::N 10) 'STRING) . truthpkg))
        :atom-alist '((<numvars> . ,TRUTH::N) (<numvars-1> . ,(1- TRUTH::N))
          (<numvars+1> . ,(1+ TRUTH::N))
          (<width> . ,(ASH 1 TRUTH::N))
          (<width-1> . ,(1- (ASH 1 TRUTH::N)))
          (<width/2> . ,(ASH 1 (1- TRUTH::N)))
          (<-width/2> . ,(- (ASH 1 (1- TRUTH::N))))
          (<width+1> . ,(1+ (ASH 1 TRUTH::N)))
          (<mask> . ,(1- (ASH 1 (ASH 1 TRUTH::N)))))
        :features ',(AND (< TRUTH::N 6) '(:FIXNUM)))))
  (deftruthsize 6)
  (deftruthsize 5)
  (deftruthsize 4)
  (deftruthsize 3))