Function lemma_registration_distinguishes_reused_address 

pub proof fn lemma_registration_distinguishes_reused_address<T>(
    ptr: *mut T,
) -> tracked res : (RcuBlockInfo<T>, RcuBlockInfo<T>, RcuBlockInfo<T>)

requires

ptr.addr() != 0,

ensures

res.0.domain() == res.1.domain(),

res.0.domain() == res.2.domain(),

res.0.obj() == res.1.obj(),

res.0.obj() < res.2.obj(),

res.0.addr() == res.1.addr() == res.2.addr() == ptr.addr(),

Proves that address reuse creates a new ID while duplication preserves it.

Preconditions

The pointer has a nonzero address.

Postconditions

Two copies of the first registration agree, while a second registration at that same address has a different allocation ID in the same domain.