bneb-dev

  fn bubble_sort(arr: Ptr<i32>, n: i64)
      requires n > 0
      ensures forall i in 0..(n-1) => arr[i] <= arr[i+1]
  {
      for i in 0..n {
          invariant forall k in 0..(i-1) => arr[k] <= arr[k+1];
          // bubble pass
      }
  }

  let mut i = 0;
  while i < 5 {
    arr[i] = val;
    i += 1;
  }