• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
        • 3v-syntax-sexprp
        • Sexpr-rewriting
          • 4v-shannon-expansion
          • Onehot-rewriting
            • 4v-onehot-sexpr-list-prime
            • 4v-onehot-sexpr-prime
            • 4v-onehot-rw-sexpr-alist-aux
            • 4v-onehot-rw-sexpr-alist
            • 4v-onehot-rw-sexpr
            • 4vs-onehot
            • 4vs-ite*-list-dumb
            • 4v-onehot-filter
            • 4v-onehot-list-p
          • 4v-sexpr-restrict-with-rw
          • 4v-sexpr-compose-with-rw
          • Sexpr-rewrite
          • Sexpr-rewrite-default
          • Sexpr-rewriting-internals
          • *sexpr-rewrites*
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Onehot-rewriting

4v-onehot-sexpr-list-prime

Efficiently reduce a list of sexprs under the assumption that some variables are one-hot.

Logically, this function does nothing more than compute 4v-onehot-sexpr-prime for each sexpr in a list.

With mbe we do something tricky for better performance. The real function we execute is basically a wide version of 4v-onehot-sexpr-prime's auxilliary function.

What is this performance hack all about? Our main goal in onehot rewriting is to simplify the update functions of modules that have one-hot inputs. In this context, we have some particular set of variables that we think are one-hot, say A1...An, and a whole list of (related) update functions, represented as the s-expressions S1...Sk.

We want to apply our onehot rewrite on on each of these expressions. The simplest thing to do would be to call 4v-onehot-rw-sexpr on each expression and just cons together the results, as in the logical definition. But if we do this, then we are likely going to miss out on many opportunities to reuse memoized results.

Why? The problem is that each sexpr needs to be restrict/rewritten with a number of alists. Recall that we effectively replace each sexpr with:

(ITE* A1 SEXPR|_{A1=T,A2=NIL,A3=NIL,...AN=NIL)
 (ITE* A2 SEXPR|_{A1=NIL,A2=T,A3=NIL,...AN=NIL}
  ...
   (ITE* AN SEXPR|_{A1=NIL,A2=NIL,A3=NIL,...,AN=T} (X)) ...))

But these alists only depend on the variables Ai, not on the sexprs Si. For better performance, we want to use the same alist to rewrite all of the sexprs at once, since there is presumably a lot of sharing between the update functions. It turns out this optimization is not too bad to implement.

Definitions and Theorems

Function: 4v-onehot-sexpr-list-prime-exec

