Convert more === to == (#2462)

Author: Chris-Hawblitzel

dependencies/syn/dev/main.rs

@@ -3,8 +3,8 @@ syn_dev::r#mod! {
 
     pub fn ref_mut_array_unsizing_coercion<T, const N: usize>(r: &mut [T; N]) -> (out: &mut [T])
     ensures
-        out.view() === old(r).view(),
-        final(out).view() === final(r).view(),
+        out.view() == old(r).view(),
+        final(out).view() == final(r).view(),
     opens_invariants none
     no_unwind
 {

dependencies/syn/src/expr.rs

@@ -2201,7 +2201,7 @@ pub(crate) mod parsing {
     // (i) without the diagnostic, syn's error message would otherwise be baffling
     //
     // (ii) this case is a little more relevant due to verus specifications in
-    //      function signatures, e.g., `requires x === Foo { a: 5 }` is not allowed
+    //      function signatures, e.g., `requires x == Foo { a: 5 }` is not allowed
     //      without additional parentheses.
     fn is_certainly_not_a_block(input: ParseStream) -> bool {
         let input = input.fork();

examples/guide/bst_map_generic.rs

@@ -700,9 +700,9 @@ fn vec_with_mut_refs(i: usize)
 
     *v[i] = 1;
 
-    assert(i == 0 ==> (a, b, c) === (1, 0, 0));
-    assert(i == 1 ==> (a, b, c) === (0, 1, 0));
-    assert(i == 2 ==> (a, b, c) === (0, 0, 1));
+    assert(i == 0 ==> (a, b, c) == (1, 0, 0));
+    assert(i == 1 ==> (a, b, c) == (0, 1, 0));
+    assert(i == 2 ==> (a, b, c) == (0, 0, 1));
 }
 // ANCHOR_END: vec_with_mut_refs_broken
 */
@@ -723,9 +723,9 @@ fn vec_with_mut_refs(i: usize)
     assert(has_resolved(v[1]));
     assert(has_resolved(v[2]));
 
-    assert(i == 0 ==> (a, b, c) === (1, 0, 0));
-    assert(i == 1 ==> (a, b, c) === (0, 1, 0));
-    assert(i == 2 ==> (a, b, c) === (0, 0, 1));
+    assert(i == 0 ==> (a, b, c) == (1, 0, 0));
+    assert(i == 1 ==> (a, b, c) == (0, 1, 0));
+    assert(i == 2 ==> (a, b, c) == (0, 0, 1));
 }
 // ANCHOR_END: vec_with_mut_refs
 
@@ -750,9 +750,9 @@ fn tree_map_with_mut_refs(i: u64)
         lemma_tree_map_has_resolved(tree_map, 2);
     }
 
-    assert(i == 0 ==> (a, b, c) === (1, 0, 0));
-    assert(i == 1 ==> (a, b, c) === (0, 1, 0));
-    assert(i == 2 ==> (a, b, c) === (0, 0, 1));
+    assert(i == 0 ==> (a, b, c) == (1, 0, 0));
+    assert(i == 1 ==> (a, b, c) == (0, 1, 0));
+    assert(i == 2 ==> (a, b, c) == (0, 0, 1));
 }
 // ANCHOR_END: tree_map_with_mut_refs
 

examples/scache/rwlock.rs

@@ -212,7 +212,7 @@ RwLock {
 
     transition!{
         take_exc_lock_finish_writeback(clean: bool) {
-            require pre.flag !== Flag::Writeback && pre.flag !== Flag::WritebackAndPendingExcLock;
+            require pre.flag != Flag::Writeback && pre.flag != Flag::WritebackAndPendingExcLock;
 
             remove exc_state -= Some(let ExcState::PendingAwaitWriteback{bucket, value});
             add exc_state += Some(ExcState::Pending{bucket, visited_count: 0, clean, value});
@@ -429,7 +429,7 @@ RwLock {
     transition!{
         shared_check_loading(bucket: BucketId) {
             require bucket < RC_WIDTH;
-            require pre.flag !== Flag::Loading;
+            require pre.flag != Flag::Loading;
 
             remove shared_state -= { SharedState::Pending2{bucket} };
             birds_eye let value = pre.storage.get_Some_0();
@@ -538,8 +538,8 @@ RwLock {
 
     pub open spec fn count_loading_refs(loading_state: Option<LoadingState>, match_bucket: BucketId) -> nat {
         match loading_state {
-            Some(LoadingState::PendingCounted{bucket}) => if bucket===Some(match_bucket) { 1 } else { 0 },
-            Some(LoadingState::Obtained{bucket}) => if bucket===Some(match_bucket) { 1 } else { 0 },
+            Some(LoadingState::PendingCounted{bucket}) => if bucket == Some(match_bucket) { 1 } else { 0 },
+            Some(LoadingState::Obtained{bucket}) => if bucket == Some(match_bucket) { 1 } else { 0 },
             _ => 0
         }
     }
@@ -650,7 +650,7 @@ RwLock {
                     Some(LoadingState::PendingCounted{..}) => false,
                     _ => true
                 }
-                &&& self.flag !== Flag::Unmapped
+                &&& self.flag != Flag::Unmapped
             }
             SharedState::Obtained{bucket, value} => {
                 &&& Some(value) == self.storage
@@ -660,7 +660,7 @@ RwLock {
                     _ => true
                 }
                 &&& self.loading_state.is_None()
-                &&& self.flag !== Flag::Unmapped
+                &&& self.flag != Flag::Unmapped
             }
         }
     }
@@ -853,7 +853,7 @@ RwLock {
         // shared_storage_invariant
         let new_ss = SharedState::Obtained{bucket: pre_exc.get_Obtained_bucket().get_Some_0(), value};
         assert forall |ss| post.shared_state.count(ss) > 0 implies post.shared_state_valid(ss) by {
-            if ss !== new_ss {
+            if ss != new_ss {
                 assert(pre.shared_state_valid(ss));
             }
         }

examples/state_machines/interner.rs

@@ -30,7 +30,7 @@ tokenized_state_machine! {InternSystem<T> {
 
     transition!{
         insert(val: T) {
-            require(forall |i: int| 0 <= i && i < pre.auth.len() ==> pre.auth.index(i) !== val);
+            require(forall |i: int| 0 <= i && i < pre.auth.len() ==> pre.auth.index(i) != val);
             update auth = pre.auth.push(val);
         }
     }
@@ -72,7 +72,7 @@ tokenized_state_machine! {InternSystem<T> {
             0 <= j && j < self.auth.len() &&
             i != j
             ==>
-            self.auth.index(i) !== self.auth.index(j)
+            self.auth.index(i) != self.auth.index(j)
     }
 
     #[inductive(empty)]

examples/state_machines/petersons_algorithm.rs

@@ -30,7 +30,7 @@ tokenized_state_machine! { Petersons<T> {
         &&& (self.thread_1 == ThreadState::Idle) <==> !self.flag_1
         &&& !(self.thread_0 == ThreadState::Critical && self.thread_1 == ThreadState::Critical)
         &&& self.storage.is_Some() <==>
-            (self.thread_0 !== ThreadState::Critical && self.thread_1 !== ThreadState::Critical)
+            (self.thread_0 != ThreadState::Critical && self.thread_1 != ThreadState::Critical)
         &&& self.thread_0 == ThreadState::Critical && self.turn == 1 ==> self.thread_1 == ThreadState::Idle || self.thread_1 == ThreadState::SetFlag
         &&& self.thread_1 == ThreadState::Critical && self.turn == 0 ==> self.thread_0 == ThreadState::Idle || self.thread_0 == ThreadState::SetFlag
         &&& self.turn == 0 || self.turn == 1

examples/state_machines/tutorial/fifo.rs

@@ -354,7 +354,7 @@ tokenized_state_machine!{FifoQueue<T> {
             assert(post.storage.dom().contains(i));
             /*
             assert(
-                post.storage.index(i).id() ===
+                post.storage.index(i).id() ==
                 post.backing_cells.index(i)
             );
             assert(if post.in_active_range(i) {
@@ -399,7 +399,7 @@ tokenized_state_machine!{FifoQueue<T> {
             } else {
                 assert(post.storage.dom().contains(i));
                 assert(
-                    post.storage.index(i).id() ===
+                    post.storage.index(i).id() ==
                     post.backing_cells.index(i)
                 );
                 assert(if post.in_active_range(i) {
@@ -423,7 +423,7 @@ tokenized_state_machine!{FifoQueue<T> {
         let head = pre.consumer.get_Consuming_0();
         assert(post.storage.dom().contains(head));
         assert(
-                post.storage.index(head).id() ===
+                post.storage.index(head).id() ==
                 post.backing_cells.index(head as int)
             );
         assert(if post.in_active_range(head) {
@@ -472,7 +472,7 @@ struct_with_invariants!{
             // The Cell IDs in the instance protocol match the cell IDs in the actual vector:
             &&& self.instance@.backing_cells().len() == self.buffer@.len()
             &&& forall|i: int| 0 <= i && i < self.buffer@.len() as int ==>
-                self.instance@.backing_cells().index(i) ===
+                self.instance@.backing_cells().index(i) ==
                     self.buffer@.index(i).id()
         }
 

examples/syntax.rs

@@ -361,7 +361,7 @@ pub(crate) proof fn binary_ops<A>(a: A, x: int) {
     assert(false <== false <== false);
     assert(!(false <== (false <== false)));
     assert((false <== false) <== false);
-    assert(2 + 2 !== 3);
+    assert(2 + 2 != 3);
     assert(a == a);
     assert(false <==> true && false);
 }

source/rust_verify_test/tests/adts.rs

@@ -524,7 +524,7 @@ test_verify_one_file! {
 
         fn test() -> (s: (S, S))
             ensures
-                s.0 === s.1,
+                s.0 == s.1,
         {
 
             let s1 = S { a: 10, b: Ghost(20) };
@@ -548,7 +548,7 @@ test_verify_one_file! {
         fn test() {
             let s1 = S { a: 10, b: Ghost(20) };
             let s2 = S { a: 10, b: Ghost(30) };
-            assert(s1 === s2); // FAILS
+            assert(s1 == s2); // FAILS
         }
     } => Err(e) => assert_one_fails(e)
 }

source/rust_verify_test/tests/closures.rs

@@ -44,7 +44,7 @@ test_verify_one_file! {
 
         proof fn testfun<A>(a: A, b: bool) {
             let aa = polytestfun(a, |x: A, y: A| (if b { x } else { y }));
-            assert(a === aa);
+            assert(a == aa);
         }
 
         spec fn specf(x: u32, f: spec_fn(u32) -> u32) -> u32 {