Drop using container approach sponsored by WFs, settings just run it

Author: F-WRunTime

.github/workflows/container-test.yml

@@ -51,17 +51,18 @@ jobs:
     needs: publish-test-image
     permissions:
       packages: read
-    container:
-      image: ${{ needs.publish-test-image.outputs.image-name }}:ubuntu-jammy-${{ needs.publish-test-image.outputs.kmir-version }}_${{ needs.publish-test-image.outputs.k-version }}-${{ needs.publish-test-image.outputs.short-sha }}
-      credentials:
-        username: ${{ github.repository_owner }}
-        password: ${{ secrets.GITHUB_TOKEN }}
     steps:
       - name: Checkout code
         uses: actions/checkout@v4
         with:
           submodules: recursive
-          ref: sample-challenge-11-proofs  
+          ref: sample-challenge-11-proofs
+      - name: Start KMIR Container
+        run: |
+          docker run --detach --rm --name kmir --tty --interactive ${{ needs.publish-test-image.outputs.image-name }}:ubuntu-jammy-${{ needs.publish-test-image.outputs.kmir-version }}_${{ needs.publish-test-image.outputs.k-version }}-${{ needs.publish-test-image.outputs.short-sha }}
+      - name: Stream files to Container
+        run: |
+          docker cp rust-verification-proofs kmir:/home/kmir/
       - name: kmir Prove
         run: |
           cd rust-verification-proofs/unchecked_add

rust-verification-proofs/README.md

