pub broadcast proof fn lemma_paddr_to_meta_biinjective(paddr: Paddr)Expand description
requires
valid_frame_paddr(paddr),#[trigger] meta_to_frame(frame_to_meta(paddr)) == paddr,