Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190#![cfg_attr(verus_keep_ghost, verifier::exec_allows_no_decreases_clause)]fn main() {}
// ## 11 -- 10-program.rs
#[allow(unused_imports)]use {verus_builtin::*, verus_builtin_macros::*, prelude::*, seq::*, vstd::*};
verus! {
// ## A -- A-program.rsfn max(a: u64, b: u64) -> (ret: u64) ensures ret == a || ret == b, ret >= a && ret >= b,{ if a >= b { a } else { b }}
fn max_test2() { let x = 3; let y = 4; let ret = max(x, y); assert(ret == 4);}
// ## B -- B-program.rsfn main_1() { let x = 3; let y = 4; assert(x != y);}
// ## B -- B-program.rs.smt sat// ## C -- C-prime.rsspec fn divides(factor: nat, candidate: nat) -> bool { candidate % factor == 0}
spec fn is_prime(candidate: nat) -> bool { &&& 1 < candidate &&& forall|factor: nat| 1 < factor && factor < candidate ==> !divides(factor, candidate)}
fn test_prime(candidate: u64) -> (result: bool) requires 1 < candidate, ensures result == is_prime(candidate as nat),{ let mut factor: u64 = 2; while factor < candidate invariant 1 < factor <= candidate, forall|smallerfactor: nat| 1 < smallerfactor < factor ==> !divides(smallerfactor, candidate as nat), { if candidate % factor == 0 { assert(divides(factor as nat, candidate as nat)); assert(!is_prime(candidate as nat)); return false; } factor = factor + 1; } true}
fn assertions() { assert(divides(3, 6)); assert(divides(12, 24)); assert(is_prime(2)); assert(is_prime(3)); assert(!divides(4, 5)); assert(is_prime(5));}
// ## D -- D-fibo.rsspec fn fibo(n: nat) -> nat decreases n,{ if n == 0 { 0 } else if n == 1 { 1 } else { fibo((n - 2) as nat) + fibo((n - 1) as nat) }}
proof fn lemma_fibo_is_monotonic(i: nat, j: nat) requires i <= j, ensures fibo(i) <= fibo(j), decreases j - i,{ // ---- if j < 2 { } else if i == j { } else if i == j - 1 { } else { lemma_fibo_is_monotonic(i, (j - 1) as nat); lemma_fibo_is_monotonic(i, (j - 2) as nat); }}
// ## D/2 -- D-fibo.rsspec fn fibo_fits_u64(n: nat) -> bool { fibo(n) <= 0xffff_ffff_ffff_ffff}
exec fn fibo_impl(n: u64) -> (result: u64) requires fibo_fits_u64(n as nat), ensures result == fibo(n as nat),{ // ---- if n == 0 { return 0; } let mut prev: u64 = 0; let mut cur: u64 = 1; let mut i: u64 = 1; while i < n invariant 0 < i <= n, fibo_fits_u64(n as nat), fibo_fits_u64(i as nat), cur == fibo(i as nat), prev == fibo((i - 1) as nat), { i = i + 1; proof { lemma_fibo_is_monotonic(i as nat, n as nat); } let new_cur = cur + prev; prev = cur; cur = new_cur; } cur}
// ## E -- E-reverse.rs -- spec variables/* See vectors.rsfn reverse(v: &mut Vec<u64>) { ensures([ v.len() == old(v).len(), forall(|i: int| 0 <= i && i < old(v).len() >>= v.index(i) == old(v).index(old(v).len() - i - 1)), ]);
let length = v.len(); #[verifier::spec] let v1 = *v; let mut n: usize = 0; while n < length / 2 { invariant([ length == v.len(), forall(|i: int| n <= i && i + n < length >>= v.index(i) == v1.index(i)), forall(|i: int| 0 <= i && i < n >>= v.index(i) == v1.index(length - i - 1)), forall(|i: int| 0 <= i && i < n >>= v1.index(i) == v.index(length - i - 1)), ]);
let x = *v.index(n); let y = *v.index(length - 1 - n); v.set(n, y); v.set(length - 1 - n, x);
n = n + 1; }}*/
// F -- F-linear-proof// cell::RefCell::Cell<X>// G -- G-bitvector.rsfn mod8_bw(x: u32) -> (ret: u32) ensures ret == x % 8,{ assert(x & 7 == x % 8) by (bit_vector); x & 7}
} // verus!