Release notes are the following:

### Major Changes
* Fix compilation issue with proc_macro2  (v1.0.80+) and Kani v0.49.0
(model-checking#3138).

### What's Changed
* Implement valid value check for `write_bytes` by @celinval in
model-checking#3108
* Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

**Full Changelog**:
model-checking/kani@kani-0.49.0...kani-0.50.0

…-checking#3149)

The toolchain upgrade itself didn't require any modification, but it
looks like the rust toolchain script includes any untracked files to the
PR, which is the root cause of the model-checking#3146 CI failure.

Thus, I made the following changes (each one of them in its own commit):
  1. Moved the upgrade step to its own script.
  2. Added a bit of debugging and doc to the script.
  3. Added a new step that cleans the workspace before the PR creation.
  4. Actually update the toolchain.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Update Rust toolchain from nightly-2024-04-18 to nightly-2024-04-19
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
rust-lang/rust@becebb3
up to
rust-lang/rust@e3181b0.

I would like to propose that we stabilize the cover statement as is. Any
further improvements or changes can be done separately, with or without
an RFC.

I am also updating the contracts RFC status since parts of it have been
integrated to Kani, but it is still unstable.

### Call-out

This PR requires at least 2 approvals.

Update Rust toolchain from nightly-2024-04-19 to nightly-2024-04-20
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
rust-lang/rust@e3181b0
up to
rust-lang/rust@f9b1614.

…3140)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`2d5e891` to `5f88e54`.

Dependency upgrade resulting from `cargo update`.

Update Rust toolchain from nightly-2024-04-20 to nightly-2024-04-21
without any other source changes.
This is an automatically generated pull request. If any of the CI checks
fail, manual intervention is required. In such a case, review the
changes at https://github.com/rust-lang/rust from
rust-lang/rust@f9b1614
up to
rust-lang/rust@dbce3b4.

