Circuits as certificates

A verifier that guesses a circuit reads it from a certificate of a fixed length. This file fixes such a format for De Morgan circuits with n inputs, one output and at most s gates, of length certLength n s, monotone in the number of inputs (certLength_mono_left). Wire numbers are below w = n + s and are written in unary in fields of w bits (unaryField); an operation takes three bits (Op.bits). A certificate lists the number of gates in a field of s bits, the output wire, and then s rows of 3 + 2 w bits, the first of which hold the gates (certificate).

Every bit string reads as a list of gates and an output wire (readCertificate): a field is read as its number of ones, any three bits as an operation, and the arguments of a gate are cut to the arity of its operation. Reading is polynomial-time (Cslib.Circuits.Boolean.computableInPolyTime_readCertificate), and the certificate of a circuit, followed by any bits, reads as its code (readCertificate_certificate_append). A string that is not the certificate of a circuit may read as gates that read wires not yet computed; the polynomial-time test codeCheck tells the codes of circuits apart (codeCheck_eq_true_iff).

Main definitions

• Cslib.Circuits.Boolean.certLength: the length of certificates.
• Cslib.Circuits.Boolean.certificate: the certificate of a circuit code.
• Cslib.Circuits.Boolean.readCertificate: the gates and the output wire read from a certificate.
• Cslib.Circuits.Boolean.codeCheck: the test for codes of circuits.

Main results

• Cslib.Circuits.Boolean.certLength_mono_left: certificate length is monotone in the input count.
• Cslib.Circuits.Boolean.length_certificate: certificates have length certLength n s.
• Cslib.Circuits.Boolean.readCertificate_certificate_append: a certificate reads as the code of its circuit.
• Cslib.Circuits.Boolean.codeCheck_eq_true_iff: codeCheck tests Program.IsCodeFrom.
• Cslib.Circuits.Boolean.computableInPolyTime_readCertificate, Cslib.Circuits.Boolean.computableInPolyTime_codeCheck: reading certificates and checking codes are polynomial-time.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

Fields and rows

def Cslib.Circuits.Boolean.unaryField (width a : ℕ) : List Bool

The number a in a field of width bits: a ones, then zeros.

@[simp]

theorem Cslib.Circuits.Boolean.length_unaryField (width a : ℕ) (h : a ≤ width) : (unaryField width a).length = width

@[simp]

theorem Cslib.Circuits.Boolean.count_unaryField (width a : ℕ) : List.count true (unaryField width a) = a

def Cslib.Circuits.Boolean.Op.bits : Op → List Bool

An operation in three bits.

@[simp]

theorem Cslib.Circuits.Boolean.Op.length_bits (op : Op) : op.bits.length = 3

def Cslib.Circuits.Boolean.Op.ofBits : Bool × Bool × Bool → Op

The operation read from any three bits.

theorem Cslib.Circuits.Boolean.Op.ofBits_bits (op : Op) : ofBits (op.bits.getD 0 false, op.bits.getD 1 false, op.bits.getD 2 false) = op

def Cslib.Circuits.Boolean.gateRow (width : ℕ) (g : Op × List ℕ) : List Bool

The row of a gate whose wire numbers are below width: its operation, then its first two arguments in fields of width bits.

def Cslib.Circuits.Boolean.readRow (width : ℕ) (row : List Bool) : Op × List ℕ

The gate read from a row of 3 + 2 * width bits, with as many arguments as its operation takes.

theorem Cslib.Circuits.Boolean.length_gateRow {width : ℕ} {g : Op × List ℕ} (h : ∀ i ∈ g.2, i ≤ width) : (gateRow width g).length = 3 + 2 * width

theorem Cslib.Circuits.Boolean.readRow_gateRow {width : ℕ} {g : Op × List ℕ} (harity : g.2.length = signature.Arity g.1) (h : ∀ i ∈ g.2, i ≤ width) : readRow width (gateRow width g) = g

A row reads as its gate, when the gate has the arity of its operation.

Certificates

def Cslib.Circuits.Boolean.certLength (n s : ℕ) : ℕ

The length of the certificates of circuits with n inputs and at most s gates.

