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    /// Whether no node runs or completes before all predecessors complete.
137    pub open spec fn no_run_before_predecessors(&self) -> bool {
138        forall|n: usize| n < self.num_nodes
139            && (#[trigger] self.nstate@[n as int] == StepGraphNodeState::Running
140                || self.nstate@[n as int] == StepGraphNodeState::Complete)
141            ==> Self::predecessors_complete_in(self.edges@, self.nstate@, n)
142    }
143
144    /// Whether all dependency-ordered execution obligations hold.
145    pub open spec fn inv(&self) -> bool {
146        self.type_invariant() && self.eligibility_closed()
147    }
148
149    #[expect(clippy::ptr_arg, reason = "Verus sequence-view contracts are stated over Vec for StepGraph edges")]
150    #[expect(clippy::indexing_slicing, reason = "Verus proves the predecessor cursor remains in bounds")]
151    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the predecessor cursor increment remains in bounds")]
152    fn has_predecessor_exec(edges: &Vec<(usize, usize)>, node: usize) -> (b: bool)
153        ensures b == Self::has_predecessor_in(edges@, node),
154    {
155        let mut i = 0;
156        while i < edges.len()
157            invariant
158                i <= edges.len(),
159                forall|k: int| 0 <= k < i ==> edges@[k].1 != node,
160            decreases edges.len() - i,
161        {
162            if edges[i].1 == node {
163                assert(Self::has_predecessor_in(edges@, node));
164                return true;
165            }
166            i += 1;
167        }
168        false
169    }
170
171    #[expect(clippy::indexing_slicing, reason = "the type invariant and loop invariant bound edge and predecessor-state indices")]
172    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the predecessor-completion cursor increment remains in bounds")]
173    fn predecessors_complete_exec(&self, node: usize) -> (b: bool)
174        requires
175            self.type_invariant(),
176            node < self.num_nodes,
177        ensures b == Self::predecessors_complete_in(self.edges@, self.nstate@, node),
178    {
179        let mut i = 0;
180        while i < self.edges.len()
181            invariant
182                i <= self.edges.len(),
183                self.type_invariant(),
184                forall|k: int| 0 <= k < i && self.edges@[k].1 == node
185                    ==> self.nstate@[self.edges@[k].0 as int]
186                        == StepGraphNodeState::Complete,
187            decreases self.edges.len() - i,
188        {
189            if self.edges[i].1 == node
190                && !matches!(
191                    self.nstate[self.edges[i].0],
192                    StepGraphNodeState::Complete
193                )
194            {
195                assert(!Self::predecessors_complete_in(self.edges@, self.nstate@, node));
196                return false;
197            }
198            i += 1;
199        }
200        true
201    }
202
203    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the state-construction cursor remains within the node bound")]
204    /// Construct initial readiness states for a valid edge set.
205    pub fn new(num_nodes: usize, edges: Vec<(usize, usize)>) -> (s: StepGraph)
206        requires
207            Self::edges_valid(edges@, num_nodes),
208            Self::edges_distinct(edges@),
209        ensures
210            s.num_nodes == num_nodes,
211            s.edges@ == edges@,
212            s.nstate@.len() == num_nodes,
213            forall|n: usize| n < num_nodes ==>
214                #[trigger] s.nstate@[n as int]
215                    == if Self::has_predecessor_in(edges@, n) {
216                        StepGraphNodeState::NotReady
217                    } else {
218                        StepGraphNodeState::Ready
219                    },
220            s.inv(),
221            s.no_run_before_predecessors(),
222    {
223        let mut nstate = Vec::new();
224        let mut n = 0;
225        while n < num_nodes
226            invariant
227                n <= num_nodes,
228                nstate@.len() == n,
229                forall|k: usize| k < n ==>
230                    #[trigger] nstate@[k as int]
231                        == if Self::has_predecessor_in(edges@, k) {
232                            StepGraphNodeState::NotReady
233                        } else {
234                            StepGraphNodeState::Ready
235                        },
236            decreases num_nodes - n,
237        {
238            if Self::has_predecessor_exec(&edges, n) {
239                nstate.push(StepGraphNodeState::NotReady);
240            } else {
241                nstate.push(StepGraphNodeState::Ready);
242            }
243            n += 1;
244        }
245        let s = StepGraph { num_nodes, edges, nstate };
246        assert(s.eligibility_closed()) by {
247            assert forall|node: usize| node < s.num_nodes
248                && #[trigger] s.nstate@[node as int] != StepGraphNodeState::NotReady
249                implies Self::predecessors_complete_in(s.edges@, s.nstate@, node) by {
250                assert(!Self::has_predecessor_in(s.edges@, node));
251            }
252        }
253        s
254    }
255
256    #[expect(clippy::indexing_slicing, reason = "the action guard and Verus invariant bound the node-state index")]
257    /// Promote a node after every predecessor completes.
258    pub fn become_ready(&mut self, node: usize) -> (accepted: bool)
259        requires old(self).inv(),
260        ensures
261            final(self).num_nodes == old(self).num_nodes,
262            final(self).edges@ == old(self).edges@,
263            become_ready_action(
264                old(self).nstate@,
265                final(self).nstate@,
266                node as int,
267                Self::has_predecessor_in(old(self).edges@, node)
268                    && Self::predecessors_complete_in(
269                        old(self).edges@,
270                        old(self).nstate@,
271                        node,
272                    ),
273                accepted,
274            ),
275            states_monotone(old(self).nstate@, final(self).nstate@),
276            final(self).inv(),
277            final(self).no_run_before_predecessors(),
278    {
279        if node < self.num_nodes
280            && matches!(self.nstate[node], StepGraphNodeState::NotReady)
281            && Self::has_predecessor_exec(&self.edges, node)
282            && self.predecessors_complete_exec(node)
283        {
284            let ghost old_states = self.nstate@;
285            self.nstate.set(node, StepGraphNodeState::Ready);
286            assert(self.eligibility_closed()) by {
287                assert forall|m: usize| m < self.num_nodes
288                    && #[trigger] self.nstate@[m as int] != StepGraphNodeState::NotReady
289                    implies Self::predecessors_complete_in(self.edges@, self.nstate@, m) by {
290                    if m == node {
291                        assert forall|e: int| 0 <= e < self.edges@.len()
292                            && self.edges@[e].1 == m
293                            implies #[trigger] self.nstate@[self.edges@[e].0 as int]
294                                == StepGraphNodeState::Complete by {
295                            let p = self.edges@[e].0;
296                            assert(old_states[p as int] == StepGraphNodeState::Complete);
297                            assert(p != node);
298                        }
299                    } else {
300                        assert(Self::predecessors_complete_in(self.edges@, old_states, m));
301                        assert forall|e: int| 0 <= e < self.edges@.len()
302                            && self.edges@[e].1 == m
303                            implies #[trigger] self.nstate@[self.edges@[e].0 as int]
304                                == StepGraphNodeState::Complete by {
305                            let p = self.edges@[e].0;
306                            assert(old_states[p as int] == StepGraphNodeState::Complete);
307                            assert(p != node);
308                        }
309                    }
310                }
311            }
312            true
313        } else {
314            false
315        }
316    }
317
318    #[expect(clippy::indexing_slicing, reason = "the action guard and Verus invariant bound the node-state index")]
319    /// Start one ready node.
320    pub fn start_running(&mut self, node: usize) -> (accepted: bool)
321        requires old(self).inv(),
322        ensures
323            final(self).num_nodes == old(self).num_nodes,
324            final(self).edges@ == old(self).edges@,
325            start_running_action(
326                old(self).nstate@,
327                final(self).nstate@,
328                node as int,
329                true,
330                accepted,
331            ),
332            states_monotone(old(self).nstate@, final(self).nstate@),
333            final(self).inv(),
334            final(self).no_run_before_predecessors(),
335    {
336        if node < self.num_nodes && matches!(self.nstate[node], StepGraphNodeState::Ready) {
337            let ghost old_states = self.nstate@;
338            self.nstate.set(node, StepGraphNodeState::Running);
339            assert(self.eligibility_closed()) by {
340                assert forall|m: usize| m < self.num_nodes
341                    && #[trigger] self.nstate@[m as int] != StepGraphNodeState::NotReady
342                    implies Self::predecessors_complete_in(self.edges@, self.nstate@, m) by {
343                    assert(Self::predecessors_complete_in(self.edges@, old_states, m));
344                    assert forall|e: int| 0 <= e < self.edges@.len()
345                        && self.edges@[e].1 == m
346                        implies #[trigger] self.nstate@[self.edges@[e].0 as int]
347                            == StepGraphNodeState::Complete by {
348                        let p = self.edges@[e].0;
349                        assert(old_states[p as int] == StepGraphNodeState::Complete);
350                        assert(p != node);
351                    }
352                }
353            }
354            true
355        } else {
356            false
357        }
358    }
359
360    #[expect(clippy::indexing_slicing, reason = "the action guard and Verus invariant bound the node-state index")]
361    /// Complete one running node.
362    pub fn complete_node(&mut self, node: usize) -> (accepted: bool)
363        requires old(self).inv(),
364        ensures
365            final(self).num_nodes == old(self).num_nodes,
366            final(self).edges@ == old(self).edges@,
367            complete_node_action(
368                old(self).nstate@,
369                final(self).nstate@,
370                node as int,
371                true,
372                accepted,
373            ),
374            states_monotone(old(self).nstate@, final(self).nstate@),
375            final(self).inv(),
376            final(self).no_run_before_predecessors(),
377    {
378        if node < self.num_nodes && matches!(self.nstate[node], StepGraphNodeState::Running) {
379            let ghost old_states = self.nstate@;
380            self.nstate.set(node, StepGraphNodeState::Complete);
381            assert(self.eligibility_closed()) by {
382                assert forall|m: usize| m < self.num_nodes
383                    && #[trigger] self.nstate@[m as int] != StepGraphNodeState::NotReady
384                    implies Self::predecessors_complete_in(self.edges@, self.nstate@, m) by {
385                    assert(Self::predecessors_complete_in(self.edges@, old_states, m));
386                    assert forall|e: int| 0 <= e < self.edges@.len()
387                        && self.edges@[e].1 == m
388                        implies #[trigger] self.nstate@[self.edges@[e].0 as int]
389                            == StepGraphNodeState::Complete by {
390                        let p = self.edges@[e].0;
391                        if p != node {
392                            assert(self.nstate@[p as int] == old_states[p as int]);
393                        }
394                    }
395                }
396            }
397            true
398        } else {
399            false
400        }
401    }
402
403    #[expect(clippy::indexing_slicing, reason = "Verus proves the completion cursor remains in bounds")]
404    #[expect(clippy::arithmetic_side_effects, reason = "Verus proves the completion cursor increment remains in bounds")]
405    /// Execute the terminal stutter when every node is complete.
406    pub fn done_stuttering(&mut self) -> (enabled: bool)
407        requires old(self).inv(),
408        ensures
409            enabled == (forall|i: int| 0 <= i < old(self).nstate@.len()
410                ==> #[trigger] old(self).nstate@[i] == StepGraphNodeState::Complete),
411            final(self).num_nodes == old(self).num_nodes,
412            final(self).edges@ == old(self).edges@,
413            final(self).nstate@ == old(self).nstate@,
414            final(self).inv(),
415    {
416        let mut i = 0;
417        while i < self.nstate.len()
418            invariant
419                i <= self.nstate.len(),
420                self.inv(),
421                forall|k: int| 0 <= k < i ==>
422                    self.nstate@[k] == StepGraphNodeState::Complete,
423            decreases self.nstate.len() - i,
424        {
425            if !matches!(self.nstate[i], StepGraphNodeState::Complete) {
426                return false;
427            }
428            i += 1;
429        }
430        true
431    }
432}
433
434}
automation_structures/modalities/step_graph.rs

automation_structures/modalities/
step_graph.rs