…3159)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`5f88e54` to `9730578`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/9730578c0d562d80bbbe663161b3a5408ed3116c"><code>9730578</code></a>
chore: release 1.37.0 (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2187">#2187</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/b862ad982859f03d7e45f5d6291f749697a04a0f"><code>b862ad9</code></a>
s2n-quic-dc: initial commit (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2185">#2185</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/e0f224b848e725f94e7c9050ca1dfec16eb39bd8"><code>e0f224b</code></a>
feat(s2n-quic-core): allow forced PTO transmissions (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2130">#2130</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/bfb921daed2330c21202d441594a538458a3e5f2"><code>bfb921d</code></a>
feat(s2n-quic-core): Add ability to create an incremental reader
initialized ...</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/23b07e41b6ead9621972cb0687fc3610540f7f77"><code>23b07e4</code></a>
feat(s2n-quic): allow disabling active connection migration support (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2182">#2182</a>)</li>
<li>See full diff in <a
href="https://github.com/aws/s2n-quic/compare/5f88e549821518e71b550faf353a8b9970a29deb...9730578c0d562d80bbbe663161b3a5408ed3116c">compare
view</a></li>
</ul>
</details>
<br />


Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.

[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)

---

<details>
<summary>Dependabot commands and options</summary>
<br />

You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)


</details>

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

Fixes cargo audit CI job by updating `rustix`.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

We had a spurious update attempt logged in model-checking#3155 for the job prior to
this fix would empty out the version strings. This was caused by use of
undefined variables.

Resolves: model-checking#3155

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: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

Dependency upgrade resulting from `cargo update`.

Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>

…3166)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`9730578` to `1436af7`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/1436af712b6e73edc11640dc7c3cae23e456c0a8"><code>1436af7</code></a>
ci: Remove neqo from required resumption test clients (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2191">#2191</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/c0bcef639de0e2a6a89202e84c9933d99d431047"><code>c0bcef6</code></a>
build: remove --cfg s2n_quic_unstable (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2190">#2190</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/fed54a59dcfdbc70e7c3c2d4b1cf3c4991ad4403"><code>fed54a5</code></a>
feat(s2n-quic-platform): make message methods public (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2189">#2189</a>)</li>
<li>See full diff in <a
href="https://github.com/aws/s2n-quic/compare/9730578c0d562d80bbbe663161b3a5408ed3116c...1436af712b6e73edc11640dc7c3cae23e456c0a8">compare
view</a></li>
</ul>
</details>
<br />


Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.

[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)

---

<details>
<summary>Dependabot commands and options</summary>
<br />

You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)


</details>

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

…hecking#3134)

The Rust specification does not guarantee that ZST-typed symbols are
backed by unique objects, and `rustc` appears to make use of this as can
be demonstrated for both locals and statics. For parameters no such
example has been found, but as there remains a lack of a guarantee we
err on the safe side.

Resolves: model-checking#3129

This PR modifies the pattern used to exclude files from the copyright
check for `expected` files. This ensures we check the copyright in files
under `tests/expected/` while it skips the check for `expected` and
`*.expected` files. It also adds/modifies copyright headers for some
files that weren't being checked until now.

Resolves model-checking#3141

…del-checking#3169)

This is an additional fix for
model-checking#3098. With this fix, Kani
should be able to check for contracts using modifies clauses that
contain references to types that doesn't implement `kani::Arbitrary`.
The verification will still fail if the same contract is used as a
verified stub.

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Dependency upgrade resulting from `cargo update`.

Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com>

…3174)

Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from
`1436af7` to `6dd41e0`.
<details>
<summary>Commits</summary>
<ul>
<li><a
href="https://github.com/aws/s2n-quic/commit/6dd41e09195bc22dbac93a48f8ab35f8063726dc"><code>6dd41e0</code></a>
build: fix clippy warnings for 1.78 (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2199">#2199</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/de5c33e800ffff14c235ed0ae7d695222f84dcca"><code>de5c33e</code></a>
refactor(s2n-quic-core): improve reassembler error handling (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2197">#2197</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/b085808f4c898f6d4d4e68b14d6a762170fb19b1"><code>b085808</code></a>
chore(s2n-quic-crypto): remove custom aesgcm implementation (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2186">#2186</a>)</li>
<li><a
href="https://github.com/aws/s2n-quic/commit/7188ce4081096256267e44d63f532a40d2c7df64"><code>7188ce4</code></a>
feat(dc): DcSupportedVersions transport parameter (<a
href="https://redirect.github.com/aws/s2n-quic/issues/2193">#2193</a>)</li>
<li>See full diff in <a
href="https://github.com/aws/s2n-quic/compare/1436af712b6e73edc11640dc7c3cae23e456c0a8...6dd41e09195bc22dbac93a48f8ab35f8063726dc">compare
view</a></li>
</ul>
</details>
<br />


Dependabot will resolve any conflicts with this PR as long as you don't
alter it yourself. You can also trigger a rebase manually by commenting
`@dependabot rebase`.

[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)

---

<details>
<summary>Dependabot commands and options</summary>
<br />

You can trigger Dependabot actions by commenting on this PR:
- `@dependabot rebase` will rebase this PR
- `@dependabot recreate` will recreate this PR, overwriting any edits
that have been made to it
- `@dependabot merge` will merge this PR after your CI passes on it
- `@dependabot squash and merge` will squash and merge this PR after
your CI passes on it
- `@dependabot cancel merge` will cancel a previously requested merge
and block automerging
- `@dependabot reopen` will reopen this PR if it is closed
- `@dependabot close` will close this PR and stop Dependabot recreating
it. You can achieve the same result by closing it manually
- `@dependabot show <dependency name> ignore conditions` will show all
of the ignore conditions of the specified dependency
- `@dependabot ignore this major version` will close this PR and stop
Dependabot creating any more for this major version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this minor version` will close this PR and stop
Dependabot creating any more for this minor version (unless you reopen
the PR or upgrade to it yourself)
- `@dependabot ignore this dependency` will close this PR and stop
Dependabot creating any more for this dependency (unless you reopen the
PR or upgrade to it yourself)


</details>

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

We should try to produce a source location wherever possible to ease
debugging and coverage reporting.

Update Cargo.lock with the following package version changes:


```
anyhow      1.0.82  ->  1.0.83
getrandom   0.2.14  ->  0.2.15
num-bigint  0.4.4   ->  0.4.5
ryu         1.0.17  ->  1.0.18
syn         2.0.60  ->  2.0.61
winnow      0.6.7   ->  0.6.8
```

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

For reference, here is the auto-generated changelog

## What's Changed
* Upgrade toolchain to 2024-04-18 and improve toolchain workflow by
@celinval in model-checking#3149
* Automatic toolchain upgrade to nightly-2024-04-19 by @github-actions
in model-checking#3150
* Stabilize cover statement and update contracts RFC by @celinval in
model-checking#3091
* Automatic toolchain upgrade to nightly-2024-04-20 by @github-actions
in model-checking#3154
* Bump tests/perf/s2n-quic from `2d5e891` to `5f88e54` by @dependabot in
model-checking#3140
* Automatic cargo update to 2024-04-22 by @github-actions in
model-checking#3157
* Automatic toolchain upgrade to nightly-2024-04-21 by @github-actions
in model-checking#3158
* Bump tests/perf/s2n-quic from `5f88e54` to `9730578` by @dependabot in
model-checking#3159
* Fix cargo audit error by @jaisnan in
model-checking#3160
* Fix cbmc-update CI job by @tautschnig in
model-checking#3156
* Automatic cargo update to 2024-04-29 by @github-actions in
model-checking#3165
* Bump tests/perf/s2n-quic from `9730578` to `1436af7` by @dependabot in
model-checking#3166
* Do not assume that ZST-typed symbols refer to unique objects by
@tautschnig in model-checking#3134
* Fix copyright check for `expected` tests by @adpaco-aws in
model-checking#3170
* Remove kani::Arbitrary from the modifies contract instrumentation by
@feliperodri in model-checking#3169
* Automatic cargo update to 2024-05-06 by @github-actions in
model-checking#3172
* Bump tests/perf/s2n-quic from `1436af7` to `6dd41e0` by @dependabot in
model-checking#3174
* Avoid unnecessary uses of Location::none() by @tautschnig in
model-checking#3173


**Full Changelog**:
model-checking/kani@kani-0.50.0...kani-0.51.0

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: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>