Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532#[allow(unused_imports)]use verus_builtin::*;#[allow(unused_imports)]use verus_builtin_macros::*;use vstd::prelude::*;
verus! {
// ANCHOR: specspec fn triangle(n: nat) -> nat decreases n,{ if n == 0 { 0 } else { n + triangle((n - 1) as nat) }}
// ANCHOR_END: spec/*// ANCHOR: bogusspec fn bogus(i: int) -> int { bogus(i) + 1 // FAILS, error due to nontermination}// ANCHOR_END: bogus
// ANCHOR: exploit_bogusproof fn exploit_bogus() ensures false,{ assert(bogus(3) == bogus(3) + 1);}// ANCHOR_END: exploit_bogus*/
/*// ANCHOR: lacks_fuelfn test_triangle_fail() { assert(triangle(0) == 0); // succeeds assert(triangle(10) == 55); // FAILS}// ANCHOR_END: lacks_fuel*/
// ANCHOR: step_by_stepfn test_triangle_step_by_step() { assert(triangle(0) == 0); assert(triangle(1) == 1); assert(triangle(2) == 3); assert(triangle(3) == 6); assert(triangle(4) == 10); assert(triangle(5) == 15); assert(triangle(6) == 21); assert(triangle(7) == 28); assert(triangle(8) == 36); assert(triangle(9) == 45); assert(triangle(10) == 55); // succeeds}// ANCHOR_END: step_by_step
// ANCHOR: fuelfn test_triangle_reveal() { proof { reveal_with_fuel(triangle, 11); } assert(triangle(10) == 55);}// ANCHOR_END: fuel
// ANCHOR: fuel_byfn test_triangle_assert_by() { assert(triangle(10) == 55) by { reveal_with_fuel(triangle, 11); }}// ANCHOR_END: fuel_by
// ANCHOR: minspec fn min(x: int, y: int) -> int { if x <= y { x } else { y }}// ANCHOR_END: min
/*// ANCHOR: rec_failfn rec_triangle(n: u32) -> (sum: u32) ensures sum == triangle(n as nat),{ if n == 0 { 0 } else { n + rec_triangle(n - 1) // FAILS: possible overflow }}// ANCHOR_END: rec_fail*/
// ANCHOR: recfn rec_triangle(n: u32) -> (sum: u32) requires triangle(n as nat) <= u32::MAX, ensures sum == triangle(n as nat), decreases n,{ if n == 0 { 0 } else { n + rec_triangle(n - 1) }}// ANCHOR_END: rec
// ANCHOR: mutfn mut_triangle(n: u32, sum: &mut u32) requires triangle(n as nat) <= u32::MAX, ensures *final(sum) == triangle(n as nat), decreases n,{ if n == 0 { *sum = 0; } else { mut_triangle(n - 1, sum); *sum = *sum + n; }}// ANCHOR_END: mut
/*// ANCHOR: tail_failfn tail_triangle(n: u32, idx: u32, sum: &mut u32) requires idx <= n, *old(sum) == triangle(idx as nat), triangle(n as nat) <= u32::MAX, ensures *sum == triangle(n as nat),{ if idx < n { let idx = idx + 1; *sum = *sum + idx; tail_triangle(n, idx, sum); }}// ANCHOR_END: tail_fail*/
// ANCHOR: monoproof fn triangle_is_monotonic(i: nat, j: nat) ensures i <= j ==> triangle(i) <= triangle(j), decreases j,{ // We prove the statement `i <= j ==> triangle(i) <= triangle(j)` // by induction on `j`.
if j == 0 { // The base case (`j == 0`) is trivial since it's only // necessary to reason about when `i` and `j` are both 0. // So no proof lines are needed for this case. } else { // In the induction step, we can assume the statement is true // for `j - 1`. In Verus, we can get that fact into scope with // a recursive call substituting `j - 1` for `j`.
triangle_is_monotonic(i, (j - 1) as nat);
// Once we know it's true for `j - 1`, the rest of the proof // is trivial. }}
// ANCHOR_END: mono/*// ANCHOR: circularproof fn circular_reasoning() ensures false,{ circular_reasoning(); // FAILS, does not terminate}// ANCHOR_END: circular*/
// ANCHOR: tailfn tail_triangle(n: u32, idx: u32, sum: &mut u32) requires idx <= n, *old(sum) == triangle(idx as nat), triangle(n as nat) <= u32::MAX, ensures *final(sum) == triangle(n as nat), decreases n - idx,{ if idx < n { let idx = idx + 1; assert(*sum + idx <= u32::MAX) by { triangle_is_monotonic(idx as nat, n as nat); } *sum = *sum + idx; tail_triangle(n, idx, sum); }}// ANCHOR_END: tail
// ANCHOR: loopfn loop_triangle(n: u32) -> (sum: u32) requires triangle(n as nat) <= u32::MAX, ensures sum == triangle(n as nat),{ let mut sum: u32 = 0; let mut idx: u32 = 0; while idx < n invariant idx <= n, sum == triangle(idx as nat), triangle(n as nat) <= u32::MAX, decreases n - idx, { idx = idx + 1; assert(sum + idx <= u32::MAX) by { triangle_is_monotonic(idx as nat, n as nat); } sum = sum + idx; } sum}// ANCHOR_END: loop
// ANCHOR: loop_returnfn loop_triangle_return(n: u32) -> (sum: u32) ensures sum == triangle(n as nat) || (sum == 0xffff_ffff && triangle(n as nat) > u32::MAX),{ let mut sum: u32 = 0; let mut idx: u32 = 0; while idx < n invariant idx <= n, sum == triangle(idx as nat), decreases n - idx, { idx = idx + 1; if sum as u64 + idx as u64 > u32::MAX as u64 { proof { triangle_is_monotonic(idx as nat, n as nat); } return 0xffff_ffff; } sum = sum + idx; } sum}// ANCHOR_END: loop_return
#[verusfmt::skip]// ANCHOR: loop_breakfn loop_triangle_break(n: u32) -> (sum: u32) ensures sum == triangle(n as nat) || (sum == 0xffff_ffff && triangle(n as nat) > u32::MAX),{ let mut sum: u32 = 0; let mut idx: u32 = 0; while idx < n invariant_except_break idx <= n, sum == triangle(idx as nat), ensures sum == triangle(n as nat) || (sum == 0xffff_ffff && triangle(n as nat) > u32::MAX), decreases n - idx, { idx = idx + 1; if sum as u64 + idx as u64 > u32::MAX as u64 { proof { triangle_is_monotonic(idx as nat, n as nat); } sum = 0xffff_ffff; break; } sum = sum + idx; } sum}// ANCHOR_END: loop_break
// ANCHOR: for_loopfn for_loop_triangle(n: u32) -> (sum: u32) requires triangle(n as nat) <= u32::MAX, ensures sum == triangle(n as nat),{ let mut sum: u32 = 0;
for idx in 0..n invariant sum == triangle(idx as nat), triangle(n as nat) <= u32::MAX, { assert(sum + idx + 1 <= u32::MAX) by { triangle_is_monotonic((idx + 1) as nat, n as nat); } sum = sum + idx + 1; } sum}// ANCHOR_END: for_loop
// ANCHOR: ackermannspec fn ackermann(m: nat, n: nat) -> nat decreases m, n,{ if m == 0 { n + 1 } else if n == 0 { ackermann((m - 1) as nat, 1) } else { ackermann((m - 1) as nat, ackermann(m, (n - 1) as nat)) }}
proof fn test_ackermann() { reveal_with_fuel(ackermann, 9); assert(ackermann(2, 3) == 9);}// ANCHOR_END: ackermann
// ANCHOR: evenspec fn abs(i: int) -> int { if i < 0 { -i } else { i }}
spec fn is_even(i: int) -> bool decreases abs(i),{ if i == 0 { true } else if i > 0 { is_odd(i - 1) } else { is_odd(i + 1) }}
spec fn is_odd(i: int) -> bool decreases abs(i),{ if i == 0 { false } else if i > 0 { is_even(i - 1) } else { is_even(i + 1) }}
proof fn even_odd_mod2(i: int) ensures is_even(i) <==> i % 2 == 0, is_odd(i) <==> i % 2 == 1, decreases abs(i),{ if i < 0 { even_odd_mod2(i + 1); } if i > 0 { even_odd_mod2(i - 1); }}
fn test_even() { proof { reveal_with_fuel(is_even, 11); } assert(is_even(10));}
fn test_odd() { proof { reveal_with_fuel(is_odd, 11); } assert(!is_odd(10));}// ANCHOR_END: even
#[verusfmt::skip]mod M {use verus_builtin::*;
spec fn abs(i: int) -> int { if i < 0 { -i } else { i }}
// ANCHOR: even2spec fn is_even(i: int) -> bool decreases abs(i), 0int,{ if i == 0 { true } else if i > 0 { is_odd(i - 1) } else { is_odd(i + 1) }}
spec fn is_odd(i: int) -> bool decreases abs(i), 1int,{ !is_even(i)}
proof fn even_odd_mod2(i: int) ensures is_even(i) <==> i % 2 == 0, is_odd(i) <==> i % 2 == 1, decreases abs(i),{ reveal_with_fuel(is_odd, 2); if i < 0 { even_odd_mod2(i + 1); } if i > 0 { even_odd_mod2(i - 1); }}
fn test_even() { proof { reveal_with_fuel(is_even, 21); } assert(is_even(10));}
fn test_odd() { proof { reveal_with_fuel(is_odd, 22); } assert(!is_odd(10));}// ANCHOR_END: even2}
// ANCHOR: example_decreases_toproof fn example_decreases_to(s: Seq<int>) requires s.len() == 5{ assert(decreases_to!(8int => 4int));
// fails: can't decrease to negative number // assert(decreases_to!(8 => -2));
// Comma-separated elements are treated lexicographically: assert(decreases_to!(12int, 8int, 1int => 12int, 4int, 50000int));
// Datatypes decrease-to their fields: let x = Some(8int); assert(decreases_to!(x => x->0));
let y = (true, false); assert(decreases_to!(y => y.0));
// fails: tuples are not treated lexicographically // assert(decreases_to!((20, 9) => (11, 15)));
// sequence decreases-to an element of the sequence assert(decreases_to!(s => s[2]));
// sequence decreases-to a subrange of the sequence assert(decreases_to!(s => s[1..3]));}// ANCHOR_END: example_decreases_to
// ANCHOR: example_proof_in_specspec fn floor_log2(n: u64) -> int decreases n{ if n <= 1 { 0 } else { proof { assert(n > 1 ==> (n >> 1) < n) by(bit_vector); } floor_log2(n >> 1) + 1 } }// ANCHOR_END: example_proof_in_spec
// ANCHOR: example_proof_using_viaspec fn floor_log2_via(n: u64) -> int decreases n via floor_log2_decreases_proof{ if n <= 1 { 0 } else { floor_log2_via(n >> 1) + 1 } }
#[via_fn]proof fn floor_log2_decreases_proof(n: u64) { assert(n > 1 ==> (n >> 1) < n) by(bit_vector);}// ANCHOR_END: example_proof_using_via
fn main() {}
} // verus!