Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124#![feature(proc_macro_hygiene)]
use vstd::prelude::*;
// ANCHOR: verus_spec#[verus_spec(sum => requires x < 100, y < 100, ensures sum < 200, )]fn my_exec_fun(x: u32, y: u32) -> u32 { x + y }// ANCHOR_END: verus_spec
// ANCHOR: loop#[verus_spec(v => ensures true)]fn test_for_loop(n: u32) -> Vec<u32> { let mut v: Vec<u32> = Vec::new();
#[verus_spec( invariant v@ =~= Seq::new(i as nat, |k| k as u32), )] for i in 0..n { v.push(i); } v}// ANCHOR_END: loop
// ANCHOR: proof#[verus_spec]fn exec_with_proof() { proof_decl!{ let ghost mut i = 0int; assert(true); } test_for_loop(10); proof!{ assert(i == 0); }}// ANCHOR_END: proof
// ANCHOR: proof_with#[verus_spec(ret =>with Tracked(y): Tracked<&mut int>, Ghost(w): Ghost<u32> -> z: Ghost<u32>requires x < 100, *old(y) < 100,ensures *final(y) == x, ret == x + 1, z@ == x,)]fn exec_tracked(x: u32) -> u32 { proof! { *y = x as int; } proof_with!(|= Ghost(x)); (x + 1)}
#[verus_spec]fn exec_tracked_test(x: u32) { proof_decl!{ let ghost mut z = 0u32; let tracked mut y = 0; }
proof_with!{Tracked(&mut y), Ghost(0) => Ghost(z)} let x = exec_tracked(1);
proof!{ assert(y == 1); assert(z == 1); assert(x == 2); }}
fn exec_external_test(x: u32) -> u32 { exec_tracked(1)}
// ANCHOR_END: proof_with
// ANCHOR: dual_spec#[verus_verify(dual_spec, closed)]#[verus_spec( requires x < 100, y < 100, returns f(x, y))]pub fn f(x: u32, y: u32) -> u32 { proof!{ assert(true); } { proof!{assert(true);} x + y }}
#[verus_verify(dual_spec, open)]#[verus_spec( requires x < 100, returns f2(x),)]pub fn f2(x: u32) -> u32 { f(x, 1)}// ANCHOR_END: dual_spec