Skip to main content

frame_preserving_update

vstd::resource::relations

Function frame_preserving_update 

Source 
pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool
Expand description
{ forall |c| P::op(a, c).valid() ==> P::op(b, c).valid() }

A frame preserving update is an update of a value from a --> b such that every value c that could compose with a (also called the frame) can still compose with b.