Struct AuthUpdate 

pub struct AuthUpdate<U>(pub U);

Tuple Fields

0: U

Trait Implementations

impl<R: UnitRA, U: LocalUpdate<R>> Update<View<AuthViewRel<R>>> for AuthUpdate<U>

fn premise(self, from: Auth<R>) -> bool

(open, inline)

match from.auth() {
    Some(auth) => self.0.premise(auth, from.frag()),
    None => false,
}

fn update(self, from: Auth<R>, _: ()) -> Auth<R>

requires

self.premise(from)

ensures

result.auth() == Some(self.0.update(from.auth().unwrap_logic(), from.frag()).0)

ensures

result.frag() == self.0.update(from.auth().unwrap_logic(), from.frag()).1

fn frame_preserving(self, from: Auth<R>, frame: Auth<R>)

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = ()