Realization rules with absorbed local work

Realizes bounds native instructions by C * (memory charge + local work + 1) with one existential exchange factor C. Local work within a constant multiple of the memory charge plus another grading can therefore be traded for a larger factor (Realizes.mono_mul). In particular, a composition of glue, binds and branches has the same certificate with local work 0: its native cost is O(memory charge + 1). So does a runtime-bounded loop whose body begins with a query, because that query's charge pays each iteration's control unit; a query-free loop keeps its graded charge.

The rules below are the C2 rules bind, branch, glueVector and iterateRuntime with that absorption applied. They are the target shapes of the realize tactic. Glue takes GlueComputable certificates, whose instruction budgets stay hidden.

Main definitions

• WordEncoding: the word encoding realize uses for an intermediate answer type.
• blockWords: a block as its base address and length.

Main results

• Realizes.mono_mul: absorb local work dominated by a constant multiple of the memory charge plus another grading.
• Realizes.congr: transport a certificate along pointwise equal programs.
• Realizes.consequence_valid: strengthen the domain under the client's valid history.
• Realizes.bind₀, Realizes.branch₀: sequencing and branching with absorbed control work. Realizes.bind₀_of_run states the continuation's domain at a closed form of the first client's reply and next memory.
• Realizes.pure₀: finite-result glue from GlueComputable coordinates, with a visible domain and an explicit word-fit obligation.
• Realizes.iterate₀: loops whose body begins with a query.

These are derived rules over the existing realization kernel; no execution semantics or certificate is added. Environment, domain and work transport laws are publicly imported from the LoopCongr module.

class Cslib.WordRAM.Realization.WordEncoding (α : Type) : Type

The faithful word encoding realize uses when a bind passes an answer of type α to its continuation. Instances cover words, unit, optional words, Booleans, blocks and pairs.

• width : ℕ

  The number of words.

• encode : α ↪ Fin (width α) → ℕ

  The faithful encoding.

@[instance_reducible]

instance Cslib.WordRAM.Realization.instWordEncodingNat : WordEncoding ℕ

@[instance_reducible]

instance Cslib.WordRAM.Realization.instWordEncodingUnit : WordEncoding Unit

@[instance_reducible]

instance Cslib.WordRAM.Realization.instWordEncodingOptionNat : WordEncoding (Option ℕ)

@[instance_reducible, instance 100]

instance Cslib.WordRAM.Realization.instWordEncodingOption {α : Type} [WordEncoding α] : WordEncoding (Option α)

Optional values use a presence tag followed by their unshifted payload words. The scalar instance retains its legacy vector normal form.

@[instance_reducible]

instance Cslib.WordRAM.Realization.instWordEncodingBool : WordEncoding Bool

def Cslib.WordRAM.Realization.blockWords : Block ↪ Fin 2 → ℕ

A block is encoded by its base address and its length.

@[instance_reducible]

instance Cslib.WordRAM.Realization.instWordEncodingBlock : WordEncoding Block

@[instance_reducible]

instance Cslib.WordRAM.Realization.instWordEncodingProd {α β : Type} [WordEncoding α] [WordEncoding β] : WordEncoding (α × β)

A pair is encoded by its two encodings, first component first.

theorem Cslib.WordRAM.Realization.Realizes.mono_mul {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work work' : δ → DataStructure.Memory.State → ℕ} (h : Realizes B p input output safe work) (K : ℕ) (hwork : ∀ (d : δ) (s : DataStructure.Memory.State), work d s ≤ K * (memoryCost (p d) s + work' d s + 1)) : Realizes B p input output safe work'

Local work within a constant multiple of the memory charge plus another grading is absorbed by the exchange factor. The new factor is C * (K + 1); the emitter and scratch are unchanged.

theorem Cslib.WordRAM.Realization.Realizes.congr {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {p' : δ → DataStructure.Memory.Prog α} (h : Realizes B p input output safe work) (hp : ∀ (d : δ), p d = p' d) : Realizes B p' input output safe work

Pointwise equal programs have the same certificates.

theorem Cslib.WordRAM.Realization.Realizes.consequence_valid {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe : ℕ → δ → DataStructure.Memory.State → Prop} {work : δ → DataStructure.Memory.State → ℕ} {safe' : ℕ → δ → DataStructure.Memory.State → Prop} (h : Realizes B p input output safe work) (hsafe : ∀ (w : ℕ) (d : δ) (s : DataStructure.Memory.State), (∀ (i : Fin k), Fits w (input d i)) → DataStructure.Memory.WellFormed w s → (DataStructure.Memory.spec w).ValidHistory s ((DataStructure.Memory.spec w).clientHistory s (p d)) → safe' w d s → safe w d s) : Realizes B p input output safe' work

Strengthen the visible domain using, besides the input fits and memory well-formedness, the validity of the client's own history from the entry memory, which every execution supplies.

theorem Cslib.WordRAM.Realization.Realizes.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 : Realizes B p input answer safeP fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) (hQ : Realizes B q ((input.prodMap answer).trans (Fin.appendEquiv k l).toEmbedding) output' safeQ fun (x : δ × α) (x_1 : DataStructure.Memory.State) => 0) : 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 (x : δ) (x_1 : DataStructure.Memory.State) => 0

Sequencing with the bind's control unit absorbed.

theorem Cslib.WordRAM.Realization.Realizes.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 : Realizes B p input answer safeP fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) (hQ : Realizes 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) : 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, reply d s) (next d s)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Sequencing with the first client's reply and next memory given in closed form, so that the continuation's domain is stated at them rather than at the interpreter's run.

