tla-rs 0.1.0

Rust implementation of the IronFleet verified distributed systems framework
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

use vstd::prelude::*;

verus! {

/// Equivalent to `choose |i:int| low <= i < high && p(i)` except it guarantees to pick the smallest
/// such value `i` where `p(i)` is true.
pub proof fn choose_smallest(low: int, high: int, p: spec_fn(int)->bool) -> (res:int)
  requires
    exists |i:int| #![trigger(p(i))] low <= i < high && p(i),
  ensures
    low <= res < high,
    p(res),
    forall |i:int| #![trigger(p(i))] low <= i < res ==> !p(i),
  decreases
    high - low,
{
  if p(low) {
    low
  } else {
    choose_smallest(low + 1, high, p)
  }
}

} // verus!