Definitions for programs with shared gates over the full binary basis

This file holds the definitions behind the bounded-sharing Nechiporuk bounds, so that both the proof internals (Complexitylib.Algebraic.LowerBound.Nechiporuk.Sharing.Internal) and the surface statements (Complexitylib.Algebraic.LowerBound.Nechiporuk.Sharing) can refer to them:

• leaf and gate counts of full-binary-basis formulas (Binary.Formula.gates, occ, inputLeaves, sharedLeaves, inputLeavesIn);
• programs with shared gates (Nechiporuk.SharedProgram), their semantics and size measures, and the per-block measures SharedProgram.activeShared and SharedProgram.activeSharedLeaves, which advance a block through each shared gate with SharedProgram.stepBlock;
• the circuit-side sharing measures sharedFanOut, activeSharedGateCount, activeSharedFanOut, gateBlockSpan, and highSpanSharedFanOut, where a gate is active on a block Y when its syntactic input cone contains a coordinate of Y (gateActive).

def Algebraic.Binary.Formula.gates {N : ℕ} : Formula N → ℕ

The number of binary gates in a formula.

Equations

• (Algebraic.Binary.Formula.var index).gates = 0
• (Algebraic.Binary.Formula.const value).gates = 0
• (Algebraic.Binary.Formula.gate op left right).gates = left.gates + right.gates + 1

def Algebraic.Binary.Formula.occ {N : ℕ} (v : ℕ) : Formula N → ℕ

The number of variable leaves with index v.

Equations

• Algebraic.Binary.Formula.occ v (Algebraic.Binary.Formula.var index) = if ↑index = v then 1 else 0
• Algebraic.Binary.Formula.occ v (Algebraic.Binary.Formula.const value) = 0
• Algebraic.Binary.Formula.occ v (Algebraic.Binary.Formula.gate op left right) = Algebraic.Binary.Formula.occ v left + Algebraic.Binary.Formula.occ v right

def Algebraic.Binary.Formula.inputLeaves {N : ℕ} : Formula N → ℕ → ℕ

The number of variable leaves on the primary input variables 0, …, m - 1.

Equations

• (Algebraic.Binary.Formula.var i).inputLeaves x✝ = if ↑i < x✝ then 1 else 0
• (Algebraic.Binary.Formula.const value).inputLeaves x✝ = 0
• (Algebraic.Binary.Formula.gate op l r).inputLeaves x✝ = l.inputLeaves x✝ + r.inputLeaves x✝

def Algebraic.Binary.Formula.sharedLeaves {N : ℕ} : Formula N → ℕ → ℕ

The number of variable leaves on the shared variables from m on.

Equations

• (Algebraic.Binary.Formula.var i).sharedLeaves x✝ = if x✝ ≤ ↑i then 1 else 0
• (Algebraic.Binary.Formula.const value).sharedLeaves x✝ = 0
• (Algebraic.Binary.Formula.gate op l r).sharedLeaves x✝ = l.sharedLeaves x✝ + r.sharedLeaves x✝

def Algebraic.Binary.Formula.inputLeavesIn {N n : ℕ} (Y : Finset (Fin n)) : Formula N → ℕ

The number of variable leaves on variables below n that belong to Y.

Equations

• Algebraic.Binary.Formula.inputLeavesIn Y (Algebraic.Binary.Formula.var index) = if h : ↑index < n then if ⟨↑index, h⟩ ∈ Y then 1 else 0 else 0
• Algebraic.Binary.Formula.inputLeavesIn Y (Algebraic.Binary.Formula.const value) = 0
• Algebraic.Binary.Formula.inputLeavesIn Y (Algebraic.Binary.Formula.gate op left right) = Algebraic.Binary.Formula.inputLeavesIn Y left + Algebraic.Binary.Formula.inputLeavesIn Y right

inductive Algebraic.Nechiporuk.SharedProgram : ℕ → ℕ → Type

A program on n inputs with k shared gates over the full binary basis: k + 1 binary formulas, where each formula reads the primary inputs and the values of the earlier shared formulas.

