Sound and complete blocks of nondeterministic counter code

Compositional reasoning for nondeterministic counter programs whose choice bit is register 0. Block.Sound P w B Post l regs T G says that every branch from label l, with registers regs above the choice, halts in a configuration satisfying Post or reaches label T with registers satisfying G, keeping all registers at most B. Block.Complete P w l regs T G says that, whatever the current choice bit, some branch reaches T with registers satisfying G. Both compose sequentially and absorb shifted deterministic code; guessCode guesses a register value below a bound.

Main definitions

• Turing.CounterProgram.Block.Sound, Turing.CounterProgram.Block.Complete: block contracts.
• Turing.CounterProgram.Block.guessCode: nondeterministically guess a bounded value.

Main results

• Turing.CounterProgram.Block.Sound.bind, Turing.CounterProgram.Block.Complete.bind: sequential composition.
• Turing.CounterProgram.Block.Sound.guess, Turing.CounterProgram.Block.Complete.guess: the guessed value is any number below the bound.

def Turing.CounterProgram.Block.Sound (P : CounterProgram) (w : List Bool) (B : ℕ) (Post : Config → Prop) (l : ℕ) (regs : List ℕ) (T : ℕ) (G : List ℕ → Prop) : Prop

Sound l regs T G: from the label l with the registers regs above the choice, every branch halts satisfying Post or reaches the label T with registers satisfying G above the choice, keeping its registers at most B.

def Turing.CounterProgram.Block.Complete (P : CounterProgram) (w : List Bool) (l : ℕ) (regs : List ℕ) (T : ℕ) (G : List ℕ → Prop) : Prop

Complete l regs T G: from the label l with the registers regs above the choice, whatever the choice, some branch reaches the label T with registers satisfying G above the choice.

theorem Turing.CounterProgram.Block.instr_of_eq {P : CounterProgram} {l l' : ℕ} {i : Instr} (h : P.instr l = i) (hl : l = l') : P.instr l' = i

Transport an instruction fact along an equality of labels, for labels computed by omega.

theorem Turing.CounterProgram.Block.codeAt_of_eq {P : CounterProgram} {l l' : ℕ} {c : List Instr} (h : P.CodeAt l c) (hl : l = l') : P.CodeAt l' c

Transport a code-placement fact along an equality of labels.

theorem Turing.CounterProgram.Reaches.sassign {P : CounterProgram} {w : List Bool} {B c l i next : ℕ} {e : Expr} {regs : List ℕ} {s' : Config} (hl : P.instr l = (Instr.assign i e next).shift) (hc : c ≤ B) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Oblivious B) (next, c :: regs.set i (Expr.eval regs e)) s') : P.Reaches w (P.Oblivious B) (l, c :: regs) s'

theorem Turing.CounterProgram.Reaches.slt {P : CounterProgram} {w : List Bool} {B c l yes no : ℕ} {x y : Expr} {regs : List ℕ} {s' : Config} (hl : P.instr l = (Instr.lt x y yes no).shift) (hc : c ≤ B) (hB : ∀ r ∈ regs, r ≤ B) (h : P.Reaches w (P.Oblivious B) (if Expr.eval regs x < Expr.eval regs y then yes else no, c :: regs) s') : P.Reaches w (P.Oblivious B) (l, c :: regs) s'

theorem Turing.CounterProgram.Block.Sound.bind {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {l T T' : ℕ} {regs : List ℕ} {G G' : List ℕ → Prop} (h : Sound P w B Post l regs T G) (h' : ∀ (regs' : List ℕ), G regs' → Sound P w B Post T regs' T' G') : Sound P w B Post l regs T' G'

