Function vstd::pcm::frame_preserving_update

pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool