Notes about KMIR tool application PR feedback

[jberthold]

Small things

• Goto transcode -> Goto transcoder (kmir.md "Verification Backend" section)
• delete "critical" in "critical intermediate representation" (checkbox section)
• Link to mir-semantics repo on github in checkbox section
• Should we maintain (and link to) a list of missing features in mir-semantics? (Question in the Checkbox section)
• Mention docker image as an option in the CI question in the checkbox section

Larger content to add or modify

• Don't speculate over future kup based things in the doc.s here
• Document what is in the docker image
• Say more about K framework in general before explaining how kmir is based on it
• address detailed questions in Add kmir tool description and CI workflow model-checking/verify-rust-std#310 (comment) by rewording the description after the MIR diagram
• Explain "how 'symbolic execution' and 'proof' go together" in 1st paragraph:
  • K enables symbolic execution of MIR by rewriting
  • a program property becomes an all-path reachability problem in a rewriting system
  • a proof of reachability proves the property (given the semantics of MIR)
    This should probably be very short in the 1st paragraph but then be expanded in the subsequent section about K and kmir below.

[jberthold]

Branch add-kmir-tool-version2 for edits, to be copied over when ready

[jberthold]

I removed kontrol and evm-semantics from the links section and renamed it "Background Reading". Maybe we can remove this section in favour of a longer description of K Framework in the earlier part.

[jberthold]

More radical suggestions to modify the kmir.md description:

• Remove "Versioning" entirely
• Largely modify the "CI" section to only describe tool usage and how to find/install it, and move this into "Steps to Use the Tool
• Make "Licenses" a paragraph in the first section (removing its heading)

We could post this on the PR as a suggestion, asking whether we should do it.

[jberthold]

Edits done as described