Evaluating a circuit with guessed values at a cut #
Program.evalCut replaces the values of a selected set of gates by guesses,
and evaluates every other gate normally. Program.CutConsistent checks the
equation of each selected gate against this evaluation. Only selected gates
need guesses; no values for the other gates are part of the certificate.
The construction works for any signature and interpretation, not just Boolean circuits. It provides the semantic part of cutting shared gates. Turning the pieces into formulas and bounding their leaf counts requires further work.
@[irreducible]
def
Cslib.Circuits.Program.evalCut
{σ : Signature}
{n g : ℕ}
{U : Type u_1}
(p : Program σ n g)
(cut : Finset (Fin g))
(I : Interpretation σ U)
(x : Fin n → U)
(guess : ↥cut → U)
(j : Fin g)
:
U
Evaluate a program, using the guessed value whenever a selected gate is read.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Cslib.Circuits.Program.CutConsistent
{σ : Signature}
{n g : ℕ}
{U : Type u_1}
(p : Program σ n g)
(cut : Finset (Fin g))
(I : Interpretation σ U)
(x : Fin n → U)
(guess : ↥cut → U)
:
A guess is consistent if every cut gate's own equation produces its guessed value.