![Non-audit banners (1).png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/Non_audit_banners_1_30ba98e1cc.png) Runtime Verification is excited to announce the open public alpha of KMIR. KMIR defines the formal operational semantics of the Middle Intermediate Representation (MIR) of Rust in K, giving developers access to the K framework tool suite for MIR programs. The K framework includes a parser, interpreter, and symbolic execution engine. This allows MIR programs to be directly executed and brings them a step closer to formal verification via the K framework. While this work has received funding through a grant from [The Web3 Foundation](https://web3.foundation/), the development of the syntax and semantics was carried out independently. We want to thank the Web3 Foundation for its generous grant and its unwavering support throughout this project. In this blog, we will show how to extract MIR from the Rust compilation process, and how to execute MIR programs with KMIR. The project source code can be viewed on the [KMIR Github](https://github.com/runtimeverification/mir-semantics), however KMIR is easily accessible through our package manager kup. kup invokes nix to build the latest version of KMIR on your local machine, adding it to the PATH. To install kup, run the following in your terminal (this will also install nix if it is not already on your system): ``` bash <(curl https://kframework.org/install) ``` From here you can see all of the Runtime Verification tools available for download through: ``` kup list ``` ![1_blog_kup_list.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/1_blog_kup_list_7c1a1dbade.png) To install the latest version of KMIR run: ``` kup install kmir ``` You can verify the install by running `kup list` again and you should see that kmir is installed. To see the list of commands for kmir, run: ``` kmir --help ``` ![2_blog_kmir_help.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/2_blog_kmir_help_87e11c1899.png) Congratulations! You have now installed KMIR on your machine and are ready to work with some MIR. Let’s move onto the demo. ### Demo In this demo, we'll use KMIR to directly interpret and execute a MIR program. Note that this is different from using the compiled binary from rustc, because rustc first translates MIR into LLVM, which is used to the binary. First we need an example Rust program, from which we will extract the MIR representation ###### sum-to-n.rs The example we will use is a program that calculates the sum of natural numbers from zero to `n`. In particular we will choose `n = 5` and assert that the result is `15`. Copy the code below into a file named `sum-to-n.rs`. ```undefined fn main () { let mut sum = 0; let mut i = 0; while i <= 5 { sum += i; i += 1; } assert!(sum == 15); } ``` To verify that this example is indeed correct, you can run the following and see that no error is produced (the assertion passed). ``` undefined rustc sum-to-n.rs --o sum-to-n ./sum-to-n ``` Now that we have our source code, we need to extract the compiled MIR program. ###### rustc –emit mir Before we begin, the current version of KMIR is pinned to a specific version of nightly rust (`46514218f 2023-06-20`), so we are going to need to install that. If you are using rustup, this can be done with the `default` command and using the date one day after the date you wish to install: ``` rustup default nightly-2023-06-21 ``` To confirm you have the correct version you can check with: ``` rustc --version ``` ![4_blog_rustc_version.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/4_blog_rustc_version_1b86b0f721.png) Once you are using the correct version, we can extract the MIR by calling the Rust compiler again, but this time with some additional flags: ```undefined rustc --emit mir -C overflow-checks=off -Zmir-enable-passes=-ConstDebugInfo,-PromoteTemps -o sum_to_n.mir sum_to_n.rs ``` Here's a brief explanation of these additional flags: - Codegen flag `-C overflow-checks=off` will remove calls to functions that check for overflow from the MIR. - The MIR flag `-Zmir-enable-passes` provides options `-ConstDebugInfo` and `-PromoteTemps` however these will not affect this particular program. But `-ConstDebugInfo` will stop MIR expanding type information in debug scope for constants, and `-PromoteTemps` will stop the compiler from promoting temporary MIR places to have `’static` lifetimes. ![3_blog_mir_output.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/3_blog_mir_output_19128e40cb.png) Now that we have extracted the MIR, let’s look into it and understand what it does. ###### sum_to_n.mir At a high level, a MIR program can be thought of as a [Control Flow Graph](https://en.wikipedia.org/wiki/Control-flow_graph) (CFG) representation of the original Rust source program. This MIR program is one `main` function that can be thought of as 3 distinct segments: - **Place and Local Declarations** - The first thing that happens in a function is the declaration of `Places` and `Locals` that will be used to store information during the life of the function with their type information. `Places` and `Locals` are always numbered with an underscore prefix. Note that `_2` was skipped here because it will be declared in the Scope Tree. `Places` and `Locals` look the same in the output MIR, their distinction is that `Places` refer to data stored on the heap, and `Locals` as data stored on the stack. The distinction between them is not important for this example, so we will refer to both `Locals` and `Places` as `Places`. `Place` `_0` indicates the return data location for the encapsulating function. ![5_blog_mir_local_decls.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/5_blog_mir_local_decls_f594bae489.png) - **Scope Tree** - After `Places` are declared, the `scope` blocks will use `debug` statements to tie the original Rust variables to `Places`. `scope 1` links `Place _1` to `sum`, and is followed by the declaration of `_2`. `scope 2` is contained within `scope 1`, and links `Place _2` to `i`. ![6_blog_mir_scope_tree.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/6_blog_mir_scope_tree_089114ba46.png) - **Basic Blocks** - These contain the logic of the function. Each Basic Block contains a non-branching sequence of instructions to be executed, with a terminator at the end. The terminator will indicate if the block terminates execution, or specify which other Basic Block should continue the execution. These Basic Blocks together with their terminators for the nodes and edges of the CFG. Basic Block names have the form “bb” with `bb0` being the function’s entry point. For our example: - `bb0` initialises the `_1` and `_2` `Places` to `0`. - The `while` loop from the Rust source translates to `bb1` and `bb2`: - `bb1` is the guard of the loop, the terminator branches after the check, and can move to the body of the loop `bb2`, or exit the loop to `bb3`. - `bb2` performs the loop additions and returns to `bb1`. - `bb3` translates the `assert!` in the Rust source, i.e., it checks that the result of the computation is equal to `15` and transfers the execution to either `bb4` or `bb5`. - `bb4` and `bb5` are leaf nodes. If the assertion that `sum == 15` fails, execution reaches `bb4` which terminates in an error. Otherwise, `bb5` terminates successfully. ![7_blog_mir_basic_blocks.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/7_blog_mir_basic_blocks_edf248cef4.png) Now that we have an understanding of the contents of `sum_to_n.mir`, let’s use KMIR to execute the program. ###### kmir run Before executing `kmir run sum-to-n.mir`, let’s understand two flags: `--output pretty` will change the output from the default `kast` to a human readable representation. `--depth` will tell KMIR how many steps to take before stopping, which allows us to inspect the state throughout the execution. Let’s look at the configuration of the program before any execution has taken place, so `--depth 0`. ``` kmir run --output pretty --depth 0 sum_to_n.mir ``` ![8_blog_depth_0.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/8_blog_depth_0_815abb0613.png) The state of the program is printed in XML-like cells. The most interesting cell is the `` cell, which currently contains the K representation of the entire `sum_to_n.mir` program! As the program is interpreted, the `` cell will transform to show the list of internal functions that are queued for execution. The other cells are pretty empty at the moment, but a notable mention is the `` cell which is currently `4` (our initial dummy value), and which will be updated to either `2` for an error such as a `panic!`, or `0` if termination ends successfully. By looking at the phase cell, we can see that we are in the `Initialisation` phase. In this phase the entire `sum_to_n` program will be interpreted to fill out a `` entry in the `` cell with the `main` function. Here is a truncated example of the `main` `` entry: ![12_blog_function_cell.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/12_blog_function_cell_4f5db866dc.png) The `` cells will record the `Place` declarations, and the `` cells will record the basic blocks. To have a look at this information all filled out, let’s skip to the start of the `Execution` phase by running again with `--depth 22`. ``` kmir run --output pretty --depth 22 sum_to_n.mir ``` The output is much larger now, but you should be able to go through and match up the configuration to the `sum_to_n.mir` file. The next thing to note is that the `` cell is not about to execute to the `main` function. ![9_blog_depth_22.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/9_blog_depth_22_dbaf3cfc52.png) It takes 160 steps to execute the whole function and terminate the program. By increasing the depth on the way to 160 you can see the state update as the basic blocks are executed. We will leave that for you, however let’s have a look at the final state of the program - we can omit the `--depth` flag entirely for this. ``` kmir run --output pretty sum_to_n.mir ``` We can see that the `` cell is now empty, and the `` was 0. ![10_blog_return_val.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/10_blog_return_val_7b107af95a.png) Success! We can further convince ourselves that the result is correct by examining `Place _1` which if you recall, was linked to `sum` in our scope tree. We can see that `_1` is 15 as we expect! ![11_blog_local_1.png](https://strapi-rv-bucket-01.s3.us-east-2.amazonaws.com/11_blog_local_1_a3bdb45c09.png) ##### Conclusion Thank you for your interest in KMIR, this project is still in active development as we push towards better coverage of the MIR syntax and semantics, with the end goal of having full formal verification. We aim to improve the experience by streamlining the process from extracting the MIR to verifying program properties. If you have any questions, or run into any problems during this tutorial, feel free to join the [Runtime Verification discord](https://discord.com/invite/CurfmXNtbN) to ask and chat anytime! We thank the Web3 Foundation for their support. ## About Runtime Verification Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field. ## About Web 3 Foundation Web3 Foundation funds research and development teams building the technology stack of the decentralized web. It was established in Zug, Switzerland by Ethereum co-founder and former CTO Gavin Wood. Polkadot is the Foundation's flagship project.

Author: Daniel Cumming