• output {n : ℕ} (F : Binary.Formula n) : SharedProgram n 0

  Return a binary formula of the current variables.

• share {n k : ℕ} (G : Binary.Formula n) (P : SharedProgram (n + 1) k) : SharedProgram n (k + 1)

  Compute a shared binary formula and continue with its value as a new last variable.

def Algebraic.Nechiporuk.SharedProgram.eval {n k : ℕ} : SharedProgram n k → (Fin n → Bool) → Bool

Evaluate a binary program with shared gates.

Equations

• (Algebraic.Nechiporuk.SharedProgram.output F).eval x✝ = F.eval x✝
• (Algebraic.Nechiporuk.SharedProgram.share G P).eval x✝ = P.eval (Fin.snoc x✝ (G.eval x✝))

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.eval_output {n : ℕ} (F : Binary.Formula n) (x : Fin n → Bool) : (output F).eval x = F.eval x

A program that only returns F evaluates as F.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.eval_share {n k : ℕ} (G : Binary.Formula n) (P : SharedProgram (n + 1) k) (x : Fin n → Bool) : (share G P).eval x = P.eval (Fin.snoc x (G.eval x))

A shared gate evaluates G and appends its value as the last variable.

def Algebraic.Nechiporuk.SharedProgram.Computes {n k : ℕ} (P : SharedProgram n k) (f : Cslib.BooleanFunction n) : Prop

A program computes f when it agrees with f on every input.

Equations

• P.Computes f = ∀ (x : Fin n → Bool), P.eval x = f x

theorem Algebraic.Nechiporuk.SharedProgram.Computes.eval_eq {n k : ℕ} {P : SharedProgram n k} {f : Cslib.BooleanFunction n} (h : P.Computes f) : P.eval = f

A program computing f has evaluation function f.

def Algebraic.Nechiporuk.SharedProgram.gates {n k : ℕ} : SharedProgram n k → ℕ

The number of binary gates, summed over the formulas of the program.

Equations

• (Algebraic.Nechiporuk.SharedProgram.output F).gates = F.gates
• (Algebraic.Nechiporuk.SharedProgram.share G P).gates = G.gates + P.gates

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.gates_output {n : ℕ} (F : Binary.Formula n) : (output F).gates = F.gates

The gates of an output-only program are those of its formula.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.gates_share {n k : ℕ} (G : Binary.Formula n) (P : SharedProgram (n + 1) k) : (share G P).gates = G.gates + P.gates

The gates of share G P are those of G plus those of P.

def Algebraic.Nechiporuk.SharedProgram.inputLeaves {N k : ℕ} : SharedProgram N k → ℕ → ℕ

The number of variable leaves on the variables 0, …, m - 1, summed over the formulas.

Equations

• (Algebraic.Nechiporuk.SharedProgram.output F).inputLeaves x✝ = F.inputLeaves x✝
• (Algebraic.Nechiporuk.SharedProgram.share G P).inputLeaves x✝ = G.inputLeaves x✝ + P.inputLeaves x✝

def Algebraic.Nechiporuk.SharedProgram.sharedLeaves {N k : ℕ} : SharedProgram N k → ℕ → ℕ

The number of variable leaves on the variables from m on, summed over the formulas.

Equations

• (Algebraic.Nechiporuk.SharedProgram.output F).sharedLeaves x✝ = F.sharedLeaves x✝
• (Algebraic.Nechiporuk.SharedProgram.share G P).sharedLeaves x✝ = G.sharedLeaves x✝ + P.sharedLeaves x✝

def Algebraic.Nechiporuk.SharedProgram.inputLeavesIn {n : ℕ} (Y : Finset (Fin n)) {N k : ℕ} : SharedProgram N k → ℕ

The number of variable leaves on variables below n that lie in Y, summed over the formulas.

Equations

