Aurea

We'll probably soon get some merge conflicts in `prusti-server` since Cedric and Joseph will be finishing the IDE improvements project soon.

The eventual syntax will be `closure!( #[requires(..)] |..| .. )` to match method annotations. However, the various closure features are still put on hold and I'm not sure I'll get...

I don't think we have tried the `install` command yet. Maybe this would run into issues with the Prusti binary not being able to determine the location of the downloaded...

This is similar to #1202, and the fix should be the same (#1269).

Using specifications within trait `impl` blocks requires that you annotate the `impl` block with `#[refine_trait_spec]`. This is not yet documented, but [will be](https://github.com/viperproject/prusti-dev/blob/f72f63176b82b1940042d05a651b260be6e75104/docs/user-guide/src/verify/impl_block_specs.md).

Sorry for the delay in responding! There is no core limitation here, just various bits and pieces that are not done "yet". I'll start with providing the modified file that...

> Once this PR has laid the ground-work for adding specs to the Rust standard library, how hard/easy would it be for an advanced end-user to contribute standard library specs...

We should report a better error for this, but the problem is with the specification. In the postcondition (in the first snippet), the expression `x` does not make sense, because...

But IIUC this is not good to do for the test suite in general, since it would not share the same server for all the tests and so reduce performance,...

The main motivation for `refine_spec` was for extern specs (see usage in #1249), which are trusted. Checking a `refine_spec` attached to a function with an implementation is difficult: in the...