Merge branch 'model-checking:main' into transmute_unchecked

.github/workflows/goto-transcoder.yml

@@ -0,0 +1,37 @@
+# This workflow executes the supported contracts in goto-transcoder
+
+name: Run GOTO Transcoder (ESBMC)
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/goto-transcoder.yml'
+      - 'scripts/run-kani.sh'
+      - 'scripts/run-goto-transcoder.sh'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  verify-rust-std:
+    name: Verify contracts with goto-transcoder
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Generate contracts programs
+      - name: Generate contracts
+        run: ./scripts/run-kani.sh --kani-args --keep-temps --only-codegen --target-dir kani/contracts
+
+      # Step 3: Run goto-transcoder
+      - name: Run goto-transcoder
+        run: ./scripts/run-goto-transcoder.sh kani/contracts checked_unchecked.*.out

.github/workflows/kani-metrics.yml

@@ -0,0 +1,42 @@
+name: Kani Metrics Update
+
+on:
+  schedule:
+    - cron: '0 0 * * 0'  # Run at 00:00 UTC every Sunday
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  update-kani-metrics:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout Repository
+      uses: actions/checkout@v4
+      with:
+        submodules: true
+
+    # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
+    - name: Set up Python
+      uses: actions/setup-python@v4
+      with:
+        python-version: '3.x'
+
+    - name: Compute Kani Metrics
+      run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
+
+    - name: Create Pull Request
+      uses: peter-evans/create-pull-request@v7
+      with:
+        commit-message: Update Kani metrics
+        title: 'Update Kani Metrics'
+        body: |
+          This is an automated PR to update Kani metrics.
+          
+          The metrics have been updated by running `./scripts/run-kani.sh --run metrics`.
+        branch: update-kani-metrics
+        delete-branch: true
+        base: main

.gitignore

@@ -26,6 +26,8 @@ library/target
 *.rmeta
 *.mir
 Cargo.lock
+/doc/mdbook-metrics/target
+*.png
 
 ## Temporary files
 *~
@@ -46,7 +48,8 @@ package-lock.json
 ## Kani
 *.out
 
-
+## GOTO-Transcoder
+goto-transcoder
 # Added by cargo
 #
 # already existing elements were commented out

doc/book.toml

@@ -19,5 +19,11 @@ runnable = false
 
 [output.linkcheck]
 
+[preprocessor.metrics]
+# Note that the manifest-path is doc/mdbook-metrics, meaning that to build this book, you need to run "mdbook build doc"
+# rather than "mdbook build" from inside the doc/ directory.
+# We choose the former because our "Build Book" Github workflow runs "mdbook build doc."
+command = "cargo run --manifest-path=doc/mdbook-metrics/Cargo.toml"
+
 [rust]
 edition = "2021"

doc/mdbook-metrics/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "mdbook-kani-metrics"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+mdbook = { version = "^0.4" }
+serde_json = "1.0.132"

doc/mdbook-metrics/src/main.rs

