Correctness and linear cost of regular-domain validation

The DFA scan and input rewind leave every work tape and the output empty. The execution phase then reproduces the original machine's complete run.

def Complexity.CslibGuard.baseCfg {k : ℕ} {σ Q : Type} (w : List Bool) (q : Option (State σ Q)) (p : Fin (w.length + 2)) : Turing.Cfg k Bool (State σ Q) w

An otherwise initial configuration at a specified input position and control.

Equations

• Complexity.CslibGuard.baseCfg w q p = { state := q, inputPos := p, workTapes := fun (x : Fin k) (x_1 : ℤ) => none, workTapePos := fun (x : Fin k) => 0, output := [] }

def Complexity.CslibGuard.scanCfg {k : ℕ} {σ Q : Type} (D : DFA Bool σ) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.Cfg k Bool (State σ Q) w

The DFA scan after the first t input bits.

Equations

• Complexity.CslibGuard.scanCfg D w t ht = Complexity.CslibGuard.baseCfg w (some (Complexity.CslibGuard.State.scan (D.eval (List.take t w)))) ⟨t + 1, ⋯⟩

def Complexity.CslibGuard.rewindCfg {k : ℕ} {σ Q : Type} (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.Cfg k Bool (State σ Q) w

Rewinding with the input head at native position t.

Equations

• Complexity.CslibGuard.rewindCfg w t ht = Complexity.CslibGuard.baseCfg w (some Complexity.CslibGuard.State.rewind) ⟨t, ⋯⟩

def Complexity.CslibGuard.liftCfg {k : ℕ} {σ Q : Type} {w : List Bool} (c : Turing.Cfg k Bool Q w) : Turing.Cfg k Bool (State σ Q) w

Embed source execution without changing any tape or head.

Equations

• Complexity.CslibGuard.liftCfg c = Turing.Cfg.mapState (Option.map Complexity.CslibGuard.State.run) c

theorem Complexity.CslibGuard.step_lift {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w : List Bool} (c : Turing.Cfg k Bool Q w) : Turing.MultiTapeTM.step (liftCfg c) = liftCfg (Turing.MultiTapeTM.step c)

theorem Complexity.CslibGuard.run_lift {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w : List Bool} (c : Turing.Cfg k Bool Q w) (t : ℕ) : Turing.MultiTapeTM.runFrom (liftCfg c) t = liftCfg (Turing.MultiTapeTM.runFrom c t)

theorem Complexity.CslibGuard.scan_zero {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) (w : List Bool) : scanCfg D w 0 ⋯ = Turing.MultiTapeTM.initCfg w

theorem Complexity.CslibGuard.scan_step {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) (w : List Bool) (t : ℕ) (ht : t < w.length) : Turing.MultiTapeTM.step (scanCfg D w t ⋯) = scanCfg D w (t + 1) ⋯

theorem Complexity.CslibGuard.run_succ {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w : List Bool} (c : Turing.Cfg k Bool (State σ Q) w) (t : ℕ) : Turing.MultiTapeTM.runFrom c (t + 1) = Turing.MultiTapeTM.step (Turing.MultiTapeTM.runFrom c t)

theorem Complexity.CslibGuard.run_add {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w : List Bool} (c : Turing.Cfg k Bool (State σ Q) w) (t u : ℕ) : Turing.MultiTapeTM.runFrom c (t + u) = Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.runFrom c t) u

theorem Complexity.CslibGuard.run_scan {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) t = scanCfg D w t ht

theorem Complexity.CslibGuard.rewind_step {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) (w : List Bool) (t : ℕ) (ht : t + 1 ≤ w.length) : Turing.MultiTapeTM.step (rewindCfg w (t + 1) ht) = rewindCfg w t ⋯

theorem Complexity.CslibGuard.run_rewind {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.MultiTapeTM.runFrom (rewindCfg w t ht) t = rewindCfg w 0 ⋯

theorem Complexity.CslibGuard.prepare {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w : List Bool} (hw : w ∈ D.accepts) : Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (2 * w.length + 2) = liftCfg (Turing.MultiTapeTM.initCfg w)

theorem Complexity.CslibGuard.rejected {k : ℕ} {σ Q : Type} (M : Turing.MultiTapeTM k Bool Q) (D : DFA Bool σ) {w : List Bool} (hw : w ∉ D.accepts) : (Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (w.length + 1)).state = none ∧ (Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (w.length + 1)).output = []