Also comment out a line that crashes when not run from the same
directory. This was problematic for working with Prusti Assistant.

Ported change from PR viperproject#1334

Port basic functionality for the new prusti-server work flow according
to PR viperproject#1334 .

Querying signatures, spans of call contract collection and call finding
does not work yet.
PR: viperproject#1334

Defpath only verification does not work since test_entrypoint currently
just puts the entire program into the request regardless of the
verification tasks at hand.
Update the flags in the documentation.
PR: viperproject#1334

Requires the viperserver backend to support these messages too.

Every body owner function that is not passed to be verified explicitly
acts as though it were pure and trusted to skip the encoding of their
bodies.
Additionally, VERIFY_ONLY_DEFPATH now takes a vector of String instead
of just a string.

`SpanOfCallContracts` now has a vector as it's `call_spans` field so
only one object is created per function definition rather than one per
call.
`CallSpanFinder` now also collects local functions for call contract
span emission. Functions that are never called need not be emitted.

A main goal here is that the vir-viper translation happens on the same
thread that encodes the program in the local verification case. This
should happen so the allocated arena, which is thread local, can be
used.
Additionally, the JVM reliant bits are a bit more hidden from the
general procedure.

* Impure generics

* Fixed bug due to type parameters not being encoded

* Remove fractional perm

* mk_bool doesn't need extra typarams

* domain fields don't need a full encoding of their type yet

* type alias for do_encode_full result

* parameterise TaskEncoderDependencies by the owning encoder

* remove some dependency unwraps

* remove 'tcx lifetime, use 'vir

* check for cycles when requesting dependencies or emitting output ref

* add try operators for some emit output refs

Move backtranslation to where server messages are processed.
Move `EncodingInfo` to encoder crate.

- The viper program is now sent using a `GlobalRef`, so it actually
compiles.
- Cache usage no longer involves the `VerificationRequestProcessing`
object.
- The cache is now lazy, therefore only loads if the `ENABLE_CACHE` flag
  is set.
- The `VerificationRequestProcessing` object is no longer constructed
  when all the requests are cache hits. The thread it holds is also not
spawned as a result.

Also change backtranslation of viper identifiers.
Note that caching may not work properly for now if the
`GENERATE_VIPER_MESSAGES` flag is set. Fixing this is a WIP.

… rewrite-2023-assistant-features

Also clean up some imports.

The same error with different positions used to produce the same hashes
(generated using java's `hashCode` function).

This previously made it impossible to selectively verify in single file
programs. It still does not work when running through x.py.

This reverts commit f3cf4ef.