StackSimulation.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite-control compilation of stack programs, with an explicit tape encoding.

lemma OAI.RationalHitting.TMTime.StackToOne.go_time line 12
lemma OAI.RationalHitting.TMTime.StackToOne.return_time line 26
def OAI.RationalHitting.TMTime.StackToOne.stackWeight line 44
lemma OAI.RationalHitting.TMTime.StackToOne.stackWeight_run line 50
lemma OAI.RationalHitting.TMTime.StackToOne.stWrite_length line 56
lemma OAI.RationalHitting.TMTime.StackToOne.updated_length line 61

theorem OAI.RationalHitting.TMTime.StackToOne.continuation_time line 74

Source documentation

Real TM1 transition count for the compiled continuation of a TM2 statement. The multipliers count sweeps to and from actual stack tops.

theorem continuation_time (q : TM2.Stmt Γ Λ σ) (v : σ)
    (S : ∀ k, List (Γ k)) (T : ListBlank (∀ k, Option (Γ k))) (L : ℕ)
    (hT : ∀ k, T.map (proj k) = ListBlank.mk ((S k).map some).reverse)
    (hS : ∀ k, (S k).length ≤ L) :
    ∃ u b, u ≤ stackWeight q*(2*(L+stackWeight q)+3) ∧
      TrCfg (TM2.stepAux q v S) b ∧
      exec (TM1.step (tr M)) u (TM1.stepAux (trNormal q) v (Tape.mk' ∅ (addBottom T))) = some b := by
…

Mentions: OAI.RationalHitting.TMTime.StackToOne.stackWeight, OAI.RationalHitting.TMTime.exec

lemma OAI.RationalHitting.TMTime.StackToOne.statement_length line 133
theorem OAI.RationalHitting.TMTime.StackToOne.step_time line 153

theorem OAI.RationalHitting.TMTime.StackToOne.execution_time line 172

Source documentation

A bounded TM2 run on stacks of initial length <=L is simulated by Mathlib's single tape TM1 interpreter in at most C*t*(2*(L+C*t)+4) macro-transitions. C is a fixed syntactic maximum over the finite program, not input advice.

theorem execution_time [Inhabited Λ] (F : Finset Λ) (hF : TM2.Supports M F)
    (C : ℕ) (hC : ∀ l ∈ F, stackWeight (M l)+1 ≤ C)
    (t : ℕ) (a b : TM2.Cfg Γ Λ σ)
    (a' : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ) (L : ℕ)
    (ha : a.l ∈ Finset.insertNone F) (hS : ∀ k, (a.stk k).length ≤ L)
    (htr : TrCfg a a') (hr : exec (TM2.step M) t a = some b) :
    ∃ u b', u ≤ C*t*(2*(L+C*t)+4) ∧ TrCfg b b' ∧
      exec (TM1.step (tr M)) u a' = some b' := by
…

Mentions: OAI.RationalHitting.TMTime.StackToOne.stackWeight, OAI.RationalHitting.TMTime.exec

theorem OAI.RationalHitting.TMTime.StackToOne.halts line 210
def OAI.RationalHitting.TMTime.FiniteStates.stateEncode line 223
def OAI.RationalHitting.TMTime.FiniteStates.stateDecode line 226
lemma OAI.RationalHitting.TMTime.FiniteStates.stateEncode_default line 229
lemma OAI.RationalHitting.TMTime.FiniteStates.stateDecode_encode line 232
def OAI.RationalHitting.TMTime.FiniteStates.machine line 238
def OAI.RationalHitting.TMTime.FiniteStates.cfg line 242
lemma OAI.RationalHitting.TMTime.FiniteStates.step_cfg line 245
lemma OAI.RationalHitting.TMTime.FiniteStates.cfg_init line 251
lemma OAI.RationalHitting.TMTime.FiniteStates.execution line 255
lemma OAI.RationalHitting.TMTime.FiniteStates.run_support line 270

theorem OAI.RationalHitting.TMTime.FiniteStates.finite_machine line 282

Source documentation

Finite-support compression has no transition or tape overhead.

theorem finite_machine (M : TM0.Machine Γ Λ) (S : Finset Λ)
    (hs : TM0.Supports M (S : Set Λ)) :
    ∃ (m : ℕ) (G : TM0.Machine Γ (Fin (m+1))), ∀ (l : List Γ) (t : ℕ) (a : TM0.Cfg Γ Λ),
      exec (TM0.step M) t (TM0.init l)=some a → TM0.step M a=none →
      ∃ b : TM0.Cfg Γ (Fin (m+1)), exec (TM0.step G) t (TM0.init l)=some b ∧
        TM0.step G b=none ∧ b.Tape=a.Tape := by
…

Mentions: OAI.RationalHitting.TMTime.exec