That's the goal at least! We explicitly do not have a notion of "undef" or "poison" values in our IR, and to the largest degree possible we want determinism (modulo e.g. some NaN-related stuff right now). Our current discussion with some researchers wanting to formally verify our lowerings will likely push us toward the start of some formal spec for the IR as well, though exactly how that will work or be maintained is not yet decided.

I'm not super-familiar with the pointer provenance work in Rust but I'll read more about this; thanks for the mention!