Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103#![allow(unused_imports)]use verus_builtin::*;use verus_builtin_macros::*;use vstd::{modes::*, prelude::*, seq::*, *};
verus! {
enum List<A> { Nil, Cons(A, Box<List<A>>),}
spec fn len<A>(list: &List<A>) -> nat decreases list,{ match list { List::Nil => 0, List::Cons(_, tl) => 1 + len(tl), }}
fn get_len<A>(list: &List<A>) -> (r: u64) requires len(list) <= 0xffffffffffffffff, ensures r == len(list),{ let mut n: u64 = 0; let mut iter = list; loop invariant len(list) <= 0xffffffffffffffff, n + len(iter) == len(list), ensures n == len(list), decreases len(iter), { match iter { List::Nil => { break; }, List::Cons(_, tl) => { iter = tl; proof { reveal_with_fuel(len, 2); } n = n + 1; }, } } n}
fn mk_range(start: u32, length: u32) -> (r: List<u32>) requires start + length <= 0xffff_ffff, ensures len::<u32>(&r) == length, decreases length,{ if length == 0 { List::Nil } else { List::Cons(start, Box::new(mk_range(start + 1, length - 1))) }}
fn main() { let x = List::Cons(100u64, Box::new(List::Nil)); let i = match x { List::Nil => 1, List::Cons(n, _) if n < 10 => n + 2, List::Cons(n, _) if n < 100 => n + 3, List::Cons(n, _) if n < 200 => n + 4, List::Cons(n, _) => n + 5, }; assert(i == 104); let mut j: u64 = 0; match x { List::Nil => { j = 1; }, List::Cons(n, _) => { j = n; }, } assert(j == 100); let k: u32 = match List::Cons(100u64, Box::new(List::Nil)) { List::Nil => { j = 11; 6 }, List::Cons(n, _) => { j = n + 1; 7 }, }; assert(j == 101); assert(k == 7);}
} // verus!