Proof summary improvements #1216
Commits on Jun 2, 2021
-
Track some additional metadata about theorems,
including source positions.
-
Add annotations to rewrite rules and simpsets.
This allows users to add metadata their rewrite rules, and have rewriting steps record and return the metadata for rules what were actually used in rewriting. The intention is to use these annotations to link rewrite rules back to theorems/axioms that generated them so proof steps can determine the dependencies of a proof.
-
Update uses of saw-core API WRT simpset annotations.
Currently, we use trivial `()` annotations and ignore annotations collected by rewrite steps. The plan is to allocate unique nonces for each theorem and use those to track theorem dependencies.
-
Update saw-remote-api with Simpset changes.
TODO! We currently are allowing users to create simpsets from raw terms, and probably we should only let `Theorem` values be turned into rewrite rules.
-
Deprecate
addsimp'andaddsimps'.Instead, users should use `core_axiom` or `prove_print (admit "...")` to turn terms into theorems for use with `addsimp` or `addsimps`.
-
Start tracking theorem dependencies.
Add a unique value to each generated theorem, and compute the set of theorems a proof depends on while checking evidence. Track the collection of all proved theorems during a run in a `TheoremDB`; later we should be able to generate a graph of theorem depencencies from this database.
-
Add a new
ProvedSpecrecord for tracking metadata aboutspecs that have been proved or assumed.
-
-
-
-
Add elapsed time metadata to theorems and proved specifications.
These are now output in JSON verification summaries.
-
-
Add a rough cut at visualizing a proof dependency graph.
We parse a verification summary JSON file and produce a Graphviz file intended to be fed into `dot` to produce a visulaization. For large proofs, especially, the layout is problematic; however, even so, it seems like a helpful way to scroll through a proof and get a sense of what is proved and what depends on what.
-
Use HTML-like tables instead of graph clusters for
displaying verification conditions of method specs. This reduces clutter in the graph and produces more readable output.
-
Remove the case that builds a rewrite rule directly from a term
in saw-remote-api
