Requests for commonly used rust/cargo

[panda2134]

This discussion collects a list of rust language features frequently used in coding, yet unsupported by verus.

[panda2134]

Verification on explicit type conversion is not supported

In rust language, From and Into traits are used to implement type conversion. Usually, the user only implements the From trait, and the rust compiler calls it whenever a .into() is called.

However, the verus compiler cannot correctly handle these two traits. A minimal example is provided below:

use vstd::prelude::*;
use vstd::string::new_strlit;

verus! {
    #[repr(u8)]
    #[derive(Debug, PartialEq, Eq)]
    pub enum FileType {
        Dir = 1,
        File = 2,
    }
    
    impl From<u32> for FileType {
        #[verifier(external_body)]
        fn from(val: u32) -> Self {
            match val {
                1 => FileType::Dir,
                2 => FileType::File,
                _ => panic!("Invalid file type"),
            }
        }
    }
    
    impl From<FileType> for u32 {
        #[verifier(external_body)]
        fn from(val: FileType) -> Self {
            match val {
                FileType::Dir => 1,
                FileType::File => 2,
            }
        }
    }

    fn main() {
        let val = FileType::Dir;
        let t: u32 = val.into();
        assert(t >= 1 && t <= 2);
    }
}

When one attempts to verify the file with verus, the following error is generated, indicating that verus does not correctly handle val.into():

error: `core::convert::impl&%3::into` is not supported (note: you may be able to add a Verus specification to this function with the `external_fn_specification` attribute) (note: the vstd library provides some specification for the Rust std library, but it is currently limited)
  --> 1.rs:35:22
   |
35 |         let t: u32 = val.into();
   |                      ^^^^^^^^^^

[panda2134]

Vector literal is not supported

It is common in rust code that a vector is define with macros. For instance, vec![3, 4, 5] defines a vector with three i32 elements. This is not properly supported with verus. Consider the following code:

use vstd::prelude::*;
use vstd::std_specs::core;

verus! {

    fn main() {
        let v = vec![1, 2, 3];
    }
}

For this file, verus halts with the following error:

error: The verifier does not yet support the following Rust feature:
unsizing operation from `std::boxed::Box<[i32; 3]>` to `std::boxed::Box<[i32]>`

[utaal]

Note: vec![1, 2, 3] desugars into Box::new([1, 2, 3]).to_vec() (or something like that).

[panda2134]

Integration with cargo

It would be better if we can add some documentation on using verus with cargo, so cargo can add all build arguments about dependencies to the verus call. This seems to be doable with [custom toolchains](https://rust-lang.github.io/rustup/concepts/toolchains.html#custom-toolchains), but we need better documentation about this.

If we look into [source code of rustup](https://github.com/rust-lang/rustup/blob/2a5a69e0914ff419554d684ca71eb1d72c72bcb3/src/cli/rustup_mode.rs#L1240), we can note that a valid rust toolchain only requires the lib/ directory, and the rustc compiler bin/rustc. Maybe we can make a toolchain that includes verus as the "rustc". By switching to this toolchain, the user can then use verus to verify and compile a cargo project.

[utaal]

Basic vstd functions for (debug) printing in verified code

println! and friends are not supported in verified code yet. We can provide simpler, trusted alternatives for those for now.
As requested by @panda2134.