@@ -0,0 +1,106 @@
+use mdbook::book::{Book, Chapter};
+use mdbook::errors::Error;
+use mdbook::preprocess::{CmdPreprocessor, Preprocessor, PreprocessorContext};
+use mdbook::BookItem;
+use std::{env, io, path::Path, process::Command};
+
+fn main() {
+    let mut args = std::env::args().skip(1);
+    match args.next().as_deref() {
+        Some("supports") => {
+            // Supports all renderers.
+            return;
+        }
+        Some(arg) => {
+            eprintln!("unknown argument: {arg}");
+            std::process::exit(1);
+        }
+        None => {}
+    }
+
+    if let Err(e) = handle_preprocessing() {
+        eprintln!("{}", e);
+        std::process::exit(1);
+    }
+}
+
+// Plot the Kani metrics.
+// The mdbook builder reads the postprocessed book from stdout,
+// so suppress all Command output to avoid having its output interpreted as part of the book
+fn run_kani_metrics_script() -> Result<(), Error> {
+    // This will be the absolute path to the "doc/" folder
+    let original_dir = env::current_dir()?;
+    let tools_path = original_dir.join(Path::new("doc/src/tools"));
+
+    let kani_std_analysis_path = Path::new("scripts/kani-std-analysis");
+    env::set_current_dir(kani_std_analysis_path)?;
+
+    Command::new("pip")
+        .args(&["install", "-r", "requirements.txt"])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    Command::new("python")
+        .args(&[
+            "kani_std_analysis.py",
+            "--plot-only",
+            "--plot-dir",
+            &tools_path.to_string_lossy(),
+        ])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    env::set_current_dir(&original_dir)?;
+
+    Ok(())
+}
+
+struct AddKaniGraphs;
+
+impl Preprocessor for AddKaniGraphs {
+    fn name(&self) -> &str {
+        "add-metrics"
+    }
+
+    fn run(&self, _ctx: &PreprocessorContext, mut book: Book) -> Result<Book, Error> {
+        book.for_each_mut(|item| {
+            if let BookItem::Chapter(ch) = item {
+                if ch.name == "Kani" {
+                    add_graphs(ch);
+                    return;
+                }
+            }
+        });
+        Ok(book)
+    }
+}
+
+fn add_graphs(chapter: &mut Chapter) {
+    let new_content = r#"
+## Kani Metrics
+
+Note that these metrics are for x86-64 architectures.
+
+## `core`
+![Unsafe Metrics](core_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
+
+![Safe Metrics](core_safe_metrics.png)
+"#;
+
+    chapter.content.push_str(new_content);
+}
+
+pub fn handle_preprocessing() -> Result<(), Error> {
+    run_kani_metrics_script()?;
+    let pre = AddKaniGraphs;
+    let (ctx, book) = CmdPreprocessor::parse_input(io::stdin())?;
+
+    let processed_book = pre.run(&ctx, book)?;
+    serde_json::to_writer(io::stdout(), &processed_book)?;
+
+    Ok(())
+}

doc/src/SUMMARY.md

@@ -9,7 +9,6 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
 
-
 ---
 
 - [Challenges](./challenges.md)
@@ -27,3 +26,4 @@
   - [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
   - [13: Safety of `CStr`](./challenges/0013-cstr.md)
   - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md)
+  - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md)

doc/src/challenges/0015-intrinsics-simd.md