theorem Turing.CounterProgram.Block.Sound.mono {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {l T : ℕ} {regs : List ℕ} {G G' : List ℕ → Prop} (h : Sound P w B Post l regs T G) (hG : ∀ (regs' : List ℕ), G regs' → G' regs') : Sound P w B Post l regs T G'

theorem Turing.CounterProgram.Block.Sound.exit {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {l : ℕ} {regs : List ℕ} {G : List ℕ → Prop} (hG : G regs) : Sound P w B Post l regs l G

theorem Turing.CounterProgram.Block.Sound.halt {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {l T : ℕ} {regs : List ℕ} {G : List ℕ → Prop} (hB : 1 ≤ B) (hl : (P.instr l).halts = true) (hPost : ∀ (c : Bool), Post (l, c.toNat :: regs)) (hregs : ∀ r ∈ regs, r ≤ B) : Sound P w B Post l regs T G

A halting label satisfying Post.

theorem Turing.CounterProgram.Block.Sound.of_oblivious {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {l T : ℕ} {regs : List ℕ} {G : List ℕ → Prop} (hB : 1 ≤ B) {l' : ℕ} {regs' : List ℕ} (hr' : P.Reaches w (P.Oblivious B) (l, 0 :: regs) (l', 0 :: regs')) (h : Sound P w B Post l' regs' T G) : Sound P w B Post l regs T G

Oblivious deterministic code, above the choice.

theorem Turing.CounterProgram.Block.Sound.of_reaches {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {l T : ℕ} {regs : List ℕ} {G : List ℕ → Prop} (hB : 1 ≤ B) {b : ℕ} {code : List Instr} (hP : P.CodeAt b (List.map Instr.shift code)) {l' : ℕ} {regs' : List ℕ} (hr : (padded b code).Reaches w ((padded b code).Running B) (l, regs) (l', regs')) (h : Sound P w B Post l' regs' T G) : Sound P w B Post l regs T G

Deterministic code placed by padded, shifted above the choice.

theorem Turing.CounterProgram.Block.Sound.choice {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} {l T : ℕ} {regs : List ℕ} {G : List ℕ → Prop} (hB : 1 ≤ B) {yes no : ℕ} (hl : P.instr l = Instr.lt (Expr.reg 0) (Expr.const 1) yes no) (hregs : ∀ r ∈ regs, r ≤ B) (hyes : Sound P w B Post yes regs T G) (hno : Sound P w B Post no regs T G) : Sound P w B Post l regs T G

A choice: the label yes on the choice false, and no on true.

theorem Turing.CounterProgram.Block.Complete.refl {P : CounterProgram} {w : List Bool} {l : ℕ} {regs : List ℕ} {G : List ℕ → Prop} (hG : G regs) : Complete P w l regs l G

theorem Turing.CounterProgram.Block.Complete.mono {P : CounterProgram} {w : List Bool} {l T : ℕ} {regs : List ℕ} {G G' : List ℕ → Prop} (h : Complete P w l regs T G) (hG : ∀ (regs' : List ℕ), G regs' → G' regs') : Complete P w l regs T G'

theorem Turing.CounterProgram.Block.Complete.bind {P : CounterProgram} {w : List Bool} {l T T' : ℕ} {regs : List ℕ} {G G' : List ℕ → Prop} (h : Complete P w l regs T G) (h' : ∀ (regs' : List ℕ), G regs' → Complete P w T regs' T' G') : Complete P w l regs T' G'

theorem Turing.CounterProgram.Block.Complete.of_oblivious {P : CounterProgram} {w : List Bool} {l T : ℕ} {regs : List ℕ} {G : List ℕ → Prop} {B l' : ℕ} {regs' : List ℕ} (hr' : P.Reaches w (P.Oblivious B) (l, 0 :: regs) (l', 0 :: regs')) (h : Complete P w l' regs' T G) : Complete P w l regs T G

Oblivious deterministic code, above the choice.

theorem Turing.CounterProgram.Block.Complete.of_reaches {P : CounterProgram} {w : List Bool} {l T : ℕ} {regs : List ℕ} {G : List ℕ → Prop} {B b : ℕ} {code : List Instr} (hP : P.CodeAt b (List.map Instr.shift code)) {l' : ℕ} {regs' : List ℕ} (hr : (padded b code).Reaches w ((padded b code).Running B) (l, regs) (l', regs')) (h : Complete P w l' regs' T G) : Complete P w l regs T G

Deterministic code placed by padded, shifted above the choice.

theorem Turing.CounterProgram.Block.Complete.choice {P : CounterProgram} {w : List Bool} {l T : ℕ} {regs : List ℕ} {G : List ℕ → Prop} {B l' : ℕ} {regs' : List ℕ} (hr' : P.Reaches w (P.Oblivious B) (l, 0 :: regs) (l', 0 :: regs')) (hne : l ≠ l') {yes no : ℕ} (hl : P.instr l' = Instr.lt (Expr.reg 0) (Expr.const 1) yes no) (h : Complete P w yes regs' T G ∨ Complete P w no regs' T G) : Complete P w l regs T G

A step of deterministic code into a choice, then the branch of either label.

def Turing.CounterProgram.Block.guessCode (b x : ℕ) (N : Expr) (E R : ℕ) : List Instr

A guess of register x (above the choice) below the value of N: set it to 0, then while it is below N, either stop at E or increment it; reject at R when it reaches N.

theorem Turing.CounterProgram.Block.length_guessCode (b x : ℕ) (N : Expr) (E R : ℕ) : (guessCode b x N E R).length = 4

theorem Turing.CounterProgram.Block.Sound.guess {P : CounterProgram} {w : List Bool} {B : ℕ} {Post : Config → Prop} (hB : 1 ≤ B) {b x E R : ℕ} {N : Expr} (hP : P.CodeAt b (guessCode b x N E R)) (hR : (P.instr R).halts = true) (hPost : ∀ (s : Config), s.1 = R → Post s) {regs : List ℕ} (hx : x < regs.length) (hN : ∀ (y : ℕ), Expr.eval (regs.set x y) N = Expr.eval regs N) (hNB : Expr.eval regs N ≤ B) (hregs : ∀ r ∈ regs, r ≤ B) : Sound P w B Post b regs E fun (regs' : List ℕ) => ∃ m < Expr.eval regs N, regs' = regs.set x m

Every branch of a guess reaches E with a value below N, or rejects.

theorem Turing.CounterProgram.Block.Complete.guess {P : CounterProgram} {w : List Bool} {B b x E R : ℕ} {N : Expr} (hP : P.CodeAt b (guessCode b x N E R)) {regs : List ℕ} (hx : x < regs.length) (hN : ∀ (y : ℕ), Expr.eval (regs.set x y) N = Expr.eval regs N) (hNB : Expr.eval regs N ≤ B) (hregs : ∀ r ∈ regs, r ≤ B) {m : ℕ} (hm : m < Expr.eval regs N) : Complete P w b regs E fun (x_1 : List ℕ) => x_1 = regs.set x m

Some branch of a guess reaches E with any value below N.