Make summarize_verification report whether definitions depend on unsafe primitives or axioms (e.g., fix)

[RyanGlScott]

I propose that we extend the summarize_verification command such that it lists any unsafe primitives or axioms that a proof uses. The particular use case I have in mind is reporting whether any proofs depend on the SAWCore fix function, which has the potential to introduce unsoundness if wielded improperly. For example, here is an example of a proof of False (relying on fix), as well a use of summarize_verification afterwards:

// test.saw
enable_experimental;

let f = parse_core "fix (EqTrue False) (id (EqTrue False))";
f_thm <- prove_core (goal_exact f) "EqTrue False";

summarize_verification;

SAW's current output is:

$ ~/Software/saw-1.1/bin/saw test.saw
[13:32:51.593] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"


# Theorems Proved or Assumed

* Theorem:
~~~~
  EqTrue False
~~~~

This shows a proof of False, but it doesn't include the very important caveat that it relies on the unsafe fix primitive. This is especially important when you consider that one can introduce fix implicitly by writing recursive Cryptol definitions. (For example, let {{ r = ~r : Bit }}; gets translated to a SAWCore definition involving fix behind the scenes.) Inspired by Coq's Print Assumptions command, I propose that we extend the output so that it looks something like this:

# Theorems Proved or Assumed

* Theorem:
~~~~
  EqTrue False

Depends on the following unsafe primitives or axioms:
* fix
~~~~

Another axiom that would be worth reporting here is unsafeAssert.

We will need to think a bit about which primitives or axioms should count as "unsafe" in this context. The SAWCore prelude defines many primitives and axioms that aren't really unsafe, but rather left undefined so that they can be overridden with more efficient implementations (e.g., boolEq). It might be overwhelming to include every single primitive and axiom in the list of output, so perhaps we should omit things like boolEq (or only print them if the user specifically requests them).