Padded circuit satisfiability -- definitions

A query is the canonical pair of a tagged circuit-family code and an arbitrary ruler string. The ruler's contents are ignored; its length fixes the exact assignment width. This prevents a serialized circuit from being interpreted at a different input arity.

def Complexity.CircuitSAT.Witness (query witness : List Bool) : Prop

A witness has exactly the width advertised by the query's ruler and makes the query's tagged circuit code evaluate to true. The query uses canonical pairing syntax; pairLang Witness separately validates its outer pair.

Equations

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

def Complexity.CircuitSAT.language : Language

Tagged circuit codes having a satisfying assignment of the exact width specified by their paired ruler string.

Equations

• Complexity.CircuitSAT.language = {query : List Bool | ∃ (witness : List Bool), Complexity.CircuitSAT.Witness query witness}

def Complexity.CircuitSAT.ExtensionWitness (query witness : List Bool) : Prop

A witness extends the public prefix carried by a query with exactly the number of bits advertised by its ruler, and the combined input makes the tagged circuit code evaluate to true. A query has the canonical shape pair code (pair prefix ruler).

Equations

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

def Complexity.CircuitSAT.extensionLanguage : Language

Tagged circuits having an accepting extension of the exact width specified by the query's ruler.

Equations

• Complexity.CircuitSAT.extensionLanguage = {query : List Bool | ∃ (witness : List Bool), Complexity.CircuitSAT.ExtensionWitness query witness}