From d7ce8c77fe527a0efcaa6cbfb384f06f22775934 Mon Sep 17 00:00:00 2001
From: Julian Dunskus <julian.dunskus@gmail.com>
Date: Fri, 3 Feb 2023 03:33:01 +0100
Subject: [PATCH] conditionalize std specs

---
 prusti-contracts/prusti-std/Cargo.toml               |  5 ++++-
 prusti-contracts/prusti-std/src/alloc_spec/mod.rs    |  4 ++--
 prusti-contracts/prusti-std/src/lib.rs               | 12 +++++++++++-
 .../prusti-std/src/{ => std_spec}/collections.rs     |  0
 prusti-contracts/prusti-std/src/std_spec/mod.rs      |  1 +
 5 files changed, 18 insertions(+), 4 deletions(-)
 rename prusti-contracts/prusti-std/src/{ => std_spec}/collections.rs (100%)
 create mode 100644 prusti-contracts/prusti-std/src/std_spec/mod.rs

diff --git a/prusti-contracts/prusti-std/Cargo.toml b/prusti-contracts/prusti-std/Cargo.toml
index dcd32a40031..1793ba19167 100644
--- a/prusti-contracts/prusti-std/Cargo.toml
+++ b/prusti-contracts/prusti-std/Cargo.toml
@@ -14,6 +14,9 @@ categories = ["development-tools", "development-tools::testing"]
 [dependencies]
 prusti-contracts = { path = "../prusti-contracts", version = "0.1.2" }
 
-# Forward "prusti" flag
 [features]
+default = ["alloc", "std"]
+alloc = []
+std = []
+# Forward "prusti" flag
 prusti = ["prusti-contracts/prusti"]
diff --git a/prusti-contracts/prusti-std/src/alloc_spec/mod.rs b/prusti-contracts/prusti-std/src/alloc_spec/mod.rs
index 50003f71cd4..88b18b9c830 100644
--- a/prusti-contracts/prusti-std/src/alloc_spec/mod.rs
+++ b/prusti-contracts/prusti-std/src/alloc_spec/mod.rs
@@ -1,5 +1,5 @@
-// In future, it might make sense to move these specs to yet another crate or have a feature to disable the std parts of this crate.
-// alloc is usable in some no_std environments, so it would be helpful to support the use case of core + alloc without std.
+// These specs can't be built-in like the core specs since some no_std crates may not even have an allocator.
+// Instead, prusti-std supports no_std through a feature.
 
 pub mod string;
 pub mod vec;
diff --git a/prusti-contracts/prusti-std/src/lib.rs b/prusti-contracts/prusti-std/src/lib.rs
index 1e327ce7f61..a67c1354035 100644
--- a/prusti-contracts/prusti-std/src/lib.rs
+++ b/prusti-contracts/prusti-std/src/lib.rs
@@ -1,6 +1,16 @@
 #![feature(allocator_api)] // to specify Vec
+#![no_std] // disable std by default
 
+// link to std if the feature is set
+#[cfg(feature = "std")]
+extern crate std;
+
+// Even alloc can be disabled for consistency with std, and in preparation for future specs for other, possibly no_std, crates.
+#[cfg(feature = "alloc")]
 extern crate alloc;
 
+// modules have a `_spec` suffix to avoid name conflicts with their crates.
+#[cfg(feature = "alloc")]
 pub mod alloc_spec;
-pub mod collections;
+#[cfg(feature = "std")]
+pub mod std_spec;
diff --git a/prusti-contracts/prusti-std/src/collections.rs b/prusti-contracts/prusti-std/src/std_spec/collections.rs
similarity index 100%
rename from prusti-contracts/prusti-std/src/collections.rs
rename to prusti-contracts/prusti-std/src/std_spec/collections.rs
diff --git a/prusti-contracts/prusti-std/src/std_spec/mod.rs b/prusti-contracts/prusti-std/src/std_spec/mod.rs
new file mode 100644
index 00000000000..2e4fe9b79c2
--- /dev/null
+++ b/prusti-contracts/prusti-std/src/std_spec/mod.rs
@@ -0,0 +1 @@
+pub mod collections;