Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300#![allow(unused_imports)]use vstd::{map::*, prelude::*, seq::*, set::*};
verus! {
// ANCHOR: macroproof fn test_seq1() { let s: Seq<int> = seq![0, 10, 20, 30, 40]; assert(s.len() == 5); assert(s[2] == 20); assert(s[3] == 30); assert(s[2..4] == seq![20, 30]); assert(s[2..] == seq![20, 30, 40]); assert(s[..4] == seq![0, 10, 20, 30]);}
proof fn test_set1() { let s: Set<int> = set![0, 10, 20, 30, 40]; assert(s.contains(20)); assert(s.contains(30)); assert(!s.contains(60));
let s: ISet<int> = iset![0, 10, 20, 30, 40]; assert(s.finite()); assert(s.contains(20)); assert(s.contains(30)); assert(!s.contains(60));}
proof fn test_map1() { let m: Map<int, int> = map![0 => 0, 10 => 100, 20 => 200, 30 => 300, 40 => 400]; assert(m.dom().contains(20)); assert(m.dom().contains(30)); assert(!m.dom().contains(60)); assert(m[20] == 200); assert(m[30] == 300);}
// ANCHOR_END: macro#[verusfmt::skip]mod m0 {use vstd::{seq::*, prelude::*};
// ANCHOR: new0proof fn test_seq2() { let s: Seq<int> = Seq::new(5, |i: int| 10 * i); assert(s.len() == 5); assert(s[2] == 20); assert(s[3] == 30); assert(s[2..4] == seq![20, 30]); assert(s[2..] == seq![20, 30, 40]); assert(s[..4] == seq![0, 10, 20, 30]);}// ANCHOR_END: new0}
// ANCHOR: newproof fn test_seq2() { let s: Seq<int> = Seq::new(5, |i: int| 10 * i); assert(s.len() == 5); assert(s[2] == 20); assert(s[3] == 30);}
proof fn test_set2() { let s_finite: Set<int> = Set::range(0, 41).filter(|i: int| i % 10 == 0); assert(s_finite.contains(20)); assert(s_finite.contains(30)); assert(!s_finite.contains(60));
let s: ISet<int> = ISet::new(|i: int| 0 <= i <= 40 && i % 10 == 0); assert(s.contains(20)); assert(s.contains(30)); assert(!s.contains(60));
let s_infinite: ISet<int> = ISet::new(|i: int| i % 10 == 0); assert(s_infinite.contains(20)); assert(s_infinite.contains(30)); assert(!s_infinite.contains(35));}
proof fn test_map2() { let m: IMap<int, int> = IMap::new(|i: int| 0 <= i <= 40 && i % 10 == 0, |i: int| 10 * i); assert(m[20] == 200); assert(m[30] == 300);
let m_infinite: IMap<int, int> = IMap::new(|i: int| i % 10 == 0, |i: int| 10 * i); assert(m_infinite[20] == 200); assert(m_infinite[30] == 300); assert(m_infinite[90] == 900);
let m_finite: Map<int, int> = Map::new(Set::range(0, 41), |i: int| 10 * i); assert(m_finite[20] == 200); assert(m_finite[30] == 300);}// ANCHOR_END: new
/*// ANCHOR: test_eq_failproof fn check_eq(x: Seq<int>, y: Seq<int>) requires x == y,{}
proof fn test_eq_fail() { let s1: Seq<int> = seq![0, 10, 20, 30, 40]; let s2: Seq<int> = seq![0, 10] + seq![20] + seq![30, 40]; let s3: Seq<int> = Seq::new(5, |i: int| 10 * i); check_eq(s1, s2); // FAILS, even though s1 equals s2 check_eq(s1, s3); // FAILS, even though s1 equals s3}// ANCHOR_END: test_eq_fail*/
// ANCHOR: test_eqproof fn check_eq_extensionally(x: Seq<int>, y: Seq<int>) requires x =~= y,{}
proof fn test_eq() { let s1: Seq<int> = seq![0, 10, 20, 30, 40]; let s2: Seq<int> = seq![0, 10] + seq![20] + seq![30, 40]; let s3: Seq<int> = Seq::new(5, |i: int| 10 * i); check_eq_extensionally(s1, s2); // succeeds check_eq_extensionally(s1, s3); // succeeds}// ANCHOR_END: test_eq
// ANCHOR: test_eq2proof fn check_eq(x: Seq<int>, y: Seq<int>) requires x == y,{}
proof fn test_eq2() { let s1: Seq<int> = seq![0, 10, 20, 30, 40]; let s2: Seq<int> = seq![0, 10] + seq![20] + seq![30, 40]; let s3: Seq<int> = Seq::new(5, |i: int| 10 * i); assert(s1 =~= s2); assert(s1 =~= s3); check_eq(s1, s2); // succeeds check_eq(s1, s3); // succeeds}// ANCHOR_END: test_eq2
/*// ANCHOR: lemma_len_intersect_failpub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>) ensures s1.intersect(s2).len() <= s1.len(), decreases s1.len(),{ if s1.is_empty() {
} else { let a = s1.choose();
lemma_len_intersect(s1.remove(a), s2); }}// ANCHOR_END: lemma_len_intersect_fail
// ANCHOR: lemma_len_intersect_sketchpub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>) ensures s1.intersect(s2).len() <= s1.len(), decreases s1.len(),{ if s1.is_empty() { // s1 is the empty set. // Therefore, s1.intersect(s2) is also empty. // So both s1.len() and s1.intersect(s2).len() are 0, // and 0 <= 0. } else { // s1 is not empty, so it has at least one element. // Let a be an element from s1. // Let s1' be the set s1 with the element a removed (i.e. s1' == s1 - {a}). // Removing an element decreases the cardinality by 1, so s1'.len() == s1.len() - 1. // By induction, s1'.intersect(s2).len() <= s1'.len(), so: // (s1 - {a}).intersect(s2).len() <= s1'.len() // (s1.intersect(s2) - {a}).len() <= s1'.len() // (s1.intersect(s2) - {a}).len() <= s1.len() - 1 // case a in s1.intersect(s2): // (s1.intersect(s2) - {a}).len() == s1.intersect(s2).len() - 1 // case a not in s1.intersect(s2): // (s1.intersect(s2) - {a}).len() == s1.intersect(s2).len() // In either case: // s1.intersect(s2).len() <= (s1.intersect(s2) - {a}).len() + 1 // Putting all the inequalities together: // s1.intersect(s2).len() <= (s1.intersect(s2) - {a}).len() + 1 <= (s1.len() - 1) + 1 // So: // s1.intersect(s2).len() <= (s1.len() - 1) + 1 // s1.intersect(s2).len() <= s1.len() }}// ANCHOR_END: lemma_len_intersect_sketch
// ANCHOR: lemma_len_intersectpub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>) ensures s1.intersect(s2).len() <= s1.len(), decreases s1.len(),{ if s1.is_empty() { assert(s1.intersect(s2) =~= s1); } else { let a = s1.choose(); assert(s1.intersect(s2).remove(a) =~= s1.remove(a).intersect(s2)); lemma_len_intersect(s1.remove(a), s2); }}// ANCHOR_END: lemma_len_intersect*/
// ANCHOR: lemma_len_intersect_commentedpub proof fn lemma_len_intersect<A>(s1: Set<A>, s2: Set<A>) ensures s1.intersect(s2).len() <= s1.len(), decreases s1.len(),{ if s1.is_empty() { assert(s1.intersect(s2).len() == 0) by { assert(s1.intersect(s2) =~= s1); } } else { let a = s1.choose(); lemma_len_intersect(s1.remove(a), s2); // by induction: s1.remove(a).intersect(s2).len() <= s1.remove(a).len() assert(s1.intersect(s2).remove(a).len() <= s1.remove(a).len()) by { assert(s1.intersect(s2).remove(a) =~= s1.remove(a).intersect(s2)); } // simplifying ".remove(a).len()" yields s1.intersect(s2).len() <= s1.len())
}}// ANCHOR_END: lemma_len_intersect_commented
// ANCHOR: test_vec1fn test_vec1() { let mut v: Vec<u32> = Vec::new(); v.push(0); v.push(10); v.push(20); v.push(30); v.push(40); assert(v.len() == 5); assert(v[2] == 20); assert(v[3] == 30); v.set(2, 21); assert(v[2] == 21); assert(v[3] == 30);}// ANCHOR_END: test_vec1
// ANCHOR: test_vec2spec fn has_five_sorted_numbers(s: Seq<u32>) -> bool { s.len() == 5 && s[0] <= s[1] <= s[2] <= s[3] <= s[4]}
fn test_vec2() { let mut v: Vec<u32> = Vec::new(); v.push(0); v.push(10); v.push(20); v.push(30); v.push(40); v.set(2, 21); assert(v@ =~= seq![0, 10, 21, 30, 40]); assert(v@ =~= seq![0, 10] + seq![21] + seq![30, 40]); assert(v@[2] == 21); assert(v@[3] == 30); assert(v@[2..4] =~= seq![21, 30]); assert(has_five_sorted_numbers(v@));}// ANCHOR_END: test_vec2
// ANCHOR: ret_spec_fnspec fn adder(x: int) -> spec_fn(int) -> int { |y: int| x + y}
proof fn test_adder() { let f = adder(10); assert(f(20) == 30); assert(f(60) == 70);}// ANCHOR_END: ret_spec_fn
fn main() {}
} // verus!