A few more primitive to SyncView.

creusot-std/src/std/sync/view.rs

@@ -1,5 +1,5 @@
 use crate::prelude::*;
-use core::marker::PhantomData;
+use core::{marker::PhantomData, panic};
 
 #[cfg(creusot)]
 use core::cmp::Ordering;
@@ -40,6 +40,15 @@ impl SyncView {
     pub fn new() -> Ghost<Self> {
         panic!("Should not be called outside ghost code")
     }
+
+    #[check(ghost)]
+    #[trusted]
+    #[requires(*to <= *self)]
+    #[ensures(^self == *to)]
+    #[allow(unused_variables)]
+    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
+        panic!("Should not be called outside ghost code")
+    }
 }
 
 impl OrdLogic for SyncView {
@@ -106,6 +115,7 @@ impl OrdLogic for SyncView {
 pub struct ReleaseSyncView(());
 
 impl Clone for ReleaseSyncView {
+    #[check(ghost)]
     #[ensures(result == *self)]
     fn clone(&self) -> Self {
         *self
@@ -118,6 +128,15 @@ impl ReleaseSyncView {
     pub fn new() -> Ghost<Self> {
         panic!("Should not be called outside ghost code")
     }
+
+    #[check(ghost)]
+    #[trusted]
+    #[requires(*to <= (*self)@)]
+    #[ensures((^self)@ == *to)]
+    #[allow(unused_variables)]
+    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
+        panic!("Should not be called outside ghost code")
+    }
 }
 
 impl View for ReleaseSyncView {
@@ -149,6 +168,15 @@ impl AcquireSyncView {
     pub fn new() -> Ghost<Self> {
         panic!("Should not be called outside ghost code")
     }
+
+    #[check(ghost)]
+    #[trusted]
+    #[requires(*to <= (*self)@)]
+    #[ensures((^self)@ == *to)]
+    #[allow(unused_variables)]
+    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
+        panic!("Should not be called outside ghost code")
+    }
 }
 
 impl View for AcquireSyncView {
@@ -172,7 +200,7 @@ impl<T> Objective for AtView<T> {}
 
 impl<T> AtView<T> {
     #[logic(opaque)]
-    pub fn view_logic(&self) -> SyncView {
+    pub fn view(&self) -> SyncView {
         dead
     }
 
@@ -183,15 +211,15 @@ impl<T> AtView<T> {
 
     #[check(ghost)]
     #[trusted]
-    #[ensures(result.0 == result.1.view_logic() && result.1.val() == *val)]
+    #[ensures(result.0 == result.1.view() && result.1.val() == *val)]
     #[allow(unused_variables)]
     pub fn new(val: Ghost<T>) -> Ghost<(SyncView, Self)> {
         Ghost::conjure()
     }
 
     #[check(ghost)]
     #[trusted]
-    #[requires(self.view_logic() <= sync_view)]
+    #[requires(self.view() <= sync_view)]
     #[ensures(result == self.val())]
     #[allow(unused_variables)]
     pub fn sync(self, sync_view: SyncView) -> T {
@@ -200,8 +228,11 @@ impl<T> AtView<T> {
 
     #[check(ghost)]
     #[trusted]
-    #[ensures(result == self.view_logic())]
-    pub fn view(&self) -> SyncView {
+    #[requires(self.view() <= *to)]
+    #[ensures((^self).view() == *to)]
+    #[ensures((*self).val() == (^self).val())]
+    #[allow(unused_variables)]
+    pub fn weaken(&mut self, to: Snapshot<SyncView>) {
         panic!("Should not be called outside ghost code")
     }
 }

examples/message_passing/relacq.rs

@@ -55,7 +55,7 @@ impl Protocol for MessagePassingAtomicInv {
                     None => true
                 },
                 State::Synchronisation(data_own, tok_write) => excl_write == tok_write.id() && forall<t> match self.atomic_own.val().get(t) {
-                    Some((b, view)) => !b || (b && perm == *data_own.val().ward() && data_own.val().val()@ == 1 && data_own.view_logic() <= view),
+                    Some((b, view)) => !b || (b && perm == *data_own.val().ward() && data_own.val().val()@ == 1 && data_own.view() <= view),
                     None => true
                 },
                 State::Readable(tok_write, tok_read) => excl_write == tok_write.id() && excl_read == tok_read.id(),

examples/message_passing/relacq_options.rs

@@ -48,7 +48,7 @@ impl Protocol for MessagePassingAtomicInv {
                     b &&
                     self.tok_write.val() == Some(Excl(())) &&
                         match self.at_view {
-                            Some(at_view) => *self.data == *at_view.val().ward() && at_view.val().val()@ == 1 && at_view.view_logic() <= view,
+                            Some(at_view) => *self.data == *at_view.val().ward() && at_view.val().val()@ == 1 && at_view.view() <= view,
                             None => self.tok_read.val() == Some(Excl(()))
                         },
                 None => true

examples/message_passing/rlx.rs

@@ -56,7 +56,7 @@ impl Protocol for MessagePassingAtomicInv {
                     None => true
                 },
                 State::Synchronisation(data_own, tok_write) => excl_write == tok_write.id() && forall<t> match self.atomic_own.val().get(t) {
-                    Some((b, view)) => !b || (b && perm == *data_own.val().ward() && data_own.val().val()@ == 1 && data_own.view_logic() <= view),
+                    Some((b, view)) => !b || (b && perm == *data_own.val().ward() && data_own.val().val()@ == 1 && data_own.view() <= view),
                     None => true
                 },
                 State::Readable(tok_write, tok_read) => excl_write == tok_write.id() && excl_read == tok_read.id(),