Boolean circuits as data

The circuits of the succinct Cook–Levin theorem (planning/succinct-cook-levin.md, S0; answer_reduction.tex sec:ar-tms): a circuit is a list of gates in topological order, each gate reading input bits or the values of earlier gates, the last gate being the output. Fan-in is at most two by the shape of the gates; fan-out at most two and a terminal output gate are the well-formedness conditions (Circuit.WellFormed) that the arithmetization of the Tseitin formula needs for its individual-degree bound (prop:tseitin-arith-degree). The gate count is the paper's size parameter s. Circuits are first-order data with a SizedEncoding, so that a program of the ambient model can output one (MIPRE.SAT.SuccinctCookLevin.describe).

inductive MIPRE.SAT.Gate : Type

A gate: an input bit, a constant, or a binary/unary gate on the values of earlier gates, named by their positions in the gate list.

• input (i : ℕ) : Gate
• const (b : Bool) : Gate
• and (u v : ℕ) : Gate
• or (u v : ℕ) : Gate
• not (u : ℕ) : Gate

@[instance_reducible]

instance MIPRE.SAT.instDecidableEqGate : DecidableEq Gate

Equations

• MIPRE.SAT.instDecidableEqGate = MIPRE.SAT.instDecidableEqGate.decEq

def MIPRE.SAT.instDecidableEqGate.decEq (x✝ x✝¹ : Gate) : Decidable (x✝ = x✝¹)

Equations

• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.input a) (MIPRE.SAT.Gate.input b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.input i) (MIPRE.SAT.Gate.const b) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.input i) (MIPRE.SAT.Gate.and u v) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.input i) (MIPRE.SAT.Gate.or u v) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.input i) (MIPRE.SAT.Gate.not u) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.const b) (MIPRE.SAT.Gate.input i) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.const a) (MIPRE.SAT.Gate.const b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.const b) (MIPRE.SAT.Gate.and u v) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.const b) (MIPRE.SAT.Gate.or u v) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.const b) (MIPRE.SAT.Gate.not u) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.and u v) (MIPRE.SAT.Gate.input i) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.and u v) (MIPRE.SAT.Gate.const b) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.and a a_1) (MIPRE.SAT.Gate.and b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.and u v) (MIPRE.SAT.Gate.or u_1 v_1) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.and u v) (MIPRE.SAT.Gate.not u_1) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.or u v) (MIPRE.SAT.Gate.input i) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.or u v) (MIPRE.SAT.Gate.const b) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.or u v) (MIPRE.SAT.Gate.and u_1 v_1) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.or a a_1) (MIPRE.SAT.Gate.or b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.or u v) (MIPRE.SAT.Gate.not u_1) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.not u) (MIPRE.SAT.Gate.input i) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.not u) (MIPRE.SAT.Gate.const b) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.not u) (MIPRE.SAT.Gate.and u_1 v) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.not u) (MIPRE.SAT.Gate.or u_1 v) = isFalse ⋯
• MIPRE.SAT.instDecidableEqGate.decEq (MIPRE.SAT.Gate.not a) (MIPRE.SAT.Gate.not b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def MIPRE.SAT.instReprGate.repr : Gate → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MIPRE.SAT.instReprGate : Repr Gate

Equations

• MIPRE.SAT.instReprGate = { reprPrec := MIPRE.SAT.instReprGate.repr }

@[instance_reducible]

instance MIPRE.SAT.instInhabitedGate : Inhabited Gate

Equations

• MIPRE.SAT.instInhabitedGate = { default := MIPRE.SAT.instInhabitedGate.default }

def MIPRE.SAT.Gate.refs : Gate → List ℕ

The gates a gate reads, with multiplicity.

Equations

• (MIPRE.SAT.Gate.input i).refs = []
• (MIPRE.SAT.Gate.const b).refs = []
• (MIPRE.SAT.Gate.and u v).refs = [u, v]
• (MIPRE.SAT.Gate.or u v).refs = [u, v]
• (MIPRE.SAT.Gate.not u).refs = [u]

def MIPRE.SAT.Gate.eval (x : ℕ → Bool) (vals : List Bool) : Gate → Bool

The value of a gate given the input bits x and the values vals of the earlier gates (a missing reference reads false).

Equations

• MIPRE.SAT.Gate.eval x vals (MIPRE.SAT.Gate.input i) = x i
• MIPRE.SAT.Gate.eval x vals (MIPRE.SAT.Gate.const b) = b
• MIPRE.SAT.Gate.eval x vals (MIPRE.SAT.Gate.and u v) = (vals.getD u false && vals.getD v false)
• MIPRE.SAT.Gate.eval x vals (MIPRE.SAT.Gate.or u v) = (vals.getD u false || vals.getD v false)
• MIPRE.SAT.Gate.eval x vals (MIPRE.SAT.Gate.not u) = !vals.getD u false

def MIPRE.SAT.Gate.toData : Gate → Cost.Data

Gates as data: a tag and a payload.

Equations

• (MIPRE.SAT.Gate.input i).toData = (MIPRE.Cost.Data.ofNat 0).cons (MIPRE.Cost.encode i)
• (MIPRE.SAT.Gate.const b).toData = (MIPRE.Cost.Data.ofNat 1).cons (MIPRE.Cost.encode b)
• (MIPRE.SAT.Gate.and u v).toData = (MIPRE.Cost.Data.ofNat 2).cons (MIPRE.Cost.encode (u, v))
• (MIPRE.SAT.Gate.or u v).toData = (MIPRE.Cost.Data.ofNat 3).cons (MIPRE.Cost.encode (u, v))
• (MIPRE.SAT.Gate.not u).toData = (MIPRE.Cost.Data.ofNat 4).cons (MIPRE.Cost.encode u)

def MIPRE.SAT.Gate.ofData? : Cost.Data → Option Gate

Decoding gates.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.SAT.Gate.ofData? MIPRE.Cost.Data.nil = none

theorem MIPRE.SAT.Gate.ofData?_toData (g : Gate) : ofData? g.toData = some g

@[instance_reducible]

instance MIPRE.SAT.Gate.instSizedEncoding : Cost.SizedEncoding Gate

Equations

• MIPRE.SAT.Gate.instSizedEncoding = { encode := MIPRE.SAT.Gate.toData, decode := MIPRE.SAT.Gate.ofData?, decode_encode := MIPRE.SAT.Gate.ofData?_toData }

@[instance_reducible]

instance MIPRE.SAT.instSizedEncodingListGate : Cost.SizedEncoding (List Gate)

A list of gates as data.

Equations

• MIPRE.SAT.instSizedEncodingListGate = { encode := MIPRE.Cost.Data.ofList MIPRE.SAT.Gate.toData, decode := MIPRE.Cost.Data.toList? MIPRE.SAT.Gate.ofData?, decode_encode := ⋯ }

structure MIPRE.SAT.Circuit : Type

A Boolean circuit: inputs input bits and a list of gates in topological order, the last gate being the output.

• inputs : ℕ

  The number of input bits.

• gates : List Gate

  The gates, in an order in which every gate reads only earlier ones.

@[instance_reducible]

instance MIPRE.SAT.instDecidableEqCircuit : DecidableEq Circuit

Equations

• MIPRE.SAT.instDecidableEqCircuit = MIPRE.SAT.instDecidableEqCircuit.decEq

def MIPRE.SAT.instDecidableEqCircuit.decEq (x✝ x✝¹ : Circuit) : Decidable (x✝ = x✝¹)

Equations

• MIPRE.SAT.instDecidableEqCircuit.decEq { inputs := a, gates := a_1 } { inputs := b, gates := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def MIPRE.SAT.instReprCircuit.repr : Circuit → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MIPRE.SAT.instReprCircuit : Repr Circuit

Equations

• MIPRE.SAT.instReprCircuit = { reprPrec := MIPRE.SAT.instReprCircuit.repr }

@[instance_reducible]

instance MIPRE.SAT.instInhabitedCircuit : Inhabited Circuit

Equations

• MIPRE.SAT.instInhabitedCircuit = { default := MIPRE.SAT.instInhabitedCircuit.default }

@[irreducible]

def MIPRE.SAT.Circuit.valueAt (C : Circuit) (x : ℕ → Bool) : ℕ → Bool

The value of gate g of C on the input bits x: the gate evaluated on the values of the earlier gates (a gate beyond the list reads as the constant false).

Equations

• C.valueAt x x✝ = MIPRE.SAT.Gate.eval x (List.ofFn fun (k : Fin x✝) => C.valueAt x ↑k) (C.gates.getD x✝ (MIPRE.SAT.Gate.const false))

def MIPRE.SAT.Circuit.eval (C : Circuit) (x : ℕ → Bool) : Bool

The output of C on the input bits x: the value of the last gate (false for the empty circuit).

Equations

• C.eval x = if C.gates = [] then false else C.valueAt x (C.gates.length - 1)

theorem MIPRE.SAT.Circuit.valueAt_eq (C : Circuit) (x : ℕ → Bool) (g : ℕ) : C.valueAt x g = Gate.eval x (List.ofFn fun (k : Fin g) => C.valueAt x ↑k) (C.gates.getD g (Gate.const false))

def MIPRE.SAT.Circuit.evalBits (C : Circuit) (l : List Bool) : Bool

The output of C on a bit string (missing bits read false).

Equations

• C.evalBits l = C.eval fun (i : ℕ) => l.getD i false

def MIPRE.SAT.Circuit.size (C : Circuit) : ℕ

The number of gates: the paper's size parameter.

Equations

• C.size = C.gates.length

def MIPRE.SAT.Circuit.fanout (C : Circuit) (u : ℕ) : ℕ

The number of wires leaving gate u.

Equations

• C.fanout u = (List.map (fun (g : MIPRE.SAT.Gate) => List.count u g.refs) C.gates).sum

structure MIPRE.SAT.Circuit.WellFormed (C : Circuit) : Prop

Well-formedness (sec:ar-tms): every gate reads earlier gates and existing inputs, fan-out is at most two, the output gate is read by no gate, and there is an output gate.

• refs_lt (k : ℕ) (h : k < C.gates.length) (u : ℕ) : u ∈ C.gates[k].refs → u < k
• inputs_lt (i : ℕ) : Gate.input i ∈ C.gates → i < C.inputs
• fanout_le (u : ℕ) : C.fanout u ≤ 2
• output_terminal : C.fanout (C.gates.length - 1) = 0
• nonempty : C.gates ≠ []

@[instance_reducible]

instance MIPRE.SAT.Circuit.instSizedEncoding : Cost.SizedEncoding Circuit

Circuits as data: the pair of the input count and the gate list.

Equations

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

def MIPRE.SAT.bitsOfNat (m i : ℕ) : List Bool

The m-bit binary encoding of i (least significant bit first; rem:plugging-in-integers).

Equations

• MIPRE.SAT.bitsOfNat m i = List.ofFn fun (k : Fin m) => i.testBit ↑k

@[simp]

theorem MIPRE.SAT.length_bitsOfNat (m i : ℕ) : (bitsOfNat m i).length = m