Revision.lean

1 import MachineTheory.DependencyGraph
2 
3 /-! # Selective certificate reuse
4 
5 The checker receives only a typed restriction of the actual artifact state.
6 `Complete` is an explicit semantic locality obligation, not a hash property.
7 Old witnesses carry established old claims. New external premises remain explicit.
8 -/
9 namespace Komorebi.MachineTheory.Dependency
10 open Finset
11 variable {V I : Type*} [Fintype V] [DecidableEq V]
12 variable {A : I → Type*} [∀ i, DecidableEq (A i)] {W : V → Type*}
13 
14 structure System (G : Graph V I) (A : I → Type*) (W : V → Type*) where
15   claim : (∀ i, A i) → V → Prop
16   external : (∀ i, A i) → V → Prop
17   check : (v : V) → ((i : {i // i ∈ G.direct v}) → A i.val) → W v → Bool
18   sound : ∀ a v w, check v (G.view a v) w = true → external a v →
19     (∀ u ∈ G.parents v, claim a u) → claim a v
20 
21 variable {G : Graph V I} (S : System G A W)
22 
23 /-- Semantic completeness for the declared restriction and parent claims.
24 It is a proof obligation supplied by an instance, not automatically inferred. -/
25 def System.Complete : Prop :=
26   ∀ a b v, G.view a v = G.view b v →
27     (∀ u ∈ G.parents v, S.claim a u ↔ S.claim b u) →
28     (S.external a v ↔ S.external b v) → (S.claim a v ↔ S.claim b v)
29 
30 def System.Established (a : ∀ i, A i) (v : V) (w : W v) : Prop :=
31   S.check v (G.view a v) w = true ∧ S.external a v ∧ S.claim a v
32 
33 /-- Outside the exact forward closure, the full claim meaning is preserved.
34 The induction uses the checked topological rank and all parent meanings. -/
35 theorem System.nonstale_meaning (complete : S.Complete)
36     (rank : V → ℕ) (ordered : G.Ranked rank)
37     (a b : ∀ i, A i)
38     (external : ∀ v, v ∉ G.stale a b → (S.external a v ↔ S.external b v))
39     (v : V) (hv : v ∉ G.stale a b) : S.claim a v ↔ S.claim b v := by
40   have go : ∀ n v, rank v = n → v ∉ G.stale a b → (S.claim a v ↔ S.claim b v) := by
41     intro n
42     induction n using Nat.strong_induction_on with
43     | h n ih =>
44       intro v hn hclean
45       apply complete a b v (G.nonstale_view a b hclean)
46       · intro u hu
47         exact ih (rank u) (by rw [← hn]; exact ordered v u hu) u rfl
48           (G.nonstale_parents a b hclean hu)
49       · exact external v hclean
50   exact go (rank v) v rfl hv
51 
52 /-- Core 7.1, reuse direction. Equal names or digests do not appear as premises. -/
53 theorem System.selective_reuse (complete : S.Complete)
54     (rank : V → ℕ) (ordered : G.Ranked rank)
55     (a b : ∀ i, A i) (old : ∀ v, W v)
56     (previously_established : ∀ v, S.Established a v (old v))
57     (external_now : ∀ v, v ∉ G.stale a b → S.external b v) :
58     ∀ v, v ∉ G.stale a b → S.Established b v (old v) := by
59   intro v hv
60   obtain ⟨hc,he,hp⟩ := previously_established v
61   refine ⟨?_,external_now v hv,?_⟩
62   · rw [← G.nonstale_view a b hv]
63     exact hc
64   · have hm := S.nonstale_meaning complete rank ordered a b
65       (fun u hu => ⟨fun _ => external_now u hu,fun _ => (previously_established u).2.1⟩) v hv
66     exact hm.mp hp
67 
68 omit [Fintype V] [DecidableEq V] [∀ i, DecidableEq (A i)] in
69 /-- This local restoration rule consumes actual revised parents and external premises. -/
70 theorem System.restore (b : ∀ i, A i) (v : V) (w : W v)
71     (checked : S.check v (G.view b v) w = true) (he : S.external b v)
72     (parents : ∀ u ∈ G.parents v, S.claim b u) : S.Established b v w :=
73   ⟨checked,he,S.sound b v w checked he parents⟩
74 
75 /-- A checker's equality is obtained from its actual restricted input. -/
76 theorem System.check_unchanged (a b : ∀ i, A i) (v : V) (w : W v)
77     (hv : v ∉ G.stale a b) : S.check v (G.view a v) w = S.check v (G.view b v) w := by
78   rw [G.nonstale_view a b hv]
79 
80 end Komorebi.MachineTheory.Dependency

Back to source controls