Remote verification server

[romac]

Let's investigate what a remote verification server would look like.

1. Set up a container-based Inox server with a shared verification cache
2. Add a --remote-server=URL flag to Stainless to instruct it to send the VCs to the remote server.
3. ???
4. Profit!

The verification cache could just a be a key-value store from the serialized VC hash (eg. SHA-3) to the the serialized VCResult.

Whenever the server at the given URL receives a VC to verify:

1. It looks in the cache to see whether or not this VC has already been verified, and sends back the result if it has.
2. It spawns a new container containing an instance of Inox, and sends it the VC to verify, eg. over HTTP (I have a branch of Inox somewhere which adds a --server mode which listens for connections over HTTP, though it currently only handles TIP input).
3. It then store the result of the verification in the VC cache and sends back the result.

[vkuncak]

Following what was done for https://github.com/epfl-lara/rust-stainless/ and watch mode, it may be even more convenient to make the entire Stainless work as a server.

[vkuncak]

Indeed, we should enable stainless to run in such a "deamon mode" where it starts up and receives requests for more programs to check. This is rather similar to watch mode but accepts different files. It is related to the functionality in the equivalence checker. It would avoid startup times across different programs. It would also improve performance of a stainless as a service.

What I have in mind was in fact working on serialized xlang trees generated by a prototype Rust front end developed by Georg Schmid and Yann Bolliger:

https://github.com/epfl-lara/stainless/commit/1ea2e5adefb4ad917d2f8f5804d68ce31508838a

from

https://github.com/epfl-lara/stainless/compare/rust-interop

[vkuncak]

See also: https://github.com/samuelchassot/Stainless-codespaces