Evidence tracking

[robdockins]

As part of #1102, some internal changes were made to proof state handling and the Theorem type. In particular Theorem values now contain Evidence which is produced when a proof is finished. However, right now we are not really collecting and using this evidence in user-reportable ways, and there remain some soundness holes. This ticket exists to track these issues.

1. Theorem values can be used to generate rewrite rules that are placed into Simpsets, which can be used in rewriting steps in later proofs. The evidence associated with theorems is currently discarded when they are made into a rewrite rule. As a result, we are simply trusting that Simpset values represent valid rewrites during evidence checking, and we loose the provenance of the used theorems.
2. llvm_verify and friends discard the theorem value and evidence generated regarding individual verification condition proofs. These should probably be collected in completed MethodSpec values and somehow propagated into further proofs when used as overrides.
3. Exported proof obligations should probably be tracked better, e.g., by capturing the filename of the generated file and a hash of its contents to help connect the recorded evidence with the generated artifacts.
4. Evidence values should be somehow used to present users with a more comprehensive listing of what the trust base of their proofs is. What axioms were stated and used? What proofs were stated but admitted, and are those in-progress proofs or ones we believe are infeasible for some reason? What statements were proved by which solvers? What statements were random tested? What external files must be validated? etc. We may even want to somehow express policy statements to describe when a proof has reached an acceptable level of "done".
5. I worry that the Evidence values themselves may cause a lot of memory pressure in large proofs as we increase their lifetimes by tracking them more carefully. We should consider if we should summarize evidence in a more compact representation instead, based on the decisions we make regarding point 4 above.

[nano-o]

Not sure is this counts as evidence tracking, but, for user-reporting purposes, it would also be nice if Theorem had a source location (when it makes sense). E.g., a line number in a saw-script file where the theorem was stated.

[robdockins]

At the moment, all the points above except point 3 are pretty well addressed. So far, the need to track evidence doesn't seem to have resulted in undue memory pressure, so point 5 so far hasn't needed fixing.