Nonuniform circuits as polynomial advice — definitions

This file defines the original-input-indexed running-time budget used when a circuit family's canonical member code is supplied as advice to the verified serialized-circuit evaluator.

def Complexity.CircuitFamily.adviceEvalTime (F : CircuitFamily Basis.andOr2) (n : ℕ) : ℕ

Time for the serialized evaluator on the advised input carrying the canonical code for the length-n member of F. The pairing length is stated explicitly because advised time is charged against n, not against the longer machine input.

Equations

• F.adviceEvalTime n = Complexity.CircuitCode.Machine.evalFamilyTime (2 * (F.encodeAt n).length + 2 + n)