The assembled simulation

The dispatch phase (DescriptiveComplexity.HaltHard.sim_norm) and the six pops of SimRet.lean assemble into the correctness statement of the simulating machine: from the resting configuration of a continuation k and value v, the machine reaches an accepting configuration exactly when the abstract evaluation Turing.ToPartrec.Cont.eval of k on v terminates (DescriptiveComplexity.HaltHard.reach_acc_iff_evalDom).

The two directions meet at DescriptiveComplexity.HaltHard.popTarget, the continuation and value the machine rests at after one pop – Turing.ToPartrec.stepRet, one frame at a time. The machine side is DescriptiveComplexity.HaltHard.cycle_counted: a counted run from rest to the rest of the pop target. Its count is positive whenever the pop dispatches a code – the run factors through a dispatch configuration whose state is not the resting state – and the two pops that may in principle be silent (cons₂, and fix on a zero flag) shrink the continuation instead, so both directions recurse along the lexicographic order on (steps, continuation size): forward on the abstract step count, since those two pops do not consume an abstract step, and backward on the machine step count, split along the cycle by determinism (DescriptiveComplexity.HaltHard.stepsTo_det). The abstract side of each pop is DescriptiveComplexity.HaltHard.stepRet_popTarget, and termination of the abstract machine is traded for termination of Turing.ToPartrec.Cont.eval through Turing.ToPartrec.stepRet_eval.

The pop target

def DescriptiveComplexity.HaltHard.popTarget {c : Turing.ToPartrec.Code} : PCont c → List ℕ → PCont c × List ℕ

The pop target: the continuation and value the machine rests at after popping the top frame of k with value v – Turing.ToPartrec.stepRet, one frame at a time, with the dispatches it triggers carried out by DescriptiveComplexity.HaltHard.pStepNormal. On the empty continuation the machine accepts instead, so that case is junk.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.HaltHard.popTarget DescriptiveComplexity.HaltHard.PCont.halt x✝ = (DescriptiveComplexity.HaltHard.PCont.halt, x✝)
• DescriptiveComplexity.HaltHard.popTarget (DescriptiveComplexity.HaltHard.PCont.cons₁ p as k) x✝ = DescriptiveComplexity.HaltHard.pStepNormal p (DescriptiveComplexity.HaltHard.PCont.cons₂ x✝ k) as
• DescriptiveComplexity.HaltHard.popTarget (DescriptiveComplexity.HaltHard.PCont.cons₂ ns k) x✝ = (k, ns.headI :: x✝)
• DescriptiveComplexity.HaltHard.popTarget (DescriptiveComplexity.HaltHard.PCont.comp p k) x✝ = DescriptiveComplexity.HaltHard.pStepNormal p k x✝

theorem DescriptiveComplexity.HaltHard.stepRet_popTarget {c : Turing.ToPartrec.Code} {k : PCont c} (hk : k ≠ PCont.halt) (v : List ℕ) : Turing.ToPartrec.stepRet k.toCont v = Turing.ToPartrec.Cfg.ret (popTarget k v).1.toCont (popTarget k v).2 ∨ Turing.ToPartrec.stepRet k.toCont v = Turing.ToPartrec.stepRet (popTarget k v).1.toCont (popTarget k v).2 ∧ sizeOf (popTarget k v).1 < sizeOf k

One abstract step reaches the pop target: Turing.ToPartrec.stepRet on k and v is either the Turing.ToPartrec.Cfg.ret of the pop target – when the pop dispatches a code – or, for the two silent pops, definitionally the stepRet of the pop target, whose continuation is then smaller.

Termination of the abstract machine, as counted runs

def DescriptiveComplexity.HaltHard.ASteps : ℕ → Turing.ToPartrec.Cfg → Turing.ToPartrec.Cfg → Prop

Counted runs of the abstract machine Turing.ToPartrec.step.

Equations

• DescriptiveComplexity.HaltHard.ASteps 0 x✝¹ x✝ = (x✝¹ = x✝)
• DescriptiveComplexity.HaltHard.ASteps n.succ x✝¹ x✝ = ∃ (d : Turing.ToPartrec.Cfg), Turing.ToPartrec.step x✝¹ = some d ∧ DescriptiveComplexity.HaltHard.ASteps n d x✝

theorem DescriptiveComplexity.HaltHard.ASteps.trans_step {n : ℕ} {a b d : Turing.ToPartrec.Cfg} : ASteps n a b → Turing.ToPartrec.step b = some d → ASteps (n + 1) a d

A counted abstract run, extended by one step at its end.

theorem DescriptiveComplexity.HaltHard.asteps_of_reaches {a b : Turing.ToPartrec.Cfg} (h : StateTransition.Reaches Turing.ToPartrec.step a b) : ∃ (n : ℕ), ASteps n a b

An abstract reachability is a counted run of some length.

