Verify/ptr const slice type #10
Closed
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Create two new workflows: - Rust Tests: Run the Rust repository tests for the standard library. - Kani: Run `kani verify-std` to verify the standard library. Note that we don't have any harness yet to verify.
Add an initial template for challenges, and also a CI status badge for README and tools page. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Adds a section in the book assuming no knowledge from the reader about Kani or the verification effort. Co-authored-by: Felipe R. Monteiro <[email protected]>
…w pointers (#14) Adds the challenge to `Verify the memory safery of core intrinsics using raw pointers` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Michael Tautschnig <[email protected]> Co-authored-by: Celina G. Val <[email protected]>
I also added one proof-of-concept harness to ensure Kani can verify it.
This is a draft challenge about verifying calls to transmute
With path-based filters for CI jobs we cannot consistently use branch protection as jobs marked "required" wouldn't necessarily run on a given PR.
Add contracts to `core::mem::swap` and `core::intrinsics::typed_swap`. Co-authored-by: Michael Tautschnig <[email protected]>
Adds a copyright file to the repository. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Celina G. Val <[email protected]>
The challenges numbers in the index are being counted as a new chapter. Instead convert "Challenges" into a chapter, and add a little blob for the challenges chapter, since mdbook requires all chapters to be a page.
Removes copyright strings, and allows this project to be in contribution model sync with upstream.
Creates an issue template for new issues that are for tracking challenges. Right now, anyone can add a tracking issue for a challenge without the link to the challenge in the runbook. This template will help remind them of the order of creation which would be to first, create the challenge in the runbook, then create the tracking issue. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…ecking#32) This PR adds 1. An empty committee `toml` file as a cache that will be used by the CI workflow to check if the approvers belong to the committee. 2. Some simple guidelines for users to apply to become a part of the committee. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <[email protected]>
In this challenge, we want to look at the safe usage of pointer arithmetic operations. Co-authored-by: Michael Tautschnig <[email protected]> Co-authored-by: Zyad Hassan <[email protected]>
> Please add a description of your PR. > If this is a solution to an open challenge, please explain your solution. > > Don't forget to check our book to ensure your solution satisfy the overall > requirements as well as the challenge success criteria. > By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Adds process/CI workflow to check that the approvers for every PR are in a committee of recognized approvers. This is a much simplified version of the r?bot that rust-lang uses. ## Testing Scenarios ### Happy path What happens when 2 of the approvers are in the committee Run: https://github.com/jaisnan/rust-dev/pull/16/checks?check_run_id=26914353663 ## What if someone not in the list approves, and 1 from the committee approves? In this scenario, we have a committee that consists of someone called "jaisu-1". But if the approvals came from one ID that's recognized, and another called "Jaisu-1" (Note to the reader: "jaisu-1" != "Jaisu-1"), then the workflow fails and the PR merge is (rightfully) blocked. Run: https://github.com/jaisnan/rust-dev/pull/15/checks?check_run_id=26914179444 ## Call-Outs 1. We need to add a requirement through settings that at least 2 approvers are required before merging, and allow anyone to approve (if it's not already the setting). 2. Once the first iteration of a committee is finalized, we can merge this workflow to begin the approval checking. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Fixes: https://github.com/model-checking/verify-rust-std/actions/runs/9878423942/job/27283663117 which is a 403 error from github. [Source for fix](https://stackoverflow.com/questions/70435286/resource-not-accessible-by-integration-on-github-post-repos-owner-repo-ac) Test: https://github.com/jaisnan/rust-dev/pull/22/checks?check_run_id=27285370500 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
These contracts seek to capture what is described in documentation and debug assertions.
In preparation for subtree recreation
This challenge is concerned with verifying the memory safety of BTreeMap's `btree::node` module. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Add contracts for `char_try_from_u32`, `from_u32_unchecked`, `from_u8_unchecked`, `from_u8`, and `as_ascii`. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
The CI job for subtree update timesout because it takes more than 6hrs. While we figure out how to solve that problem, this process makes sure there's an automated way for anyone to update the repo's subtree hosted library, with a one click script/command. The structure of this process follows the (would-be) CI workflow closely i.e 1. Call `scripts/run_update_with_checks.sh` 2. This script in turn calls the other scripts in order 3. Pull and update local `subtree/library` with updates from [rust-lang](https://github.com/rust-lang/rust) 4. Merge `subtree/library` onto local `SYNC-{DATE}` where {DATE} is the date tracked by Kani's `features/verify-rust-std` branch. 5. Update toolchain to the date tracked by kani's `features/verify-rust-std` branch and commit. 6. Test this branch with `check_rustc` which checks for compilation compatibility of the updated library and `check_kani` which checks that Kani's injected harnesses verify as expected. ## Call-out This currently only automates the process of updating the subtree and running all checks on it. After that, the process of issuing a PR from the SYNC-DATE branch of the local repo is still in the responsibility of the dev running the script. There is ongoing work to automate the process of writing/pushing branches as well. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
) Minor changes to documentation to clarify some confusion and make it more accessible. Related to :- model-checking#85 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech <[email protected]>
Currently, this harness takes 21 minutes in CI. The only point of this harness is to verify the contract for pointee types with a non-power of two byte size--17 was an arbitrary choice. Reducing to 5 and changing the solver reduces verification time to 57 seconds on my local machine. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
…d` (model-checking#88) Towards model-checking#53 ### Changes - added contract and harness for `non_null::new` - added contract and harness for `non_null::new_unchecked` The difference between the two APIs is that `non_null::new` can handle null pointers while `non_null::new_unchecked` does not. Therefore the contract for `non_null::new` does not require a `nonnull` pointer. ### Re-validation To re-validate the verification results, run `kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify::non_null_check_new`. This will run both harnesses. All default checks should pass. --------- Co-authored-by: OwO <[email protected]> Co-authored-by: Zyad Hassan <[email protected]>
This PR adds to the documentation in the Verification Tools->Kani section of the [challenge book](https://model-checking.github.io/verify-rust-std/tools/kani.html). ### Changes - New step to help Kani user run specific proofs and identify harness full names. ### Issue I tried to follow step 1 & 2 but Kani could not find the harnesses in the example code. At this point there are many proofs in the library so I couldn't find the full name of the harness in the example code by just running all proofs. I tried to move `example.rs` into `library/core/src/ptr/` and use `--harness ptr::verify::example` or `--harness dummy_proof` but both got `error: no harnesses matched the harness filter`. --------- Co-authored-by: Jaisurya Nanduri <[email protected]> Co-authored-by: Felipe R. Monteiro <[email protected]>
Exercise all public member functions of `Layout` and assert properties over the result. Some of those should, perhaps, become `ensures` clauses. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val <[email protected]>
Verify/ptr const integer types
Adds proofs for composite type - tuple
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Generate slice harness for array
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.