[intuitiveness] Minimize the need for background knowledge

As we discussed in #743, I believe we need to reduce the background knowledge required for better understanding and easier verification. While our input specification is quite straightforward, the results are not easy to interpret and require knowledge of K, EVM semantics, and Kontrol's encoding algorithms. Therefore, we should develop a way to analyze the results and present information that can be understood without needing knowledge beyond Solidity. I'm not yet sure how to design this, but it might look something like this:

VERIFICATION PASSED
Verification Target: …
Precondition: …
Postcondition: …

VERIFICATION OUT-OF-TIME
A call graph with solidity expressions to split.

VERIFICATION FAILED
Location of the failed solidity program.
Reason for this failure.

The structure should be designed by experienced verification personnel to ensure that the information provided is sufficient to adjust assumptions and assertions or to identify issues in the verification target.

Start by reviewing the discussion in #743 and how Kontrol currently presents verification results. Define a user-facing structure for passed, out-of-time, and failed verification that is understandable with Solidity knowledge alone, then get the design validated by experienced verification personnel.