automation_structures/connectives/
cursor.rs

1//! Executable Cursor connective.
2//!
3//! Cursor retains a position. It carries no delivery, replay, persistence, or exactly-once
4//! obligation. Its owner supplies the admissible bound and movement rule.
5
6use vstd::prelude::*;
7
8verus! {
9
10/// Owner-supplied bound for a retained cursor position.
11pub open spec fn cursor_admitted(position: nat, head: nat) -> bool {
12    position <= head
13}
14
15/// A retained position beyond the admitted head is rejected.
16pub proof fn regression_rejected(position: nat, head: nat)
17    requires position > head,
18    ensures !cursor_admitted(position, head),
19{
20}
21
22/// A retained position with owner-supplied movement obligations.
23pub struct Cursor {
24    /// Retained monotone position.
25    pub position: usize,
26}
27
28impl Cursor {
29    /// Construct a cursor at an admitted position.
30    pub fn new(position: usize) -> (cursor: Self)
31        ensures cursor.position == position,
32    {
33        Self { position }
34    }
35
36    /// Move monotonically to `position`.
37    pub fn advance_to(&mut self, position: usize)
38        requires old(self).position <= position,
39        ensures final(self).position == position,
40    {
41        self.position = position;
42    }
43}
44
45}
automation_structures/connectives/cursor.rs

automation_structures/connectives/
cursor.rs