• Algebraic.Nechiporuk.SharedProgram.inputLeavesIn Y (Algebraic.Nechiporuk.SharedProgram.output F) = Algebraic.Binary.Formula.inputLeavesIn Y F
• Algebraic.Nechiporuk.SharedProgram.inputLeavesIn Y (Algebraic.Nechiporuk.SharedProgram.share G P) = Algebraic.Binary.Formula.inputLeavesIn Y G + Algebraic.Nechiporuk.SharedProgram.inputLeavesIn Y P

def Algebraic.Nechiporuk.SharedProgram.occ (v : ℕ) {N k : ℕ} : SharedProgram N k → ℕ

The number of variable leaves with index v, summed over the formulas of the program.

Equations

• Algebraic.Nechiporuk.SharedProgram.occ v (Algebraic.Nechiporuk.SharedProgram.output F) = Algebraic.Binary.Formula.occ v F
• Algebraic.Nechiporuk.SharedProgram.occ v (Algebraic.Nechiporuk.SharedProgram.share G P) = Algebraic.Binary.Formula.occ v G + Algebraic.Nechiporuk.SharedProgram.occ v P

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.occ_output {N : ℕ} (v : ℕ) (F : Binary.Formula N) : occ v (output F) = Binary.Formula.occ v F

Occurrences in an output-only program are those of its formula.

@[simp]

theorem Algebraic.Nechiporuk.SharedProgram.occ_share {N k : ℕ} (v : ℕ) (G : Binary.Formula N) (P : SharedProgram (N + 1) k) : occ v (share G P) = Binary.Formula.occ v G + occ v P

Occurrences in share G P are those of G plus those of P.

def Algebraic.Nechiporuk.SharedProgram.castBlock {N : ℕ} (Y : Finset (Fin N)) : Finset (Fin (N + 1))

Embed a block Y ⊆ Fin N into Fin (N + 1) without including Fin.last N.

Equations

• Algebraic.Nechiporuk.SharedProgram.castBlock Y = Finset.map Fin.castSuccEmb Y

def Algebraic.Nechiporuk.SharedProgram.snocBlock {N : ℕ} (Y : Finset (Fin N)) : Finset (Fin (N + 1))

Extend a block Y ⊆ Fin N to Fin (N + 1) by including the new shared variable Fin.last N.

Equations

• Algebraic.Nechiporuk.SharedProgram.snocBlock Y = insert (Fin.last N) (Finset.map Fin.castSuccEmb Y)

def Algebraic.Nechiporuk.SharedProgram.stepBlock {N : ℕ} (G : Binary.Formula N) (Y : Finset (Fin N)) : Finset (Fin (N + 1))

Advance a block across share G P: include Fin.last N iff G has a leaf in Y.

Equations

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

def Algebraic.Nechiporuk.SharedProgram.leavesIn {N k : ℕ} : SharedProgram N k → Finset (Fin N) → ℕ

The block leaf count of a program on Y when every shared variable is unconditionally added to the block.

Equations

• (Algebraic.Nechiporuk.SharedProgram.output F).leavesIn x✝ = Algebraic.Binary.Formula.leavesIn x✝ F
• (Algebraic.Nechiporuk.SharedProgram.share G P).leavesIn x✝ = Algebraic.Binary.Formula.leavesIn x✝ G + P.leavesIn (Algebraic.Nechiporuk.SharedProgram.snocBlock x✝)

def Algebraic.Nechiporuk.SharedProgram.activeShared {N k : ℕ} : SharedProgram N k → Finset (Fin N) → ℕ

The number of shared gates of P that are active on Y (have at least one leaf in the current active block).

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.Nechiporuk.SharedProgram.output F).activeShared x✝ = 0

def Algebraic.Nechiporuk.SharedProgram.activeLeavesIn {N k : ℕ} : SharedProgram N k → Finset (Fin N) → ℕ

The active leaf count of P on Y, advancing the block via stepBlock at each shared gate.

Equations

