Edits necessary to get things working once the verus crate-rename lands

verified-node-replication/src/constants.rs

@@ -5,8 +5,8 @@
 //! verification. The constants mostly define the size of the log, and certain thresholds
 //! when warnings are being printed etc.
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 verus! {
 

verified-node-replication/src/exec/context.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{
     atomic_ghost::AtomicU64,

verified-node-replication/src/exec/log.rs

@@ -1,6 +1,6 @@
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{
     atomic_ghost::{AtomicBool, AtomicU64},

verified-node-replication/src/exec/mod.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 

verified-node-replication/src/exec/replica.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{
     atomic_ghost::AtomicU64,

verified-node-replication/src/exec/rwlock.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 use vstd::{
     atomic_ghost::{AtomicBool, AtomicU64},
     atomic_with_ghost,

verified-node-replication/src/exec/utils.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::{prelude::*, seq::Seq};
 

verified-node-replication/src/lib.rs

@@ -8,8 +8,8 @@
 //!
 //! This top-level module contains the trusted traits and the top-level lemmas.
 #[allow(unused_imports)]
-use builtin::*;
-use state_machines_macros::state_machine;
+use verus_builtin::*;
+use verus_state_machines_macros::state_machine;
 use vstd::prelude::*;
 
 pub mod constants;

verified-node-replication/src/spec/cyclicbuffer.rs

@@ -2,14 +2,14 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 
 use vstd::cell::{CellId, PointsTo};
 
-use state_machines_macros::*;
+use verus_state_machines_macros::*;
 
 use crate::Dispatch;
 

verified-node-replication/src/spec/flat_combiner.rs

@@ -2,12 +2,12 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 
-use state_machines_macros::*;
+use verus_state_machines_macros::*;
 
 use super::types::*;
 // use super::utils::*;

verified-node-replication/src/spec/linearization.rs

@@ -3,7 +3,7 @@
 //
 // The Linearization Proof
 #[allow(unused_imports)]
-use builtin::*;
+use verus_builtin::*;
 // use vstd::*;
 use vstd::prelude::*;
 

verified-node-replication/src/spec/rwlock.rs

@@ -2,9 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
-use state_machines_macros::tokenized_state_machine;
+use verus_builtin::*;
+use verus_builtin_macros::*;
+use verus_state_machines_macros::tokenized_state_machine;
 use vstd::{multiset::*, prelude::*};
 
 verus! {

verified-node-replication/src/spec/simple_log.rs

@@ -1,9 +1,9 @@
 // Verified Node Replication Library
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-use builtin::*;
-use builtin_macros::*;
-use state_machines_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
+use verus_state_machines_macros::*;
 
 use vstd::prelude::*;
 

verified-node-replication/src/spec/types.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use crate::Dispatch;
 

verified-node-replication/src/spec/unbounded_log.rs

@@ -3,9 +3,9 @@
 //
 // rust_verify/tests/example.rs ignore
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
-use state_machines_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
+use verus_state_machines_macros::*;
 
 use vstd::map::Map;
 use vstd::prelude::*;

verified-node-replication/src/spec/unbounded_log_refines_simplelog.rs

@@ -3,8 +3,8 @@
 //
 // rust_verify/tests/example.rs ignore
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 
@@ -15,7 +15,7 @@ use vstd::seq::Seq;
 use vstd::seq_lib::*;
 
 #[cfg(verus_keep_ghost)]
-use state_machines_macros::*;
+use verus_state_machines_macros::*;
 
 use crate::{Dispatch, InputOperation, OutputOperation, ReqId};
 

verified-node-replication/src/spec/utils.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
 #[allow(unused_imports)]
-use builtin::*;
-use builtin_macros::*;
+use verus_builtin::*;
+use verus_builtin_macros::*;
 
 use vstd::prelude::*;
 use vstd::set::Set;