De Morgan circuit restriction

This module partially evaluates a De Morgan circuit after fixing one input. Every old wire is represented by a Boolean constant or by a possibly-negated wire of the residual circuit. Binary gates made constant, projections, or tautologies are deleted; every other binary gate is retained. The construction tracks the exact number of deleted charged gates.

Restricting a whole program

structure Algebraic.DeMorgan.ProgramRestriction {n g : ℕ} (source : Program signature (n + 1) g) (selected : Fin (n + 1)) (fixedValue : Bool) : Type

Result of restricting a program. deleted records exactly the charged source gates removed by partial evaluation.

• gateCount : ℕ

  Number of residual internal gates, including free materialization gates.

• result : Program signature n self.gateCount

  Residual program on the remaining inputs.

• values : Wire (n + 1) g → ResidualValue n self.gateCount

  Residual constant or signed wire representing every source wire.

• trace_eq (input : Fin n → Bool) (sourceWire : Wire (n + 1) g) : ResidualValue.eval self.result input (self.values sourceWire) = source.trace interpretation ((InputSubstitution.fix selected fixedValue).apply input) sourceWire

  Every represented source wire has the correct restricted semantics.

• selected_eq : self.values (Wire.input selected) = ResidualValue.constant fixedValue

  The selected source input is represented by its fixed Boolean value.

• followsOrigins (sourceWire : Wire (n + 1) g) : self.values sourceWire = (origins source sourceWire).bindWires self.values

  Partial evaluation follows every chain of zero-cost origin gates.

• deleted : Finset (Fin g)

  Charged internal gates deleted during partial evaluation.

• cost_eq : self.deleted.card + Program.cost binaryCost self.result = Program.cost binaryCost source

  Deleted gates account exactly for the charged-cost decrease.

theorem Algebraic.DeMorgan.ProgramRestriction.line_eval {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (restriction : ProgramRestriction source selected fixedValue) (line : Line signature (n + 1) g) (input : Fin n → Bool) : line.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input) (source.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input)) = interpretation line.op fun (argument : Fin (arity line.op)) => ResidualValue.eval restriction.result input (restriction.values (line.wires argument))

Evaluate a source line through a restriction of its preceding program.

theorem Algebraic.DeMorgan.ProgramRestriction.binaryLine_eval {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (restriction : ProgramRestriction source selected fixedValue) (op : BinaryOp) (left right : Wire (n + 1) g) (input : Fin n → Bool) : op.eval (ResidualValue.eval restriction.result input (restriction.values left)) (ResidualValue.eval restriction.result input (restriction.values right)) = (binaryLine op left right).eval interpretation ((InputSubstitution.fix selected fixedValue).apply input) (source.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input))

Evaluation of a binary source line from its residual arguments.

def Algebraic.DeMorgan.ProgramRestriction.empty {n : ℕ} (selected : Fin (n + 1)) (fixedValue : Bool) : ProgramRestriction Program.empty selected fixedValue

Restriction of the empty program.

Equations

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

def Algebraic.DeMorgan.ProgramRestriction.reuseLast {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (prior : ProgramRestriction source selected fixedValue) (line : Line signature (n + 1) g) (value : ResidualValue n prior.gateCount) (value_eq : ∀ (input : Fin n → Bool), ResidualValue.eval prior.result input value = line.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input) (source.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input))) (value_origin_eq : value = (origins (source.gate line) (Wire.gate (Fin.last g))).bindWires (Wire.lastCases value prior.values)) (free : binaryCost line.op = 0) : ProgramRestriction (source.gate line) selected fixedValue

Append a free source gate represented by an existing residual value. No charged gate is added to either the result or the deletion set.

Equations

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

def Algebraic.DeMorgan.ProgramRestriction.deleteLast {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (prior : ProgramRestriction source selected fixedValue) (line : Line signature (n + 1) g) (value : ResidualValue n prior.gateCount) (value_eq : ∀ (input : Fin n → Bool), ResidualValue.eval prior.result input value = line.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input) (source.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input))) (charged : binaryCost line.op = 1) : ProgramRestriction (source.gate line) selected fixedValue

Append a charged source gate whose restricted value is already available. The new source gate is recorded as deleted.

Equations

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

def Algebraic.DeMorgan.ProgramRestriction.retainLast {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (prior : ProgramRestriction source selected fixedValue) (line : Line signature (n + 1) g) {op : BinaryOp} {left right : ResidualValue n prior.gateCount} (retained : RetainedGate prior.result op left right) (output_eq : ∀ (input : Fin n → Bool), retained.result.trace interpretation input retained.output = line.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input) (source.eval interpretation ((InputSubstitution.fix selected fixedValue).apply input))) (charged : binaryCost line.op = 1) : ProgramRestriction (source.gate line) selected fixedValue

Append a charged source gate retained by partial evaluation. The materializer's wire embedding is propagated to all earlier residual values.

Equations

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

noncomputable def Algebraic.DeMorgan.ProgramRestriction.appendBinary {n g : ℕ} {source : Program signature (n + 1) g} {selected : Fin (n + 1)} {fixedValue : Bool} (prior : ProgramRestriction source selected fixedValue) (line : Line signature (n + 1) g) (op : BinaryOp) (leftWire rightWire : Wire (n + 1) g) (line_eq : line = binaryLine op leftWire rightWire) : ProgramRestriction (source.gate line) selected fixedValue

Restrict one charged binary gate after its preceding program.

Equations

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

noncomputable def Algebraic.DeMorgan.restrictProgram {n g : ℕ} (selected : Fin (n + 1)) (fixedValue : Bool) (source : Program signature (n + 1) g) : ProgramRestriction source selected fixedValue

Partial-evaluate every gate of a program after fixing one input.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.DeMorgan.restrictProgram selected fixedValue Cslib.Circuits.Program.empty = Algebraic.DeMorgan.ProgramRestriction.empty selected fixedValue