verus-lang / verus Goto Github PK

View Code? Open in Web Editor NEW

1.1K 1.1K 58.0 15.65 MB

Verified Rust for low-level systems code

License: MIT License

Rust 99.69% Shell 0.17% Nix 0.01% PowerShell 0.01% Batchfile 0.01% HTML 0.10% Dockerfile 0.01%

verus's People

Contributors

Stargazers

Watchers

verus's Issues

verification error message lists unrelated precondition

This:

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use pervasive::*;

fn get_bool() -> bool {
    ensures(|b: bool| b == true);
    true
}

fn require_false() -> bool {
    requires(false);                // line 12
    false
}

fn main() {
    let x = 6;

    if !get_bool() {
        require_false();
    }

    assert(x == 7);              // line 23
}

gives the following error message:

Verifying root module
error: assertion failure
  --> l.rs:23:5
   |
12 |     requires(false);
   |              ----- failed precondition
...
23 |     assert(x == 7);
   |     ^^^^^^^^^^^^^^

This doesn't make any sense at all - line 12 should easily pass verification, and also, it isn't even a precondition of the actual failing assert on line 23

when fixed, un-ignore test added in 5c6c14d

Test variable assignment inside while loops

Regression test for #10

Yes, it would be good to test variable assignment inside while loops:

variables that get assigned should be havoc'd
variables that don't get assigned should have their original value
variables that are declared inside the while loop should not cause any changes in behavior to variables outside the while loop

Originally posted by @Chris-Hawblitzel in #10 (review)

Timeouts in recommends checks (in nonlinear queries) are reported incorrectly, and look like verification failures

The context doesn't say that the timeout occurred in the recommends check, so it appears that the main function check timed-out instead.

Consider setting an rlimit for the test suite

If the user does not specify an rlimit via the VERIFY_EXTRA_ARGS environment variable, then the args we pass to the verifier are instantiated via a default() call:
https://github.com/secure-foundations/verus/blob/b44a565193338c90fa50fe2f0620664cf6f26d0f/source/rust_verify/tests/common/mod.rs#L124
This appears to set the rlimit to 0, which means a test can potentially run forever. I might suggest that we add something like:

         our_args.verify_pervasive |= verify_pervasive;
+        our_args.rlimit = DEFAULT_RLIMIT_SECS;
         our_args

I tried this as an experiment, and on the CI machine, it causes e18_pass from rust_verify/tests/summer_school.rs to fail, so we may want to tweak that test or introduce the ability to locally increase the rlimit before adopting a test-suite-wide rlimit.

Panic when recommends checking `forall_arith`

