diff --git a/.github/workflows/kmir.yml b/.github/workflows/kmir.yml
new file mode 100644
index 0000000000000..1c49e43f3a0c1
--- /dev/null
+++ b/.github/workflows/kmir.yml
@@ -0,0 +1,53 @@
+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 KMIR proofs
+ runs-on: ubuntu-latest
+ env:
+ container_name: "kmir-${{ github.run_id }}"
+
+ steps:
+ - name: Checkout Repository
+ uses: actions/checkout@v4
+
+ - name: Run Challenge 11 Proofs
+ run: |
+ docker run --rm -t \
+ --name ${{ env.container_name }} \
+ -w /home/kmir/workspace \
+ -u $(id -u):$(id -g) \
+ -v $PWD:/home/kmir/workspace \
+ runtimeverificationinc/kmir:ubuntu-jammy-latest \
+ kmir-proofs/0011-floats-ints/run-proofs.sh
+
+ run-kmir-proofs-negative:
+ name: Run KMIR negative proofs
+ runs-on: ubuntu-latest
+ env:
+ container_name: "kmir-neg-${{ github.run_id }}"
+
+ steps:
+ - name: Checkout Repository
+ uses: actions/checkout@v4
+
+ - name: Run Challenge 11 Negative Proofs
+ run: |
+ docker run --rm -t \
+ --name ${{ env.container_name }} \
+ -w /home/kmir/workspace \
+ -u $(id -u):$(id -g) \
+ -v $PWD:/home/kmir/workspace \
+ runtimeverificationinc/kmir:ubuntu-jammy-latest \
+ kmir-proofs/0011-floats-ints/run-proofs.sh --negative
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index cb6d9337dd32d..ec6ec4fc0a547 100644
--- a/doc/src/SUMMARY.md
+++ b/doc/src/SUMMARY.md
@@ -11,6 +11,7 @@
- [GOTO Transcoder](./tools/goto-transcoder.md)
- [VeriFast](./tools/verifast.md)
- [Flux](./tools/flux.md)
+ - [KMIR](./tools/kmir.md)
---
diff --git a/doc/src/tools.md b/doc/src/tools.md
index f0c9b40cb2792..e8a89865aea83 100644
--- a/doc/src/tools.md
+++ b/doc/src/tools.md
@@ -14,4 +14,8 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
| ESBMC (GOTO-Transcoder) | [](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml) |
| Flux | [](https://github.com/model-checking/verify-rust-std/actions/workflows/flux.yml) |
| Kani Rust Verifier | [](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml) |
+ | KMIR Symbolic Rust Execution | [](https://github.com/model-checking/verify-rust-std/actions/workflows/kmir.yml) |
| VeriFast for Rust | [](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml) |
+
+
+
diff --git a/doc/src/tools/kmir.md b/doc/src/tools/kmir.md
new file mode 100644
index 0000000000000..2d932c8fbb53b
--- /dev/null
+++ b/doc/src/tools/kmir.md
@@ -0,0 +1,472 @@
+## 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 Public / 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:
+
+
+
+
+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. KMIR is designed to provide sound
+assurances about undefined behavior (UB) in Rust’s MIR. Rather than statically
+over‑approximating or flagging UB at every unsafe block, KMIR models the full
+MIR semantics, including UB transitions, using a **refusal-to-execute** strategy.
+This means that if symbolic execution reaches a MIR instruction and cannot prove
+that executing it would not result in UB (e.g., an out-of-bounds pointer dereference
+or an unchecked arithmetic overflow), execution halts in a `UB DETECTED` state.
+This state cannot be unified with a valid target state in the proof, so the proof
+fails. KMIR systematically explores all feasible paths under the user-supplied
+preconditions. Only when **every** path terminates without hitting UB *and*
+satisfies the target property does KMIR declare the program UB-free (and correct
+for the property). This ensures that any “no UB” claim holds under the sole assumption
+that KMIR’s implementation is correct.
+
+Programs modelled in K Framework can be executed _symbolically_, i.e., operating
+on abstract input which is not fully specified but characterized by _path conditions_
+(e.g., that an integer variable holds an unknown but non-negative value).
+
+In practice, KMIR proof harnesses work similarly to property tests. Arguments
+to the entry function are automatically instantiated as fully symbolic values,
+so the proof covers all possible inputs. Post-conditions are expressed using
+`assert!` statements. Pre-conditions can be added using `std::intrinsics::assume`,
+which constrains the symbolic path condition to restrict the inputs under
+consideration. This design allows users to write verification harnesses in
+plain Rust without needing to learn write K (excepting advanced features).
+
+```rust
+#![feature(core_intrinsics)]
+use std::intrinsics::assume;
+
+fn abs_safe(x: i32) {
+ unsafe { assume(x != i32::MIN); }
+ let result = x.abs();
+ assert!(result >= 0);
+}
+```
+
+When KMIR is directed to prove `abs_safe`, `x` is instantiated symbolically.
+The `assume` adds `x != i32::MIN` as a path constraint, and KMIR proves the
+assertion holds for all values satisfying that constraint.
+
+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 Public 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 Solidity 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.
+
+By default, KMIR will attempt to exhaustively unroll a loop. Loop invariants
+have been applied to the verification of the Solana P-Token / SPL-Token
+Equivalence (see Case Study 2.) to summarise the behaviour of iterator [
+[P-Token Loop](https://github.com/runtimeverification/solana-token/blob/proofs/specs/shared/inner_test_validate_owner.rs),
+[P-Token Lemma](https://github.com/runtimeverification/mir-semantics/blob/mk/lemmas-inner_test_validate_owner/kmir/src/kmir/kdist/mir-semantics/symbolic/inner_test_validate_owner.md)
+].
+
+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:
+
+
+
+
+## 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 symbolic
+ 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.
+
+## Known Limitations
+
+KMIR is under active development. The following summarises notable limitations
+at the time of writing:
+
+**Language features not yet supported:**
+- Floating point types (`f16`, `f32`, `f64`, `f128`)
+- Heap allocating types: `String`s and `Vec`
+- Smart pointers (`Box`, `Rc`, `Arc`)
+- Async/await
+- Multi-threading and atomics
+- Dynamic trait objects `dyn T`
+
+**Language feature partially supported:**
+- Iterators
+- Casts
+- `unsafe` code (`Unions`, raw pointers, etc.)
+- `usize`/`isize` are modelled as fixed-width, not architecture-dependent
+
+## Steps to Use the Tool
+
+### Installation
+
+3 methods to install KMIR are listed. Recommended is the Nix installation via kup.
+
+
+
+Installing KMIR via kup (cached install shown; first install takes longer)
+
+
+#### Nix (via kup)
+
+The recommended installation method uses
+[`kup`](https://github.com/runtimeverification/kup), the K Framework package
+manager. This installs K Framework, `kmir`, and `stable-mir-json` on your
+system via [Nix](https://nixos.org/).
+
+The following script installs Nix (if not already present) and `kup`:
+
+```bash
+bash <(curl https://kframework.org/install)
+```
+
+Then install `kmir`:
+
+```bash
+kup install kmir
+```
+
+`kmir` is now installed on the path:
+```bash
+kmir --help
+```
+
+#### Docker
+
+KMIR is available as a Docker image on
+[Docker Hub](https://hub.docker.com/r/runtimeverificationinc/kmir/tags).
+The image contains K Framework, the `kmir` tool, and `stable-mir-json`.
+
+The following commands may require `sudo` permissions.
+
+```bash
+docker run --rm \
+ runtimeverificationinc/kmir:ubuntu-jammy-0.4.206 \
+ kmir --help
+```
+
+To run a proof using Docker, mount your working directory into the container:
+
+```bash
+docker run --rm \
+ -u $(id -u):$(id -g) \
+ -v /path/to/your/files:/workspace \
+ runtimeverificationinc/kmir: \
+ kmir prove /workspace/program.rs --proof-dir /workspace/proofs --verbose
+```
+
+The `-u` flag ensures files created inside the container have the correct
+ownership on the host. The `-v` flag mounts a host directory so that input
+files are accessible and proof output persists after the container exits.
+
+#### From source
+
+The tools can be built from source as described in the
+[`mir-semantics` repository](https://github.com/runtimeverification/mir-semantics).
+This requires [Python](https://www.python.org/) >= 3.10,
+[`uv`](https://docs.astral.sh/uv/),
+[K Framework](https://github.com/runtimeverification/k), and Rust via
+[`rustup`](https://rustup.rs/).
+
+```bash
+git clone --recurse-submodules https://github.com/runtimeverification/mir-semantics.git
+cd mir-semantics
+make build
+make stable-mir-json
+```
+
+`kmir` can be invoked via `uv` (from repo root):
+
+```bash
+uv --project kmir/ -- kmir --help
+```
+
+### Usage (Verification)
+
+The `kmir` tool works with Stable MIR extracted from Rust programs via
+[`stable-mir-json`](https://github.com/runtimeverification/stable-mir-json),
+a custom driver for `rustc` that serializes a crate's Stable MIR to JSON.
+
+| Command | Purpose |
+| --- | --- |
+| `kmir prove` | Prove a Rust program (*.rs) terminates without panics or undefined behaviour |
+| `kmir show` | Inspect a static proof graph (nodes, statistics, rule applications) |
+| `kmir view` | Interactive proof viewer |
+| `kmir prune` | Remove a node and its subtree from a proof |
+| `kmir section-edge` | Split a proof edge into finer sections |
+| `kmir link` | Link multiple SMIR JSON files into one (for multi-crate projects) |
+
+To prove a program:
+
+```bash
+kmir prove .rs --proof-dir [--start-symbol ] --verbose
+```
+
+Where `` is the Rust source file to verify, `` is the directory
+where proof artifacts are stored, and `` is the entry function to
+verify (defaults to `main` if omitted).
+
+This invokes `stable-mir-json` internally, then performs an all-path
+reachability proof that the program reaches normal termination under all
+possible inputs. Any statements that would panic or cause undefined behaviour
+terminate execution, so successful completion proves their absence.
+Pre-conditions and post-conditions can be modelled using conditional execution
+and assertions.
+
+To inspect proof results, the proof ID is `.`, e.g., proving
+`program.rs` produces proof ID `program.main`:
+
+```bash
+kmir show . --proof-dir --leaves --statistics
+kmir view . --proof-dir
+```
+
+
+
+kmir prove on passing proof with kmir show (time is shortened, real time is in output)
+
+
+
+
+kmir prove on failing proof with kmir view (time is shortened, real time is in output)
+
+
+#### Useful Prove Flags
+
+Proof state is automatically written to disk at every branch point and leaf
+node. Additional state can be emitted with flags to `kmir prove`.
+
+It is recommended to use `--terminate-on-thunk`, which stops the proof when
+an unevaluated symbolic value (thunk) is encountered. This does not affect
+soundness, but gives feedback of the proof failure from the earliest point
+a K rule could not apply.
+
+If a `--proof-dir ` is supplied, proof progress is written to disk.
+If a proof is cancelled before completion, calling the same command with
+the same `--proof-dir ` will read the state from disk and continue
+the proof from there. Otherwise the `--reload` flag will start the proof
+overwriting the previous entry.
+
+Furthermore, performance for a proof can be increased with parallelism.
+We recommend `--max-workers 4` which empirical evidence suggests is an
+optimal number of workers for a proof.
+
+| Flag | Effect |
+| --- | --- |
+| `--reload` | Discard existing proof progress and restart from scratch |
+| `--terminate-on-thunk` | Stop proof at unevaluated thunks (recommended) |
+| `--break-on-thunk` | Emit state at thunk evaluation |
+| `--break-on-calls` | Emit state at all function and intrinsic calls |
+| `--break-on-function-calls` | Emit state at function calls only |
+| `--break-on-intrinsic-calls` | Emit state at intrinsic calls only |
+| `--break-on-function ` | Emit state when calling a function whose name contains `` (repeatable) |
+| `--max-depth ` | Emit state every steps |
+| `--max-iterations ` | Stop proof after iterations (states are emitted) |
+| `--fail-fast` | Stop proof at the earliest failure (leaves other branches pending) |
+| `--max-workers ` (best 4) | Max workers for parallel execution |
+
+
+## KMIR Case Studies
+
+### Case Study 1: Verify Std Rust Challenge 11
+
+[Challenge 11](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html)
+requires verifying the safety of public unsafe methods for numeric primitives
+in `core::num`. KMIR successfully verified the correctness of all scoped integer
+operations. Float operations remain future work. For details, please visit the
+[proof suite](https://github.com/runtimeverification/mir-semantics/tree/master/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints).
+
+For each unsafe method, two harness files are written:
+
+**PASSING** (
+[unchecked_add.rs](https://github.com/runtimeverification/mir-semantics/blob/master/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add.rs)
+): calls the unsafe method only when its safety precondition holds. KMIR proves
+all paths terminate without UB:
+
+```rust
+fn unchecked_add_u128(a: u128, b: u128) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+```
+
+**FAILING** (
+[unchecked_add-fail.rs](https://github.com/runtimeverification/mir-semantics/blob/master/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/unchecked_add-fail.rs)
+): calls the unsafe method on arbitrary symbolic inputs without a precondition.
+KMIR detects UB on overflow paths and the proof fails:
+
+```rust
+fn unchecked_add_u128(a: u128, b: u128) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b)); // UB
+}
+```
+
+Each failing test has an expected failure state recorded in the
+[show](https://github.com/runtimeverification/mir-semantics/tree/master/kmir/src/tests/integration/data/verify-rust-std/0011-floats-ints/show)
+directory.
+
+The full set of verified methods covers all integer types (i8-i128, u8-u128):
+
+| Method | Types | Status |
+| --- | --- | --- |
+| `unchecked_add` | all integer types | verified |
+| `unchecked_sub` | all integer types | verified |
+| `unchecked_mul` | all integer types | verified |
+| `unchecked_shl` | all integer types | verified |
+| `unchecked_shr` | all integer types | verified |
+| `unchecked_neg` | signed types only | verified |
+| `wrapping_shl` | all integer types | verified |
+| `wrapping_shr` | all integer types | verified |
+| `widening_mul` | u8, u16, u32, u64 | verified |
+| `carrying_mul` | u8, u16, u32, u64 | verified |
+| `to_int_unchecked` | f16, f32, f64, f128 | pending (float support) |
+
+### Case Study 2: Solana P-Token / SPL-Token Equivalence Proofs
+
+KMIR has been used to formally verify the equivalence of the
+[Solana P-Token](https://github.com/runtimeverification/solana-token/tree/proofs/p-token)
+(a compute-optimized rewrite using
+[Pinocchio](https://github.com/anza-xyz/pinocchio)) against the original
+[Solana SPL-Token](https://github.com/runtimeverification/solana-token/tree/proofs/program)
+program.
+
+The verification proves that the P-Token program simulates the SPL-Token
+program: for each SPL-Token state and instruction (a request to perform an
+operation such as Transfer or Burn), there is an equivalent P-Token state
+and instruction that produces the same result. Both programs must agree on
+state transitions and error behaviour.
+
+Each instruction is verified twice (once for each implementation) against a
+shared specification harness that captures the initial account state, invokes
+the instruction processor with symbolic input, and verifies the same
+postcondition holds after execution. 41 proofs are required to demonstrate
+equivalence.
+
+For more details, please see:
+- [Proof Status](https://github.com/runtimeverification/solana-token/issues/24)
+- [Multisig Proof Status](https://github.com/runtimeverification/solana-token/issues/97)
+- [Shared Specifications](https://github.com/runtimeverification/solana-token/tree/proofs/specs)
+- [SPL-Token Implementation](https://github.com/runtimeverification/solana-token/blob/proofs/program/src/processor.rs)
+- [P-Token Implementation](https://github.com/runtimeverification/solana-token/tree/proofs/p-token/src/processor)
+
+A detailed report covering the Solana programming model, the formal
+equivalence methodology, and per-instruction verification conditions is
+available in the
+[equivalence proofs report](https://github.com/runtimeverification/solana-token/blob/proofs/RV_EQUIVALENCE_PROOFS_REPORT.md).
+
+## 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.
diff --git a/kmir-proofs/0011-floats-ints/carrying_mul.rs b/kmir-proofs/0011-floats-ints/carrying_mul.rs
new file mode 100644
index 0000000000000..fbe975d3185f5
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/carrying_mul.rs
@@ -0,0 +1,36 @@
+#![feature(bigint_helper_methods)]
+
+fn main() {
+ carrying_mul_u8(0, 0, 0);
+ carrying_mul_u16(0, 0, 0);
+ carrying_mul_u32(0, 0, 0);
+ carrying_mul_u64(0, 0, 0);
+}
+
+fn carrying_mul_u8(a: u8, b: u8, c: u8) {
+ let (lo, hi) = a.carrying_mul(b, c);
+ let expected = (a as u16) * (b as u16) + (c as u16);
+ assert!(lo == (expected as u8));
+ assert!(hi == ((expected >> u8::BITS) as u8));
+}
+
+fn carrying_mul_u16(a: u16, b: u16, c: u16) {
+ let (lo, hi) = a.carrying_mul(b, c);
+ let expected = (a as u32) * (b as u32) + (c as u32);
+ assert!(lo == (expected as u16));
+ assert!(hi == ((expected >> u16::BITS) as u16));
+}
+
+fn carrying_mul_u32(a: u32, b: u32, c: u32) {
+ let (lo, hi) = a.carrying_mul(b, c);
+ let expected = (a as u64) * (b as u64) + (c as u64);
+ assert!(lo == (expected as u32));
+ assert!(hi == ((expected >> u32::BITS) as u32));
+}
+
+fn carrying_mul_u64(a: u64, b: u64, c: u64) {
+ let (lo, hi) = a.carrying_mul(b, c);
+ let expected = (a as u128) * (b as u128) + (c as u128);
+ assert!(lo == (expected as u64));
+ assert!(hi == ((expected >> u64::BITS) as u64));
+}
diff --git a/kmir-proofs/0011-floats-ints/run-proofs.sh b/kmir-proofs/0011-floats-ints/run-proofs.sh
new file mode 100755
index 0000000000000..2630c71d6346e
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/run-proofs.sh
@@ -0,0 +1,49 @@
+#!/bin/bash
+# Run KMIR proofs for Challenge 11: Safety of Methods for Numeric Primitive Types
+# https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html
+#
+# Usage: ./run-proofs.sh # run passing proofs
+# ./run-proofs.sh --negative # run negative proofs (expect failure)
+
+set -eux
+
+if ! command -v kmir &> /dev/null; then
+ echo "ERROR: kmir not found on PATH"
+ exit 2
+fi
+
+DIR=$(realpath "$(dirname "$0")")
+cd "$DIR"
+
+if [ "${1:-}" = "--negative" ]; then
+ PROOF_DIR=proofs-fail
+ rm -rf "$PROOF_DIR"
+
+ # Negative tests: proofs should FAIL as KMIR detects UB.
+ # If any proof unexpectedly passes, the script exits non-zero.
+ printf '%s\n' \
+ "kmir prove unchecked_add-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_add_u8,unchecked_add_u16,unchecked_add_u32,unchecked_add_u64,unchecked_add_u128,unchecked_add_i8,unchecked_add_i16,unchecked_add_i32,unchecked_add_i64,unchecked_add_i128" \
+ "kmir prove unchecked_sub-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_sub_u8,unchecked_sub_u16,unchecked_sub_u32,unchecked_sub_u64,unchecked_sub_u128,unchecked_sub_i8,unchecked_sub_i16,unchecked_sub_i32,unchecked_sub_i64,unchecked_sub_i128" \
+ "kmir prove unchecked_mul-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_mul_u8,unchecked_mul_u16,unchecked_mul_u32,unchecked_mul_u64,unchecked_mul_u128,unchecked_mul_i8,unchecked_mul_i16,unchecked_mul_i32,unchecked_mul_i64,unchecked_mul_i128" \
+ "kmir prove unchecked_shl-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_shl_u8,unchecked_shl_u16,unchecked_shl_u32,unchecked_shl_u64,unchecked_shl_u128,unchecked_shl_i8,unchecked_shl_i16,unchecked_shl_i32,unchecked_shl_i64,unchecked_shl_i128" \
+ "kmir prove unchecked_shr-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_shr_u8,unchecked_shr_u16,unchecked_shr_u32,unchecked_shr_u64,unchecked_shr_u128,unchecked_shr_i8,unchecked_shr_i16,unchecked_shr_i32,unchecked_shr_i64,unchecked_shr_i128" \
+ "kmir prove unchecked_neg-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_neg_i8,unchecked_neg_i16,unchecked_neg_i32,unchecked_neg_i64,unchecked_neg_i128" \
+ | xargs -P 2 -I{} bash -xc 'if {}; then echo "ERROR: expected failure but passed: {}"; exit 1; fi'
+else
+ PROOF_DIR=proofs
+ rm -rf "$PROOF_DIR"
+
+ # Positive tests: proofs should PASS
+ printf '%s\n' \
+ "kmir prove carrying_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol carrying_mul_u8,carrying_mul_u16,carrying_mul_u32,carrying_mul_u64" \
+ "kmir prove unchecked_add.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_add_u8,unchecked_add_u16,unchecked_add_u32,unchecked_add_u64,unchecked_add_u128,unchecked_add_i8,unchecked_add_i16,unchecked_add_i32,unchecked_add_i64,unchecked_add_i128" \
+ "kmir prove widening_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol widening_mul_u8,widening_mul_u16,widening_mul_u32,widening_mul_u64" \
+ "kmir prove unchecked_sub.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_sub_u8,unchecked_sub_u16,unchecked_sub_u32,unchecked_sub_u64,unchecked_sub_u128,unchecked_sub_i8,unchecked_sub_i16,unchecked_sub_i32,unchecked_sub_i64,unchecked_sub_i128" \
+ "kmir prove unchecked_neg.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_neg_i8,unchecked_neg_i16,unchecked_neg_i32,unchecked_neg_i64,unchecked_neg_i128" \
+ "kmir prove unchecked_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_mul_u8,unchecked_mul_u16,unchecked_mul_u32,unchecked_mul_u64,unchecked_mul_u128,unchecked_mul_i8,unchecked_mul_i16,unchecked_mul_i32,unchecked_mul_i64,unchecked_mul_i128" \
+ "kmir prove unchecked_shl.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_shl_u8,unchecked_shl_u16,unchecked_shl_u32,unchecked_shl_u64,unchecked_shl_u128,unchecked_shl_i8,unchecked_shl_i16,unchecked_shl_i32,unchecked_shl_i64,unchecked_shl_i128" \
+ "kmir prove unchecked_shr.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_shr_u8,unchecked_shr_u16,unchecked_shr_u32,unchecked_shr_u64,unchecked_shr_u128,unchecked_shr_i8,unchecked_shr_i16,unchecked_shr_i32,unchecked_shr_i64,unchecked_shr_i128" \
+ "kmir prove wrapping_shl.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol wrapping_shl_u8,wrapping_shl_u16,wrapping_shl_u32,wrapping_shl_u64,wrapping_shl_u128,wrapping_shl_i8,wrapping_shl_i16,wrapping_shl_i32,wrapping_shl_i64,wrapping_shl_i128" \
+ "kmir prove wrapping_shr.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol wrapping_shr_u8,wrapping_shr_u16,wrapping_shr_u32,wrapping_shr_u64,wrapping_shr_u128,wrapping_shr_i8,wrapping_shr_i16,wrapping_shr_i32,wrapping_shr_i64,wrapping_shr_i128" \
+ | xargs -P 2 -I{} bash -xc '{}'
+fi
diff --git a/kmir-proofs/0011-floats-ints/unchecked_add-fail.rs b/kmir-proofs/0011-floats-ints/unchecked_add-fail.rs
new file mode 100644
index 0000000000000..85680b316bb54
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_add-fail.rs
@@ -0,0 +1,64 @@
+#![feature(unchecked_math)]
+
+fn main() {
+ unchecked_add_u8(0, 0);
+ unchecked_add_u16(0, 0);
+ unchecked_add_u32(0, 0);
+ unchecked_add_u64(0, 0);
+ unchecked_add_u128(0, 0);
+ unchecked_add_i8(0, 0);
+ unchecked_add_i16(0, 0);
+ unchecked_add_i32(0, 0);
+ unchecked_add_i64(0, 0);
+ unchecked_add_i128(0, 0);
+}
+
+fn unchecked_add_u8(a: u8, b: u8) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u16(a: u16, b: u16) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u32(a: u32, b: u32) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u64(a: u64, b: u64) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_u128(a: u128, b: u128) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i8(a: i8, b: i8) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i16(a: i16, b: i16) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i32(a: i32, b: i32) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i64(a: i64, b: i64) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
+
+fn unchecked_add_i128(a: i128, b: i128) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == a.wrapping_add(b));
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_add.rs b/kmir-proofs/0011-floats-ints/unchecked_add.rs
new file mode 100644
index 0000000000000..ef210d2d08ca7
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_add.rs
@@ -0,0 +1,84 @@
+#![feature(unchecked_math)]
+
+fn main() {
+ unchecked_add_u8(0, 0);
+ unchecked_add_u16(0, 0);
+ unchecked_add_u32(0, 0);
+ unchecked_add_u64(0, 0);
+ unchecked_add_u128(0, 0);
+ unchecked_add_i8(0, 0);
+ unchecked_add_i16(0, 0);
+ unchecked_add_i32(0, 0);
+ unchecked_add_i64(0, 0);
+ unchecked_add_i128(0, 0);
+}
+
+fn unchecked_add_u8(a: u8, b: u8) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_u16(a: u16, b: u16) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_u32(a: u32, b: u32) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_u64(a: u64, b: u64) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_u128(a: u128, b: u128) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_i8(a: i8, b: i8) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_i16(a: i16, b: i16) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_i32(a: i32, b: i32) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_i64(a: i64, b: i64) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_add_i128(a: i128, b: i128) {
+ if let Some(expected) = a.checked_add(b) {
+ let result = unsafe { a.unchecked_add(b) };
+ assert!(result == expected);
+ }
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_mul-fail.rs b/kmir-proofs/0011-floats-ints/unchecked_mul-fail.rs
new file mode 100644
index 0000000000000..1fb9684cd9731
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_mul-fail.rs
@@ -0,0 +1,64 @@
+#![feature(unchecked_math)]
+
+fn main() {
+ unchecked_mul_u8(0, 0);
+ unchecked_mul_u16(0, 0);
+ unchecked_mul_u32(0, 0);
+ unchecked_mul_u64(0, 0);
+ unchecked_mul_u128(0, 0);
+ unchecked_mul_i8(0, 0);
+ unchecked_mul_i16(0, 0);
+ unchecked_mul_i32(0, 0);
+ unchecked_mul_i64(0, 0);
+ unchecked_mul_i128(0, 0);
+}
+
+fn unchecked_mul_u8(a: u8, b: u8) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u16(a: u16, b: u16) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u32(a: u32, b: u32) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u64(a: u64, b: u64) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_u128(a: u128, b: u128) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i8(a: i8, b: i8) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i16(a: i16, b: i16) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i32(a: i32, b: i32) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i64(a: i64, b: i64) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
+
+fn unchecked_mul_i128(a: i128, b: i128) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == a.wrapping_mul(b));
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_mul.rs b/kmir-proofs/0011-floats-ints/unchecked_mul.rs
new file mode 100644
index 0000000000000..f364a4d47e412
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_mul.rs
@@ -0,0 +1,84 @@
+#![feature(unchecked_math)]
+
+fn main() {
+ unchecked_mul_u8(0, 0);
+ unchecked_mul_u16(0, 0);
+ unchecked_mul_u32(0, 0);
+ unchecked_mul_u64(0, 0);
+ unchecked_mul_u128(0, 0);
+ unchecked_mul_i8(0, 0);
+ unchecked_mul_i16(0, 0);
+ unchecked_mul_i32(0, 0);
+ unchecked_mul_i64(0, 0);
+ unchecked_mul_i128(0, 0);
+}
+
+fn unchecked_mul_u8(a: u8, b: u8) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_u16(a: u16, b: u16) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_u32(a: u32, b: u32) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_u64(a: u64, b: u64) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_u128(a: u128, b: u128) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_i8(a: i8, b: i8) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_i16(a: i16, b: i16) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_i32(a: i32, b: i32) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_i64(a: i64, b: i64) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_mul_i128(a: i128, b: i128) {
+ if let Some(expected) = a.checked_mul(b) {
+ let result = unsafe { a.unchecked_mul(b) };
+ assert!(result == expected);
+ }
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_neg-fail.rs b/kmir-proofs/0011-floats-ints/unchecked_neg-fail.rs
new file mode 100644
index 0000000000000..35c732a0dcabb
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_neg-fail.rs
@@ -0,0 +1,34 @@
+#![feature(unchecked_neg)]
+
+fn main() {
+ unchecked_neg_i8(0);
+ unchecked_neg_i16(0);
+ unchecked_neg_i32(0);
+ unchecked_neg_i64(0);
+ unchecked_neg_i128(0);
+}
+
+fn unchecked_neg_i8(a: i8) {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i16(a: i16) {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i32(a: i32) {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i64(a: i64) {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == a.wrapping_neg());
+}
+
+fn unchecked_neg_i128(a: i128) {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == a.wrapping_neg());
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_neg.rs b/kmir-proofs/0011-floats-ints/unchecked_neg.rs
new file mode 100644
index 0000000000000..b9c70684c61a3
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_neg.rs
@@ -0,0 +1,44 @@
+#![feature(unchecked_neg)]
+
+fn main() {
+ unchecked_neg_i8(0);
+ unchecked_neg_i16(0);
+ unchecked_neg_i32(0);
+ unchecked_neg_i64(0);
+ unchecked_neg_i128(0);
+}
+
+fn unchecked_neg_i8(a: i8) {
+ if let Some(expected) = a.checked_neg() {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_neg_i16(a: i16) {
+ if let Some(expected) = a.checked_neg() {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_neg_i32(a: i32) {
+ if let Some(expected) = a.checked_neg() {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_neg_i64(a: i64) {
+ if let Some(expected) = a.checked_neg() {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_neg_i128(a: i128) {
+ if let Some(expected) = a.checked_neg() {
+ let result = unsafe { a.unchecked_neg() };
+ assert!(result == expected);
+ }
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_shl-fail.rs b/kmir-proofs/0011-floats-ints/unchecked_shl-fail.rs
new file mode 100644
index 0000000000000..3d35ab3166a0e
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_shl-fail.rs
@@ -0,0 +1,64 @@
+#![feature(unchecked_shifts)]
+
+fn main() {
+ unchecked_shl_u8(0, 0);
+ unchecked_shl_u16(0, 0);
+ unchecked_shl_u32(0, 0);
+ unchecked_shl_u64(0, 0);
+ unchecked_shl_u128(0, 0);
+ unchecked_shl_i8(0, 0);
+ unchecked_shl_i16(0, 0);
+ unchecked_shl_i32(0, 0);
+ unchecked_shl_i64(0, 0);
+ unchecked_shl_i128(0, 0);
+}
+
+fn unchecked_shl_u8(a: u8, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u16(a: u16, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u32(a: u32, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u64(a: u64, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_u128(a: u128, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i8(a: i8, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i16(a: i16, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i32(a: i32, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i64(a: i64, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
+
+fn unchecked_shl_i128(a: i128, b: u32) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == a.wrapping_shl(b));
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_shl.rs b/kmir-proofs/0011-floats-ints/unchecked_shl.rs
new file mode 100644
index 0000000000000..86fde4935a4a6
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_shl.rs
@@ -0,0 +1,84 @@
+#![feature(unchecked_shifts)]
+
+fn main() {
+ unchecked_shl_u8(0, 0);
+ unchecked_shl_u16(0, 0);
+ unchecked_shl_u32(0, 0);
+ unchecked_shl_u64(0, 0);
+ unchecked_shl_u128(0, 0);
+ unchecked_shl_i8(0, 0);
+ unchecked_shl_i16(0, 0);
+ unchecked_shl_i32(0, 0);
+ unchecked_shl_i64(0, 0);
+ unchecked_shl_i128(0, 0);
+}
+
+fn unchecked_shl_u8(a: u8, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_u16(a: u16, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_u32(a: u32, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_u64(a: u64, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_u128(a: u128, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_i8(a: i8, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_i16(a: i16, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_i32(a: i32, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_i64(a: i64, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shl_i128(a: i128, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ let result = unsafe { a.unchecked_shl(b) };
+ assert!(result == expected);
+ }
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_shr-fail.rs b/kmir-proofs/0011-floats-ints/unchecked_shr-fail.rs
new file mode 100644
index 0000000000000..c1192257fb18d
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_shr-fail.rs
@@ -0,0 +1,64 @@
+#![feature(unchecked_shifts)]
+
+fn main() {
+ unchecked_shr_u8(0, 0);
+ unchecked_shr_u16(0, 0);
+ unchecked_shr_u32(0, 0);
+ unchecked_shr_u64(0, 0);
+ unchecked_shr_u128(0, 0);
+ unchecked_shr_i8(0, 0);
+ unchecked_shr_i16(0, 0);
+ unchecked_shr_i32(0, 0);
+ unchecked_shr_i64(0, 0);
+ unchecked_shr_i128(0, 0);
+}
+
+fn unchecked_shr_u8(a: u8, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u16(a: u16, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u32(a: u32, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u64(a: u64, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_u128(a: u128, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i8(a: i8, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i16(a: i16, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i32(a: i32, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i64(a: i64, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
+
+fn unchecked_shr_i128(a: i128, b: u32) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == a.wrapping_shr(b));
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_shr.rs b/kmir-proofs/0011-floats-ints/unchecked_shr.rs
new file mode 100644
index 0000000000000..13d7f806496e1
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_shr.rs
@@ -0,0 +1,84 @@
+#![feature(unchecked_shifts)]
+
+fn main() {
+ unchecked_shr_u8(0, 0);
+ unchecked_shr_u16(0, 0);
+ unchecked_shr_u32(0, 0);
+ unchecked_shr_u64(0, 0);
+ unchecked_shr_u128(0, 0);
+ unchecked_shr_i8(0, 0);
+ unchecked_shr_i16(0, 0);
+ unchecked_shr_i32(0, 0);
+ unchecked_shr_i64(0, 0);
+ unchecked_shr_i128(0, 0);
+}
+
+fn unchecked_shr_u8(a: u8, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_u16(a: u16, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_u32(a: u32, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_u64(a: u64, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_u128(a: u128, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_i8(a: i8, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_i16(a: i16, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_i32(a: i32, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_i64(a: i64, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_shr_i128(a: i128, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ let result = unsafe { a.unchecked_shr(b) };
+ assert!(result == expected);
+ }
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_sub-fail.rs b/kmir-proofs/0011-floats-ints/unchecked_sub-fail.rs
new file mode 100644
index 0000000000000..fd27fa0c4a230
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_sub-fail.rs
@@ -0,0 +1,64 @@
+#![feature(unchecked_math)]
+
+fn main() {
+ unchecked_sub_u8(0, 0);
+ unchecked_sub_u16(0, 0);
+ unchecked_sub_u32(0, 0);
+ unchecked_sub_u64(0, 0);
+ unchecked_sub_u128(0, 0);
+ unchecked_sub_i8(0, 0);
+ unchecked_sub_i16(0, 0);
+ unchecked_sub_i32(0, 0);
+ unchecked_sub_i64(0, 0);
+ unchecked_sub_i128(0, 0);
+}
+
+fn unchecked_sub_u8(a: u8, b: u8) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u16(a: u16, b: u16) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u32(a: u32, b: u32) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u64(a: u64, b: u64) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_u128(a: u128, b: u128) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i8(a: i8, b: i8) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i16(a: i16, b: i16) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i32(a: i32, b: i32) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i64(a: i64, b: i64) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
+
+fn unchecked_sub_i128(a: i128, b: i128) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == a.wrapping_sub(b));
+}
diff --git a/kmir-proofs/0011-floats-ints/unchecked_sub.rs b/kmir-proofs/0011-floats-ints/unchecked_sub.rs
new file mode 100644
index 0000000000000..8745dd6d3a2d0
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/unchecked_sub.rs
@@ -0,0 +1,84 @@
+#![feature(unchecked_math)]
+
+fn main() {
+ unchecked_sub_u8(0, 0);
+ unchecked_sub_u16(0, 0);
+ unchecked_sub_u32(0, 0);
+ unchecked_sub_u64(0, 0);
+ unchecked_sub_u128(0, 0);
+ unchecked_sub_i8(0, 0);
+ unchecked_sub_i16(0, 0);
+ unchecked_sub_i32(0, 0);
+ unchecked_sub_i64(0, 0);
+ unchecked_sub_i128(0, 0);
+}
+
+fn unchecked_sub_u8(a: u8, b: u8) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_u16(a: u16, b: u16) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_u32(a: u32, b: u32) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_u64(a: u64, b: u64) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_u128(a: u128, b: u128) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_i8(a: i8, b: i8) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_i16(a: i16, b: i16) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_i32(a: i32, b: i32) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_i64(a: i64, b: i64) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
+
+fn unchecked_sub_i128(a: i128, b: i128) {
+ if let Some(expected) = a.checked_sub(b) {
+ let result = unsafe { a.unchecked_sub(b) };
+ assert!(result == expected);
+ }
+}
diff --git a/kmir-proofs/0011-floats-ints/widening_mul.rs b/kmir-proofs/0011-floats-ints/widening_mul.rs
new file mode 100644
index 0000000000000..806c63d3f541d
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/widening_mul.rs
@@ -0,0 +1,36 @@
+#![feature(bigint_helper_methods)]
+
+fn main() {
+ widening_mul_u8(0, 0);
+ widening_mul_u16(0, 0);
+ widening_mul_u32(0, 0);
+ widening_mul_u64(0, 0);
+}
+
+fn widening_mul_u8(a: u8, b: u8) {
+ let (lo, hi) = a.widening_mul(b);
+ let expected = (a as u16) * (b as u16);
+ assert!(lo == (expected as u8));
+ assert!(hi == ((expected >> u8::BITS) as u8));
+}
+
+fn widening_mul_u16(a: u16, b: u16) {
+ let (lo, hi) = a.widening_mul(b);
+ let expected = (a as u32) * (b as u32);
+ assert!(lo == (expected as u16));
+ assert!(hi == ((expected >> u16::BITS) as u16));
+}
+
+fn widening_mul_u32(a: u32, b: u32) {
+ let (lo, hi) = a.widening_mul(b);
+ let expected = (a as u64) * (b as u64);
+ assert!(lo == (expected as u32));
+ assert!(hi == ((expected >> u32::BITS) as u32));
+}
+
+fn widening_mul_u64(a: u64, b: u64) {
+ let (lo, hi) = a.widening_mul(b);
+ let expected = (a as u128) * (b as u128);
+ assert!(lo == (expected as u64));
+ assert!(hi == ((expected >> u64::BITS) as u64));
+}
diff --git a/kmir-proofs/0011-floats-ints/wrapping_shl.rs b/kmir-proofs/0011-floats-ints/wrapping_shl.rs
new file mode 100644
index 0000000000000..e28de33769a20
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/wrapping_shl.rs
@@ -0,0 +1,72 @@
+fn main() {
+ wrapping_shl_u8(0, 0);
+ wrapping_shl_u16(0, 0);
+ wrapping_shl_u32(0, 0);
+ wrapping_shl_u64(0, 0);
+ wrapping_shl_u128(0, 0);
+ wrapping_shl_i8(0, 0);
+ wrapping_shl_i16(0, 0);
+ wrapping_shl_i32(0, 0);
+ wrapping_shl_i64(0, 0);
+ wrapping_shl_i128(0, 0);
+}
+
+fn wrapping_shl_u8(a: u8, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_u16(a: u16, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_u32(a: u32, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_u64(a: u64, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_u128(a: u128, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_i8(a: i8, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_i16(a: i16, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_i32(a: i32, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_i64(a: i64, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
+
+fn wrapping_shl_i128(a: i128, b: u32) {
+ if let Some(expected) = a.checked_shl(b) {
+ assert!(a.wrapping_shl(b) == expected);
+ }
+}
diff --git a/kmir-proofs/0011-floats-ints/wrapping_shr.rs b/kmir-proofs/0011-floats-ints/wrapping_shr.rs
new file mode 100644
index 0000000000000..ab182baf0832d
--- /dev/null
+++ b/kmir-proofs/0011-floats-ints/wrapping_shr.rs
@@ -0,0 +1,72 @@
+fn main() {
+ wrapping_shr_u8(0, 0);
+ wrapping_shr_u16(0, 0);
+ wrapping_shr_u32(0, 0);
+ wrapping_shr_u64(0, 0);
+ wrapping_shr_u128(0, 0);
+ wrapping_shr_i8(0, 0);
+ wrapping_shr_i16(0, 0);
+ wrapping_shr_i32(0, 0);
+ wrapping_shr_i64(0, 0);
+ wrapping_shr_i128(0, 0);
+}
+
+fn wrapping_shr_u8(a: u8, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_u16(a: u16, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_u32(a: u32, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_u64(a: u64, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_u128(a: u128, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_i8(a: i8, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_i16(a: i16, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_i32(a: i32, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_i64(a: i64, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
+
+fn wrapping_shr_i128(a: i128, b: u32) {
+ if let Some(expected) = a.checked_shr(b) {
+ assert!(a.wrapping_shr(b) == expected);
+ }
+}
diff --git a/kmir-proofs/README.md b/kmir-proofs/README.md
new file mode 100644
index 0000000000000..76f899d7ce20f
--- /dev/null
+++ b/kmir-proofs/README.md
@@ -0,0 +1,107 @@
+# 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.
+
+The following description assumes that the `kmir` tool and `stable-mir-json` are
+installed and available on the path.
+
+## Program Property Proofs in KMIR
+
+The most user-friendly way to create and run a proof in KMIR is the `prove-rs`
+functionality, which allows a user to prove that a given program will
+run to completion without an error.
+
+Desired post-conditions of the program, such as properties of the computed result,
+can be formulated as simple `assert` statements. Preconditions can be modelled
+as `if` statements which skip execution altogether if the precondition is not met.
+They can be added to a test function using the following macro:
+
+```Rust
+/// If the precondition is not met, the program is not executed (exits cleanly, ex falso quodlibet)
+macro_rules! precondition {
+ ($pre:expr, $block:expr) => {
+ if $pre { $block }
+ };
+}
+```
+If the precondition is not met, the statements in `$block` won't be executed. If
+the `$block` is executed, we can assume that the boolean expression `$pre` holds
+true.
+
+KMIR will stop executing the program as soon as any undefined behaviour arises
+from the executed statements. Therefore, running to completion proves the absense
+of undefined behaviour, as well as the post-conditions expressed as assertions
+(possibly under the assumption of preconditions modelled using the above macro).
+
+## Example: Proving Absense of Undefined Behaviour in `unchecked_*` arithmetic
+
+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.
+
+
+As an example of a property proof in KMIR, consider the following function which
+tests that `unchecked_add` does not trigger undefined behaviour if its safety
+conditions are met by the arguments:
+
+```Rust
+fn unchecked_add_i32(a: i32, b: i32) {
+
+ precondition!(
+ ((a as i128 + b as i128) <= i32::MAX as i128) &&
+ ( a as i128 + b as i128 >= i32::MIN as i128),
+ // =========================================
+ unsafe {
+ let result = a.unchecked_add(b);
+ assert!(result as i128 == a as i128 + b as i128)
+ }
+ );
+}
+```
+
+According to the [documentation of the unchecked_add function for the i32 primitive
+type](https://doc.rust-lang.org/std/primitive.i32.html#method.unchecked_add),
+
+> "This results in undefined behavior when `self + rhs > i32::MAX` or
+> `self + rhs < i32::MIN`, i.e. when `checked_add` would return `None`"
+
+
+If the sum of the two arguments `a` and `b` does not exceed the bounds of type `i32`
+(checked by computing it in range `i128`), the `unchecked_add` function should
+not trigger undefined behaviour and produce the correct result, expressed by the
+`precondition` macro and the assertion at the end of the unsafe block.
+
+To run the proof, we execute `kmir prove-rs` and provide the function name as
+the `--start-symbol`. The `--verbose` option allows for watching the proof being
+executed, the `--proof-dir` will contain data about the proof's intermediate states
+that can be inspected afterwards.
+
+```shell
+kmir prove-rs unchecked_arithmetic.rs --proof-dir proof --start-symbol unchecked_add_i32 --verbose
+```
+
+After the proof finishes, the prover reports whether it passed or failed, and some
+details about the execution control flow graph (such as number of nodes and leaves).
+The graph can be shown or interactively inspected using commands `kmir show` and `kmir view`:
+
+```shell
+kmir view --proof-dir proof unchecked_arithmetic.unchecked_add_i32
+kmir show --proof-dir proof unchecked_arithmetic.unchecked_add_i32 [--no-full-printer]
+```
+
+While `kmir show` only prints the control flow graph, `kmir view` opens an interactive
+viewer where the graph nodes can be selected and displayed in different modes.