Add support for serializing / deserializing SAW core modules to/from disk

[eddywestbrook]

It would be really helpful if we could take an entire SAW core module and write it out to disk, to "freeze" it, in order to save progress in the middle of a long proof. This sort of feature could also have other uses; e.g., it could allow multiple different verification processes to run in parallel, in different instances of SAW, and then have all the results be loaded by future tasks that rely on those results.

[brianhuffman]

I don't think there's anything inherently hard about doing this. But before we can really get started on implementing it, we need to figure out exactly how we want it to work.

First, we need a way to specify exactly what gets exported: Do we want to dump the entire environment of every known definition and declaration in the current SharedContext? Probably the user should be able to specify some subset of the known declarations.

Also, should we take a transitive closure of dependencies for exported definitions, or should we omit certain low-level definitions from the export? For example, if we have a bunch of saw-core constants defined in terms of other constants that are defined in the saw-core prelude, we don't necessarily want to export all the contents of the saw-core prelude at the same time.

On the import side, we have some other decisions to make too. If you export a saw-core module that includes definitions of constants and datatypes, and then you import that module back in, should it always redefine fresh copies of everything that was imported? Or, if one or more of the imported declarations is already present in the current SharedContext, should it re-use the already-existing constants and types of the same names? But then, what if something of the same name exists, but it doesn't have exactly the same definition? Should we make a fresh, separate copy in that case, or re-use the similarly-named-but-different constant?

[eddywestbrook]

In response to @brianhuffman: Here is how I was imagining this would work, as a starting point, but please point out any problems!

The point of making this export / import per-module is so that we can use SAW modules as a convenient way to specify what definitions actually need to get serialized / deserialized. The idea would be that each SAW “session” would make its own SAW core module, which would keep all of the definitions, proofs, axioms, etc., that were created in that session. Those objects in the session module would be the objects that would be serialized. Any objects not created in that session would be objects in one of the preludes, which have already been pre-loaded into SAW, and so shouldn’t be serialized.

If you then have session 2 that depends on objects from session 1, then session 2 has to import the module that was created for session 1. When you serialize session 2, you only serialize its module, not that of session 1, because you have already serialized session 1 to a different file. This sort of separation is important when you have import diamonds, as in having sessions 2 and 3 independently relying on session 1, and session 4 then relying on both 2 and 3. We want session 4 to be able to import both 2 and 3 but have them both rely on a single import of 1, and not import 1 twice.

It might be nice to have syntax to start a new session that depends on a set of serialized former sessions. It might also be nice to store in the serialized sessions the file names of (or maybe some other sort of reference to?) the other sessions they depend on, so the user can just load the sessions they need and have their dependencies be loaded automatically, rather than having to manually specify a session and all its dependencies.

[eddywestbrook]

Copying some text from the Mattermost discussion on this topic:

The reason I think of this as a way to do separate compilation for proofs is that I am assuming a particular use case, where every lemma that is proved (or, at least, every lemma that we want to remember having proved) is added as a term to the current module

If the proofs are calls to SMT or other external tools, we could instead add them as axioms

I know that this idea doesn’t quite fit with how Crucible verification works, because Crucible symbolic verification only makes SAW core terms for the intermediate proof goals it generates and passes to solvers; that is, when you verify a function by symbolic execution, that verification isn’t translated to a SAW core term that somehow attests to that fact

However, an approach I have been considering for Heapster proof state that could apply here as well would be to use SAW core as a serialization target, once we have this feature of serializing SAW core terms. That is, if I have some state object I want to save, I can convert it to / from SAW core, and then let the SAW core serializer handle the rest

One benefit of this approach is that if those bigger, higher-level state objects contain SAW core terms, those would get serialized as well, together with the SAW core representation of the state object...