Support contracts & stubs in trait implementations (partial fix) #4250
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
github-actions
bot
added
Z-EndToEndBenchCI
This was referenced Jul 30, 2025
carolynzech
force-pushed
the
trait-implementations
branch
from
1049f78 to
4ed5d8e
Compare
added 8 commits
July 30, 2025 16:55
the default syn error message is just that it expects a function body, which isn't all that useful
carolynzech
force-pushed
the
trait-implementations
branch
from
4870c48 to
78037a1
Compare
tautschnig
approved these changes
Aug 1, 2025
Merged
via the queue into
model-checking:main
with commit Aug 1, 2025
22139f0
16 of 18 checks passed
github-merge-queue bot
pushed a commit
that referenced
this pull request
Aug 7, 2025
from the autogenerated : ## What's Changed * Ensure that contract closures are FnOnce by @vonaka in #4151 * Adjust sized hierarchy for Kani's memory predicates by @tautschnig in #4193 * Update to Rust edition 2024 by @tautschnig in #4197 * `ptr_offset_from`: Replace arithmetic over pointers by offset arithmetic by @tautschnig in #4180 * Automatic cargo update to 2025-07-07 by @github-actions[bot] in #4208 * Bump tests/perf/s2n-quic from `b8f8cca` to `8715fdf` by @dependabot[bot] in #4209 * Upgrade Rust toolchain to 2025-07-04 by @tautschnig in #4199 * Upgrade Rust toolchain to 2025-07-10 by @thanhnguyen-aws in #4215 * Update CBMC dependency to 6.7.1 by @tautschnig in #4178 * Split compiler flags to avoid dependency recompilation by @AlexanderPortland in #4211 * Fix the bug that assign clause cannot be inferred for the inner loop of nested loops by @thanhnguyen-aws in #4179 * Upgrade Rust toolchain to 2025-07-11 by @thanhnguyen-aws in #4219 * Automatic toolchain upgrade to nightly-2025-07-12 by @github-actions[bot] in #4222 * Fix bug: `goto-cc` crash when there are two quantifers in one proof by @thanhnguyen-aws in #4221 * Automatic toolchain upgrade to nightly-2025-07-13 by @github-actions[bot] in #4223 * Automatic cargo update to 2025-07-14 by @github-actions[bot] in #4224 * Cleanup links to issues that have been addressed by @tautschnig in #4200 * Selectively enable and fix (slow) Tokio tests by @tautschnig in #4203 * Bump tests/perf/s2n-quic from `32ba87d` to `1cbd879` by @dependabot[bot] in #4227 * Implement support for Cargo.toml's default-members by @tautschnig in #4201 * Do not invoke memset with count of zero by @tautschnig in #4205 * Support bitwuzla, cvc5, z3 as solver attribute values by @tautschnig in #4218 * Use CBMC's shuffle_vector expression by @tautschnig in #4204 * Move tests from slow/kani back to regular suite by @tautschnig in #4202 * Automatic toolchain upgrade to nightly-2025-07-14 by @github-actions[bot] in #4225 * Enable GitHub Linux/Arm runners in CI by @tautschnig in #3841 * Automatic cargo update to 2025-07-21 by @github-actions[bot] in #4231 * Skip codegen for unneeded harnesses by @AlexanderPortland in #4213 * Strongly type differing compiler args for clarity by @AlexanderPortland in #4220 * Remove StableMIR ICE workaround by @carolynzech in #4235 * Fix bug: Kani unwinds loops with contract in generic function (with -Z loop-contracts) by @thanhnguyen-aws in #4232 * Automatic cargo update to 2025-07-28 by @github-actions[bot] in #4238 * Bump tests/perf/s2n-quic from `1cbd879` to `4938450` by @dependabot[bot] in #4242 * Upgrade Rust toolchain to 2025-07-21 by @tautschnig in #4241 * Remove `pretty_ty` and use rustc_public's formatter instead by @tautschnig in #4243 * Upgrade Rust toolchain to 2025-07-24 by @tautschnig in #4244 * Documentation cleanup of UB detected by Kani by @tautschnig in #4245 * Upgrade Rust toolchain to 2025-07-29 by @tautschnig in #4247 * Automatic toolchain upgrade to nightly-2025-07-30 by @github-actions[bot] in #4253 * Add unstable option prove-safety-only by @tautschnig in #4239 * Set bits_per_byte in byte_extract expressions by @tautschnig in #4255 * `KaniAttributes` Path Resolution Refactor by @carolynzech in #4249 * Automatic toolchain upgrade to nightly-2025-07-31 by @github-actions[bot] in #4256 * Support contracts & stubs in trait implementations (partial fix) by @carolynzech in #4250 * [Breaking Changes] Remove unstable list feature and default memory checks by @carolynzech in #4258 * Upgrade Rust toolchain to 2025-08-01 by @tautschnig in #4261 * Autoharness: add support for references by @tautschnig in #4234 * Turn off debug assertions under `--prove-safety-only` by @tautschnig in #4262 * Automatic toolchain upgrade to nightly-2025-08-02 by @github-actions[bot] in #4264 * Automatic toolchain upgrade to nightly-2025-08-03 by @github-actions[bot] in #4265 * Automatic cargo update to 2025-08-04 by @github-actions[bot] in #4267 * Automatic toolchain upgrade to nightly-2025-08-04 by @github-actions[bot] in #4266 * Introduce thread pool for writing goto binaries in parallel by @AlexanderPortland in #4236 * Major-version update cargo dependencies by @tautschnig in #4240 * Bump tests/perf/s2n-quic from `4938450` to `8f510f0` by @dependabot[bot] in #4270 * Automatic toolchain upgrade to nightly-2025-08-05 by @github-actions[bot] in #4271 * Automatic toolchain upgrade to nightly-2025-08-06 by @github-actions[bot] in #4272 * Avoid updating irrelevant symbols when handling quantifiers by @AlexanderPortland in #4268 * Lazily evaluate debug info by @AlexanderPortland in #4269 * Clone a template `BodyTransformer` to avoid re-initialization by @AlexanderPortland in #4259 * Ensuring that MIR constants are marked as static consts by @vonaka in #4233 * Fix release job dependencies by @tautschnig in #4273 ## New Contributors * @vonaka made their first contribution in #4151 **Full Changelog**: kani-0.64.0...kani-0.65.0 --------- Co-authored-by: Zyad Hassan <[email protected]>
github-merge-queue bot
pushed a commit
that referenced
this pull request
Aug 28, 2025
The recent support for stubbing trait impls #4250 assumed that generic args must be types which caused a crash when they're not. This PR takes into account that case. Resolves #4322 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Support stubs and contracts in trait functions. For now, we don't support generic parameters, so we print an error message telling users that if they try. See #1997 (comment) for what we'd need to do to support that.
Resolves #2524
Towards #1997
Towards #4084
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.