From 5252a77d90f7a46b6dad55a0a1ab01252d0bbb6e Mon Sep 17 00:00:00 2001 From: jaybosamiya <5683582+jaybosamiya@users.noreply.github.com> Date: Mon, 25 Mar 2024 18:34:49 +0000 Subject: [PATCH] chore: update to latest Verus snapshot --- .../source/rust_verify/example/syntax.rs | 143 ++++++++---------- .../source/vstd/source/vstd/atomic.rs | 8 +- .../source/vstd/source/vstd/atomic_ghost.rs | 26 +--- .../source/vstd/source/vstd/std_specs/num.rs | 16 +- 4 files changed, 74 insertions(+), 119 deletions(-) diff --git a/examples/verus-snapshot/source/rust_verify/example/syntax.rs b/examples/verus-snapshot/source/rust_verify/example/syntax.rs index 33a479f..91c1237 100644 --- a/examples/verus-snapshot/source/rust_verify/example/syntax.rs +++ b/examples/verus-snapshot/source/rust_verify/example/syntax.rs @@ -1,10 +1,11 @@ #![allow(unused_imports)] -use builtin::*; use builtin_macros::*; -use vstd::{modes::*, prelude::*, seq::*, *}; +use builtin::*; +use vstd::{*, prelude::*, seq::*, modes::*}; #[verifier::external] -fn main() {} +fn main() { +} verus! { @@ -54,8 +55,8 @@ fn test_my_funs(x: u32, y: u32) // my_proof_fun(x, y); // not allowed in exec code // let u = my_spec_fun(x, y); // not allowed exec code proof { - let u = my_spec_fun(x as int, y as int); // allowed in proof code - my_proof_fun(u / 2, y as int); // allowed in proof code + let u = my_spec_fun(x as int, y as int); // allowed in proof code + my_proof_fun(u / 2, y as int); // allowed in proof code } } @@ -65,14 +66,12 @@ pub open spec fn my_pub_spec_fun1(x: int, y: int) -> int { // function and body visible to all x / 2 + y / 2 } - /* TODO pub open(crate) spec fn my_pub_spec_fun2(x: u32, y: u32) -> u32 { // function visible to all, body visible to crate x / 2 + y / 2 } */ - // TODO(main_new) pub(crate) is not being handled correctly // pub(crate) open spec fn my_pub_spec_fun3(x: int, y: int) -> int { // // function and body visible to crate @@ -82,7 +81,6 @@ pub closed spec fn my_pub_spec_fun4(x: int, y: int) -> int { // function visible to all, body visible to module x / 2 + y / 2 } - pub(crate) closed spec fn my_pub_spec_fun5(x: int, y: int) -> int { // function visible to crate, body visible to module x / 2 + y / 2 @@ -94,7 +92,7 @@ fn test_rec(x: u64, y: u64) requires 0 < x < 100, y < 100 - x, - decreases x, + decreases x { if x > 1 { test_rec(x - 1, y + 1); @@ -104,7 +102,7 @@ fn test_rec(x: u64, y: u64) /// Multiple decreases clauses are ordered lexicographically, so that later clauses may /// increase when earlier clauses decrease. spec fn test_rec2(x: int, y: int) -> int - decreases x, y, + decreases x, y { if y > 0 { 1 + test_rec2(x, y - 1) @@ -122,15 +120,14 @@ spec fn test_rec2(x: int, y: int) -> int /// - recommends .. "when" specifies a proof function that proves the /// recommendations of the functions invoked in the body spec fn add0(a: nat, b: nat) -> nat - recommends - a > 0, + recommends a > 0 via add0_recommends { a + b } spec fn dec0(a: int) -> int - decreases a, + decreases a when a > 0 via dec0_decreases { @@ -161,17 +158,17 @@ proof fn dec0_decreases(a: int) { /// - variables in spec code are always ghost /// For example: fn test_my_funs2( - a: u32, // exec variable - b: u32, // exec variable + a: u32, // exec variable + b: u32, // exec variable ) requires a < 100, b < 100, { - let s = a + b; // s is an exec variable + let s = a + b; // s is an exec variable proof { - let u = a + b; // u is a ghost variable - my_proof_fun(u / 2, b as int); // my_proof_fun(x, y) takes ghost parameters x and y + let u = a + b; // u is a ghost variable + my_proof_fun(u / 2, b as int); // my_proof_fun(x, y) takes ghost parameters x and y } } @@ -184,31 +181,27 @@ spec fn f1(i: int) -> int { fn assert_by_test() { assert(f1(3) > 3) by { - reveal(f1); // reveal f1's definition just inside this block + reveal(f1); // reveal f1's definition just inside this block } assert(f1(3) > 3); } /// "assert by" can also invoke specialized provers for bit-vector reasoning or nonlinear arithmetic. fn assert_by_provers(x: u32) { - assert(x ^ x == 0u32) by (bit_vector); - assert(2 <= x && x < 10 ==> x * x > x) by (nonlinear_arith); + assert(x ^ x == 0u32) by(bit_vector); + assert(2 <= x && x < 10 ==> x * x > x) by(nonlinear_arith); } /// "assert by" provers can also appear on function signatures to select a specific prover /// for the function body. proof fn lemma_mul_upper_bound(x: int, x_bound: int, y: int, y_bound: int) by (nonlinear_arith) - requires - x <= x_bound, - y <= y_bound, - 0 <= x, - 0 <= y, - ensures - x * y <= x_bound * y_bound, + requires x <= x_bound, y <= y_bound, 0 <= x, 0 <= y, + ensures x * y <= x_bound * y_bound, { } + /// "assert by" can use nonlinear_arith with proof code, /// where "requires" clauses selectively make facts available to the proof code. proof fn test5_bound_checking(x: u32, y: u32, z: u32) @@ -217,7 +210,7 @@ proof fn test5_bound_checking(x: u32, y: u32, z: u32) y <= 0xffff, z <= 0xffff, { - assert(x * z == mul(x, z)) by (nonlinear_arith) + assert(x * z == mul(x, z)) by(nonlinear_arith) requires x <= 0xffff, z <= 0xffff, @@ -241,6 +234,7 @@ fn test_assert_forall_by() { } assert(f1(1) + f1(2) == 5); assert(f1(3) + f1(4) == 9); + // to prove forall|...| P ==> Q, write assert forall|...| P implies Q by {...} assert forall|x: int| x < 10 implies f1(x) < 11 by { assert(x < 10); @@ -257,6 +251,7 @@ fn test_choose() { let x_witness = choose|x: int| f1(x) == 10; assert(f1(x_witness) == 10); } + assume(exists|x: int, y: int| f1(x) + f1(y) == 30); proof { let (x_witness, y_witness): (int, int) = choose|x: int, y: int| f1(x) + f1(y) == 30; @@ -270,11 +265,11 @@ fn test_single_trigger1() { // Use [my_spec_fun(x, y)] as the trigger assume(forall|x: int, y: int| f1(x) < 100 && f1(y) < 100 ==> #[trigger] my_spec_fun(x, y) >= x); } - fn test_single_trigger2() { // Use [f1(x), f1(y)] as the trigger - assume(forall|x: int, y: int| #[trigger] - f1(x) < 100 && #[trigger] f1(y) < 100 ==> my_spec_fun(x, y) >= x); + assume(forall|x: int, y: int| + #[trigger] f1(x) < 100 && #[trigger] f1(y) < 100 ==> my_spec_fun(x, y) >= x + ); } /// To manually specify multiple triggers, use #![trigger]: @@ -283,7 +278,8 @@ fn test_multiple_triggers() { assume(forall|x: int, y: int| #![trigger my_spec_fun(x, y)] #![trigger f1(x), f1(y)] - f1(x) < 100 && f1(y) < 100 ==> my_spec_fun(x, y) >= x); + f1(x) < 100 && f1(y) < 100 ==> my_spec_fun(x, y) >= x + ); } /// Verus can often automatically choose a trigger if no manual trigger is given. @@ -311,17 +307,16 @@ spec fn simple_conjuncts(x: int, y: int) -> bool { &&& x < 100 &&& y < 100 } - spec fn complex_conjuncts(x: int, y: int) -> bool { let b = x < y; &&& b &&& if false { - &&& b ==> b - &&& !b ==> !b - } else { - ||| b ==> b - ||| !b - } + &&& b ==> b + &&& !b ==> !b + } else { + ||| b ==> b + ||| !b + } &&& false ==> true } @@ -333,14 +328,17 @@ pub(crate) proof fn binary_ops(a: A, x: int) { assert(false ==> true); assert(true && false ==> false && false); assert(!(true && (false ==> false) && false)); + assert(false ==> false ==> false); assert(false ==> (false ==> false)); assert(!((false ==> false) ==> false)); + assert(false <== false <== false); assert(!(false <== (false <== false))); assert((false <== false) <== false); assert(2 + 2 !== 3); assert(a == a); + assert(false <==> true && false); } @@ -363,7 +361,7 @@ fn test_views() { v.push(10); v.push(20); proof { - let s: Seq = v@; // v@ is equivalent to v.view() + let s: Seq = v@; // v@ is equivalent to v.view() assert(s[0] == 10); assert(s[1] == 20); } @@ -371,7 +369,10 @@ fn test_views() { /// struct and enum declarations may be declared exec (default), tracked, or ghost, /// and fields may be declared exec (default), tracked or ghost. -tracked struct TrackedAndGhost(tracked T, ghost G); +tracked struct TrackedAndGhost( + tracked T, + ghost G, +); /// Proof code may manipulate tracked variables directly. /// Declarations of tracked variables must be explicitly marked as "tracked". @@ -382,7 +383,7 @@ proof fn test_tracked( tracked w: int, tracked x: int, tracked y: int, - z: int, + z: int ) -> tracked TrackedAndGhost<(int, int), int> { consume(w); let tracked tag: TrackedAndGhost<(int, int), int> = TrackedAndGhost((x, y), z); @@ -400,7 +401,7 @@ fn test_ghost(x: u32, y: u32) let ghost mut v = u + 1; assert(v == x + y + 1); proof { - v = v + 1; // proof code may assign to ghost mut variables + v = v + 1; // proof code may assign to ghost mut variables } let ghost w = { let temp = v + 1; @@ -426,21 +427,18 @@ fn test_ghost_wrappers(x: u32, y: Ghost) let mut v: Ghost = Ghost(u@ + 1); assert(v@ == x + y@ + 1); proof { - v@ = v@ + 1; // proof code may assign to the view of exec variables of type Ghost/Tracked + v@ = v@ + 1; // proof code may assign to the view of exec variables of type Ghost/Tracked } - let w: Ghost = Ghost( - { - // proof block that returns a ghost value - let temp = v@ + 1; - temp + 1 - }, - ); + let w: Ghost = Ghost({ + // proof block that returns a ghost value + let temp = v@ + 1; + temp + 1 + }); assert(w@ == x + y@ + 4); } fn test_consume(t: Tracked) - requires - t@ <= 7, + requires t@ <= 7 { proof { let tracked x = t.get(); @@ -450,10 +448,7 @@ fn test_consume(t: Tracked) } /// Ghost(...) and Tracked(...) patterns can unwrap Ghost<...> and Tracked<...> values: -fn test_ghost_unwrap( - x: u32, - Ghost(y): Ghost, -) // unwrap so that y has typ u32, not Ghost +fn test_ghost_unwrap(x: u32, Ghost(y): Ghost) // unwrap so that y has typ u32, not Ghost requires x < 100, y < 100, @@ -463,15 +458,13 @@ fn test_ghost_unwrap( let Ghost(mut v): Ghost = Ghost(u + 1); assert(v == x + y + 1); proof { - v = v + 1; // assign directly to ghost mut v + v = v + 1; // assign directly to ghost mut v } - let Ghost(w): Ghost = Ghost( - { - // proof block that returns a ghost value - let temp = v + 1; - temp + 1 - }, - ); + let Ghost(w): Ghost = Ghost({ + // proof block that returns a ghost value + let temp = v + 1; + temp + 1 + }); assert(w == x + y + 4); } @@ -483,8 +476,10 @@ struct S {} fn test_ghost_tuple_match(t: (Tracked, Tracked, Ghost, Ghost)) -> Tracked { let ghost g: (int, int) = (10, 20); assert(g.0 + g.1 == 30); + let ghost (g1, g2) = g; assert(g1 + g2 == 30); + // b1, b2: Tracked and g3, g4: Ghost let (Tracked(b1), Tracked(b2), Ghost(g3), Ghost(g4)) = t; Tracked(b2) @@ -529,8 +524,7 @@ spec fn my_uninterpreted_fun1(i: int, j: int) -> int; spec fn my_uninterpreted_fun2(i: int, j: int) -> int recommends 0 <= i < 10, - 0 <= j < 10, -; + 0 <= j < 10; /// Trait functions may have specifications trait T { @@ -540,8 +534,7 @@ trait T { 0 <= j < 10, ensures i <= r, - j <= r, - ; + j <= r; } enum ThisOrThat { @@ -552,7 +545,7 @@ enum ThisOrThat { proof fn uses_is(t: ThisOrThat) { match t { ThisOrThat::This(..) => assert(t is This), - ThisOrThat::That { .. } => assert(t is That), + ThisOrThat::That {..} => assert(t is That), } } @@ -566,22 +559,20 @@ proof fn uses_arrow_matches_1(t: ThisOrThat) } proof fn uses_arrow_matches_2(t: ThisOrThat) - requires - t matches ThisOrThat::That { v: a } && a == 3, + requires t matches ThisOrThat::That { v: a } && a == 3, { assert(t is That && t->v == 3); } #[verifier::external_body] -struct Collection {} +struct Collection { } impl Collection { pub spec fn spec_has(&self, v: nat) -> bool; } proof fn uses_spec_has(c: Collection) - requires - c has 3, + requires c has 3, { assert(c has 3); assert(c has 3 == c has 3); diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs index 561c6df..906cff9 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/atomic.rs @@ -471,13 +471,7 @@ macro_rules! atomic_bool_methods { }; } -make_bool_atomic!( - PAtomicBool, - PermissionBool, - PermissionDataBool, - AtomicBool, - bool -); +make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool); make_unsigned_integer_atomic!( PAtomicU8, diff --git a/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs b/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs index 1da04c3..4dee0b0 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/atomic_ghost.rs @@ -114,33 +114,15 @@ declare_atomic_type!(AtomicU64, PAtomicU64, PermissionU64, u64, AtomicPredU64); declare_atomic_type!(AtomicU32, PAtomicU32, PermissionU32, u32, AtomicPredU32); declare_atomic_type!(AtomicU16, PAtomicU16, PermissionU16, u16, AtomicPredU16); declare_atomic_type!(AtomicU8, PAtomicU8, PermissionU8, u8, AtomicPredU8); -declare_atomic_type!( - AtomicUsize, - PAtomicUsize, - PermissionUsize, - usize, - AtomicPredUsize -); +declare_atomic_type!(AtomicUsize, PAtomicUsize, PermissionUsize, usize, AtomicPredUsize); declare_atomic_type!(AtomicI64, PAtomicI64, PermissionI64, i64, AtomicPredI64); declare_atomic_type!(AtomicI32, PAtomicI32, PermissionI32, i32, AtomicPredI32); declare_atomic_type!(AtomicI16, PAtomicI16, PermissionI16, i16, AtomicPredI16); declare_atomic_type!(AtomicI8, PAtomicI8, PermissionI8, i8, AtomicPredI8); -declare_atomic_type!( - AtomicIsize, - PAtomicIsize, - PermissionIsize, - isize, - AtomicPredIsize -); - -declare_atomic_type!( - AtomicBool, - PAtomicBool, - PermissionBool, - bool, - AtomicPredBool -); +declare_atomic_type!(AtomicIsize, PAtomicIsize, PermissionIsize, isize, AtomicPredIsize); + +declare_atomic_type!(AtomicBool, PAtomicBool, PermissionBool, bool, AtomicPredBool); /// Performs a given atomic operation on a given atomic /// while providing access to its ghost state. diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs index 0fee85b..63edbb6 100644 --- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs +++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/num.rs @@ -165,20 +165,8 @@ num_specs!(u8, i8, u8_specs, i8_specs, 0x100); num_specs!(u16, i16, u16_specs, i16_specs, 0x1_0000); num_specs!(u32, i32, u32_specs, i32_specs, 0x1_0000_0000); num_specs!(u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000); -num_specs!( - u128, - i128, - u128_specs, - i128_specs, - 0x1_0000_0000_0000_0000_0000_0000_0000_0000 -); -num_specs!( - usize, - isize, - usize_specs, - isize_specs, - (usize::MAX - usize::MIN + 1) -); +num_specs!(u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000); +num_specs!(usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1)); verus! {