OAI/Computability/UniqueGames/PCP/SourceRuntimeSpace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Intermediate tape-space bounds derived from actual successful machine prefixes, and their use in the separately checked physical finalizer.

  1. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.configurationLength line 20

    Source documentation

    All stacks are counted, even when their symbol types differ.

    def configurationLength (tm : FinTM2) (cfg : tm.Cfg) : Nat :=
…
  2. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.initial_configurationLength line 23
  3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.step_configurationLength line 33
  4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.execution_configurationLength line 43

    Source documentation

    Every successfully executed prefix bounds the space in its actual endpoint.

    theorem execution_configurationLength (tm : FinTM2) {start finish : tm.Cfg}
    {budget : Nat}
    (run : StateTransition.EvalsToInTime tm.step start (some finish) budget) :
    configurationLength tm finish ≤ configurationLength tm start +
      budget * (Fintype.card tm.K * Runtime.programPushBound tm) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.configurationLength

  5. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.prefix_configurationLength line 51
  6. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial line 58
  7. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial_eval line 61
  8. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.prefix_length_polynomial line 66
  9. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.totalLength_eq_configurationLength line 76

    Source documentation

    This equality only identifies the actual endpoint stacks with a Boolean finalizer's stacks. It makes no execution or time assumption.

    theorem totalLength_eq_configurationLength (tm : FinTM2) (finish : tm.Cfg)
    (base : tm.K → List Bool)
    (sameLengths : ∀ k, (base k).length = (finish.stk k).length) :
    SourceRuntimeFinish.totalLength base = configurationLength tm finish := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.totalLength, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.configurationLength

  10. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.finishCost_le_of_prefix line 84

    Source documentation

    The actual physical finalizer's cost is bounded by the space reached by the actual prefix. Repeated cleanup keys remain permitted.

    theorem finishCost_le_of_prefix (tm : FinTM2) (input : List (tm.Γ tm.k₀))
    {finish : tm.Cfg} {budget : Nat}
    (run : StateTransition.EvalsToInTime tm.step (initList tm input) (some finish) budget)
    (clearKeys : List tm.K) (accumulator output : tm.K)
    (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
    (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
    (base : tm.K → List Bool) (outputEmpty : base output = [])
    (sameLengths : ∀ k, (base k).length = (finish.stk k).length) :
    SourceRuntimeFinish.finishCost clearKeys accumulator base ≤ input.length +
      budget * (Fintype.card tm.K * Runtime.programPushBound tm) + clearKeys.length + 2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishCost

  11. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.completedTime line 100
  12. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.completedTime_eval line 104
  13. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeSpace.prefixAndFinishInTime line 113

    Source documentation

    Composition retains both actual execution witnesses. The cleanup witness is supplied by SourceRuntimeFinish.finishInTime in the caller's real program.

    def prefixAndFinishInTime (tm : FinTM2) (input : List (tm.Γ tm.k₀))
    (time : Polynomial Nat) {middle finish : tm.Cfg}
    (prefixRun : StateTransition.EvalsToInTime tm.step (initList tm input)
      (some middle) (time.eval input.length))
    (clearKeys : List tm.K) (accumulator output : tm.K)
    (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
    (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
    (base : tm.K → List Bool) (outputEmpty : base output = [])
    (sameLengths : ∀ k, (base k).length = (middle.stk k).length)
    (finishRun : StateTransition.EvalsToInTime tm.step middle (some finish)
      (SourceRuntimeFinish.finishCost clearKeys accumulator base)) :
    StateTransition.EvalsToInTime tm.step (initList tm input) (some finish)
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishCost