Misc Verus Examples

Misc Verus Examples.md

Miscellaneous Verus Examples

rust_ownership.rs

mod ownership {
#[cfg(any())]
fn f1(v: Vec<u64>) -> (Vec<u64>, Vec<u64>) {

  let v1 = v;

  let v2 = v;

  (v1, v2)
}

fn f2(v: Vec<u64>)  {
  let v1: &Vec<u64> = &v;

  let v2: &Vec<u64> = &v;

  assert!(v1 == v2);
}

fn g(p: &mut Vec<u64>, q: &Vec<u64>) { todo!() }

fn h(mut v: Vec<u64>) {
  g(&mut v, &v);
}
}

swap_odd.rs

// vim: set filetype=verus laststatus=0:
use vstd::prelude::*; verus! {

spec fn is_odd(n: int) -> bool {
  n % 2 == 1
}

fn swap_odd(a: &mut u64, b: &u64)
  requires
    (*old(a) as int + *b as int) < u64::MAX,
    is_odd(*b as int),
  ensures is_odd(*a as int) == !is_odd(*old(a) as int),
{
  *a = *a + *b;
}

fn main() {
  let mut v = 0;
  let w = 3;
  swap_odd(&mut v, &w);
  assert(is_odd(v as int) && is_odd(w as int));
}

} // verus!

vrange.rs

// vim: set filetype=verus laststatus=0:
use vstd::prelude::*;

verus! {

// [a, b)

fn min_in_range(v: Vec<u64>, a: usize, b: usize)
  -> (n: u64)
  requires
    0 <= a < b <= v.len(),
  ensures
    exists|i: int| a <= i < b && v[i] == n,
    forall|i: int| a <= i < b ==> v[i] >= n,
{
  let mut min = v[a];
  let ghost mut idx: int = a as int;

  for j in a+1..b
    invariant
      b <= v.len(),
      a <= idx < j,
      v[idx] == min,
      forall|i: int| a <= i < j ==> v[i] >= min,
  {
    if v[j] < min {
      min = v[j];
      proof {
        idx = j as int;
      }
    }
  }
  min
}

}