Skip to main content

perm_u64_with

ostd::specs::mm::frame::meta_owners

Function perm_u64_with 

Source 
pub uninterp fn perm_u64_with(p: PermissionU64, v: u64) -> PermissionU64
Expand description

Value-updaters for the opaque tracked permission types inside MetadataInnerPerms. Each uninterp operation produces a new permission with the same id as the input but a specified value; the paired axioms document the expected behavior. The conversions are implemented in exec by external_body primitives, so the laws are axiomatic.