Update text and book

.github/workflows/book.yml

@@ -0,0 +1,59 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This workflow is responsible for building and releasing the book.
+# It should only run when there has been a change to the book files
+# or via manual trigger.
+
+name: Build Book
+on:
+  workflow_dispatch:
+  pull_request:
+    paths:
+      - 'doc/**'
+  push:
+    paths:
+      - 'doc/**'
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Install mdbook
+        run: |
+          cargo install mdbook --version "^0.4" --locked
+          echo "${HOME}/.cargo/bin" >> $GITHUB_PATH
+
+      - name: Install linkchecker
+        run: cargo install mdbook-linkcheck --version "^0.7" --locked
+
+      - name: Build Documentation
+        run: mdbook build doc
+
+      - name: Upload book
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: book/html
+          retention-days: "2"
+
+  deploy:
+    needs: build
+    runs-on: ubuntu-latest
+    if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
+
+    # Grant GITHUB_TOKEN the permissions required to make a Pages deployment
+    permissions:
+      pages: write      # to deploy to Pages
+      id-token: write   # to verify source
+
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4

README.md

@@ -0,0 +1,43 @@
+# Rust std-lib verification
+
+This repository is a fork of the official Rust programming
+language repository, created solely to verify the Rust standard
+library. It should not be used as an alternative to the official
+Rust releases.
+
+The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
+1. Contributing to the core mechanism of verifying the rust standard library
+2. Creating new techniques to perform scalable verification
+3. Apply techniques to verify previously unverified parts of the standard library.
+
+## [Kani](https://github.com/model-checking/kani)
+
+The Kani Rust Verifier is a bit-precise model checker for Rust.
+Kani verifies:
+* Memory safety (e.g., null pointer dereferences)
+* User-specified assertions (i.e `assert!(...)`)
+* The absence of panics (eg., `unwrap()` on `None` values)
+* The absence of some types of unexpected behavior (e.g., arithmetic overflows).
+
+You can find out more about Kani from the [Kani book](https://model-checking.github.io/kani/) or the [Kani repository on Github](https://github.com/model-checking/kani).
+
+## Contact
+
+For questions, suggestions or feedback, feel free to open an [issue here](https://github.com/model-checking/verify-rust-std/issues).
+
+## Security
+
+See [SECURITY](https://github.com/model-checking/kani/security/policy) for more information.
+
+## License
+
+### Kani
+
+Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
+See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details.
+
+## Rust
+
+Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
+
+See [the Rust repository](https://github.com/rust-lang/rust) for details.

doc/book.toml

@@ -0,0 +1,25 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[book]
+title = "Verify Rust Std Lib"
+description = "How & What?"
+authors = ["Kani Developers"]
+language = "en"
+multilingual = false
+
+[build]
+build-dir = "../book"
+
+[output.html]
+site-url = "/verify-rust-std/"
+git-repository-url = "https://github.com/model-checking/verify-rust-std"
+edit-url-template = "https://github.com/model-checking/verify-rust-std/edit/main/doc/{path}"
+
+[output.html.playground]
+runnable = false
+
+[output.linkcheck]
+
+
+[rust]
+edition = "2021"

doc/src/SUMMARY.md

@@ -0,0 +1,15 @@
+# Verify Rust Std Lib
+
+[Introduction](intro.md)
+
+- [General Rules](./general-rules.md)
+  - [Challenge Template](./template.md)
+
+- [Verification Tools](./tools.md)
+  - [Kani](./tools/kani.md)
+
+
+---
+
+# Challenges
+- [Coming soon](./todo.md)

doc/src/general-rules.md

@@ -0,0 +1,83 @@
+# General Rules
+
+## Terms / Concepts
+
+**Verification Target:** [Our repository](https://github.com/model-checking/verify-rust-std) is a fork of the original Rust repository,
+and we kept a copy of the Rust standard library inside the `library/` folder that shall be used as the verification target for all our challenges.
+We will periodically update the `library/` folder to track newer versions of the [official Rust standard library](https://github.com/rust-lang/rust/).
+NOTE: This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation.
+**Challenges:** Each individual verification effort will have a
+tracking issue where contributors can add comments and ask clarification questions.
+You can find the list of [open challenges here](https://github.com/model-checking/verify-rust-std/labels/Challenge).
+
+**Solutions:** Solutions to a problem should be submitted as a single Pull Request (PR) to this repository. 
+The solution should run as part of the CI.
+See more details about [minimum requirements for each solution](general-rules.md#solution-requirements).
+
+
+## Basic Workflow
+
+1. A verification effort will be published in the repository with
+appropriate details, and a tracking issue labeled with “Challenge”
+will be opened, so it can be used for clarifications and questions, as
+well as to track the status of the challenge.
+
+2. Participants should create a fork of the repository where they will implement their proposed solution.
+3. Once they submit their solution for analysis, participants should create a PR against the repository for analysis.
+   Please make sure your solution meets [the minimum requirements described here](general-rules.md#solution-requirements).
+4. Each contribution will be reviewed on a first come, first served basis.
+   Acceptance will be based on a review by a committee.
+5. Once approved by the review committee, the change will be merged into the repository.
+
+## Solution Requirements
+
+A proposed solution to a verification problem will only **be reviewed** if all the minimum requirements below are met:
+
+* Each contribution or attempt should be submitted via a pull request to be analyzed by reviewers. 
+* By submitting the solution, participants confirm that they can use, modify, copy, and redistribute their contribution,
+  under the terms of their choice.
+* The contribution must be automated and should be checked and pass as part of the PR checks.
+* All tools used by the solution must be in [the list of accepted tools](tools.md#approved-tools),
+  and previously integrated in the repository.
+  If that is not the case, please submit a separate [tool application first](todo.md).
+* There is no restriction on the number of contributors for a solution.
+  Make sure you have the rights to submit your solution and that all contributors are properly mentioned.
+* The solution cannot impact the runtime logic of the standard library unless the change is proposed and incorporated
+  into the Rust standard library.
+
+Any exception to these requirements will only be considered if it is specified as part of the acceptance criteria of the
+challenged being solved.
+
+## Call for Challenges
+
+The goal of the effort is to enable the verification of the entire Rust standard library.
+The type of obstacles users face may depend on which part of the standard library you would like to verify. Thus, our challenges are developed with the target of verifying a specific section of the standard library or strengthening existing verification.
+
+Everyone is welcome to submit new challenge proposals for review by our committee.
+Follow the following steps to create a new proposal:
+
+1. Create a tracking issue using the Issue template [Challenge Proposal](todo.md) for your challenge.
+2. In your fork of this repository do the following:
+    1. Copy the template file (`book/src/challenge_template.md`) to `book/src/challenges/<ID_NUMBER>-<challenge-name>.md`.
+    2. Fill in the details according to the template instructions.
+    3. Add a link to the new challenge inside `book/src/SUMMARY.md`
+    4. Submit a pull request.
+3. Address any feedback in the pull request.
+4. If approved, we will publish your challenge and add the “Challenge” label to the tracking issue.
+
+## Tool Applications
+
+Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools):
+
+* Any new tool that participants want to enable will require an application using the Issue template [Tool application](todo.md).
+* The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS
+* A new tool application should clearly specify the differences to existing techniques and provide sufficient background
+  of why this is needed.
+* The tool application should also include mechanisms to audit its implementation and correctness.
+* Once the tool is approved, the participant needs to create a PR that creates a new action that runs the
+  std library verification using the new tool, as well as an entry to the “Approved Tools” section of this book.
+* Once the PR is merged, the tool is considered integrated.
+* The repository will be updated periodically, which can impact the tool capacity to analyze the new version of the repository.
+  I.e., the action may no longer pass after an update.
+  This will not impact the approval status of the tool, however,
+  new solutions that want to employ the tool may need to ensure the action is passing first.

doc/src/intro.md

@@ -0,0 +1,17 @@
+# Verify Rust Standard Library Effort
+
+The Verify Rust Standard Library effort is an ongoing investment that
+targets the verification of the [Rust standard
+library](https://doc.rust-lang.org/std/). The goal of this is
+to provide automated verification that can be used to verify that a
+given Rust standard library implementation is safe.
+
+Efforts are largely classified in the following areas:
+
+1. Contributing to the core mechanism of verifying the rust standard library
+2. Creating new techniques to perform scalable verification
+3. Apply techniques to verify previously unverified parts of the standard library.
+
+
+We encourage everyone to watch this repository to be notified of any
+changes.

doc/src/template.md

@@ -0,0 +1 @@
+# Challenge Template

doc/src/todo.md

@@ -0,0 +1,3 @@
+# 🚧 Under Construction 🚧
+
+This section is still under construction. Please check it back again soon and we’ll have more details for you.

doc/src/tools.md

@@ -0,0 +1,18 @@
+# Verification Tools
+
+The verification tool ecosystem for Rust is rapidly growing, and we welcome the usage of different tools to solve our challenges.
+In this chapter, you can find a list of tools that have already been approved for new solutions,
+what is their CI current status, as well as more details on how to use them.
+
+If the tool you would like to add a new tool to the list of tool applications,
+please see the [Tool Application](general-rules.md#tool-applications) section.
+
+## Approved tools:
+
+| Tool      | CI Status |
+|-----------|-----------|
+ | Kani     | TODO      |
+
+
+
+

doc/src/tools/kani.md

@@ -0,0 +1,7 @@
+# Kani Rust Verifier
+
+The Kani Rust Verifier is a bit-precise model checker for Rust.
+This page will give more details on how to use Kani to verify the standard library.
+You can find more informations about how to install and use Kani in the
+[Kani book](https://model-checking.github.io/kani/).
+

library/portable-simd/README.md

@@ -0,0 +1,59 @@
+# The Rust standard library's portable SIMD API
+![Build Status](https://github.com/rust-lang/portable-simd/actions/workflows/ci.yml/badge.svg?branch=master)
+
+Code repository for the [Portable SIMD Project Group](https://github.com/rust-lang/project-portable-simd).
+Please refer to [CONTRIBUTING.md](./CONTRIBUTING.md) for our contributing guidelines.
+
+The docs for this crate are published from the main branch.
+You can [read them here][docs].
+
+If you have questions about SIMD, we have begun writing a [guide][simd-guide].
+We can also be found on [Zulip][zulip-project-portable-simd].
+
+If you are interested in support for a specific architecture, you may want [stdarch] instead.
+
+## Hello World
+
+Now we're gonna dip our toes into this world with a small SIMD "Hello, World!" example. Make sure your compiler is up to date and using `nightly`. We can do that by running 
+
+```bash
+rustup update -- nightly
+```
+
+or by setting up `rustup default nightly` or else with `cargo +nightly {build,test,run}`. After updating, run 
+```bash
+cargo new hellosimd
+```
+to create a new crate. Finally write this in `src/main.rs`:
+```rust
+#![feature(portable_simd)]
+use std::simd::f32x4;
+fn main() {
+    let a = f32x4::splat(10.0);
+    let b = f32x4::from_array([1.0, 2.0, 3.0, 4.0]);
+    println!("{:?}", a + b);
+}
+```
+
+Explanation: We construct our SIMD vectors with methods like `splat` or `from_array`. Next, we can use operators like `+` on them, and the appropriate SIMD instructions will be carried out. When we run `cargo run` you should get `[11.0, 12.0, 13.0, 14.0]`.
+
+## Supported vectors
+
+Currently, vectors may have up to 64 elements, but aliases are provided only up to 512-bit vectors.
+
+Depending on the size of the primitive type, the number of lanes the vector will have varies. For example, 128-bit vectors have four `f32` lanes and two `f64` lanes.
+
+The supported element types are as follows:
+* **Floating Point:** `f32`, `f64`
+* **Signed Integers:** `i8`, `i16`, `i32`, `i64`, `isize` (`i128` excluded)
+* **Unsigned Integers:** `u8`, `u16`, `u32`, `u64`, `usize` (`u128` excluded)
+* **Pointers:** `*const T` and `*mut T` (zero-sized metadata only)
+* **Masks:** 8-bit, 16-bit, 32-bit, 64-bit, and `usize`-sized masks
+
+Floating point, signed integers, unsigned integers, and pointers are the [primitive types](https://doc.rust-lang.org/core/primitive/index.html) you're already used to.
+The mask types have elements that are "truthy" values, like `bool`, but have an unspecified layout because different architectures prefer different layouts for mask types.
+
+[simd-guide]: ./beginners-guide.md
+[zulip-project-portable-simd]: https://rust-lang.zulipchat.com/#narrow/stream/257879-project-portable-simd
+[stdarch]: https://github.com/rust-lang/stdarch
+[docs]: https://rust-lang.github.io/portable-simd/core_simd

library/portable-simd/crates/core_simd/examples/README.md

@@ -0,0 +1,13 @@
+### `stdsimd` examples
+
+This crate is a port of example uses of `stdsimd`, mostly taken from the `packed_simd` crate.
+
+The examples contain, as in the case of `dot_product.rs`, multiple ways of solving the problem, in order to show idiomatic uses of SIMD and iteration of performance designs.
+
+Run the tests with the command 
+
+```
+cargo run --example dot_product
+```
+
+and verify the code for `dot_product.rs` on your machine.

library/rustc-std-workspace-core/README.md

@@ -0,0 +1,29 @@
+# The `rustc-std-workspace-core` crate
+
+This crate is a shim and empty crate which simply depends on `libcore` and
+reexports all of its contents. The crate is the crux of empowering the standard
+library to depend on crates from crates.io
+
+Crates on crates.io that the standard library depend on need to depend on the
+`rustc-std-workspace-core` crate from crates.io, which is empty. We use
+`[patch]` to override it to this crate in this repository. As a result, crates
+on crates.io will draw a dependency edge to `libcore`, the version defined in
+this repository. That should draw all the dependency edges to ensure Cargo
+builds crates successfully!
+
+Note that crates on crates.io need to depend on this crate with the name `core`
+for everything to work correctly. To do that they can use:
+
+```toml
+core = { version = "1.0.0", optional = true, package = 'rustc-std-workspace-core' }
+```
+
+Through the use of the `package` key the crate is renamed to `core`, meaning
+it'll look like
+
+```
+--extern core=.../librustc_std_workspace_core-XXXXXXX.rlib
+```
+
+when Cargo invokes the compiler, satisfying the implicit `extern crate core`
+directive injected by the compiler.

library/rustc-std-workspace-std/README.md

@@ -0,0 +1,3 @@
+# The `rustc-std-workspace-std` crate
+
+See documentation for the `rustc-std-workspace-core` crate.