theorem Cslib.Circuits.Boolean.certLength_mono_left {m n : ℕ} (h : m ≤ n) (s : ℕ) : certLength m s ≤ certLength n s

Certificate length is monotone in the number of inputs.

def Cslib.Circuits.Boolean.certificate (n s : ℕ) (gates : List (Op × List ℕ)) (output : ℕ) : List Bool

The certificate of a circuit with n inputs and at most s gates, given by its gate list and its output wire: the number of gates and the output wire in fields of s and n + s bits, the rows of the gates, and rows of zeros up to s rows.

def Cslib.Circuits.Boolean.readCertificate (n s : ℕ) (w : List Bool) : List (Op × List ℕ) × ℕ

The gates and the output wire read from a certificate for circuits with n inputs and at most s gates. Every bit string reads as some gates and some wire.

theorem Cslib.Circuits.Boolean.length_readCertificate_le (n s : ℕ) (w : List Bool) : (readCertificate n s w).1.length ≤ s

A certificate reads as at most s gates.

theorem Cslib.Circuits.Boolean.length_certificate {n s : ℕ} {gates : List (Op × List ℕ)} {output : ℕ} (hs : gates.length ≤ s) (houtput : output ≤ n + s) (hgates : ∀ g ∈ gates, ∀ i ∈ g.2, i ≤ n + s) : (certificate n s gates output).length = certLength n s

The certificate of a circuit has length certLength n s.

theorem Cslib.Circuits.Boolean.readCertificate_certificate_append {n s : ℕ} {gates : List (Op × List ℕ)} {output : ℕ} (hcode : Program.IsCodeFrom signature n 0 gates) (hs : gates.length ≤ s) (houtput : output ≤ n + s) (extra : List Bool) : readCertificate n s (certificate n s gates output ++ extra) = (gates, output)

A certificate reads as the code of its circuit, whatever bits follow it.

theorem Cslib.Circuits.Boolean.readCertificate_certificate_code_append {n s : ℕ} (c : Circuit signature n 1) (hs : c.size ≤ s) (extra : List Bool) : readCertificate n s (certificate n s c.code.1 (c.outputs 0).toNat ++ extra) = (c.code.1, (c.outputs 0).toNat)

The certificate of a circuit with at most s gates reads as its code.

theorem Cslib.Circuits.Boolean.length_certificate_code {n s : ℕ} (c : Circuit signature n 1) (hs : c.size ≤ s) : (certificate n s c.code.1 (c.outputs 0).toNat).length = certLength n s

The certificate of a circuit with at most s gates has length certLength n s.

Checking codes

def Cslib.Circuits.Boolean.codeCheck (n : ℕ) (gates : List (Op × List ℕ)) : Bool

Whether a list of gates is the code of a program on n inputs (Program.IsCodeFrom), as a Boolean test: every entry has the arity of its operation and reads only inputs and earlier gates.

theorem Cslib.Circuits.Boolean.codeCheck_eq_true_iff {n : ℕ} {gates : List (Op × List ℕ)} : codeCheck n gates = true ↔ Program.IsCodeFrom signature n 0 gates

Reading certificates in polynomial time

theorem Cslib.Circuits.Boolean.computableInPolyTime_readRow : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool) => readRow p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) encGate

Reading a gate from a row is polynomial-time, for the field width in unary.

theorem Cslib.Circuits.Boolean.computableInPolyTime_codeCheck {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} {gates : γ → List (Op × List ℕ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates encIn (Turing.MultiTapeTM.encList encGate)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => codeCheck (n a) (gates a)) encIn Turing.MultiTapeTM.encBool

Checking that a list of gates is a code is polynomial-time, with the number of inputs in unary.

theorem Cslib.Circuits.Boolean.computableInPolyTime_readCertificate {γ : Type} {encIn : γ ↪ List Bool} {n s : γ → ℕ} {w : γ → List Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => readCertificate (n a) (s a) (w a)) encIn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList encGate) Turing.MultiTapeTM.encNat)

Reading certificates is polynomial-time, for the number of inputs and the number of gates in unary.