Do not depend on crate alloc in no_std mode, by refactoring the use of the Perm type.

creusot-std/src/cell/permcell.rs

@@ -4,13 +4,13 @@
 //! track of the logical value.
 
 use crate::{
-    ghost::perm::{Container, Perm, SendPerm, SyncPerm},
+    ghost::{
+        NotObjective,
+        perm::{Perm, PermTarget},
+    },
     prelude::*,
 };
-use core::cell::UnsafeCell;
-
-#[cfg(not(feature = "std"))]
-use alloc::boxed::Box;
+use core::{cell::UnsafeCell, marker::PhantomData};
 
 /// Cell with ghost permissions
 ///
@@ -26,20 +26,16 @@ use alloc::boxed::Box;
 #[opaque]
 pub struct PermCell<T: ?Sized>(UnsafeCell<T>);
 
-impl<T: Sized> Container for PermCell<T> {
+impl<T: Sized> PermTarget for PermCell<T> {
     type Value = T;
+    type PermPayload = (NotObjective, PhantomData<T>);
 }
 
 #[trusted]
 unsafe impl<T> Send for PermCell<T> {}
 #[trusted]
 unsafe impl<T> Sync for PermCell<T> {}
 
-#[trusted]
-impl<T: Send> SendPerm for PermCell<T> {}
-#[trusted]
-impl<T: Sync> SyncPerm for PermCell<T> {}
-
 impl<T: Sized> Invariant for Perm<PermCell<T>> {
     #[logic(open, prophetic, inline)]
     #[creusot::trusted_trivial_if_param_trivial]
@@ -54,7 +50,7 @@ impl<T> PermCell<T> {
     #[check(terminates)]
     #[ensures(result.0 == *result.1.ward())]
     #[ensures((*result.1)@ == value)]
-    pub fn new(value: T) -> (Self, Ghost<Box<Perm<PermCell<T>>>>) {
+    pub fn new(value: T) -> (Self, Ghost<Perm<PermCell<T>>>) {
         let this = Self(UnsafeCell::new(value));
         let perm = Ghost::conjure();
         (this, perm)
@@ -107,7 +103,7 @@ impl<T> PermCell<T> {
     #[check(terminates)]
     #[requires(self == *perm.ward())]
     #[ensures(result == perm@)]
-    pub fn into_inner(self, perm: Ghost<Box<Perm<PermCell<T>>>>) -> T {
+    pub fn into_inner(self, perm: Ghost<Perm<PermCell<T>>>) -> T {
         let _ = perm;
         self.0.into_inner()
     }

creusot-std/src/ghost.rs

@@ -24,7 +24,7 @@ mod shared;
 
 pub use self::{
     fn_ghost::{FnGhost, FnGhostWrapper},
-    perm::Container,
+    perm::PermTarget,
     shared::GhostShared,
 };
 
@@ -300,4 +300,4 @@ define_objective! {}
 ///
 /// This negative implementation primarily targets `Perm<PermCell<T>>` and
 /// `Perm<*const T>`.
-pub(crate) struct NotObjective {}
+pub struct NotObjective {}

creusot-std/src/ghost/invariant.rs

@@ -40,7 +40,7 @@
 //!     }
 //! }
 //!
-//! struct PermCellNAInv<T>(Box<Perm<PermCell<T>>>);
+//! struct PermCellNAInv<T>(Perm<PermCell<T>>);
 //! impl<T: Invariant> Protocol for PermCellNAInv<T> {
 //!     type Public = Id;
 //!

creusot-std/src/ghost/perm.rs

@@ -1,25 +1,20 @@
 //! Generic permissions for accessing memory pointed to by pointers or within an interior mutable
 //! type.
 
+use crate::prelude::*;
 #[cfg(creusot)]
 use crate::resolve::structural_resolve;
-use crate::{ghost::NotObjective, prelude::*};
-use core::marker::PhantomData;
 
-pub trait Container {
+pub trait PermTarget {
     type Value: ?Sized;
+    type PermPayload: ?Sized;
 
     #[logic(open, inline)]
     fn is_disjoint(&self, _self_val: &Self::Value, other: &Self, _other_val: &Self::Value) -> bool {
         self != other
     }
 }
 
-#[trusted]
-pub trait SendPerm: Container {}
-#[trusted]
-pub trait SyncPerm: Container {}
-
 /// Token that represents the ownership of the contents of a container object. The container is
 /// either an interior mutable type (e.g., `Perm` or atomic types) or a raw pointer.
 ///
@@ -66,18 +61,9 @@ pub trait SyncPerm: Container {}
 /// Certain facts about the layout and alignment of pointers can be made available
 /// through the type invariant of [`crate::std::ptr::PtrLive`] by calling [`Perm::live`].
 #[opaque]
-pub struct Perm<C: ?Sized + Container>(
-    NotObjective,
-    #[allow(unused)] *mut (),
-    #[allow(unused)] [PhantomData<C::Value>],
-);
-
-#[trusted]
-unsafe impl<C: ?Sized + SendPerm> Send for Perm<C> {}
-#[trusted]
-unsafe impl<C: ?Sized + SyncPerm> Sync for Perm<C> {}
+pub struct Perm<C: ?Sized + PermTarget>(#[allow(unused)] C::PermPayload);
 
-impl<C: ?Sized + Container> Perm<C> {
+impl<C: ?Sized + PermTarget> Perm<C> {
     /// Returns the underlying container that is managed by this permission.
     #[logic(opaque)]
     pub fn ward<'a>(self) -> &'a C {
@@ -99,7 +85,7 @@ impl<C: ?Sized + Container> Perm<C> {
     pub fn disjoint_lemma(&mut self, other: &Self) {}
 }
 
-impl<C: ?Sized + Container> Resolve for Perm<C> {
+impl<C: ?Sized + PermTarget> Resolve for Perm<C> {
     #[logic(open, prophetic, inline)]
     #[creusot::trusted_trivial_if_param_trivial]
     fn resolve(self) -> bool {
@@ -114,7 +100,7 @@ impl<C: ?Sized + Container> Resolve for Perm<C> {
     fn resolve_coherence(self) {}
 }
 
-impl<C: ?Sized + Container<Value: Sized>> View for Perm<C> {
+impl<C: ?Sized + PermTarget<Value: Sized>> View for Perm<C> {
     type ViewTy = C::Value;
 
     #[logic(open, inline)]

creusot-std/src/lib.rs

@@ -45,10 +45,8 @@
 //!
 //! 7. [`prelude`][mod@prelude]: What you should import before doing anything with Creusot
 #![cfg_attr(feature = "nightly", allow(incomplete_features, internal_features))]
-#![cfg_attr(
-    feature = "nightly",
-    feature(step_trait, allocator_api, unboxed_closures, tuple_trait, edition_panic)
-)]
+#![cfg_attr(feature = "nightly", feature(step_trait, unboxed_closures, tuple_trait, edition_panic))]
+#![cfg_attr(all(feature = "nightly", feature = "std"), feature(allocator_api))]
 #![cfg_attr(
     creusot,
     feature(

creusot-std/src/std.rs

@@ -2,7 +2,6 @@
 mod array;
 mod bool;
 mod borrow;
-mod boxed;
 pub mod cell;
 pub mod char;
 pub mod clone;
@@ -20,13 +19,11 @@ pub mod option;
 pub mod panicking;
 pub mod ptr;
 pub mod range;
-pub mod rc;
 pub mod result;
 pub mod slice;
 pub mod string;
 pub mod time;
 mod tuples;
-pub mod vec;
 
 // Every std-dependent part of the Creusot Standard Library must be disabled when
 // compiling with [no_std].
@@ -36,15 +33,17 @@ pub mod collections {
     pub mod hash_map;
     pub mod hash_set;
 }
-
+#[cfg(feature = "std")]
+mod boxed;
 #[cfg(feature = "std")]
 pub mod deque;
-
 #[cfg(feature = "std")]
 pub mod io;
-
+#[cfg(feature = "std")]
+pub mod rc;
 #[cfg(feature = "std")]
 pub mod sync;
-
 #[cfg(feature = "std")]
 pub mod thread;
+#[cfg(feature = "std")]
+pub mod vec;

creusot-std/src/std/boxed.rs

@@ -2,13 +2,10 @@
 use crate::resolve::structural_resolve;
 use crate::{invariant::*, prelude::*};
 #[cfg(feature = "nightly")]
-use core::alloc::Allocator;
-
-#[cfg(not(feature = "std"))]
-use alloc::boxed::Box;
+use std::alloc::Allocator;
 
 #[cfg(creusot)]
-use core::ops::{Deref, DerefMut};
+use std::ops::{Deref, DerefMut};
 
 #[cfg(feature = "nightly")]
 impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A> {

creusot-std/src/std/convert.rs

@@ -1,8 +1,6 @@
 use crate::prelude::*;
 #[cfg(all(creusot, feature = "std"))]
-use alloc::alloc::Allocator;
-#[cfg(all(creusot, not(feature = "std")))]
-use alloc::boxed::Box;
+use std::alloc::Allocator;
 
 extern_spec! {
     mod core {
@@ -37,7 +35,10 @@ extern_spec! {
         #[ensures(result == Some(x))]
         fn from(x: T) -> Self;
     }
+}
 
+#[cfg(feature = "std")]
+extern_spec! {
     impl<T> From<T> for Box<T> {
         #[check(ghost)]
         #[ensures(*result == x)]
@@ -71,10 +72,7 @@ extern_spec! {
             Box::new(s)
         }
     }
-}
 
-#[cfg(feature = "std")]
-extern_spec! {
     impl<T: Clone> From<&[T]> for Vec<T>
     {
         // FIXME: inherit ghost/terminates from clone

creusot-std/src/std/deque.rs

@@ -5,7 +5,7 @@ use crate::prelude::*;
 use crate::{invariant::inv, resolve::structural_resolve};
 
 #[cfg(feature = "nightly")]
-use core::alloc::Allocator;
+use std::alloc::Allocator;
 #[cfg(feature = "nightly")]
 use std::collections::VecDeque;
 use std::collections::vec_deque::Iter;

creusot-std/src/std/ptr.rs

@@ -4,16 +4,16 @@ pub use self::nonnull::NonNullExt;
 #[cfg(creusot)]
 use crate::std::mem::{align_of_logic, size_of_logic, size_of_val_logic};
 use crate::{
-    ghost::perm::{Container, Perm},
+    ghost::{
+        NotObjective,
+        perm::{Perm, PermTarget},
+    },
     prelude::*,
 };
 use core::marker::PhantomData;
 #[cfg(creusot)]
 use core::ptr::Pointee;
 
-#[cfg(not(feature = "std"))]
-use alloc::boxed::Box;
-
 /// Metadata of a pointer in logic.
 ///
 /// [`std::ptr::metadata`] in logic.
@@ -519,8 +519,9 @@ extern_spec! {
     }
 }
 
-impl<T: ?Sized> Container for *const T {
+impl<T: ?Sized> PermTarget for *const T {
     type Value = T;
+    type PermPayload = (NotObjective, PhantomData<T>, [bool]);
 
     #[logic(open, inline)]
     fn is_disjoint(&self, self_val: &T, other: &Self, other_val: &T) -> bool {
@@ -547,6 +548,7 @@ impl<T: ?Sized> Perm<*const T> {
     /// cell initialized with `v`.
     #[check(terminates)] // can overflow the number of available pointer adresses
     #[ensures(*result.1.ward() == result.0 && *result.1.val() == v)]
+    #[cfg(feature = "std")]
     pub fn new(v: T) -> (*mut T, Ghost<Box<Perm<*const T>>>)
     where
         T: Sized,
@@ -559,6 +561,7 @@ impl<T: ?Sized> Perm<*const T> {
     #[check(terminates)] // can overflow the number of available pointer adresses
     #[ensures(*result.1.ward() == result.0 && *result.1.val() == *val)]
     #[erasure(Box::into_raw)]
+    #[cfg(feature = "std")]
     pub fn from_box(val: Box<T>) -> (*mut T, Ghost<Box<Perm<*const T>>>) {
         (Box::into_raw(val), Ghost::conjure())
     }
@@ -676,6 +679,7 @@ impl<T: ?Sized> Perm<*const T> {
     #[ensures(*result == *own.val())]
     #[allow(unused_variables)]
     #[erasure(Box::from_raw)]
+    #[cfg(feature = "std")]
     pub unsafe fn to_box(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) -> Box<T> {
         unsafe { Box::from_raw(ptr) }
     }
@@ -690,6 +694,7 @@ impl<T: ?Sized> Perm<*const T> {
     /// [type documentation](Perm).
     #[check(terminates)]
     #[requires(ptr as *const T == *own.ward())]
+    #[cfg(feature = "std")]
     pub unsafe fn drop(ptr: *mut T, own: Ghost<Box<Perm<*const T>>>) {
         let _ = unsafe { Self::to_box(ptr, own) };
     }

creusot-std/src/std/rc.rs

@@ -1,11 +1,11 @@
 use crate::prelude::*;
 #[cfg(creusot)]
 use crate::std::ptr::PointerExt as _;
-use alloc::rc::Rc;
-#[cfg(feature = "nightly")]
-use alloc::{alloc::Allocator, boxed::Box};
 #[cfg(creusot)]
-use core::ops::Deref;
+use std::ops::Deref;
+use std::rc::Rc;
+#[cfg(feature = "nightly")]
+use std::{alloc::Allocator, boxed::Box};
 
 /// Extension trait for [`Rc`].
 pub trait RcExt {

creusot-std/src/std/slice.rs

@@ -1,14 +1,14 @@
 #[cfg(creusot)]
 use crate::resolve::structural_resolve;
 use crate::{ghost::perm::Perm, invariant::*, logic::ops::IndexLogic, prelude::*};
-#[cfg(all(creusot, feature = "std"))]
-use core::alloc::Allocator;
 #[cfg(creusot)]
 use core::ops::{Index, IndexMut};
 use core::{
     ops::{Range, RangeFrom, RangeFull, RangeInclusive, RangeTo, RangeToInclusive},
     slice::*,
 };
+#[cfg(all(creusot, feature = "std"))]
+use std::alloc::Allocator;
 
 impl<T> Invariant for [T] {
     #[logic(open, prophetic)]

creusot-std/src/std/sync.rs

@@ -5,10 +5,10 @@ use std::sync::Arc;
 use crate::std::ptr::PointerExt as _;
 
 #[cfg(creusot)]
-use core::ops::Deref;
+use std::ops::Deref;
 
 #[cfg(feature = "nightly")]
-use core::alloc::Allocator;
+use std::alloc::Allocator;
 
 pub mod atomic;
 #[cfg(feature = "sc-drf")]
@@ -28,6 +28,7 @@ pub trait ArcExt {
     #[logic]
     fn as_ptr_logic(self) -> *const Self::Pointee;
 }
+
 #[cfg(feature = "nightly")]
 impl<T: ?Sized, A: Allocator> ArcExt for Arc<T, A> {
     type Pointee = T;