… `non_null::offset_from` (model-checking#93)

Towards model-checking#53

Changes
added contract and harness for non_null::sub
added contract and harness for non_null::sub_ptr

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 both
harnesses. All default checks should pass:

```
SUMMARY:
 ** 0 of 1622 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.3814842s

SUMMARY:
 ** 0 of 1780 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.44192737s

Complete - 2 successfully verified harnesses, 0 failures, 2 total.
```

The proof now only handles the array with a fixed size and uses a random
element in the arr for subtraction. The element is i32 type. Is this ok
for the current stage? Or maybe we need to consider other types such as
i64, etc and maybe change the arr to a bigger size?

---------

Co-authored-by: OwO <[email protected]>
Co-authored-by: Qinyuan Wu <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>

Fix invariant return

Add to_bytes and to_bytes_with_nul harnesses

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