GapCVP proof, part 02

noncomputable def GapCVP.CLPhaseSpecification.CorrectedGuessingAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

Check the guessing phase, its preserved tracks, and the witness and input guesses.

Equations

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

noncomputable def GapCVP.CLPhaseCompleteness.decodeCorrectedPhaseRow {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) {width : ℕ} (row : CL.Position width → CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) : CL.Position width → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm

GapCVP reduction support.

Equations

• GapCVP.CLPhaseCompleteness.decodeCorrectedPhaseRow machine row position = (GapCVP.CLCompleteVerifierSimulation.completePhaseSymbolEquiv machine.tm).symm (row position)

noncomputable def GapCVP.CLPhaseTableauSimulation.FirstBlockAnchored (tm : Turing.FinTM2) (cell : CLCompleteVerifierSimulation.CompletePhaseCell tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPhaseTableauSimulation.PhaseBoundaryPreserved (tm : Turing.FinTM2) (window : CLCompleteVerifierSimulation.CompletePhaseWindow tm) : Bool

Check that a local step preserves whether the cell is in the first machine block.

Equations

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

noncomputable def GapCVP.CLPhaseTableauSimulation.AnchoredGuessingAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPhaseTableauSimulation.AnchoredInitializationAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPhaseTableauSimulation.AnchoredVerificationAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPhaseTableauSimulation.AnchoredAcceptanceAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLPhaseTraceInduction.canonicalAnchoredVerifyingRow (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (configuration : machine.tm.Cfg) (hsupported : CLPushAlphabet.StackAtomSupported machine configuration = true) (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) (annotation : Bool) : CL.Position (CLCellRowBounds.rowWidth bound machine x) → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm

GapCVP reduction support.

Equations

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

def GapCVP.CLPhaseGlobalSimulation.anchoredVerifierWindowAt (tm : Turing.FinTM2) (width : ℕ) (first next : CL.Position width → CLCompleteVerifierSimulation.CompletePhaseCell tm) (position : CL.Position width) : CLCompleteVerifierSimulation.CompletePhaseWindow tm

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.CLWholeTraceSoundness.AnchoredPhaseTrace (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : Type

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLWholeTraceSoundness.AnchoredPhaseMasks (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (position : CL.Position (CLCellRowBounds.rowWidth bound machine x)) (cell : CLCompleteVerifierSimulation.CompletePhaseCell machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStackShiftSoundness.OccupiedVerifierPrefix {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStackVerifierSimulation.StackSoundAnchoredVerificationAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStackVerifierSimulation.StackSoundAnchoredPhaseAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStackVerifierSimulation.stackSoundAnchoredPhaseAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

• GapCVP.CLStackVerifierSimulation.stackSoundAnchoredPhaseAllowed machine window = decide (GapCVP.CLStackVerifierSimulation.StackSoundAnchoredPhaseAllowed machine window = true)

theorem GapCVP.CLStackVerifierSimulation.stackSoundAnchoredPhaseAllowed_iff {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : stackSoundAnchoredPhaseAllowed machine window = true ↔ StackSoundAnchoredPhaseAllowed machine window = true

noncomputable def GapCVP.CLStackVerifierSimulation.stackSoundAnchoredPhaseSymbolAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CL.WindowSymbols (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLStackVerifierSimulation.stackSoundAnchoredPhaseSpecification (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : CL.Specification (Polynomial.eval x.length (CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine)) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)

GapCVP reduction support.

Equations

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

theorem GapCVP.CLAnchoredTraceSimulation.stackSoundValidTrace_window (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (trace : CLWholeTraceSoundness.AnchoredPhaseTrace bound machine x) (htrace : CL.ValidTrace (CLStackVerifierSimulation.stackSoundAnchoredPhaseSpecification bound machine x) trace = true) (window : CL.Window (CLCellRowBounds.rowWidth bound machine x)) : CLStackVerifierSimulation.StackSoundAnchoredPhaseAllowed machine (CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace (↑window).1) (CL.leftPosition window), CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace (↑window).1) (↑window).2, CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace (↑window).1) (CL.rightPosition window), CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace (CL.nextTime window)) (↑window).2) = true

noncomputable def GapCVP.CLArbitraryRowOccupancy.DecodableOrBlank {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (atom : CLBoundedStates.CellAtom machine.tm) : Bool

Check that a cell atom is blank or decodes to a symbol of the designated stack.

Equations

• GapCVP.CLArbitraryRowOccupancy.DecodableOrBlank machine stack atom = decide (atom = none ∨ ∃ (value : machine.tm.Γ stack), GapCVP.CLPushAlphabet.cellAtomValue machine stack atom = some value)

noncomputable def GapCVP.CLArbitraryRowOccupancy.PhaseRowAtomsWellTyped {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (row : CL.Position width → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CLWholeTimeOccupancy.stackSoundValidTrace_all_verifier_rows_wellTyped (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (trace : CLWholeTraceSoundness.AnchoredPhaseTrace bound machine x) (htrace : CL.ValidTrace (CLStackVerifierSimulation.stackSoundAnchoredPhaseSpecification bound machine x) trace = true) (time : CL.Time (CLCellRowBounds.rowWidth bound machine x)) : (∀ (position : CL.Position (CLCellRowBounds.rowWidth bound machine x)), (CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace time) position).mode = CLBoundedStates.PhaseTag.verifying) → CLArbitraryRowOccupancy.PhaseRowAtomsWellTyped machine (CLCellRowBounds.rowWidth bound machine x) (CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace time)) = true

noncomputable def GapCVP.CLCompactWindowSoundness.NoInteriorPaddingHoles (tm : Turing.FinTM2) (atoms : List (CLBoundedStates.CellAtom tm)) : Bool

GapCVP reduction support.

Equations

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

def GapCVP.CLBoundedRowInduction.packedPhaseCapacity (tm : Turing.FinTM2) (width : ℕ) : ℕ

Total number of atom positions across all blocks of a phase row.

Equations

• GapCVP.CLBoundedRowInduction.packedPhaseCapacity tm width = (width + 1) * GapCVP.CLLocalWindows.blockSize tm

def GapCVP.CLBoundedRowInduction.fullPackedPhaseStackAtoms {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (row : CL.Position width → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm) (stack : machine.tm.K) : List (CLBoundedStates.CellAtom machine.tm)

GapCVP reduction support.

Equations

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

def GapCVP.CLBoundedRowInduction.decodedFullPackedPhaseStack {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (row : CL.Position width → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm) (stack : machine.tm.K) : List (machine.tm.Γ stack)

Decode a stack from the packed phase row, discarding atoms without a stack symbol.

Equations

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

def GapCVP.CLFullStackStepSoundness.decodedFullPackedPhaseConfiguration {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (row : CL.Position width → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm) : machine.tm.Cfg

GapCVP reduction support.

Equations

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

theorem GapCVP.CLNaturalTimeCompiler.stackSoundValidTrace_firstAcceptance_actualReachable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (trace : CLWholeTraceSoundness.AnchoredPhaseTrace bound machine x) (htrace : CL.ValidTrace (CLStackVerifierSimulation.stackSoundAnchoredPhaseSpecification bound machine x) trace = true) : ∃ (time : Fin (CLCellRowBounds.rowWidth bound machine x)) (position : CL.Position (CLCellRowBounds.rowWidth bound machine x)) (certificate : List Bool), have first := CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace time.castSucc); have next := CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace time.succ); CLPhaseTableauSimulation.AnchoredAcceptanceAllowed machine (CLPhaseGlobalSimulation.anchoredVerifierWindowAt machine.tm (CLCellRowBounds.rowWidth bound machine x) first next position) = true ∧ (∀ (other : CL.Position (CLCellRowBounds.rowWidth bound machine x)), (first other).mode = CLBoundedStates.PhaseTag.verifying) ∧ (∀ (other : CL.Position (CLCellRowBounds.rowWidth bound machine x)), CLWholeTraceSoundness.AnchoredPhaseMasks bound machine x other (first other) = true) ∧ (∀ (stack : machine.tm.K), CLCompactWindowSoundness.NoInteriorPaddingHoles machine.tm (CLBoundedRowInduction.fullPackedPhaseStackAtoms machine (CLCellRowBounds.rowWidth bound machine x) first stack) = true) ∧ certificate.length ≤ Polynomial.eval x.length bound ∧ Nonempty (CLNondeterminism.FiniteRun (CLNondeterminism.GuessStep bound machine x) (CLNondeterminism.GuessState.guessing []) (CLNondeterminism.GuessState.verifying certificate (CLFullStackStepSoundness.decodedFullPackedPhaseConfiguration machine (CLCellRowBounds.rowWidth bound machine x) first)) ↑time) ∧ (∃ (verifierRun : StateTransition.EvalsTo machine.tm.step (Turing.initList machine.tm (CLVerifier.verifierInput machine x certificate)) (some (CLFullStackStepSoundness.decodedFullPackedPhaseConfiguration machine (CLCellRowBounds.rowWidth bound machine x) first))), ↑time = certificate.length + 1 + verifierRun.steps) ∧ ↑time ≤ Polynomial.eval x.length (CLNondeterminism.guessTimePolynomial bound machine) ∧ ∀ (earlier : CL.Time (CLCellRowBounds.rowWidth bound machine x)), ↑earlier ≤ ↑time → ∀ (other : CL.Position (CLCellRowBounds.rowWidth bound machine x)), (CLPhaseCompleteness.decodeCorrectedPhaseRow machine (trace earlier) other).mode ≠ CLBoundedStates.PhaseTag.accepting

noncomputable def GapCVP.CLAcceptanceAnchor.ReplicatedMachineHeadCoherent (tm : Turing.FinTM2) (window : CLCompleteVerifierSimulation.CompletePhaseWindow tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLAcceptanceAnchor.TrueOutputMachineHead {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (cell : CLCompleteVerifierSimulation.CompletePhaseCell machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLAcceptanceAnchor.AcceptanceAnchoredPhaseAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CLCompleteVerifierSimulation.CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CLAcceptanceAnchor.trueOutputMachineHead_actualVerifierHalt (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (row : CL.Position (CLCellRowBounds.rowWidth bound machine x) → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm) (hcertificate : certificate.length ≤ Polynomial.eval x.length bound) (verifierRun : StateTransition.EvalsTo machine.tm.step (Turing.initList machine.tm (CLVerifier.verifierInput machine x certificate)) (some (CLFullStackStepSoundness.decodedFullPackedPhaseConfiguration machine (CLCellRowBounds.rowWidth bound machine x) row))) (hrow : CLArbitraryRowOccupancy.PhaseRowAtomsWellTyped machine (CLCellRowBounds.rowWidth bound machine x) row = true) (hholes : ∀ (stack : machine.tm.K), CLCompactWindowSoundness.NoInteriorPaddingHoles machine.tm (CLBoundedRowInduction.fullPackedPhaseStackAtoms machine (CLCellRowBounds.rowWidth bound machine x) row stack) = true) (hfirst : CLCompleteVerifierSimulation.completeIsFirstBlock machine.tm (row 0) = true) (hanchor : CLPhaseTableauSimulation.FirstBlockAnchored machine.tm (row 0) = true) (htrue : TrueOutputMachineHead machine (row 0) = true) (hcontrol : CLTableauSimulationCert.machineControlOfBlock machine.tm (CLCompleteVerifierSimulation.completeMachineHead machine.tm (row 0)) = some ((Turing.haltList machine.tm (CLVerifier.verifierOutput machine true)).l, (Turing.haltList machine.tm (CLVerifier.verifierOutput machine true)).var)) : verifier (x, certificate) = true ∧ CLFullStackStepSoundness.decodedFullPackedPhaseConfiguration machine (CLCellRowBounds.rowWidth bound machine x) row = Turing.haltList machine.tm (CLVerifier.verifierOutput machine true)

noncomputable def GapCVP.CLVerifiedLocalTableauCompiler.canonicalAnchoredGuessingRow (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (annotation : Bool) : CL.Position (CLCellRowBounds.rowWidth bound machine x) → CLCompleteVerifierSimulation.CompletePhaseCell machine.tm

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CLVerifiedLocalTableauCompiler.canonicalAnchoredGuessingRow_initial (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) : canonicalAnchoredGuessingRow bound machine x [] false = CLCompleteVerifierSimulation.initialPhaseCell bound machine x

noncomputable def GapCVP.CLVerifiedLocalTableauCompiler.AllCanonicalAcceptanceAnchoredVerifierTraceWindows (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) {steps : ℕ} (configuration : Fin (steps + 1) → machine.tm.Cfg) (hsupported : ∀ (time : Fin (steps + 1)), CLPushAlphabet.StackAtomSupported machine (configuration time) = true) (hint : Fin (steps + 1) → CLExactVerifierTransition.FiniteVerifierHint machine.tm) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CLVerifiedLocalTableauCompiler.canonicalAcceptanceAnchoredVerifierTraceWindows_iff_actualRun (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) {steps : ℕ} (configuration : Fin (steps + 1) → machine.tm.Cfg) (hsupported : ∀ (time : Fin (steps + 1)), CLPushAlphabet.StackAtomSupported machine (configuration time) = true) (hspace : ∀ (time : Fin (steps + 1)) (stack : machine.tm.K), ((configuration time).stk stack).length ≤ CLCellRowBounds.rowWidth bound machine x) : (∃ (hint : Fin (steps + 1) → CLExactVerifierTransition.FiniteVerifierHint machine.tm), AllCanonicalAcceptanceAnchoredVerifierTraceWindows bound machine x certificate configuration hsupported hint = true) ↔ ∀ (time : Fin steps), machine.tm.step (configuration time.castSucc) = some (configuration time.succ)

theorem GapCVP.CLVerifiedLocalTableauCompiler.canonicalTrueHalt_acceptanceAnchoredWindows (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (hsupported : CLPushAlphabet.StackAtomSupported machine (Turing.haltList machine.tm (CLVerifier.verifierOutput machine true)) = true) (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) (position : CL.Position (CLCellRowBounds.rowWidth bound machine x)) : CLAcceptanceAnchor.AcceptanceAnchoredPhaseAllowed machine (CLPhaseGlobalSimulation.anchoredVerifierWindowAt machine.tm (CLCellRowBounds.rowWidth bound machine x) (CLPhaseTraceInduction.canonicalAnchoredVerifyingRow bound machine x certificate (Turing.haltList machine.tm (CLVerifier.verifierOutput machine true)) hsupported hint false) (fun (x : CL.Position (CLCellRowBounds.rowWidth bound machine x)) => CLCompleteVerifierSimulation.acceptingPhaseCell machine.tm) position) = true

theorem GapCVP.CLFinalTableauAssembly.canonicalGuessingStep_acceptanceAnchoredWindows (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (oldAnnotation bit : Bool) (hbound : certificate.length < Polynomial.eval x.length bound) (position : CL.Position (CLCellRowBounds.rowWidth bound machine x)) : CLAcceptanceAnchor.AcceptanceAnchoredPhaseAllowed machine (CLPhaseGlobalSimulation.anchoredVerifierWindowAt machine.tm (CLCellRowBounds.rowWidth bound machine x) (CLVerifiedLocalTableauCompiler.canonicalAnchoredGuessingRow bound machine x certificate oldAnnotation) (CLVerifiedLocalTableauCompiler.canonicalAnchoredGuessingRow bound machine x (certificate ++ [bit]) bit) position) = true

theorem GapCVP.CLFinalTableauAssembly.canonicalInitialization_acceptanceAnchoredWindows (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x certificate : List Bool) (hsupported : CLPushAlphabet.StackAtomSupported machine (Turing.initList machine.tm (CLVerifier.verifierInput machine x certificate)) = true) (oldAnnotation : Bool) (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) (position : CL.Position (CLCellRowBounds.rowWidth bound machine x)) : CLAcceptanceAnchor.AcceptanceAnchoredPhaseAllowed machine (CLPhaseGlobalSimulation.anchoredVerifierWindowAt machine.tm (CLCellRowBounds.rowWidth bound machine x) (CLVerifiedLocalTableauCompiler.canonicalAnchoredGuessingRow bound machine x certificate oldAnnotation) (CLPhaseTraceInduction.canonicalAnchoredVerifyingRow bound machine x certificate (Turing.initList machine.tm (CLVerifier.verifierInput machine x certificate)) hsupported hint false) position) = true