Hoare contracts through work-tape placement

⚠️ Unreviewed by Bolton

A stage of a larger machine is a small machine placed in a block of the layout's tapes. Its contract should travel with it: what it promises about its own tapes should become a promise about the block, and the tapes on either side should come back untouched.

That is the rule below. The frame it carries is the one TM.placeWorkTM needs anyway — every tape outside the block is start-invariant with its head off the marker, so the placed machine's structurally mandatory idle writes leave it exactly as it was.

Main results

• TM.placeWorkTM_hoareTime — a placed stage's contract, with the surrounding tapes framed

theorem Complexity.TM.placeWorkTM_hoareTime {n : ℕ} (tm : TM n) {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (pre₀ post₀ : ℕ) (extras : Fin (pre₀ + n + post₀) → Tape) (hinv : ∀ (i : Fin (pre₀ + n + post₀)), ¬placeWorkInMiddle pre₀ n i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre₀ + n + post₀)), ¬placeWorkInMiddle pre₀ n i → 1 ≤ (extras i).head) : (placeWorkTM pre₀ post₀ tm).HoareTime (fun (inp : Tape) (work : Fin (pre₀ + n + post₀) → Tape) (out : Tape) => (∀ (i : Fin (pre₀ + n + post₀)), ¬placeWorkInMiddle pre₀ n i → work i = extras i) ∧ pre inp (fun (j : Fin n) => work (placeWorkIdx pre₀ post₀ j)) out) (fun (inp : Tape) (work : Fin (pre₀ + n + post₀) → Tape) (out : Tape) => (∀ (i : Fin (pre₀ + n + post₀)), ¬placeWorkInMiddle pre₀ n i → work i = extras i) ∧ post inp (fun (j : Fin n) => work (placeWorkIdx pre₀ post₀ j)) out) b

A placed stage keeps its contract, and its neighbours. The precondition asks that the tapes outside the block are the given frame and that the block satisfies the stage's own precondition; the postcondition returns the frame unchanged and the stage's postcondition on the block.