PriceRevision.lean

1 import MachineTheory.PriceExamples
2 import MachineTheory.RevisionAdmission
3 
4 /-! # Repricing preserves a controller but not its old benefit certificate
5 
6 This instance uses Block 11's actual invalidation and replay. The program and
7 event semantics are fixed. Artifact false is an integer read price; artifact true
8 is a recorded integer saving, with test price fixed at one. A correct calculation
9 and a nonnegative advantage are deliberately different dependent claims.
10 -/
11 namespace Komorebi.MachineTheory.PriceRevision
12 open Dependency PriceExamples ResourcePrices Finset
13 
14 abbrev Node := Fin 3
15 abbrev Data := Bool → ℤ
16 
17 /-- Calculated directly from the inherited compiled event counters. -/
18 def actualSaving (r : ℤ) : ℤ :=
19   r*(fullCounts false : ℤ)+(fullCounts true : ℤ) -
20     (r*(streamCounts false : ℤ)+(streamCounts true : ℤ))
21 
22 theorem actualSaving_eq (r : ℤ) : actualSaving r=31*r-153 := by
23   rcases counter_binding with ⟨h0,h1,h2,h3⟩
24   simp only [actualSaving,h0,h1,h2,h3]
25   ring
26 
27 /-- The exact integer quote agrees with the general real-price theorem. -/
28 theorem actualSaving_real (r : ℤ) :
29     (actualSaving r : ℝ) = saving perUse (prices (r : ℝ) 1) := by
30   rw [actualSaving_eq,priced_scan]
31   push_cast
32   ring
33 
34 /-- Node 0: execution; node 1: correct quote; node 2: nonnegative advantage. -/
35 def graph : Graph Node Bool where
36   parents := fun v => if v=2 then {1} else ∅
37   direct := fun v => if v=0 then ∅ else if v=1 then univ else {true}
38 
39 def rank (v : Node) : ℕ := v.val
40 
41 theorem rank_checked : graph.Ranked rank := by
42   unfold Graph.Ranked
43   decide
44 
45 def meaning (a : Data) (v : Node) : Prop :=
46   if v=0 then
47     PrefixExamples.streamEight.answer=PrefixExamples.fullEight.answer ∧
48       ∀ t, PrefixExamples.streamEight.answer=some t → BinaryExamples.eight.Valid 3 univ t
49   else if v=1 then a true=actualSaving (a false)
50   else a true=actualSaving (a false) ∧ 0 ≤ a true
51 
52 /-- The checker sees exactly the declared local view. -/
53 def localCheck : (v : Node) → ({i // i∈graph.direct v} → ℤ) → Bool → Bool
54   | ⟨0,_⟩, _, w => w
55   | ⟨1,_⟩, a, w => w && decide (a ⟨true,by change true ∈ graph.direct (1 : Node); decide⟩=actualSaving (a ⟨false,by change false ∈ graph.direct (1 : Node); decide⟩))
56   | ⟨2,_⟩, a, w => w && decide (0 ≤ a ⟨true,by change true ∈ graph.direct (2 : Node); decide⟩)
57   | ⟨n+3,h⟩, _, _ => False.elim (by omega)
58 
59 def system : System graph (fun _ => ℤ) (fun _ => Bool) where
60   claim := meaning
61   external := fun _ _ => True
62   check := localCheck
63   sound := by
64     intro a v w hc _ hp
65     fin_cases v
66     · exact same_valid_controller
67     · change (w && decide (a true=actualSaving (a false)))=true at hc
68       change a true=actualSaving (a false)
69       exact of_decide_eq_true (Bool.and_eq_true_iff.mp hc).2
70     · have hv : a true=actualSaving (a false) := hp 1 (by decide)
71       change (w && decide (0 ≤ a true))=true at hc
72       exact ⟨hv,of_decide_eq_true (Bool.and_eq_true_iff.mp hc).2⟩
73 
74 /-- Semantic completeness is proved for this quote family, including invalid quotes. -/
75 theorem meanings_complete : system.Complete := by
76   intro a b v hview hp _
77   fin_cases v
78   · rfl
79   · have h0 : a false=b false := congrFun hview ⟨false,by decide⟩
80     have h1 : a true=b true := congrFun hview ⟨true,by decide⟩
81     change (a true=actualSaving (a false)) ↔ (b true=actualSaving (b false))
82     rw [h0,h1]
83   · have h1 : a true=b true := congrFun hview ⟨true,by decide⟩
84     have hv := hp 1 (by decide)
85     change (a true=actualSaving (a false)) ↔ (b true=actualSaving (b false)) at hv
86     change (a true=actualSaving (a false) ∧ 0 ≤ a true) ↔
87       (b true=actualSaving (b false) ∧ 0 ≤ b true)
88     apply and_congr hv
89     rw [h1]
90 
91 def before : Data := fun i => if i then 2 else 5
92 
93 def staleQuote : Data := fun i => if i then 2 else 1
94 
95 def correctedQuote : Data := fun i => if i then -122 else 1
96 
97 def oldWitness : Node → Bool := fun _ => true
98 
99 def allFresh : Node → Option Bool := fun _ => some true
100 
101 def externalOK : Node → Bool := fun _ => true
102 
103 theorem old_checks : ∀ v, system.check v (graph.view before v) (oldWitness v)=true := by
104   decide
105 
106 /-- Every old certificate is established before any reuse is attempted. -/
107 theorem old_established : ∀ v,system.Established before v (oldWitness v) :=
108   system.established_from_checks rank rank_checked before oldWitness old_checks (fun _ => trivial)
109 
110 theorem reprice_propagates :
111     graph.changedRoots before staleQuote={1} ∧ graph.stale before staleQuote={1,2} ∧
112     graph.stale before correctedQuote={1,2} := by
113   decide
114 
115 def staleResult := system.finish before staleQuote oldWitness allFresh externalOK rank
116 
117 def correctedResult := system.finish before correctedQuote oldWitness allFresh externalOK rank
118 
119 /-- A still-positive old quote is rejected, and its apparent benefit cannot be used. -/
120 theorem stale_quote_outcomes :
121     staleResult 0=.reused true ∧ staleResult 1=.rejected ∧ staleResult 2=.blockedParents := by
122   decide
123 
124 /-- A valid negative quote is re-established without inventing a benefit certificate. -/
125 theorem corrected_quote_outcomes :
126     correctedResult 0=.reused true ∧ correctedResult 1=.rechecked true ∧ correctedResult 2=.rejected := by
127   decide
128 
129 /-- Soundness is inherited from the same generic replay, including all partial stages. -/
130 theorem every_stage_sound (a : Data) (n : ℕ) :
131     system.SoundState a (system.replay before a oldWitness allFresh externalOK rank n) :=
132   system.replay_sound meanings_complete rank rank_checked before a oldWitness allFresh externalOK
133     old_established (fun _ _ => trivial) (fun _ _ => trivial) n
134 
135 theorem restored_calculation : system.Established correctedQuote 1 true := by
136   have hs := every_stage_sound correctedQuote (finishAt rank)
137   apply hs 1 true
138   change (correctedResult 1).witness?=some true
139   rw [corrected_quote_outcomes.2.1]
140   rfl
141 
142 theorem benefit_now_false : ¬ system.claim correctedQuote 2 := by
143   change ¬ (correctedQuote true=actualSaving (correctedQuote false) ∧ 0 ≤ correctedQuote true)
144   norm_num [correctedQuote]
145 
146 /-- Repricing has not changed the actual program returned by either compiler. -/
147 theorem execution_certificate_reused : system.Established correctedQuote 0 true := by
148   have hs := every_stage_sound correctedQuote (finishAt rank)
149   apply hs 0 true
150   change (correctedResult 0).witness?=some true
151   rw [corrected_quote_outcomes.1]
152   rfl
153 
154 /-- The restored quote is the actual real saving, including its negative sign. -/
155 theorem restored_negative_real_saving :
156     saving perUse (prices (correctedQuote false : ℝ) 1)= (correctedQuote true : ℝ) ∧
157       saving perUse (prices (correctedQuote false : ℝ) 1) < 0 := by
158   have hq : correctedQuote true=actualSaving (correctedQuote false) := restored_calculation.2.2
159   constructor
160   · rw [← actualSaving_real,← hq]
161   · rw [priced_scan]
162     norm_num [correctedQuote]
163 
164 end Komorebi.MachineTheory.PriceRevision

Back to source controls