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/convert.rs

@@ -0,0 +1,77 @@
+use crate::*;
+
+/// Specifies that `From::from`, if implemented, is a pure method, allowing its usage in specs.
+/// This enables specifying the blanket impl of `Into` as calling `From::from`.
+///
+/// Does not apply to types that do not implement `Copy`, since pure methods can only involve `Copy` types.
+pub auto trait PureFrom {}
+
+#[extern_spec]
+trait From<T> {
+    #[refine_spec(where Self: Copy + PureFrom, T: Copy, [pure])]
+    fn from(other: T) -> Self;
+}
+
+#[extern_spec]
+impl<T, U> Into<U> for T
+where
+    U: From<T>,
+{
+    // When From is pure, we can use it to specify the behavior of Into
+    #[refine_spec(where U: Copy + PureFrom, T: Copy, [
+        pure,
+        ensures(result === U::from(self))
+    ])]
+    // FUTURE(where_equality): we can specify the behavior of Into for identity conversions even if impure, but for that we need equality constraints
+    // #[refine_spec(where T = U, [ensures(result === self)])]
+    fn into(self) -> U;
+}
+
+// identity conversion
+#[extern_spec]
+impl<T> From<T> for T {
+    #[ensures(result === other)]
+    #[refine_spec(where T: Copy, [pure])]
+    fn from(other: T) -> Self;
+}
+
+// numeric conversions
+
+// specifies From<T> for lossless numeric conversions using as casts
+macro_rules! specify_numeric_from {
+    ($from:ty => $($to:ty)*) => ($(
+        #[extern_spec]
+        impl From<$from> for $to {
+            #[pure]
+            #[ensures(result == num as Self)]
+            fn from(num: $from) -> Self;
+        }
+    )*)
+}
+
+specify_numeric_from!(bool => u8 i8 u16 i16 u32 i32 u64 i64 usize isize);
+
+specify_numeric_from!(u8 => u16 i16 u32 i32 u64 i64 usize);
+specify_numeric_from!(u16 => u32 i32 u64 i64);
+specify_numeric_from!(u32 => u64 i64);
+specify_numeric_from!(i8 => i16 i32 i64 isize);
+specify_numeric_from!(i16 => i32 i64);
+specify_numeric_from!(i32 => i64);
+// size is not guaranteed to be at least 32 or at most 64 bits, so not valid for many conversions one might expect
+
+// int-to-float conversions are exact when the int type has at most as many bits as the float's mantissa
+specify_numeric_from!(u8 => f32 f64);
+specify_numeric_from!(u16 => f32 f64);
+specify_numeric_from!(u32 => f64);
+specify_numeric_from!(i8 => f32 f64);
+specify_numeric_from!(i16 => f32 f64);
+specify_numeric_from!(i32 => f64);
+
+specify_numeric_from!(f32 => f64);
+
+#[cfg(version("1.26"))]
+specify_numeric_from!(i16 => isize);
+#[cfg(version("1.26"))]
+specify_numeric_from!(u16 => usize);
+#[cfg(version("1.26"))]
+specify_numeric_from!(u8 => isize);

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

@@ -0,0 +1,83 @@
+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(snapshot_equality(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 }
+
+// specify behavior for tuples (have to rely on PureDefault)
+
+// recursive like https://github.com/rust-lang/rust/blob/a5fa99eed20a46a88c0c85eed6552a94b6656634/library/core/src/tuple.rs#L10
+macro_rules! specify_tuple_default {
+    (impl $( $T:ident )*) => {
+        #[extern_spec]
+        impl<$($T,)*> Default for ($($T,)*) where
+            $($T: Default,)*
+        {
+            #[refine_spec(where
+                $($T: Copy + PureDefault,)*
+            [
+                pure,
+                ensures(snapshot_equality(&result, &($($T::default(),)*))),
+            ])]
+            fn default() -> Self;
+        }
+    };
+    (impls $T:ident $( $U:ident )+) => {
+        specify_tuple_default!(impl $T $($U)+);
+        specify_tuple_default!(impls $($U)+);
+    };
+    (impls $T:ident) => {
+        specify_tuple_default!(impl $T);
+    };
+}
+
+specify_tuple_default!(impls E D C B A Z Y X W V U T);
+
+// more specific types
+
+#[extern_spec]
+impl<T> Default for Option<T> {
+    #[refine_spec(where Self: Copy, [pure])]
+    #[ensures(result.is_none())]
+    fn default() -> Self;
+}

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

@@ -0,0 +1,88 @@
+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);
+
+#[refine_trait_spec]
+impl<T: KnownSize, const N: usize> KnownSize for [T; N] {
+    #[pure]
+    fn size() -> usize {
+        T::size() * N
+    }
+
+    #[pure]
+    fn align() -> usize {
+        T::align()
+    }
+}

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

@@ -0,0 +1,16 @@
+pub mod clone;
+pub mod convert;
+pub mod default;
+pub mod mem;
+pub mod ops;
+pub mod option;
+pub mod result;
+pub mod slice;
+
+// 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 convert::PureFrom;
+pub use default::PureDefault;
+pub use mem::KnownSize;

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

@@ -0,0 +1,14 @@
+#[allow(unused_imports)]
+use crate::*;
+
+#[allow(unused_imports)]
+use core::ops::Index;
+
+// FUTURE(#1221): This spec is currently not usable due to issue #1221.
+/*
+#[extern_spec]
+trait Index<Idx> {
+    #[pure]
+    fn index(&self, idx: Idx) -> &Self::Output;
+}
+*/

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

@@ -0,0 +1,3 @@
+pub mod index;
+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