Machine-facing encoding of fan-in-two AND/OR circuits

This file defines a proof-free, on-tape representation of the library's Basis.andOr2 circuits. A raw circuit is an ordered list of gates. For an input arity N, wires 0, ..., N - 1 are primary inputs and gate i produces wire N + i. Thus topological well-formedness says that both references of gate i are strictly less than N + i. The last gate is the sole output.

The evaluator is intentionally iterative. It stores each wire value in an array exactly once, so sharing in the circuit DAG does not cause the recursive recomputation performed by the proof-oriented Circuit.wireValue definition.

The bit format is deterministic and self-delimiting. Naturals use terminated unary (n one-bits followed by a zero-bit), a gate stores three fixed bits and two unary references, and a circuit starts with its unary gate count. Exact decoding rejects truncation and trailing garbage. Unary references make the format polynomially long in the input arity and number of gates; a binary format can be added later without changing the raw circuit semantics.

structure Complexity.CircuitCode.RawGate : Type

A proof-free fan-in-two AND/OR gate.

input₀ and input₁ are absolute wire indices. Negation flags are applied before the AND/OR operation, matching Gate.negated in the typed circuit model.

• op : AndOrOp

  Whether the gate computes AND or OR of its (possibly negated) inputs.

• input₀ : ℕ

  Absolute wire index of the first input.

• input₁ : ℕ

  Absolute wire index of the second input.

• negated₀ : Bool

  Whether the first input value is negated before applying op.

• negated₁ : Bool

  Whether the second input value is negated before applying op.

def Complexity.CircuitCode.instDecidableEqRawGate.decEq (x✝ x✝¹ : RawGate) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.CircuitCode.instDecidableEqRawGate : DecidableEq RawGate

Equations

• Complexity.CircuitCode.instDecidableEqRawGate = Complexity.CircuitCode.instDecidableEqRawGate.decEq

@[reducible, inline]

abbrev Complexity.CircuitCode.RawCircuit : Type

A raw single-output circuit. The output is the value of the last gate.

Equations

• Complexity.CircuitCode.RawCircuit = List Complexity.CircuitCode.RawGate

def Complexity.CircuitCode.RawGate.WellFormedAt (g : RawGate) (available : ℕ) : Prop

Both inputs of a gate must refer to already available wires.

Equations

• g.WellFormedAt available = (g.input₀ < available ∧ g.input₁ < available)

@[implicit_reducible]

instance Complexity.CircuitCode.RawGate.instDecidableWellFormedAt (g : RawGate) (available : ℕ) : Decidable (g.WellFormedAt available)

Equations

• g.instDecidableWellFormedAt available = id inferInstance

def Complexity.CircuitCode.RawGate.isWellFormedAt (g : RawGate) (available : ℕ) : Bool

Boolean checker corresponding to WellFormedAt.

Equations

• g.isWellFormedAt available = decide (g.WellFormedAt available)

def Complexity.CircuitCode.RawGate.eval (g : RawGate) (value₀ value₁ : Bool) : Bool

Evaluate a gate once its two (unnegated) input values are known.

Equations

• g.eval value₀ value₁ = match g.op with | Complexity.AndOrOp.and => (g.negated₀ ^^ value₀) && (g.negated₁ ^^ value₁) | Complexity.AndOrOp.or => g.negated₀ ^^ value₀ || g.negated₁ ^^ value₁

def Complexity.CircuitCode.RawCircuit.TopologicallyWellFormed (N : ℕ) (c : RawCircuit) : Prop

Every gate reference points to a primary input or an earlier gate.

Equations

• Complexity.CircuitCode.RawCircuit.TopologicallyWellFormed N c = ∀ (i : Fin (List.length c)), (List.get c i).WellFormedAt (N + ↑i)

@[implicit_reducible]

instance Complexity.CircuitCode.RawCircuit.instDecidableTopologicallyWellFormed (N : ℕ) (c : RawCircuit) : Decidable (TopologicallyWellFormed N c)

Equations

• Complexity.CircuitCode.RawCircuit.instDecidableTopologicallyWellFormed N c = id Fintype.decidableForallFintype

def Complexity.CircuitCode.RawCircuit.WellFormed (N : ℕ) (c : RawCircuit) : Prop

A valid single-output raw circuit is nonempty and topologically ordered.

Equations

• Complexity.CircuitCode.RawCircuit.WellFormed N c = (c ≠ [] ∧ Complexity.CircuitCode.RawCircuit.TopologicallyWellFormed N c)

@[implicit_reducible]

instance Complexity.CircuitCode.RawCircuit.instDecidableWellFormed (N : ℕ) (c : RawCircuit) : Decidable (WellFormed N c)

Equations

• Complexity.CircuitCode.RawCircuit.instDecidableWellFormed N c = id inferInstance

def Complexity.CircuitCode.RawCircuit.isWellFormed (N : ℕ) (c : RawCircuit) : Bool

Boolean checker for the explicit well-formedness predicate.

Equations

• Complexity.CircuitCode.RawCircuit.isWellFormed N c = decide (Complexity.CircuitCode.RawCircuit.WellFormed N c)

def Complexity.CircuitCode.RawCircuit.evalAux? : RawCircuit → Array Bool → Option (Array Bool)

Evaluate gates in order, appending each result to the memo array.

Failure means that a gate contains a forward or out-of-range reference.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.RawCircuit.evalAux? [] x✝ = some x✝

def Complexity.CircuitCode.RawCircuit.eval? (c : RawCircuit) (input : List Bool) : Option Bool

