Autoharness: assume safety invariants of generated values

[tautschnig]

Description

Automatic harnesses (kani autoharness) now assume that the nondeterministic values they generate respect the type's safety invariant (kani::Invariant), including for nested types.

Previously, automatic harnesses generated values purely via Arbitrary, so a safety invariant was respected only if it happened to be baked into the type's Arbitrary implementation (e.g. via #[safety_constraint(...)] or a manual impl Arbitrary that assumes is_safe()). Types with an Invariant implementation but an unconstrained (or compiler-synthesized) Arbitrary implementation received invariant-violating inputs, producing spurious counterexamples. Per the Unsafe Code Guidelines' definition of a safety invariant, safe code may assume its inputs uphold their types' safety invariants, so these counterexamples are noise.

This PR is split into two commits:

1. Move the Invariant trait into kani_core (new generate_invariant! macro) so it is also available in no_core mode, and add an assume_safe<T: Invariant> model function (KaniModel::AssumeSafe) that assumes value.is_safe(). The trait remains available as kani::Invariant; no user-facing change.
2. In the autoharness transformation passes, wrap every generated nondeterministic ADT value whose type implements Invariant in a call to the AssumeSafe model. Since this happens in call_kani_any_for_ty, which is shared by AutomaticHarnessPass (harness arguments, including behind references) and AutomaticArbitraryPass (fields of compiler-synthesized Arbitrary implementations), nested invariants are respected as well. A new implements_invariant check mirrors the existing implements_arbitrary resolution approach.

Note that automatic harnesses still do not assert type invariants (e.g. on return values); that remains the job of function contracts such as #[kani::ensures(|result| result.is_safe())]. The autoharness reference documentation now spells out both halves of this behavior.

Testing

New script-based test cargo_autoharness_assume_invariant with 8 automatic harnesses: manual Invariant with compiler-synthesized Arbitrary, manual Invariant with unconstrained derived Arbitrary, #[safety_constraint], two nested-invariant variants, an argument behind a reference, and two negative controls (verifying that the harness neither assumes more than the invariant nor invents invariants for types without an Invariant implementation). Before this change, three of these harnesses failed spuriously.

Manually verified no regressions in: all existing autoharness and autoderive script-based tests, the Invariant and derive-invariant suites, verify_std_cmd/std_codegen (exercising the no_core path), kani-compiler unit tests, and the kani library doctests.

Towards #3832 (ticks the "Types with invariants that the harnesses need to respect" box).

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

[Copilot]

Pull request overview

This PR updates Kani’s automatic harness generation (kani autoharness) to assume type safety invariants (kani::Invariant::is_safe()) for generated nondeterministic values, including for nested ADT fields, reducing spurious counterexamples caused by invariant-violating inputs.

Changes:

• Move/generate the Invariant trait from kani into kani_core (via generate_invariant!) and add an assume_safe<T: Invariant>(T) -> T model function (KaniModel::AssumeSafe).
• Update the autoharness and compiler-synthesized Arbitrary paths to wrap generated ADT values with AssumeSafe when the type implements Invariant.
• Add a new script-based regression test and update autoharness reference docs to describe invariant assumptions.

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tests/script-based-pre/cargo_autoharness_assume_invariant/src/lib.rs	New regression crate covering invariant assumptions (including nested and negative controls).
tests/script-based-pre/cargo_autoharness_assume_invariant/config.yml	Script-based test configuration for the new regression test.
tests/script-based-pre/cargo_autoharness_assume_invariant/Cargo.toml	New test crate manifest for the regression.
tests/script-based-pre/cargo_autoharness_assume_invariant/assume-invariant.sh	Runs cargo kani autoharness -Z autoharness for the new test.
tests/script-based-pre/cargo_autoharness_assume_invariant/assume-invariant.expected	Expected summary output: 6 successes / 2 failures (exit code 1).
library/kani/src/lib.rs	Removes old invariant module exports (potential compatibility impact).
library/kani/src/invariant.rs	Removes the prior Invariant trait/module implementation (now generated from kani_core).
library/kani_core/src/lib.rs	Adds mod invariant; and invokes generate_invariant!() in kani_lib!.
library/kani_core/src/invariant.rs	Introduces generate_invariant! macro, the Invariant trait, and assume_safe model.
kani-compiler/src/kani_middle/transform/automatic.rs	Wraps generated ADT nondet values with AssumeSafe when Invariant is implemented.
kani-compiler/src/kani_middle/mod.rs	Adds implements_invariant resolution helper mirroring implements_arbitrary.
kani-compiler/src/kani_middle/kani_functions.rs	Adds KaniModel::AssumeSafe marker mapping.
docs/src/reference/experimental/autoharness.md	Documents invariant assumptions (needs wording alignment with implementation scope).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.