Contracts & Harnesses for `unchecked_add` by Yenyun035 · Pull Request #91 · model-checking/verify-rust-std

and others added 14 commits

September 10, 2024 17:11

@Yenyun035

@Yenyun035

@Yenyun035

celinval

yew005 added 2 commits

September 24, 2024 14:16

@feliperodri feliperodri changed the title AWS-Team 2: Contracts & Harnesses for unchecked_add Contracts & Harnesses for unchecked_add

Sep 27, 2024

feliperodri

feliperodri

@Yenyun035

feliperodri

yew005 and others added 3 commits

September 29, 2024 19:47
* Added harnesses for unchecked multiplication (`unchecked_mul`) and shift right (`unchecked_shr`)
* Added a macro and input limits for multiplication proofs
* Reduced duplicity in code by using macros to generate proof harnesses

@Yenyun035 Yenyun035 changed the title Contracts & Harnesses for unchecked_add Contracts & Harnesses for unchecked_add, unchecked_mul, unchecked_shr

Sep 30, 2024

@rajathkotyal

@rajathkotyal

@Yenyun035 Yenyun035 changed the title Contracts & Harnesses for unchecked_add, unchecked_mul, unchecked_shr Contracts & Harnesses for unchecked_add

Oct 2, 2024

@Yenyun035

feliperodri

carolynzech pushed a commit that referenced this pull request

Oct 7, 2024

Dhvani-Kapadia added a commit to danielhumanmod/verify-rust-std that referenced this pull request

Oct 7, 2024

carolynzech pushed a commit that referenced this pull request

Nov 14, 2024
Towards #53

