Skip to main content

axiom_permission_u64_ext_eq

vstd_extra::auxiliary

Function axiom_permission_u64_ext_eq 

Source 
pub proof fn axiom_permission_u64_ext_eq(p1: PermissionU64, p2: PermissionU64)
Expand description
requires
p1.id() == p2.id(),
p1.value() == p2.value(),
ensures
p1 == p2,

Extensional equality for PermissionU64: two permissions with the same id() and value() are equal. This is sound because PermissionU64’s view is determined entirely by (patomic, value), and the tracked struct is a newtype wrapper around its view.