SafeEndingPolicies.lean

1 import MachineTheory.SafeEnding
2 
3 /-! Core 8.3 with genuine history-dependent policies and all-path semantics.
4 A configuration retains past state/action pairs and its current observed state.
5 An ending guarantee includes both local safety/legality at every finite prefix
6 and the absence of an infinite non-ending execution. Thus deadlock cannot win
7 by making the set of infinite paths empty. The stop input is observed before
8 selection of the next action and retains the full pre-command history.
9 -/
10 namespace Komorebi.MachineTheory.SafeEnding
11 
12 universe u v w
13 variable {Z : Type u} {A : Type v}
14 
15 abbrev Config (Z : Type u) (A : Type v) := List (Z × A) × Z
16 abbrev Strategy (Z : Type u) (A : Type v) := Config Z A → Option A
17 
18 def start (x : Z) : Config Z A := ([], x)
19 
20 /-- Finite reachability contains all legal adversarial successors. -/
21 inductive Reach {C : Type w} (r : C → C → Prop) (c : C) : C → Prop
22   | refl : Reach r c c
23   | tail {d e : C} : Reach r c d → r d e → Reach r c e
24 
25 /-- The policy selects one action from the full history before the successor. -/
26 def edge (M : Model Z A) (catalogue : Z → Finset A) (σ : Strategy Z A)
27     (c d : Config Z A) : Prop :=
28   ∃ a, σ c = some a ∧ a ∈ catalogue c.2 ∧
29     d.1 = (c.2, a) :: c.1 ∧ d.2 ∈ M.post c.2 a
30 
31 def endEdge (M : Model Z A) (σ : Strategy Z A) (c d : Config Z A) : Prop :=
32   c.2 ∉ M.goal ∧ edge M M.finish σ c d
33 
34 def runEdge (M : Model Z A) (σ : Strategy Z A) := edge M M.run σ
35 
36 /-- Universal total correctness until the first goal arrival. -/
37 structure EndingGuarantee (M : Model Z A) (σ : Strategy Z A) (x : Z) : Prop where
38   total : ∀ c, Reach (endEdge M σ) (start x) c →
39     c.2 ∈ M.safe ∧ (c.2 ∉ M.goal → ∃ a, σ c = some a ∧ a ∈ M.finish c.2)
40   noInfinite : ∀ p : ℕ → Config Z A, p 0 = start x →
41     (∀ n, endEdge M σ (p n) (p (n + 1))) → False
42 
43 /-- The running guarantee is local at every legal prefix, so it forbids deadlock. -/
44 def RunningGuarantee (M : Model Z A) (σ : Strategy Z A) (x : Z) : Prop :=
45   ∀ c, Reach (runEdge M σ) (start x) c →
46     c.2 ∈ M.safe ∧ ∃ a, σ c = some a ∧ a ∈ M.run c.2
47 
48 /-- One observable policy input. In ending mode it retains the command epoch's
49 configuration as well as the entire subsequent state/action history. -/
50 inductive PolicyInput (Z : Type u) (A : Type v)
51   | running (current : Config Z A)
52   | ending (atCommand : Config Z A) (current : Config Z A)
53 
54 abbrev Policy (Z : Type u) (A : Type v) := PolicyInput Z A → Option A
55 
56 def before (P : Policy Z A) : Strategy Z A := fun c => P (.running c)
57 def after (P : Policy Z A) (anchor : Config Z A) : Strategy Z A :=
58   fun c => P (.ending anchor c)
59 
60 /-- Any command epoch may switch the same policy to a surely terminating ending.
61 No assumption of memorylessness is imposed on the supplied policy. -/
62 structure SwitchingGuarantee (M : Model Z A) (P : Policy Z A) (x : Z) : Prop where
63   run_total : RunningGuarantee M (before P) x
64   end_on_command : ∀ c, Reach (runEdge M (before P)) (start x) c →
65     EndingGuarantee M (after P c) c.2
66 
67 noncomputable section
68 
69 /-- The rank-decreasing strategy ignores history, but its specification quantifies
70 all histories and every successor of the selected action. -/
71 def rankedStrategy [Fintype Z] (M : Model Z A) : Strategy Z A :=
72   fun c => endingAction M c.2
73 
74 theorem ranked_edge [Fintype Z] (M : Model Z A) {c d : Config Z A}
75     (hc : c.2 ∈ endingRegion M) (he : endEdge M (rankedStrategy M) c d) :
76     d.2 ∈ endingRegion M ∧ endRank M d.2 < endRank M c.2 := by
77   obtain ⟨hg, a, hσ, _, _, hp⟩ := he
78   obtain ⟨b, hb, _, hdesc⟩ := endingAction_spec M hc hg
79   have hab : a = b := Option.some.inj (hσ.symm.trans hb)
80   subst b
81   exact hdesc d.2 hp
82 
83 theorem ranked_reachable [Fintype Z] (M : Model Z A) {x : Z}
84     (hx : x ∈ endingRegion M) {c : Config Z A}
85     (hr : Reach (endEdge M (rankedStrategy M)) (start x) c) :
86     c.2 ∈ endingRegion M := by
87   induction hr with
88   | refl => exact hx
89   | tail _ he ih => exact (ranked_edge M ih he).1
90 
91 /-- Every finite execution prefix consumes at least one unit of first-entry rank
92 per transition. This is a universal path theorem, not bounded enumeration. -/
93 theorem ending_rank_budget [Fintype Z] (M : Model Z A) {x : Z}
94     (hx : x ∈ endingRegion M) (p : ℕ → Config Z A) (h0 : p 0 = start x)
95     (n : ℕ) (hp : ∀ k, k < n → endEdge M (rankedStrategy M) (p k) (p (k + 1))) :
96     (p n).2 ∈ endingRegion M ∧ n + endRank M (p n).2 ≤ endRank M x := by
97   induction n with
98   | zero => simpa [h0, start] using hx
99   | succ n ih =>
100     have old := ih (fun k hk => hp k (by omega))
101     have step := ranked_edge M old.1 (hp n (by omega))
102     exact ⟨step.1, by omega⟩
103 
104 /-- If a legal prefix reaches the full first-entry budget, its last state is a goal.
105 Earlier arrivals end the prefix semantics already. -/
106 theorem ending_rank_arrival [Fintype Z] (M : Model Z A) {x : Z}
107     (hx : x ∈ endingRegion M) (p : ℕ → Config Z A) (h0 : p 0 = start x)
108     (hp : ∀ k, k < endRank M x → endEdge M (rankedStrategy M) (p k) (p (k + 1))) :
109     (p (endRank M x)).2 ∈ M.goal := by
110   have h := ending_rank_budget M hx p h0 (endRank M x) hp
111   apply (endRank_zero_iff M h.1).mp
112   omega
113 
114 theorem ranked_guarantee [Fintype Z] (M : Model Z A) {x : Z}
115     (hx : x ∈ endingRegion M) : EndingGuarantee M (rankedStrategy M) x := by
116   refine ⟨?_, ?_⟩
117   · intro c hr
118     have hc := ranked_reachable M hx hr
119     refine ⟨endingRegion_safe M hc, ?_⟩
120     intro hg
121     obtain ⟨a, hσ, ha, _⟩ := endingAction_spec M hc hg
122     exact ⟨a, hσ, ha⟩
123   · intro p h0 hp
124     have h := ending_rank_budget M hx p h0 (endRank M x + 1) (fun k _ => hp k)
125     omega
126 
127 /-- Safety and legality plus nonempty enabled successors rule out a fake ending
128 obtained simply by deadlocking before the goal. -/
129 theorem ending_prefix_extends (M : Model Z A) {σ : Strategy Z A} {x : Z}
130     (h : EndingGuarantee M σ x) {c : Config Z A}
131     (hr : Reach (endEdge M σ) (start x) c) (hg : c.2 ∉ M.goal) :
132     ∃ d, endEdge M σ c d := by
133   obtain ⟨a, hσ, ha⟩ := (h.total c hr).2 hg
134   obtain ⟨y, hy⟩ := M.post_nonempty c.2 a (Or.inr ha)
135   exact ⟨((c.2, a) :: c.1, y), hg, a, hσ, ha, rfl, hy⟩
136 
137 /-- Necessity for arbitrary history-dependent policies: outside the attractor an
138 adversary constructs an infinite legal non-ending play, unless safety or legality
139 has already failed. The action is chosen before this adversarial response. -/
140 theorem guarantee_mem_ending [Fintype Z] (M : Model Z A) {σ : Strategy Z A} {x : Z}
141     (h : EndingGuarantee M σ x) : x ∈ endingRegion M := by
142   classical
143   by_contra hx
144   let Bad := {c : Config Z A // Reach (endEdge M σ) (start x) c ∧ c.2 ∉ endingRegion M}
145   let initial : Bad := ⟨start x, Reach.refl, hx⟩
146   have extend : ∀ b : Bad, ∃ d : Bad, endEdge M σ b.val d.val := by
147     intro b
148     have ht := h.total b.val b.property.1
149     have hg : b.val.2 ∉ M.goal := fun hg => b.property.2 (goal_subset_region M hg)
150     obtain ⟨a, hσ, ha⟩ := ht.2 hg
151     obtain ⟨y, hy, hn⟩ := outside_successor M ht.1 b.property.2 ha
152     let c : Config Z A := ((b.val.2, a) :: b.val.1, y)
153     have he : endEdge M σ b.val c := ⟨hg, a, hσ, ha, rfl, hy⟩
154     exact ⟨⟨c, Reach.tail b.property.1 he, hn⟩, he⟩
155   let step : Bad → Bad := fun b => Classical.choose (extend b)
156   let path : ℕ → Bad := fun n => Nat.rec initial (fun _ b => step b) n
157   apply h.noInfinite (fun n => (path n).val) rfl
158   intro n
159   exact Classical.choose_spec (extend (path n))
160 
161 theorem ending_region_iff [Fintype Z] (M : Model Z A) (x : Z) :
162     x ∈ endingRegion M ↔ ∃ σ : Strategy Z A, EndingGuarantee M σ x :=
163   ⟨fun hx => ⟨rankedStrategy M, ranked_guarantee M hx⟩,
164    fun ⟨_, h⟩ => guarantee_mem_ending M h⟩
165 
166 /-- A canonical positional policy. One observed command bit changes the branch. -/
167 def canonicalPolicy [Fintype Z] (M : Model Z A) : Policy Z A
168   | .running c => runningAction M c.2
169   | .ending _ c => endingAction M c.2
170 
171 theorem canonical_run_edge [Fintype Z] (M : Model Z A) {c d : Config Z A}
172     (hc : c.2 ∈ runningRegion M) (he : runEdge M (before (canonicalPolicy M)) c d) :
173     d.2 ∈ runningRegion M := by
174   obtain ⟨a, hσ, _, _, hp⟩ := he
175   obtain ⟨b, hb, _, hpost⟩ := runningAction_spec M hc
176   have hab : a = b := Option.some.inj (hσ.symm.trans hb)
177   subst b
178   exact hpost hp
179 
180 theorem canonical_run_reachable [Fintype Z] (M : Model Z A) {x : Z}
181     (hx : x ∈ runningRegion M) {c : Config Z A}
182     (hr : Reach (runEdge M (before (canonicalPolicy M))) (start x) c) :
183     c.2 ∈ runningRegion M := by
184   induction hr with
185   | refl => exact hx
186   | tail _ he ih => exact canonical_run_edge M ih he
187 
188 theorem canonical_guarantee [Fintype Z] (M : Model Z A) {x : Z}
189     (hx : x ∈ runningRegion M) : SwitchingGuarantee M (canonicalPolicy M) x := by
190   refine ⟨?_, ?_⟩
191   · intro c hr
192     have hc := canonical_run_reachable M hx hr
193     obtain ⟨a, hσ, ha, _⟩ := runningAction_spec M hc
194     exact ⟨runningRegion_safe M hc, a, hσ, ha⟩
195   · intro c hr
196     exact ranked_guarantee M (runningRegion_subset_ending M (canonical_run_reachable M hx hr))
197 
198 /-- The no-command condition admits actual infinite execution; it is not a
199 universal assertion about an empty set of legal streams. -/
200 theorem running_has_infinite_path (M : Model Z A) {σ : Strategy Z A} {x : Z}
201     (h : RunningGuarantee M σ x) :
202     ∃ p : ℕ → Config Z A, p 0 = start x ∧
203       (∀ n, runEdge M σ (p n) (p (n + 1))) ∧ (∀ n, (p n).2 ∈ M.safe) := by
204   classical
205   let Live := {c : Config Z A // Reach (runEdge M σ) (start x) c}
206   let initial : Live := ⟨start x, Reach.refl⟩
207   have extend : ∀ b : Live, ∃ d : Live, runEdge M σ b.val d.val := by
208     intro b
209     obtain ⟨a, hσ, ha⟩ := (h b.val b.property).2
210     obtain ⟨y, hy⟩ := M.post_nonempty b.val.2 a (Or.inl ha)
211     let c : Config Z A := ((b.val.2, a) :: b.val.1, y)
212     have he : runEdge M σ b.val c := ⟨a, hσ, ha, rfl, hy⟩
213     exact ⟨⟨c, Reach.tail b.property he⟩, he⟩
214   let step : Live → Live := fun b => Classical.choose (extend b)
215   let path : ℕ → Live := fun n => Nat.rec initial (fun _ b => step b) n
216   refine ⟨fun n => (path n).val, rfl, ?_, ?_⟩
217   · intro n
218     exact Classical.choose_spec (extend (path n))
219   · intro n
220     exact (h (path n).val (path n).property).1
221 
222 /-- Any history-dependent policy with the command guarantee starts in the
223 computed safe-running region. Past history and the stop epoch remain accessible. -/
224 theorem switching_mem_running [Fintype Z] (M : Model Z A) {P : Policy Z A} {x : Z}
225     (h : SwitchingGuarantee M P x) : x ∈ runningRegion M := by
226   let R : Z → Prop := fun y => ∃ c : Config Z A,
227     Reach (runEdge M (before P)) (start x) c ∧ c.2 = y
228   have hEnd : ∀ y, R y → y ∈ endingRegion M := by
229     intro y hy
230     obtain ⟨c, hc, rfl⟩ := hy
231     exact guarantee_mem_ending M (h.end_on_command c hc)
232   have hRun : ∀ y, R y → ∃ a ∈ M.run y, ∀ z ∈ M.post y a, R z := by
233     intro y hy
234     obtain ⟨c, hc, rfl⟩ := hy
235     obtain ⟨a, hσ, ha⟩ := (h.run_total c hc).2
236     refine ⟨a, ha, ?_⟩
237     intro z hz
238     let d : Config Z A := ((c.2, a) :: c.1, z)
239     have he : runEdge M (before P) c d := ⟨a, hσ, ha, rfl, hz⟩
240     exact ⟨d, Reach.tail hc he, rfl⟩
241   exact running_maximal M R hEnd hRun x ⟨start x, Reach.refl, rfl⟩
242 
243 /-- Source-facing Core 8.3 equivalence. No positional or bounded-time premise is
244 imposed on the policy in the necessary direction. The sufficient policy is
245 positional and has a separately proved first-entry-rank bound. -/
246 theorem safe_continuation_iff [Fintype Z] (M : Model Z A) (x : Z) :
247     x ∈ runningRegion M ↔ ∃ P : Policy Z A, SwitchingGuarantee M P x :=
248   ⟨fun hx => ⟨canonicalPolicy M, canonical_guarantee M hx⟩,
249    fun ⟨_, h⟩ => switching_mem_running M h⟩
250 
251 /-- The same constructed policy retains its exact ending budget at every command
252 configuration reachable before the command is received. -/
253 theorem command_rank_bound [Fintype Z] (M : Model Z A) {x : Z}
254     (hx : x ∈ runningRegion M) {anchor : Config Z A}
255     (hr : Reach (runEdge M (before (canonicalPolicy M))) (start x) anchor)
256     (p : ℕ → Config Z A) (h0 : p 0 = start anchor.2)
257     (n : ℕ) (hp : ∀ k, k < n →
258       endEdge M (after (canonicalPolicy M) anchor) (p k) (p (k + 1))) :
259     (p n).2 ∈ endingRegion M ∧ n + endRank M (p n).2 ≤ endRank M anchor.2 :=
260   ending_rank_budget M (runningRegion_subset_ending M (canonical_run_reachable M hx hr)) p h0 n hp
261 
262 
263 /-- The constructed command branch reaches the goal no later than its first-entry
264 rank, interpreted on legal nonterminal prefixes. -/
265 theorem command_rank_arrival [Fintype Z] (M : Model Z A) {x : Z}
266     (hx : x ∈ runningRegion M) {anchor : Config Z A}
267     (hr : Reach (runEdge M (before (canonicalPolicy M))) (start x) anchor)
268     (p : ℕ → Config Z A) (h0 : p 0 = start anchor.2)
269     (hp : ∀ k, k < endRank M anchor.2 →
270       endEdge M (after (canonicalPolicy M) anchor) (p k) (p (k + 1))) :
271     (p (endRank M anchor.2)).2 ∈ M.goal :=
272   ending_rank_arrival M (runningRegion_subset_ending M (canonical_run_reachable M hx hr)) p h0 hp
273 
274 /-- The full manuscript endpoint states the equivalence and the existence of the
275 same policy's first-entry-rank guarantee in one declaration. -/
276 theorem source_core83 [Fintype Z] (M : Model Z A) (x : Z) :
277     x ∈ runningRegion M ↔ ∃ P : Policy Z A,
278       SwitchingGuarantee M P x ∧
279       ∀ anchor, Reach (runEdge M (before P)) (start x) anchor →
280         ∀ p : ℕ → Config Z A, p 0 = start anchor.2 →
281           ∀ n, (∀ k, k < n → endEdge M (after P anchor) (p k) (p (k + 1))) →
282             n + endRank M (p n).2 ≤ endRank M anchor.2 := by
283   constructor
284   · intro hx
285     refine ⟨canonicalPolicy M, canonical_guarantee M hx, ?_⟩
286     intro anchor hr p h0 n hp
287     exact (command_rank_bound M hx hr p h0 n hp).2
288   · rintro ⟨P, h, _⟩
289     exact switching_mem_running M h
290 
291 end
292 end Komorebi.MachineTheory.SafeEnding

Back to source controls