Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214#![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 { b } else { a } /*+*/ if a >= b { a } else { b }}
// ;; Function-Def crate::max// (push)// (declare-const ret~10@ Int)// (declare-const a~2@ Int)// (declare-const b~4@ Int)// (assert fuel_defaults)// (assert (uInv 64 a~2@))// (assert (uInv 64 b~4@))// ;; postcondition not satisfied// (declare-const %%location_label%%0 Bool)// ;; postcondition not satisfied// (declare-const %%location_label%%1 Bool)// (declare-const %%query%% Bool)// (assert// (=>// %%query%%// (not (=>// (= ret~10@ (ite// (>= a~2@ b~4@)// a~2@// b~4@// ))// (and// (=>// %%location_label%%0// (or// (= ret~10@ a~2@)// (= ret~10@ b~4@)// ))// (=>// %%location_label%%1// (and// (>= ret~10@ a~2@)// (>= ret~10@ b~4@)// )))))))// (assert %%query%%)// (set-option :rlimit 30000000)// (check-sat)// (set-option :rlimit 0)// (pop)// ## B -- B-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); }}
spec 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}
// ## C -- C-linearity.rs//- exec fn f(v: Vec<u64>) -> (Vec<u64>, Vec<u64>) {//- let v1 = v;//- let v2 = v;//- (v1, v2)//- }/*+*/
exec fn f(v: Vec<u64>) { /*+*/ let v1: Ghost<Vec<u64>> = Ghost(v); /*+*/ let v2: Ghost<Vec<u64>> = Ghost(v); /*+*/ assert(v1@.len() == v2@.len()); /*+*/}
exec fn g(v1: &mut Vec<u64>, v2: &mut Vec<u64>) requires old(v1)@.len() == 2, old(v2)@.len() == 3, ensures final(v1)@.len() == final(v2)@.len(),{ v1.push(42); v1.push(43); v2.push(52);}
// exec fn g_(v1: Vec<u64>, v2: Vec<u64>) -> (out: (Vec<u64>, Vec<u64>))// requires// v1@.len() == 2,// v2@.len() == 3,// ensures// out.0@.len() == out.1@.len()// {// let v1a = v1.push(42);// let v1b = v1.push(43);// let v2a.push(52);// (v1b, v2a)// }// ## 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(); #[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!