Provide Specs for the Standard Library

prusti-contracts/prusti-contracts/src/core_spec/clone.rs

@@ -0,0 +1,12 @@
+use crate::*;
+
+#[extern_spec]
+trait Clone {
+    #[ghost_constraint(Self: SnapshotEqualClone, [
+		ensures(result === self),
+	])]
+    fn clone(&self) -> Self;
+}
+
+/// Specifies that `Clone::clone`, if implemented, preserves snapshot equality (`===`).
+pub auto trait SnapshotEqualClone {}

prusti-contracts/prusti-contracts/src/core_spec/default.rs

@@ -0,0 +1,45 @@
+use crate::*;
+
+#[extern_spec]
+trait Default {
+    #[ghost_constraint(Self: Copy + PureDefault, [pure])]
+    fn default() -> Self;
+}
+
+/// Specifies that `Default::default`, if implemented, is a pure method, allowing its usage in specs.
+///
+/// Does not apply to types that do not implement `Copy`, since pure methods can only involve `Copy` types.
+pub auto trait PureDefault {}
+
+// analogous to https://github.com/rust-lang/rust/blob/872631d0f0fadffe3220ab1bd9c8f1f2342341e2/library/core/src/default.rs#L190-L202
+macro_rules! default_spec {
+    ($t:ty, $v:expr) => {
+        #[extern_spec]
+        impl Default for $t {
+            #[pure]
+            #[ensures(result == $v)]
+            fn default() -> Self;
+        }
+    };
+}
+
+default_spec! { (), () }
+default_spec! { bool, false }
+default_spec! { char, '\x00' }
+
+default_spec! { usize, 0 }
+default_spec! { u8, 0 }
+default_spec! { u16, 0 }
+default_spec! { u32, 0 }
+default_spec! { u64, 0 }
+default_spec! { u128, 0 }
+
+default_spec! { isize, 0 }
+default_spec! { i8, 0 }
+default_spec! { i16, 0 }
+default_spec! { i32, 0 }
+default_spec! { i64, 0 }
+default_spec! { i128, 0 }
+
+default_spec! { f32, 0.0f32 }
+default_spec! { f64, 0.0f64 }

prusti-contracts/prusti-contracts/src/core_spec/mem.rs

@@ -0,0 +1,65 @@
+use crate::*;
+
+#[extern_spec]
+mod core {
+    mod mem {
+        use crate::*;
+
+        #[pure]
+        #[ghost_constraint(T: core_spec::mem::KnownSize, [ensures(result == T::size())])]
+        fn size_of<T>() -> usize;
+
+        #[pure]
+        #[ghost_constraint(T: core_spec::mem::KnownSize, [ensures(result == T::align())])]
+        fn align_of<T>() -> usize;
+
+        #[ensures(*x === old(snap(y)) && *y === old(snap(x)))]
+        fn swap<T>(x: &mut T, y: &mut T);
+    }
+}
+
+pub trait KnownSize {
+    #[pure]
+    fn size() -> usize;
+
+    #[pure]
+    fn align() -> usize;
+}
+
+macro_rules! known_size_spec {
+    ($t:ty, $size:expr, $align:expr) => {
+        #[refine_trait_spec]
+        impl KnownSize for $t {
+            #[pure]
+            #[ensures(result == $size)]
+            fn size() -> usize {
+                $size
+            }
+
+            #[pure]
+            #[ensures(result == $align)]
+            fn align() -> usize {
+                $align
+            }
+        }
+    };
+}
+
+known_size_spec!(bool, 1, 1);
+
+known_size_spec!(i8, 1, 1);
+known_size_spec!(i16, 2, 2);
+known_size_spec!(i32, 4, 4);
+known_size_spec!(i64, 8, 8);
+known_size_spec!(i128, 16, 16);
+
+known_size_spec!(u8, 1, 1);
+known_size_spec!(u16, 2, 2);
+known_size_spec!(u32, 4, 4);
+known_size_spec!(u64, 8, 8);
+known_size_spec!(u128, 16, 16);
+
+known_size_spec!(f32, 4, 4);
+known_size_spec!(f64, 8, 8);
+
+// usize/isize are not specified exactly because they are platform-dependent and programmers should not depend on their specific values anyway.

prusti-contracts/prusti-contracts/src/core_spec/mod.rs

@@ -0,0 +1,11 @@
+pub mod default;
+pub mod option;
+pub mod result;
+pub mod clone;
+pub mod mem;
+
+// NOTE: specs marked with FUTURE are not fully expressible yet (in a clean way).
+// They are due to be revised later as features are added.
+
+pub use clone::SnapshotEqualClone;
+pub use default::PureDefault;

prusti-contracts/prusti-contracts/src/core_spec/ops/try.rs

@@ -0,0 +1,34 @@
+use crate::*;
+
+#[allow(unused_imports)]
+use core::ops::*;
+#[allow(unused_imports)]
+use std::convert::Infallible;
+
+#[extern_spec]
+impl<T, E> Try for Result<T, E> {
+    #[ensures(result === Ok(output))]
+    fn from_output(output: T) -> Self;
+
+    #[ensures(match old(self) {
+		Ok(output) => result === ControlFlow::Continue(output),
+		Err(error) => result === ControlFlow::Break(Err(error)),
+	})]
+    fn branch(self) -> ControlFlow<Result<Infallible, E>, T>;
+}
+
+#[extern_spec]
+impl<T> Try for Option<T> {
+    #[ensures(result === Some(output))]
+    fn from_output(output: T) -> Self;
+
+    #[ensures(match old(self) {
+		Some(output) => result === ControlFlow::Continue(output),
+		//None => result === ControlFlow::Break(None),
+		None => match result {
+			ControlFlow::Break(residual) => residual.is_none(),
+			_ => false,
+		},
+	})]
+    fn branch(self) -> ControlFlow<Option<Infallible>, T>;
+}