The bounded closure loop

tcCode decides bounded reachability of a target tuple from a source tuple along the edges computed by compiled body code, in a universe of size n. It keeps the current tuple and a step counter, tests the current tuple against the target, guesses a successor below n ^ k, decodes its base-n digits, runs the body, and counts the step; it rejects once the counter reaches the value M₀ of the step-bound expression. Every branch therefore halts, and the loop certifies exactly the paths of at most M₀ steps. Closures use M₀ = n ^ k; inductive counting uses smaller bounds.

Main results

• Cslib.Logic.FO.Ordered.TCModelChecker.loop_sound: every branch rejects or reaches the exit with the target reachable within M₀ steps.
• Cslib.Logic.FO.Ordered.TCModelChecker.loop_complete: a path of at most M₀ steps gives a branch reaching the exit.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.reaches_digits {P : Turing.CounterProgram} {w : List Bool} {B b r d k n : ℕ} (hP : P.CodeAt b (assignChain b d k (ClosureKernel.digitE r))) (hrd : r < d ∨ d + k ≤ r) (hd : 0 < d) {regs : List ℕ} (hlen : d + k ≤ regs.length) (h0 : regs.getD 0 0 = n) (hnB : n ≤ B) (hB : ∀ x ∈ regs, x ≤ B) (g : Fin (n ^ k)) (hg : regs.getD r 0 = ↑g) : ∃ (regs' : List ℕ), P.Reaches w (P.Oblivious B) (b, 0 :: regs) (b + k, 0 :: regs') ∧ regs'.length = regs.length ∧ (∀ (j : ℕ), j < d ∨ d + k ≤ j → regs'.getD j 0 = regs.getD j 0) ∧ (∀ (i : Fin k), regs'.getD (d + ↑i) 0 = ↑(finFunctionFinEquiv.symm g i)) ∧ ∀ x ∈ regs', x ≤ B

Decoding register r, holding g < n ^ k, into registers d + i writes the tuple finFunctionFinEquiv.symm g.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.tcCode_parts {P : Turing.CounterProgram} {b base k : ℕ} {src dst : Fin k → Turing.CounterProgram.Expr} {M : Turing.CounterProgram.Expr} {body : List Turing.CounterProgram.Instr} {T R : ℕ} (hP : P.CodeAt b (tcCode b base k src dst M body T R)) : P.CodeAt b (assignChain b base k fun (i : ℕ) => if h : i < k then src ⟨i, h⟩ else Turing.CounterProgram.Expr.const 0) ∧ P.instr (b + k) = (Turing.CounterProgram.Instr.assign (base + 2 * k + 1) (Turing.CounterProgram.Expr.const 0) (b + k + 1)).shift ∧ P.instr (b + k + 1) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.const 0) (ClosureKernel.testExpr base k dst) (b + k + 2) T).shift ∧ P.instr (b + k + 2) = (Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg (base + 2 * k + 1)) M (b + k + 3) R).shift ∧ P.CodeAt (b + k + 3) (Turing.CounterProgram.Block.guessCode (b + k + 3) (base + 2 * k) ((Turing.CounterProgram.Expr.reg 0).pow k) (b + k + 7) R) ∧ P.CodeAt (b + k + 7) (assignChain (b + k + 7) (base + k) k (ClosureKernel.digitE (base + 2 * k))) ∧ P.CodeAt (b + 2 * k + 7) body ∧ P.CodeAt (b + 2 * k + 7 + body.length) (assignChain (b + 2 * k + 7 + body.length) base k fun (i : ℕ) => Turing.CounterProgram.Expr.reg (base + k + i)) ∧ P.instr (b + 3 * k + 7 + body.length) = (Turing.CounterProgram.Instr.assign (base + 2 * k + 1) ((Turing.CounterProgram.Expr.reg (base + 2 * k + 1)).add (Turing.CounterProgram.Expr.const 1)) (b + k + 1)).shift

structure Cslib.Logic.FO.Ordered.TCModelChecker.LoopInv (n B base k : ℕ) (regs₀ : List ℕ) (us : Fin k → Fin n) (t : ℕ) (regs : List ℕ) : Prop

The loop invariant at the test label: registers below base and the length are kept, the current tuple is in registers base + i, and the step counter is t.

• kept : Turing.CounterProgram.Kept B base regs₀ regs

  The registers below base and the length are kept, and every register is bounded.

• le_length : base + 2 * k + 2 ≤ regs.length

  The loop's registers exist.

• cur (i : Fin k) : regs.getD (base + ↑i) 0 = ↑(us i)

  The current tuple is in registers base + i.

• counter : regs.getD (base + 2 * k + 1) 0 = t

  The step counter is in register base + 2 * k + 1.

structure Cslib.Logic.FO.Ordered.TCModelChecker.LoopMid (n B base k : ℕ) (regs₀ : List ℕ) (us ws : Fin k → Fin n) (t : ℕ) (regs : List ℕ) extends Cslib.Logic.FO.Ordered.TCModelChecker.LoopInv n B base k regs₀ us t regs : Prop

The state after decoding a successor: the loop invariant, the decoded tuple in registers base + k + i.

