Verifier unable to handle persistent memory difference because it lacks aliasing information. As a result, it assumes the user will provide assertions that help the verifier drive it to equivalence. Builds case for introducing different types of assumptions, allowing the user to introduce assumptions that two pointers don't alias or two memory regions do not overlap. This allows persistent memory differences to safely exist in the eq domain because we know those instances are isolated and the assertions are expected to be provable somehow.
From @danmatichuk
Verifier unable to handle persistent memory difference because it lacks aliasing information. As a result, it assumes the user will provide assertions that help the verifier drive it to equivalence. Builds case for introducing different types of assumptions, allowing the user to introduce assumptions that two pointers don't alias or two memory regions do not overlap. This allows persistent memory differences to safely exist in the eq domain because we know those instances are isolated and the assertions are expected to be provable somehow.