What's the best practice to combine verified code and original rust code?

[HaoYang670]

Hi,

We have a rust project maintained and we'd like to try verus to replace some runtime test.
However, we don't want to refactor the whole project, instead we want to get a taste from simple util functions.

Is it achievable?

[utaal]

Hi,
Making it easier to mix Verus and regular Rust code is something that we have been working on, and there is a PR (#733) that will be merged soon (by @hayley-leblanc and @Chris-Hawblitzel) that will make it easier.

Do these utility functions that you want to try out have any (Cargo) dependencies? If they don't have any dependencies, and once the #733 is merged, you should be able to move these simple functions to a separate crate that you verify with Verus and that you can use as a regular cargo dependency.

When built outside Verus, the verus! macro will erase all Verus-specific code and leave you with a regular Rust interface that you can call into from your rust project.

[HaoYang670]

Thanks @utaal.

Do these utility functions that you want to try out have any (Cargo) dependencies?

Those utils arr not depended on any 3rd party crate and they are all pure functions (no side effect).

you should be able to move these simple functions to a separate crate
Hmm. Separating them into a new crate maybe not what we expect. Is it possible to have mod-gain control?

[hayley-leblanc]

I just ran a quick test to see if the changes in PR #733 support verifying code in a module with unverified code in the same crate. This wasn't one of our goals and we hadn't previously tested it, but there is some limited support for this.

Verus has a --verify-module option that can verify individual modules which may do what you want, but if unverified sections contain features/syntax that is not supported by Verus, --verify-module will still not work. E.g., the code at this playground link https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=02a1a4fc4872e4a8db021fe478048d2d verifies with --verify-module test_mod (note that it does not verify at the provided link as the Verus playground does not provide the option to use that flag and callers do not prove that they satisfy the preconditions of the verified functions). However, if we uncomment the printlns in main() , the code will not verify (regardless of whether we use --verify-module) because the printlns do an implicit pointer cast which is not supported in Verus.

[HaoYang670]

Thanks @hayley-leblanc, glad to know that, I will have a try.

I think it would be better if the verus macro could work like the unsafe{...}, which we just need to block the code we want to verify.

[Chris-Hawblitzel]

@HaoYang670 The new pull request #771 adds an --external-by-default flag that may give you what you're looking for.

[utaal-b]

@HaoYang670 I am going to close this as potentially resolved by #771, but feel free to re-open if you have further questions.