@@ -0,0 +1,95 @@
+# Formal Rust Code Verification Using KMIR  
+
+This subrepository contains a collection of programs and specifications that aim to illustrate how KMIR can be used to validate the properties of Rust programs and the Rust language itself. The code made available in this repository was developed taking as references the challenges present on the [Verify Rust Standard Library Effort](https://model-checking.github.io/verify-rust-std/intro.html).
+
+## Table of Contents
+
+
+- [Project Setup](#project-setup)
+- [Proof 1: Proving a Maximum Finding Function That only Uses `lower-than (<)`](#proof-1-proving-a-maximum-finding-function-that-only-uses-lower-than)
+- [Proof 2: Proving Unsafe Arithmetic Operations](#proof-2-proving-unsafe-arithmetic-operations)
+
+## Project Setup
+
+In order to run and explore the proofs elaborated here, make sure that KMIR can be locally executed in your machine following the instructions available in [this repository's README file](https://github.com/runtimeverification/mir-semantics/tree/sample-challenge-11-proofs).
+
+[Be sure to have Rust installed](https://www.rust-lang.org/tools/install) in your machine, have the specific components and toolchain necessary to run KMIR. To guarantee it, with `rustup` installed, run the following commands: 
+
+```bash
+rustup component add rust-src rustc-dev llvm-tools-preview
+rustup toolchain install nightly-2024-11-29
+rustup default nightly-2024-11-29
+```
+
+**(Optional)** Additionally, if you would like to build your own code specifications to be proven with KMIR, install the [Rust Stable MIR Pretty Printing](https://github.com/runtimeverification/stable-mir-json/tree/20820cc6abd8fd22769931a3f8754ee35ab24c05) tool. It won't be necessary to install it if you'd like to understand how KMIR works and to execute its proofs, but it is needed currently to help us traverse program states, as seen in the [steps needed to achieve Proof 1's specification](https://github.com/runtimeverification/mir-semantics/tree/sample-challenge-11-proofs/rust-verification-proofs/maximum-proof). To install the Rust Stable MIR Pretty Printing tool, in the root of this project, run:
+
+```bash
+git submodule update --init --recursive
+make stable-mir-json
+```
+
+The usage of this tool will be abstracted in the future, removing the need to construct claims manually.
+
+## Proof 1: 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(a, max(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.
+
+Information on how the specification was created can be found in the longer [description of `maximum-proof`](https://github.com/runtimeverification/mir-semantics/tree/sample-challenge-11-proofs/rust-verification-proofs/maximum-proof).
+
+To run this proof in your terminal from this folder, execute:
+
+```Bash
+cd maximum-proof
+poetry -C ../../kmir/ run -- kmir prove run  $PWD/maximum-spec.k --proof-dir $PWD/proof
+```
+
+## Proof 2: Proving Unsafe Arithmetic Operations
+
+The proofs in this section 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. Here, we implement proof of concepts of how KMIR can be used to prove the following unsafe methods according to their undefined behaviors: `unchecked_add`, `unchecked_sub`, `unchecked_mul`, `unchecked_shl`, `unchecked_shr`, and `unchecked_neg`.
+
+For these functions, the proofs were carried out using variables of the `i16` integer type, and the criteria for triggering undefined behaviors for these methods were obtained in the [i16 type documentation page](https://doc.rust-lang.org/std/primitive.i16.html).
+
+To obtain the specifications that prove the presence/absence of undefined behavior for these functions, analogous processes to the ones discussed in [Proof 1](#proof-1-proving-a-maximum-finding-function-that-only-uses-lower-than) were performed.
+
+For an illustration of how we specify the requirements of the proof, which, in this case, are the assertions that would help us detect the presence/absence of undefined behavior in the unsafe methods, let's explore how we can prove safety conditions for the `unchecked_add` operation. Consider the following function:
+
+https://github.com/runtimeverification/mir-semantics/blob/e2de329d009cde25f505819d7c8c9815571db9e7/rust-verification-proofs/unchecked_add/unchecked-add.rs#L11-L14
+
+`unchecked_op` is a function that receives two `i16` arguments and executes an `unchecked_add` of the first parameter by the second, returning an `i16` value resulting from this operation. 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), considering the safety of this function "This results in undefined behavior when `self + rhs > i16::MAX or self + rhs < i16::MIN`, i.e. when `checked_add` would return `None`". By the process further disclosed in Proof 1, we can obtain a valid representation of a function call for `unchecked_op` and modify the variable values to be symbolic. The next step is to define the conditions these values should meet to verify safety conditions elaborated for `unchecked_add`. To this goal, see the following code snippet:
+
+https://github.com/runtimeverification/mir-semantics/blob/e2de329d009cde25f505819d7c8c9815571db9e7/rust-verification-proofs/unchecked_add/unchecked-op-spec.k#L66-L73
+
+The parameters for `unchecked_add` in this specification for KMIR are represented as A and B, which now are symbolic values. To specify the goal of our verification process, we implemented the above code snippet into the specification, which adds a requirement to the execution of our symbolic execution engine. In other words, our proof will only be successful if the specified requirements above are respected. 
+
+In this `requires` clause, first, we use the semantics of K to specify A and B's boundaries, as `i16`s: `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)`. The next section of this `requires` clause specifies the safety conditions for the `unchecked_add` method: `andBool A +Int B <Int (1 <<Int 15) andBool 0 -Int (1 <<Int 15) <=Int A +Int B`.
+
+To run the proofs for these functions, run the commands below, replacing `$METHOD_NAME` with the desired unsafe method name:
+
+```Bash
+cd $METHOD_NAME
+poetry -C ../../kmir/ run -- kmir prove run  $PWD/unchecked-op-spec.k --proof-dir $PWD/proof 
+```
+
+The proof for `unchecked_add` is expected to work as described. Currently, we expect some of the other unsafe arithmetic proofs to manifest unpredicted behavior and end its execution prior to providing the proof's result. This behavior is due to an unfinished implementation of the operations under test and will be addressed in due course.

rust-verification-proofs/maximum-proof/README.md

@@ -0,0 +1,98 @@
+# Turning the max-with-lt program into a property proof 
+
+## Example program that we start from
+
+```rust
+fn main() {
+
+    let a:usize = 42;
+    let b:usize = 22;
+    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(a, max(b, c))
+    let max_ab = if a < b {b} else {a};
+    if max_ab < c {c} else {max_ab}
+}
+```
+
+We want to prove a property of `maximum`:
+- When called with `a`, `b`, and `c`, 
+- the `result` will be greater or equal all of the arguments,
+- and equal to one (or more) of them.
+
+The `main` program above states this using some concrete values of `a`, `b`, and `c`. We will run this program to construct a general symbolic claim and prove it.
+
+In a future version, we will be able to start directly with the `maximum` function call and provide symbolic arguments to it. This will save some manual work setting up the claim file and fits the target of proving based on property tests.
+
+## Extracting Stable MIR for the program
+
+Before we can run the program using the MIR semantics, we have to compile it with a special compiler to extract Stable MIR from it. This step differs a bit depending on whether the program has multiple crates, in our case it is just a simple `rustc` invocation. This creates `main-max-with-lt.smir.json`. (Run the below commmands from the `mir-semantics/rust-verification-proofs/maximum-proof/` directory).
+
+```shell
+cargo -Z unstable-options -C ../../deps/stable-mir-json/ run -- -Zno-codegen --out-dir $PWD $PWD/main-max-with-lt.rs
+```
+The Stable MIR for the program can also be rendered as a graph, using the `--dot` option. This creates `main-max-with-lt.smir.dot`.
+
+```shell
+cargo -Z unstable-options -C ../../deps/stable-mir-json/ run -- --dot -Zno-codegen --out-dir $PWD $PWD/main-max-with-lt.rs
+```
+## Constructing the claim by executing `main` to certain points
+Through concrete execution of the parsed K program we can interrupt the execution after a given number of rewrite steps to inspect the intermediate state. This will help us with writing our claim manually until the process is automated.
+
+1. The program (`main`) reaches the call to `maximum` after 22 steps.  
+   The following command runs it and displays the resulting program state.
+
+    ```shell
+    poetry -C ../../kmir/ run -- kmir run $PWD/main-max-with-lt.smir.json --depth 22 | less -S
+    ```
+    - Arguments `a`, `b`, and `c` are initialised to `Integer`s as `locals[1]` to `locals[3]`
+    - A `call` terminator calling function `ty(25)` is executed next (front of the `k` cell)
+    - The function table contains `ty(25) -> "maximum" code.
+    - Other state (how `main` continues, its other local variables, and some internal functions) is relevant to the proof we want to perform.
+2. The program executes for a total of 92 steps to reach the point where it `return`s from `maximum`.  
+   The following command runs it and displays the resulting program state.
+
+    ```shell
+    poetry -C ../../kmir/ run -- kmir run $PWD/main-max-with-lt.smir.json --depth 92 | less -S
+    ```
+    - The value `locals[0]` is now set to an `Integer`. This will be the target of our assertions.
+    - A `return` terminator is executed next (front of the `k` cell), it will return `locals[0]`
+    - It should be an `Integer` with the desired properties as stated above
+
+State 1. defines our start state for the claim. Irrelevant parts are elided (replaced by variables). 
+* The code of the `maximum` function in the `functions` table needs to be kept. We also keep its identifier `ty(25)`. Other functions can be removed (we won't perform a return).
+* The `call` terminator is kept, calling `ty(25)` with arguments from `locals[1,2,3]`. `target` is modified to be `noBasicBlockIdx` to force termination of the prover (no block to jump back to).
+* The four locals `0` - `3` are required in their original order to provide the function arguments. The values of `a`, `b`, and `c` in locals `1` - `3` are replaced with symbolic variables used in the proof.
+* We could keep all other locals but do not have to (however it is important that the list of locals has a known length).
+* `main`s other details in `currentFrame` are irrelevant and elided.
+
+
+State 2. is the end state, where all that matters is the returned value.
+
+* The `locals` list should contain this `?RESULT` value at index `0`
+* The `?RESULT` value should have the properties stated (equivalent to the assertion in `main`)
+* Because of the modified `target`, the program should end, i.e., have an `#EndProgram` in the `k` cell.
+
+The above is written as a _claim_ in K framework language into a `maximum-spec.k` file.
+Most of the syntax can be copied from the output of the `kmir run` commands above, and irrelevant parts replaced by `_` (LHS) or `?_` (RHS).
+
+Alternatively, it is possible to construct a claim that the entire rest of the program after initialising the variables will result in the desired `?RESULT`, i.e., the assertion in `main` is executed successfully and the program ends in `#EndProgram` after checking it. This would require more steps.
+
+## Running the prover on the claim and viewing the proof
+Now that we have constructed claim, we can run use the KMIR verifier to perform symbollic execution, and can view the state of proof through the KMIR proof viewer.
+```shell
+poetry -C ../../kmir/ run -- kmir prove run  $PWD/maximum-spec.k --proof-dir $PWD/proof
+```
+
+The proof steps are saved in the `$PWD/proof` directory for later inspection using `kmir prove view`. This is especially important when the proof does _not_ succeed immediately.
+
+```shell
+poetry -C ../../kmir/ run -- kmir prove view MAXIMUM-SPEC.maximum-spec --proof-dir $PWD/proof
+```

rust-verification-proofs/maximum-proof/main-max-with-lt.rs

@@ -0,0 +1,18 @@
+
+fn main() {
+
+    let a:usize = 42;
+    let b:usize = 22;
+    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(a, max(b, c))
+    let max_ab = if a < b {b} else {a};
+    if max_ab < c {c} else {max_ab}
+}