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 {
+    #[refine_spec(where 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 {
+    #[refine_spec(where 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,75 @@
+use crate::*;
+
+#[extern_spec(core)]
+mod mem {
+    #[pure]
+    #[refine_spec(where T: KnownSize, [ensures(result == T::size())])]
+    fn size_of<T>() -> usize;
+
+    #[pure]
+    #[refine_spec(where T: 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]
+            fn size() -> usize {
+                $size
+            }
+
+            #[pure]
+            fn align() -> usize {
+                $align
+            }
+        }
+    };
+    ($t:ty, $size:expr) => {
+        known_size_spec!($t, $size, $size);
+    };
+}
+
+known_size_spec!(bool, 1);
+
+known_size_spec!(i8, 1);
+known_size_spec!(i16, 2);
+known_size_spec!(i32, 4);
+known_size_spec!(i64, 8);
+known_size_spec!(i128, 16);
+
+known_size_spec!(u8, 1);
+known_size_spec!(u16, 2);
+known_size_spec!(u32, 4);
+known_size_spec!(u64, 8);
+known_size_spec!(u128, 16);
+
+known_size_spec!(f32, 4);
+known_size_spec!(f64, 8);
+
+#[cfg(target_pointer_width = "16")]
+known_size_spec!(usize, 2);
+#[cfg(target_pointer_width = "16")]
+known_size_spec!(isize, 2);
+
+#[cfg(target_pointer_width = "32")]
+known_size_spec!(usize, 4);
+#[cfg(target_pointer_width = "32")]
+known_size_spec!(isize, 4);
+
+#[cfg(target_pointer_width = "64")]
+known_size_spec!(usize, 8);
+#[cfg(target_pointer_width = "64")]
+known_size_spec!(isize, 8);

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

@@ -0,0 +1,12 @@
+pub mod clone;
+pub mod default;
+pub mod mem;
+pub mod ops;
+pub mod option;
+pub mod result;
+
+// 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/mod.rs

@@ -0,0 +1,2 @@
+pub mod ref_forwarding;
+pub mod r#try;

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

@@ -0,0 +1,65 @@
+use crate::*;
+
+#[allow(unused_imports)]
+use core::ops::*;
+
+macro_rules! specify_ref_op {
+    (impl $trait:tt fn $name:ident as $op:tt for $($t:ty)*) => ($(
+        #[extern_spec]
+        impl $trait<$t> for &$t {
+            #[pure]
+            #[ensures(result == *self $op other)]
+            fn $name(self, other: $t) -> $t;
+        }
+
+        #[extern_spec]
+        impl $trait<&$t> for $t {
+            #[pure]
+            #[ensures(result == self $op *other)]
+            fn $name(self, other: &$t) -> $t;
+        }
+
+        #[extern_spec]
+        impl $trait<&$t> for &$t {
+            #[pure]
+            #[ensures(result == *self $op *other)]
+            fn $name(self, other: &$t) -> $t;
+        }
+    )*)
+}
+
+specify_ref_op! { impl Add fn add as + for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op! { impl Sub fn sub as - for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op! { impl Mul fn mul as * for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op! { impl Div fn div as / for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op! { impl Rem fn rem as % for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+
+// FUTURE(bitvectors): bitwise operations on non-boolean types are experimental (`encode_bitvectors` to enable). could specify: usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128
+specify_ref_op! { impl BitAnd fn bitand as & for bool }
+specify_ref_op! { impl BitOr fn bitor as | for bool }
+specify_ref_op! { impl BitXor fn bitxor as ^ for bool }
+
+// FUTURE(bitvectors): left/right shifts. these will need special care since LHS and RHS may have different types
+
+macro_rules! specify_ref_op_assign {
+    (impl $trait:tt fn $name:ident as $op:tt for $($t:ty)*) => ($(
+        #[extern_spec]
+        impl $trait<&$t> for $t {
+            #[ensures(*self == old(*self) $op *other)]
+            fn $name(&mut self, other: &$t);
+        }
+    )*)
+}
+
+specify_ref_op_assign! { impl AddAssign fn add_assign as + for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op_assign! { impl SubAssign fn sub_assign as - for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op_assign! { impl MulAssign fn mul_assign as * for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op_assign! { impl DivAssign fn div_assign as / for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+specify_ref_op_assign! { impl RemAssign fn rem_assign as % for usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128 f32 f64 }
+
+// FUTURE(bitvectors): bitwise operations on non-boolean types are experimental (`encode_bitvectors` to enable). could specify: usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128
+specify_ref_op_assign! { impl BitAndAssign fn bitand_assign as & for bool }
+specify_ref_op_assign! { impl BitOrAssign fn bitor_assign as | for bool }
+specify_ref_op_assign! { impl BitXorAssign fn bitxor_assign as ^ for bool }
+
+// FUTURE(bitvectors): left/right shifts. these will need special care since LHS and RHS may have different types

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

@@ -0,0 +1,34 @@
+use crate::*;
+
+#[allow(unused_imports)]
+use core::convert::Infallible;
+#[allow(unused_imports)]
+use core::ops::*;
+
+#[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>;
+}