Struct View 

pub struct View<R: ViewRel>(/* private fields */);

Implementations

impl<R: ViewRel> View<R>

pub fn auth(self) -> Option<R::Auth>

Returns the authoritative part of a given View

pub fn frag(self) -> R::Frag

ensures

R::rel(self.auth(), result)

pub fn ext_eq(self, other: Self) -> bool

(open)

let _ = Subset::<InnerView<R>>::view_inj;
self.auth() == other.auth() && self.frag() == other.frag()

ensures

result == (self == other)

pub fn new(auth: Option<R::Auth>, frag: R::Frag) -> Self

Create a new View with given authority and fragment.

requires

R::rel(auth, frag)

ensures

result.auth() == auth

ensures

result.frag() == frag

pub fn new_auth(auth: R::Auth) -> Self

Create a new View containing an authoritative version of x.

(open, inline)

Self::new(Some(auth), R::Frag::unit())

pub fn new_frag(frag: R::Frag) -> Self

Create a new View containing a fragment version of x.

(open, inline)

Self::new(None, frag)

requires

R::rel(None, frag)

Trait Implementations

impl<R: ViewRel> RA for View<R>

fn op(self, other: Self) -> Option<Self>

(open)

pearlite! {
    match self.frag().op(other.frag()) {
        Some(f) => match (self.auth(), other.auth()) {
            (None, a) => if R::rel(a, f) { Some(Self::new(a, f)) } else { None },
            (a, None) => if R::rel(a, f) { Some(Self::new(a, f)) } else { None },
            _ => None
        }
        None => None
    }
}

fn factor(self, factor: Self) -> Option<Self>

(open)

let _ = Subset::<InnerView<R>>::view_inj;
match self.frag().factor(factor.frag()) {
    Some(f) => match (self.auth(), factor.auth()) {
        (Some(a), None) => Some(Self::new(Some(a), f)),
        (a1, a2) => {
            if a1 == a2 {
                Some(Self::new_frag(f))
            } else {
                None
            }
        }
    },
    None => None,
}

ensures

match result {
        Some(c) => factor.op(c) == Some(self),
        None => forall<c: Self> factor.op(c) != Some(self),
    }

fn commutative(a: Self, b: Self)

(open(pub(self)), law)

ensures

a.op(b) == b.op(a)

fn associative(a: Self, b: Self, c: Self)

(open(pub(self)), law)

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

(open)

Some(self.core_total())

ensures

match result {
        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
        None => true
    }

fn core_is_maximal_idemp(self, i: Self)

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
        Some(c) => i.incl(c),
        None => false,
    }

fn incl(self, other: Self) -> bool

Inclusion of RA.

fn incl_op(self, other: Self, comb: Self)

(law, sealed)

fn incl_eq(self, other: Self) -> bool

(open, sealed)

fn incl_eq_op(a: Self, b: Self, x: Self) -> bool

(open, sealed)

fn update(self, x: Self) -> bool

Ensures that we can go from self to x without making composition with the frame invalid.

fn update_nondet(self, s: Set<Self>) -> bool

This is used in Resource::update_nondet.

fn incl_transitive(a: Self, b: Self, c: Self)

RA::incl is transitive.

impl<R: ViewRel> UnitRA for View<R>

fn unit() -> Self

ensures

forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x)

fn core_total(self) -> Self

(open)

let _ = R::Frag::core_is_total;
let _ = Self::ext_eq;
Self::new_frag(self.frag().core_total())

ensures

result.op(result) == Some(result)

ensures

result.op(self) == Some(self)

fn core_is_total(self)

ensures

self.core() == Some(self.core_total())

fn incl_refl()

(law, sealed)

fn unit_core()

(law, sealed)

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

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

(open)

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

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

(open)

let from_auth = from.auth().unwrap_logic();
let (auth, frag) = self.0.update(from_auth, from.frag());
self.0.frame_preserving(from_auth, from.frag(), from_auth.factor(from.frag()));
Auth::new(Some(auth), frag)

requires

self.premise(from)

ensures

let (auth, frag) = self.0.update(from.auth().unwrap_logic(), from.frag());
AuthViewRel::rel(Some(auth), frag)

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

impl<R: ViewRel, Choice> Update<View<R>> for ViewUpdate<R, Choice>

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

(open)

pearlite! {
    from.auth() != None &&
    (forall<ch: Choice> R::rel(Some(self.0[ch].0), self.0[ch].1)) &&
    forall<frame: R::Frag>
        match from.frag().op(frame) {
            Some(ff) => R::rel(from.auth(), ff),
            None => false
        } ==>
        exists<ch: Choice>
            match self.0[ch].1.op(frame) {
                Some(ff) => R::rel(Some(self.0[ch].0), ff),
                None => false
            }
}

fn update(self, from: View<R>, ch: Choice) -> View<R>

(open)

View::new(Some(self.0[ch].0), self.0[ch].1)

requires

self.premise(from)

fn frame_preserving(self, from: View<R>, frame: View<R>) -> Choice

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = Choice

impl<R: ViewRel> Update<View<R>> for ViewUpdateInsert<R>

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

(open)

pearlite! {
    from.auth() != None &&
    forall<f: R::Frag> R::rel(from.auth(), f) ==>
        match self.1.op(f) {
            Some(ff) => R::rel(Some(*self.0), ff),
            None => false
        }
}

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

(open)

View::new(Some(*self.0), *self.1)

requires

self.premise(from)

ensures

R::rel(Some(*self.0), *self.1)

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

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = ()

impl<R: ViewRel> Update<View<R>> for ViewUpdateRemove<R>

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

(open)

pearlite! {
    from.auth() != None &&
    forall<f: R::Frag>
        match from.frag().op(f) {
            Some(ff) => R::rel(from.auth(), ff),
            None => false
        } ==>
        R::rel(Some(*self.0), f)
}

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

(open)

View::new_auth(*self.0)

requires

self.premise(from)

ensures

R::rel(Some(*self.0), R::Frag::unit())

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

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = ()