Fixed-environment transport for bounded memory-client loops

Equal body programs at two fixed environments give equal bounded iterations. Pointwise equal body-work charges and equivalent body domains likewise transport the iteration's work and safety conditions along its actual reached memory states. These are semantic laws of the existing free programs: they need no fit, history or resource assumptions.

Main results

• iterate_comap: pull a loop body back along a map of its environment.
• iterate_congr: equal bodies at fixed environments give equal iterations.
• iterationSafe_congr: transport iteration domains between agreeing bodies and environments.
• iterationWork_congr: transport local work between agreeing bodies and environments.

The transport rules are original infrastructure over the existing memory-client loops.

theorem Cslib.WordRAM.Realization.iterate_comap {δ ε σ : Type} (g : ε → δ) (body : δ × σ → DataStructure.Memory.Prog σ) (e : ε) (n : ℕ) (a : σ) : iterate body (g e) n a = iterate (fun (x : ε × σ) => body (g x.1, x.2)) e n a

A loop may receive any function of its environment: it is the loop over the whole environment whose body applies that function.

theorem Cslib.WordRAM.Realization.iterate_congr {δ σ δ' : Type} {body : δ × σ → DataStructure.Memory.Prog σ} {body' : δ' × σ → DataStructure.Memory.Prog σ} {d : δ} {d' : δ'} (hbody : ∀ (a : σ), body (d, a) = body' (d', a)) (n : ℕ) (a : σ) : iterate body d n a = iterate body' d' n a

Equal body programs at fixed environments give equal bounded iterations, including their complete memory histories.

theorem Cslib.WordRAM.Realization.iterationSafe_congr {δ σ δ' : Type} {body : δ × σ → DataStructure.Memory.Prog σ} {body' : δ' × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} {safe' : ℕ → δ' × σ → DataStructure.Memory.State → Prop} {w : ℕ} {d : δ} {d' : δ'} (hbody : ∀ (a : σ), body (d, a) = body' (d', a)) (hsafe : ∀ (a : σ) (s : DataStructure.Memory.State), safe w (d, a) s ↔ safe' w (d', a) s) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : iterationSafe body safe w d n a s ↔ iterationSafe body' safe' w d' n a s

Iteration domains agree when the bodies and their domains agree at fixed environments.

theorem Cslib.WordRAM.Realization.iterationWork_congr {δ σ δ' : Type} {body : δ × σ → DataStructure.Memory.Prog σ} {body' : δ' × σ → DataStructure.Memory.Prog σ} {work : δ × σ → DataStructure.Memory.State → ℕ} {work' : δ' × σ → DataStructure.Memory.State → ℕ} {d : δ} {d' : δ'} (hbody : ∀ (a : σ), body (d, a) = body' (d', a)) (hwork : ∀ (a : σ) (s : DataStructure.Memory.State), work (d, a) s = work' (d', a) s) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : iterationWork body work d n a s = iterationWork body' work' d' n a s

The local work is invariant under agreeing bodies and body charges at their environments.