• (Algebraic.Nechiporuk.SharedProgram.output F).activeLeavesIn x✝ = Algebraic.Binary.Formula.leavesIn x✝ F
• (Algebraic.Nechiporuk.SharedProgram.share G P).activeLeavesIn x✝ = Algebraic.Binary.Formula.leavesIn x✝ G + P.activeLeavesIn (Algebraic.Nechiporuk.SharedProgram.stepBlock G x✝)

def Algebraic.Nechiporuk.SharedProgram.activeSharedLeaves {N k : ℕ} : SharedProgram N k → Finset (Fin N) → ℕ

The number of shared-variable leaves of P that read shared gates active on Y.

Equations

• One or more equations did not get rendered due to their size.
• (Algebraic.Nechiporuk.SharedProgram.output F).activeSharedLeaves x✝ = 0

Sharing measures of binary circuits

def Algebraic.Nechiporuk.sharedFanOut {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ℕ

The total fan-out of all shared gates (gates of fan-out at least two) of a circuit.

Equations

• Algebraic.Nechiporuk.sharedFanOut c = ∑ g : Fin c.size with 2 ≤ Algebraic.KW.gateFanOut c g, Algebraic.KW.gateFanOut c g

def Algebraic.Nechiporuk.gateActive {σ : Signature} {n : ℕ} (Y : Finset (Fin n)) {t : ℕ} : Program σ n t → Fin t → Bool

Whether gate g of p has at least one input from Y in its syntactic cone.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Nechiporuk.gateActive Y Cslib.Circuits.Program.empty = Fin.elim0

def Algebraic.Nechiporuk.wireActive {σ : Signature} {n : ℕ} (Y : Finset (Fin n)) {t : ℕ} (p : Program σ n t) : Wire n t → Bool

Whether wire w of p has at least one input from Y in its syntactic cone.

Equations

• Algebraic.Nechiporuk.wireActive Y p (Cslib.Circuits.Wire.input i) = decide (i ∈ Y)
• Algebraic.Nechiporuk.wireActive Y p (Cslib.Circuits.Wire.gate g) = Algebraic.Nechiporuk.gateActive Y p g

def Algebraic.Nechiporuk.activeSharedGateCount {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (Y : Finset (Fin n)) : ℕ

The number of shared gates of c whose syntactic cone intersects Y.

Equations

• Algebraic.Nechiporuk.activeSharedGateCount c Y = {g : Fin c.size | 2 ≤ Algebraic.KW.gateFanOut c g ∧ Algebraic.Nechiporuk.gateActive Y c.program g = true}.card

def Algebraic.Nechiporuk.activeSharedFanOut {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (Y : Finset (Fin n)) : ℕ

The total fan-out of the shared gates of c whose syntactic cone intersects Y.

Equations

• Algebraic.Nechiporuk.activeSharedFanOut c Y = ∑ g : Fin c.size with 2 ≤ Algebraic.KW.gateFanOut c g ∧ Algebraic.Nechiporuk.gateActive Y c.program g = true, Algebraic.KW.gateFanOut c g

def Algebraic.Nechiporuk.gateBlockSpan {σ : Signature} {n t B : ℕ} (Y : Fin B → Finset (Fin n)) (p : Program σ n t) (g : Fin t) : ℕ

The number of blocks in Y : Fin B → Finset (Fin n) on which gate g of p is active.

Equations

• Algebraic.Nechiporuk.gateBlockSpan Y p g = {i : Fin B | Algebraic.Nechiporuk.gateActive (Y i) p g = true}.card

def Algebraic.Nechiporuk.highSpanSharedFanOut {σ : Signature} {n m B : ℕ} (c : Circuit σ n m) (Y : Fin B → Finset (Fin n)) (d : ℕ) : ℕ

The total fan-out of the shared gates of c that are active on strictly more than d of the blocks Y.

Equations

• Algebraic.Nechiporuk.highSpanSharedFanOut c Y d = ∑ g : Fin c.size with 2 ≤ Algebraic.KW.gateFanOut c g ∧ d < Algebraic.Nechiporuk.gateBlockSpan Y c.program g, Algebraic.KW.gateFanOut c g