automation_structures/modalities/
step_graph.rs

1//! Finite-index StepGraph execution carrier.
2
3use crate::execution_api::StepState as StepGraphNodeState;
4use vstd::prelude::*;
5
6verus! {
7
8/// Monotone rank of the shared StepGraph node-state vocabulary.
9pub open spec fn state_rank(state: StepGraphNodeState) -> int {
10    match state {
11        StepGraphNodeState::NotReady => 0,
12        StepGraphNodeState::Ready => 1,
13        StepGraphNodeState::Running => 2,
14        StepGraphNodeState::Complete => 3,
15    }
16}
17
18/// Every node state is retained or advances monotonically.
19pub open spec fn states_monotone(
20    before: Seq<StepGraphNodeState>,
21    after: Seq<StepGraphNodeState>,
22) -> bool {
23    &&& after.len() == before.len()
24    &&& forall|i: int| 0 <= i < before.len() ==>
25        state_rank(after[i]) >= state_rank(before[i])
26}
27
28/// Blocked-node release action over any faithful state carrier.
29pub open spec fn become_ready_action(
30    before: Seq<StepGraphNodeState>,
31    after: Seq<StepGraphNodeState>,
32    node: int,
33    eligible: bool,
34    accepted: bool,
35) -> bool {
36    let enabled = 0 <= node < before.len()
37        && before[node] == StepGraphNodeState::NotReady
38        && eligible;
39    &&& accepted == enabled
40    &&& after == if accepted {
41        before.update(node, StepGraphNodeState::Ready)
42    } else {
43        before
44    }
45}
46
47/// Ready-node start action over any faithful state carrier.
48pub open spec fn start_running_action(
49    before: Seq<StepGraphNodeState>,
50    after: Seq<StepGraphNodeState>,
51    node: int,
52    selected: bool,
53    accepted: bool,
54) -> bool {
55    let enabled = 0 <= node < before.len()
56        && selected
57        && before[node] == StepGraphNodeState::Ready;
58    &&& accepted == enabled
59    &&& after == if accepted {
60        before.update(node, StepGraphNodeState::Running)
61    } else {
62        before
63    }
64}
65
66/// Running-node completion action over any faithful state carrier.
67pub open spec fn complete_node_action(
68    before: Seq<StepGraphNodeState>,
69    after: Seq<StepGraphNodeState>,
70    node: int,
71    selected: bool,
72    accepted: bool,
73) -> bool {
74    let enabled = 0 <= node < before.len()
75        && selected
76        && before[node] == StepGraphNodeState::Running;
77    &&& accepted == enabled
78    &&& after == if accepted {
79        before.update(node, StepGraphNodeState::Complete)
80    } else {
81        before
82    }
83}
84
85/// Predecessor-governed step-graph owner.
86pub struct StepGraph {
87    /// Number of execution nodes.
88    pub num_nodes: usize,
89    /// Directed predecessor edges.
90    pub edges: Vec<(usize, usize)>,
91    /// Lifecycle state by node index.
92    pub nstate: Vec<StepGraphNodeState>,
93}
94
95impl StepGraph {
96    /// Whether every dependency edge names two valid nodes.
97    pub open spec fn edges_valid(edges: Seq<(usize, usize)>, num_nodes: usize) -> bool {
98        forall|i: int| 0 <= i < edges.len() ==>
99            #[trigger] edges[i].0 < num_nodes && edges[i].1 < num_nodes
100    }
101
102    /// Whether the dependency edge sequence contains no duplicate edge.
103    pub open spec fn edges_distinct(edges: Seq<(usize, usize)>) -> bool {
104        forall|i: int, j: int|
105            0 <= i < edges.len() && 0 <= j < edges.len() && i != j
106                ==> #[trigger] edges[i] != #[trigger] edges[j]
107    }
108
109    /// Whether `node` has at least one incoming dependency edge.
110    pub open spec fn has_predecessor_in(edges: Seq<(usize, usize)>, node: usize) -> bool {
111        exists|i: int| 0 <= i < edges.len() && edges[i].1 == node
112    }
113
114    /// Whether every predecessor of `node` is complete in `states`.
115    pub open spec fn predecessors_complete_in(
116        edges: Seq<(usize, usize)>, states: Seq<StepGraphNodeState>, node: usize,
117    ) -> bool {
118        forall|i: int| 0 <= i < edges.len() && edges[i].1 == node
119            ==> #[trigger] states[edges[i].0 as int] == StepGraphNodeState::Complete
120    }
121
122    /// Whether node states and dependency edges have valid shape and values.
123    pub open spec fn type_invariant(&self) -> bool {
124        &&& self.nstate@.len() == self.num_nodes
125        &&& Self::edges_valid(self.edges@, self.num_nodes)
126        &&& Self::edges_distinct(self.edges@)
127    }
128
129    /// Whether readiness agrees with predecessor completion.
130    pub open spec fn eligibility_closed(&self) -> bool {
131        forall|n: usize| n < self.num_nodes
132            && #[trigger] self.nstate@[n as int] != StepGraphNodeState::NotReady
133            ==> Self::predecessors_complete_in(self.edges@, self.nstate@, n)
134    }
135
136    /// Derived consequence of `eligibility_closed`: no node runs or completes before all
137    /// predecessors complete.
138    pub open spec fn no_run_before_predecessors(&self) -> bool {
139        forall|n: usize| n < self.num_nodes
140            && (#[trigger] self.nstate@[n as int] == StepGraphNodeState::Running
141                || self.nstate@[n as int] == StepGraphNodeState::Complete)
142            ==> Self::predecessors_complete_in(self.edges@, self.nstate@, n)
143    }
144
145    /// Whether all dependency-ordered execution contract clauses hold.
146    pub open spec fn inv(&self) -> bool {
147        self.type_invariant() && self.eligibility_closed()
148    }
149
150    #[expect(clippy::ptr_arg, reason = "Verus sequence-view contracts are stated over Vec for StepGraph edges")]
151    #[expect(clippy::indexing_slicing, reason = "Verus proves the predecessor cursor remains in bounds")]
152    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the predecessor cursor increment remains in bounds")]
153    fn has_predecessor_exec(edges: &Vec<(usize, usize)>, node: usize) -> (b: bool)
154        ensures b == Self::has_predecessor_in(edges@, node),
155    {
156        let mut i = 0;
157        while i < edges.len()
158            invariant
159                i <= edges.len(),
160                forall|k: int| 0 <= k < i ==> edges@[k].1 != node,
161            decreases edges.len() - i,
162        {
163            if edges[i].1 == node {
164                assert(Self::has_predecessor_in(edges@, node));
165                return true;
166            }
167            i += 1;
168        }
169        false
170    }
171
172    #[expect(clippy::indexing_slicing, reason = "the type invariant and loop invariant bound edge and predecessor-state indices")]
173    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the predecessor-completion cursor increment remains in bounds")]
174    fn predecessors_complete_exec(&self, node: usize) -> (b: bool)
175        requires
176            self.type_invariant(),
177            node < self.num_nodes,
178        ensures b == Self::predecessors_complete_in(self.edges@, self.nstate@, node),
179    {
180        let mut i = 0;
181        while i < self.edges.len()
182            invariant
183                i <= self.edges.len(),
184                self.type_invariant(),
185                forall|k: int| 0 <= k < i && self.edges@[k].1 == node
186                    ==> self.nstate@[self.edges@[k].0 as int]
187                        == StepGraphNodeState::Complete,
188            decreases self.edges.len() - i,
189        {
190            if self.edges[i].1 == node
191                && !matches!(
192                    self.nstate[self.edges[i].0],
193                    StepGraphNodeState::Complete
194                )
195            {
196                assert(!Self::predecessors_complete_in(self.edges@, self.nstate@, node));
197                return false;
198            }
199            i += 1;
200        }
201        true
202    }
203
204    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the state-construction cursor remains within the node bound")]
205    /// Construct initial readiness states for a valid edge set.
206    pub fn new(num_nodes: usize, edges: Vec<(usize, usize)>) -> (s: StepGraph)
207        requires
208            Self::edges_valid(edges@, num_nodes),
209            Self::edges_distinct(edges@),
210        ensures
211            s.num_nodes == num_nodes,
212            s.edges@ == edges@,
213            s.nstate@.len() == num_nodes,
214            forall|n: usize| n < num_nodes ==>
215                #[trigger] s.nstate@[n as int]
216                    == if Self::has_predecessor_in(edges@, n) {
217                        StepGraphNodeState::NotReady
218                    } else {
219                        StepGraphNodeState::Ready
220                    },
221            s.inv(),
222            s.no_run_before_predecessors(),
223    {
224        let mut nstate = Vec::new();
225        let mut n = 0;
226        while n < num_nodes
227            invariant
228                n <= num_nodes,
229                nstate@.len() == n,
230                forall|k: usize| k < n ==>
231                    #[trigger] nstate@[k as int]
232                        == if Self::has_predecessor_in(edges@, k) {
233                            StepGraphNodeState::NotReady
234                        } else {
235                            StepGraphNodeState::Ready
236                        },
237            decreases num_nodes - n,
238        {
239            if Self::has_predecessor_exec(&edges, n) {
240                nstate.push(StepGraphNodeState::NotReady);
241            } else {
242                nstate.push(StepGraphNodeState::Ready);
243            }
244            n += 1;
245        }
246        let s = StepGraph { num_nodes, edges, nstate };
247        assert(s.eligibility_closed()) by {
248            assert forall|node: usize| node < s.num_nodes
249                && #[trigger] s.nstate@[node as int] != StepGraphNodeState::NotReady
250                implies Self::predecessors_complete_in(s.edges@, s.nstate@, node) by {
251                assert(!Self::has_predecessor_in(s.edges@, node));
252            }
253        }
254        s
255    }
256
257    #[expect(clippy::indexing_slicing, reason = "the action guard and Verus invariant bound the node-state index")]
258    /// Promote a node after every predecessor completes.
259    pub fn become_ready(&mut self, node: usize) -> (accepted: bool)
260        requires old(self).inv(),
261        ensures
262            final(self).num_nodes == old(self).num_nodes,
263            final(self).edges@ == old(self).edges@,
264            become_ready_action(
265                old(self).nstate@,
266                final(self).nstate@,
267                node as int,
268                Self::has_predecessor_in(old(self).edges@, node)
269                    && Self::predecessors_complete_in(
270                        old(self).edges@,
271                        old(self).nstate@,
272                        node,
273                    ),
274                accepted,
275            ),
276            states_monotone(old(self).nstate@, final(self).nstate@),
277            final(self).inv(),
278            final(self).no_run_before_predecessors(),
279    {
280        if node < self.num_nodes
281            && matches!(self.nstate[node], StepGraphNodeState::NotReady)
282            && Self::has_predecessor_exec(&self.edges, node)
283            && self.predecessors_complete_exec(node)
284        {
285            let ghost old_states = self.nstate@;
286            self.nstate.set(node, StepGraphNodeState::Ready);
287            assert(self.eligibility_closed()) by {
288                assert forall|m: usize| m < self.num_nodes
289                    && #[trigger] self.nstate@[m as int] != StepGraphNodeState::NotReady
290                    implies Self::predecessors_complete_in(self.edges@, self.nstate@, m) by {
291                    if m == node {
292                        assert forall|e: int| 0 <= e < self.edges@.len()
293                            && self.edges@[e].1 == m
294                            implies #[trigger] self.nstate@[self.edges@[e].0 as int]
295                                == StepGraphNodeState::Complete by {
296                            let p = self.edges@[e].0;
297                            assert(old_states[p as int] == StepGraphNodeState::Complete);
298                            assert(p != node);
299                        }
300                    } else {
301                        assert(Self::predecessors_complete_in(self.edges@, old_states, m));
302                        assert forall|e: int| 0 <= e < self.edges@.len()
303                            && self.edges@[e].1 == m
304                            implies #[trigger] self.nstate@[self.edges@[e].0 as int]
305                                == StepGraphNodeState::Complete by {
306                            let p = self.edges@[e].0;
307                            assert(old_states[p as int] == StepGraphNodeState::Complete);
308                            assert(p != node);
309                        }
310                    }
311                }
312            }
313            true
314        } else {
315            false
316        }
317    }
318
319    #[expect(clippy::indexing_slicing, reason = "the action guard and Verus invariant bound the node-state index")]
320    /// Start one ready node.
321    pub fn start_running(&mut self, node: usize) -> (accepted: bool)
322        requires old(self).inv(),
323        ensures
324            final(self).num_nodes == old(self).num_nodes,
325            final(self).edges@ == old(self).edges@,
326            start_running_action(
327                old(self).nstate@,
328                final(self).nstate@,
329                node as int,
330                true,
331                accepted,
332            ),
333            states_monotone(old(self).nstate@, final(self).nstate@),
334            final(self).inv(),
335            final(self).no_run_before_predecessors(),
336    {
337        if node < self.num_nodes && matches!(self.nstate[node], StepGraphNodeState::Ready) {
338            let ghost old_states = self.nstate@;
339            self.nstate.set(node, StepGraphNodeState::Running);
340            assert(self.eligibility_closed()) by {
341                assert forall|m: usize| m < self.num_nodes
342                    && #[trigger] self.nstate@[m as int] != StepGraphNodeState::NotReady
343                    implies Self::predecessors_complete_in(self.edges@, self.nstate@, m) by {
344                    assert(Self::predecessors_complete_in(self.edges@, old_states, m));
345                    assert forall|e: int| 0 <= e < self.edges@.len()
346                        && self.edges@[e].1 == m
347                        implies #[trigger] self.nstate@[self.edges@[e].0 as int]
348                            == StepGraphNodeState::Complete by {
349                        let p = self.edges@[e].0;
350                        assert(old_states[p as int] == StepGraphNodeState::Complete);
351                        assert(p != node);
352                    }
353                }
354            }
355            true
356        } else {
357            false
358        }
359    }
360
361    #[expect(clippy::indexing_slicing, reason = "the action guard and Verus invariant bound the node-state index")]
362    /// Complete one running node.
363    pub fn complete_node(&mut self, node: usize) -> (accepted: bool)
364        requires old(self).inv(),
365        ensures
366            final(self).num_nodes == old(self).num_nodes,
367            final(self).edges@ == old(self).edges@,
368            complete_node_action(
369                old(self).nstate@,
370                final(self).nstate@,
371                node as int,
372                true,
373                accepted,
374            ),
375            states_monotone(old(self).nstate@, final(self).nstate@),
376            final(self).inv(),
377            final(self).no_run_before_predecessors(),
378    {
379        if node < self.num_nodes && matches!(self.nstate[node], StepGraphNodeState::Running) {
380            let ghost old_states = self.nstate@;
381            self.nstate.set(node, StepGraphNodeState::Complete);
382            assert(self.eligibility_closed()) by {
383                assert forall|m: usize| m < self.num_nodes
384                    && #[trigger] self.nstate@[m as int] != StepGraphNodeState::NotReady
385                    implies Self::predecessors_complete_in(self.edges@, self.nstate@, m) by {
386                    assert(Self::predecessors_complete_in(self.edges@, old_states, m));
387                    assert forall|e: int| 0 <= e < self.edges@.len()
388                        && self.edges@[e].1 == m
389                        implies #[trigger] self.nstate@[self.edges@[e].0 as int]
390                            == StepGraphNodeState::Complete by {
391                        let p = self.edges@[e].0;
392                        if p != node {
393                            assert(self.nstate@[p as int] == old_states[p as int]);
394                        }
395                    }
396                }
397            }
398            true
399        } else {
400            false
401        }
402    }
403
404    #[expect(clippy::indexing_slicing, reason = "Verus proves the completion cursor remains in bounds")]
405    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the completion cursor increment remains in bounds")]
406    /// Execute the terminal stutter when every node is complete.
407    pub fn done_stuttering(&mut self) -> (enabled: bool)
408        requires old(self).inv(),
409        ensures
410            enabled == (forall|i: int| 0 <= i < old(self).nstate@.len()
411                ==> #[trigger] old(self).nstate@[i] == StepGraphNodeState::Complete),
412            final(self).num_nodes == old(self).num_nodes,
413            final(self).edges@ == old(self).edges@,
414            final(self).nstate@ == old(self).nstate@,
415            final(self).inv(),
416    {
417        let mut i = 0;
418        while i < self.nstate.len()
419            invariant
420                i <= self.nstate.len(),
421                self.inv(),
422                forall|k: int| 0 <= k < i ==>
423                    self.nstate@[k] == StepGraphNodeState::Complete,
424            decreases self.nstate.len() - i,
425        {
426            if !matches!(self.nstate[i], StepGraphNodeState::Complete) {
427                return false;
428            }
429            i += 1;
430        }
431        true
432    }
433}
434
435}
automation_structures/modalities/step_graph.rs

automation_structures/modalities/
step_graph.rs
