no std allowed

flux_support/src/extern_specs/iter.rs

@@ -1,6 +1,6 @@
 #![allow(unused)]
 use crate::assert;
-use std::slice::Iter;
+use std::slice::Iter; // TODO: not allowed to use std
 
 #[flux_rs::extern_spec(std::slice)]
 #[flux_rs::refined_by(idx: int, len: int)]

flux_support/src/extern_specs/slice.rs

@@ -1,5 +1,5 @@
 #![allow(unused)]
-use std::slice::{Iter, SliceIndex};
+use std::slice::{Iter, SliceIndex}; // TODO: not allowed to use std
 
 // #[flux_rs::extern_spec]
 // #[generics(Self as base, T as base)]

flux_support/src/flux_ptr.rs

@@ -1,11 +1,19 @@
+use core::clone::Clone;
+use core::cmp::Eq;
+use core::cmp::PartialEq;
 use core::cmp::PartialOrd;
 use core::convert::From;
+use core::fmt::Debug;
+use core::marker::Copy;
 use core::ops::{Deref, DerefMut};
 use core::option::Option;
 use core::option::Option::Some;
+use core::prelude::rust_2021::derive;
 use core::ptr::NonNull;
+use core::todo;
+use core::unimplemented;
 use flux_rs::{refined_by, sig};
-use std::ops::Rem;
+use std::ops::Rem; // TODO: not allowed to use std
 
 #[flux_rs::opaque]
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]

flux_support/src/flux_range.rs

@@ -1,3 +1,10 @@
+use core::clone::Clone;
+use core::cmp::Eq;
+use core::cmp::PartialEq;
+use core::fmt::Debug;
+use core::marker::Copy;
+use core::prelude::rust_2021::derive;
+
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 #[flux_rs::refined_by(start: int, end: int)]
 pub struct FluxRange {

flux_support/src/flux_register_interface.rs

@@ -1,5 +1,9 @@
 // VTOCK-TODO: how to do defs without breaking compilation
+use core::clone::Clone;
+use core::marker::Copy;
 use core::ops::{Add, AddAssign};
+use core::prelude::rust_2021::derive;
+use core::unimplemented;
 pub use tock_registers::debug;
 pub use tock_registers::fields::TryFromValue;
 use tock_registers::fields::{Field, FieldValue};