Residual values for De Morgan circuits

Partial evaluation represents a Boolean value by a constant or a possibly negated wire. This module contains the local Boolean simplifier and the small proof-carrying constructions that realize such values inside a De Morgan program. Whole-program restriction is deliberately kept in a separate module.

inductive Algebraic.DeMorgan.ResidualValue (n g : ℕ) : Type

A Boolean constant or a signed wire in a residual program.

• constant {n g : ℕ} (value : Bool) : ResidualValue n g
• wire {n g : ℕ} (negated : Bool) (wire : Wire n g) : ResidualValue n g

@[instance_reducible]

instance Algebraic.DeMorgan.instDecidableEqResidualValue {n✝ g✝ : ℕ} : DecidableEq (ResidualValue n✝ g✝)

Equations

• Algebraic.DeMorgan.instDecidableEqResidualValue = Algebraic.DeMorgan.instDecidableEqResidualValue.decEq

def Algebraic.DeMorgan.instDecidableEqResidualValue.decEq {n✝ g✝ : ℕ} (x✝ x✝¹ : ResidualValue n✝ g✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.DeMorgan.instDecidableEqResidualValue.decEq (Algebraic.DeMorgan.ResidualValue.constant a) (Algebraic.DeMorgan.ResidualValue.constant b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Algebraic.DeMorgan.instDecidableEqResidualValue.decEq (Algebraic.DeMorgan.ResidualValue.constant value) (Algebraic.DeMorgan.ResidualValue.wire negated wire) = isFalse ⋯
• Algebraic.DeMorgan.instDecidableEqResidualValue.decEq (Algebraic.DeMorgan.ResidualValue.wire negated wire) (Algebraic.DeMorgan.ResidualValue.constant value) = isFalse ⋯

def Algebraic.DeMorgan.ResidualValue.eval {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) : ResidualValue n g → Bool

Evaluate a residual value in a residual program.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.DeMorgan.ResidualValue.eval program input (Algebraic.DeMorgan.ResidualValue.constant value) = value

def Algebraic.DeMorgan.ResidualValue.mapWires {n g h : ℕ} (wireMap : Wire n g → Wire n h) : ResidualValue n g → ResidualValue n h

Transport a residual value through a wire map.

Equations

• Algebraic.DeMorgan.ResidualValue.mapWires wireMap (Algebraic.DeMorgan.ResidualValue.constant value) = Algebraic.DeMorgan.ResidualValue.constant value
• Algebraic.DeMorgan.ResidualValue.mapWires wireMap (Algebraic.DeMorgan.ResidualValue.wire negated residualWire) = Algebraic.DeMorgan.ResidualValue.wire negated (wireMap residualWire)

def Algebraic.DeMorgan.ResidualValue.negate {n g : ℕ} : ResidualValue n g → ResidualValue n g

Boolean negation of a residual value.

Equations

• (Algebraic.DeMorgan.ResidualValue.constant value).negate = Algebraic.DeMorgan.ResidualValue.constant !value
• (Algebraic.DeMorgan.ResidualValue.wire negated residualWire).negate = Algebraic.DeMorgan.ResidualValue.wire (!negated) residualWire

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.negate_negate {n g : ℕ} (value : ResidualValue n g) : value.negate.negate = value

def Algebraic.DeMorgan.ResidualValue.bindWires {n g k h : ℕ} (value : ResidualValue n g) (values : Wire n g → ResidualValue k h) : ResidualValue k h

Replace every wire in a residual value by another residual value. This is the small substitution operation used to state that partial evaluation follows zero-cost origin chains.

Equations

• (Algebraic.DeMorgan.ResidualValue.constant value_1).bindWires values = Algebraic.DeMorgan.ResidualValue.constant value_1
• (Algebraic.DeMorgan.ResidualValue.wire negated residualWire).bindWires values = if negated = true then (values residualWire).negate else values residualWire

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.bindWires_constant {n g k h : ℕ} (values : Wire n g → ResidualValue k h) (value : Bool) : (constant value).bindWires values = constant value

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.bindWires_wire_false {n g k h : ℕ} (values : Wire n g → ResidualValue k h) (wire : Wire n g) : (ResidualValue.wire false wire).bindWires values = values wire

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.bindWires_wire_true {n g k h : ℕ} (values : Wire n g → ResidualValue k h) (wire : Wire n g) : (ResidualValue.wire true wire).bindWires values = (values wire).negate

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.mapWires_negate {n g h : ℕ} (value : ResidualValue n g) (wireMap : Wire n g → Wire n h) : mapWires wireMap value.negate = (mapWires wireMap value).negate

theorem Algebraic.DeMorgan.ResidualValue.mapWires_injective {n g h : ℕ} {wireMap : Wire n g → Wire n h} (injective : Function.Injective wireMap) : Function.Injective fun (value : ResidualValue n g) => mapWires wireMap value

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.bindWires_negate {n g k h : ℕ} (value : ResidualValue n g) (values : Wire n g → ResidualValue k h) : value.negate.bindWires values = (value.bindWires values).negate

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.mapWires_bindWires {n g k h l : ℕ} (value : ResidualValue n g) (values : Wire n g → ResidualValue k h) (wireMap : Wire k h → Wire k l) : mapWires wireMap (value.bindWires values) = value.bindWires fun (wire : Wire n g) => mapWires wireMap (values wire)

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.bindWires_mapWires {n g h k l : ℕ} (value : ResidualValue n g) (wireMap : Wire n g → Wire n h) (values : Wire n h → ResidualValue k l) : (mapWires wireMap value).bindWires values = value.bindWires fun (wire : Wire n g) => values (wireMap wire)

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.eval_constant {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) (value : Bool) : eval program input (constant value) = value

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.eval_wire_false {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) (residualWire : Wire n g) : eval program input (wire false residualWire) = program.trace interpretation input residualWire

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.eval_wire_true {n g : ℕ} (program : Program signature n g) (input : Fin n → Bool) (residualWire : Wire n g) : eval program input (wire true residualWire) = !program.trace interpretation input residualWire

@[simp]

theorem Algebraic.DeMorgan.ResidualValue.eval_negate {n g : ℕ} (value : ResidualValue n g) (program : Program signature n g) (input : Fin n → Bool) : eval program input value.negate = !eval program input value

inductive Algebraic.DeMorgan.BinaryOp : Type

The two charged De Morgan connectives.

• and : BinaryOp
• or : BinaryOp

@[instance_reducible]

instance Algebraic.DeMorgan.instDecidableEqBinaryOp : DecidableEq BinaryOp

Equations

• Algebraic.DeMorgan.instDecidableEqBinaryOp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Algebraic.DeMorgan.BinaryOp.operation : BinaryOp → Op

Operation symbol corresponding to a charged connective.

Equations

• Algebraic.DeMorgan.BinaryOp.and.operation = Algebraic.DeMorgan.Op.and
• Algebraic.DeMorgan.BinaryOp.or.operation = Algebraic.DeMorgan.Op.or

def Algebraic.DeMorgan.BinaryOp.eval : BinaryOp → Bool → Bool → Bool

Boolean semantics of a charged connective.

Equations

• Algebraic.DeMorgan.BinaryOp.and.eval = fun (left right : Bool) => left && right
• Algebraic.DeMorgan.BinaryOp.or.eval = fun (left right : Bool) => left || right

def Algebraic.DeMorgan.BinaryOp.absorbing : BinaryOp → Bool

The value which makes a binary operation independent of its other input.

Equations

• Algebraic.DeMorgan.BinaryOp.and.absorbing = false
• Algebraic.DeMorgan.BinaryOp.or.absorbing = true

def Algebraic.DeMorgan.BinaryOp.inputForSignedAbsorbing (op : BinaryOp) (negated : Bool) : Bool

Source-input value making a possibly-negated literal absorbing.

Equations

• op.inputForSignedAbsorbing negated = if negated = true then !op.absorbing else op.absorbing

@[simp]

theorem Algebraic.DeMorgan.BinaryOp.signed_inputForSignedAbsorbing (op : BinaryOp) (negated : Bool) : (if negated = true then !op.inputForSignedAbsorbing negated else op.inputForSignedAbsorbing negated) = op.absorbing

@[simp]

theorem Algebraic.DeMorgan.BinaryOp.eval_absorbing_right (op : BinaryOp) (left : Bool) : op.eval left op.absorbing = op.absorbing

@[simp]

theorem Algebraic.DeMorgan.BinaryOp.cost_operation (op : BinaryOp) : binaryCost op.operation = 1

def Algebraic.DeMorgan.simplifyBinary {n g : ℕ} (op : BinaryOp) (left right : ResidualValue n g) : Option (ResidualValue n g)

Simplify a binary De Morgan gate. none means both signed inputs are genuinely needed and the charged gate must be retained.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.and (Algebraic.DeMorgan.ResidualValue.constant false) right = some (Algebraic.DeMorgan.ResidualValue.constant false)
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.and left (Algebraic.DeMorgan.ResidualValue.constant false) = some (Algebraic.DeMorgan.ResidualValue.constant false)
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.and (Algebraic.DeMorgan.ResidualValue.constant true) right = some right
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.and left (Algebraic.DeMorgan.ResidualValue.constant true) = some left
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.or (Algebraic.DeMorgan.ResidualValue.constant true) right = some (Algebraic.DeMorgan.ResidualValue.constant true)
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.or left (Algebraic.DeMorgan.ResidualValue.constant true) = some (Algebraic.DeMorgan.ResidualValue.constant true)
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.or (Algebraic.DeMorgan.ResidualValue.constant false) right = some right
• Algebraic.DeMorgan.simplifyBinary Algebraic.DeMorgan.BinaryOp.or left (Algebraic.DeMorgan.ResidualValue.constant false) = some left

theorem Algebraic.DeMorgan.simplifyBinary_and_of_argument_false {n g : ℕ} (values : Fin 2 → ResidualValue n g) (argument : Fin 2) (constant : values argument = ResidualValue.constant false) : simplifyBinary BinaryOp.and (values 0) (values 1) = some (ResidualValue.constant false)

A false argument annihilates an AND gate, in either input position.

theorem Algebraic.DeMorgan.simplifyBinary_or_of_argument_true {n g : ℕ} (values : Fin 2 → ResidualValue n g) (argument : Fin 2) (constant : values argument = ResidualValue.constant true) : simplifyBinary BinaryOp.or (values 0) (values 1) = some (ResidualValue.constant true)

A true argument annihilates an OR gate, in either input position.

theorem Algebraic.DeMorgan.simplifyBinary_of_argument_constant {n g : ℕ} (op : BinaryOp) (values : Fin 2 → ResidualValue n g) (argument : Fin 2) (value : Bool) (constant : values argument = ResidualValue.constant value) : ∃ (result : ResidualValue n g), simplifyBinary op (values 0) (values 1) = some result

Any constant argument makes a binary De Morgan gate simplifiable.

theorem Algebraic.DeMorgan.simplifyBinary_of_common_value {n g : ℕ} (op : BinaryOp) (value : ResidualValue n g) (leftNegated rightNegated : Bool) : ∃ (result : ResidualValue n g), simplifyBinary op (if leftNegated = true then value.negate else value) (if rightNegated = true then value.negate else value) = some result

Two signed forms of one residual value always make a binary gate simplify.

theorem Algebraic.DeMorgan.simplifyBinary_sound {n g : ℕ} {op : BinaryOp} {left right result : ResidualValue n g} (simplifies : simplifyBinary op left right = some result) (program : Program signature n g) (input : Fin n → Bool) : ResidualValue.eval program input result = op.eval (ResidualValue.eval program input left) (ResidualValue.eval program input right)

simplifyBinary preserves the value of a gate whenever it succeeds.

Materialization

def Algebraic.DeMorgan.constantLine {n g : ℕ} (value : Bool) : Line signature n g

A free constant line.

Equations

• Algebraic.DeMorgan.constantLine false = { op := Algebraic.DeMorgan.Op.false, wires := Fin.elim0 }
• Algebraic.DeMorgan.constantLine true = { op := Algebraic.DeMorgan.Op.true, wires := Fin.elim0 }

def Algebraic.DeMorgan.identityLine {n g : ℕ} (sourceWire : Wire n g) : Line signature n g

A free identity line.

Equations

• Algebraic.DeMorgan.identityLine sourceWire = { op := Algebraic.DeMorgan.Op.id, wires := fun (x : Fin (Algebraic.DeMorgan.signature.Arity Algebraic.DeMorgan.Op.id)) => sourceWire }

def Algebraic.DeMorgan.notLine {n g : ℕ} (sourceWire : Wire n g) : Line signature n g

A free negation line.

Equations

• Algebraic.DeMorgan.notLine sourceWire = { op := Algebraic.DeMorgan.Op.not, wires := fun (x : Fin (Algebraic.DeMorgan.signature.Arity Algebraic.DeMorgan.Op.not)) => sourceWire }

def Algebraic.DeMorgan.binaryLine {n g : ℕ} (op : BinaryOp) (left right : Wire n g) : Line signature n g

A charged binary line.

Equations

• Algebraic.DeMorgan.binaryLine Algebraic.DeMorgan.BinaryOp.and left right = { op := Algebraic.DeMorgan.Op.and, wires := fun (i : Fin (1 + 1)) => Fin.cases left (fun (x : Fin 1) => right) i }
• Algebraic.DeMorgan.binaryLine Algebraic.DeMorgan.BinaryOp.or left right = { op := Algebraic.DeMorgan.Op.or, wires := fun (i : Fin (1 + 1)) => Fin.cases left (fun (x : Fin 1) => right) i }

theorem Algebraic.DeMorgan.binaryLine_mapWires {n g h : ℕ} (op : BinaryOp) (left right : Wire n g) (wireMap : Wire n g → Wire n h) : (binaryLine op left right).mapWires wireMap = binaryLine op (wireMap left) (wireMap right)

Mapping the wires of a binary line maps its two named arguments.

theorem Algebraic.DeMorgan.binaryLine_wire_eq_left_or_right {n g : ℕ} (op : BinaryOp) (left right : Wire n g) (argument : Fin (signature.Arity (binaryLine op left right).op)) : (binaryLine op left right).wires argument = left ∨ (binaryLine op left right).wires argument = right

Every argument wire of a binary line is one of its two named inputs.

theorem Algebraic.DeMorgan.andLine_eq_binaryLine {n g : ℕ} (wires : Fin 2 → Wire n g) : { op := Op.and, wires := wires } = binaryLine BinaryOp.and (wires 0) (wires 1)

Every binary AND line is determined by its two arguments.

theorem Algebraic.DeMorgan.orLine_eq_binaryLine {n g : ℕ} (wires : Fin 2 → Wire n g) : { op := Op.or, wires := wires } = binaryLine BinaryOp.or (wires 0) (wires 1)

Every binary OR line is determined by its two arguments.

@[simp]

theorem Algebraic.DeMorgan.constantLine_cost {n g : ℕ} (value : Bool) : binaryCost (constantLine value).op = 0

@[simp]

theorem Algebraic.DeMorgan.identityLine_cost {n g : ℕ} (sourceWire : Wire n g) : binaryCost (identityLine sourceWire).op = 0

@[simp]

theorem Algebraic.DeMorgan.notLine_cost {n g : ℕ} (sourceWire : Wire n g) : binaryCost (notLine sourceWire).op = 0

@[simp]

theorem Algebraic.DeMorgan.binaryLine_cost {n g : ℕ} (op : BinaryOp) (left right : Wire n g) : binaryCost (binaryLine op left right).op = 1

@[simp]

theorem Algebraic.DeMorgan.binaryLine_eval {n g : ℕ} (op : BinaryOp) (left right : Wire n g) (program : Program signature n g) (input : Fin n → Bool) : (binaryLine op left right).eval interpretation input (program.eval interpretation input) = op.eval (program.trace interpretation input left) (program.trace interpretation input right)

@[simp]

theorem Algebraic.DeMorgan.binaryLine_interpretation {n g : ℕ} (op : BinaryOp) (left right : Wire n g) (values : Wire n g → Bool) : (interpretation (binaryLine op left right).op fun (argument : Fin (arity (binaryLine op left right).op)) => values ((binaryLine op left right).wires argument)) = op.eval (values left) (values right)

Applying a binary line to an arbitrary wire valuation reads its two inputs.

theorem Algebraic.DeMorgan.ResidualValue.eval_mapWires {n g h : ℕ} (value : ResidualValue n g) (wireMap : Wire.Renaming n g h) (source : Program signature n g) (result : Program signature n h) (input : Fin n → Bool) (preserves : ∀ (sourceWire : Wire n g), result.trace interpretation input (wireMap.apply sourceWire) = source.trace interpretation input sourceWire) : eval result input (mapWires wireMap.apply value) = eval source input value

structure Algebraic.DeMorgan.Materialization {n g : ℕ} (program : Program signature n g) (value : ResidualValue n g) : Type

Materialize a residual value as a wire, adding only zero-cost gates and embedding every old wire into the extended program.

• gateCount : ℕ

  Gate count of the extended program.

• result : Program signature n self.gateCount

  Extended program.

• embedding : Wire.Renaming n g self.gateCount

  Inclusion of all old wires.

• output : Wire n self.gateCount

  Wire carrying the materialized value.

• embedding_eq (input : Fin n → Bool) (sourceWire : Wire n g) : self.result.trace interpretation input (self.embedding.apply sourceWire) = program.trace interpretation input sourceWire

  The embedding preserves every old wire.

• output_eq (input : Fin n → Bool) : self.result.trace interpretation input self.output = ResidualValue.eval program input value

  The output wire realizes value.

• cost_eq : Program.cost binaryCost self.result = Program.cost binaryCost program

  Materialization has zero charged cost.

def Algebraic.DeMorgan.materialize {n g : ℕ} (program : Program signature n g) (value : ResidualValue n g) : Materialization program value

Materialize a constant or signed wire using at most one free gate.

Equations

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

structure Algebraic.DeMorgan.RetainedGate {n g : ℕ} (program : Program signature n g) (op : BinaryOp) (left right : ResidualValue n g) : Type

Retain a genuinely binary gate after materializing its signed arguments. The extension adds exactly one unit of charged cost.

• gateCount : ℕ

  Gate count of the extended program.

• result : Program signature n self.gateCount

  Extended program ending in the retained charged gate.

• embedding : Wire.Renaming n g self.gateCount

  Inclusion of all old wires.

• output : Wire n self.gateCount

  Output of the retained gate.

• embedding_eq (input : Fin n → Bool) (sourceWire : Wire n g) : self.result.trace interpretation input (self.embedding.apply sourceWire) = program.trace interpretation input sourceWire

  The embedding preserves every old wire.

• output_eq (input : Fin n → Bool) : self.result.trace interpretation input self.output = op.eval (ResidualValue.eval program input left) (ResidualValue.eval program input right)

  The output has the requested binary semantics.

• cost_eq : Program.cost binaryCost self.result = Program.cost binaryCost program + 1

  Retaining the gate adds exactly one unit of charged cost.

def Algebraic.DeMorgan.retainGate {n g : ℕ} (program : Program signature n g) (op : BinaryOp) (left right : ResidualValue n g) : RetainedGate program op left right

Materialize two signed arguments and append their charged gate.

Equations

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