Add kmir tool description and CI workflow #310
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
When setting `shell: bash`, the internal command used in the github job is different from when nothing is set, see https://docs.github.com/en/actions/writing-workflows/workflow-syntax-for-github-actions#jobsjob_iddefaultsrunshell
- Focused on fixing read/write permission issues in previous image - New image introduces new env and bash profile for additional exec calls used in CI.
- Still requires some additional steps to fetch the results from the running container but this is a starting point.
…een CI environments
tautschnig
reviewed
Apr 4, 2025
doc/src/tools/kmir.md
Outdated
| **KMIR** | ||
|
|
||
| ## Description | ||
| [KMIR](https://github.com/runtimeverification/mir-semantics) is a formal verification tool for Rust that defines the operational semantics of Rust’s Middle Intermediate Representation (MIR) in K (through Stable MIR). By leveraging the [K framework](https://kframework.org/), KMIR provides a parser, interpreter, and symbolic execution engine for MIR programs. This tool enables direct execution of concrete and symbolic input, with step-by-step inspection of the internal state of the MIR program's execution, serving as a foundational step toward full formal verification of Rust programs. Through the dependency [Stable MIR JSON](https://github.com/runtimeverification/stable-mir-json/), KMIR allows developers to extract serialized Stable MIR from Rust’s compilation process, execute it, and eventually prove critical properties of their code. Soon, KMIR will be available via our package manager, [kup](https://github.com/runtimeverification/kup), which will make it easily installable and integrable into various workflows. |
There was a problem hiding this comment.
- Meta-note: very long lines make it quite hard to given focussed feedback. Mind breaking lines at 80, 10, or maybe 120 characters?
- I don't know whether it's useful to speculate on the availability of KMIR via
kupin this document. This is probably best placed on your blog or website as it may become stale in this place. - It is not entirely clear (at this point of reading) how "symbolic execution" and "proof" go together (possibly those do via loop invariants?). Perhaps place a forward reference to avoid confusion?
There was a problem hiding this comment.
Hmm, even after reading the full text here I don't know the answer to the third item above. Please clarify.
doc/src/tools/kmir.md
Outdated
|  | ||
|
|
||
|
|
||
| Particular to this challenge, KMIR verifies program correctness using the correct-by-construction symbolic execution engine and verifier derived from the K encoding of the Stable MIR semantics. The K semantics framework is based on reachability logic, which is a theory describing transition systems in [matching logic](http://www.matching-logic.org/). Transition rules of the semantics are rewriting steps that match patterns and transform the current continuation and state accordingly. An all-path-reachability proof in this system verifies that a particular _target_ end state is _always_ reachable from a given starting state. The rewrite rules branch on symbolic inputs covering the possible transitions, creating a model that is provably complete, and requiring unification on every leaf state. A one-path-reachability proof is similar to the above, but the proof requirement is that at least one leaf state unifies with the target state. One feature of such a system is that the requirement for an SMT is minimized to determining completeness on path conditions when branching would occur. |
There was a problem hiding this comment.
- In "to this challenge", what does "this" refer to?
- I think it would be helpful to have one paragraph on the K framework itself before diving into KMIR in more detail.
- What exactly is correct-by-construction here? Is it the symbolic execution algorithm, assuming the K encoding of Stable MIR is correct?
- To me, the "One feature of such a system ..." sentence is a technical detail when the bigger picture has hardly been conveyed. Perhaps that should be left to some later paragraph?
doc/src/tools/kmir.md
Outdated
| ## Tool Information | ||
|
|
||
| * [x] Does the tool perform Rust verification? | ||
| *Yes – It performs verification at the MIR level, which is a critical intermediate representation of Rust programs.* |
There was a problem hiding this comment.
If MIR is "critical", which IR would not be critical? (I'd suggest to just omit "critical"...)
doc/src/tools/kmir.md
Outdated
| * [x] Does the tool deal with *unsafe* Rust code? | ||
| *Yes – By operating on MIR, KMIR can analyze both safe and unsafe Rust code.* | ||
| * [x] Does the tool run independently in CI? | ||
| *Yes – KMIR can be integrated into CI workflows via our package manager and Nix-based build system.* |
There was a problem hiding this comment.
Hmm, but then you have a Docker container. Is the "package manager" piece more of a prospective situation?
doc/src/tools/kmir.md
Outdated
| * [x] Does the tool run independently in CI? | ||
| *Yes – KMIR can be integrated into CI workflows via our package manager and Nix-based build system.* | ||
| * [x] Is the tool open source? | ||
| *Yes – KMIR is open source and available on GitHub.* |
There was a problem hiding this comment.
I'd suggest to provide a link a this point.
doc/src/tools/kmir.md
Outdated
| * [x] Is the tool open source? | ||
| *Yes – KMIR is open source and available on GitHub.* | ||
| * [x] Is the tool under development? | ||
| *Yes – KMIR is actively under development, with ongoing improvements to MIR syntax coverage and verification capabilities.* |
There was a problem hiding this comment.
Since you mention this: is there a place where current limitations are documented?
doc/src/tools/kmir.md
Outdated
| ## Comparison to Other Approved Tools | ||
| The other tools approved at the time of writing are Kani, Verifast, and Goto-transcoder (ESBMC). | ||
|
|
||
| - **Verification Backend:** KMIR primarily differs from all of these tools by utilizing a unique verification backend through the K framework and reachability logic (as explained in the description above). KMIR has little dependence on an SAT solver or SMT solver. Kani's CBMC backend and Goto-transcode (ESBMC) encode the verification problem into an SAT / SMT verification condition to be discharged by the appropriate solver. Kani recently added a Lean backend through Aeneas, however Lean does not support matching or reachability logic currently. Verifast performs symbollic execution of the verification target like KMIR, however reasoning is performed by annotating functions with design-by-contract components in separation logic. |
There was a problem hiding this comment.
Nit pick: Goto-transcode -> Goto-transcoder
|
@tautschnig Thank you very much for your detailed feedback on the text. Will try to address your points in a revised version coming soon.
Very true, sorry for this. Keeping each paragraph in a single line is sometimes necessary for weak renderers but certainly not a good idea for a PR to be commented on. In a first commit from here, I will just reformat all Markdown to 80-column paragraphs (w/o any non-formatting changes) to get this problem out of the way. |
10 tasks
|
Here is a revised version of the
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds the
kmirtool to the doc.s and sets up a CI workflow that runs the tool on a few examples.The examples are drawn from Challenge 11 (unchecked arithmetic operations).
The tool is described using the text from the related issue #296 , and the example proofs come with a description that explains how they were set up.
The
kmirtool is work in progress, we expect tool usage to change. Specifically the proof setup will be automated in a future version, enabling the tool to work directly with Rust code.kmiris provided as a docker image from Dockerhub for the CI workflow. This image also includesstable-mir-jsonand was assembled for general usage by developers to try the tool in its current state.Resolves #296