automation-structures 0.1.1

Reusable, formally specified building blocks for composing automation systems.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

//! Executable Cursor connective.
//!
//! Cursor retains a position. It carries no delivery, replay, persistence, or exactly-once
//! obligation. Its owner supplies the admissible bound and movement rule.

use vstd::prelude::*;

verus! {

/// Owner-supplied bound for a retained cursor position.
pub open spec fn cursor_admitted(position: nat, head: nat) -> bool {
    position <= head
}

/// A retained position beyond the admitted head is rejected.
pub proof fn regression_rejected(position: nat, head: nat)
    requires position > head,
    ensures !cursor_admitted(position, head),
{
}

/// A retained position with owner-supplied movement obligations.
pub struct Cursor {
    pub position: usize,
}

impl Cursor {
    /// Construct a cursor at an admitted position.
    pub fn new(position: usize) -> (cursor: Self)
        ensures cursor.position == position,
    {
        Self { position }
    }

    /// Move monotonically to `position`.
    pub fn advance_to(&mut self, position: usize)
        requires old(self).position <= position,
        ensures final(self).position == position,
    {
        self.position = position;
    }
}

}