resource: make Loc a newtype to avoid int confusion

Author: bsdinis

examples/pcm/agreement.rs

@@ -132,7 +132,8 @@ impl<T> AgreementResource<T> {
         ensures
             self.inv(),
             result.inv(),
-            self.id() == result.id() == old(self).id(),
+            self.id() == old(self).id(),
+            result.id() == old(self).id(),
             self@ == result@,
             self@ == old(self)@,
     {

examples/pcm/count_to_two.rs

@@ -10,6 +10,7 @@ use std::sync::Arc;
 use vstd::atomic::*;
 use vstd::atomic_ghost::*;
 use vstd::invariant::*;
+use vstd::resource::Loc;
 
 verus! {
 
@@ -40,8 +41,8 @@ pub struct CounterTrackedState {
 // `oneshot1_id` -- the ID of thread 1's one-shot
 pub struct CounterInvariantConstants {
     pub x_id: int,
-    pub oneshot0_id: int,
-    pub oneshot1_id: int,
+    pub oneshot0_id: Loc,
+    pub oneshot1_id: Loc,
 }
 
 // This is the invariant predicate that will be maintained for the
@@ -99,7 +100,7 @@ impl CounterSharedState {
 
     // This function gets, from the shared state's constants, the ID
     // of the one-shot associated with the given thread.
-    pub open spec fn get_oneshot_id(self, which_thread: int) -> int
+    pub open spec fn get_oneshot_id(self, which_thread: int) -> Loc
         recommends
             which_thread == 0 || which_thread == 1,
     {

examples/pcm/log.rs

@@ -205,7 +205,8 @@ impl<T> LogResource<T> {
                 let (half1, half2) = halves;
                 &&& half1@ is HalfAuthority
                 &&& half2@ is HalfAuthority
-                &&& half1.id() == half2.id() == self.id()
+                &&& half1.id() == self.id()
+                &&& half2.id() == self.id()
                 &&& half1@.log() == self@.log()
                 &&& half2@ == half1@
             }),
@@ -234,7 +235,8 @@ impl<T> LogResource<T> {
             old(self).id() == old(other).id(),
         ensures
             self@ is HalfAuthority,
-            self.id() == other.id() == old(self).id(),
+            self.id() == old(self).id(),
+            other.id() == old(self).id(),
             self@.log() == old(self)@.log() + seq![v],
             other@ == self@,
     {

examples/pcm/monotonic_counter.rs

@@ -240,7 +240,8 @@ impl MonotonicCounterResource {
             ({
                 let (r1, r2) = return_value;
                 let value = self@->FullRightToAdvance_value;
-                &&& r1.id() == r2.id() == self.id()
+                &&& r1.id() == self.id()
+                &&& r2.id() == self.id()
                 &&& r1@ == (MonotonicCounterResourceValue::HalfRightToAdvance { value })
                 &&& r2@ == r1@
             }),
@@ -281,7 +282,8 @@ impl MonotonicCounterResource {
             old(other)@ is HalfRightToAdvance,
         ensures
             old(self)@ == old(other)@,
-            self.id() == other.id() == old(self).id(),
+            self.id() == old(self).id(),
+            other.id() == old(self).id(),
             other@ == self@,
             self@ == (MonotonicCounterResourceValue::HalfRightToAdvance {
                 value: old(self)@->HalfRightToAdvance_value + 1,
@@ -339,7 +341,8 @@ fn main() {
     proof {
         half1.increment_using_two_halves(&mut half2);
     }
-    assert(half1.id() == half2.id() == id);
+    assert(half1.id() == id);
+    assert(half2.id() == id);
     assert(half1@.n() == half2@.n() == v1 + 1);
     assert(half1@.n() == 1);
     let tracked mut lower_bound = half1.extract_lower_bound();

examples/pcm/oneshot.rs

@@ -41,7 +41,8 @@
 //! ```
 //! let ghost id = half1.id();
 //! proof { half1.perform_using_two_halves(&mut half2); }
-//! assert(half1.id() == half2.id() == id);
+//! assert(half1.id() == id);
+//! assert(half2.id() == id);
 //! assert(half1@ is Complete);
 //! assert(half2@ is Complete);
 //! ```
@@ -173,7 +174,8 @@ impl OneShotResource {
                 let (half1, half2) = return_value;
                 &&& half1@ is HalfRightToComplete
                 &&& half2@ is HalfRightToComplete
-                &&& half2.id() == half1.id() == self.id()
+                &&& half1.id() == self.id()
+                &&& half2.id() == self.id()
             }),
     {
         let half = OneShotResourceValue::HalfRightToComplete {  };
@@ -219,7 +221,8 @@ impl OneShotResource {
             old(other)@ is HalfRightToComplete,
             self@ is Complete,
             other@ is Complete,
-            other.id() == self.id() == old(self).id(),
+            self.id() == old(self).id(),
+            other.id() == old(self).id(),
     {
         self.r.validate();
         other.r.validate();
@@ -277,11 +280,13 @@ fn main() {
     proof {
         half1.perform_using_two_halves(&mut half2);
     }
-    assert(half1.id() == half2.id() == id);
+    assert(half1.id() == id);
+    assert(half2.id() == id);
     assert(half1@ is Complete);
     assert(half2@ is Complete);
     let tracked knowledge = half1.duplicate();
-    assert(knowledge.id() == half1.id() == id);
+    assert(knowledge.id() == id);
+    assert(half1.id() == id);
     assert(knowledge@ is Complete);
 }
 

source/vstd/resource/lib.rs

@@ -114,7 +114,8 @@ pub proof fn split_mut<P: PCM>(tracked r: &mut Resource<P>, left: P, right: P) -
     requires
         old(r).value() == P::op(left, right),
     ensures
-        r.loc() == other.loc() == old(r).loc(),
+        r.loc() == old(r).loc(),
+        other.loc() == old(r).loc(),
         r.value() == left,
         other.value() == right,
 {
@@ -152,7 +153,8 @@ pub proof fn redistribute<P: PCM>(
         old(r1).loc() == old(r2).loc(),
         P::op(old(r1).value(), old(r2).value()) == P::op(v1, v2),
     ensures
-        r1.loc() == r2.loc() == old(r1).loc(),
+        r1.loc() == old(r1).loc(),
+        r2.loc() == old(r1).loc(),
         r1.value() == v1,
         r2.value() == v2,
 {
@@ -178,7 +180,8 @@ pub proof fn update_and_redistribute<P: PCM>(
         old(r1).loc() == old(r2).loc(),
         frame_preserving_update(P::op(old(r1).value(), old(r2).value()), P::op(v1, v2)),
     ensures
-        r1.loc() == r2.loc() == old(r1).loc(),
+        r1.loc() == old(r1).loc(),
+        r2.loc() == old(r1).loc(),
         r1.value() == v1,
         r2.value() == v2,
 {

source/vstd/resource/mod.rs

@@ -13,6 +13,7 @@ pub use lib::*;
 
 verus! {
 
-pub type Loc = int;
+#[derive(Eq, PartialEq)]
+pub struct Loc(int);
 
 } // verus!

source/vstd/tokens.rs

@@ -19,7 +19,7 @@ broadcast use {
 /// Unique identifier for every VerusSync instance.
 /// Every "Token" and "Instance" object has an `InstanceId`. These ID values must agree
 /// to perform any token operation.
-pub ghost struct InstanceId(pub int);
+pub type InstanceId = super::resource::Loc;
 
 /// Interface for VerusSync tokens created for a field marked with the
 /// `variable`, `option` or `persistent_option` strategies.