Uniform sequential realization of memory clients

The continuation has one realization for the environment paired with its runtime answer. Its source registers append the first computation's answer slots to the original inputs. The predecessor's auxiliary words are dead after its answer is available, so the continuation reuses them. Its bank already contains the final output slots, so no result copy is needed. The retained witness gives the concrete scratch, factor and emitter with the existing Spec.

Main definitions

• bindSharedLeft, bindSharedRight: the shared-bank layout for retained binds.
• Realizes.Witness.bind: sequential composition retaining data and sharing dead scratch.

Main results

• bindShared_layout: both stages' register premises from those of the composite bank.
• bindShared_appendWords: the continuation's source bank after the predecessor's frame and output.
• bind_cost_le: additive cost bound under the maximum of two exchange factors.
• Realizes.bind: sequential realization with additive memory and local-work charges.
• Realizes.Witness.bind_execWithin: tighter native budgets on the same supplied emitter.

def Cslib.WordRAM.Realization.bindSharedLeft {m n₂ l n₁ : ℕ} (i : Fin (m + n₂ + 1)) : Fin (m + (l + max n₁ n₂) + 1)

The continuation's prefix in a bind that shares dead predecessor auxiliary words.

def Cslib.WordRAM.Realization.bindSharedRight {m n₂ l n₁ : ℕ} (i : Fin (l + n₁ + 1)) : Fin (m + (l + max n₁ n₂) + 1)

The predecessor's live answer is placed at the tail; its dead auxiliary words share the continuation's prefix. Each stage map is injective, although their union need not be.

theorem Cslib.WordRAM.Realization.bindShared_layout {r k m l n₁ n₂ : ℕ} {frontier : Fin r} {src : Fin k → Fin r} {tmp : Fin (m + (l + max n₁ n₂) + 1) → Fin r} (hi : Function.Injective tmp) (hd : ∀ (i : Fin k) (j : Fin (m + (l + max n₁ n₂) + 1)), src i ≠ tmp j) (hf : ∀ (j : Fin (m + (l + max n₁ n₂) + 1)), tmp j ≠ frontier) (hs : ∀ (i : Fin k), src i ≠ frontier) : Function.Injective (tmp ∘ bindSharedRight) ∧ Function.Injective (tmp ∘ bindSharedLeft) ∧ (∀ (i : Fin (k + l)) (j : Fin (m + n₂ + 1)), Fin.append src (fun (a : Fin l) => tmp (bindSharedRight (Fin.castAdd (n₁ + 1) a))) i ≠ tmp (bindSharedLeft j)) ∧ ∀ (i : Fin (k + l)), Fin.append src (fun (a : Fin l) => tmp (bindSharedRight (Fin.castAdd (n₁ + 1) a))) i ≠ frontier

The register premises of both stages of a shared-bank bind. If the composite bank tmp is injective and avoids the sources src and the frontier, then the predecessor's bank tmp ∘ bindSharedRight and the continuation's bank tmp ∘ bindSharedLeft are injective. The continuation's sources, src followed by the predecessor's live answer slots, avoid its bank and the frontier.

theorem Cslib.WordRAM.Realization.bindShared_appendWords {δ α : Type} {r k m l n₁ n₂ : ℕ} {frontier : Fin r} {src : Fin k → Fin r} {tmp : Fin (m + (l + max n₁ n₂) + 1) → Fin r} {input : δ ↪ Fin k → ℕ} {answer : α ↪ Fin l → ℕ} {d : δ} {a : α} {x z : Data r} (hin : x.regs ∘ src = input d) (hframe : ∀ (i : Fin r), i ≠ frontier → (∀ (j : Fin (l + n₁ + 1)), (tmp ∘ bindSharedRight) j ≠ i) → z.regs i = x.regs i) (hd : ∀ (i : Fin k) (j : Fin (m + (l + max n₁ n₂) + 1)), src i ≠ tmp j) (hs : ∀ (i : Fin k), src i ≠ frontier) (hout : ∀ (j : Fin l), z.regs ((tmp ∘ bindSharedRight) (Fin.castAdd (n₁ + 1) j)) = answer a j) : (z.regs ∘ Fin.append src fun (i : Fin l) => tmp (bindSharedRight (Fin.castAdd (n₁ + 1) i))) = (appendWords input answer) (d, a)

