Add kmir tool description and CI workflow

.github/workflows/kmir.yml

@@ -0,0 +1,45 @@
+name: KMIR
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/kmir.yml'
+      - 'kmir-proofs/**'
+
+jobs:
+  run-kmir-proofs:
+    name: Run supplied KMIR proofs
+    runs-on: ubuntu-latest
+    env:
+      container_name: "kmir-${{ github.run_id }}"
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+
+      - name: Start Tool Container
+        run: |
+          docker run --detach --rm -t \
+            --name ${{ env.container_name }} \
+            -w /workspace \
+            runtimeverificationinc/kmir:ubuntu-jammy-0.3.112_7.1.229-9e17ccd /bin/bash
+
+      - name: Copy KMIR proofs into container
+        run: |
+          docker cp kmir-proofs ${{ env.container_name }}:/workspace/kmir-proofs
+
+      - name: Run KMIR Verification for all proofs provided
+        run: |
+          for k_file in kmir-proofs/*/*-spec.k; do
+            echo "Running ${k_file}"
+            docker exec -t ${{ env.container_name }} kmir prove run ${k_file}
+          done
+
+      - name: Stop Tool Container
+        if: always()
+        run: docker stop ${{ env.container_name }}

doc/src/SUMMARY.md

@@ -10,6 +10,7 @@
   - [Kani](./tools/kani.md)
   - [GOTO Transcoder](./tools/goto-transcoder.md)
   - [VeriFast](./tools/verifast.md)
+  - [KMIR](./tools/kmir.md)
 
 ---
 

doc/src/tools.md

@@ -14,7 +14,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
  | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |
  | GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml)      |
  | VeriFast for Rust   | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml)      |
-
+ | KMIR Symbolic Rust Execution | [![KMIR](https://github.com/model-checking/verify-rust-std/actions/workflows/kmir.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kmir.yml)      |
 
 
 

doc/src/tools/kmir.md

@@ -0,0 +1,198 @@
+## Tool Name
+**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.
+
+This diagram describes the extraction and verification workflow for KMIR:
+
+![kmir_env_diagram_march_2025](https://github.com/user-attachments/assets/bf426c8d-f241-4ad6-8cb2-86ca06d8d15b)
+
+
+The K Framework ([kframework.org](https://kframework.org/) is the basis of how
+KMIR operates to guarantee properties of Rust programs. K is a rewrite-based
+semantic framework based on [matching logic](http://www.matching-logic.org/) in
+which programming languages, their operational semantics and type systems, and
+formal analysis tools can be defined through syntax, configurations, and rules.
+The _syntax_ definitions in KMIR model the AST of Stable MIR (e.g., the
+statements and terminator of a basic block in a function body) and configuration
+data that exists at runtime (e.g., the stack frame structure of a function
+call).
+The _configuration_ of a KMIR program organizes the state of an executed program in
+nested configuration units called cells (e.g., a stack frame is part of a stack
+stored in the configuration).
+_K Framework transition rules_ of the KMIR semantics are rewriting steps that
+match patterns and transform the current continuation and state accordingly.
+They describe how program configuration and its contained data changes when
+particular program statements or terminators are executed (e.g., a returning
+function modifies the call stack and writes a return value into the caller's
+local variables).
+
+Using the K semantics of Stable MIR, the KMIR execution of an entire Rust
+program represented as Stable MIR breaks down to a series of configuration
+rewrites that compute data held in local variables, and the program may either
+terminate normally or reach an exception or construct with undefined behaviour,
+which terminates the execution abnormally. Programs modelled in K Framework can
+be executed _symbolically_, i.e., operating on abstract input which is not fully
+specified but characterised by _path conditions_ (e.g., that an integer variable
+holds an unknown but non-negative value).
+
+K (and thus KMIR) verifies program correctness by performing an
+_all-path-reachability proof_ using the symbolic execution engine and verifier
+derived from the K encoding of the Stable MIR operational 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/).
+An all-path-reachability proof in this system verifies that a particular
+_target_ end state is _always_ reached from a given starting state.
+The rewrite rules branch on symbolic inputs covering the possible transitions,
+creating a model that is provably complete. For all-path reachability, every
+leaf state is required to unify with the target 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.
+
+When performing a proof of a program that involves recursion or a loop construct,
+one of several possible techniques can be used:
+
+1) K (and thus KMIR) are capable of unbounded verification via allowing the
+   user to write loop invariants. However, these loop invariants would then
+   need to be written in K's native language.
+2) As potential future work, it would be possible to implement an annotation
+   language to provide the required context for loop invariant directly in
+   source code (as done in the past using natspec for Solitidy code).
+3) In general, K also supports bounded loop unrolling, by way of identifying
+   loop heads and counting how many times the same loop head has been observed.
+   This technique is managed by the all-path reachability prover library for
+   K and works out of the box with suitable arguments, without requiring any
+   special support from the back-end.
+
+Our front-end, at the time of writing, does not have either of these
+options turned on. As soon as larger programs will require it, we will decide
+whether the preference is to implement support for user-supplied K-level
+loop invariants, or bounded loop unrolling support, or (probably) offer both.
+
+KMIR also prioritizes UI with interactive proof exploration available
+out-of-the-box through the terminal KCFG (K Control Flow Graph) viewer, allowing
+users to inspect intermediate states of the proof to get feedback on the
+successful path conditions and failing at unifying with the target state. An
+example of a KMIR proof being analyzed using the KCFG viewer can be seen below:
+
+<img width="1231" alt="image" src="https://github.com/user-attachments/assets/a9f86957-7ea5-4bf6-bee2-202487aacc9b" />
+
+
+## Tool Information
+
+* [x] Does the tool perform Rust verification?
+  *Yes – It performs verification at the MIR level, an intermediate
+  representation of Rust programs in the Rust compiler `rustc`.*
+* [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 or through a docker image provided.*
+* [x] Is the tool open source?
+  *Yes – KMIR is [open source and available on GitHub](https://github.com/runtimeverification/mir-semantics).*
+* [x] Is the tool under development?
+  *Yes – KMIR is actively under development, with ongoing improvements to MIR
+  syntax coverage and verification capabilities.*
+* [x] Will you or your team be able to provide support for the tool?
+  *Yes – The Runtime Verification team is committed to supporting KMIR and will
+  provide ongoing maintenance and community support.*
+
+## Licenses
+KMIR is released under an OSI-approved open source license. It is distributed
+under the BSD-3 clause license, which is compatible with the Rust standard
+library licenses. Please refer to the [KMIR GitHub
+repository](https://github.com/runtimeverification/mir-semantics?tab=BSD-3-Clause-1-ov-file)
+for full license details.
+
+## 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-transcoder (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.
+- **Verification Input:** KMIR takes input from Stable MIR JSON, an effort to
+  serialize the internal MIR in a portable way that can be reusable by other
+  projects.
+- **K Ecosystem:** Since all tools in the K ecosystem share a common foundation
+  of K, all projects benefit from development done by other K projects. This
+  means that performance and user experience are projected to improve due to the
+  continued development of other semantics.
+
+## Steps to Use the Tool
+
+The [KMIR docker
+image](https://github.com/runtimeverification/mir-semantics/blob/c221c81d73a56c48692a087a2ced29917de99246/Dockerfile.kmir)
+is currently the best option for casual users of KMIR. It contains an
+installation of K Framework, the tool `kmir`, and the `stable-mir-json`
+extraction tool, which is a custom version of `rustc` which extracts Stable MIR
+as JSON or as graphviz' *.dot when compiling a crate.
+The image is [available on Docker Hub](https://hub.docker.com/r/runtimeverificationinc/kmir/tags).
+
+Alternatively, the tools for `kmir` can be built from source as [described in
+the `mir-semantics` repository's
+`README.md`](https://github.com/runtimeverification/mir-semantics). This
+requires an installation of `K Framework`, best done [using the `kup`
+tool](https://github.com/runtimeverification/kup/README.md), and includes a
+git submodule dependency on `stable-mir-json`.
+
+The `stable-mir-json` tool is a custom version of `rustc` which, while compiling
+Rust code, writes the code's Stable MIR, represented in a JSON format, to a
+file.  Just like `rustc` itself, `stable-mir-json` extracts MIR of a single
+crate and must be invoked via `cargo` for multi-crate programs. Besides the JSON
+extraction, `stable-mir-json` can also write a graphviz `dot` file representing
+the Stable MIR structure of all functions and their call graph within the crate.
+
+The `kmir` tool provides commands to work with the Stable MIR representation of
+Rust programs that `stable-mir-json` extracts.
+
+* Run Stable MIR code extracted from Rust programs (`kmir run my-program.smir.json`);
+* Prove a property about a Rust program, which is given as a K "claim" and
+  proven using an all-path reachability proof in K (`kmir prove run my-program-spec.k`);
+* Inspect the control flow graph of a program's proof constructed by the `kmir
+  prove run` command (`kmir prove view Module.Proof-Identifier`).
+
+Examples of proofs using KMIR, and how to derive them from a Rust program
+manually, are [provided in the `kmir-proofs`
+directory](https://github.com/model-checking/verify-rust-std/tree/main/kmir-proofs).
+
+The `kmir` tool is under active development at the time of writing.
+Constructing a K claim from a given Rust program is currently a manual process
+but will be automated in a future version. Likewise, at the time of writing, the
+`kmir` tool does not automatically extract Stable MIR from a Rust program, the
+Stable MIR must be extracted by invoking `stable-mir-json` manually.
+
+
+## Background Reading
+
+- **[Matching Logic](http://www.matching-logic.org/)**
+  Matching Logic is a foundational logic underpinning the K framework, providing
+  a unified approach to specifying, verifying, and reasoning about programming
+  languages and their properties in a correct-by-construction manner.
+
+- **[K Framework](https://kframework.org/)**
+  The K Framework is a rewrite-based executable semantic framework designed for
+  defining programming languages, type systems, and formal analysis tools. It
+  automatically generates language analysis tools directly from their formal
+  semantics.

kmir-proofs/README.md

@@ -0,0 +1,135 @@
+# Formal Rust Code Verification Using KMIR
+
+This directory contains a collection of programs and specifications to
+illustrate how KMIR can validate the properties of Rust programs and
+standard library functions.
+
+
+## Setup
+
+KMIR verification can either be run from [docker images provided under
+`runtimeverificationinc/kmir`](https://hub.docker.com/r/runtimeverificationinc/kmir),
+or using a local installation of
+[`mir-semantics`](https://github.com/runtimeverification/mir-semantics/)
+with its dependency
+[`stable-mir-json`](https://github.com/runtimeverification/stable-mir-json). The
+installation is described in the repository's `README.md` files.
+
+## Example Proof: Proving a Maximum Finding Function That only Uses `lower-than`
+
+Considering a function that receives three integer arguments, this
+function should return the highest value among them. Assertions can be
+used to enforce this condition, and an example code that tests this
+function can be seen below:
+
+```Rust
+fn main() {
+
+    let a:usize = 42;
+    let b:usize = 43;
+    let c:usize = 0;
+
+    let result = maximum(a, b, c);
+
+    assert!(result >= a && result >= b && result >= c
+        && (result == a || result == b || result == c ) );
+}
+
+fn maximum(a: usize, b: usize, c: usize) -> usize {
+    // max(max(a,b), c)
+    let max_ab = if a < b {b} else {a};
+    if max_ab < c {c} else {max_ab}
+}
+```
+
+Notice in this case that `a`, `b`, and `c` are concrete, fixed
+values. To turn the parameters of `maximum` into symbolic variables,
+we can obtain the representation of the function call to `maximum`
+executed using KMIR and then replace the concrete values of these
+variables with symbolic values. Furthermore, the assertion specified
+in the code can be manually translated as a requirement that should be
+met by the symbolic variables, meaning that any value that they can
+assume must respect the conditions contained in the
+specification. Following this approach, we can utilize KMIR to give us
+formal proof that, for any valid `isize` input, the maximum value
+among the three parameters will be returned.
+
+Work on KMIR is in progress and the way a Rust program is turned into
+a K claim will be automated in the near future, but is currently a
+manual process described in the longer [description of
+`maximum-example-proof`](./maximum-example-proof/README.md).
+
+To run this proof in your terminal from this folder, execute:
+
+```sh
+cd maximum-proof
+kmir prove run  $PWD/maximum-spec.k --proof-dir $PWD/proof
+```
+
+If option `--proof-dir` was used, the finished (or an unfinished) proof can be inspected using the following command:
+
+```sh
+kmir prove view MAXIMUM-SPEC.maximum-spec --proof-dir $PWD/proof
+```
+
+## Example Proofs: Safety of Unsafe Arithmetic Operations
+
+The proofs in subdirectory `unchecked_arithmetic` concern a section of
+the challenge of securing [Safety of Methods for Numeric Primitive
+Types](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html#challenge-11-safety-of-methods-for-numeric-primitive-types)
+of the Verify Rust Standard Library Effort.
+
+The `*-spec.k` files set up a proof of concept of how KMIR can be used
+to prove unsafe methods according to their undefined behaviors. Proofs
+were set up using the same method as described for the
+`maximum-example-proof`.
+
+All K claim files follow the same pattern (illustrated using
+`unchecked_add` on `i16` as an example):
+
+1) For a given unsafe operation, a calling wrapper function
+   `unchecked_op` is written and translated to Stable MIR
+
+```rust
+ fn unchecked_op(a: i16, b: i16) -> i16 {
+     let unchecked_res = unsafe { a.unchecked_add(b) };
+     unchecked_res
+ }
+```
+
+2) A K configuration for a Rust program that calls this function with
+   symbolic `i16` arguments `A` and `B` is constructed (currently in a
+   manual fashion). The `i16` arguments are represented as `Integer(A,
+   16, true)`.
+
+3) According to the [documentation of the unchecked_add function for
+   the i16 primitive
+   type](https://doc.rust-lang.org/std/primitive.i16.html#method.unchecked_add),
+
+> "This results in undefined behavior when `self + rhs > i16::MAX` or
+> `self + rhs < i16::MIN`, i.e. when `checked_add` would return `None`"
+
+  This safety condition is translated into a `requires` clause in the
+  K claim. In addition, the invariants for `A`'s and `B`'s
+  representation as `i16` can be assumed, giving:
+
+```
+ requires // i16 invariants
+            0 -Int (1 <<Int 15) <=Int A
+    andBool A <Int (1 <<Int 15)
+    andBool 0 -Int (1 <<Int 15) <=Int B
+    andBool B <Int (1 <<Int 15)
+    // invariant of the `unchecked_add` operation
+    andBool A +Int B <Int (1 <<Int 15)
+    andBool 0 -Int (1 <<Int 15) <=Int A +Int B
+```
+
+4) The KMIR semantics would stop the execution instantly when any
+   undefined behaviour is detected (i.e., in case of an overflow or
+   underflow). The K claim as a whole states that the called function
+   will execute to its `Return` point, without causing any undefined
+   behaviour.
+
+Claims were set up for functions: `unchecked_add`, `unchecked_sub`,
+and `unchecked_mul`, and for type `i16` but are easy to adapt for
+other bit width and unsigned numbers.