Boolean arithmetic in the De Morgan basis

Boolean-ring addition is XOR and multiplication is AND. This module gives a concrete translation from arithmetic circuits over Bool to the manuscript's De Morgan basis. XOR is implemented by

(left OR right) AND NOT (left AND right),

so it costs four standard gates; AND costs one; Boolean constants are free in the weighted model. Composing this translation with the reusable arithmetic expression compiler yields verified De Morgan circuits for Boolean polynomials, together with an exact 4 * additions + multiplications cost.

def Algebraic.DeMorgan.arithmeticGateCount : Arithmetic.Op Bool → ℕ

The number of De Morgan gates simulating each Boolean arithmetic operation.

Equations

• Algebraic.DeMorgan.arithmeticGateCount Algebraic.Arithmetic.Op.add = 4
• Algebraic.DeMorgan.arithmeticGateCount Algebraic.Arithmetic.Op.mul = 1
• Algebraic.DeMorgan.arithmeticGateCount (Algebraic.Arithmetic.Op.constant value) = 1

def Algebraic.DeMorgan.arithmeticOperation (op : Arithmetic.Op Bool) : Circuit signature (Arithmetic.arity op) 1

The De Morgan circuit simulating each Boolean arithmetic operation: exclusive or for addition, conjunction for multiplication, and a constant gate.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algebraic.DeMorgan.arithmeticOperation_size (op : Arithmetic.Op Bool) : (arithmeticOperation op).size = arithmeticGateCount op

The simulation of each Boolean arithmetic operation uses arithmeticGateCount gates.

def Algebraic.DeMorgan.arithmeticTranslation : Translation (Arithmetic.signature Bool) signature

Translate Boolean-ring arithmetic to the De Morgan basis.

Equations

• Algebraic.DeMorgan.arithmeticTranslation = { operation := Algebraic.DeMorgan.arithmeticOperation }

theorem Algebraic.DeMorgan.arithmeticTranslation_pull : arithmeticTranslation.pull interpretation = Arithmetic.nativeInterpretation

The concrete operation circuits have the intended Boolean-ring semantics.

theorem Algebraic.DeMorgan.arithmeticTranslation_pullCost : arithmeticTranslation.pullCost standardCost = Arithmetic.weightedCost 4 1

The pulled-back manuscript cost is exactly four per XOR and one per AND.

def Algebraic.DeMorgan.ArithmeticExpression.finSum {n : ℕ} (count : ℕ) : (Fin count → Arithmetic.Expression Bool n) → Arithmetic.Expression Bool n

XOR a finite family of Boolean-ring expressions. The empty sum is the constant false expression.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.DeMorgan.ArithmeticExpression.finSum 0 x_2 = Algebraic.Arithmetic.Expression.constant false

@[simp]

theorem Algebraic.DeMorgan.ArithmeticExpression.finSum_eval {n : ℕ} (count : ℕ) (terms : Fin count → Arithmetic.Expression Bool n) (input : Fin n → Bool) : Arithmetic.Expression.eval id input (finSum count terms) = ∑ index : Fin count, Arithmetic.Expression.eval id input (terms index)

Evaluation of the expression-level finite sum is Boolean-ring summation.

theorem Algebraic.DeMorgan.ArithmeticExpression.finSum_weightedCost {n : ℕ} (addition multiplication count : ℕ) (terms : Fin count → Arithmetic.Expression Bool n) : Arithmetic.Expression.weightedCost addition multiplication (finSum count terms) = ∑ index : Fin count, Arithmetic.Expression.weightedCost addition multiplication (terms index) + count * addition

Exact weighted expression cost of a finite XOR fold.

def Algebraic.DeMorgan.ArithmeticExpression.circuit {n : ℕ} (expression : Arithmetic.Expression Bool n) : Circuit signature n 1

Compile a Boolean-ring expression into the De Morgan basis.

Equations

• Algebraic.DeMorgan.ArithmeticExpression.circuit expression = Algebraic.DeMorgan.arithmeticTranslation.compile expression.circuit

@[simp]

theorem Algebraic.DeMorgan.ArithmeticExpression.circuit_size {n : ℕ} (expression : Arithmetic.Expression Bool n) : (circuit expression).size = arithmeticTranslation.compiledGateCount expression.circuit

The exact gate count of circuit.

@[simp]

theorem Algebraic.DeMorgan.ArithmeticExpression.circuit_eval {n : ℕ} (expression : Arithmetic.Expression Bool n) (input : Fin n → Bool) : (circuit expression).eval interpretation input 0 = Arithmetic.Expression.eval id input expression

Compiled Boolean expressions have exactly their Boolean-ring semantics.

@[simp]

theorem Algebraic.DeMorgan.ArithmeticExpression.circuit_cost {n : ℕ} (expression : Arithmetic.Expression Bool n) : (circuit expression).cost standardCost = Arithmetic.Expression.weightedCost 4 1 expression

Exact standard De Morgan cost of a compiled Boolean expression.