Skip to main content

axiom_unique_entry_new

ostd::specs::mm::embedding

Function axiom_unique_entry_new 

Source 
pub proof fn axiom_unique_entry_new(paddr: Paddr) -> tracked res : UniqueEntry
Expand description
ensures
res.paddr == paddr,

Tracked constructor for UniqueEntry.