(defun 4v-onehot-sexpr-list-prime-exec (vars false-bindings sexprs)
  "Returns SEXPRS'"
  (declare (xargs :guard t))
  (b* (((when (atom vars))
        (fast-alist-free false-bindings)
        (replicate (len sexprs) (4vs-x)))
       (var (car vars))
       (bindings (hons-acons var (4vs-t) false-bindings))
       (sexprs/bindings
            (4v-sexpr-restrict-with-rw-list sexprs bindings))
       (- (clear-memoize-table '4v-sexpr-restrict-with-rw))
       (false-bindings (hons-acons var (4vs-f) bindings)))
    (4vs-ite*-list-dumb
         (car vars)
         sexprs/bindings
         (4v-onehot-sexpr-list-prime-exec (cdr vars)
                                          false-bindings sexprs))))

Theorem: alist-equiv-implies-equal-4v-onehot-sexpr-list-prime-exec-2

(defthm alist-equiv-implies-equal-4v-onehot-sexpr-list-prime-exec-2
 (implies
   (alist-equiv false-bindings false-bindings-equiv)
   (equal
        (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs)
        (4v-onehot-sexpr-list-prime-exec
             vars false-bindings-equiv sexprs)))
 :rule-classes (:congruence))

Theorem: len-of-4v-onehot-sexpr-list-prime-exec

(defthm len-of-4v-onehot-sexpr-list-prime-exec
 (equal
  (len (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs))
  (len sexprs)))

Function: 4v-onehot-sexpr-list-prime-aux

(defun 4v-onehot-sexpr-list-prime-aux (vars false-bindings sexprs)
 (declare (xargs :guard t))
 (mbe
  :logic
  (if (atom sexprs)
      nil
   (cons
        (4v-onehot-sexpr-prime-aux vars false-bindings (car sexprs))
        (4v-onehot-sexpr-list-prime-aux
             vars false-bindings (cdr sexprs))))
  :exec
  (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs)))

Theorem: 4v-onehot-sexpr-list-prime-exec-removal

(defthm 4v-onehot-sexpr-list-prime-exec-removal
  (equal
       (4v-onehot-sexpr-list-prime-exec vars false-bindings sexprs)
       (4v-onehot-sexpr-list-prime-aux vars false-bindings sexprs)))

Function: 4v-onehot-sexpr-list-prime

(defun 4v-onehot-sexpr-list-prime (vars sexprs)
  (declare (xargs :guard (and (atom-listp vars)
                              (not (member-equal nil vars)))))
  (mbe :logic
       (if (atom sexprs)
           nil
         (cons (4v-onehot-sexpr-prime vars (car sexprs))
               (4v-onehot-sexpr-list-prime vars (cdr sexprs))))
       :exec (4v-onehot-sexpr-list-prime-aux
                  vars
                  (make-fast-alist (4v-onehot-false-bindings vars))
                  sexprs)))

Theorem: 4v-onehot-sexpr-list-prime-of-take

(defthm 4v-onehot-sexpr-list-prime-of-take
  (implies (<= (nfix n) (len x))
           (equal (4v-onehot-sexpr-list-prime vars (take n x))
                  (take n (4v-onehot-sexpr-list-prime vars x))))
  :rule-classes ((:rewrite)))

Theorem: set-equiv-congruence-over-4v-onehot-sexpr-list-prime

(defthm set-equiv-congruence-over-4v-onehot-sexpr-list-prime
  (implies (set-equiv x y)
           (set-equiv (4v-onehot-sexpr-list-prime vars x)
                      (4v-onehot-sexpr-list-prime vars y)))
  :rule-classes ((:congruence)))

Theorem: subsetp-of-4v-onehot-sexpr-list-prime-when-subsetp

(defthm subsetp-of-4v-onehot-sexpr-list-prime-when-subsetp
  (implies (subsetp x y)
           (subsetp (4v-onehot-sexpr-list-prime vars x)
                    (4v-onehot-sexpr-list-prime vars y)))
  :rule-classes ((:rewrite)))

Theorem: member-of-4v-onehot-sexpr-prime-in-4v-onehot-sexpr-list-prime

(defthm
      member-of-4v-onehot-sexpr-prime-in-4v-onehot-sexpr-list-prime
  (implies (member k x)
           (member (4v-onehot-sexpr-prime vars k)
                   (4v-onehot-sexpr-list-prime vars x)))
  :rule-classes ((:rewrite)))

Theorem: 4v-onehot-sexpr-list-prime-of-rev

(defthm 4v-onehot-sexpr-list-prime-of-rev
  (equal (4v-onehot-sexpr-list-prime vars (rev x))
         (rev (4v-onehot-sexpr-list-prime vars x)))
  :rule-classes ((:rewrite)))

Theorem: 4v-onehot-sexpr-list-prime-of-list-fix

(defthm 4v-onehot-sexpr-list-prime-of-list-fix
  (equal (4v-onehot-sexpr-list-prime vars (list-fix x))
         (4v-onehot-sexpr-list-prime vars x))
  :rule-classes ((:rewrite)))

Theorem: 4v-onehot-sexpr-list-prime-of-append

(defthm 4v-onehot-sexpr-list-prime-of-append
  (equal (4v-onehot-sexpr-list-prime vars (append a b))
         (append (4v-onehot-sexpr-list-prime vars a)
                 (4v-onehot-sexpr-list-prime vars b)))
  :rule-classes ((:rewrite)))

Theorem: cdr-of-4v-onehot-sexpr-list-prime

(defthm cdr-of-4v-onehot-sexpr-list-prime
  (equal (cdr (4v-onehot-sexpr-list-prime vars x))
         (4v-onehot-sexpr-list-prime vars (cdr x)))
  :rule-classes ((:rewrite)))

Theorem: car-of-4v-onehot-sexpr-list-prime

(defthm car-of-4v-onehot-sexpr-list-prime
  (equal (car (4v-onehot-sexpr-list-prime vars x))
         (and (consp x)
              (4v-onehot-sexpr-prime vars (car x))))
  :rule-classes ((:rewrite)))

Theorem: 4v-onehot-sexpr-list-prime-under-iff

(defthm 4v-onehot-sexpr-list-prime-under-iff
  (iff (4v-onehot-sexpr-list-prime vars x)
       (consp x))
  :rule-classes ((:rewrite)))

Theorem: consp-of-4v-onehot-sexpr-list-prime

(defthm consp-of-4v-onehot-sexpr-list-prime
  (equal (consp (4v-onehot-sexpr-list-prime vars x))
         (consp x))
  :rule-classes ((:rewrite)))

Theorem: len-of-4v-onehot-sexpr-list-prime

(defthm len-of-4v-onehot-sexpr-list-prime
  (equal (len (4v-onehot-sexpr-list-prime vars x))
         (len x))
  :rule-classes ((:rewrite)))

Theorem: true-listp-of-4v-onehot-sexpr-list-prime

(defthm true-listp-of-4v-onehot-sexpr-list-prime
  (true-listp (4v-onehot-sexpr-list-prime vars x))
  :rule-classes :type-prescription)

Theorem: 4v-onehot-sexpr-list-prime-when-not-consp

(defthm 4v-onehot-sexpr-list-prime-when-not-consp
  (implies (not (consp x))
           (equal (4v-onehot-sexpr-list-prime vars x)
                  nil))
  :rule-classes ((:rewrite)))

Theorem: 4v-onehot-sexpr-list-prime-of-cons

(defthm 4v-onehot-sexpr-list-prime-of-cons
  (equal (4v-onehot-sexpr-list-prime vars (cons a b))
         (cons (4v-onehot-sexpr-prime vars a)
               (4v-onehot-sexpr-list-prime vars b)))
  :rule-classes ((:rewrite)))

Theorem: 4v-sexpr-vars-list-of-4v-onehot-sexpr-list-prime

(defthm 4v-sexpr-vars-list-of-4v-onehot-sexpr-list-prime
 (implies
  (atom-listp vars)
  (subsetp-equal
       (4v-sexpr-vars-list (4v-onehot-sexpr-list-prime vars sexprs))
       (append vars (4v-sexpr-vars-list sexprs)))))