After the predecessor writes answer a into its live tail slots and preserves registers outside frontier and tmp ∘ bindSharedRight, the continuation's source bank holds appendWords input answer (d, a).

theorem Cslib.WordRAM.Realization.bind_cost_le {C₁ C₂ t₁ t₂ t : ℕ} (ht : t₁ + t₂ + 1 ≤ t) : C₁ * (t₁ + 1) + C₂ * (t₂ + 1) ≤ max C₁ C₂ * (t + 1)

Combine two stage cost bounds C₁ * (t₁ + 1) and C₂ * (t₂ + 1) under max C₁ C₂.

theorem Cslib.WordRAM.Realization.Realizes.Witness.bind_execWithin {B : Basis} {δ α β : Type} {k l m : ℕ} {p : δ → DataStructure.Memory.Prog α} {q : δ × α → DataStructure.Memory.Prog β} {input : δ ↪ Fin k → ℕ} {answer : α ↪ Fin l → ℕ} {output : β ↪ Fin m → ℕ} {safeP : ℕ → δ → DataStructure.Memory.State → Prop} {safeQ : ℕ → δ × α → DataStructure.Memory.State → Prop} {workP : δ → DataStructure.Memory.State → ℕ} {workQ : δ × α → DataStructure.Memory.State → ℕ} (hP : Witness B p input answer safeP workP) (hQ : Witness B q (appendWords input answer) output safeQ workQ) : let n₁ := hP.scratchSize; let n₂ := hQ.scratchSize; have C₁ := hP.factor; have C₂ := hQ.factor; let N := l + max n₁ n₂; have left := bindSharedLeft; have right := bindSharedRight; have emit := fun {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) (tmp : Fin (m + N + 1) → Fin r) => (hP.code frontier src (tmp ∘ right)).seq (hQ.code frontier (Fin.append src fun (i : Fin l) => tmp (right (Fin.castAdd (n₁ + 1) i))) (tmp ∘ left)); ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) (tmp : Fin (m + N + 1) → Fin r), Function.Injective tmp → (∀ (i : Fin k) (j : Fin (m + N + 1)), src i ≠ tmp j) → (∀ (j : Fin (m + N + 1)), tmp j ≠ frontier) → (∀ (i : Fin k), src i ≠ frontier) → ¬(emit frontier src tmp).ReadsWidth ∧ ∀ (w : ℕ) (d : δ) (x : Data r), have s := memoryState frontier x; have a := (DataStructure.Memory.spec 0).clientResult s (p d); have s' := (DataStructure.Memory.spec 0).clientState s (p d); have nextSrc := Fin.append src fun (i : Fin l) => tmp (right (Fin.castAdd (n₁ + 1) i)); Data.Bounded w x → x.regs ∘ src = input d → safeP w d s ∧ safeQ w (d, a) s' → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a))) → ∀ (TP TQ : ℕ), (Function.Injective (tmp ∘ right) → (∀ (i : Fin k) (j : Fin (l + n₁ + 1)), src i ≠ (tmp ∘ right) j) → (∀ (j : Fin (l + n₁ + 1)), (tmp ∘ right) j ≠ frontier) → (∀ (i : Fin k), src i ≠ frontier) → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (p d)) → ∀ (z : Data r), ExecWithin w (hP.code frontier src (tmp ∘ right)) x z (C₁ * (memoryCost (p d) s + workP d s + 1)) → ExecWithin w (hP.code frontier src (tmp ∘ right)) x z TP) → (∀ (z : Data r), Function.Injective (tmp ∘ left) → (∀ (i : Fin (k + l)) (j : Fin (m + n₂ + 1)), nextSrc i ≠ (tmp ∘ left) j) → (∀ (j : Fin (m + n₂ + 1)), (tmp ∘ left) j ≠ frontier) → (∀ (i : Fin (k + l)), nextSrc i ≠ frontier) → Data.Bounded w z → z.regs ∘ nextSrc = (appendWords input answer) (d, a) → memoryState frontier z = s' → safeQ w (d, a) (memoryState frontier z) → (DataStructure.Memory.spec w).ValidHistory (memoryState frontier z) ((DataStructure.Memory.spec w).clientHistory (memoryState frontier z) (q (d, a))) → ∀ (y : Data r), ExecWithin w (hQ.code frontier nextSrc (tmp ∘ left)) z y (C₂ * (memoryCost (q (d, a)) (memoryState frontier z) + workQ (d, a) (memoryState frontier z) + 1)) → ExecWithin w (hQ.code frontier nextSrc (tmp ∘ left)) z y TQ) → ∃ (y : Data r), ExecWithin w (emit frontier src tmp) x y (TP + TQ) ∧ memoryState frontier y = (DataStructure.Memory.spec w).clientState s (PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a)) ∧ (∀ (i : Fin m), y.regs (tmp (Fin.castAdd (N + 1) i)) = output ((DataStructure.Memory.spec w).clientResult s (PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a))) i) ∧ ∀ (i : Fin r), i ≠ frontier → (∀ (j : Fin (m + N + 1)), tmp j ≠ i) → y.regs i = x.regs i

Tighten the native budgets of the supplied component runs without changing code, domain or semantic postconditions. The continuation receives the predecessor's derived encoded answer, exact intermediate memory, boundedness, safety and valid history. Both stages receive their derived layout premises. Only execution bounds are supplied by the callbacks; the complete frame/input/memory proof is shared with Witness.bind. The resulting bound is additive on the same retained sequential emitter.

def Cslib.WordRAM.Realization.Realizes.Witness.bind {B : Basis} {δ α β : Type} {k l m : ℕ} {p : δ → DataStructure.Memory.Prog α} {q : δ × α → DataStructure.Memory.Prog β} {input : δ ↪ Fin k → ℕ} {answer : α ↪ Fin l → ℕ} {output : β ↪ Fin m → ℕ} {safeP : ℕ → δ → DataStructure.Memory.State → Prop} {safeQ : ℕ → δ × α → DataStructure.Memory.State → Prop} {workP : δ → DataStructure.Memory.State → ℕ} {workQ : δ × α → DataStructure.Memory.State → ℕ} (hP : Witness B p input answer safeP workP) (hQ : Witness B q (appendWords input answer) output safeQ workQ) : Witness B (fun (d : δ) => PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a)) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => safeP w d s ∧ safeQ w (d, (DataStructure.Memory.spec 0).clientResult s (p d)) ((DataStructure.Memory.spec 0).clientState s (p d))) fun (d : δ) (s : DataStructure.Memory.State) => workP d s + workQ (d, (DataStructure.Memory.spec 0).clientResult s (p d)) ((DataStructure.Memory.spec 0).clientState s (p d)) + 1