@@ -0,0 +1,149 @@
+# Challenge 15: Contracts and Tests for SIMD Intrinsics
+
+- **Status:** Open
+- **Reward:** 
+- **Solution:** 
+- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/173
+- **Start date:** 2025/02/01
+- **End date:** 2025/08/01
+
+-------------------
+
+
+## Goal
+
+A number of Rust projects rely on the SIMD intrinsics provided by
+[core::arch](https://doc.rust-lang.org/beta/core/arch/) for
+performance. This includes libraries like [hashbrown]() that are used
+in
+[HashMap](https://doc.rust-lang.org/std/collections/struct.HashMap.html),
+as well as third-party cryptographic libraries like
+[libcrux](https://github.com/cryspen/libcrux) and
+[Dalek](https://github.com/dalek-cryptography/curve25519-dalek) that
+are used in mainstream software projects. 
+
+The goal of this project is to provide testable formal specifications
+for the 100 most commonly used intrinsics for x86_64 and aarch64
+platforms, chosen specifically to cover all the intrinsics used in
+hashbrown and in popular cryptographic libraries.
+
+For each intrinsic, the main goal is to provide contracts in the form
+of pre- and post-conditions, and to verify whether these contracts
+hold when the intrinsics are executed in Rust.  A secondary goal is to
+use these contracts as formal specifications of the intrinsics API
+when doing proofs of Rust programs.
+
+
+## Motivation
+
+Rust is the language of choice for new security-critical and
+performance-sensitive projects, and consequently a number of new
+cryptographic projects use Rust to build their infrastructure and
+trusted computing base. However, the SIMD intrinsics in Rust lack
+documentation and are easy to misuse, and so even the best Rust programmers
+need to wade through Intel or Arm assembly documentation to understand
+the functional behavior of these intrinsics.
+
+Separately, when formally verifying cryptographic libraries, each
+project needs to define its own semantics for SIMD instructions.
+Indeed such SIMD specifications have currently been defined for
+cryptographic verification projects in [F*](https://github.com/hacl-star/hacl-star), 
+[EasyCrypt](https://github.com/jasmin-lang/jasmin), and [HOL Light](https://github.com/awslabs/s2n-bignum/tree/main).
+This specification work is both time-consuming and error-prone,
+there is also no guarantee of consistency between the instruction
+semantics used in these different tools.
+
+Consequently, we believe there is a strong need for a consistent,
+formal, testable specification of the SIMD intrinsics that can aid
+Rust developers. Furthermore, we believe that this
+specification should written in a way that can be used to aid formal
+verification of Rust programs using various proof assistants. 
+
+## Description
+
+Consider the function [`_mm_blend_epi16`](https://doc.rust-lang.org/beta/core/arch/x86_64/fn._mm_blend_epi16.html)
+in [core::arch::x86_64](https://doc.rust-lang.org/beta/core/arch/x86_64/index.html):
+
+```
+pub unsafe fn _mm_blend_epi16(
+    a: __m128i,
+    b: __m128i,
+    const IMM8: i32,
+) -> __m128i
+```
+
+Its description says:
+```
+Blend packed 16-bit integers from a and b using the mask IMM8.
+
+The mask bits determine the selection. A clear bit selects the corresponding element of a, and a set bit the corresponding element of b.
+```
+
+It then points to [Intel's documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_blend_epi16) for the C intrinsic which provides the pseudocode:
+```
+FOR j := 0 to 7
+i := j*16
+IF imm8[j]
+dst[i+15:i] := b[i+15:i]
+ELSE
+dst[i+15:i] := a[i+15:i]
+FI
+ENDFOR
+```
+
+We propose to reflect the behavior of the semantics as described in
+Intel's documentation directly as pre- and post-conditions in Rust.
+
+```
+#[requires(IMM8 >= 0 && IMM8 <= 255)]
+#[ensures(|result|
+    forall (|j| implies(j >= 0 && j < 8,
+        if get_bit(IMM8,j) then
+            get_lane(result, j) == get_lane(b,j)
+        else
+            get_lane(result, j) == get_lane(a,j))))]
+pub unsafe fn _mm_blend_epi16(
+    a: __m128i,
+    b: __m128i,
+    const IMM8: i32,
+) -> __m128i
+```
+
+This contract can then be used to automatically generate tests
+for the intrinsic, which can be put in CI.
+
+As a second layer of assurance, these contracts can be compiled
+to some verification framework and proved to be sound against
+a hand-written model of the intrinsics functions.
+
+Finally, Rust verification toolchains can also rely on this contract
+to model the intrinsics library within their analyses. This would
+enable the verification of Rust applications that rely on SIMD intrinsics.
+
+
+### Assumptions
+
+The contracts we write for the SIMD intrinsics should be well tested
+but, in the end, are hand-written based on the documentation
+of the intrinsics provided by Intel and ARM. Consequently, the
+user must trust that these semantics are correctly written.
+
+When using the contracts within a formal verification project,
+the user will, as usual, have to trust that the verification
+tool correctly encodes the semantics of Rust and performs
+a sound analysis within a clearly documented model.
+
+### Success Criteria
+
+The goal is to annotate >= 100 intrinsics in `core::arch::x86_64` and
+`core::arch::aarch64` with contracts, and all these contracts will be
+tested comprehensively in Rust. These functions should include all the
+intrinsics currently used in standard libraries like
+[hashbrown](https://github.com/rust-lang/hashbrown) (the basis
+of the Rust [HashMap](https://doc.rust-lang.org/std/collections/struct.HashMap.html) implementation).
+
+An additional success criterion is to show that these contracts can be
+used by verification tools to prove properties about example code that
+uses them. Of particular interest is code used in cryptographic
+libraries, but even other standalone examples using SIMD intrinsics
+would be considered valuable. 

doc/src/tools.md

@@ -12,6 +12,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
 | Tool                | CI Status |
 |---------------------|-------|
  | 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)      |