Work bounds under the entry contract

A requested entry domain, fitting input words, well-formed memory and the client's valid history may justify both its safety conditions and its local-work bound. These consequence rules keep the original emitter, scratch bank and exchange factor. They change neither the program nor its whole-memory and register-frame guarantees, and introduce no new execution model.

Main results

• Realizes.consequence_work: compare work under the requested entry contract.
• RealizesBounded.consequence_work: the same rule retaining frontier-bounded accesses.

The rules are original infrastructure over the existing realization contracts.

theorem Cslib.WordRAM.Realization.Realizes.consequence_work {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe safe' : ℕ → δ → DataStructure.Memory.State → Prop} {work work' : δ → DataStructure.Memory.State → ℕ} (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) (hwork : ∀ (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 → work d s ≤ work' d s) : Realizes B p input output safe' work'

Strengthen safety and compare local work under the requested entry domain and the client's valid history. The emitter, scratch size, exchange factor and width freedom are unchanged.

theorem Cslib.WordRAM.Realization.RealizesBounded.consequence_work {B : Basis} {δ α : Type} {k l : ℕ} {p : δ → DataStructure.Memory.Prog α} {input : δ ↪ Fin k → ℕ} {output : α ↪ Fin l → ℕ} {safe safe' : ℕ → δ → DataStructure.Memory.State → Prop} {work work' : δ → DataStructure.Memory.State → ℕ} (h : RealizesBounded 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) (hwork : ∀ (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 → work d s ≤ work' d s) : RealizesBounded B p input output safe' work'

Strengthen safety and compare local work under the requested entry domain and valid history, retaining frontier-bounded accesses and all of the original witness resources.