Retain one uniform sequential emitter while reusing the predecessor's dead auxiliary words. Only its runtime answer remains live in a separate tail bank. The continuation's result slots are already the composite result slots, so no copies or extra charge are introduced.

theorem Cslib.WordRAM.Realization.Realizes.bind {B : Basis} {δ α β : Type} {k l m : ℕ} {p : δ → DataStructure.Memory.Prog α} {q : δ × α → DataStructure.Memory.Prog β} {input : δ ↪ Fin k → ℕ} {answer : α ↪ Fin l → ℕ} {output : β ↪ Fin m → ℕ} {safeP : ℕ → δ → DataStructure.Memory.State → Prop} {safeQ : ℕ → δ × α → DataStructure.Memory.State → Prop} {workP : δ → DataStructure.Memory.State → ℕ} {workQ : δ × α → DataStructure.Memory.State → ℕ} (hP : Realizes B p input answer safeP workP) (hQ : Realizes B q (appendWords input answer) output safeQ workQ) : Realizes B (fun (d : δ) => PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a)) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => safeP w d s ∧ safeQ w (d, (DataStructure.Memory.spec 0).clientResult s (p d)) ((DataStructure.Memory.spec 0).clientState s (p d))) fun (d : δ) (s : DataStructure.Memory.State) => workP d s + workQ (d, (DataStructure.Memory.spec 0).clientResult s (p d)) ((DataStructure.Memory.spec 0).clientState s (p d)) + 1