• kept : Turing.CounterProgram.Kept B base regs₀ regs
• le_length : base + 2 * k + 2 ≤ regs.length
• cur (i : Fin k) : regs.getD (base + ↑i) 0 = ↑(us i)
• counter : regs.getD (base + 2 * k + 1) 0 = t
• next (i : Fin k) : regs.getD (base + k + ↑i) 0 = ↑(ws i)

  The decoded successor is in registers base + k + i.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.loop_init {P : Turing.CounterProgram} {w : List Bool} {n B b base k T R : ℕ} {src dst : Fin k → Turing.CounterProgram.Expr} {M : Turing.CounterProgram.Expr} {body : List Turing.CounterProgram.Instr} {regs₀ : List ℕ} (hP : P.CodeAt b (tcCode b base k src dst M body T R)) (hlen : base + 2 * k + 2 ≤ regs₀.length) (hnB : n ≤ B) (hB : ∀ r ∈ regs₀, r ≤ B) {s₀ : Fin k → Fin n} (hsrc : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (i : Fin k), Turing.CounterProgram.Expr.eval regs (src i) = ↑(s₀ i)) : ∃ (regs : List ℕ), P.Reaches w (P.Oblivious B) (b, 0 :: regs₀) (b + k + 1, 0 :: regs) ∧ LoopInv n B base k regs₀ s₀ 0 regs

Initialization: copy the source tuple and reset the step counter.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.loop_sound {P : Turing.CounterProgram} {w : List Bool} {n B b base k T R : ℕ} {Post : Turing.CounterProgram.Config → Prop} {src dst : Fin k → Turing.CounterProgram.Expr} {M : Turing.CounterProgram.Expr} {body : List Turing.CounterProgram.Instr} {regs₀ : List ℕ} {M₀ : ℕ} {z₀ : Fin k → Fin n} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} {s₀ : Fin k → Fin n} (hP : P.CodeAt b (tcCode b base k src dst M body T R)) (hbase : 0 < base) (hB1 : 1 ≤ B) (hnB : n ≤ B) (hNB : n ^ k ≤ B) (hMB : M₀ ≤ B) (h0 : regs₀.getD 0 0 = n) (hR : (P.instr R).halts = true) (hPost : ∀ (s : Turing.CounterProgram.Config), s.1 = R → Post s) (hdst : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (i : Fin k), Turing.CounterProgram.Expr.eval regs (dst i) = ↑(z₀ i)) (hM : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → Turing.CounterProgram.Expr.eval regs M = M₀) (hbody : ∀ (us ws : Fin k → Fin n) (t : ℕ) (regs₃ : List ℕ), LoopMid n B base k regs₀ us ws t regs₃ → Turing.CounterProgram.Block.Sound P w B Post (b + 2 * k + 7) regs₃ (b + 2 * k + 7 + body.length) fun (regs' : List ℕ) => Turing.CounterProgram.Kept B (base + 2 * k + 2) regs₃ regs' ∧ E us ws) (e t : ℕ) (us : Fin k → Fin n) (regs : List ℕ) : M₀ - t = e → t ≤ M₀ → LoopInv n B base k regs₀ us t regs → Relation.RelatesWithinSteps E s₀ us t → Turing.CounterProgram.Block.Sound P w B Post (b + k + 1) regs T fun (regs' : List ℕ) => Turing.CounterProgram.Kept B base regs₀ regs' ∧ Relation.RelatesWithinSteps E s₀ z₀ M₀

Soundness of the closure loop: from a state with step counter t ≤ M₀ and current tuple reachable from s₀ within t steps, every branch either rejects or reaches T with the target z₀ reachable from s₀ within M₀ steps.

theorem Cslib.Logic.FO.Ordered.TCModelChecker.loop_complete {P : Turing.CounterProgram} {w : List Bool} {n B b base k T R : ℕ} {src dst : Fin k → Turing.CounterProgram.Expr} {M : Turing.CounterProgram.Expr} {body : List Turing.CounterProgram.Instr} {regs₀ : List ℕ} {M₀ : ℕ} {z₀ : Fin k → Fin n} {E : (Fin k → Fin n) → (Fin k → Fin n) → Prop} (hP : P.CodeAt b (tcCode b base k src dst M body T R)) (hbase : 0 < base) (hnB : n ≤ B) (hNB : n ^ k ≤ B) (hMB : M₀ ≤ B) (h0 : regs₀.getD 0 0 = n) (hdst : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → ∀ (i : Fin k), Turing.CounterProgram.Expr.eval regs (dst i) = ↑(z₀ i)) (hM : ∀ (regs : List ℕ), (∀ j < base, regs.getD j 0 = regs₀.getD j 0) → Turing.CounterProgram.Expr.eval regs M = M₀) (hbody : ∀ (us ws : Fin k → Fin n) (t : ℕ) (regs₃ : List ℕ), LoopMid n B base k regs₀ us ws t regs₃ → E us ws → Turing.CounterProgram.Block.Complete P w (b + 2 * k + 7) regs₃ (b + 2 * k + 7 + body.length) (Turing.CounterProgram.Kept B (base + 2 * k + 2) regs₃)) (m t : ℕ) (us : Fin k → Fin n) (regs : List ℕ) : Relation.RelatesInSteps E us z₀ m → t + m ≤ M₀ → LoopInv n B base k regs₀ us t regs → Turing.CounterProgram.Block.Complete P w (b + k + 1) regs T (Turing.CounterProgram.Kept B base regs₀)

Completeness of the closure loop: from a state with step counter t, a path of m steps to the target with t + m ≤ M₀ gives a branch reaching T.