More features in exec_spec! and introduce exec_spec_trusted!

[zero-to-nat]

Additions to exec_spec!

• quantifiers
  • guard exprs can now have < and <= for both lower and upper bound
• Compilation of structs and enums
  • add impl of ExecSpecEq
  • add #[derive(Eq, Hash, PartialEq)] in order to ensure compatibility with HashMap, HashSet, ExecMultiset
• More Seq functions*
  • add, push, update, subrange, empty, to_multiset, drop_first, drop_last, take, skip, last, first, is_prefix_of, is_suffix_of, contains, index_of, index_of_first, index_of_last
• Map<K, V> compiles to HashMap<K, V>, with support for these functions:
  • equality, len, indexing**, empty, dom, insert, remove, get
• Set<T> compiles to HashSet<T>, with support these functions:
  • equality, len, empty, contains, insert, remove, union, intersect, difference
• Multiset<T> compiles to (new type) ExecMultiset<T>, with support for these functions:
  • equality, len, count, empty, singleton, add, sub
• More Option functions
  • unwrap
• More informative errors: supported types, expected quantifier format

Modifications for exec_spec_trusted! mode only

• all function signatures are marked with #[verifier::external_body]
• multivariable quantifiers are supported in this mode only. The current code does not attempt to generate loop invariants or triggers for quantifiers with multiple variables
• quantifiers over char. My implementation uses char::from_u32, for which Verus does not currently have a spec

*Function support: many of the new and existing spec-to-exec translations for supported functions on vstd types are marked external_body. Some cases are due to the use of iterators, and other cases due to a nontrivial proof (e.g. see my note for Map). We should perhaps update the documentation to state that many translations are trusted.

**Map indexing: indexing is only supported on Map<K, V> where K is a primitive type (e.g. usize). I couldn't get the conversion between ref and owned types to work correctly for more complex types.

View and DeepView for HashMap and HashSet: The impls for these traits were moved into vstd/view.rs to resolve issues with building without Verus. This follows analogous changes in #1140 and #1827.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[zhengyao-lin]

Thanks for these significant functionality and usability improvements to the macro! I only have some minor refactoring suggestions.

[zhengyao-lin]

I wonder if we should toggle trusted/verified using an attribute on the function itself (instead of having two macros), since they behave the same on structs/enums.

[zero-to-nat]

This is a good point. Since the trusted mode currently supports more Verus features than the untrusted mode, I would be somewhat inclined towards keeping them separate macros, in order to emphasize the differences between them.

FWIW, it appears that users can add some definitions within exec_spec! and use them within exec_spec_trusted!. I added a unit test for this scenario.

@parno, would you have any opinions on this?

[parno]

I think my top-level concern is that it should be clear at the source level how much trust these macros require. For example, I don't like the idea that, say, exec_spec(true) would mean trusted and exec_spec(false) would mean untrusted, since a reader/reviewer won't immediately know what that means. I could switching to a derive macro style, where there's a derive(ExecSpec) for datatypes, and a derive(ExecSpecTrusted) and derive(ExecSpecUntrusted) for functions, though even there, it might be confusing as to whether derive(ExecSpec) is trusted or untrusted.

[zero-to-nat]

In that case, perhaps it is cleaner to stick with the current macro approach. Would you prefer that we rename exec_spec! to exec_spec_untrusted!?

[zhengyao-lin]

Sounds good. Regarding naming, exec_spec_unverified might be more intuitive?

[parno]

Thanks for all of the hard work you've put into this! This is a very nice expansion of both the functionality and the usability of exec_spec.

I think we should also update the documentation for exec_spec to clarify what parts are actually verified. Right now, I think the docs make it seem like all of the generated code is verified, but some of it depends on external_body functions, which isn't as strong of a guarantee.

[parno]

The double negative in the first sentence is a bit confusing. Can we rephrase it?

Also, this bit "Instead, the code generated by the macro" is ambiguous w.r.t. which macro it is referring to.

[zero-to-nat]

Thanks for the feedback! I tried to make the wording clearer.

[zero-to-nat]

Thanks for all of the hard work you've put into this! This is a very nice expansion of both the functionality and the usability of exec_spec.

I think we should also update the documentation for exec_spec to clarify what parts are actually verified. Right now, I think the docs make it seem like all of the generated code is verified, but some of it depends on external_body functions, which isn't as strong of a guarantee.

Thank you for the comments @parno!

I have updated the guide documentation to make explicit exactly which vstd functions have trusted translations to exec code.

Also, upon reflection, I think that it does not make sense to add pre- and postconditions to functions compiled by exec_spec_trusted!. I believe the intention is that such code should not be used in verified projects, and so it should not have specs. I removed this part of the macro, but let me know if you have any further thoughts on this.