One uniform continuation emitter consumes the original environment and the first runtime answer. Its domain and work charge are evaluated at the deterministic intermediate state. All emitted code, register banks and the exchange constant precede runtime answers.

theorem Cslib.WordRAM.Realization.RealizesBounded.bind {B : Basis} {δ α β : Type} {k l m : ℕ} {p : δ → DataStructure.Memory.Prog α} {q : δ × α → DataStructure.Memory.Prog β} {input : δ ↪ Fin k → ℕ} {answer : α ↪ Fin l → ℕ} {output : β ↪ Fin m → ℕ} {safeP : ℕ → δ → DataStructure.Memory.State → Prop} {safeQ : ℕ → δ × α → DataStructure.Memory.State → Prop} {workP : δ → DataStructure.Memory.State → ℕ} {workQ : δ × α → DataStructure.Memory.State → ℕ} (hP : RealizesBounded B p input answer safeP workP) (hQ : RealizesBounded B q (appendWords input answer) output safeQ workQ) : RealizesBounded B (fun (d : δ) => PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a)) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => safeP w d s ∧ safeQ w (d, (DataStructure.Memory.spec 0).clientResult s (p d)) ((DataStructure.Memory.spec 0).clientState s (p d))) fun (d : δ) (s : DataStructure.Memory.State) => workP d s + workQ (d, (DataStructure.Memory.spec 0).clientResult s (p d)) ((DataStructure.Memory.spec 0).clientState s (p d)) + 1

Frontier-bounded sequential composition of two Memory.Prog realizations.

theorem Cslib.WordRAM.Realization.RealizesBounded.bind₀ {B : Basis} {δ α β : Type} {k l m : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {q : δ × α → DataStructure.Memory.Prog β} {answer : α ↪ Fin l → ℕ} {output' : β ↪ Fin m → ℕ} {safeP : ℕ → δ → DataStructure.Memory.State → Prop} {safeQ : ℕ → δ × α → DataStructure.Memory.State → Prop} (hP : RealizesBounded B p input answer safeP fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) (hQ : RealizesBounded B q ((input.prodMap answer).trans (Fin.appendEquiv k l).toEmbedding) output' safeQ fun (x : δ × α) (x_1 : DataStructure.Memory.State) => 0) : RealizesBounded B (fun (d : δ) => PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a)) input output' (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => safeP w d s ∧ safeQ w (d, (DataStructure.Memory.spec 0).clientResult s (p d)) ((DataStructure.Memory.spec 0).clientState s (p d))) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Sequencing with the bind's control unit absorbed (work = 0).

theorem Cslib.WordRAM.Realization.RealizesBounded.bind₀_of_run {B : Basis} {δ α β : Type} {k l m : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {q : δ × α → DataStructure.Memory.Prog β} {answer : α ↪ Fin l → ℕ} {output' : β ↪ Fin m → ℕ} {safeP : ℕ → δ → DataStructure.Memory.State → Prop} {safeQ : ℕ → δ × α → DataStructure.Memory.State → Prop} (hP : RealizesBounded B p input answer safeP fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) (hQ : RealizesBounded B q ((input.prodMap answer).trans (Fin.appendEquiv k l).toEmbedding) output' safeQ fun (x : δ × α) (x_1 : DataStructure.Memory.State) => 0) (reply : δ → DataStructure.Memory.State → α) (next : δ → DataStructure.Memory.State → DataStructure.Memory.State) (hreply : ∀ (d : δ) (s : (DataStructure.Memory.spec 0).State), (DataStructure.Memory.spec 0).clientResult s (p d) = reply d s) (hnext : ∀ (d : δ) (s : (DataStructure.Memory.spec 0).State), (DataStructure.Memory.spec 0).clientState s (p d) = next d s) : RealizesBounded B (fun (d : δ) => PFunctor.FreeM.bind (p d) fun (a : α) => q (d, a)) input output' (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => safeP w d s ∧ safeQ w (d, reply d s) (next d s)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Sequencing with closed-form reply and next memory (work = 0).