SchedulingContracts.lean

1 module
2 public import Mathlib.Algebra.Order.Floor.Semiring
3 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
4 public import Mathlib.Algebra.Order.AbsoluteValue.Basic
5 public import Mathlib.Data.Rat.Floor
6 public import Mathlib.Data.Finset.Card
7 public import Mathlib.Tactic
8 
9 /-!
10 Author: Komorebi P.
11 Paper VIII 10.2, 10.4--10.6, 11.3, with a mathematical implementation of 2.9.
12 Times are declared real-valued models, never claimed hardware measurements.
13 -/
14 public section
15 set_option autoImplicit false
16 namespace KomorebiPaperVIII
17 open scoped BigOperators
18 
19 /-- Complete signature fields required for fair timing comparisons. -/
20 structure BenchmarkSignature (Case Output Reference Scope : Type*) where
21   caseKey : Case
22   outputContract : Output
23   reference : Reference
24   timingScope : Scope
25   deriving DecidableEq
26 
27 /-- Extra metadata such as measured time is deliberately absent from this relation. -/
28 def FairMatch {C O R S : Type*} (a b : BenchmarkSignature C O R S) : Prop :=
29   a.caseKey = b.caseKey ∧ a.outputContract = b.outputContract ∧
30     a.reference = b.reference ∧ a.timingScope = b.timingScope
31 
32 theorem fair_match_iff_eq {C O R S : Type*} (a b : BenchmarkSignature C O R S) :
33     FairMatch a b ↔ a = b := by
34   constructor
35   · rintro ⟨hc, ho, hr, hs⟩
36     cases a; cases b
37     simp_all
38   · intro h; subst b; exact ⟨rfl, rfl, rfl, rfl⟩
39 
40 theorem fair_matching_equivalence {C O R S : Type*} :
41     Equivalence (FairMatch (C := C) (O := O) (R := R) (S := S)) := by
42   constructor
43   · intro a; exact (fair_match_iff_eq a a).2 rfl
44   · intro a b h; exact (fair_match_iff_eq b a).2 ((fair_match_iff_eq a b).1 h).symm
45   · intro a b c hab hbc
46     exact (fair_match_iff_eq a c).2
47       (((fair_match_iff_eq a b).1 hab).trans ((fair_match_iff_eq b c).1 hbc))
48 
49 /-- A decoded run actually returns the explicit object and includes conversion time. -/
50 def decodedRun {X C Y : Type*} (compressed : X → C) (decode : C → Y)
51     (runTime : X → ℝ) (decodeTime : C → ℝ) (x : X) : Y × ℝ :=
52   (decode (compressed x), runTime x + decodeTime (compressed x))
53 
54 theorem contract_conversion {X C Y : Type*} (compressed : X → C) (explicit : X → Y)
55     (decode : C → Y) (runTime : X → ℝ) (decodeTime : C → ℝ)
56     (hdecode : ∀ x, decode (compressed x) = explicit x) (x : X) :
57     (decodedRun compressed decode runTime decodeTime x).1 = explicit x ∧
58     (decodedRun compressed decode runTime decodeTime x).2 =
59       runTime x + decodeTime (compressed x) := by
60   exact ⟨hdecode x, rfl⟩
61 
62 theorem direct_compressed_consumption {X C Y Z : Type*}
63     (compressed : X → C) (explicit : X → Y) (decode : C → Y)
64     (consume : Y → Z) (hdecode : ∀ x, decode (compressed x) = explicit x) :
65     (fun x => consume (decode (compressed x))) = fun x => consume (explicit x) := by
66   funext x
67   rw [hdecode x]
68 
69 theorem omitted_decode_understates_time {X C Y : Type*} (compressed : X → C)
70     (decode : C → Y) (runTime : X → ℝ) (decodeTime : C → ℝ)
71     (x : X) (h : 0 < decodeTime (compressed x)) :
72     runTime x < (decodedRun compressed decode runTime decodeTime x).2 := by
73   dsimp [decodedRun]
74   linarith
75 
76 /-- Active shape classes are exactly the image of the complete kernel signature. -/
77 def activeShapeClasses {E Shape : Type*} [Fintype E] [DecidableEq Shape]
78     (key : E → Shape) : Finset Shape := Finset.univ.image key
79 
80 theorem shape_launch_count {E Shape : Type*} [Fintype E] [DecidableEq Shape]
81     (key : E → Shape) : (activeShapeClasses key).card ≤ Fintype.card E := by
82   exact Finset.card_image_le
83 
84 theorem each_block_has_shape {E Shape : Type*} [Fintype E] [DecidableEq Shape]
85     (key : E → Shape) (e : E) : key e ∈ activeShapeClasses key := by
86   exact Finset.mem_image_of_mem key (Finset.mem_univ e)
87 
88 /-- Grouping does not duplicate or lose any block contribution. -/
89 theorem grouped_execution_output {E Shape V : Type*} [Fintype E] [DecidableEq Shape]
90     [AddCommMonoid V] (key : E → Shape) (value : E → V) :
91     (∑ k ∈ activeShapeClasses key, ∑ e ∈ Finset.univ.filter (fun e => key e = k), value e) =
92       ∑ e, value e := by
93   exact Finset.sum_fiberwise_of_maps_to (fun e _ => each_block_has_shape key e) value
94 
95 theorem grouped_execution_work {E Shape : Type*} [Fintype E] [DecidableEq Shape]
96     (key : E → Shape) (work : E → ℕ) :
97     (∑ k ∈ activeShapeClasses key, ∑ e ∈ Finset.univ.filter (fun e => key e = k), work e) =
98       ∑ e, work e := by
99   exact grouped_execution_output key work
100 
101 theorem amortization_threshold (setup baseline candidate reuse : ℝ)
102     (h : candidate < baseline) :
103     setup + reuse * candidate < reuse * baseline ↔ setup / (baseline - candidate) < reuse := by
104   rw [div_lt_iff₀ (sub_pos.mpr h)]
105   constructor <;> intro hh <;> nlinarith
106 
107 theorem no_amortization (setup baseline candidate reuse : ℝ)
108     (hs : 0 ≤ setup) (hr : 0 ≤ reuse) (h : baseline ≤ candidate) :
109     ¬ setup + reuse * candidate < reuse * baseline := by
110   have hm := mul_le_mul_of_nonneg_left h hr
111   linarith
112 
113 /-- Strict profitability, not mere break-even, gives floor plus one. -/
114 noncomputable def minimumReuse (setup baseline candidate : ℝ) : ℕ :=
115   ⌊setup / (baseline - candidate)⌋₊ + 1
116 
117 theorem integer_amortization_threshold (setup baseline candidate : ℝ)
118     (hs : 0 ≤ setup) (h : candidate < baseline) (reuse : ℕ) :
119     setup + (reuse : ℝ) * candidate < (reuse : ℝ) * baseline ↔
120       minimumReuse setup baseline candidate ≤ reuse := by
121   rw [amortization_threshold setup baseline candidate reuse h, minimumReuse]
122   rw [← Nat.floor_lt (div_nonneg hs (le_of_lt (sub_pos.mpr h)))]
123   omega
124 
125 theorem minimum_reuse_attains (setup baseline candidate : ℝ)
126     (hs : 0 ≤ setup) (h : candidate < baseline) :
127     setup + (minimumReuse setup baseline candidate : ℝ) * candidate <
128       (minimumReuse setup baseline candidate : ℝ) * baseline ∧
129     ∀ reuse : ℕ, reuse < minimumReuse setup baseline candidate →
130       ¬ setup + (reuse : ℝ) * candidate < (reuse : ℝ) * baseline := by
131   constructor
132   · exact (integer_amortization_threshold setup baseline candidate hs h _).2 le_rfl
133   · intro reuse hr
134     rw [integer_amortization_threshold setup baseline candidate hs h reuse]
135     omega
136 
137 theorem graph_replay_threshold (capture ordinary replay reuse : ℝ) (h : replay < ordinary) :
138     capture + reuse * replay < reuse * ordinary ↔ capture / (ordinary - replay) < reuse := by
139   exact amortization_threshold capture ordinary replay reuse h
140 
141 /-- Necessity includes an actual per-use advantage; zero uses cannot be profitable. -/
142 theorem materialization_threshold (materialize compressed explicit reuse : ℝ)
143     (hm : 0 ≤ materialize) (hr : 0 ≤ reuse) :
144     materialize + reuse * explicit < reuse * compressed ↔
145       explicit < compressed ∧ materialize / (compressed - explicit) < reuse := by
146   constructor
147   · intro h
148     have he : explicit < compressed := by
149       by_contra hn
150       exact no_amortization materialize compressed explicit reuse hm hr (le_of_not_gt hn) h
151     exact ⟨he, (amortization_threshold materialize compressed explicit reuse he).1 h⟩
152   · rintro ⟨he, hs⟩
153     exact (amortization_threshold materialize compressed explicit reuse he).2 hs
154 
155 theorem zero_setup_first_use (baseline candidate : ℝ) (_h : candidate < baseline) :
156     minimumReuse 0 baseline candidate = 1 := by
157   simp [minimumReuse]
158 
159 theorem exact_break_even_regression :
160     minimumReuse 6 5 3 = 4 ∧
161       ¬ (6 : ℝ) + 3 * 3 < 3 * 5 ∧ (6 : ℝ) + 4 * 3 < 4 * 5 := by
162   norm_num [minimumReuse]
163 
164 end KomorebiPaperVIII
165 
166 -- FINAL AXIOM AUDITS
167 #print axioms KomorebiPaperVIII.fair_match_iff_eq
168 #print axioms KomorebiPaperVIII.fair_matching_equivalence
169 #print axioms KomorebiPaperVIII.contract_conversion
170 #print axioms KomorebiPaperVIII.direct_compressed_consumption
171 #print axioms KomorebiPaperVIII.omitted_decode_understates_time
172 #print axioms KomorebiPaperVIII.shape_launch_count
173 #print axioms KomorebiPaperVIII.each_block_has_shape
174 #print axioms KomorebiPaperVIII.grouped_execution_output
175 #print axioms KomorebiPaperVIII.grouped_execution_work
176 #print axioms KomorebiPaperVIII.amortization_threshold
177 #print axioms KomorebiPaperVIII.no_amortization
178 #print axioms KomorebiPaperVIII.integer_amortization_threshold
179 #print axioms KomorebiPaperVIII.minimum_reuse_attains
180 #print axioms KomorebiPaperVIII.graph_replay_threshold
181 #print axioms KomorebiPaperVIII.materialization_threshold
182 #print axioms KomorebiPaperVIII.zero_setup_first_use
183 #print axioms KomorebiPaperVIII.exact_break_even_regression

Back to source controls