automation_structures/primitives/
convergence_governor_phase_aware.rs

1// Phase-aware convergence-governor executable correspondence boundary.
2//
3// A sub-threshold delta is classified differently before and after a threshold
4// event. The gradient_phase field records that classification, and the
5// peak_observed latch prevents COOLING from carrying a COLD phase. The TLA+
6// `ConvergenceGovernorPhaseAware` spec has four state variables —
7// state, gradient_phase, delta_history, peak_observed — and its .cfg checks
8// four invariants:
9//
10//   TypeInvariant             == well-typed (state/phase enums, len<=Window, peak bool)
11//   NoCoolingFromCold         == state = COOLING => gradient_phase /= COLD
12//   ConvergenceRequiresHistory== state ∈ {COOLING,CONVERGED} => peak_observed
13//   ConvergedRequiresPeak     == state = CONVERGED => peak_observed
14//
15// All four are discharged under the full Update dynamics. The inductive proof
16// carries the `WarmStateRequiresPeak` strengthening:
17//   peak_implies: state ∈ {COOLING,CONVERGED,AWAKENED} => peak_observed
18// (the AWAKENED case is required to close the AWAKENED -> CONVERGED step).
19// ConvergenceRequiresHistory and ConvergedRequiresPeak then follow as weakenings.
20// NoCoolingFromCold holds because the only routes into COOLING either force
21// new_peak (ACTIVE -> COOLING) or stay in COOLING where peak_observed was
22// already TRUE, and ClassifyPhase returns COLD only when peak is FALSE.
23//
24// `update` computes the post-slide window average internally. Callers supply
25// only the new delta, so ordinary Rust and verified callers share one canonical
26// transition boundary.
27
28use vstd::prelude::*;
29
30verus! {
31
32/// Governor state. Enum => `state ∈ GovernorStates` holds by construction.
33#[derive(Clone, Copy, PartialEq, Eq, Debug)]
34pub enum GovState {
35    /// Learning remains active.
36    Active,
37    /// A peak was observed and the recent average is declining.
38    Cooling,
39    /// The recent average is below the convergence threshold.
40    Converged,
41    /// Activity after convergence exceeded the awakening threshold.
42    Awakened,
43}
44
45/// Gradient-trajectory phase. Enum => `gradient_phase ∈ GradientPhases` by
46/// construction.
47#[derive(Clone, Copy, PartialEq, Eq, Debug)]
48pub enum Phase {
49    /// No peak has been observed and the delta remains below threshold.
50    Cold,
51    /// The first threshold event has been observed.
52    Warming,
53    /// A post-peak delta is at or above threshold.
54    ActiveLearning,
55    /// A post-peak delta is below threshold.
56    Declining,
57}
58
59/// A phase-aware convergence governor.
60pub struct ConvergenceGovernorPhaseAware {
61    pub threshold: u64,
62    pub awaken_threshold: u64,
63    pub window: usize,
64    pub max_delta: u64,
65    pub state: GovState,
66    pub gradient_phase: Phase,
67    pub delta_history: Vec<u64>,
68    pub peak_observed: bool,
69}
70
71impl ConvergenceGovernorPhaseAware {
72    // ── Phase classification (TLA+ ClassifyPhase) ───────────────────────
73
74    /// Classify the current delta and pre-step peak latch. `Declining` records
75    /// a sub-threshold delta after the latch; it does not assert monotonicity.
76    pub open spec fn classify_phase_spec(delta: u64, peak: bool, threshold: u64) -> Phase {
77        if !peak && delta < threshold {
78            Phase::Cold
79        } else if !peak && delta >= threshold {
80            Phase::Warming
81        } else if peak && delta >= threshold {
82            Phase::ActiveLearning
83        } else {
84            Phase::Declining
85        }
86    }
87
88    /// Executable ClassifyPhase.
89    pub fn classify_phase(delta: u64, peak: bool, threshold: u64) -> (p: Phase)
90        ensures p == Self::classify_phase_spec(delta, peak, threshold),
91    {
92        if !peak && delta < threshold {
93            Phase::Cold
94        } else if !peak && delta >= threshold {
95            Phase::Warming
96        } else if peak && delta >= threshold {
97            Phase::ActiveLearning
98        } else {
99            Phase::Declining
100        }
101    }
102
103    // ── Transition (TLA+ Update state CASE) ─────────────────────────────
104
105    /// State transition corresponding to the TLA+ `Update` CASE expression.
106    /// ACTIVE -> COOLING requires the post-step peak latch.
107    pub open spec fn next_state_spec(s: GovState, avg: u64, new_peak: bool, threshold: u64, awaken: u64)
108        -> GovState {
109        match s {
110            GovState::Active =>
111                if avg < threshold * 2 && new_peak { GovState::Cooling } else { GovState::Active },
112            GovState::Cooling =>
113                if avg < threshold { GovState::Converged }
114                else if avg >= threshold * 2 { GovState::Active }
115                else { GovState::Cooling },
116            GovState::Converged =>
117                if avg > awaken { GovState::Awakened } else { GovState::Converged },
118            GovState::Awakened =>
119                if avg < threshold { GovState::Converged } else { GovState::Awakened },
120        }
121    }
122
123    /// Executable transition.
124    pub fn next_state(s: GovState, avg: u64, new_peak: bool, threshold: u64, awaken: u64)
125        -> (out: GovState)
126        requires threshold <= u64::MAX / 2,
127        ensures out == Self::next_state_spec(s, avg, new_peak, threshold, awaken),
128    {
129        match s {
130            GovState::Active =>
131                if avg < threshold * 2 && new_peak { GovState::Cooling } else { GovState::Active },
132            GovState::Cooling =>
133                if avg < threshold { GovState::Converged }
134                else if avg >= threshold * 2 { GovState::Active }
135                else { GovState::Cooling },
136            GovState::Converged =>
137                if avg > awaken { GovState::Awakened } else { GovState::Converged },
138            GovState::Awakened =>
139                if avg < threshold { GovState::Converged } else { GovState::Awakened },
140        }
141    }
142
143    // ── Specifications ──────────────────────────────────────────────────
144
145    /// TLA+ `TypeInvariant`'s window clause (+ the overflow / nonempty-window
146    /// bounds; the enum and bool clauses are carried by the types).
147    pub open spec fn type_invariant(&self) -> bool {
148        self.delta_history.len() <= self.window
149            && self.threshold <= u64::MAX / 2
150            && self.window >= 1
151            && self.window as int * self.max_delta as int <= u64::MAX as int
152            && forall|i: int| 0 <= i < self.delta_history.len() ==>
153                #[trigger] self.delta_history@[i] <= self.max_delta
154    }
155
156    /// `WarmStateRequiresPeak` strengthening: any non-ACTIVE state implies a
157    /// peak was observed. Includes AWAKENED so AWAKENED -> CONVERGED preserves it.
158    pub open spec fn peak_implies(&self) -> bool {
159        (self.state == GovState::Cooling || self.state == GovState::Converged
160            || self.state == GovState::Awakened) ==> self.peak_observed
161    }
162
163    /// TLA+ `NoCoolingFromCold`.
164    pub open spec fn no_cooling_from_cold(&self) -> bool {
165        self.state == GovState::Cooling ==> self.gradient_phase != Phase::Cold
166    }
167
168    /// TLA+ `ConvergenceRequiresHistory` (a weakening of peak_implies).
169    pub open spec fn convergence_requires_history(&self) -> bool {
170        (self.state == GovState::Cooling || self.state == GovState::Converged) ==> self.peak_observed
171    }
172
173    /// TLA+ `ConvergedRequiresPeak` (a weakening of peak_implies).
174    pub open spec fn converged_requires_peak(&self) -> bool {
175        self.state == GovState::Converged ==> self.peak_observed
176    }
177
178    /// Full maintained invariant.
179    pub open spec fn inv(&self) -> bool {
180        self.type_invariant() && self.peak_implies() && self.no_cooling_from_cold()
181    }
182
183    /// TLA+ `SumSeq`: the sum of a delta window.
184    pub open spec fn sum_seq(s: Seq<u64>) -> int
185        decreases s.len(),
186    {
187        if s.len() == 0 {
188            0
189        } else {
190            Self::sum_seq(s.take(s.len() - 1)) + s[s.len() - 1] as int
191        }
192    }
193
194    /// Extending a delta sequence extends its mathematical sum by that delta.
195    pub proof fn lemma_sum_push(s: Seq<u64>, delta: u64)
196        ensures Self::sum_seq(s.push(delta)) == Self::sum_seq(s) + delta as int,
197    {
198        assert(s.push(delta).take(s.len() as int) =~= s);
199    }
200
201    /// TLA+ `Update`'s `new_history`: drop the oldest when the window is full,
202    /// then append the new delta. A function of the PRE-state and `delta` only.
203    pub open spec fn slide_window(&self, delta: u64) -> Seq<u64> {
204        if self.delta_history@.len() >= self.window {
205            self.delta_history@.drop_first().push(delta)
206        } else {
207            self.delta_history@.push(delta)
208        }
209    }
210
211    /// TLA+ `Update`'s `avg`. The slid window is never empty (`type_invariant`
212    /// carries `window >= 1`), so the division is well defined.
213    pub open spec fn window_avg(&self, delta: u64) -> int {
214        Self::sum_seq(self.slide_window(delta)) / self.slide_window(delta).len() as int
215    }
216
217    // ── Init (TLA+ Init) ────────────────────────────────────────────────
218
219    /// Start ACTIVE / COLD / no peak. Realises the TLA+ `Init`.
220    pub fn new(threshold: u64, awaken_threshold: u64, window: usize, max_delta: u64)
221        -> (g: ConvergenceGovernorPhaseAware)
222        requires
223            threshold <= u64::MAX / 2,
224            window >= 1,
225            window as int * max_delta as int <= u64::MAX as int,
226        ensures
227            g.threshold == threshold,
228            g.awaken_threshold == awaken_threshold,
229            g.window == window,
230            g.max_delta == max_delta,
231            g.state == GovState::Active,
232            g.gradient_phase == Phase::Cold,
233            g.delta_history@.len() == 0,
234            g.peak_observed == false,
235            g.inv(),
236    {
237        ConvergenceGovernorPhaseAware {
238            threshold, awaken_threshold, window, max_delta,
239            state: GovState::Active, gradient_phase: Phase::Cold, delta_history: Vec::new(),
240            peak_observed: false,
241        }
242    }
243
244    // ── Update (TLA+ Update) ────────────────────────────────────────────
245
246    /// One governor step: classify the phase, update the peak latch, slide the
247    /// window, compute its average, and transition. Realises the TLA+
248    /// `Update(delta)` and re-establishes all four checked invariants.
249    pub fn update(&mut self, delta: u64) -> (avg: u64)
250        requires
251            old(self).inv(),
252            delta <= old(self).max_delta,
253        ensures
254            avg as int == old(self).window_avg(delta),
255            final(self).threshold == old(self).threshold,
256            final(self).awaken_threshold == old(self).awaken_threshold,
257            final(self).window == old(self).window,
258            final(self).max_delta == old(self).max_delta,
259            final(self).gradient_phase
260                == Self::classify_phase_spec(delta, old(self).peak_observed, old(self).threshold),
261            final(self).peak_observed == (old(self).peak_observed || delta >= old(self).threshold),
262            final(self).state == Self::next_state_spec(
263                old(self).state, avg,
264                old(self).peak_observed || delta >= old(self).threshold,
265                old(self).threshold, old(self).awaken_threshold),
266            // Transition fidelity: `type_invariant()` bounds only
267            // the post-state window's LENGTH; without this the contract admits
268            // a governor that classifies the phase and transitions correctly and
269            // never records the delta.
270            final(self).delta_history@ == old(self).slide_window(delta),
271            final(self).type_invariant(),
272            final(self).no_cooling_from_cold(),
273            final(self).convergence_requires_history(),
274            final(self).converged_requires_peak(),
275            final(self).inv(),
276    {
277        let old_peak = self.peak_observed;
278        let old_state = self.state;
279        let new_phase = Self::classify_phase(delta, old_peak, self.threshold);
280        let new_peak = old_peak || (delta >= self.threshold);
281        let ghost pre_hist = self.delta_history@;
282        if self.delta_history.len() >= self.window {
283            self.delta_history.remove(0);
284            assert(self.delta_history@ =~= pre_hist.drop_first());
285        }
286        self.delta_history.push(delta);
287        assert(self.delta_history@ =~= old(self).slide_window(delta));
288        proof {
289            assert(self.delta_history.len() <= self.window);
290            assert(self.delta_history.len() as int * self.max_delta as int
291                <= self.window as int * self.max_delta as int) by (nonlinear_arith)
292                requires
293                    self.delta_history.len() <= self.window,
294                    self.max_delta >= 0;
295        }
296        let avg = Self::history_average(&self.delta_history, self.max_delta);
297        let new_state = Self::next_state(
298            old_state,
299            avg,
300            new_peak,
301            self.threshold,
302            self.awaken_threshold,
303        );
304        self.gradient_phase = new_phase;
305        self.peak_observed = new_peak;
306        self.state = new_state;
307        avg
308    }
309
310    fn history_average(history: &Vec<u64>, _max_delta: u64) -> (average: u64)
311        requires
312            history.len() >= 1,
313            history.len() as int * _max_delta as int <= u64::MAX as int,
314            forall|i: int| 0 <= i < history.len() ==>
315                #[trigger] history@[i] <= _max_delta,
316        ensures average as int == Self::sum_seq(history@) / history.len() as int,
317    {
318        let mut total: u64 = 0;
319        let mut index: usize = 0;
320        while index < history.len()
321            invariant
322                index <= history.len(),
323                total as int == Self::sum_seq(history@.take(index as int)),
324                total as int <= index as int * _max_delta as int,
325                index as int * _max_delta as int <= u64::MAX as int,
326                history.len() as int * _max_delta as int <= u64::MAX as int,
327                forall|i: int| 0 <= i < history.len() ==>
328                    #[trigger] history@[i] <= _max_delta,
329            decreases history.len() - index,
330        {
331            proof {
332                Self::lemma_sum_push(history@.take(index as int), history@[index as int]);
333                assert(history@.take(index as int + 1)
334                    =~= history@.take(index as int).push(history@[index as int]));
335                assert(total as int + history@[index as int] as int
336                    <= (index as int + 1) * _max_delta as int) by (nonlinear_arith)
337                    requires
338                        total as int <= index as int * _max_delta as int,
339                        history@[index as int] <= _max_delta;
340                assert((index as int + 1) * _max_delta as int
341                    <= history.len() as int * _max_delta as int) by (nonlinear_arith)
342                    requires
343                        index + 1 <= history.len(),
344                        _max_delta >= 0;
345            }
346            total = total + history[index];
347            index = index + 1;
348        }
349        assert(history@.take(history.len() as int) =~= history@);
350        assert(total as int == Self::sum_seq(history@));
351        let denominator = history.len() as u64;
352        assert(denominator > 0);
353        let average = total / denominator;
354        assert(average as int == total as int / denominator as int);
355        assert(denominator as int == history.len() as int);
356        assert(average as int == Self::sum_seq(history@) / history.len() as int);
357        average
358    }
359}
360
361}
automation_structures/primitives/convergence_governor_phase_aware.rs

automation_structures/primitives/
convergence_governor_phase_aware.rs
