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

Perform an update on an authority/fragment pair.

This is similar to Update, but is instead used by Authority::update to simultaneously change the value of an authority/fragment pair.

Note that contrary to Update, this has to be deterministic.

Required Methods

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

The premise of the update.

This must be true for the authority and the fragment before applying the update.

logic

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

The update performed.

This describe how to change the authority/fragment pair.

logic

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

Frame preservation.

This is a lemma that must be proven by implementors to ensure that the update is consistent.

It states that the ‘missing piece’ of the authority from the fragment is still the same after the update.

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

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

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

logic(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)>, )

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

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

Apply no update.

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

logic(open, inline)

true

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

logic(open, inline)

from_auth, from_frag

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

logic

requires

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

ensures

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

Implementors

impl LocalUpdate<Int> for Int

Add an integer to an authority/fragment pair of integers.

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

Apply a ‘raw’ local update.

This will update the value of the authority/fragment to the provided pair.

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

impl<R: UnitRA> LocalUpdate<R> for OpLocalUpdate<R>