Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117use verus_builtin::*;use verus_builtin_macros::*;#[allow(unused_imports)]use vstd::{modes::*, prelude::*, seq::*, *};
verus! {
spec fn arith_sum_int(i: int) -> int decreases i,{ if i <= 0 { 0 } else { i + arith_sum_int(i - 1) }}
#[verifier::opaque]spec fn arith_sum_u64(i: u64) -> u64 decreases i,{ if i == 0 { 0 } else { (i + arith_sum_u64((i - 1) as u64)) as u64 }}
proof fn arith_sum_int_nonneg(i: nat) ensures arith_sum_int(i as int) >= 0, decreases i,{ if i > 0 { arith_sum_int_nonneg((i - 1) as nat); }}
proof fn arith_sum_test1() { assert(arith_sum_int(0) == 0); // Recursive functions default to 1 fuel, so without the assert above, // the following assert will fail assert(arith_sum_int(1) == 1); assert(arith_sum_int(2) == 3); assert(arith_sum_int(3) == 6);}
proof fn arith_sum_test2() { // Instead of writing out intermediate assertions, // we can instead boost the fuel setting reveal_with_fuel(arith_sum_int, 4); assert(arith_sum_int(3) == 6);}
proof fn arith_sum_test3() { reveal_with_fuel(arith_sum_u64, 4); assert(arith_sum_u64(3) == 6);}
proof fn arith_sum_monotonic(i: nat, j: nat) requires i <= j, ensures arith_sum_int(i as int) <= arith_sum_int(j as int), decreases j,{ if i < j { arith_sum_monotonic(i, (j - 1) as nat); }}
fn compute_arith_sum(n: u64) -> (sum: u64) requires n < 100, ensures arith_sum_int(n as int) == sum,{ let mut sum: u64 = 0; for i in 0..n invariant n < 100, arith_sum_int(i as int) == sum, sum <= 100 * i, { sum = sum + (i + 1); } sum}
fn run_arith_sum(n: u64) -> u64 { let mut result: u64 = 0; if n < 100 { result = compute_arith_sum(n); } result}
fn exec_with_decreases(n: u64) -> u64 decreases 100 - n,{ if n < 100 { exec_with_decreases(n + 1) } else { n }}
} // verus!fn main() { let args = std::env::args(); for arg in args { if let Ok(n) = arg.parse::<u64>() { println!("{}", run_arith_sum(n)); } }}