Evaluate a raw circuit on a list of primary-input values.

The empty gate list has no designated output and is rejected.

Equations

• c.eval? input = if List.isEmpty c = true then none else do let wires ← c.evalAux? input.toArray wires[input.length + List.length c - 1]?

Terminated unary fields

def Complexity.CircuitCode.NatCode.encode (n : ℕ) : List Bool

Self-delimiting unary: n one-bits followed by a zero terminator.

Equations

• Complexity.CircuitCode.NatCode.encode n = List.replicate n true ++ [false]

def Complexity.CircuitCode.NatCode.decodeAux? : List Bool → ℕ → Option (ℕ × List Bool)

Parse one terminated-unary prefix, returning the unconsumed suffix.

Equations

• Complexity.CircuitCode.NatCode.decodeAux? [] x✝ = none
• Complexity.CircuitCode.NatCode.decodeAux? (false :: rest) x✝ = some (x✝, rest)
• Complexity.CircuitCode.NatCode.decodeAux? (true :: rest) x✝ = Complexity.CircuitCode.NatCode.decodeAux? rest (x✝ + 1)

def Complexity.CircuitCode.NatCode.decodePrefix? (bits : List Bool) : Option (ℕ × List Bool)

Parse one terminated-unary prefix.

Equations

• Complexity.CircuitCode.NatCode.decodePrefix? bits = Complexity.CircuitCode.NatCode.decodeAux? bits 0

Gate serialization

def Complexity.CircuitCode.RawGate.opBit (g : RawGate) : Bool

Operation bit: one is AND and zero is OR.

Equations

• g.opBit = match g.op with | Complexity.AndOrOp.and => true | Complexity.AndOrOp.or => false

def Complexity.CircuitCode.RawGate.opOfBit : Bool → AndOrOp

Decode the operation bit used by opBit.

Equations

• Complexity.CircuitCode.RawGate.opOfBit true = Complexity.AndOrOp.and
• Complexity.CircuitCode.RawGate.opOfBit false = Complexity.AndOrOp.or

def Complexity.CircuitCode.RawGate.encode (g : RawGate) : List Bool

Encode a gate as operation, negation flags, then two unary references.

Equations

• g.encode = [g.opBit, g.negated₀, g.negated₁] ++ Complexity.CircuitCode.NatCode.encode g.input₀ ++ Complexity.CircuitCode.NatCode.encode g.input₁

def Complexity.CircuitCode.RawGate.decodePrefix? : List Bool → Option (RawGate × List Bool)

Parse one gate prefix, returning the unconsumed suffix.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.RawGate.decodePrefix? x✝ = none

Circuit serialization

def Complexity.CircuitCode.RawCircuit.decodeGates? : ℕ → List Bool → Option (RawCircuit × List Bool)

Parse exactly count gate prefixes and return the remaining suffix.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.RawCircuit.decodeGates? 0 x✝ = some ([], x✝)

def Complexity.CircuitCode.RawCircuit.encode (c : RawCircuit) : List Bool

Serialize a circuit as its unary gate count followed by its gates.

Equations

• c.encode = Complexity.CircuitCode.NatCode.encode (List.length c) ++ List.flatMap Complexity.CircuitCode.RawGate.encode c

def Complexity.CircuitCode.RawCircuit.decodePrefix? (bits : List Bool) : Option (RawCircuit × List Bool)

Decode one circuit prefix and return the unconsumed suffix.

Equations

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

def Complexity.CircuitCode.RawCircuit.decode? (bits : List Bool) : Option RawCircuit

Decode exactly one circuit. Any trailing bits are rejected.

Equations

• Complexity.CircuitCode.RawCircuit.decode? bits = match Complexity.CircuitCode.RawCircuit.decodePrefix? bits with | some (c, []) => some c | x => none

def Complexity.CircuitCode.RawGate.ofGate {W : ℕ} (g : Gate Basis.andOr2 W) : RawGate

Translate a typed fan-in-two gate to the proof-free wire format.

Equations

• Complexity.CircuitCode.RawGate.ofGate g = { op := g.op, input₀ := ↑(g.inputs ⟨0, ⋯⟩), input₁ := ↑(g.inputs ⟨1, ⋯⟩), negated₀ := g.negated ⟨0, ⋯⟩, negated₁ := g.negated ⟨1, ⋯⟩ }

def Complexity.CircuitCode.RawCircuit.ofCircuit {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : RawCircuit

Translate a typed single-output circuit to an ordered raw circuit.

Internal gates retain their order and the typed output gate is appended as the last raw gate.

Equations

• Complexity.CircuitCode.RawCircuit.ofCircuit c = (List.ofFn fun (i : Fin G) => Complexity.CircuitCode.RawGate.ofGate (c.gates i)) ++ [Complexity.CircuitCode.RawGate.ofGate (c.outputs 0)]

def Complexity.CircuitCode.encodeCircuit {N G : ℕ} [NeZero N] (c : Circuit Basis.andOr2 N 1 G) : List Bool

Serialize a typed fan-in-two circuit as machine-facing bits.

Equations

• Complexity.CircuitCode.encodeCircuit c = (Complexity.CircuitCode.RawCircuit.ofCircuit c).encode

def Complexity.CircuitCode.evalCode (N : ℕ) (code input : List Bool) : Option Bool

Decode and evaluate a circuit code against an input of exactly N bits.

Equations

• Complexity.CircuitCode.evalCode N code input = if input.length = N then do let circuit ← Complexity.CircuitCode.RawCircuit.decode? code circuit.eval? input else none