## Changes
Three function contracts & four harnesses:
- added contract and harness for `non_null::add`
- added contract and harness for `non_null::addr`
- added contract and harnesses for `non_null::align_offset`, including
both positive and negative harness that triggers panic. The ensures
clause for `align_offset` is referenced from
[`align_offset`](https://github.com/model-checking/verify-rust-std/pull/69/files)
in `library/core/src/ptr/mod.rs`.


## Revalidation
To revalidate the verification results, run `kani verify-std -Z
unstable-options "path/to/library" -Z function-contracts -Z
mem-predicates --harness ptr::non_null::verify`. This will run all six
harnesses in the module. All default checks should pass:
```
SUMMARY:
 ** 0 of 1556 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.28004378s

Complete - 6 successfully verified harnesses, 0 failures, 6 total.
```
### :exclamation: Warning
Running the above command with the default installed cargo kani will
result in compilation error due to the latest merged from
[PR#91](#91).
Detailed errors are commented under that PR. This issue is waiting to be
resolved.

## TODO:

- Use `Layout` to create dynamically sized arrays in place of fixed size
array in harnesses. This approach currently has errors and is documented
in
[discussion](#104).
- Verify multiple data types: these will be added in future PR.
- Add `requires` clause in contract to constrain `count` to be within
object memory size: there is a current
[issue](#99)
with using `ub_checks::can_write` to get the object size. A workaround
is implemented in the harness.

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 <cmzech@amazon.com>

@Yenyun035 Yenyun035 deleted the c-0011-core-nums-yenyunw-unsafe-ints branch

November 27, 2024 08:10

tautschnig pushed a commit to tautschnig/verify-rust-std that referenced this pull request

Apr 29, 2025
Introduce and use specialized `//@ ignore-auxiliary` for test support files instead of using `//@ ignore-test`

### Summary

Add a semantically meaningful directive for ignoring test *auxiliary* files. This is for auxiliary files that *participate* in actual tests but should not be built by `compiletest` (i.e. these files are involved through `mod xxx;` or `include!()` or `#[path = "xxx"]`, etc.).

### Motivation

A specialized directive like `//@ ignore-auxiliary` makes it way easier to audit disabled tests via `//@ ignore-test`.
  - These support files cannot use the canonical `auxiliary/` dir because they participate in module resolution or are included, or their relative paths can be important for test intention otherwise.

Follow-up to:
- rust-lang#139705
- rust-lang#139783
- rust-lang#139740

See also discussions in:

- [#t-compiler > Directive name for non-test aux files?](https://rust-lang.zulipchat.com/#narrow/channel/131828-t-compiler/topic/Directive.20name.20for.20non-test.20aux.20files.3F/with/512773817)
- [#t-compiler > Handling disabled &model-checking#96;//@ ignore-test&model-checking#96; tests](https://rust-lang.zulipchat.com/#narrow/channel/131828-t-compiler/topic/Handling.20disabled.20.60.2F.2F.40.20ignore-test.60.20tests/with/512005974)
- [#t-compiler/meetings > &model-checking#91;steering&model-checking#93; 2025-04-11 Dealing with disabled tests](https://rust-lang.zulipchat.com/#narrow/channel/238009-t-compiler.2Fmeetings/topic/.5Bsteering.5D.202025-04-11.20Dealing.20with.20disabled.20tests/with/511717981)

### Remarks on remaining unconditionally disabled tests under `tests/`

After this PR, against commit 79a272c, only **14** remaining test files are disabled through `//@ ignore-test`:

<details>
<summary>Remaining `//@ ignore-test` files under `tests/`</summary>

```
tests/debuginfo/drop-locations.rs
4://@ ignore-test (broken, see rust-lang#128971)

tests/rustdoc/macro-document-private-duplicate.rs
1://@ ignore-test (fails spuriously, see issue rust-lang#89228)

tests/rustdoc/inline_cross/assoc-const-equality.rs
3://@ ignore-test (FIXME: rust-lang#125092)

tests/ui/match/issue-27021.rs
7://@ ignore-test (rust-lang#54987)

tests/ui/match/issue-26996.rs
7://@ ignore-test (rust-lang#54987)

tests/ui/issues/issue-49298.rs
9://@ ignore-test (rust-lang#54987)

tests/ui/issues/issue-59756.rs
2://@ ignore-test (rustfix needs multiple suggestions)

tests/ui/precondition-checks/write.rs
5://@ ignore-test (unimplemented)

tests/ui/precondition-checks/read.rs
5://@ ignore-test (unimplemented)

tests/ui/precondition-checks/write_bytes.rs
5://@ ignore-test (unimplemented)

tests/ui/explicit-tail-calls/drop-order.rs
2://@ ignore-test: tail calls are not implemented in rustc_codegen_ssa yet, so this causes 🧊

tests/ui/panics/panic-short-backtrace-windows-x86_64.rs
3://@ ignore-test (rust-lang#92000)

tests/ui/json/json-bom-plus-crlf-multifile-aux.rs
3://@ ignore-test Not a test. Used by other tests

tests/ui/traits/next-solver/object-soundness-requires-generalization.rs
2://@ ignore-test (see rust-lang#114196)
```
</details>

Of these, most are either **unimplemented**, or **spurious**, or **known-broken**. The outstanding one is `tests/ui/json/json-bom-plus-crlf-multifile-aux.rs` which I did not want to touch in *this* PR -- that aux file has load-bearing BOM and carriage returns and byte offset matters. I think those test files that require special encoding / BOM probably are better off as `run-make` tests. See rust-lang#139968 for that aux file.

### Review advice

- Best reviewed commit-by-commit.
- The directive name diverged from the most voted `//@ auxiliary` because I think that's easy to confuse with `//@ aux-{crate,dir}`.

r? compiler

github-actions bot pushed a commit that referenced this pull request

Nov 30, 2025
…uarantees, r=scottmcm

Make explicit that `TypeId`'s layout and size are unstable

Or worded differently, explicitly remark non-stable-guarantee of `TypeId` layout and size.

This PR makes no *additional* guarantees or non-guarantees, it only emphasizes that `TypeId`'s size and layout are unstable like any other `#[repr(Rust)]` types.

This was discussed during [#t-compiler/meetings > &#91;weekly&#93; 2025-10-30 @ 💬](https://rust-lang.zulipchat.com/#narrow/channel/238009-t-compiler.2Fmeetings/topic/.5Bweekly.5D.202025-10-30/near/547949347), where the compiler team discussed a request rust-lang#148265 to have the standard library (and language) commit to `TypeId` guaranteeing a size upper bound of 16 bytes. In the meeting, the consensus was:

- We were sympathetic to the use case discussed in the request PR, however we feel like this stability guarantee is premature, given that there are unresolved questions surrounding the intended purpose of `TypeId`, and concerns surrounding its collision-resistance properties rust-lang#10389 and rust-lang#129014. We would prefer not making any of such guarantee until the collision-resistance concerns are resolved.
- Committing to a stability guarantee on the size upper bound now would close the door to making `TypeId` larger (even if unlikely for perf reasons).

Given that we have previously broken people who asserted the size of `TypeId` is 8 bytes, it was also discussed in the meeting that we should *explicitly* note that the size and layout of `TypeId` is not a stable guarantee, and is subject to changes between Rust releases, and thus cannot be relied upon -- if breakage in people's code is due to that assumption, it will be considered a won't-fix.

- So even if `#[repr(Rust)]` types have unstable size and layout, this PR makes it explicit for `TypeId` since this type can feel "special" and users can be lead into thinking its size and layout is something they can rely upon.

r? `@scottmcm` (or libs/libs-api/lang)