CLRS-Lean
Chapter 34. NP-Completeness
34.4. NP-Completeness Proofs
34.4. Cook--Levin infrastructure
34.4. Verifier circuitization
34.4. Complete verifier-circuit generator body

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorValidityRows
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTail
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.TransitionFamilyScript
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.PolyBuilder.VerifierBodyController

Executable Cook--Levin verifier body

This module compiles the canonical validity rows, adjacent-row transition scripts, and post-transition tail into the continuous verifier-body controller. Its generated bytes are exactly the suffix following the shared Boolean pool in verifierCircuit.

              namespace CLRS.Chapter34.Turing.CookLevinnoncomputable sectionopen StateTransitionopen PolyBuilder

Semantic circuit suffix following the exact header/input/pool prefix.

def verifierCircuitBodyGateStream
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (x : List Γ) : List CircuitSym :=
  verifierValidityGateStream W x ++
    verifierTransitionGateStream W x ++
    verifierCircuitTailGateStream W x

Canonical runtime operands for the complete verifier body.

noncomputable def compileVerifierBodyScript
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (x : List Γ) : AffineVerifierBodyScript :=
  { validityFrames := verifierValidityRowFramesByLength W x.length
    transitionScripts := compileTransitionFamilyScriptsAt W.machine.tm
      ((verifierHeight W).eval x.length)
      ((verifierHorizon W).eval x.length)
    tailScript := compileVerifierTailScript W x }

The compiled body script denotes exactly the canonical semantic suffix.


theorem compileVerifierBodyScript_gateStream_eq
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (x : List Γ) :
    affineVerifierBodyGateStream (compileVerifierBodyScript W x) =
      verifierCircuitBodyGateStream W x := by
  have hvalid := arithmeticValidityRowsGateStream_eq_semantic W.machine.tm
    ((verifierHeight W).eval x.length)
    ((verifierHorizon W).eval x.length)
  have htransition := compileTransitionFamilyScriptsAt_gateStream_eq
    W.machine.tm ((verifierHeight W).eval x.length)
      ((verifierHorizon W).eval x.length)
  simp only [compileVerifierBodyScript, affineVerifierBodyGateStream,
    verifierCircuitBodyGateStream]
  rw [show affineValidityRowFamilyGateStream
        (verifierValidityRowFramesByLength W x.length) =
      verifierValidityGateStream W x by
    rw [verifierValidityGateStream_eq_byLength]
    simpa [verifierValidityRowFramesByLength,
      verifierValidityGateStreamByLength] using hvalid]
  rw [show affineTransitionFamilyGateStream
        (compileTransitionFamilyScriptsAt W.machine.tm
          ((verifierHeight W).eval x.length)
          ((verifierHorizon W).eval x.length)) =
      verifierTransitionGateStream W x by
    simpa [verifierTransitionGateStream,
      verifierTransitionGateStreamByLength] using htransition]
  rw [compileVerifierTailScript_gateStream_eq]

The already generated pool prefix followed by the generated body is the complete verifier-circuit encoding, byte for byte.


theorem verifierCircuitPoolPrefix_append_body
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (x : List Γ) :
    verifierCircuitPoolPrefix W x ++
        affineVerifierBodyGateStream (compileVerifierBodyScript W x) =
      encodeCircuit (verifierCircuit W x) := by
  rw [compileVerifierBodyScript_gateStream_eq]
  simpa [verifierCircuitBodyGateStream, verifierCircuitTransitionPrefix,
    verifierCircuitValidityPrefix, List.append_assoc] using
    verifierCircuitTransitionPrefix_append_tail W x

One fixed program computes the exact verifier body from its compiled runtime operand stream.

def verifierCircuitBody_run
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (x : List Γ) (output : List CircuitSym) :
    EvalsToInTime (step affineVerifierBodyRevProgram)
      (affineVerifierBodyLoopCfg
        (encodeAffineVerifierBodyScript
          (compileVerifierBodyScript W x)) output)
      (some (haltCfg affineVerifierBodyRevProgram
        ((verifierCircuitBodyGateStream W x).reverse ++ output)))
      (affineVerifierBodyRevSteps (compileVerifierBodyScript W x)) := by
  simpa [compileVerifierBodyScript_gateStream_eq] using
    affineVerifierBody_run (compileVerifierBodyScript W x) output

Starting with the already generated prefix in the reverse-output accumulator, the same body run halts with the complete circuit encoding.


def verifierCircuitBody_run_afterPool
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (x : List Γ) :
    EvalsToInTime (step affineVerifierBodyRevProgram)
      (affineVerifierBodyLoopCfg
        (encodeAffineVerifierBodyScript (compileVerifierBodyScript W x))
        (verifierCircuitPoolPrefix W x).reverse)
      (some (haltCfg affineVerifierBodyRevProgram
        (encodeCircuit (verifierCircuit W x)).reverse))
      (affineVerifierBodyRevSteps (compileVerifierBodyScript W x)) := by
  have hrun := verifierCircuitBody_run W x
    (verifierCircuitPoolPrefix W x).reverse
  have hbytes := verifierCircuitPoolPrefix_append_body W x
  have hsemantic : verifierCircuitPoolPrefix W x ++
        verifierCircuitBodyGateStream W x =
      encodeCircuit (verifierCircuit W x) := by
    simpa [compileVerifierBodyScript_gateStream_eq] using hbytes
  have houtput : (verifierCircuitBodyGateStream W x).reverse ++
        (verifierCircuitPoolPrefix W x).reverse =
      (encodeCircuit (verifierCircuit W x)).reverse := by
    simpa [List.reverse_append] using congrArg List.reverse hsemantic
  simpa [houtput] using hrun

The specialized verifier body inherits the uniform quadratic envelope in its exact compiled runtime encoding.

theorem verifierCircuitBody_steps_le
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (x : List Γ) :
    affineVerifierBodyRevSteps (compileVerifierBodyScript W x) ≤
      10000 * (encodeAffineVerifierBodyScript
        (compileVerifierBodyScript W x)).length ^ 2 + 200 :=
  affineVerifierBody_steps_le (compileVerifierBodyScript W x)

Once a concrete polynomial-time compiler produces the canonical operand script from the raw source input, generic machine composition yields the exact forward verifier-body gate stream. This theorem isolates the only missing machine-level premise instead of treating compileVerifierBodyScript as an oracle.

noncomputable def
    verifierCircuitBodyGateStream_computableInPolyTime_of_scriptCompiler
    {Γ : Type} {L : Language Γ} (W : VerifierWitness L)
    (compiler : _root_.Turing.TM2ComputableInPolyTime id
      encodeAffineVerifierBodyScript (compileVerifierBodyScript W)) :
    _root_.Turing.TM2ComputableInPolyTime id id
      (verifierCircuitBodyGateStream W) := by
  let composed :=
    _root_.Turing.TM2Comp.TM2ComputableInPolyTime.comp_scratch compiler
      affineVerifierBodyGateStream_computableInPolyTime
  simpa [Function.comp_def, compileVerifierBodyScript_gateStream_eq] using
    Classical.choice composed

endend CLRS.Chapter34.Turing.CookLevin