Struct FMapKeyLocalUpdate 

pub struct FMapKeyLocalUpdate<K, U>(pub Snapshot<K>, pub U);

Modifies a key-value mapping in an authority/fragment pair of FMaps.

It requires that the key is in the fragment.

Tuple Fields

0: Snapshot<K>

1: U

Trait Implementations

impl<K, V: RA, U: LocalUpdate<V>> LocalUpdate<FMap<K, V>> for FMapKeyLocalUpdate<K, U>

fn premise(self, from_auth: FMap<K, V>, from_frag: FMap<K, V>) -> bool

logic(open, inline)

match (from_auth.get(*self.0), from_frag.get(*self.0)) {
    (Some(auth_v), Some(frag_v)) => self.1.premise(auth_v, frag_v),
    (_, None) => false,
    _ => true,
}

fn update( self, from_auth: FMap<K, V>, from_frag: FMap<K, V>, ) -> (FMap<K, V>, FMap<K, V>)

logic(open, inline)

let (auth, frag) = self.1.update(from_auth[*self.0], from_frag[*self.0]);
(from_auth.insert(*self.0, auth), from_frag.insert(*self.0, frag))

fn frame_preserving( self, from_auth: FMap<K, V>, from_frag: FMap<K, V>, frame: Option<FMap<K, V>>, )

logic

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = self.update(from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))