Struct SyncView 

pub struct SyncView(/* private fields */);

A witness to the current view, containing all the events observed by this thread.

In Cosmo, SyncView corresponds to the notation ↑V In Relaxed RustBelt, SyncView corresponds to the notation V.cur

Implementations

impl SyncView

pub fn new() -> Ghost<Self>

ghost

pub fn weaken(&mut self, to: Snapshot<SyncView>)

ghost

requires

*to <= *self

ensures

^self == *to

Trait Implementations

impl Clone for SyncView

fn clone(&self) -> Self

ensures

result == *self

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for SyncView

impl From<ReleaseSyncView> for SyncView

fn from(value: ReleaseSyncView) -> Self

ghost

ensures

result == value@

impl From<SyncView> for AcquireSyncView

fn from(value: SyncView) -> Self

ghost

ensures

result@ == value

impl OrdLogic for SyncView

fn cmp_log(self, _: Self) -> Ordering

logic(opaque)

fn cmp_le_log(x: Self, y: Self)

logic(law)

ensures

x.le_log(y) == (x.cmp_log(y) != Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(law)

ensures

x.lt_log(y) == (x.cmp_log(y) == Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(law)

ensures

x.ge_log(y) == (x.cmp_log(y) != Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(law)

ensures

x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater)

fn refl(x: Self)

logic(law)

ensures

x.cmp_log(x) == Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(law)

requires

x.cmp_log(y) == Ordering::Less

ensures

y.cmp_log(x) == Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(law)

requires

x.cmp_log(y) == Ordering::Greater

ensures

y.cmp_log(x) == Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(law)

ensures

(x == y) == (x.cmp_log(y) == Ordering::Equal)

fn le_log(self, o: Self) -> bool

The logical <= operation.

fn lt_log(self, o: Self) -> bool

The logical < operation.

fn ge_log(self, o: Self) -> bool

The logical >= operation.

fn gt_log(self, o: Self) -> bool

The logical > operation.