Generate contracts of dependencies as assertions by carolynzech · Pull Request #3802 · model-checking/kani

carolynzech · 2024-12-30T21:43:31Z

Generates contract clauses of dependencies as assertions, with an option --no-assert-contracts to disable it. This works by adding a new contract mode that outputs the original body of the function with its contract clauses asserted. During the FunctionWithContractPass, we use this closure, unless --no-assert-contracts was passed, in which case we use the regular body.

I'm omitting a description of why this is useful from the PR description--there's one in the module documentation, and I want that to be a self-contained explanation (i.e., if something is unclear, I want to fix it there).

(Also did a minor bit of cleanup, renaming ClosureType to ContractMode and moving split_for_remembers to the shared module since it has contract-specific logic.)

Resolves #3326

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

…piler)

…as-assertions

zhassan-aws

Nice, thanks!

Only a few comments.

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

@tautschnig

## What's Changed * Package Docker release step: ensure compiler is installed by @tautschnig in #3789 * Improve `--jobs` UI by @carolynzech in #3790 * Update kissat to v4.0.1 by @remi-delmas-3000 in #3791 * Automatic cargo update to 2024-12-23 by @github-actions in #3792 * Bump tests/perf/s2n-quic from `0b3f892` to `a54686e` by @dependabot in #3793 * Upgrade toolchain to nightly-2024-12-18 by @zhassan-aws in #3794 * Automatic cargo update to 2024-12-30 by @github-actions in #3800 * fix: clippy by @ShoyuVanilla in #3806 * Update dependencies (02.01.2025). by @remi-delmas-3000 in #3809 * Update charon submodule by @zhassan-aws in #3801 * Upgrade toolchain to 2024-12-19 by @zhassan-aws in #3810 * Automatic cargo update to 2025-01-06 by @github-actions in #3812 * Bump tests/perf/s2n-quic from `a54686e` to `ac52a48` by @dependabot in #3813 * Generate contracts of dependencies as assertions by @carolynzech in #3802 * Fix hanging command in `std-analysis.sh` by @carolynzech in #3818 * Add UB checks for ptr_offset_from* intrinsics by @celinval in #3757 * Toolchain update 06-01-2025 by @remi-delmas-3000 in #3814 * Automatic toolchain upgrade to nightly-2025-01-07 by @github-actions in #3820 * Include manifest-path when checking if packages are in the workspace by @qinheping in #3819 ## New Contributors * @ShoyuVanilla made their first contribution in #3806 **Full Changelog**: kani-0.57.0...kani-0.58.0 --------- Co-authored-by: Celina G. Val <celinval@amazon.com>

Several postconditions in NonNull compared raw pointers with `==` or `core::ptr::eq`: as_ptr, new, new_unchecked, the slice as_mut_ptr, and - via ptr::eq - as_ref, as_mut, as_uninit_ref and as_uninit_mut. For wide pointers (T: ?Sized with dyn metadata) such comparisons also compare vtable pointers, whose identity is unspecified in Rust; Kani rejects them with "Reached unstable vtable comparison 'Eq'". With dependency contracts asserted (the Kani default since model-checking/kani#3802), any harness whose call graph evaluates these clauses on a trait-object NonNull fails, e.g. ptr::non_null::verify::non_null_check_from_raw_part_trait (the comparison surfaces in ptr::eq::<dyn SampleTrait>, reached from as_ref's postcondition). Compare with core::ptr::addr_eq instead, which is well-defined for any pointer types. All these functions produce their result directly from `self`, so metadata is preserved by construction, and the accompanying comments already described the intent as address preservation. The casts in the as_uninit_* clauses need explicit turbofish types now that the comparison no longer constrains their type parameter. Verified (Kani 152c6a8c + CBMC 6.10.0): non_null_check_from_raw_part_trait now passes with contracts asserted - this was the last remaining verdict difference on a 125-harness sample between runs with and without --no-assert-contracts. The non_null_check_{as_ref,as_mut,as_uninit*,from_raw_part*,as_ptr,new} harnesses pass in both configurations, with one exception: non_null_check_as_uninit_slice_mut fails with contracts asserted both with and without this change (a pre-existing dereference/alignment issue reached via asserted contracts, tracked separately). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

model-checking#4709) When checking the contract of a function F (`proof_for_contract`), every call to F in the harness's call graph is dispatched to F's contract check closure — including calls made while evaluating *other functions' contract clauses*. Since contracts of dependencies are asserted by default (model-checking#3802), such calls are common: e.g. `NonNull::new`'s postcondition calls `NonNull::as_ptr`, so a `proof_for_contract(as_ptr)` harness in model-checking/verify-rust-std that constructs its input via `NonNull::new` dispatches a clause-context call to the check closure, which fails CBMC's single-top-level-call assertion: ``` Failed Checks: Only a single top-level call to function ... when checking contract ... ``` (With diffblue/cbmc#9149, the failure mode would change to spurious assigns-clause violations from running write-set checking in the clause's context — the dispatch itself is the bug.) ### Fix Track clause evaluation at runtime: the contract macros bracket every requires / ensures / modifies / history expression with `enter_contract_clause` / `exit_contract_clause`, which maintain a depth counter in `kani_core`. The contract transformation pass then computes the contract mode for check modes as `mode * (1 - in_contract_clause())` instead of a constant (branch-free: one call, one cast, two integer ops), dispatching clause-context calls to the original body (mode 0). The original body has exact semantics and — unlike dispatching to the contract replacement — does not require the return type to implement `Arbitrary`. Details worth reviewer attention: * `proof_for_contract` harnesses (and automatic harnesses) reset the depth counter at harness entry, since statics are not reliably zero-initialized in every configuration (caught by `modifies/field_pass.rs`). * `enter/exit_contract_clause` are exported with a `__VERIFIER` symbol prefix so CBMC's DFCC treats them as verification-internal and does not flag the counter update as an assigns-clause violation of the function under contract checking (caught by `generic_infinity_recursion.rs`; see `dfcc_is_cprover_function_symbol` in CBMC). * The counter uses saturating arithmetic: DFCC havocs static state inside the enforced region, so the depth value there is arbitrary. All reads occur between an enter/exit pair where the depth is at least 1 regardless of the havocked base value, so dispatch remains correct. ### Testing New regression tests cover both directions: a harness constructing its input through a function whose postcondition calls the verification target now passes, and a wrong postcondition on the target still fails (the actual check is not weakened). Full `expected/function-contract` (111) and `kani/FunctionContracts` (8) suites pass. End-to-end on verify-rust-std (Kani pin 152c6a8 + CBMC 6.10.0): `ptr::non_null::verify::non_null_check_as_ptr` passes without `--no-assert-contracts`, with no regression on a 9-harness validation batch. Part of the effort to make dropping `--no-assert-contracts` from verify-rust-std's `run-kani.sh` feasible (see also model-checking/verify-rust-std#622, model-checking#623, model-checking#624, and diffblue/cbmc#9149). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe Monteiro <felisous@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>

Contracts of dependencies are asserted by default (model-checking#3802) as an aid for detecting API misuse in user code. Calls made while evaluating *contract clauses*, however, are specification-level plumbing: clause expressions compute a predicate over pre-/post-states, and the functions they call are best executed with their exact semantics. Re-asserting dependency contracts inside every clause evaluation multiplies verification cost - clauses of contract-dense code (e.g. the Rust standard library in model-checking/verify-rust-std) routinely call contracted functions like NonNull::as_ptr, paying the assert-closure overhead per clause instance - without checking any user code. Extend the clause-context dispatch introduced for check modes to assert mode: calls to a contracted dependency that occur during clause evaluation now execute the original body (mode 0). The body remains fully inlined and UB-checked; only the requires/ensures assertions of the *callee's* contract are skipped in this context. The new regression test checks both halves: a clause calling a contracted function with precondition-violating (but well-defined) arguments verifies successfully, while the same misuse in user code is still caught. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Signed-off-by: Felipe Monteiro <felisous@amazon.com>

…-checking#4715) Kani's function-contract instrumentation wraps every requires/ensures clause in a closure capturing the contracted function's arguments by reference. Evaluating a clause loads each captured argument through a reference that closure construction itself created from a live local of the enclosing frame - a load that cannot fail - yet CBMC's --pointer-check instruments each one with all six pointer-validity checks. On contract-heavy code these vacuous checks dominate the reported property count: verifying ffi::c_str::verify::check_to_bytes from verify-rust-std with dependency contracts asserted (the default since model-checking#3802) produces 943 checks, of which 294 are pointer_dereference sextets on contract-closure capture loads. With this change the same harness reports 649 checks. Note that this is a report-noise and formula-size reduction, not a solve-time one: measured end-to-end verification time and peak memory on that harness are unchanged, as the solver discharged these locally-provable checks cheaply. Suppress these checks by attaching CBMC's disable:pointer-check source-location pragma - the same mechanism backing kanitool::disable_checks, already used by the mem-init instrumentation - to exactly those statements whose every dereference is a direct load of a by-reference closure capture in a contract-clause closure. A local qualifies only if: * the current instance is a closure taking its environment by value (contract closures are invoked in place; escaping closures, whose captures could outlive the frame, are called via reference-typed environments and remain fully checked); * the innermost enclosing non-closure item carries a Kani contract (kanitool::checked_with); kanitool::is_contract_generated cannot be used due to model-checking#3921; * the closure environment is never written to; * the local is reference-typed, never address-taken, and its single assignment copies an environment field whose corresponding capture is a ByRef capture of an unprojected place. The ByRef-capture condition matters for soundness: a by-value capture of reference type (e.g. a &mut argument moved into the closure, as in tests/expected/function-contract/mutable-references/return_mut_ref.rs) holds a caller-provided reference whose dereference must remain checked. User-written dereferences inside clause expressions (e.g. #[requires(*ptr == 42)]) always remain checked: they operate on a different MIR local, assigned from the capture load rather than from an environment field. Regression tests cover all three behaviours: capture loads generate no pointer checks; a valid user-written clause dereference keeps its (passing) checks; an invalid user-written clause dereference is still caught. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe Monteiro <felisous@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com> Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> Co-authored-by: Felipe Monteiro <felisous@amazon.com>

…model-checking#4710) Stacked on model-checking#4709 (first commit; review only the last commit here). Contracts of dependencies are asserted by default (model-checking#3802) as an aid for detecting API misuse in *user code*. Calls made while evaluating *contract clauses*, however, are specification-level plumbing: clause expressions compute a predicate over pre-/post-states, and the functions they call are best executed with their exact semantics. Re-asserting dependency contracts inside every clause evaluation multiplies verification cost on contract-dense code (clauses in model-checking/verify-rust-std routinely call contracted functions such as `NonNull::as_ptr`, paying the assert-closure overhead per clause instance) without checking any user code. This PR extends the clause-context dispatch introduced in model-checking#4709 from check modes to assert mode: calls to a contracted dependency occurring during clause evaluation execute the original body (mode 0). The body remains fully inlined and UB-checked; only the requires/ensures assertions of the callee's contract are skipped in this context — a genuine UB-causing misuse inside a clause is still caught by the UB checks themselves. The regression test covers both halves: a clause calling a contracted function with precondition-violating (but well-defined) arguments verifies successfully, while the same misuse in user code still fails on the asserted precondition. Measurements on verify-rust-std (Kani pin 152c6a8 + CBMC 6.10.0, contracts asserted): semantics-driven change with modest performance impact on sampled harnesses after the fixes in verify-rust-std#622/model-checking#623/model-checking#624 landed (`check_to_bytes` and `non_null_check_read` within noise; `num::nonzero::verify::check_mul_i128_edge_pos` improved from 29.4s to 8.1s measured against the pre-fix baseline, attribution shared with verify-rust-std#624). The full `expected/function-contract` suite passes with `--force-rerun` (112/112). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe Monteiro <felisous@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>

…ing#627) `NonNull::slice_from_raw_parts` is a safe function with no validity requirements on `data`: per its documentation, it is safe to construct the pointer, and only its *use* is subject to safety conditions. Its postcondition however evaluated `unsafe { result.as_ref() }.len()`, creating a reference to the pointed-to memory just to read the slice length — undefined behavior when `data` is dangling or misaligned, and a failing check when the contract is evaluated in such a context. This surfaces with dependency contracts asserted (the Kani default since model-checking/kani#3802): `ptr::non_null::verify::non_null_check_as_uninit_slice_mut` constructs, legitimately, a `NonNull` slice pointer whose span may exceed the backing allocation; evaluating `slice_from_raw_parts`' postcondition then fails with "misaligned pointer to reference cast" / "dereference failure: pointer invalid" inside `NonNull::as_ref`. CI currently masks this with `--no-assert-contracts`. This PR reads the length from the wide-pointer metadata via `NonNull::len` instead, which involves no dereference (and no unsafe code) and is the property the clause is about in the first place. Blame: the dereferencing clause dates to the original contracts in 07318df (model-checking#127). Verified with Kani 152c6a8c + CBMC 6.10.0: `non_null_check_as_uninit_slice_mut`, `non_null_check_slice_from_raw_parts`, `non_null_check_as_uninit_slice` and `non_null_check_len` pass both with and without `--no-assert-contracts` (the first previously failed with contracts asserted — the last remaining failure of that kind known on the 125-harness sample after model-checking#622, model-checking#623, model-checking#624, model-checking#625, model-checking#626). 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: Kiro <kiro-agent@users.noreply.github.com>

…g#622) The `x % 2 != 0` precondition on `ptr::mod_inv`, added in 6be9ca4 (model-checking#457), is violated by `mod_inv`'s only caller: `align_offset::<T>(p, 1)` with `size_of::<T>() > 1` takes the GENERAL_CASE path (since `1 % stride != 0`) and computes `s2 = (stride & 0) >> 0 = 0`, calling `mod_inv(0, 1)`. This is reachable e.g. via `<[u16]>::align_to::<u8>()`. The violation is currently invisible in CI because `run-kani.sh` passes `--no-assert-contracts`; with dependency contracts asserted (the Kani default since model-checking/kani#3802), the harnesses `slice::verify::align_to_from_u16::align_to_u8`, `slice::verify::align_to_mut_from_char::align_to_mut_u8`, `slice::verify::align_to_mut_from_u32::align_to_mut_u8`, and `ptr::verify::check_align_offset_u16` all fail on the asserted `x % 2 != 0` clause. The call is mathematically sound — modulo `m == 1` every value is trivially an inverse (the unique residue is 0), and `align_offset` masks the returned value with `a2 - 1 == 0` — so it is the precondition that is too strict, not the caller that is wrong: an inverse of `x` modulo a power of two `m` exists iff `gcd(x, m) == 1`, which for `m > 1` means odd `x` but for `m == 1` holds for all `x`. This PR weakens the precondition to `m == 1 || x % 2 != 0` and fixes the (kani-disabled) postcondition for the same degenerate case (`% m == 1 % m` instead of `% m == 1`, since modulo 1 the result is 0). Verified with Kani 152c6a8c + CBMC 6.10.0: the four harnesses above now pass with contracts asserted, and the eight `ptr::verify::check_align_offset*` proof harnesses pass both with and without `--no-assert-contracts`. Found while investigating what still blocks removing `--no-assert-contracts` from `run-kani.sh`: this is one of two genuine latent contract violations that asserting dependency contracts surfaces (the other: model-checking#623). 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: Kiro <kiro-agent@users.noreply.github.com>

…el-checking#623) The `proof_for_contract` harnesses for `IndexRange::next_unchecked` and `IndexRange::next_back_unchecked`, introduced in a0fca1c (model-checking#451), construct their `IndexRange` via `IndexRange::new_unchecked(start, end)` with entirely unconstrained `start` and `end`. That violates `new_unchecked`'s documented safety precondition (and `#[requires]` contract) `start <= end`: the assumption provided by the contract under verification only takes effect at the call to `next_unchecked` / `next_back_unchecked`, after the UB of the unchecked constructor call has already happened. The violation is currently invisible in CI because `run-kani.sh` passes `--no-assert-contracts`; with dependency contracts asserted (the Kani default since model-checking/kani#3802), `proof_for_index_range_next_back_unchecked` fails on the asserted `start <= end` clause. This PR constrains both harnesses with `kani::assume(start <= end)`. The stronger `start < end` required by the functions under verification continues to be assumed from their own contracts, preserving the intent of the harnesses. Verified with Kani 152c6a8c + CBMC 6.10.0: all three `ops::index_range::verify` harnesses pass both with and without `--no-assert-contracts`. Found while investigating what still blocks removing `--no-assert-contracts` from `run-kani.sh`: this is one of two genuine latent contract violations that asserting dependency contracts surfaces (the other: model-checking#622). 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: Kiro <kiro-agent@users.noreply.github.com>

…-checking#625) The requires/ensures clauses of the pointer arithmetic operations (`<*mut T>::{offset,add,sub}`, `<*const T>::{offset,add,sub}`, `NonNull::{add,sub}`, `NonNull::offset_from_unsigned`) demand `same_allocation` unconditionally (modulo a ZST escape), although the documented semantics explicitly permit zero-sized offsets on any pointer, including dangling ones: only "if the computed offset is non-zero, then self must be derived from a pointer to some allocated object". The stricter-than-documented clauses are violated by legitimate std code: empty slices may be backed by dangling pointers (`slice::from_raw_parts(ptr, 0)` for arbitrary aligned non-null `ptr` — exactly what `slice::iter`'s own `any_slice` helper generates), whereupon `Iter::new` computes `ptr.add(0)` and `len()` computes `end.offset_from_unsigned(begin)` on two equal dangling pointers. With dependency contracts asserted (the Kani default since model-checking/kani#3802), the `slice::iter::verify::verify_tup` harnesses fail on these clauses — and evaluating `same_allocation` on an allocation-less pointer is additionally a Kani unsupported construct ("Kani does not support reasoning about pointer to unallocated memory"). CI currently masks this via `--no-assert-contracts`. This PR adds the documented escape hatches: `count == 0 ||` ahead of the same-allocation disjunct in offset/add/sub requires and ensures — matching the precedent already present in `NonNull::offset` — and an equal-address escape in `NonNull::offset_from_unsigned`, matching the precedent in `<*const T>::offset_from`. Blame: the unconditional clauses date back to the original contract PRs model-checking#113 (014965a) and model-checking#93 (688b15b) and siblings. Verified with Kani 152c6a8c + CBMC 6.10.0: * `slice::iter::verify::verify_tup::{check_next_back_unchecked,check_advance_back_by}` now pass with contracts asserted; * all 265 proof harnesses matching `non_null_check_{add,sub,offset_from_unsigned}` and `ptr::verify::check_{mut,const}_{add,sub,offset}` pass both with and without `--no-assert-contracts`. Together with model-checking#622, model-checking#623, model-checking#624 and model-checking/kani#4709/rust-lang#4710, this resolves all verdict differences found on a 125-harness sample when running without `--no-assert-contracts`, except `non_null_check_from_raw_part_trait` (Kani's "unstable vtable comparison 'Eq'" limitation, reached by `as_ptr`'s postcondition on a `dyn Trait` pointee — tracked separately). 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: Kiro <kiro-agent@users.noreply.github.com>

…odel-checking#624) The requires/ensures clauses of `NonZero::new_unchecked` (and the requires of `from_mut_unchecked`) expressed "n is not zero" and "result equals n" by building a raw byte slice over the value with `slice::from_raw_parts` and iterating it. Under symbolic execution, every asserted occurrence of these clauses pays for pointer indirection, slice-iterator reasoning, and allocation tracking — and since `new_unchecked` sits beneath most `NonZero` operations, harnesses whose call graph contains `NonZero` constructions were dominated by this: with dependency contracts asserted (the Kani default since model-checking/kani#3802), `num::nonzero::verify::check_mul_u32_small` takes 59.6s of CBMC solve time, against 0.3s with `--no-assert-contracts`. This PR expresses the same properties through operations the verifier resolves directly: `NonZero::new(n).is_some()` performs the canonical zero test via the niche layout (a transmute plus discriminant test), and `intrinsics::raw_eq` compares object representations without constructing slices. Neither requires additional trait bounds on `T`. Measured with Kani 152c6a8c + CBMC 6.10.0: * `check_mul_u32_small` with contracts asserted: 59.6s → 0.6s solve time (103x). * All 56 harnesses matching `nonzero_check_new_unchecked_for*` / `nonzero_check_from_mut_unchecked*` / `check_mul*` pass both with and without `--no-assert-contracts`. Part of the effort to make dropping `--no-assert-contracts` from `run-kani.sh` feasible (see also model-checking#622, model-checking#623): the byte-inspection clauses were the single largest per-call-site cost multiplier identified when asserting dependency contracts across a 125-harness sample. 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: Kiro <kiro-agent@users.noreply.github.com>

Carolyn Zech added 8 commits December 28, 2024 14:34

replace ClosureType with ContractMode (to be consistent with kani-com…

a3f28bb

…piler)

move split_for_remembers to shared.rs; remove unused variants

b18d35a

add ContractMode for assertions to library/kani_macros

11f3e04

add option to use Assert ContractMode

1f135c9

tests

d4a8fc0

documentation

979ecb0

tweak comment

ba4a108

doc nits

e8c9311

github-actions Bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Dec 30, 2024

Carolyn Zech added 5 commits December 31, 2024 10:21

Merge branch 'main' of github.com:model-checking/kani into contracts-…

f4f5816

…as-assertions

wrap body in a closure

3ebdf3a

simplify tests to reduce runner load

397e727

add loops test

261740d

update docs to reflect body wrapper closure

98b0b2f

carolynzech commented Jan 2, 2025

View reviewed changes

Comment thread library/kani_macros/src/sysroot/contracts/mod.rs

carolynzech marked this pull request as ready for review January 2, 2025 17:58

carolynzech requested a review from a team as a code owner January 2, 2025 17:58

zhassan-aws reviewed Jan 2, 2025

View reviewed changes

celinval reviewed Jan 2, 2025

View reviewed changes

Comment thread kani_metadata/src/unstable.rs Outdated

carolynzech commented Jan 2, 2025

View reviewed changes

Comment thread tests/expected/function-contract/as-assertions/assert-postconditions.rs Outdated

carolynzech commented Jan 2, 2025

View reviewed changes

Comment thread tests/expected/function-contract/as-assertions/assert-preconditions.rs Outdated

Carolyn Zech and others added 4 commits January 2, 2025 17:43

Apply suggestions from code review

4d8c34b

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

clarify tests

d3fdcad

make asserting contracts the default

8cabda4

add simple precedence test

87288f1

carolynzech commented Jan 7, 2025

View reviewed changes

Comment thread kani-compiler/src/args.rs Outdated

carolynzech commented Jan 7, 2025

View reviewed changes

Comment thread kani-driver/src/args/mod.rs Outdated

clap nits

8baf862

carolynzech requested review from celinval and zhassan-aws January 7, 2025 17:01

carolynzech enabled auto-merge January 8, 2025 21:39

Merge branch 'main' into contracts-as-assertions

0a5e808

carolynzech changed the title ~~Add an option to generate contracts as assertions~~ Generate contracts of dependencies as assertions Jan 9, 2025

carolynzech added this pull request to the merge queue Jan 9, 2025

Merged via the queue into model-checking:main with commit addc590 Jan 9, 2025

carolynzech deleted the contracts-as-assertions branch January 9, 2025 03:42

qinheping mentioned this pull request Jan 10, 2025

Bump Kani version to 0.58.0 #3822

Merged

carolynzech mentioned this pull request Apr 15, 2025

Verification results of #[proof] and #[proof_for_contract] are different #4021

Open

This was referenced Aug 4, 2026

Elide vacuous pointer checks on contract-closure capture loads #4715

Merged

Do not dereference in slice_from_raw_parts postcondition model-checking/verify-rust-std#627

Merged

Navigation Menu

Uh oh!

Generate contracts of dependencies as assertions - #3802

Generate contracts of dependencies as assertions#3802
carolynzech merged 19 commits into
model-checking:mainfrom
carolynzech:contracts-as-assertions

carolynzech commented Dec 30, 2024 •

edited

Loading

Uh oh!

Uh oh!

zhassan-aws left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

carolynzech commented Dec 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

zhassan-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

carolynzech commented Dec 30, 2024 •

edited

Loading