Struct ProdLocalUpdate 

pub struct ProdLocalUpdate<U1, U2>(pub U1, pub U2);

Tuple Fields

0: U1

1: U2

Trait Implementations

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

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

(open)

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)

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