theorem Cslib.WordRAM.Realization.Realizes.branch₀ {B : Basis} {δ α : Type} {k l : ℕ} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {pos neg : δ → DataStructure.Memory.Prog α} {safePos safeNeg : ℕ → δ → DataStructure.Memory.State → Prop} (c : Cond k) (hp : Realizes B pos input output safePos fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) (hn : Realizes B neg input output safeNeg fun (x : δ) (x_1 : DataStructure.Memory.State) => 0) : Realizes B (fun (d : δ) => if test c (input d) then pos d else neg d) input output (fun (w : ℕ) (d : δ) (s : DataStructure.Memory.State) => if test c (input d) then safePos w d s else safeNeg w d s) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Branching with the test and jump absorbed. Only the selected alternative's domain is required.

theorem Cslib.WordRAM.Realization.Realizes.pure₀ {B : Basis} {δ α : Type} {k l : ℕ} (input : δ ↪ Fin k → ℕ) (output : α ↪ Fin l → ℕ) (f : δ → α) (g : Fin l → (Fin k → ℕ) → ℕ) {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} (need : ℕ → (Fin k → ℕ) → Prop) (hresult : ∀ (d : δ) (i : Fin l), output (f d) i = g i (input d)) (hcoord : ∀ (i : Fin l), GlueComputable B (g i) P bound) (hneed : ∀ (w : ℕ) (v : Fin k → ℕ), (∀ (i : Fin k), Fits w (v i)) → P v → need w v → Fits w (bound v)) : Realizes B (fun (d : δ) => pure (f d)) input output (fun (w : ℕ) (d : δ) (x : DataStructure.Memory.State) => P (input d) ∧ need w (input d)) fun (x : δ) (x_1 : DataStructure.Memory.State) => 0

Return a computed finite result. Each coordinate has a GlueComputable certificate over the live words with a common domain P and value envelope bound; need is any condition that, together with the live words' fit and P, makes the envelope fit. Native glue cost is absorbed.

Loops whose body issues a query

theorem Cslib.WordRAM.Realization.one_le_memoryCost_liftBind {α : Type} (o : DataStructure.Memory.Op) (k : o.Result → DataStructure.Memory.Prog α) (s : DataStructure.Memory.State) : 1 ≤ memoryCost (PFunctor.FreeM.liftBind o k) s

A client that begins with a query has memory charge at least one.

theorem Cslib.WordRAM.Realization.iterationWork_zero_le {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (hquery : ∀ (x : δ × σ) (s : DataStructure.Memory.State), 1 ≤ memoryCost (body x) s) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : iterationWork body (fun (x : δ × σ) (x_1 : DataStructure.Memory.State) => 0) d n a s ≤ memoryCost (iterate body d n a) s

When every body issues a query, the loop's control work is at most its memory charge.

@[simp]

theorem Cslib.WordRAM.Realization.iterationSafe_true {δ σ : Type} (body : δ × σ → DataStructure.Memory.Prog σ) (w : ℕ) (d : δ) (n : ℕ) (a : σ) (s : DataStructure.Memory.State) : iterationSafe body (fun (x : ℕ) (x_1 : δ × σ) (x_2 : DataStructure.Memory.State) => True) w d n a s

With trivial body domains, every iteration's domain holds.

theorem Cslib.WordRAM.Realization.Realizes.iterate₀ {δ : Type} {k l : ℕ} {σ : Type} (input : δ ↪ Fin k → ℕ) (output : σ ↪ Fin l → ℕ) {body : δ × σ → DataStructure.Memory.Prog σ} {safe : ℕ → δ × σ → DataStructure.Memory.State → Prop} (h : Realizes Basis.exact body ((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding) output safe fun (x : δ × σ) (x_1 : DataStructure.Memory.State) => 0) (hquery : ∀ (x : δ × σ) (s : DataStructure.Memory.State), 1 ≤ memoryCost (body x) s) : Realizes Basis.exact (fun (d : (δ × σ) × ℕ) => iterate body d.1.1 d.2 d.1.2) ((((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv (k + l) 1).toEmbedding) output (fun (w : ℕ) (d : (δ × σ) × ℕ) (s : DataStructure.Memory.State) => iterationSafe body safe w d.1.1 d.2 d.1.2 s) fun (x : (δ × σ) × ℕ) (x_1 : DataStructure.Memory.State) => 0

A runtime-bounded loop whose body begins with a query has local work 0: each iteration's control unit is paid by that query's memory charge.