Found by @matthias-brun in utaal/verified-nrkernel@4afc7c7

        fndecl!(fn some_fn(a: int) -> bool);

        #[proof]
        fn p() {
            ensures([
                forall_arith(|a: int, b: int| #[trigger] (a * b) == b * a),
                forall(|a: int| some_fn(a)),
            ]);
        }

panics with:

thread 'rustc' panicked at 'HasType', vir/src/sst_to_air.rs:497:66

during the recommends check.

un-ignore the regression test

vir::def::path_to_string is not injective

vir::def::path_to_string is not injective, for example:

krate: Some("a"), segments: ["b"]

and

krate: None, segments: ["a", "b"]

will generate the same string. We need to adjust the encoding so that a krate prefix is distinguished.

`error: expression has mode proof, expected mode exec` when using pervasive::map

Hi Verus developers,

Thanks for building verus and I am currently using it to verify some programs I wrote before. But I encountered some confusing errors and need some help from you.

I was running verus (./tools/rust-verify.sh rust_verify/example/myexample.rs) on the following program:

#[allow(unused_imports)]
mod pervasive;
use pervasive::map::*;

#[exec]
pub enum Myenum {
    S1,
    S2,
}

#[exec]
pub fn myfun(map: Map<i32, i32>) -> Myenum {
    if map.dom().contains(10) {
        return Myenum::S1;
    } else {
        return Myenum::S2;
    }
}

#[exec]
fn main() { }

and verus reports the error

error: expression has mode proof, expected mode exec
  --> rust_verify/example/mini.rs:14:16
   |
14 |         return Myenum::S1;
   |                ^^^^^^^^^^

error: aborting due to previous error

If I remove the usage of Map, the error will disappear. I am confused about why this error can happen as I have annotated every function and every enum with exec as shown in the code, and why it is related to the pervasive::map. I have read this doc: https://github.com/secure-foundations/verus/blob/main/source/docs/design/modes.md but still do not know what is the root cause of the error. Could you please let me know what is the best way to address this error?

Thank you

requires not checked in if/else condition

This code should fail, but passes (I think this is from 2efa2bfe6c7025d7868c673ba6c89a187b5d25ff ):

fn f(b: bool) -> bool {
    requires(b);
    true
}

fn test() -> u64 {
    if f(false) { 20 } else { 30 }
}

How to build exec code with cargo outside verus

Hi Verus team, I was trying to build my project with verus. The project structure is like

├── Cargo.lock
├── Cargo.toml
└── src
    ├── logic.rs
    └── main.rs

and it sits outside verus folder.

The logic.rs imports some files from verus:

#[allow(unused_imports)]
use builtin_macros::*;
#[allow(unused_imports)]
use builtin::*;

mod pervasive;
#[allow(unused_imports)]
use pervasive::{*, option::Option, map::*};

and is successfully verified by ./tools/rust-verify.sh ../../myproject/src/logic.rs

I imported builtin_macros and builtin in my cargo.toml

builtin_macros = { path = "../verus/source/builtin_macros" }
builtin = { path = "../verus/source/builtin" }

However, I was not able to import pervasive.

I have tried the following:

import pervasive in cargo.toml -- it does not work because there is no cargo.toml in the pervasive folder
copy verus/source/pervasive to myproject/src/pervasive -- it does not work and report

error[E0583]: file not found for module `pervasive`
 --> src/logic.rs:9:1
  |
9 | mod pervasive;
  | ^^^^^^^^^^^^^^
  |
  = help: to create the module `pervasive`, create file "src/logic/pervasive.rs" or "src/logic/pervasive/mod.rs"

move myproject/src/pervasive to myproject/src/logic/pervasive -- a lot of errors are reported like

error[E0531]: cannot find tuple struct or tuple variant `Proof` in this scope
   --> src/logic/pervasive/atomic.rs:127:17
    |
127 |             let Proof(t) = exec_proof_from_false();
    |                 ^^^^^ not found in this scope
...
493 | make_signed_integer_atomic!(PAtomicI64, PermissionI64, AtomicI64, i64, wrapping_add_i64, wrapping_sub_i64, -0x8000_0000_0000_0000, 0x7fff_ffff_ffff_fff...
    | --------------------------------------------------------------------------------------------------------------------------------------------------------- in this macro invocation

I also looked into https://github.com/utaal/verified-nrkernel/tree/main/page-table but didn't find out how to build exec code with cargo there.

Could you please let me know what is the best practice to organize and build (using cargo) projects that rely on verus but sit outside verus?

erasure panic with conditional and variant `is_*` function

use builtin::*;
use builtin_macros::*;
mod pervasive;
use crate::pervasive::*;
use crate::pervasive::option::*;


#[proof]
fn foo() {
    let x = (if (Option::Some(5)).is_Some() { 0 } else { 1 });
}

fn main() { }

gives a panic:

thread 'rustc' panicked at 'erase_expr', rust_verify/src/erase.rs:742:39
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::panic_display
   3: core::option::expect_failed
   4: core::option::Option<T>::expect
             at /Users/thance/verus/rust/library/core/src/option.rs:709:21
   5: rust_verify::erase::erase_expr_opt
             at ./rust_verify/src/erase.rs:742:30
   6: rust_verify::erase::erase_expr_opt
             at ./rust_verify/src/erase.rs:461:19
   7: rust_verify::erase::erase_stmt
             at ./rust_verify/src/erase.rs:875:25
   8: rust_verify::erase::erase_block::{{closure}}
             at ./rust_verify/src/erase.rs:1005:33
   9: core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut
             at /Users/thance/verus/rust/library/core/src/ops/function.rs:269:13
  10: core::iter::traits::iterator::Iterator::find_map::check::{{closure}}
             at /Users/thance/verus/rust/library/core/src/iter/traits/iterator.rs:2409:32
  11: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::try_fold::enumerate::{{closure}}
             at /Users/thance/verus/rust/library/core/src/iter/adapters/enumerate.rs:85:27
  12: core::iter::traits::iterator::Iterator::try_fold
             at /Users/thance/verus/rust/library/core/src/iter/traits/iterator.rs:1995:21
  13: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::try_fold
             at /Users/thance/verus/rust/library/core/src/iter/adapters/enumerate.rs:91:9
  14: core::iter::traits::iterator::Iterator::find_map
             at /Users/thance/verus/rust/library/core/src/iter/traits/iterator.rs:2415:9
  15: <core::iter::adapters::filter_map::FilterMap<I,F> as core::iter::traits::iterator::Iterator>::next
             at /Users/thance/verus/rust/library/core/src/iter/adapters/filter_map.rs:61:9
  16: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter
             at /Users/thance/verus/rust/library/alloc/src/vec/spec_from_iter_nested.rs:23:32
  17: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
             at /Users/thance/verus/rust/library/alloc/src/vec/spec_from_iter.rs:33:9
  18: <alloc::vec::Vec<T> as core::iter::traits::collect::FromIterator<T>>::from_iter
             at /Users/thance/verus/rust/library/alloc/src/vec/mod.rs:2549:9
  19: core::iter::traits::iterator::Iterator::collect
             at /Users/thance/verus/rust/library/core/src/iter/traits/iterator.rs:1745:9
  20: rust_verify::erase::erase_block
             at ./rust_verify/src/erase.rs:1001:28
  21: rust_verify::erase::erase_fn::{{closure}}
             at ./rust_verify/src/erase.rs:1078:51
  22: core::option::Option<T>::map
             at /Users/thance/verus/rust/library/core/src/option.rs:846:29
  23: rust_verify::erase::erase_fn
             at ./rust_verify/src/erase.rs:1078:20
  24: rust_verify::erase::erase_item
             at ./rust_verify/src/erase.rs:1201:19
  25: rust_verify::erase::erase_crate
             at ./rust_verify/src/erase.rs:1261:26
  26: <rust_verify::erase::CompilerCallbacks as rustc_lint::FormalVerifierRewrite>::rewrite_crate
             at ./rust_verify/src/erase.rs:1376:21
  27: rustc_interface::passes::configure_and_expand
  28: <rustc_interface::queries::Queries>::expansion
  29: <rustc_interface::queries::Queries>::prepare_outputs
  30: <rustc_interface::queries::Queries>::global_ctxt
  31: rust_verify::lifetime::check
             at ./rust_verify/src/lifetime.rs:6:5
  32: <rust_verify::erase::CompilerCallbacks as rustc_driver::Callbacks>::after_parsing
             at ./rust_verify/src/erase.rs:1397:13
  33: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorReported>>
  34: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorReported>, rustc_interface::interface::create_compiler_and_run<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#1}>
  35: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::util::setup_callbacks_and_run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorReported>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorReported>>::{closure#0}::{closure#0}, core::result::Result<(), rustc_errors::ErrorReported>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Panic when calling proof mode functions in impl

The following code panics:

struct S {}

impl S {
    #[proof]
    pub fn lemma(self) {
    }

    pub fn f(self) {
        self.lemma();
    }
}

fn main() { }

thread 'rustc' panicked at 'called `Option::unwrap()` on a `None` value', compiler/rustc_resolve/src/late.rs:2401:52
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

ping @utaal

Minor logging issue: `--log-vir` for `example/atomics.rs` and `example/og_counter.rs` panics

When I run tools/rust-verify.sh rust_verify/example/atomics.rs --log-vir logs/log.vir, it gives thread 'rustc' panicked at 'invalid atom ","', /Users/chanhee/.cargo/registry/src/github.com-1ecc6299db9ec823/sise-0.6.0/src/spaced_string_writer.rs:194:9

Similarly, it makes the following run VERIFY_LOG_IR_PATH="logs" RUSTC=../rust/install/bin/rustc ../rust/install/bin/cargo test -p rust_verify --test atomics hangs.

Nested `assert_forall_by` causes incompleteness?

Found by @matthias-brun.

#[proof]
pub fn test<S, T>() {
    assert_forall_by(|m1: Map<S, T>, m2: Map<S, T>, n: S| {
        requires(m1.dom().contains(n) && !m2.dom().contains(n));
        ensures(equal(m1.remove(n).union_prefer_right(m2), m1.union_prefer_right(m2).remove(n)));

        let union1 = m1.remove(n).union_prefer_right(m2);
        let union2 = m1.union_prefer_right(m2).remove(n);
        assert_maps_equal!(union1, union2);
        assume(equal(union1, union2));
        // TODO: verus bug? (uncomment assertions below)
        // substituting union1 and/or union2's definition makes the assertion fail:
        assert(equal(m1.remove(n).union_prefer_right(m2), union2));
        assert(equal(union1, m1.union_prefer_right(m2).remove(n)));
    });
}

@utaal fill in details

Use a visitor that doesn't require constructing an `Expr` when performing checks (and not mapping the AST)

Depends on #22 which contains an expression visitor that isn't also a mapper.

Especially in well_formed we're abusing map_expr_visitor (and similar): they require the mapper function to produce a new Expr, but when just performing checks by walking the AST this new Expr is just discarded.

Panics in bitvector reasoning

Came across two panics with bitvector reasoning.

This succeeds:

#[proof] #[verifier(bit_vector)]
fn f() {
    ensures(forall(|i: u64| i < 64 >>= ((1 as u64) << i > 0)));
}

This panics:

#[proof] #[verifier(bit_vector)]
fn f() {
    ensures(forall(|i: u64| ((1 as u64) << i > 0)));
}

thread 'rustc' panicked at 'internal error: generated ill-typed AIR code: error 'in call to has_type, argument #1 has type "BitVec64" when it should have type "Poly"' in expression '(has_type i@ (UINT 64))'', rust_verify/src/verifier.rs:354:21
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: aborting due to previous error

This succeeds:

#[proof] #[verifier(bit_vector)]
fn f() {
    ensures((1 as u64) << (1 as u64) > 0);
}

This panics:

#[proof] #[verifier(bit_vector)]
fn f() {
    ensures((1 as u64) << 1 > 0);
}

thread 'rustc' panicked at 'internal error: generated ill-typed AIR code: error 'error 'in call to <<, arguments should have the same width, but got 64 and 32' in expression '(bvshl #x0000000000000001 #x00000001)'' in expression '(bvugt (bvshl #x0000000000000001 #x00000001) #x0000000000000000)'', rust_verify/src/verifier.rs:354:21
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

ping @channy412

missing sanity checks in while loop header

Verus currently doesn't error on

    while i < 100 {
        requires([i == 5]);   // This line doesn't make sense here
        invariant([
            10 <= i,
            i <= 100,
            b1 as u64 == i * 2,
        ]);

Verus has a concept of a 'header' which has a bunch of different information. However, when we parse a while loop header, we don't check that it doesn't have any of the other information that isn't used.

I suspect it would make more sense to have two different Header types for function headers & invariant headers.

When fixed,

un-ignore test added in 3fd2346

Non-exhaustive match should not compile

un-ignore test 073e632

This:

        enum S {
            V1,
            V2,
        }

        fn f(s: S) {
            match s {
                S::V1 => assert(true),
            };
        }

is invalid Rust, https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=adda272ecc85b76b8fc40db2c8e028c3

but it succeeds in Verus.

We may also be relying on the check being in place, as the following fails too:

        #[is_variant]
        enum S {
            V1,
            V2,
        }

        fn f(s: S) {
            match s {
                S::V1 => assert(s.is_V1()),
            };
        }

Clarification on #[verifier(publish)]

Hi Verus team, I was writing some spec predicates like

pub struct ClusterState {
    ...
}

impl ClusterState {
    #[spec]
    pub fn empty(&self) -> bool {
        ... // check some fields in self
    }

    #[spec]
    pub fn well_formed(&self) -> bool {
        ... // check some fields in self
    }

    #[spec]
    pub fn trivially_true(&self) -> bool {
        true
    }
}

and I find that both empty and well_formed are always evaluated as false if I call them in another rust file, while trivially_true is sometimes true and sometimes false.

I find that #[verifier(publish)] is used in pervasive and guess that this might help. After adding this macro to each predicate they start to work properly in different rust files.

I am just wondering what is exactly the meaning of #[verifier(publish)]? And what will happen if we do not have this macro for a spec function?

`vector` and `seq` in pervasive : failing trigger for vector `set`'s properties and a trivial unsoundness bug

After calling set in prevasive/vec.rs(https://github.com/secure-foundations/verus/blob/main/source/pervasive/vec.rs#L28) , the below commented three properties are discovered through triggers in seq.rs(https://github.com/secure-foundations/verus/blob/main/source/pervasive/seq.rs#L93). During working on the bit-map example(445c6ce#diff-615c3ebc3c82354316137c5cbc27e219b3aca3447ea9ecfdc315b2f062d7c01dR123), I had to manually call one of those seq axioms. I wonder if it makes sense to add those properties as an axiom for vector's set function(as shown as below).

    #[verifier(external_body)]
    pub fn set(self, i: usize, a: A) -> Vec<A> {
        requires(i < self.view().len());
        ensures(|v2: Vec<A>| [
            equal(v2.view(), self.view().update(i, a)),
            // adding below three lines?
            //(1) self.len() == v2.len(),
            //(2) equal(v2.view().index(i), a),
            //(3) forall(|i2: int| i2 != i && i2 < self.view().len() >>= equal(v2.view().index(i2),self.view().index(i2))),
        ]);

        let mut v2 = self;
        v2.vec[i] = a;
        v2
    }

In the following function in seq.rs, i1 != i2, should be added in requires. Found this after suspiciously succeeding proof.
https://github.com/secure-foundations/verus/blob/main/source/pervasive/seq.rs#L112-L123

Integer overflow panics in debug mode but is allowed by the verifier

Integer overflow is defined to behave as follows by the currently adopted RFC 560 https://github.com/rust-lang/rfcs/blob/master/text/0560-integer-overflow.md

The operations +, -, *, can underflow and overflow. When checking is enabled this will panic. When checking is disabled this will two's complement wrap.

In modern rust, debug_assertions (which includes overflow checking) is enabled when compiling with the debug default configurations. In the release (optimized) default config, debug_assertions is disabled, and the overflowing operations will wrap.
Because of this, integer overflow is never undefined behavior[^1]. Note that this is different from the unchecked_* operations on integers, which are undefined behavior if they overflow, e.g. for u64::unchecked_add.

Verus currently admits overflowing operations which will panic when compiled with debug_assertions. This can be regarded as a soundness issue (verified code should not panic).

How to address this is still up for debate, but it may be worth noting that if we were to introduce verification conditions for integer operations that ensure there's no overflow, we could also replace the native operations with their unchecked_math counterparts, which (apparently) can use LLVM intrinsics that can be faster because they assume no overflow can occur.

/cc @Chris-Hawblitzel

issue with variable shadowing and &mut

seems to be some sort of problem with the following name-shadowing scenario:

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use pervasive::*;

fn foo(x: &mut u32) {
  ensures(equal(*x, *old(x)));
}

fn main() {
  let h = 5;

  let mut h = 6;
  foo(&mut h);

  assert(h == 5); // passes
  assert(h == 6); // fails
}

warning if the user attempts arithmetic with bounded int types in spec/proof

This is almost always a mistake - it's idiomatic to convert to an int first in spec code

Failing bit-vector example (weirdness in bit-vector, Z3)

Summarizing the discussion in the following thread (#43) :

This easy assertion fails
assert_bit_vector( (b1 == b2) || (b1 == b3) >>= (b1 | b2 | b3 == b2 | b3) );

The generated SMT file is attached below.
failing_bitvector.txt

The instability across Z3 versions seems a bit weird. This example works on older Z3 (4.4.1 and 4.8.5), but it timeout 60 seconds on versions 4.8.14(latest) and 4.8.6

Random-seed seems to have no effect in this example. (The above behavior is preserved regardless of the value of random-seed(0 to 99))

Newer versions work for u8, u16, but timeout 60 seconds on u32 and u64. Z3 could be brute-forcing on bits I think.

In the newer versions, when I remove push on line 3, it suddenly works again. This feels weird because push should not affect options in lines 1 and 2.

Also, when I comment out the following option, Z3 returns unsat instantly.
(set-option :smt.case_split 3)
Verus' default value for this option is 3. The above example works for 0,1,2,4,6 but not for 3,5.
(Information about Z3 options: https://github.com/Z3Prover/z3/blob/master/src/smt/params/smt_params_helper.pyg)

I tried manually changing the bvor encoding from binaryOp style to multiOp, ( using (bvor b1 b2 b3) instead of (bvor (bvor b1 b2) b3) ), but it still makes 60 seconds timeout.

For this issue, the current plan is to make a separate Z3 process for bit-vector reasoning (and non-linear arithmetic).

Function-check-recommends with bit-vector

After the below bit-vector example fails, the recommend re-run gives a type error. Variable declarations are in BitVec, while assumes are in integer.

Error msg:

thread 'rustc' panicked at 'internal error: generated ill-typed AIR code: error 'error 'error 'in call to I, argument #1 has type "BitVec64" when it should have type "Int"' in expression '(I bv_old@)'' in expression '(uintor 64 (I bv_old@) (I (uClip 64 (uintshl 64 (I 1) (I (uClip 64 index@))))))'' in expression '(uClip 64 (uintor 64 (I bv_old@) (I (uClip 64 (uintshl 64 (I 1) (I (uClip 64 index@)))))))'', rust_verify/src/verifier.rs:273:21

AIR log:

;; Function-Check-Recommends crate::set_bit64_proof
(set-option :smt.case_split 0)
(check-valid
 (declare-var bv_new@ (_ BitVec 64))
 (declare-var bv_old@ (_ BitVec 64))
 (declare-var index@ (_ BitVec 32))
 (declare-var bit@ Bool)
 (declare-var loc2@ (_ BitVec 32))
 (block
  (assume
   (= bv_new@ (ite
     bit@
     (uClip 64 (uintor 64 (I bv_old@) (I (uClip 64 (uintshl 64 (I 1) (I (uClip 64 index@)))))))
     (uClip 64 (uintand 64 (I bv_old@) (I (uClip 64 (uintnot 64 (I (uClip 64 (uintshl 64 (I 1)
             (I (uClip 64 index@))
  )))))))))))
  (assume
   (< index@ 64)
  )
  (assume
   (has_type loc2@ (UINT 32))
)))

Source code:

// a: bv, b: index
macro_rules! get_bit64{
    ($a:expr,$b:expr)=>{
        {
            (0x1u64 & ($a>>($b as u64))) == 1u64
        }
    }
}

// a: bv, b: index, c: bit
macro_rules! set_bit64{
    ($a:expr,$b:expr, $c:expr)=>{
        {
             if $c {$a | 1u64 << ($b as u64)}
             else {$a & (!(1u64 << ($b as u64)))}
        }
    }
}

#[verifier(bit_vector)]
#[proof]
fn set_bit64_proof(bv_new: u64, bv_old: u64, index: u32, bit: bool){
    requires([
        bv_new == set_bit64!(bv_old, index, bit),
        index < 64 ,
    ]);
    ensures([
        get_bit64!(bv_new, index) == bit,
        forall(|loc2:u32| (loc2 < 64 && loc2 != index) >>= (get_bit64!(bv_new, loc2) == get_bit64!(bv_old, loc2))),
    ]);
}

unstable bit-vector query
UPDATE: I misconstrued the smt.case_split option to have an immediate effect like smt.arith.nl. Please ignore the below.

The above example is part of https://github.com/secure-foundations/verus/blob/main/source/docs/bv_experiments/bitmap.rs.
This example used to go through(by manually setting smt.case_split to be zero), but now hits rlimit even with that option. I tried this example with rlimit=100, but it still fails after around 22 seconds.
Related issue: #49

Casting results in wrong output type emitted in air

Currently equality is only present for primitive types it seems, to get around this limitation I decided to represent an enum as u64 and simply cast as a u64 when needed. Unfortunately this results in a panic as the wrong air type is emitted, in this case "Colour" was emitted.

#[derive(Eq, PartialEq, Copy, Clone)]
#[repr(u64)]
pub enum Colour {
    Red = 1, 
    White = 2, 
    Blue = 3
}

spec fn below(c: Colour, d: Colour) -> bool {
    let c = c as u64;
    let d = d as u64;
    let red = Colour::Red as u64;
    let blue = Colour::Blue as u64;

    c == red || c == d || d == blue
}

I got around this limitation by having external_body functions that handled the conversion for me, but thought that I should perhaps note this issue.

ast_simplify doesn't respect evaluation order

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use pervasive::*;

struct Foo {
    pub a: bool,
    pub b: bool,
    pub c: bool,
}

fn do_mut(x: &mut u64) -> bool {
    ensures(|b: bool| *x == 19 && b == true);
    *x = 19;
    true
}

fn get_bool() -> bool {
    requires(false);
    false
}

fn same_foo(foo: Foo) -> Foo {
    foo
}

fn main() {
    let foo = Foo { a: false, b: false, c: false };

    let mut x = 5;

    let bar = Foo {
        a: do_mut(&mut x) || get_bool(),
        ..same_foo(foo)
    };
}

Here, we have:

error: precondition not satisfied
  --> l2.rs:33:30
   |
19 |     requires(false);
   |              ----- failed precondition
...
33 |         a: do_mut(&mut x) || get_bool(),
   |                              ^^^^^^^^^^

Note that do_mut returns true, so get_bool() should never be called; yet, the precondition fails.

Here's the relevant AIR (note that get_bool() is called before do_mut. This violates both short-circuiting and evaluation order.

;; Function-Def crate::main
 (check-valid
  (declare-const tmp%1@ Bool)
  (declare-const tmp%%2@ Bool)
  (declare-const tmp%%1@ Foo.)
  (declare-const foo@ Foo.)
  (declare-var x@ Int)
  (declare-const bar@ Foo.)
  (axiom fuel_defaults)
  (block
   (assume
    (= foo@ (Foo./Foo (%B (B false)) (%B (B false)) (%B (B false))))
   )
   (assume
    (= x@ 5)
   )
   (block
    (assert
     ("precondition not satisfied")
     (req%get_bool.)
   ))
   (block)
   (block
    (snapshot snap%CALL)
    (havoc x@)
    (assume
     (ens%do_mut. (old snap%CALL x@) x@ tmp%1@)
   ))
   (assume
    (= bar@ (Foo./Foo (%B (B (or
         tmp%1@
         tmp%%2@
       ))
      ) (%B (B (Foo./Foo/b (%Poly%Foo. (Poly%Foo. tmp%%1@))))) (%B (B (Foo./Foo/c (%Poly%Foo.
          (Poly%Foo. tmp%%1@)
 )))))))))

taking &mut of non-mut variable gives a panic instead of error

this:

fn m(v: &mut u64) {
}

fn main() {
    let v = 6;

    m(&mut v); 
}

I expect it to give the error cannot borrow v as mutable, as it is not declared as mutable

But it gives a panic instead:

Verifying root module
thread 'rustc' panicked at 'internal error: generated ill-typed AIR code: error 'cannot assign to const variable v@' in statement '(havoc v@)'', rust_verify/src/verifier.rs:162:21

I presume the problem is that our checking & VIR -> AIR conversion makes assumptions about the well-formedness of the rust code, while Rust's mut-checking takes place at a later stage.

in certain exit scenarios, verus hangs rather than exiting

I think this was probably caused by the recent change to the verus pipeline that move borrow-checking to be before verification.

erasure bug

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use pervasive::*;
use pervasive::modes::*;
use pervasive::option::*;

fn f<T>(t: Spec<Option<T>>) {
    #[spec] let x = t.value().get_Some_0();
}

fn main() {
}

gives this error:

thread 'rustc' panicked at 'internal error: MethodCall ResolvedCall', rust_verify/src/erase.rs:610:22

Different SMT files over executions of Verus - different trigger ordering, different number of check-sat

This GC example( f78bfcb ) is about using a 32-bit integer as an array of 16 elements. When I uncomment lines from 147 to 152, the verification result becomes unstable. Yi and I were looking into this example and found that Verus generates two different SMT files over separate runs. These SMT files have some different ordering of triggers and a different number of check-sat.
To be specific, in log_fail.smt file, when I manually flip the order of these two triggers(to make the ordering the same as in log_success.smt), Z3 suddenly returns unsat instead of unknown.

:pattern ((get_bit.? (I bv2@) loc2$))      ;; line 1971
:pattern ((get_bit.? (I bv@) loc2$))

Also, log_fail.smt has one more check-sat. Here is the diff of that part.

<   (get-model)                                        ;; line 2303
<   (assert
<    (not %%location_label%%0)
<   )
<   (assert
<    %%query%%
<   )
<   (set-option :rlimit 0)
<   (check-sat)
<   (set-option :rlimit 0)

Unmodified SMT files are log_success.smt and log_fail.smt
log_fail.txt
log_success.txt

I will try to make small examples that reproduce these two issues(different trigger ordering and a different number of check-sat) separately.

for exported fn, verus should check if pre/post-conditions are well-formed in export

currently, verus generates malformed air code if a pre-condition or post-condition references a fn which isn't public. it should generate a useful error message instead.

`reveal`/`reveal_with_fuel` require naming type arguments, which shouldn't be necessary

For

#[spec] #[verifier(publish)]
pub fn fold<E, F: Fn(E, A) -> E>(self, init: E, f: F) -> E {
  ... fold(expr)
}

one should be able to

reveal_with_fuel(fold, 10);

but we now require

reveal_with_fuel(fold::<nat, fn(nat,nat)->nat>, 10);

https://github.com/secure-foundations/verus/blob/9b0c1b884e4b89c59efaabcc6ae278cc32db9ef2/source/rust_verify/tests/sets.rs

panic on cycle of types (expected error without a panic)

I really don't know what's going on here... consider this code, which has a cycle of types, and should therefore be rejected:

#[allow(unused_imports)]
use builtin::*;

mod pervasive;
use pervasive::*;
use pervasive::modes::*;
use pervasive::option::*;
#[allow(unused_imports)]
use state_machines_macros::*;

pub struct X {
    pub t: X_Instance,
}

#[proof]
#[allow(non_camel_case_types)]
#[verifier(unforgeable)]
pub struct X_Instance {
    #[spec]
    state: X,
    #[spec]
    location: ::builtin::int,
}

impl X_Instance {
    #[proof]
    #[verifier(external_body)]
    #[verifier(returns(proof))]
    pub fn clone(#[proof] &self) -> Self {
        ensures(|s: Self| ::builtin::equal(*self, s));
        ::core::panicking::panic("not implemented");
    }
}
fn main() { }

Verus prints the following:

error[E0072]: recursive type `X` has infinite size
  --> o.rs:11:1
   |
11 | pub struct X {
   | ^^^^^^^^^^^^ recursive type has infinite size
12 |     pub t: X_Instance,
   |            ---------- recursive without indirection
   |
help: insert some indirection (e.g., a `Box`, `Rc`, or `&`) to make `X` representable
   |
12 |     pub t: Box<X_Instance>,
   |            ++++          +

error[E0072]: recursive type `X_Instance` has infinite size
  --> o.rs:18:1
   |
18 | pub struct X_Instance {
   | ^^^^^^^^^^^^^^^^^^^^^ recursive type has infinite size
19 |     #[spec]
20 |     state: X,
   |            - recursive without indirection
   |
help: insert some indirection (e.g., a `Box`, `Rc`, or `&`) to make `X_Instance` representable
   |
20 |     state: Box<X>,
   |            ++++ +

error[E0391]: cycle detected when computing drop-check constraints for `X_Instance`
  --> o.rs:18:1
   |
18 | pub struct X_Instance {
   | ^^^^^^^^^^^^^^^^^^^^^
   |
note: ...which requires computing drop-check constraints for `X`...
  --> o.rs:11:1
   |
11 | pub struct X {
   | ^^^^^^^^^^^^
   = note: ...which again requires computing drop-check constraints for `X_Instance`, completing the cycle
   = note: cycle used when computing dropck types for `Canonical { max_universe: U0, variables: [], value: ParamEnvAnd { param_env: ParamEnv { caller_bounds: [], reveal: UserFacing }, value: X_Instance } }`

error: aborting due to 3 previous errors; 3 warnings emitted

Some errors have detailed explanations: E0072, E0391.
For more information about an error, try `rustc --explain E0072`.
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: PoisonError { .. }', /Users/thance/verus/source/rust_verify/src/driver.rs:80:40
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::result::unwrap_failed
   3: core::result::Result<T,E>::unwrap
             at /Users/thance/verus/rust/library/core/src/result.rs:1295:23
   4: rust_verify::driver::run
             at ./rust_verify/src/driver.rs:80:24
   5: rust_verify::main
             at ./rust_verify/src/main.rs:46:30
   6: core::ops::function::FnOnce::call_once
             at /Users/thance/verus/rust/library/core/src/ops/function.rs:227:5
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

The error messages look correct, but the Verus driver panics for some reason.

Panic on equal

The following code panics:

#[allow(unused_imports)]
use builtin::*;

#[proof]
fn f() {
    equal(1 as nat, 1);
}

fn main() { }

fhs m: source 1 ν ./tools/rust-verify.sh /st/verus/test.rs
thread 'rustc' panicked at 'no entry found for key', rust_verify/src/erase.rs:373:14
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Trusted pervasive (vstd) types should be `: Structural`

Hi verus team, I was trying to check the equality of two structs that contain Option like this:

#[allow(unused_imports)]
use builtin_macros::*;
#[allow(unused_imports)]
use builtin::{ensures};

mod pervasive;
#[allow(unused_imports)]
use pervasive::{*, option::Option, map::*};

impl std::cmp::PartialEq for Option<u32> {
    #[verifier(external)]
    fn eq(&self, other: &Self) -> bool {
        match (self, other) {
            (Option::Some(a), Option::Some(b)) => a == b,
            (Option::None, Option::None) => true,
            _ => false,
        }
    }
}

impl std::cmp::Eq for Option<u32> {}

#[derive(Structural, PartialEq, Eq)]
pub struct MyStructA {
    pub content: Option<u32>,
}

fn MyFun() {
    let s1 = MyStructA{content:Option::Some(1)};
    let s2 = MyStructA{content:Option::Some(1)};
    assert(s1 == s2);
}

fn main() { }

However, verus reports the error:

error[E0277]: the trait bound `pervasive::option::Option<u32>: builtin::Structural` is not satisfied
   --> rust_verify/example/myexample.rs:23:10
    |
23  | #[derive(Structural, PartialEq, Eq)]
    |          ^^^^^^^^^^ the trait `builtin::Structural` is not implemented for `pervasive::option::Option<u32>`
    |
note: required by a bound in `builtin::AssertParamIsStructural`
   --> /Users/xudongs/verus/source/builtin/src/lib.rs:328:39
    |
328 | pub struct AssertParamIsStructural<T: Structural + ?Sized> {
    |                                       ^^^^^^^^^^ required by this bound in `builtin::AssertParamIsStructural`
    = note: this error originates in the derive macro `Structural` (in Nightly builds, run with -Z macro-backtrace for more info)

error: aborting due to previous error

For more information about this error, try `rustc --explain E0277`.
verification results:: verified: 0 errors: 0

My understanding about the equality check is:

#[derive(Structural)] is necessary for the struct we want to check equality for
if the struct has #[derive(Structural)], every field in this struct has to have #[derive(Structural)] as well

If both 1 and 2 are true, what would be the best way to check the equality of a struct that contains Option fields?

Panic with triggers in blocks

Found with @matthias-brun.

un-ignore the regression test 4b9ab27 when this is fixed

This

        use seq::*;

        struct Node {
            base_v: nat,
            values: Seq<nat>,
            nodes: Seq<Box<Node>>,
        }

        impl Node {
            #[spec] fn inv(&self) -> bool {
                forall(|i: nat, j: nat| (i < self.nodes.len() && j < self.nodes.index(i).values.len()) >>= {
                    let values = #[trigger] self.nodes.index(i).values;
                    self.base_v <= #[trigger] values.index(j)
                })
            }
        }

panics with an AIR error:

internal error: ill-typed AIR code: error 'error 'error 'error 'use of undeclared variable values$' in expression 'values$'' in expression '(Poly%pervasive.seq.Seq<nat.>. values$)'' in expression '(pervasive.seq.Seq.index.? NAT (Poly%pervasive.seq.Seq<nat.>. values$) j$)'' in expression '(=>
 (fuel_bool fuel%Node.inv.)
 (forall ((self@ Poly)) (!
   (= (Node.inv.? self@) (forall ((i$ Poly) (j$ Poly)) (!
      (=>
       (and
        (has_type i$ NAT)
        (has_type j$ NAT)
       )
       (=>
        (and
         (< (%I i$) (pervasive.seq.Seq.len.? TYPE%Node. (Poly%pervasive.seq.Seq<Node.>. (Node./Node/nodes
             (%Poly%Node. self@)
         ))))
         (< (%I j$) (pervasive.seq.Seq.len.? NAT (Poly%pervasive.seq.Seq<nat.>. (Node./Node/values
             (%Poly%Node. (pervasive.seq.Seq.index.? TYPE%Node. (Poly%pervasive.seq.Seq<Node.>. (
                 Node./Node/nodes (%Poly%Node. self@)
                )
               ) i$
        )))))))
        (let
         ((values$ (Node./Node/values (%Poly%Node. (pervasive.seq.Seq.index.? TYPE%Node. (Poly%pervasive.seq.Seq<Node.>.
               (Node./Node/nodes (%Poly%Node. self@))
              ) i$
         )))))
         (<= (Node./Node/base_v (%Poly%Node. self@)) (%I (pervasive.seq.Seq.index.? NAT (Poly%pervasive.seq.Seq<nat.>.
             values$
            ) j$
      ))))))
      :pattern ((Node./Node/values (%Poly%Node. (pervasive.seq.Seq.index.? TYPE%Node. (Poly%pervasive.seq.Seq<Node.>.
           (Node./Node/nodes (%Poly%Node. self@))
          ) i$
        ))
       ) (pervasive.seq.Seq.index.? NAT (Poly%pervasive.seq.Seq<nat.>. values$) j$)
   ))))
   :pattern ((Node.inv.? self@))
)))'', rust_verify/src/verifier.rs:152:17

Questions on set equality check

Hi Verus team,

We encountered some problems when checking the equality of set:

    #[spec] let s1: Set<i32> = Set::empty().insert(1);
    #[spec] let s2: Set<i32> = Set::empty();
    assert(!equal(s1, s2));

The assertion fails though s1 and s2 are not the same.
If we change assert(!equal(s1, s2)); to assert(equal(s1, s2));, the assertion still fails.
Is it expected behavior or a bug?
(BTW, if I add assert(!s2.contains(1)); before the last assertion then it will pass.)

This concerns us because we have some predicates like

#[spec] #[verifier(publish)]
pub fn next(s1: Set, s2: Set, v, ...) -> bool {
    ...
    && equal(s1.insert(v), s2)
}

And we want to prove that exists some s1, s2 so that next(...) is true. If Verus cannot tell whether two sets are equal or not, is it possible that the exists is always false even if there actually are some s1 and s2 which make next() true?

Panic when external items are referenced in verified code

This code verifies fine:

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use pervasive::vec::*;

fn f(s: Vec<u64>) { }

fn main() {}

But if the vec import is missing, the verifier panics:

#[allow(unused_imports)]
use builtin::*;
mod pervasive;

fn f(s: Vec<u64>) { }

fn main() {}

fhs m: source ν ./tools/rust-verify.sh /st/verus/panic.rs
Verifying root module
thread 'rustc' panicked at 'no entry found for key', vir/src/poly.rs:151:16
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'main' panicked at 'valid Mutex for verifier: PoisonError { .. }', /home/m/verus/source/rust_verify/src/driver.rs:120:10

This isn't specific to Vec, the same happens for other imports.

Erasing self of proof fns results in nonsensical calls

Un-ignore f6026d1 when this is fixed

    #[proof]
    struct Node {
        v: nat,
    }

    struct Token {}

    impl Node {
        #[proof]
        fn lemma(self, #[proof] t: Token) {}

        #[proof]
        fn other(self, #[proof] t: Token) {
            self.lemma(t);
            self.lemma(t);
        }
    }

fails with

error[E0599]: no method named `lemma` found for struct `Token` in the current scope
  --> test.rs:22:14
   |
13 | struct Token {}
   | ------------ method `lemma` not found for this
...
22 |         self.lemma(t);
   |              ^^^^^ method not found in `Token`

because we erased the receiver!

Question about implementing a Map-like struct for exec mode

According to #167, I was trying to implement a Map-like struct for exec mode. I checked how vec is implemented and was trying to implement a dict as a wrapper around std::HashMap. However, when I define the dict struct with generics, it seems that I cannot specify bounds. More details below:

xudongs@xudongs-a01:~/verus/source:$ cat rust_verify/example/myexample.rs                   
#[verifier(external_body)]
pub struct Dict<#[verifier(maybe_negative)] K: std::cmp::Eq + std::hash::Hash, #[verifier(strictly_positive)] V> 
{
    pub dict: std::collections::HashMap<K, V>,
}

fn main() { }

xudongs@xudongs-a01:~/verus/source:$ ./tools/rust-verify.sh rust_verify/example/myexample.rs
error: not yet supported: bounds on datatype parameters
  --> rust_verify/example/myexample.rs:21:1
   |
21 | / pub struct Dict<#[verifier(maybe_negative)] K: std::cmp::Eq + std::hash::Hash, #[verifier(strictly_pos...
22 | | {
23 | |     pub dict: std::collections::HashMap<K, V>,
24 | | }
   | |_^

error: aborting due to previous error

I have also tried to use where clause to specify bounds but where is not supported as well.

Could you please let me know what is the best way for me to specify bounds since it is necessary to implement a wrapper around HashMap? If this can work I am happy to implement a dict for exec mode and send a PR if it is needed.

`unknown` for a very simple failing assertion

After running Verus with the below example, Z3 gives unknown with (:reason-unknown "(incomplete quantifiers)"). I am wondering if this behavior is expected.

fn test_n(n: nat) {
    assert(n >= 5);      // FAILS
}

I expected to see sat for this example but I was a bit surprised to see unknown.
@jaybosamiya and I looked into the prelude a bit and found the prelude itself ends in unknown. There are several axioms that give unknown itself. For example, the first assert in the prelude also gives unknown.

;; ... 
;; set-option & declaration 
;; ...

(assert
 (=>
  fuel_defaults
  (forall ((id FuelId)) (!
    (= (fuel_bool id) (fuel_bool_default id))
    :pattern ((fuel_bool id))
))))
(check-sat)      ;; this gives unknown

toolchain file to require nightly

Hello,

Building fails with (current) stable Rust. Instead of forcing people to switch globally to nightly, may I suggest https://rust-lang.github.io/rustup/overrides.html#the-toolchain-file.

Even better, rather than specifying nightly, you may want to develop with nightly but publish it with a fixed date-based nightly, so any errors reported by users are easier to reproduce.

Hi Andrea,

Thank you for your talk at Rust Dublin.

yet more erasure bugs

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use crate::pervasive::{*, option::*};

#[proof]
fn foo() { 
    let update_tmp_opt: Option<int> = Option::None;

    let update_tmp_opt: Option<int> =
                (if (Option::<int>::None).is_Some() {
                     Option::None
                 } else { update_tmp_opt });
}

fn main() {
}

error[E0308]: `if` and `else` have incompatible types
  --> moo.rs:13:25
   |
11 |                 (if (Option::<int>::None).is_Some() {
   |                 ----------------------------------- `if` and `else` have incompatible types
12 |                      Option::None
   |                      ------------ expected because of this
13 |                  } else { update_tmp_opt });
   |                         ^^^^^^^^^^^^^^^^^^ expected enum `pervasive::option::Option`, found `()`
   |
   = note:   expected type `pervasive::option::Option<_>`
           found unit type `()`

error: aborting due to previous error; 1 warning emitted

Here's a version in exec-mode:

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use crate::pervasive::{*, option::*};

#[exec]
fn foo() { 
    let update_tmp_opt: Option<int> = Option::None;

    let update_tmp_opt: Option<int> =
                (if (Option::<int>::None).is_Some() {
                     Option::None
                 } else { update_tmp_opt });
}

fn main() {
}

thread 'rustc' panicked at 'erase_expr', rust_verify/src/erase.rs:724:35

The errors are different for both ... not sure if it's the same root cause.

verus doesn't handle negative integer literals properly

For example, Verus currently encodes the i64 value -0x8000_0000_0000_0000 as:

(- 0 (iClip 64 9223372036854775808)

assertion failure involving &mut argument and pattern-assignment

Not sure what's going on here. It seems to induce the failure, we need both components: the &mut argument and the destructuring of the return value.

#[allow(unused_imports)] use builtin::*;
#[allow(unused_imports)] use builtin_macros::*;
mod pervasive;
#[allow(unused_imports)] use crate::pervasive::*;

#[proof]
#[verifier(external_body)]
#[verifier(returns(proof))]
fn foo(#[proof] x: &mut int) -> (int, int)
{
    ensures(|ret: (int, int)|
        { let (a, b) = ret;
            a + b == (*x)
        }
    );

    unimplemented!();
}

fn bar(#[proof] x: int) {
    #[proof] let mut x = x;
    #[proof] let (a, b) = foo(&mut x);
    assert(a + b == x); // THIS LINE FAILS
}

fn main() { }

Verus demands `let mut` where Rust does not

If you create a variable and leave off the initializer, and declare it later,

let x: type;
// ...
x = ...;

then Rust doesn't require a mut on the declaration. However, Verus currently requires it (see the "variable must be declared 'mut' to allow assignment" error in vir/src/modes.rs)

introduction of temp variable causes flakiness

Below, dec_to_zero_asserts and dec_to_zero_asserts2 are almost the same, except that one uses a tmp variable assignment. However, only one of them passes. (Interestingly, the line that passes or fail is earlier than the changed line, but since it's all one query, this isn't too surprising.)

(This is macro-generated code, by the way, if you're wondering why it looks a little weird - the reason this came up is that I was trying to introduce temp variables in the generated code.)

#[allow(unused_imports)]
use builtin::*;
mod pervasive;
use pervasive::*;
use pervasive::modes::*;
use pervasive::option::*;

pub struct RefCounter<#[verifier(maybe_negative)] T> {
    pub counter: nat,
    pub storage: crate::pervasive::option::Option<T>,
    pub reader: crate::pervasive::multiset::Multiset<T>,
}

impl<#[verifier(maybe_negative)] T> RefCounter<T> {
    #[spec]
    pub fn invariant(&self) -> ::std::primitive::bool {
        self.reader_agrees_storage()
            && self.counter_agrees_storage()
            && self.counter_agrees_storage_rev()
            && self.counter_agrees_reader_count()
    }
    #[spec]
    fn reader_agrees_storage(&self) -> bool {
        forall(|t: T| self.reader.count(t) > 0 >>= equal(self.storage, Option::Some(t)))
    }
    #[spec]
    fn counter_agrees_storage(&self) -> bool {
        self.counter == 0 >>= self.storage.is_None()
    }
    #[spec]
    fn counter_agrees_storage_rev(&self) -> bool {
        self.storage.is_None() >>= self.counter == 0
    }
    #[spec]
    fn counter_agrees_reader_count(&self) -> bool {
        self.storage.is_Some() >>= self.reader.count(self.storage.get_Some_0()) == self.counter
    }

    #[proof]
    pub fn dec_to_zero_asserts(self: RefCounter<T>, x: T) {
        crate::pervasive::assume(self.invariant());
        {
            crate::pervasive::assume((self.reader).count(x) >= 1);
            crate::pervasive::assume(self.counter < 2);
            crate::pervasive::assert(self.counter == 1); // THIS FAILS

            let update_tmp_0 = x;
            crate::pervasive::assert(::builtin::equal(
                self.storage,
                crate::pervasive::option::Option::Some(update_tmp_0),
            ));
        }
    }

    #[proof]
    pub fn dec_to_zero_asserts2(self: RefCounter<T>, x: T) {
        crate::pervasive::assume(self.invariant());
        crate::pervasive::assume((self.reader).count(x) >= 1);
        crate::pervasive::assume(self.counter < 2);
        crate::pervasive::assert(self.counter == 1); // THIS PASSES
        crate::pervasive::assert(::builtin::equal(
            self.storage,
            crate::pervasive::option::Option::Some(x),
        ));
    }
}

fn main() { }

Bad error message when referencing a type outside the current crate in a struct definition

pub struct String {
    inner: std::string::String,
}

thread 'rustc' panicked at 'no entry found for key', vir/src/recursive_types.rs:25:21

We should tell the user that they cannot use types outside the crate for this case too.

Panic when using `#[derive(Hash)]` for enum

I found that verus panicked when running against the following program:

xudongs@xudongs-a01:~/verus/source:$ cat rust_verify/example/myexample.rs                   
#[derive(Hash)]
pub enum StringL {
    Str1,
    Str2,
}

fn main() { }

xudongs@xudongs-a01:~/verus/source:$ ./tools/rust-verify.sh rust_verify/example/myexample.rs
thread 'rustc' panicked at 'no entry found for key', vir/src/well_formed.rs:25:22
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: PoisonError { .. }', /Users/xudongs/verus/source/rust_verify/src/driver.rs:80:40

If we remove Hash or replace it with Eq or other bounds, verus will not panic.

Update triggers info message

The triggers info message:

note: Verus printed one or more automatically chosen quantifier triggers
      because it had low confidence in the chosen triggers.
      To suppress these messages, do one of the following:
        (1) manually annotate a single desired trigger using #[trigger]
            (example: forall(|i: int, j: int| f(i) && #[trigger] g(i) && #[trigger] h(j))),
        (2) manually annotate multiple desired triggers using with_triggers
            (example: forall(|i: int| with_triggers!([f(i)], [g(i)] => f(i) && g(i)))),
        (3) accept the automatically chosen trigger using #[auto_trigger]
            (example: forall(|i: int, j: int| #[auto_trigger] f(i) && g(i) && h(j)))
        (4) use the --triggers-silent command-line option to suppress all printing of triggers.
      (Note: triggers are used by the underlying SMT theorem prover to instantiate quantifiers;
      the theorem prover instantiates a quantifier whenever some expression matches the
      pattern specified by one of the quantifier's triggers.)

refers in part to the old with_triggers syntax, with_triggers!([f(i)], [g(i)] => f(i) && g(i)).

verus-lang / verus Goto Github PK

verus's People

Contributors

Stargazers

Watchers

Forkers

verus's Issues

Recommend Projects

Recommend Topics

Recommend Org