RevisionReplay.lean

1 import MachineTheory.Revision
2 import Mathlib.Data.Finset.Lattice.Fold
3 
4 /-! # Finite selective rechecking
5 
6 One fixed revised artifact snapshot is used for an entire replay. Unaffected witnesses
7 are copied. Affected vertices are checked in certified rank layers. Missing evidence,
8 failed local checks and unavailable parents/external premises are not falsehood proofs.
9 -/
10 namespace Komorebi.MachineTheory.Dependency
11 open Finset
12 
13 inductive Verdict (W : Type*) where
14   | pending
15   | missing
16   | rejected
17   | blockedParents
18   | blockedExternal
19   | reused (w : W)
20   | rechecked (w : W)
21   deriving DecidableEq, Repr
22 
23 def Verdict.witness? {W : Type*} : Verdict W → Option W
24   | .reused w | .rechecked w => some w
25   | _ => none
26 
27 def Verdict.ready {W : Type*} (s : Verdict W) : Bool := s.witness?.isSome
28 
29 theorem Verdict.ready_iff {W : Type*} (s : Verdict W) :
30     s.ready = true ↔ ∃ w, s.witness? = some w := by
31   cases s <;> simp [ready,witness?]
32 
33 variable {V I : Type*} [Fintype V] [DecidableEq V]
34 variable {A : I → Type*} [∀ i, DecidableEq (A i)] {W : V → Type*}
35 variable {G : Graph V I} (S : System G A W)
36 
37 def System.SoundState (a : ∀ i, A i) (s : ∀ v, Verdict (W v)) : Prop :=
38   ∀ v w, (s v).witness? = some w → S.Established a v w
39 
40 def initialState (G : Graph V I) (a b : ∀ i, A i) (old : ∀ v, W v) :
41     ∀ v, Verdict (W v) := fun v =>
42   if v ∈ G.stale a b then .pending else .reused (old v)
43 
44 /-- No evaluator or premise is silently supplied by the witness under test. -/
45 def System.evaluate (b : ∀ i, A i) (fresh : ∀ v, Option (W v))
46     (external : V → Bool) (s : ∀ v, Verdict (W v)) (v : V) : Verdict (W v) :=
47   if (∀ u ∈ G.parents v, (s u).ready = true) then
48     if external v then
49       match fresh v with
50       | none => .missing
51       | some w => if S.check v (G.view b v) w then .rechecked w else .rejected
52     else .blockedExternal
53   else .blockedParents
54 
55 /-- Only affected vertices in the current rank layer incur a new local check. -/
56 def System.layer (a b : ∀ i, A i) (fresh : ∀ v, Option (W v))
57     (external : V → Bool) (rank : V → ℕ) (k : ℕ)
58     (s : ∀ v, Verdict (W v)) : ∀ v, Verdict (W v) := fun v =>
59   if rank v = k ∧ v ∈ G.stale a b then S.evaluate b fresh external s v else s v
60 
61 def System.replay (S : System G A W) (a b : ∀ i, A i) (old : ∀ v, W v) (fresh : ∀ v, Option (W v))
62     (external : V → Bool) (rank : V → ℕ) : ℕ → (∀ v, Verdict (W v))
63   | 0 => initialState G a b old
64   | k+1 => S.layer a b fresh external rank k (S.replay a b old fresh external rank k)
65 
66 def finishAt (rank : V → ℕ) : ℕ := univ.sup rank + 1
67 
68 def System.finish (a b : ∀ i, A i) (old : ∀ v, W v) (fresh : ∀ v, Option (W v))
69     (external : V → Bool) (rank : V → ℕ) : ∀ v, Verdict (W v) :=
70   S.replay a b old fresh external rank (finishAt rank)
71 
72 omit [Fintype V] [DecidableEq V] [∀ i, DecidableEq (A i)] in
73 /-- A sound ready entry provides the premise to its dependents. -/
74 theorem System.claim_of_ready (b : ∀ i, A i) (s : ∀ v, Verdict (W v))
75     (hs : S.SoundState b s) {v : V} (hv : (s v).ready = true) : S.claim b v := by
76   obtain ⟨w,hw⟩ := (Verdict.ready_iff (s v)).mp hv
77   exact (hs v w hw).2.2
78 
79 omit [∀ i, DecidableEq (A i)] in
80 theorem System.evaluate_sound (b : ∀ i, A i) (fresh : ∀ v, Option (W v))
81     (external : V → Bool) (s : ∀ v, Verdict (W v))
82     (hs : S.SoundState b s) (he : ∀ v, external v = true → S.external b v) :
83     ∀ v w, (S.evaluate b fresh external s v).witness? = some w → S.Established b v w := by
84   intro v w hw
85   unfold evaluate at hw
86   split at hw
87   next hp =>
88     split at hw
89     next hex =>
90       cases hf : fresh v with
91       | none => simp [hf,Verdict.witness?] at hw
92       | some w' =>
93         simp only [hf] at hw
94         split at hw
95         next hc =>
96           have heq : w'=w := Option.some.inj hw
97           subst w'
98           apply S.restore b v w hc (he v hex)
99           intro u hu
100           exact S.claim_of_ready b s hs (hp u hu)
101         next => simp [Verdict.witness?] at hw
102     next => simp [Verdict.witness?] at hw
103   next => simp [Verdict.witness?] at hw
104 
105 omit [∀ i, DecidableEq (A i)] in
106 /-- Failed availability tests cannot create certificates. -/
107 theorem System.evaluate_ready_iff (b : ∀ i, A i) (fresh : ∀ v, Option (W v))
108     (external : V → Bool) (s : ∀ v, Verdict (W v)) (v : V) :
109     (S.evaluate b fresh external s v).ready = true ↔
110       (∀ u ∈ G.parents v, (s u).ready = true) ∧ external v = true ∧
111         ∃ w, fresh v = some w ∧ S.check v (G.view b v) w = true := by
112   constructor
113   · intro hr
114     unfold evaluate at hr
115     split at hr
116     next hp =>
117       split at hr
118       next he =>
119         cases hf : fresh v with
120         | none => simp [hf,Verdict.ready,Verdict.witness?] at hr
121         | some w =>
122           simp only [hf] at hr
123           split at hr
124           next hc => exact ⟨hp,he,⟨w,rfl,hc⟩⟩
125           next => simp [Verdict.ready,Verdict.witness?] at hr
126       next => simp [Verdict.ready,Verdict.witness?] at hr
127     next => simp [Verdict.ready,Verdict.witness?] at hr
128   · rintro ⟨hp,he,w,hf,hc⟩
129     unfold evaluate
130     rw [ite_eq_left hp,ite_eq_left he,hf]
131     change (if S.check v (G.view b v) w = true then Verdict.rechecked w else Verdict.rejected).ready = true
132     rw [ite_eq_left hc]
133     rfl
134 
135 /-- The original witness is copied literally outside the affected closure. -/
136 theorem System.replay_unaffected (a b : ∀ i, A i) (old : ∀ v, W v)
137     (fresh : ∀ v, Option (W v)) (external : V → Bool) (rank : V → ℕ)
138     (n : ℕ) (v : V) (hv : v ∉ G.stale a b) :
139     S.replay a b old fresh external rank n v = .reused (old v) := by
140   induction n with
141   | zero => simp [replay,initialState,hv]
142   | succ n ih => simp [replay,layer,hv,ih]
143 
144 /-- Soundness holds at every intermediate replay state, including partial failures. -/
145 theorem System.replay_sound (complete : S.Complete) (rank : V → ℕ) (ordered : G.Ranked rank)
146     (a b : ∀ i, A i) (old : ∀ v, W v) (fresh : ∀ v, Option (W v)) (external : V → Bool)
147     (hold : ∀ v, S.Established a v (old v))
148     (hclean : ∀ v, v ∉ G.stale a b → S.external b v)
149     (he : ∀ v, external v = true → S.external b v) (n : ℕ) :
150     S.SoundState b (S.replay a b old fresh external rank n) := by
151   induction n with
152   | zero =>
153     intro v w hw
154     change (initialState G a b old v).witness? = some w at hw
155     by_cases hv : v ∈ G.stale a b
156     · simp [initialState,hv,Verdict.witness?] at hw
157     · have heq : old v = w := by simpa [initialState,hv,Verdict.witness?] using hw
158       subst w
159       exact S.selective_reuse complete rank ordered a b old hold hclean v hv
160   | succ n ih =>
161     intro v w hw
162     change (S.layer a b fresh external rank n (S.replay a b old fresh external rank n) v).witness? = some w at hw
163     unfold layer at hw
164     split at hw
165     · exact S.evaluate_sound b fresh external _ ih he v w hw
166     · exact ih v w hw
167 
168 /-- No local checker is rerun on unaffected vertices; only the rank-layer entries change. -/
169 theorem System.replay_after_rank (a b : ∀ i, A i) (old : ∀ v, W v)
170     (fresh : ∀ v, Option (W v)) (external : V → Bool) (rank : V → ℕ)
171     {n : ℕ} {v : V} (hv : rank v < n) :
172     S.replay a b old fresh external rank (n+1) v = S.replay a b old fresh external rank n v := by
173   simp [replay,layer,Nat.ne_of_lt hv]
174 
175 /-- If revised local evidence is available and passes, topological replay restores it.
176 This is conditional completeness of this procedure, not completeness of proof search. -/
177 theorem System.replay_complete (rank : V → ℕ) (ordered : G.Ranked rank)
178     (a b : ∀ i, A i) (old : ∀ v, W v) (fresh : ∀ v, Option (W v)) (external : V → Bool)
179     (he : ∀ v ∈ G.stale a b, external v = true)
180     (hf : ∀ v ∈ G.stale a b, ∃ w, fresh v = some w ∧ S.check v (G.view b v) w = true)
181     (n : ℕ) : ∀ v, rank v < n → (S.replay a b old fresh external rank n v).ready = true := by
182   induction n with
183   | zero => intro v hv; omega
184   | succ n ih =>
185     intro v hv
186     by_cases hn : rank v < n
187     · rw [S.replay_after_rank a b old fresh external rank hn]
188       exact ih v hn
189     · have hvn : rank v = n := by omega
190       by_cases hstale : v ∈ G.stale a b
191       · change (S.layer a b fresh external rank n (S.replay a b old fresh external rank n) v).ready = true
192         simp only [layer,hvn,hstale,and_self,ite_true]
193         apply (S.evaluate_ready_iff b fresh external _ v).mpr
194         refine ⟨?_,he v hstale,hf v hstale⟩
195         intro u hu
196         apply ih u
197         rw [← hvn]
198         exact ordered v u hu
199       · rw [S.replay_unaffected a b old fresh external rank (n+1) v hstale]
200         rfl
201 
202 /-- The finite completed replay supplies every revised claim when its actual inputs pass. -/
203 theorem System.restoration (complete : S.Complete) (rank : V → ℕ) (ordered : G.Ranked rank)
204     (a b : ∀ i, A i) (old : ∀ v, W v) (fresh : ∀ v, Option (W v)) (external : V → Bool)
205     (hold : ∀ v, S.Established a v (old v))
206     (hclean : ∀ v, v ∉ G.stale a b → S.external b v)
207     (he : ∀ v, external v = true → S.external b v)
208     (havailable : ∀ v ∈ G.stale a b, external v = true)
209     (hchecks : ∀ v ∈ G.stale a b, ∃ w, fresh v = some w ∧ S.check v (G.view b v) w = true) :
210     ∀ v, ∃ w, (S.finish a b old fresh external rank v).witness? = some w ∧ S.Established b v w := by
211   intro v
212   have hr : rank v < finishAt rank := by
213     have h := Finset.le_sup (f := rank) (Finset.mem_univ v)
214     unfold finishAt
215     omega
216   have ready := S.replay_complete rank ordered a b old fresh external havailable hchecks (finishAt rank) v hr
217   obtain ⟨w,hw⟩ := (Verdict.ready_iff _).mp ready
218   refine ⟨w,hw,?_⟩
219   exact S.replay_sound complete rank ordered a b old fresh external hold hclean he _ v w hw
220 
221 /-- Partial replay certifies only the entries whose witnesses it actually returns. -/
222 theorem System.finish_sound (complete : S.Complete) (rank : V → ℕ) (ordered : G.Ranked rank)
223     (a b : ∀ i, A i) (old : ∀ v, W v) (fresh : ∀ v, Option (W v)) (external : V → Bool)
224     (hold : ∀ v, S.Established a v (old v))
225     (hclean : ∀ v, v ∉ G.stale a b → S.external b v)
226     (he : ∀ v, external v = true → S.external b v) :
227     S.SoundState b (S.finish a b old fresh external rank) :=
228   S.replay_sound complete rank ordered a b old fresh external hold hclean he _
229 
230 end Komorebi.MachineTheory.Dependency

Back to source controls