Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.4. NP-Completeness Proofs
  4. 34.4. Cook--Levin infrastructure
  5. 34.4. Verifier circuitization
  6. 34.4. Complete quoted row sources for arbitrary transition statements
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionStatementBranchFreeQuotedRowSource import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionRecursiveBranchQuotedMuxRowSource import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionConstantQuotedRowSource import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.CookLevin.Circuitization.GeneratorTransitionDispatchPhaseTags

Complete quoted row sources for arbitrary transition statements

This removes the former branch-free restriction. At a branch node the physical source order is exactly the semantic controller order: affine head, true subtree, false subtree, fixed mux tag, and the delimiter-safe mux invocation generated by the descriptor pipeline.

noncomputable sectionnamespace CLRS.Chapter34.Turing.CookLevinopen _root_.Turing.TM2 _root_.Turing.TM2.Stmtopen PolyBuilder

Pointwise-quoted concrete source for every statement syntax tree.

noncomputable def verifierTransitionStmtQuotedSeedRowSource {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (labelOffset : TransitionAffineNat) : (context : TransitionStmtAffineContext W.machine.tm) → (q : _root_.Turing.TM2.Stmt W.machine.tm.Γ W.machine.tm.Λ W.machine.tm.σ) → (hsupport : ∀ k, stmtPushSet W.machine.tm q k ⊆ reachableAlphabet W.machine.tm k) → (hbounds : (transitionStmtRecursivePlan W.machine.tm labelOffset context q hsupport).UniformLinearRouteBounds W labelOffset) → (hpadding : VerifierTransitionRecursiveStmtPadding W context q hsupport) → VerifierTransitionSeedRowSource W | context, halt, hsupport, hbounds, hpadding => verifierTransitionAffineHeadQuotedSeedRowSource W [] | context, goto jump, hsupport, hbounds, hpadding => verifierTransitionAffineHeadQuotedSeedRowSource W (transitionStmtContextHeadPhaseForm W.machine.tm labelOffset context (.goto jump) hsupport).toList | context, load update continuation, hsupport, hbounds, hpadding => let hcontinuation : ∀ k, stmtPushSet W.machine.tm continuation k ⊆ reachableAlphabet W.machine.tm k := by simpa [stmtPushSet] using hsupport let tailBounds : (transitionStmtRecursivePlan W.machine.tm labelOffset (context.afterLoad W.machine.tm update) continuation hcontinuation).UniformLinearRouteBounds W labelOffset := by simpa [transitionStmtRecursivePlan, TransitionStmtRecursivePlan.UniformLinearRouteBounds] using hbounds let tailPadding : VerifierTransitionRecursiveStmtPadding W (context.afterLoad W.machine.tm update) continuation hcontinuation := by intro input seed hseed exact (hpadding input seed hseed).2 let head := verifierTransitionAffineHeadQuotedSeedRowSource W (transitionStmtContextHeadPhaseForm W.machine.tm labelOffset context (.load update continuation) hsupport).toList let tail := verifierTransitionStmtQuotedSeedRowSource W labelOffset (context.afterLoad W.machine.tm update) continuation hcontinuation tailBounds tailPadding head.append tail | context, push selected emit continuation, hsupport, hbounds, hpadding => let hcontinuation : ∀ k, stmtPushSet W.machine.tm continuation k ⊆ reachableAlphabet W.machine.tm k := by intro k symbol hsymbol apply hsupport k simp only [stmtPushSet] exact Finset.mem_union_right _ hsymbol let symbolAt : Fin (stateCount W.machine.tm) → SupportedSymbol W.machine.tm selected := fun code => ⟨emit ((stateEquivFin W.machine.tm).symm code), by apply hsupport selected simp [stmtPushSet]⟩ let table := fun code => encodeSupportedSymbol (symbolAt code) let tailBounds : (transitionStmtRecursivePlan W.machine.tm labelOffset (context.afterPush W.machine.tm selected table) continuation hcontinuation).UniformLinearRouteBounds W labelOffset := by simpa [transitionStmtRecursivePlan, TransitionStmtRecursivePlan.UniformLinearRouteBounds] using hbounds let tailPadding : VerifierTransitionRecursiveStmtPadding W (context.afterPush W.machine.tm selected table) continuation hcontinuation := by intro input seed hseed exact (hpadding input seed hseed).2 let head := verifierTransitionAffineHeadQuotedSeedRowSource W (transitionStmtContextHeadPhaseForm W.machine.tm labelOffset context (.push selected emit continuation) hsupport).toList let tail := verifierTransitionStmtQuotedSeedRowSource W labelOffset (context.afterPush W.machine.tm selected table) continuation hcontinuation tailBounds tailPadding head.append tail | context, peek selected update continuation, hsupport, hbounds, hpadding => let hcontinuation : ∀ k, stmtPushSet W.machine.tm continuation k ⊆ reachableAlphabet W.machine.tm k := by simpa [stmtPushSet] using hsupport let tailBounds : (transitionStmtRecursivePlan W.machine.tm labelOffset (context.afterPeek W.machine.tm selected update) continuation hcontinuation).UniformLinearRouteBounds W labelOffset := by simpa [transitionStmtRecursivePlan, TransitionStmtRecursivePlan.UniformLinearRouteBounds] using hbounds let tailPadding : VerifierTransitionRecursiveStmtPadding W (context.afterPeek W.machine.tm selected update) continuation hcontinuation := by intro input seed hseed exact (hpadding input seed hseed).2 let head := verifierTransitionAffineHeadQuotedSeedRowSource W (transitionStmtContextHeadPhaseForm W.machine.tm labelOffset context (.peek selected update continuation) hsupport).toList let tail := verifierTransitionStmtQuotedSeedRowSource W labelOffset (context.afterPeek W.machine.tm selected update) continuation hcontinuation tailBounds tailPadding head.append tail | context, pop selected update continuation, hsupport, hbounds, hpadding => let hcontinuation : ∀ k, stmtPushSet W.machine.tm continuation k ⊆ reachableAlphabet W.machine.tm k := by simpa [stmtPushSet] using hsupport let tailBounds : (transitionStmtRecursivePlan W.machine.tm labelOffset (context.afterPop W.machine.tm selected update) continuation hcontinuation).UniformLinearRouteBounds W labelOffset := by simpa [transitionStmtRecursivePlan, TransitionStmtRecursivePlan.UniformLinearRouteBounds] using hbounds let tailPadding : VerifierTransitionRecursiveStmtPadding W (context.afterPop W.machine.tm selected update) continuation hcontinuation := by intro input seed hseed exact (hpadding input seed hseed).2 let head := verifierTransitionAffineHeadQuotedSeedRowSource W (transitionStmtContextPopPhaseForms W.machine.tm labelOffset context selected update) let tail := verifierTransitionStmtQuotedSeedRowSource W labelOffset (context.afterPop W.machine.tm selected update) continuation hcontinuation tailBounds tailPadding head.append tail | context, branch test whenTrue whenFalse, hsupport, hbounds, hpadding => let htrueSupport := transitionStmtBranchTrueSupport W.machine.tm test whenTrue whenFalse hsupport let hfalseSupport := transitionStmtBranchFalseSupport W.machine.tm test whenTrue whenFalse hsupport let trueContext := transitionStmtBranchTrueContext W.machine.tm context test let falseContext := transitionStmtBranchFalseContext W.machine.tm context test whenTrue let branchBounds : (transitionStmtRecursivePlan W.machine.tm labelOffset trueContext whenTrue htrueSupport).UniformLinearRouteBounds W labelOffset ∧ (transitionStmtRecursivePlan W.machine.tm labelOffset falseContext whenFalse hfalseSupport).UniformLinearRouteBounds W labelOffset := by simpa [transitionStmtRecursivePlan, TransitionStmtRecursivePlan.UniformLinearRouteBounds, trueContext, falseContext, htrueSupport, hfalseSupport] using hbounds let htruePadding : VerifierTransitionRecursiveStmtPadding W trueContext whenTrue htrueSupport := by intro input seed hseed exact (hpadding input seed hseed).2.1 let hfalsePadding : VerifierTransitionRecursiveStmtPadding W falseContext whenFalse hfalseSupport := by intro input seed hseed exact (hpadding input seed hseed).2.2 let head := verifierTransitionAffineHeadQuotedSeedRowSource W (transitionStmtContextHeadPhaseForm W.machine.tm labelOffset context (.branch test whenTrue whenFalse) hsupport).toList let trueTree := verifierTransitionStmtQuotedSeedRowSource W labelOffset trueContext whenTrue htrueSupport branchBounds.1 htruePadding let falseTree := verifierTransitionStmtQuotedSeedRowSource W labelOffset falseContext whenFalse hfalseSupport branchBounds.2 hfalsePadding let muxTag := verifierTransitionConstantQuotedSeedRowSource W (transitionStmtPhaseKindTagCode .mux) let mux := verifierTransitionRecursiveBranchQuotedMuxSeedRowSource W labelOffset context test whenTrue whenFalse hsupport branchBounds.1 branchBounds.2 htruePadding hfalsePadding ((((head.append trueTree).append falseTree).append muxTag).append mux)

The total physical source equals the quotation of the complete recursive statement controller on every canonical transition seed.

theorem verifierTransitionStmtQuotedSeedRowSource_row_eq {Γ : Type} {L : Language Γ} (W : VerifierWitness L) (labelOffset : TransitionAffineNat) : ∀ (context : TransitionStmtAffineContext W.machine.tm) (q : _root_.Turing.TM2.Stmt W.machine.tm.Γ W.machine.tm.Λ W.machine.tm.σ) (hsupport : ∀ k, stmtPushSet W.machine.tm q k ⊆ reachableAlphabet W.machine.tm k) (hbounds : (transitionStmtRecursivePlan W.machine.tm labelOffset context q hsupport).UniformLinearRouteBounds W labelOffset) (hpadding : VerifierTransitionRecursiveStmtPadding W context q hsupport) (input : List Γ) (seed : TransitionRowSeed), seed ∈ verifierTransitionRowSeeds W input → (verifierTransitionStmtQuotedSeedRowSource W labelOffset context q hsupport hbounds hpadding).row seed = quoteUnaryFrameStream (transitionStmtRecursiveControllerFrames W.machine.tm seed labelOffset context q hsupport) := by intro context q induction q generalizing context with | halt => intro hsupport hbounds hpadding input seed hseed rfl | goto jump => intro hsupport hbounds hpadding input seed hseed rfl | load update continuation ih => intro hsupport hbounds hpadding input seed hseed simp only [verifierTransitionStmtQuotedSeedRowSource, transitionStmtRecursiveControllerFrames, VerifierTransitionSeedRowSource.append_row] rw [ih _ _ _ _ input seed hseed] simp [verifierTransitionAffineHeadQuotedSeedRowSource, quoteUnaryFrameStream, List.flatMap_append] | push selected emit continuation ih => intro hsupport hbounds hpadding input seed hseed simp only [verifierTransitionStmtQuotedSeedRowSource, transitionStmtRecursiveControllerFrames, VerifierTransitionSeedRowSource.append_row] rw [ih _ _ _ _ input seed hseed] simp [verifierTransitionAffineHeadQuotedSeedRowSource, quoteUnaryFrameStream, List.flatMap_append] | peek selected update continuation ih => intro hsupport hbounds hpadding input seed hseed simp only [verifierTransitionStmtQuotedSeedRowSource, transitionStmtRecursiveControllerFrames, VerifierTransitionSeedRowSource.append_row] rw [ih _ _ _ _ input seed hseed] simp [verifierTransitionAffineHeadQuotedSeedRowSource, quoteUnaryFrameStream, List.flatMap_append] | pop selected update continuation ih => intro hsupport hbounds hpadding input seed hseed simp only [verifierTransitionStmtQuotedSeedRowSource, transitionStmtRecursiveControllerFrames, VerifierTransitionSeedRowSource.append_row] rw [ih _ _ _ _ input seed hseed] simp [verifierTransitionAffineHeadQuotedSeedRowSource, quoteUnaryFrameStream, List.flatMap_append] | branch test whenTrue whenFalse ihTrue ihFalse => intro hsupport hbounds hpadding input seed hseed let htrueSupport := transitionStmtBranchTrueSupport W.machine.tm test whenTrue whenFalse hsupport let hfalseSupport := transitionStmtBranchFalseSupport W.machine.tm test whenTrue whenFalse hsupport let trueContext := transitionStmtBranchTrueContext W.machine.tm context test let falseContext := transitionStmtBranchFalseContext W.machine.tm context test whenTrue let branchBounds : (transitionStmtRecursivePlan W.machine.tm labelOffset trueContext whenTrue htrueSupport).UniformLinearRouteBounds W labelOffset ∧ (transitionStmtRecursivePlan W.machine.tm labelOffset falseContext whenFalse hfalseSupport).UniformLinearRouteBounds W labelOffset := by simpa [transitionStmtRecursivePlan, TransitionStmtRecursivePlan.UniformLinearRouteBounds, trueContext, falseContext, htrueSupport, hfalseSupport] using hbounds let htruePadding : VerifierTransitionRecursiveStmtPadding W trueContext whenTrue htrueSupport := by intro otherInput otherSeed hother exact (hpadding otherInput otherSeed hother).2.1 let hfalsePadding : VerifierTransitionRecursiveStmtPadding W falseContext whenFalse hfalseSupport := by intro otherInput otherSeed hother exact (hpadding otherInput otherSeed hother).2.2 have htrue := ihTrue trueContext htrueSupport branchBounds.1 htruePadding input seed hseed have hfalse := ihFalse falseContext hfalseSupport branchBounds.2 hfalsePadding input seed hseed have hheight := verifierTransitionRowSeeds_height_eq W input seed hseed have hwork : 0 < workHeight W.machine.tm seed.height := by rw [hheight] unfold workHeight exact Nat.add_pos_left (verifierHeight_eval_pos W input.length) _ have hsegments := transitionStmtRecursiveBranchMuxInvocationSegments_frames W.machine.tm seed hwork labelOffset context test whenTrue whenFalse hsupport (htruePadding input seed hseed) (hfalsePadding input seed hseed) simp only [verifierTransitionStmtQuotedSeedRowSource, transitionStmtRecursiveControllerFrames, VerifierTransitionSeedRowSource.append_row] rw [htrue, hfalse] rw [verifierTransitionRecursiveBranchQuotedMuxSeedRowSource_row] rw [hsegments] simp [verifierTransitionAffineHeadQuotedSeedRowSource, verifierTransitionConstantQuotedSeedRowSource, transitionStmtPhaseKindTagCode, quoteUnaryFrameStream, List.flatMap_append, List.append_assoc, trueContext, falseContext, This simp argument is unused: htrueSupport Hint: Omit it from the simp argument list. simp [verifierTransitionAffineHeadQuotedSeedRowSource, verifierTransitionConstantQuotedSeedRowSource, ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵transitionStmtPhaseKindTagCode, ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲quoteUnaryFrameStream, ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵List.flatMap_append, List.append_assoc, trueContext, falseContext, ht̵r̵u̵e̵S̵u̵p̵p̵o̵r̵t̵,̵ ̵h̵falseSupport, affineStmtPhaseTagCode] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`htrueSupport, This simp argument is unused: hfalseSupport Hint: Omit it from the simp argument list. simp [verifierTransitionAffineHeadQuotedSeedRowSource, verifierTransitionConstantQuotedSeedRowSource, ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵transitionStmtPhaseKindTagCode, ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲quoteUnaryFrameStream, ̵ ̵ ̵ ̵ ̵ ̵ ̵ ̵List.flatMap_append, List.append_assoc, trueContext, falseContext, htrueSupport, h̵f̵al̵s̵e̵S̵u̵p̵p̵o̵r̵t̵,̵ ̵a̵ffineStmtPhaseTagCode] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hfalseSupport, affineStmtPhaseTagCode]
end CLRS.Chapter34.Turing.CookLevin