What4 eval3

[robdockins]

Another attempt at improving the situation WRT evaluating terms more fully before passing them down to the Crucible symbolic simulator.

These patches cause the ResolveSetupValue phase to evaluate terms using the What4 SAWCore backend, but limits the definitions it will unfold to those from the prelude, or those defined locally with "let", relying on the new structured name infrastructure in SAWCore to reliably make this determination.

[robdockins]

@brianhuffman, I think this is ready to merge (pending CI), if you have a minute to review.

[robdockins]

@andreistefanescu, looks like there is a fairly serious slowdown in the s2n/hmac proofs on this branch, and a less serious slowdown in SIKE. Any off-the-cuff ideas why that might be?

[robdockins]

Some profiling and trial-and-error seems to indicate that most of the slowdown here is due to the exception-handling overheads arising from this line:

https://github.com/GaloisInc/saw-core/blob/8eefd675590ef81f819355af25d155d692e01345/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs#L1165

I'll have to find some other way to implement this.

[robdockins]

Upon some more experimentation, I think exception handling isn't actually the issue. Instead, it seems to be that fewer expressions are being evaluated to concrete values because evaluation bails when it sees a non-prelude identifier. As a result, we are getting less exact results going into the simulator, and more override variants have to be tried.

So... I guess we need to make sure to evaluate concretely whenever possible, but don't expand values whose result is symbolic if we have to unfold a non-prelude symbol. I'm not sure how to accomplish that, except by the brute-force method of evaluating things fully and seeing if they are concrete. Then, if the result is symbolic checking to see if we unfolded any disallowed symbols, and discarding the results if so.... which seems kind of wasteful, but maybe isn't so bad.

[robdockins]

Status update, short version: I think the current state of things is a bit of a local minimum here, and some more extensive refactoring will be required to do better.

Status update, longer version. The current strategy is basically: evaluate bitvector and boolean values that do not contain free variables (ExtCns), and paste in any concrete values we compute into the symbolic simulator. If the computed value is not concrete, throw it away and make an opaque "binding", which creates a fresh What4 variable and records in a table the corresponding SAWCore term. What we'd like to do is remove the restriction that evaluates only terms not containing free variables so the simulator can notice, e.g. preconditions that interact with control-flow decisions, or useful simplifications (and a (or a b) ->= a).

Attempt 1: fully evaluate every term. This basically works, but significantly slows down most proofs. For compositional verification, we typically want to treat subcomputations as opaque, which is provided by the current strategy.

Attempt 2: treat imported Cryptol terms as opaque. This basically works, but significantly slows down some proofs. We loose some opportunities for concrete evaluation with this strategy because we treat all imported terms as opaque, even if evaluation would result in concrete terms.

Attempt 3: fully evaluate every term and keep track of every constant unfolded. Only use the result if it is concrete, or if we never unfolded any constant we consider opaque. This is generating spurious counterexamples for reasons I don't understand. I suspect that the back-and-forth mapping between What4 and SAWCore is getting confused somewhere and distinct free variables are being assigned to things that should be the same.

What we would actually like to have: evaluate terms as far as possible, mapping external constants in a way that correctly respects round-tripping. When we encounter an "opaque" constant, evaluate it, but only use the result if it is concrete. Otherwise, replace the term with an uninterpreted function, as we do for external constants. All of this is made quite a bit trickier by the fact that SAWCore simulators are lazy, so the decision about what to do with results has to be delayed until the relevant thunks are eventually forced. I don't see an obvious way to shoehorn this strategy into the current SAWCore evaluator infrastructure, and the SAWCore<->What4 mappings are a bit scattered and disorganized. In addition, all this depends on the types involved in the functions and external constants being a sufficiently simple subset that they can be properly represented in What4. Handling all the corner cases properly is going to be tricky.

I think we probably need to refactor saw-core-what4 by folding the majority of crucible-saw into that package instead, and simplifying the various code paths so we can gain a lot more confidence in the correctness of the translations and round-tripping properties. This should at least let us get a proper implementation of "attempt 3" above. After that, we should figure out how to refactor the SAWCore evaluators to allow what we actually want to do. This should probably roll up the other simulator refactor we want to do, which is to pull in the Cryptol backend class, so we can uniformly represent many of the underlying primitive types and operations.