saw-core-coq: fix and document the local translation state

[Ptival]

5a37203 introduced a subtle bug in the
translation of Cryptol modules to Coq. In this commit, it was decided that all
'TranslationState' should be restored when calling `withLocalLocalEnvironment'.

Historically, 'withLocalLocalEnvironment' was only supposed to restore the
value of the 'localEnvironment' field of the translation state, hence its name.
The translation state has grown since, and includes many fields that ought to
be restored after a local (sub-)term translation. Unfortunately, the
translation state also contains fields that are meant to monotonically
accumulate global data through the translation.

Those fields are thus being erased incorrectly due to the changes made. This
commit revert those changes, making it painfully explicit which fields of the
state are to be restored or preserved so that future refactorings will have to
make a decision.

In the process, I also renamed the confusing 'localDeclarations' into
'topLevelDeclarations', since it captures declarations that appear in the
processed file (so more local than the "global", "ambient" standard library
declarations), but the name made it sound like these were more local.

[Ptival]

The changes to CryptolPrimitivesForSAWCore.v seem unrelated to this PR, and possibly due to changes in Cryptol.

The changes to SAWCorePrelude.v, on the other hand, are intriguing.

I tried to add a bit of documentation, at the very least around the parts where my lack of documentation led Brian to introduce a change that broke my unstated assumptions.

Ideally we should have some regression tests for translateCryptolModule to know when we break things there that don't appear in just the generation of the scaffolding.

[brianhuffman]

I didn't analyze everything super-carefully, but it seems good to me.

[Ptival]

@eddywestbrook any objection to merging this?

[m-yac]

@eddywestbrook any objection to merging this?

I'm not Eddy, but has this run with the latest CI? Now that Heapster has been merged to master, the CI should be able to check whether this breaks any of our Heapster examples. Though just looking at this PR's changes to SAWCorePrelude.v, I don't see any obvious way this could break our examples.

[Ptival]

Thanks @m-yac , I'm mostly worried that changes to the Coq output could cause problems in whatever proofs/automation you may have down the line.

I will rebase the PR to let the CI do its thing and see where we are.

[eddywestbrook]

Val, sorry I haven't gotten a chance to look at this in depth yet. Matt is right, mostly what I would do would be to see if it breaks our examples, which are now in the CI.

[robdockins]

Is this waiting on anything in particular?

[Ptival]

I don't think so, and it'd be good to merge it given it fixes a fairly annoying bug, I'll give it a rebase/CI round.