Autoharness --constructor-args: assumed mined invariants may exclude valid values (heuristic under-approximation)

[feliperodri]

Summary

Under -Z autoharness --constructor-args, Kani mines "type invariants" from a type's own &self methods (assertions over self's fields) and assumes them for generated nondeterministic values (kani::assume). A conjunct is admitted when it post-dominates every normal return, its slice is pure/call-free, and it is asserted in at least two distinct methods.

The "asserted in ≥2 distinct methods" frequency filter is a heuristic, not a proof of type-invariance. If two methods share a precondition that is not a universal invariant of the type, the shared condition is mined and assumed for all generated values, excluding otherwise-valid values.

Example: a type validly constructible with divisor == 0, but with

fn a(&self) { assert!(self.divisor != 0); /* ... */ }
fn b(&self) { assert!(self.divisor != 0); /* ... */ }

divisor != 0 is asserted in two methods, so it is mined and assumed. A harness for a third method fn c(&self) that must correctly handle divisor == 0 would then never explore divisor == 0 — a potential false negative (missed bug).

Status / mitigation

This is the same opt-in, (ctor)-marked, under-approximating contract as --constructor-args constructor generation (#4718) and the vacuity caveat (#4757): results only cover the values the chosen mechanism admits. The post-dominance, purity, and 2-method filters are mitigations, not guarantees, and the assume direction is arguably weaker-justified than constructor-grounded generation.

Suggested improvements

• Strengthen admission (e.g. require the conjunct to hold at every public constructor's return, or cross-check against constructor-reachable values).
• Or restrict the assume direction to conjuncts that are also implied by a viable constructor.

Documented as a known limitation; tracked here as a follow-up from the review of #4722.