theorem DescriptiveComplexity.HaltHard.exists_asteps_halt_of_dom {K : Turing.ToPartrec.Cont} {v : List ℕ} (h : (K.eval v).Dom) : ∃ (N : ℕ) (w : List ℕ), ASteps N (Turing.ToPartrec.Cfg.ret K v) (Turing.ToPartrec.Cfg.halt w)

Termination of Turing.ToPartrec.Cont.eval yields a counted abstract run from the return configuration to a halting configuration.

Transfer of termination along one pop

theorem DescriptiveComplexity.HaltHard.contEval_dom_iff_evalStep {K : Turing.ToPartrec.Cont} {v : List ℕ} : (K.eval v).Dom ↔ (StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepRet K v)).Dom

Termination of Turing.ToPartrec.Cont.eval is termination of the sequential run from the return configuration.

theorem DescriptiveComplexity.HaltHard.evalStep_ret (K : Turing.ToPartrec.Cont) (v : List ℕ) : StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.Cfg.ret K v) = StateTransition.eval Turing.ToPartrec.step (Turing.ToPartrec.stepRet K v)

Peeling the one step a return configuration always makes.

theorem DescriptiveComplexity.HaltHard.dom_popTarget {c : Turing.ToPartrec.Code} {k : PCont c} (hk : k ≠ PCont.halt) (v : List ℕ) : ((popTarget k v).1.toCont.eval (popTarget k v).2).Dom ↔ (k.toCont.eval v).Dom

Termination transfers along one pop: the abstract evaluation of a nonempty continuation terminates exactly when that of its pop target does.

The machine cycle

theorem DescriptiveComplexity.HaltHard.lstep_acc {c : Turing.ToPartrec.Code} {x : LCfg c} (hx : x.q = SimQ.acc) : lstep x = none

Accepting configurations are terminal.

theorem DescriptiveComplexity.HaltHard.cycle_counted {c : Turing.ToPartrec.Code} {k : PCont c} (hk : k ≠ PCont.halt) {fr : List (SimSym c)} (hfr : FrameSeg k fr) (g : ℕ) (v : List ℕ) (j t : ℕ) : ∃ (m : ℕ) (g' : ℕ) (fr' : List (SimSym c)) (j' : ℕ) (t' : ℕ), FrameSeg (popTarget k v).1 fr' ∧ stepsTo m (restCfg g fr v j t) (restCfg g' fr' (popTarget k v).2 j' t') ∧ (m = 0 → sizeOf (popTarget k v).1 < sizeOf k)

The counted machine cycle: from the resting configuration of a nonempty continuation, a counted run to the resting configuration of the pop target. The count is zero only if the pop was silent, in which case the continuation shrank – the escape hatch both lexicographic inductions use.

The two directions

theorem DescriptiveComplexity.HaltHard.reach_acc_of_asteps {c : Turing.ToPartrec.Code} (N : ℕ) (k : PCont c) (v w : List ℕ) (hN : ASteps N (Turing.ToPartrec.Cfg.ret k.toCont v) (Turing.ToPartrec.Cfg.halt w)) (g : ℕ) (fr : List (SimSym c)) (hfr : FrameSeg k fr) (j t : ℕ) : ∃ (x : LCfg c), x.q = SimQ.acc ∧ Reach (restCfg g fr v j t) x

Forward simulation: if the abstract machine halts from the return configuration of k and v in N steps, the simulating machine accepts from the resting configuration of any frame region of k, by lexicographic recursion on (N, sizeOf k) – the two silent pops keep N and shrink k.

theorem DescriptiveComplexity.HaltHard.dom_of_stepsTo_acc {c : Turing.ToPartrec.Code} (N : ℕ) (k : PCont c) (v : List ℕ) (g : ℕ) (fr : List (SimSym c)) (j t : ℕ) (x : LCfg c) (hfr : FrameSeg k fr) (hN : stepsTo N (restCfg g fr v j t) x) (hx : x.q = SimQ.acc) : (k.toCont.eval v).Dom

Backward simulation: if the simulating machine accepts from the resting configuration of k and v in N steps, the abstract evaluation of k on v terminates, by lexicographic recursion on (N, sizeOf k) – the counted cycle is split off the accepting run by determinism, and a silent cycle shrinks k.

The correctness statement

theorem DescriptiveComplexity.HaltHard.reach_acc_iff_evalDom {c : Turing.ToPartrec.Code} {k : PCont c} {fr : List (SimSym c)} (hfr : FrameSeg k fr) (g : ℕ) (v : List ℕ) (j t : ℕ) : (∃ (x : LCfg c), x.q = SimQ.acc ∧ Reach (restCfg g fr v j t) x) ↔ (k.toCont.eval v).Dom

Correctness of the simulating machine: from the resting configuration of a continuation k and value v, the machine reaches an accepting configuration exactly when Turing.ToPartrec.Cont.eval of k on v terminates.