Examples

fn sum(n: {i32 | v > 0}) -> {v: i32 | v >= n} {
  let mut i = 0;
  while (i <= n) {
    i += n;
  }
  n
}

// MIR
fn sum(n: {i32 | v > 0}) -> {v: i32 | v >= n} {
    let mut _0: i32;
    let mut _2: i32;
    let mut _3: bool;
    let mut _4: i32;
    let mut _5: i32;
    let mut _6: i32;
    let mut _7: (i32, bool);

    bb0: {
        _2 = const 0i32;
        goto -> bb1;
    }

    bb1: {
        _4 = _2;
        _5 = _1;
        _3 = Le(move _4, move _5);
        switchInt(_3) -> [false: bb2, otherwise: bb3];
    }

    bb2: {
        _0 = _1;
        return;
    }

    bb3: {
        _6 = _1;
        _7 = CheckedAdd(_2, move _6);
        assert(!move (_7.1: bool), "attempt to add with overflow") -> bb4;
    }

    bb4: {
        _2 = move (_7.0: i32);
        goto -> bb1;
    }
}

// CPS
fn sum(n: {i32 | v > 0}) -> {v: i32 | v >= n} {
  let i0 = 0 in
  letcont k(i) = i
}

/**@ type Range = {v: (i32, i32) | v.0 <= v.1} @*/

/**@ 
(lhs: Range, r: {Range | lhs.1 >= rhs.0 && lhs.1 >= rhs.0}) -> Range 
@*/
fn union(lhs: (i32, i32), rhs: (i32, i32)) -> (i32, i32) {
  (min(lhs.0, rhs.0), max(lhs.1, rhs.1))
}

/**@
forall a, b. 
(r: &(i32, i32), d: i32) -> ()
requires: [*r -> ({v: i32 | v == a}, {v: i32 | v == b})]
ensures: [*r -> ({v: i32 | v == a + d}, {v: i32 | v == b + d})]
@*/
fn move(r: &mut (i32, i32), d: i32) {
  r.0 += d;
  r.1 += d;
}

fn () {
  let r1 = (0, 5);
  let r2 = (10, 15);
  move(&mut r, 5);
  union(r1, r2);
}

// Vectors

/**@
(vec: &Vec<i32>, inc: i32) -> ()
requires: [*vec -> Vec<{forall a. v: i32 | v == a}>]
ensures: [*vec -> Vec<{forall a. v: i32 | v == a + inc}>]
@*/
fn inc(v: &mut Vec<i32>, inc: i32) {
    for n in &mut v {
        *n += b;
    }
}

// Structs and interior mutability

struct InteriorMut {
    val: RefCell<i32>,
}

impl InteriorMut {
    /**@
    forall a.
    (self: &InteriorMut, inc: i32) -> ()
    requires: [*self.val -> RefCell<{v: i32 | v == a}>]
    ensures: [*self.val -> RefCell<{v: i32 | v == a + inc}>]
    @*/
    fn inc(&self, inc: i32) {
        *self.val.borrow_mut() += inc;
    }
}