		Search-engine friendly clone of the ACL2 documentation.

Boolean-xor

Boolean-xor-correctness

Correctness of the circuit.

We need to split into cases based on whether the prime is 2 or not. This is not too surprising, because of the 2 that appears in the constraints, which is the same as 0 if the prime happens to be 2. It turns out that, if the prime is 2, the constraint still works (i.e. it realizes exclusive disjunction); but apparently ACL2 needs to consider this case separately. We also need to enable bitp for this proof to work. We use the prime fields library rules as with other circuits.

The extension to the circuit is boilerplate.

Definitions and Theorems

Theorem: boolean-xor-pred-to-spec

(defthm boolean-xor-pred-to-spec
  (implies (and (primep prime)
                (pfield::fep x prime)
                (pfield::fep y prime)
                (pfield::fep z prime)
                (bitp x)
                (bitp y))
           (equal (boolean-xor-pred x y z prime)
                  (boolean-xor-spec x y z prime))))

Theorem: boolean-xor-circuit-to-spec

(defthm boolean-xor-circuit-to-spec
  (implies
       (and (equal (pfcs::lookup-definition (pfname "boolean_xor")
                                            defs)
                   (boolean-xor-circuit))
            (primep prime)
            (pfield::fep x prime)
            (pfield::fep y prime)
            (pfield::fep z prime)
            (bitp x)
            (bitp y))
       (equal (pfcs::definition-satp (pfname "boolean_xor")
                                     defs (list x y z)
                                     prime)
              (boolean-xor-spec x y z prime))))