Combining shared point flags

Compute valid AND (collision OR occupied) once per point. The two arrays of collision flags and occupancy flags, and the validity array, are supplied as shared subcircuits; their costs are each charged once.

def Algebraic.MassProduction.Nonuniform.MaskedOr.expression {count : ℕ} (index : Fin count) : DeMorgan.Expression (count + count + count)

Two Boolean operations combine the three flags of one point.

Equations

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

def Algebraic.MassProduction.Nonuniform.MaskedOr.combineCircuit (count : ℕ) : Circuit DeMorgan.signature (count + count + count) count

Compile one constant-size expression per point.

Equations

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

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MaskedOr.combineCircuit_size (count : ℕ) : (combineCircuit count).size = ∑ index : Fin count, (expression index).gateCount

The exact gate count of combineCircuit.

theorem Algebraic.MassProduction.Nonuniform.MaskedOr.combineCircuit_eval {count : ℕ} (left right valid : Fin count → Bool) (index : Fin count) : (combineCircuit count).eval DeMorgan.interpretation (Fin.append (Fin.append left right) valid) index = (valid index && (left index || right index))

The combining stage reads the corresponding bits of each shared array.

theorem Algebraic.MassProduction.Nonuniform.MaskedOr.combineCircuit_cost {count : ℕ} : (combineCircuit count).cost DeMorgan.standardCost = 2 * count

Combining costs exactly two gates per point.

def Algebraic.MassProduction.Nonuniform.MaskedOr.circuit {inputs count : ℕ} (left right valid : Circuit DeMorgan.signature inputs count) : Circuit DeMorgan.signature inputs count

Evaluate each shared subcircuit once and combine their pointwise outputs.

Equations

• Algebraic.MassProduction.Nonuniform.MaskedOr.circuit left right valid = (Algebraic.MassProduction.Nonuniform.MaskedOr.combineCircuit count).comp ((left.parallel right).parallel valid)

@[simp]

theorem Algebraic.MassProduction.Nonuniform.MaskedOr.circuit_size {inputs count : ℕ} (left right valid : Circuit DeMorgan.signature inputs count) : (circuit left right valid).size = left.size + right.size + valid.size + (combineCircuit count).size

The exact gate count of circuit.

theorem Algebraic.MassProduction.Nonuniform.MaskedOr.circuit_eval {inputs count : ℕ} (left right valid : Circuit DeMorgan.signature inputs count) (input : Fin inputs → Bool) (index : Fin count) : (circuit left right valid).eval DeMorgan.interpretation input index = (valid.eval DeMorgan.interpretation input index && (left.eval DeMorgan.interpretation input index || right.eval DeMorgan.interpretation input index))

Exact pointwise semantics of the shared composition.

theorem Algebraic.MassProduction.Nonuniform.MaskedOr.circuit_cost {inputs count : ℕ} (left right valid : Circuit DeMorgan.signature inputs count) : (circuit left right valid).cost DeMorgan.standardCost = left.cost DeMorgan.standardCost + right.cost DeMorgan.standardCost + valid.cost DeMorgan.standardCost + 2 * count

Each shared subcircuit is charged once, plus two gates per point.