Trait LocalUpdate 

pub trait LocalUpdate<R: RA>: Sized {
    // Required methods
    fn premise(self, from_auth: R, from_frag: R) -> bool;
    fn update(self, from_auth: R, from_frag: R) -> (R, R);
    fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>);
}

Required Methods

fn premise(self, from_auth: R, from_frag: R) -> bool

fn update(self, from_auth: R, from_frag: R) -> (R, R)

fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>)

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))

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl<R1: RA, R2: RA, U1: LocalUpdate<R1>, U2: LocalUpdate<R2>> LocalUpdate<(R1, R2)> for (U1, U2)

fn premise(self, from_auth: (R1, R2), from_frag: (R1, R2)) -> bool

(open, inline)

self.0.premise(from_auth.0, from_frag.0) && self.1.premise(from_auth.1, from_frag.1)

fn update( self, from_auth: (R1, R2), from_frag: (R1, R2), ) -> ((R1, R2), (R1, R2))

(open, inline)

let (to_auth0, to_frag0) = self.0.update(from_auth.0, from_frag.0);
let (to_auth1, to_frag1) = self.1.update(from_auth.1, from_frag.1);
((to_auth0, to_auth1), (to_frag0, to_frag1))

fn frame_preserving( self, from_auth: (R1, R2), from_frag: (R1, R2), frame: Option<(R1, R2)>, )

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))

impl<R: RA> LocalUpdate<R> for ()

fn premise(self, _: R, _: R) -> bool

(open, inline)

true

fn update(self, from_auth: R, from_frag: R) -> (R, R)

(open, inline)

(from_auth, from_frag)

fn frame_preserving(self, auth: R, frag: R, frame: Option<R>)

requires

Some(frag).op(frame) == Some(Some(auth))

ensures

Some(frag).op(frame) == Some(Some(auth))

Implementors

impl LocalUpdate<Int> for Int

impl<K, V: RA> LocalUpdate<FMap<K, V>> for FMapInsertLocalUpdate<K, V>

impl<R1: RA, R2: RA, U: LocalUpdate<R1>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateL<U>

impl<R1: RA, R2: RA, U: LocalUpdate<R2>> LocalUpdate<Sum<R1, R2>> for SumLocalUpdateR<U>

impl<R: RA> LocalUpdate<R> for Snapshot<(R, R)>

impl<R: RA, U: LocalUpdate<R>> LocalUpdate<Option<R>> for OptionLocalUpdate<U>