Autoharness --constructor-args: an unsatisfiable constructor yields a vacuous (always-Success) harness

[feliperodri]

Summary

Under -Z autoharness --constructor-args, when Kani generates values of a private-field type through one of the type's constructors, it can produce a vacuous harness (one that assumes false on all paths and therefore reports every property as Success without actually checking anything) if the chosen constructor has no valid inputs.

Two variants:

• Assert-guarded (mined) representation constructors (introduced in Autoharness: mine constructor assertions into value filters #4718): the constructor's body is inlined and every validity statement (kani::assert/assert_unchecked calls, panics, overflow Assert terminators) is converted into an assumption. If the constructor is unsatisfiable for the generated type — e.g. contradictory debug_assert!s, or no argument value passes the asserts — the synthesized kani::any() body assumes false on all paths, making the harness vacuous.
• Checked public constructors (Option<Self>/Result<Self, E>, from Autoharness: constructor-based value generation (--constructor-args) #4717): a constructor that always returns None/Err for the generated argument space is assumed to succeed, producing the same vacuity.

This is a soundness hazard: a vacuous harness reports Success (a false negative) rather than a false alarm.

Suggested fix

Emit a reachability guard for the constructor's success path — e.g. a kani::cover! that the constructor produces a value — so that a fully-vacuous mined/checked constructor is surfaced (as an unreachable-cover failure) instead of silently passing. Harnesses are already marked (ctor) as under-approximations, but the marker does not distinguish "narrowed" from "vacuous".

Context

Follow-up from the review of #4718. Both the mined-constructor path (#4718) and the checked-constructor path (#4717) are affected.