[wodex1nhaoIeng]

--check-invariants checked the wrong field when an invariant was mined through a getter called on a field of self. In #5011, Outer::first asserts self.inner.valid(), and Inner::valid checks self.count > 0. The miner accepted &self.inner as if it were &self, then read the callee's self.count (field 0 of Inner) as field 0 of Outer, which is decoy. The mined invariant became decoy > 0, so make_valid failed and make_invalid passed: the opposite of the correct verdicts.

The getter's receiver can now be self or any field path under it. The miner records the field path from the caller's self to the receiver and prepends it to the expression mined from the callee, so Inner::valid turns into self.inner.count > 0 on Outer. Nested getters compose, since each level rebases onto its own caller. Receivers this AST can't express (a deref below a field, or a downcast under the prefix) make the miner skip the conjunct instead of guessing.

One shape that isn't explicitly guarded against: a receiver field that is itself a reference or Box, where the prefix would end at a pointer-typed field. On the current toolchain it can't reach the miner. rustc passes self.r through a reborrowed temp, which isn't rooted at self, and a Box deref lowers to BoxDerefTransmute, which the extractor rejects. I left it at that rather than adding a guard for MIR that isn't produced today.

Resolves #5011

The regression test script-based-pre/autoharness_nested_getter is the reproducer from the issue plus a two-level receiver (Deep.outer.inner). It fails on main and passes with this change. All 43 autoharness tests in script-based-pre pass, and rustfmt --check is clean on the changed file.

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